Tealeaves.Examples.VariadicLet.Demo
From Tealeaves Require
Examples.VariadicLet.Terms
Examples.VariadicLet.Instances.Simple
Examples.VariadicLet.Instances.Tele
Examples.VariadicLet.Instances.LetRec.
Import Terms.
Parameters (x y z: atom).
Definition term1: term LN :=
letin [tvar (Fr x)] (tvar (Bd 0)).
Definition term2: term LN :=
letin [tvar (Bd 0)] (tvar (Bd 0)).
Definition term3: term LN :=
letin [tvar (Fr x); tvar (Bd 0)] (tvar (Bd 0)).
Definition term4: term LN :=
letin [tvar (Fr x); tvar (Bd 1)] (tvar (Bd 0)).
Definition term5: term LN :=
letin [tvar (Fr x); tvar (Bd 0) ; tvar (Bd 1)] (tvar (Bd 2)).
Definition term6: term LN :=
letin [tvar (Bd 1) ; tvar (Bd 2) ; tvar (Bd 3)] (tvar (Bd 2)).
Definition compute_which_are_closed `{mapdt: Mapdt nat term}: list bool :=
map (LCb (Mapdt_U := mapdt)) [term1; term2; term3; term4; term5; term6].
Definition compute_column_of_table `{mapdt: Mapdt nat term}: list nat :=
map (level (Mapdt_U := mapdt)) [term1; term2; term3; term4; term5; term6].
Section JAR_table.
Compute compute_column_of_table (mapdt := Simple.Mapdt_term).
(* = 0; 1; 1; 2; 2; 4 *)
Compute compute_column_of_table (mapdt := Tele.Mapdt_term).
(* = 0; 1; 0; 1; 0; 2 *)
Compute compute_column_of_table (mapdt := LetRec.Mapdt_term).
(* = 0; 0; 0; 0; 0; 1 *)
End JAR_table.
Compute compute_which_are_closed (mapdt := Simple.Mapdt_term).
(* = true; false; false; false; false; false *)
Compute compute_which_are_closed (mapdt := Tele.Mapdt_term).
(* = true; false; true; false; true; false *)
Compute compute_which_are_closed (mapdt := LetRec.Mapdt_term).
(* = true; true; true; true; true; false *)
Module demo1.
Import Simple.
Goal LCnb 0 term1 = true. reflexivity. Qed.
Goal LCnb 0 term2 = false. reflexivity. Qed.
Goal LCnb 1 term2 = true. reflexivity. Qed.
Goal LCnb 0 term4 = false. reflexivity. Qed.
Goal LCnb 1 term4 = false. reflexivity. Qed.
Goal LCnb 0 term6 = false. reflexivity. Qed.
Goal LCnb 1 term6 = false. reflexivity. Qed.
Goal LCnb 2 term6 = false. reflexivity. Qed.
Example ex1: level term1 = 0 := ltac:(trivial).
Example ex2: level term2 = 1 := ltac:(trivial).
Example ex23: level term3 = 1 := ltac:(trivial).
Example ex3: level term4 = 2 := ltac:(trivial).
Example ex4: level term5 = 2 := ltac:(trivial).
Example ex5: level term6 = 4 := ltac:(trivial).
End demo1.
Module demo2.
Import Tele.
Example ex1: level term1 = 0 := ltac:(trivial).
Example ex2: level term2 = 1 := ltac:(trivial).
Example ex23: level term3 = 0 := ltac:(trivial).
Example ex3: level term4 = 1 := ltac:(trivial).
Example ex4: level term5 = 0 := ltac:(trivial).
Example ex5: level term6 = 2 := ltac:(trivial).
End demo2.
Module demo3.
Import LetRec.
Goal LCnb 0 term1 = true. reflexivity. Qed.
Goal LCnb 0 term2 = true. reflexivity. Qed.
Goal LCnb 0 term4 = true. reflexivity. Qed.
Example ex1: level term1 = 0 := ltac:(trivial).
Example ex2: level term2 = 0 := ltac:(trivial).
Example ex23: level term3 = 0 := ltac:(trivial).
Example ex3: level term4 = 0 := ltac:(trivial).
Example ex4: level term5 = 0 := ltac:(trivial).
Example ex5: level term6 = 1 := ltac:(trivial).
End demo3.
Examples.VariadicLet.Terms
Examples.VariadicLet.Instances.Simple
Examples.VariadicLet.Instances.Tele
Examples.VariadicLet.Instances.LetRec.
Import Terms.
Parameters (x y z: atom).
Definition term1: term LN :=
letin [tvar (Fr x)] (tvar (Bd 0)).
Definition term2: term LN :=
letin [tvar (Bd 0)] (tvar (Bd 0)).
Definition term3: term LN :=
letin [tvar (Fr x); tvar (Bd 0)] (tvar (Bd 0)).
Definition term4: term LN :=
letin [tvar (Fr x); tvar (Bd 1)] (tvar (Bd 0)).
Definition term5: term LN :=
letin [tvar (Fr x); tvar (Bd 0) ; tvar (Bd 1)] (tvar (Bd 2)).
Definition term6: term LN :=
letin [tvar (Bd 1) ; tvar (Bd 2) ; tvar (Bd 3)] (tvar (Bd 2)).
Definition compute_which_are_closed `{mapdt: Mapdt nat term}: list bool :=
map (LCb (Mapdt_U := mapdt)) [term1; term2; term3; term4; term5; term6].
Definition compute_column_of_table `{mapdt: Mapdt nat term}: list nat :=
map (level (Mapdt_U := mapdt)) [term1; term2; term3; term4; term5; term6].
Section JAR_table.
Compute compute_column_of_table (mapdt := Simple.Mapdt_term).
(* = 0; 1; 1; 2; 2; 4 *)
Compute compute_column_of_table (mapdt := Tele.Mapdt_term).
(* = 0; 1; 0; 1; 0; 2 *)
Compute compute_column_of_table (mapdt := LetRec.Mapdt_term).
(* = 0; 0; 0; 0; 0; 1 *)
End JAR_table.
Compute compute_which_are_closed (mapdt := Simple.Mapdt_term).
(* = true; false; false; false; false; false *)
Compute compute_which_are_closed (mapdt := Tele.Mapdt_term).
(* = true; false; true; false; true; false *)
Compute compute_which_are_closed (mapdt := LetRec.Mapdt_term).
(* = true; true; true; true; true; false *)
Module demo1.
Import Simple.
Goal LCnb 0 term1 = true. reflexivity. Qed.
Goal LCnb 0 term2 = false. reflexivity. Qed.
Goal LCnb 1 term2 = true. reflexivity. Qed.
Goal LCnb 0 term4 = false. reflexivity. Qed.
Goal LCnb 1 term4 = false. reflexivity. Qed.
Goal LCnb 0 term6 = false. reflexivity. Qed.
Goal LCnb 1 term6 = false. reflexivity. Qed.
Goal LCnb 2 term6 = false. reflexivity. Qed.
Example ex1: level term1 = 0 := ltac:(trivial).
Example ex2: level term2 = 1 := ltac:(trivial).
Example ex23: level term3 = 1 := ltac:(trivial).
Example ex3: level term4 = 2 := ltac:(trivial).
Example ex4: level term5 = 2 := ltac:(trivial).
Example ex5: level term6 = 4 := ltac:(trivial).
End demo1.
Module demo2.
Import Tele.
Example ex1: level term1 = 0 := ltac:(trivial).
Example ex2: level term2 = 1 := ltac:(trivial).
Example ex23: level term3 = 0 := ltac:(trivial).
Example ex3: level term4 = 1 := ltac:(trivial).
Example ex4: level term5 = 0 := ltac:(trivial).
Example ex5: level term6 = 2 := ltac:(trivial).
End demo2.
Module demo3.
Import LetRec.
Goal LCnb 0 term1 = true. reflexivity. Qed.
Goal LCnb 0 term2 = true. reflexivity. Qed.
Goal LCnb 0 term4 = true. reflexivity. Qed.
Example ex1: level term1 = 0 := ltac:(trivial).
Example ex2: level term2 = 0 := ltac:(trivial).
Example ex23: level term3 = 0 := ltac:(trivial).
Example ex3: level term4 = 0 := ltac:(trivial).
Example ex4: level term5 = 0 := ltac:(trivial).
Example ex5: level term6 = 1 := ltac:(trivial).
End demo3.