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

Add comment about the antirenaming proof

Browse source
This commit is contained in:
Yiyun Liu 2025-01-31 21:56:58 -05:00
parent d2cd3105c7
commit ecb50f1ab7
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
theories/fp_red.v
View file

@ -1282,7 +1282,7 @@ Module ERed.
(* destruct a. *) (* destruct a. *)
(* exact (ξ f). *) (* exact (ξ f). *)
(* Need to generalize to injective renaming *)
Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
Proof. Proof.
@ -1298,10 +1298,14 @@ Module ERed.
case : i => //= _ h. case : i => //= _ h.
apply f_equal with (f := subst_PTm (scons (PAbs (VarPTm var_zero)) VarPTm)) in h. apply f_equal with (f := subst_PTm (scons (PAbs (VarPTm var_zero)) VarPTm)) in h.
move : h. asimpl. move => ?. subst. move : h. asimpl. move => ?. subst.
admit.
- move => n a m ξ []//=.
move => u u0 [].
case : u => //=.
case : u0 => //=.
move => p p0 p1 p2 [? ?] [? ?]. subst.
rewrite -/var_zero.
eexists. split. apply AppEta.
move : h. asimpl => ?. subst.