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 : term LN :=
  letin [tvar (Fr x)] (tvar (Bd 0)).
Definition : term LN :=
  letin [tvar (Bd 0)] (tvar (Bd 0)).
Definition : term LN :=
  letin [tvar (Fr x); tvar (Bd 0)] (tvar (Bd 0)).
Definition : term LN :=
  letin [tvar (Fr x); tvar (Bd 1)] (tvar (Bd 0)).
Definition : term LN :=
  letin [tvar (Fr x); tvar (Bd 0) ; tvar (Bd 1)] (tvar (Bd 2)).
Definition : term LN :=
  letin [tvar (Bd 1) ; tvar (Bd 2) ; tvar (Bd 3)] (tvar (Bd 2)).

Definition compute_which_are_closed `{mapdt: Mapdt term}: list bool :=
  map (LCb (Mapdt_U := mapdt)) [; ; ; ; ; ].

Definition compute_column_of_table `{mapdt: Mapdt term}: list :=
  map (level (Mapdt_U := mapdt)) [; ; ; ; ; ].

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 = true. reflexivity. Qed.

  Goal LCnb 0 = false. reflexivity. Qed.
  Goal LCnb 1 = true. reflexivity. Qed.

  Goal LCnb 0 = false. reflexivity. Qed.
  Goal LCnb 1 = false. reflexivity. Qed.

  Goal LCnb 0 = false. reflexivity. Qed.
  Goal LCnb 1 = false. reflexivity. Qed.
  Goal LCnb 2 = false. reflexivity. Qed.

  Example : level = 0 := ltac:(trivial).
  Example : level = 1 := ltac:(trivial).
  Example : level = 1 := ltac:(trivial).
  Example : level = 2 := ltac:(trivial).
  Example : level = 2 := ltac:(trivial).
  Example : level = 4 := ltac:(trivial).

End demo1.

Module demo2.

  Import Tele.

  Example : level = 0 := ltac:(trivial).
  Example : level = 1 := ltac:(trivial).
  Example : level = 0 := ltac:(trivial).
  Example : level = 1 := ltac:(trivial).
  Example : level = 0 := ltac:(trivial).
  Example : level = 2 := ltac:(trivial).

End demo2.

Module demo3.

  Import LetRec.

  Goal LCnb 0 = true. reflexivity. Qed.
  Goal LCnb 0 = true. reflexivity. Qed.
  Goal LCnb 0 = true. reflexivity. Qed.

  Example : level = 0 := ltac:(trivial).
  Example : level = 0 := ltac:(trivial).
  Example : level = 0 := ltac:(trivial).
  Example : level = 0 := ltac:(trivial).
  Example : level = 0 := ltac:(trivial).
  Example : level = 1 := ltac:(trivial).
End demo3.