yiyunliu/pair-eta
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add some todos

Browse source
This commit is contained in:
Yiyun Liu 2025-01-04 01:48:31 -05:00
parent 68207eb3bd
commit 7ffb8a912d
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
theories/fp_red.v
View file

@ -1064,7 +1064,10 @@ Definition prov_univ {n} i0 (a : Tm n) :=
(* Can consider combine prov and provU *) (* Can consider combine prov and provU *)
#[tactic="prov_tac"]Equations prov {n} (h : Tm n) (a : Tm n) : Prop by wf (depth_tm a) lt := #[tactic="prov_tac"]Equations prov {n} (h : Tm n) (a : Tm n) : Prop by wf (depth_tm a) lt :=
prov h (TBind p0 A0 B0) := prov_bind p0 A0 B0 h; prov h (TBind p0 A0 B0) := prov_bind p0 A0 B0 h;
(* TODOS *)
(* Try forall b, prov h (a {b /x})? *) (* Try forall b, prov h (a {b /x})? *)
(* Replace the parallel red from I_Red with Strong normalization *)
(* Prove the uniqueness of eta normal form for terms in beta normal form *)
prov h (Abs a) := prov (ren_Tm shift h) a; prov h (Abs a) := prov (ren_Tm shift h) a;
prov h (App a b) := prov h a; prov h (App a b) := prov h a;
prov h (Pair a b) := prov h a /\ prov h b; prov h (Pair a b) := prov h a /\ prov h b;