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

Minor

Browse source
This commit is contained in:
Yiyun Liu 2025-01-31 16:30:06 -05:00
parent fc666956e2
commit 47473fd3cd
1 changed files with 152 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

229
theories/fp_red.v
View file

@ -20,7 +20,7 @@ Ltac2 spec_refl () :=
Ltac spec_refl := ltac2:(spec_refl ()).
Module ERed.
Module EPar.
Inductive R {n} : PTm n -> PTm n -> Prop :=
(****************** Eta ***********************)
| AppEta a0 a1 :
@ -97,7 +97,7 @@ Module ERed.
all : hauto lq:on ctrs:R use:morphing_up.
Qed.
End ERed.
End EPar.
Inductive SNe {n} : PTm n -> Prop :=
| N_Var i :
@ -333,10 +333,10 @@ Proof.
hauto lq:on rew:off inv:TRedSN db:sn.
Qed.
Lemma ered_sn_preservation n :
(forall (a : PTm n) (s : SNe a), forall b, ERed.R a b -> SNe b) /\
(forall (a : PTm n) (s : SN a), forall b, ERed.R a b -> SN b) /\
(forall (a b : PTm n) (_ : TRedSN a b), forall c, ERed.R a c -> exists d, TRedSN' c d /\ ERed.R b d).
Lemma epar_sn_preservation n :
(forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\
(forall (a : PTm n) (s : SN a), forall b, EPar.R a b -> SN b) /\
(forall (a b : PTm n) (_ : TRedSN a b), forall c, EPar.R a c -> exists d, TRedSN' c d /\ EPar.R b d).
Proof.
move : n. apply sn_mutual => n.
- sauto lq:on.
@ -344,14 +344,14 @@ Proof.
- sauto lq:on.
- move => a b ha iha hb ihb b0.
inversion 1; subst.
+ have /iha : (ERed.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
+ have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
sfirstorder use:SN_Proj.
+ sauto lq:on.
- move => a ha iha b.
inversion 1; subst.
+ have : ERed.R (PApp (ren_PTm shift a0) (VarPTm var_zero)) (PApp (ren_PTm shift b) (VarPTm var_zero)).
apply ERed.AppCong; eauto using ERed.refl.
sfirstorder use:ERed.renaming.
+ have : EPar.R (PApp (ren_PTm shift a0) (VarPTm var_zero)) (PApp (ren_PTm shift b) (VarPTm var_zero)).
apply EPar.AppCong; eauto using EPar.refl.
sfirstorder use:EPar.renaming.
move /iha.
move /SN_AppInv => [+ _].
hauto l:on use:sn_antirenaming.
@ -368,21 +368,21 @@ Proof.
exists (subst_PTm (scons b1 VarPTm) a2).
split.
sauto lq:on.
hauto lq:on use:ERed.morphing, ERed.refl inv:option.
hauto lq:on use:EPar.morphing, EPar.refl inv:option.
- sauto.
- move => a b hb ihb c.
elim /ERed.inv => //= _.
elim /EPar.inv => //= _.
move => p a0 a1 ha [*]. subst.
elim /ERed.inv : ha => //= _.
elim /EPar.inv : ha => //= _.
+ move => a0 a2 ha' [*]. subst.
exists (PProj PL a1).
split. sauto.
sauto lq:on.
+ sauto lq:on rew:off.
- move => a b ha iha c.
elim /ERed.inv => //=_.
elim /EPar.inv => //=_.
move => p a0 a1 + [*]. subst.
elim /ERed.inv => //=_.
elim /EPar.inv => //=_.
+ move => a0 a2 h1 [*]. subst.
exists (PProj PR a1).
split. sauto.
@ -658,7 +658,7 @@ Lemma tstar_proj n (a : PTm n) :
exists a0 b0, a = PPair a0 b0 /\ forall p, tstar (PProj p a) = (if p is PL then (tstar a0) else (tstar b0)).
Proof. sauto lq:on. Qed.
Module ERed'.
Module EPar'.
Inductive R {n} : PTm n -> PTm n -> Prop :=
(****************** Eta ***********************)
| AppEta a :
@ -708,39 +708,39 @@ Module ERed'.
(forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)).
Proof. eauto using renaming. Qed.
End ERed'.
End EPar'.
Module EReds.
Module EPars.
#[local]Ltac solve_s_rec :=
move => *; eapply rtc_l; eauto;
hauto lq:on ctrs:ERed'.R.
hauto lq:on ctrs:EPar'.R.
#[local]Ltac solve_s :=
repeat (induction 1; last by solve_s_rec); apply rtc_refl.
Lemma AbsCong n (a b : PTm (S n)) :
rtc ERed'.R a b ->
rtc ERed'.R (PAbs a) (PAbs b).
rtc EPar'.R a b ->
rtc EPar'.R (PAbs a) (PAbs b).
Proof. solve_s. Qed.
Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
rtc ERed'.R a0 a1 ->
rtc ERed'.R b0 b1 ->
rtc ERed'.R (PApp a0 b0) (PApp a1 b1).
rtc EPar'.R a0 a1 ->
rtc EPar'.R b0 b1 ->
rtc EPar'.R (PApp a0 b0) (PApp a1 b1).
Proof. solve_s. Qed.
Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
rtc ERed'.R a0 a1 ->
rtc ERed'.R b0 b1 ->
rtc ERed'.R (PPair a0 b0) (PPair a1 b1).
rtc EPar'.R a0 a1 ->
rtc EPar'.R b0 b1 ->
rtc EPar'.R (PPair a0 b0) (PPair a1 b1).
Proof. solve_s. Qed.
Lemma ProjCong n p (a0 a1 : PTm n) :
rtc ERed'.R a0 a1 ->
rtc ERed'.R (PProj p a0) (PProj p a1).
rtc EPar'.R a0 a1 ->
rtc EPar'.R (PProj p a0) (PProj p a1).
Proof. solve_s. Qed.
End EReds.
End EPars.
Module RReds.
@ -788,7 +788,7 @@ Proof.
move : m ξ. elim : n / a => //=; solve [hauto b:on].
Qed.
Lemma ne_ered n (a b : PTm n) (h : ERed'.R a b ) :
Lemma ne_epar n (a b : PTm n) (h : EPar'.R a b ) :
(ne a -> ne b) /\ (nf a -> nf b).
Proof.
elim : n a b /h=>//=; hauto qb:on use:ne_nf_ren, ne_nf.
@ -801,7 +801,7 @@ Definition ishf {n} (a : PTm n) :=
| _ => false
end.
Module NeERed.
Module NeEPar.
Inductive R_nonelim {n} : PTm n -> PTm n -> Prop :=
(****************** Eta ***********************)
| AppEta a0 a1 :
@ -847,16 +847,16 @@ Module NeERed.
| NVarTm i :
R_elim (VarPTm i) (VarPTm i).
Scheme ered_elim_ind := Induction for R_elim Sort Prop
with ered_nonelim_ind := Induction for R_nonelim Sort Prop.
Scheme epar_elim_ind := Induction for R_elim Sort Prop
with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
Combined Scheme ered_mutual from ered_elim_ind, ered_nonelim_ind.
Combined Scheme epar_mutual from epar_elim_ind, epar_nonelim_ind.
Lemma R_elim_nf n :
(forall (a b : PTm n), R_elim a b -> nf b -> nf a) /\
(forall (a b : PTm n), R_nonelim a b -> nf b -> nf a).
Proof.
move : n. apply ered_mutual => n //=.
move : n. apply epar_mutual => n //=.
- move => a0 a1 b0 b1 h ih h' ih' /andP [h0 h1].
have hb0 : nf b0 by eauto.
suff : ne a0 by qauto b:on.
@ -895,13 +895,13 @@ Module NeERed.
move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_nonelim.
Qed.
End NeERed.
End NeEPar.
Module Type NoForbid.
Parameter P : forall n, PTm n -> Prop.
Arguments P {n}.
Axiom P_ERed : forall n (a b : PTm n), ERed.R a b -> P a -> P b.
Axiom P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b.
Axiom P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
Axiom P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c).
Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)).
@ -916,7 +916,7 @@ End NoForbid.
Module Type NoForbid_FactSig (M : NoForbid).
Axiom P_EReds : forall n (a b : PTm n), rtc ERed.R a b -> M.P a -> M.P b.
Axiom P_EPars : forall n (a b : PTm n), rtc EPar.R a b -> M.P a -> M.P b.
Axiom P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> M.P a -> M.P b.
@ -925,9 +925,9 @@ End NoForbid_FactSig.
Module NoForbid_Fact (M : NoForbid) : NoForbid_FactSig M.
Import M.
Lemma P_EReds : forall n (a b : PTm n), rtc ERed.R a b -> P a -> P b.
Lemma P_EPars : forall n (a b : PTm n), rtc EPar.R a b -> P a -> P b.
Proof.
induction 1; eauto using P_ERed, rtc_l, rtc_refl.
induction 1; eauto using P_EPar, rtc_l, rtc_refl.
Qed.
Lemma P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> P a -> P b.
@ -936,12 +936,12 @@ Module NoForbid_Fact (M : NoForbid) : NoForbid_FactSig M.
Qed.
End NoForbid_Fact.
Module SN_NoForbid : NoForbid.
Module SN_NoForbid <: NoForbid.
Definition P := @SN.
Arguments P {n}.
Lemma P_ERed : forall n (a b : PTm n), ERed.R a b -> P a -> P b.
Proof. sfirstorder use:ered_sn_preservation. Qed.
Lemma P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b.
Proof. sfirstorder use:epar_sn_preservation. Qed.
Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed.
@ -974,14 +974,16 @@ Module SN_NoForbid : NoForbid.
End SN_NoForbid.
Module NoForbid_FactSN := NoForbid_Fact SN_NoForbid.
Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
Import M MFacts.
#[local]Hint Resolve P_ERed P_RRed P_AppPair P_ProjAbs : forbid.
#[local]Hint Resolve P_EPar P_RRed P_AppPair P_ProjAbs : forbid.
Lemma η_split n (a0 a1 : PTm n) :
ERed.R a0 a1 ->
EPar.R a0 a1 ->
P a0 ->
exists b, rtc RRed.R a0 b /\ NeERed.R_nonelim b a1.
exists b, rtc RRed.R a0 b /\ NeEPar.R_nonelim b a1.
Proof.
move => h. elim : n a0 a1 /h .
- move => n a0 a1 ha ih /[dup] hP.
@ -992,8 +994,8 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
exists (PAbs (PApp (ren_PTm shift b) (VarPTm var_zero))).
split. apply RReds.AbsCong. apply RReds.AppCong; auto using rtc_refl.
by eauto using RReds.renaming.
apply NeERed.AppEta=>//.
sfirstorder use:NeERed.R_nonelim_nothf.
apply NeEPar.AppEta=>//.
sfirstorder use:NeEPar.R_nonelim_nothf.
case : b ih0 ih1 => //=.
+ move => p ih0 ih1 _.
@ -1024,7 +1026,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
case /orP : (orNb (ishf b)).
exists (PPair (PProj PL b) (PProj PR b)).
split. sfirstorder use:RReds.PairCong,RReds.ProjCong.
hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf.
hauto lq:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
case : b ih0 ih1 => //=.
(* violates SN *)
@ -1042,14 +1044,14 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
apply RRed.ProjPair.
apply : rtc_r; eauto using RReds.ProjCong.
apply RRed.ProjPair.
- hauto lq:on ctrs:NeERed.R_nonelim use:RReds.AbsCong, P_AbsInv.
- hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.AbsCong, P_AbsInv.
- move => n a0 a1 b0 b1 ha iha hb ihb.
move => /[dup] hP /P_AppInv [hP0 hP1].
have {iha} [a2 [iha0 iha1]] := iha hP0.
have {ihb} [b2 [ihb0 ihb1]] := ihb hP1.
case /orP : (orNb (ishf a2)) => [h|].
+ exists (PApp a2 b2). split; first by eauto using RReds.AppCong.
hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf.
hauto lq:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
+ case : a2 iha0 iha1 => //=.
* move => p h0 h1 _.
inversion h1; subst.
@ -1058,21 +1060,21 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
apply : rtc_r.
apply RReds.AppCong; eauto.
apply RRed.AppAbs'. by asimpl.
hauto lq:on ctrs:NeERed.R_nonelim.
** hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.AppCong.
hauto lq:on ctrs:NeEPar.R_nonelim.
** hauto lq:on ctrs:NeEPar.R_nonelim,NeEPar.R_elim use:RReds.AppCong.
(* Impossible *)
* move => u0 u1 h. exfalso.
have : rtc RRed.R (PApp a0 b0) (PApp (PPair u0 u1) b0)
by hauto lq:on ctrs:rtc use:RReds.AppCong.
move : P_RReds hP; repeat move/[apply].
sfirstorder use:P_AppPair.
- hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong, P_PairInv.
- hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.PairCong, P_PairInv.
- move => n p a0 a1 ha ih /[dup] hP /P_ProjInv.
move : ih => /[apply]. move => [a2 [iha0 iha1]].
case /orP : (orNb (ishf a2)) => [h|].
exists (PProj p a2).
split. eauto using RReds.ProjCong.
qauto l:on ctrs:NeERed.R_nonelim, NeERed.R_elim use:NeERed.R_nonelim_nothf.
qauto l:on ctrs:NeEPar.R_nonelim, NeEPar.R_elim use:NeEPar.R_nonelim_nothf.
case : a2 iha0 iha1 => //=.
+ move => u iha0. exfalso.
@ -1086,28 +1088,101 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
apply : rtc_r.
apply RReds.ProjCong; eauto.
clear. hauto l:on inv:PTag.
hauto lq:on ctrs:NeERed.R_nonelim.
* hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong.
- hauto lq:on ctrs:rtc, NeERed.R_nonelim.
hauto lq:on ctrs:NeEPar.R_nonelim.
* hauto lq:on ctrs:NeEPar.R_nonelim,NeEPar.R_elim use:RReds.ProjCong.
- hauto lq:on ctrs:rtc, NeEPar.R_nonelim.
Qed.
End UniqueNF.
Lemma η_nf_to_ne n (a0 a1 : PTm n) :
ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 ->
(a0 = PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) \/
(a0 = PPair (PProj PL a1) (PProj PR a1)).
Proof.
move => h.
elim : n a0 a1 /h => n /=.
- sfirstorder use:ne_ered.
- hauto l:on use:ne_ered.
- scongruence use:ne_ered.
- hauto qb:on use:ne_ered, ne_nf.
- move => a b0 b1 h0 ih0 /andP [h1 h2] h3 /andP [h4 h5].
have {h3} : ~~ ne a by sfirstorder b:on.
by move /negP.
- hauto lqb:on.
- sfirstorder b:on.
- scongruence b:on.
Qed.
Module SN_UniqueNF := UniqueNF SN_NoForbid NoForbid_FactSN.
Module ERed.
Inductive R {n} : PTm n -> PTm n -> Prop :=
(****************** Eta ***********************)
| AppEta a :
R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a
| PairEta a :
R (PPair (PProj PL a) (PProj PR a)) a
(*************** Congruence ********************)
| AbsCong a0 a1 :
R a0 a1 ->
R (PAbs a0) (PAbs a1)
| AppCong0 a0 a1 b :
R a0 a1 ->
R (PApp a0 b) (PApp a1 b)
| AppCong1 a b0 b1 :
R b0 b1 ->
R (PApp a b0) (PApp a b1)
| PairCong0 a0 a1 b :
R a0 a1 ->
R (PPair a0 b) (PPair a1 b)
| PairCong1 a b0 b1 :
R b0 b1 ->
R (PPair a b0) (PPair a b1)
| ProjCong p a0 a1 :
R a0 a1 ->
R (PProj p a0) (PProj p a1).
Lemma ToEPar n (a b : PTm n) :
ERed.R a b -> EPar.R a b.
Proof.
induction 1; hauto lq:on use:EPar.refl ctrs:EPar.R.
Qed.
End ERed.
#[export]Hint Constructors ERed.R RRed.R EPar.R : red.
Module RERed.
Inductive R {n} : PTm n -> PTm n -> Prop :=
(****************** Beta ***********************)
| AppAbs a b :
R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a)
| ProjPair p a b :
R (PProj p (PPair a b)) (if p is PL then a else b)
(****************** Eta ***********************)
| AppEta a :
R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a
| PairEta a :
R (PPair (PProj PL a) (PProj PR a)) a
(*************** Congruence ********************)
| AbsCong a0 a1 :
R a0 a1 ->
R (PAbs a0) (PAbs a1)
| AppCong0 a0 a1 b :
R a0 a1 ->
R (PApp a0 b) (PApp a1 b)
| AppCong1 a b0 b1 :
R b0 b1 ->
R (PApp a b0) (PApp a b1)
| PairCong0 a0 a1 b :
R a0 a1 ->
R (PPair a0 b) (PPair a1 b)
| PairCong1 a b0 b1 :
R b0 b1 ->
R (PPair a b0) (PPair a b1)
| ProjCong p a0 a1 :
R a0 a1 ->
R (PProj p a0) (PProj p a1).
Lemma ToBetaEta n (a b : PTm n) :
R a b ->
ERed.R a b \/ RRed.R a b.
Proof. induction 1; hauto lq:on db:red. Qed.
Lemma ToBetaEtaPar n (a b : PTm n) :
R a b ->
EPar.R a b \/ RRed.R a b.
Proof.
hauto q:on use:ERed.ToEPar, ToBetaEta.
Qed.
End RERed.