Merge remote-tracking branch 'forgejo/nonessential'

theories/fp_red.v

@@ -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 :
@@ -323,10 +323,10 @@ Proof.
   hauto lq:on rew:off inv:TRedSN db:sn.
 Qed.
 
-Lemma ered_sn_preservation n :
+Lemma epar_sn_preservation n :
-  (forall (a : PTm n) (s : SNe a), forall b, ERed.R a b -> SNe b) /\
+  (forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\
-  (forall (a : PTm n) (s : SN a), forall b, ERed.R a b -> SN 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, ERed.R a c -> exists d, TRedSN' c d /\ ERed.R b d).
+  (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.
@@ -334,14 +334,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)).
+    + have : EPar.R (PApp (ren_PTm shift a0) (VarPTm var_zero))  (PApp (ren_PTm shift b) (VarPTm var_zero)).
-      apply ERed.AppCong; eauto using ERed.refl.
+      apply EPar.AppCong; eauto using EPar.refl.
-      sfirstorder use:ERed.renaming.
+      sfirstorder use:EPar.renaming.
       move /iha.
       move /SN_AppInv => [+ _].
       hauto l:on use:sn_antirenaming.
@@ -358,21 +358,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.
@@ -648,7 +648,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 :
@@ -698,39 +698,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 EPar'.R a b ->
-    rtc ERed'.R (PAbs a) (PAbs 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 EPar'.R a0 a1 ->
-    rtc ERed'.R b0 b1 ->
+    rtc EPar'.R b0 b1 ->
-    rtc ERed'.R (PApp a0 b0) (PApp a1 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 EPar'.R a0 a1 ->
-    rtc ERed'.R b0 b1 ->
+    rtc EPar'.R b0 b1 ->
-    rtc ERed'.R (PPair a0 b0) (PPair a1 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 EPar'.R a0 a1 ->
-    rtc ERed'.R (PProj p a0) (PProj p a1).
+    rtc EPar'.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
-End EReds.
+End EPars.
 
 Module RReds.
 
@@ -778,7 +778,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.
@@ -791,7 +791,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 :
@@ -837,16 +837,16 @@ Module NeERed.
   | NVarTm i :
     R_elim (VarPTm i) (VarPTm i).
 
-  Scheme ered_elim_ind := Induction for R_elim Sort Prop
+  Scheme epar_elim_ind := Induction for R_elim Sort Prop
-      with ered_nonelim_ind := Induction for R_nonelim 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.
@@ -885,19 +885,19 @@ Module NeERed.
     move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_nonelim.
   Qed.
 
-  Lemma ToERed : forall n, (forall (a b : PTm n), R_elim a b -> ERed.R a b) /\
+  Lemma ToEPar : forall n, (forall (a b : PTm n), R_elim a b -> EPar.R a b) /\
-                 (forall (a b : PTm n), R_nonelim a b -> ERed.R a b).
+                 (forall (a b : PTm n), R_nonelim a b -> EPar.R a b).
   Proof.
-    apply ered_mutual; qauto l:on ctrs:ERed.R.
+    apply ered_mutual; qauto l:on ctrs:EPar.R.
   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)).
@@ -912,7 +912,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.
 
@@ -921,9 +921,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.
@@ -932,12 +932,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.
+  Lemma P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b.
-  Proof. sfirstorder use:ered_sn_preservation. Qed.
+  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.
@@ -970,14 +970,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.
@@ -988,8 +990,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=>//.
+      apply NeEPar.AppEta=>//.
-      sfirstorder use:NeERed.R_nonelim_nothf.
+      sfirstorder use:NeEPar.R_nonelim_nothf.
 
       case : b ih0 ih1 => //=.
       + move => p ih0 ih1 _.
@@ -1020,7 +1022,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 *)
@@ -1038,14 +1040,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.
@@ -1054,21 +1056,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:NeEPar.R_nonelim.
-          ** hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.AppCong.
+          ** 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.
@@ -1082,9 +1084,9 @@ 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:NeEPar.R_nonelim.
-        * hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong.
+        * hauto lq:on ctrs:NeEPar.R_nonelim,NeEPar.R_elim use:RReds.ProjCong.
-    - hauto lq:on ctrs:rtc, NeERed.R_nonelim.
+    - hauto lq:on ctrs:rtc, NeEPar.R_nonelim.
   Qed.
 
 
@@ -1224,21 +1226,94 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
 
 End UniqueNF.
 
-Lemma η_nf_to_ne n (a0 a1 : PTm n) :
+Module SN_UniqueNF := UniqueNF SN_NoForbid NoForbid_FactSN.
-  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)).
+Module ERed.
-Proof.
+  Inductive R {n} : PTm n -> PTm n ->  Prop :=
-  move => h.
+
-  elim : n a0 a1 /h => n /=.
+  (****************** Eta ***********************)
-  - sfirstorder use:ne_ered.
+  | AppEta a :
-  - hauto l:on use:ne_ered.
+    R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a
-  - scongruence use:ne_ered.
+  | PairEta a :
-  - hauto qb:on use:ne_ered, ne_nf.
+    R (PPair (PProj PL a) (PProj PR a)) a
-  - move => a b0 b1 h0 ih0 /andP [h1 h2] h3 /andP [h4 h5].
+
-    have {h3} : ~~ ne a by sfirstorder b:on.
+  (*************** Congruence ********************)
-    by move /negP.
+  | AbsCong a0 a1 :
-  - hauto lqb:on.
+    R a0 a1 ->
-  - sfirstorder b:on.
+    R (PAbs a0) (PAbs a1)
-  - scongruence b:on.
+  | AppCong0 a0 a1 b :
-Qed.
+    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.