Library nbe_tests


Require Import syntax.
Require Import nbe_cbv_atomic.


Parameter a:atoms.

Definition nbe_v := nbe_cbv_atomic.Completeness.NbE.

Check nbe_v.

Definition NbE {A} : proof nil false A -> bare := fun p => forget_proof (forget_nf (nbe_v p)).

Some tests of the normalization algorithm

Definition id8 : proof nil false (Func Nat (Func Nat Nat)).

Eval compute in (forget_proof id8).
Eval compute in (NbE id8).

Definition id9 : proof nil false (Func Nat Nat).

Eval compute in (forget_proof id9).
Eval compute in (NbE id9).

Definition id10 : proof nil false (Func Nat Nat).

Eval compute in (forget_proof id10).
Eval compute in (NbE id10).

Definition id11 : proof nil false (Func (Func Nat Nat) (Func Nat Nat)).

Eval compute in (forget_proof id11).
Eval compute in (NbE id11).

Definition id13 : proof nil false (Func (Func Nat Nat) (Func Nat Nat)).

Eval compute in (forget_proof id13).
Eval compute in (NbE id13).

Definition id14 : proof nil false (Func (Func Nat Nat) (Func Nat Nat)).

Eval compute in (forget_proof id14).
Eval compute in (NbE id14).

Definition id16 : proof nil false (Func (Func Nat Nat) (Func (Func Nat (Func Nat Nat)) (Func Nat Nat))).

Eval compute in (forget_proof id16).
Eval compute in (NbE id16).

Definition id19 : proof nil false
  (Func (Func Nat Nat)
       (Func (Func Nat Nat)
            (Func (Func Nat Nat) (Func Nat Nat)))).

Eval compute in (forget_proof id19).
Eval compute in (NbE id19).

Definition id21 : proof nil false (Func (Sum Nat Nat) (Func Nat Nat)).

Eval compute in (forget_proof id21).
Eval vm_compute in (NbE id21).



Now some tests with numbers

Definition test22 : proof nil false Nat.

Eval compute in (forget_proof test22).
Eval compute in (NbE test22).

Definition test23 : proof nil false (Func Nat Nat).

Eval compute in (forget_proof test23).
Eval compute in (NbE test23).

Definition test24 : proof nil false (Func Nat Nat).

Eval compute in (forget_proof test24).
Eval compute in (NbE test24).

Definition test25 : proof nil false (Func Nat Nat).

Eval compute in (forget_proof test25).
Eval compute in (NbE test25).

Definition test26 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).


This is blocking becaus A is a paramter, to investigate futher...

Eval compute in (forget_proof test26).
Eval compute in (NbE test26).

Definition test27 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).

Eval compute in (forget_proof test27).
Eval compute in (NbE test27).

Definition test28 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).

Eval compute in (forget_proof test28).
Eval compute in (NbE test28).

Definition test29 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).

Eval compute in (forget_proof test29).
Eval compute in (NbE test29).


This page has been generated by coqdoc