Library EnumInt
Require Import Lists Equality Nat Enum.
Definition AppCross := R (.\"aC", "A", "B";
"A" !Nil (.\"a", "A"; !Append ("aC" "A" "B") (!Map (.\"x"; !App "a" "x") "B"))).
Definition tlenc := @lenc term tenc.
Hint Unfold tlenc.
Lemma tlenc_lam B : lambda (tlenc B).
Proof.
eapply lenc_lam.
Qed.
Lemma tlenc_cls B : closed (tlenc B).
Proof.
eapply lenc_cls, tenc_cls.
Qed.
Hint Unfold Nil Cons : cbv.
Hint Resolve tlenc_lam tlenc_cls : cbv.
Hint Rewrite tlenc_cls : cbv.
Lemma AppCross_Nil B : AppCross Nil (tlenc B) == Nil.
Proof.
crush.
Qed.
Lemma AppCross_Cons a A B : AppCross (tlenc (a::A)) (tlenc B) == Append ((lam (AppCross #0)) (tlenc A) (tlenc B)) (Map (lam (App (tenc a) #0)) (tlenc B)).
Proof.
crush.
Qed.
Lemma AppCross_correct A B : AppCross (tlenc A) (tlenc B) == tlenc(appCross A B).
Proof.
induction A.
- now rewrite AppCross_Nil.
- rewrite AppCross_Cons. simpl.
rewrite !Eta, IHA; value. unfold tlenc; rewrite Map_correct; eauto with cbv.
+ rewrite Append_correct; eauto with cbv.
+ split; value.
intros; rewrite <- App_correct. crush.
Qed.
Definition Exh_size := R (.\ "Es", "s";
"s" !I (.\ "s", "t"; !Add (!Add !(enc 1) ("Es" "s")) ("Es" "t")) (.\ "s"; (!Succ ("Es" "s")))).
Hint Unfold Exh_size : cbv.
Lemma Exh_size_var n : Exh_size (tenc #n) == enc n.
Proof.
crush.
Qed.
Lemma Exh_size_app (s t : term) : Exh_size (tenc (s t))
== Add (Add (enc 1) ((lam (Exh_size #0)) (tenc s))) ((lam (Exh_size #0)) (tenc t)).
Proof.
crush.
Qed.
Lemma Exh_size_lam s : Exh_size (tenc (lam s)) == Succ ((lam(Exh_size #0)) (tenc s)).
Proof.
crush.
Qed.
Lemma Exh_size_correct s : Exh_size (tenc s) == enc(exh_size s).
Proof.
induction s.
- now rewrite Exh_size_var.
- now rewrite Exh_size_app, !Eta, IHs1, IHs2, !Add_correct; value.
- now rewrite Exh_size_lam, !Eta, IHs, Succ_correct; value.
Qed.
Definition TT := R (.\ "TT", "n";
"n" !(tlenc([#0]))
(.\"n"; (!Append
(!Append ("TT" "n") (!Cons (!Var (!Succ "n")) !Nil))
(!Filter (.\"x"; (!Not (!(El Eq) "x" ("TT" "n"))))
(!Append (!Map !Lam ("TT" "n"))
(!AppCross ("TT" "n") ("TT" "n"))
)))
)
).
Lemma TT_0 : TT (enc 0) == tlenc([#0]).
Proof.
crush.
Qed.
Lemma TT_S n : TT (enc (S n)) == Append (Append ((lam(TT #0)) (enc n)) (Cons (Var (Succ (enc n))) Nil)) (Filter (lam(Not (El Eq #0 ((lam(TT #0)) (enc n))))) (Append (Map Lam ((lam(TT #0)) (enc n))) (AppCross ((lam(TT #0)) (enc n)) ((lam(TT #0)) (enc n))))).
Proof.
crush.
Qed.
Lemma TT_correct n : TT (enc n) == tlenc(T n).
Proof with value; eauto with cbv; unfold tlenc.
induction n...
- now rewrite TT_0.
- rewrite TT_S;
rewrite Eta at 1; value.
repeat rewrite Eta at 2; value.
rewrite !IHn, AppCross_correct...
rewrite (@Map_correct _ tenc tenc_lam tenc_cls lam)...
rewrite Append_correct...
remember (λ Not ((El Eq #0) ((λ TT #0) (enc n)))) as P.
rewrite (@Filter_correct _ tenc tenc_lam tenc_cls P (fun x : term => ~ x el T n)); subst...
rewrite Succ_correct, Var_correct. change (Nil) with (tlenc nil)...
rewrite Cons_correct...
rewrite !Append_correct... now rewrite <- app_assoc.
+ intros x.
destruct El_correct with (s := x) (A := T n) (enc := tenc) (Eq := Eq)...
* intros; decide (s = t); [left | right]; intuition; now eapply Eq_correct.
* right; intuition.
transitivity (Not (El Eq (tenc x) (TT (enc n)))).
transitivity (Not (El Eq (tenc x) ((lam (TT #0)) (enc n)))). crush.
rewrite Eta, IHn, H0; value. crush. rewrite IHn, H0. crush.
* left; intuition.
transitivity (Not (El Eq (tenc x) (TT (enc n)))).
transitivity (Not (El Eq (tenc x) ((lam (TT #0)) (enc n)))). crush.
rewrite Eta, IHn, H0; value. crush. rewrite IHn, H0. crush.
+ split; value.
intros x. eapply Lam_correct.
Qed.
Definition U : term := .\"n";
(!Nth (!TT "n") "n") !I !(tenc #0).
Hint Unfold U : cbv.
Lemma U_correct n : U (enc n) == tenc(g_inv n).
Proof.
transitivity (Nth (TT (enc n)) (enc n) I (tenc #0)). crush.
rewrite TT_correct. unfold tlenc.
rewrite Nth_correct; value.
unfold g_inv, elAt, oenc.
destruct (nth_error (T n) n); crush.
intros; value. intros; value.
Qed.
Definition AppCross := R (.\"aC", "A", "B";
"A" !Nil (.\"a", "A"; !Append ("aC" "A" "B") (!Map (.\"x"; !App "a" "x") "B"))).
Definition tlenc := @lenc term tenc.
Hint Unfold tlenc.
Lemma tlenc_lam B : lambda (tlenc B).
Proof.
eapply lenc_lam.
Qed.
Lemma tlenc_cls B : closed (tlenc B).
Proof.
eapply lenc_cls, tenc_cls.
Qed.
Hint Unfold Nil Cons : cbv.
Hint Resolve tlenc_lam tlenc_cls : cbv.
Hint Rewrite tlenc_cls : cbv.
Lemma AppCross_Nil B : AppCross Nil (tlenc B) == Nil.
Proof.
crush.
Qed.
Lemma AppCross_Cons a A B : AppCross (tlenc (a::A)) (tlenc B) == Append ((lam (AppCross #0)) (tlenc A) (tlenc B)) (Map (lam (App (tenc a) #0)) (tlenc B)).
Proof.
crush.
Qed.
Lemma AppCross_correct A B : AppCross (tlenc A) (tlenc B) == tlenc(appCross A B).
Proof.
induction A.
- now rewrite AppCross_Nil.
- rewrite AppCross_Cons. simpl.
rewrite !Eta, IHA; value. unfold tlenc; rewrite Map_correct; eauto with cbv.
+ rewrite Append_correct; eauto with cbv.
+ split; value.
intros; rewrite <- App_correct. crush.
Qed.
Definition Exh_size := R (.\ "Es", "s";
"s" !I (.\ "s", "t"; !Add (!Add !(enc 1) ("Es" "s")) ("Es" "t")) (.\ "s"; (!Succ ("Es" "s")))).
Hint Unfold Exh_size : cbv.
Lemma Exh_size_var n : Exh_size (tenc #n) == enc n.
Proof.
crush.
Qed.
Lemma Exh_size_app (s t : term) : Exh_size (tenc (s t))
== Add (Add (enc 1) ((lam (Exh_size #0)) (tenc s))) ((lam (Exh_size #0)) (tenc t)).
Proof.
crush.
Qed.
Lemma Exh_size_lam s : Exh_size (tenc (lam s)) == Succ ((lam(Exh_size #0)) (tenc s)).
Proof.
crush.
Qed.
Lemma Exh_size_correct s : Exh_size (tenc s) == enc(exh_size s).
Proof.
induction s.
- now rewrite Exh_size_var.
- now rewrite Exh_size_app, !Eta, IHs1, IHs2, !Add_correct; value.
- now rewrite Exh_size_lam, !Eta, IHs, Succ_correct; value.
Qed.
Definition TT := R (.\ "TT", "n";
"n" !(tlenc([#0]))
(.\"n"; (!Append
(!Append ("TT" "n") (!Cons (!Var (!Succ "n")) !Nil))
(!Filter (.\"x"; (!Not (!(El Eq) "x" ("TT" "n"))))
(!Append (!Map !Lam ("TT" "n"))
(!AppCross ("TT" "n") ("TT" "n"))
)))
)
).
Lemma TT_0 : TT (enc 0) == tlenc([#0]).
Proof.
crush.
Qed.
Lemma TT_S n : TT (enc (S n)) == Append (Append ((lam(TT #0)) (enc n)) (Cons (Var (Succ (enc n))) Nil)) (Filter (lam(Not (El Eq #0 ((lam(TT #0)) (enc n))))) (Append (Map Lam ((lam(TT #0)) (enc n))) (AppCross ((lam(TT #0)) (enc n)) ((lam(TT #0)) (enc n))))).
Proof.
crush.
Qed.
Lemma TT_correct n : TT (enc n) == tlenc(T n).
Proof with value; eauto with cbv; unfold tlenc.
induction n...
- now rewrite TT_0.
- rewrite TT_S;
rewrite Eta at 1; value.
repeat rewrite Eta at 2; value.
rewrite !IHn, AppCross_correct...
rewrite (@Map_correct _ tenc tenc_lam tenc_cls lam)...
rewrite Append_correct...
remember (λ Not ((El Eq #0) ((λ TT #0) (enc n)))) as P.
rewrite (@Filter_correct _ tenc tenc_lam tenc_cls P (fun x : term => ~ x el T n)); subst...
rewrite Succ_correct, Var_correct. change (Nil) with (tlenc nil)...
rewrite Cons_correct...
rewrite !Append_correct... now rewrite <- app_assoc.
+ intros x.
destruct El_correct with (s := x) (A := T n) (enc := tenc) (Eq := Eq)...
* intros; decide (s = t); [left | right]; intuition; now eapply Eq_correct.
* right; intuition.
transitivity (Not (El Eq (tenc x) (TT (enc n)))).
transitivity (Not (El Eq (tenc x) ((lam (TT #0)) (enc n)))). crush.
rewrite Eta, IHn, H0; value. crush. rewrite IHn, H0. crush.
* left; intuition.
transitivity (Not (El Eq (tenc x) (TT (enc n)))).
transitivity (Not (El Eq (tenc x) ((lam (TT #0)) (enc n)))). crush.
rewrite Eta, IHn, H0; value. crush. rewrite IHn, H0. crush.
+ split; value.
intros x. eapply Lam_correct.
Qed.
Definition U : term := .\"n";
(!Nth (!TT "n") "n") !I !(tenc #0).
Hint Unfold U : cbv.
Lemma U_correct n : U (enc n) == tenc(g_inv n).
Proof.
transitivity (Nth (TT (enc n)) (enc n) I (tenc #0)). crush.
rewrite TT_correct. unfold tlenc.
rewrite Nth_correct; value.
unfold g_inv, elAt, oenc.
destruct (nth_error (T n) n); crush.
intros; value. intros; value.
Qed.