Library nbe_tests


Require Import syntax.
Require Import nbe_cbv_atomic.
Require Import nbe_cbn_atomic.


Parameter a b:atoms.

Definition nbe_v := nbe_cbv_atomic.Completeness.NbE.
Definition nbe_n := nbe_cbn_atomic.Completeness.NbE.

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

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

Definition NbE {A} : proof nil false A -> bare * bare := fun p => (NbE_v p, NbE_n p).

Some tests of the normalization algorithm
\x.<(\y.y)(Sk.x)>
Definition test_16 : proof nil false (Func Bot Bot).

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

\x.<<<(\y.y)(Sk.x)>>>
Definition test_17 : proof nil false (Func Bot Bot).

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

\x.<<xy>>
Definition test_18 : proof nil false (Func (Func Bot Bot) (Func Bot Bot)).

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

\xy.<x(Sk.k(ky))>
Definition test_19 : proof nil false (Func (Func Bot Bot) (Func Bot Bot)).

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

\xy.<(\a.<xa>)<xy>>
Definition test_19' : proof nil false (Func (Func Bot Bot) (Func Bot Bot)).

Eval compute in (forget_proof test_19').
Eval compute in (NbE_v test_19').

\xy.<x<x(Sk.k(ky))>>
Definition test_20 : proof nil false (Func (Func Bot Bot) (Func Bot Bot)).

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

\xy.<(Sk.ky)x>
Definition test_21 : proof nil false (Func Bot (Func (Func Bot Bot) Bot)).

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

\xy.<<yx>>
Definition test_21' : proof nil false (Func Bot (Func (Func Bot Bot) Bot)).

Eval compute in (forget_proof test_21').
Eval compute in (NbE_v test_21').

\xy.<yx>
Definition test_21'' : proof nil false (Func Bot (Func (Func Bot Bot) Bot)).

Eval compute in (forget_proof test_21'').
Eval compute in (NbE_n test_21'').

\xyz. <(Sk.y(kz))(Sk'.z(k'x))>
Definition test_22 : proof nil false (Func Bot (Func (Func Bot Bot) (Func (Func Bot Bot) Bot))).

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

\xyz. <y<z<zx>>>
Definition test_22' : proof nil false (Func Bot (Func (Func Bot Bot) (Func (Func Bot Bot) Bot))).

Eval compute in (forget_proof test_22').
Eval compute in (NbE_v test_22').

\xyz. <y<z(Sk'.z(k'x))>>
Definition test_22'' : proof nil false (Func Bot (Func (Func Bot Bot) (Func (Func Bot Bot) Bot))).

Eval compute in (forget_proof test_22'').
Eval compute in (NbE_n test_22'').

\xy.<case x of (z.Sk.kz || z.z)
Definition test_23 : proof nil false (Func (Sum Bot Bot) (Func Bot Bot)).

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

Implicational version of DNS
Definition test_DNS_imp : proof nil false
  (Func
    (Func (Atom a) (Func (Func (Atom a) Bot) Bot))
    (Func (Func (Func (Atom a) (Atom a)) Bot) Bot)).

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

Implicational version of DNS (sums instead of functions)
Definition test_DNS_sums : proof nil false
                            (Func (Func (Sum (Atom a) (Func (Atom a) Bot)) Bot) Bot).

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

Implicational version of DNS (sums instead of functions) + simulating quantifier
Definition test_DNS_sums_quant : proof nil false
                            (Func (Func (Func (Atom b) (Sum (Atom a) (Func (Atom a) Bot))) Bot) Bot).

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

This page has been generated by coqdoc