Finish preservation

theories/algorithmic.v

@@ -16,13 +16,22 @@ Module HRed.
   | ProjPair p a b :
     R (PProj p (PPair a b)) (if p is PL then a else b)
 
+  | IndZero P b c :
+    R (PInd P PZero b c) b
+
+  | IndSuc P a b c :
+    R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+
   (*************** Congruence ********************)
   | AppCong a0 a1 b :
     R a0 a1 ->
     R (PApp a0 b) (PApp a1 b)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (PProj p a0) (PProj p a1).
+    R (PProj p a0) (PProj p a1)
+  | IndCong P a0 a1 b c :
+    R a0 a1 ->
+    R (PInd P a0 b c) (PInd P a1 b c).
 
   Lemma ToRRed n (a b : PTm n) : HRed.R a b -> RRed.R a b.
   Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.

theories/fp_red.v

@@ -2977,6 +2977,11 @@ Module DJoin.
     R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1).
   Proof. hauto q:on use:REReds.IndCong. Qed.
 
+  Lemma SucCong n (a0 a1 : PTm n) :
+    R a0 a1 ->
+    R (PSuc a0) (PSuc a1).
+  Proof. qauto l:on use:REReds.SucCong. Qed.
+
   Lemma FromRedSNs n (a b : PTm n) :
     rtc TRedSN a b ->
     R a b.

theories/logrel.v

@@ -1578,6 +1578,15 @@ Proof.
   rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
 Qed.
 
+Lemma SE_Nat n Γ (a b : PTm n) :
+  Γ ⊨ a ≡ b ∈ PNat ->
+  Γ ⊨ PSuc a ≡ PSuc b ∈ PNat.
+Proof.
+  move /SemEq_SemWt => [ha][hb]hE.
+  apply SemWt_SemEq; eauto using ST_Suc.
+  eauto using DJoin.SucCong.
+Qed.
+
 Lemma SE_App n Γ i (b0 b1 a0 a1 : PTm n) A B :
   Γ ⊨ PBind PPi A B ∈ (PUniv i) ->
   Γ ⊨ b0 ≡ b1 ∈ PBind PPi A B ->
@@ -1722,4 +1731,4 @@ Qed.
 
 #[export]Hint Resolve ST_Var ST_Bind ST_Abs ST_App ST_Pair ST_Proj1 ST_Proj2 ST_Univ ST_Conv
   SE_Refl SE_Symmetric SE_Transitive SE_Bind SE_Abs SE_App SE_Proj1 SE_Proj2
-  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc : sem.
+  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong : sem.

theories/preservation.v

@@ -76,6 +76,23 @@ Proof.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
+Lemma Ind_Inv n Γ P (a : PTm n) b c U :
+  Γ ⊢ PInd P a b c ∈ U ->
+  exists i, funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i /\
+       Γ ⊢ a ∈ PNat /\
+       Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P /\
+      funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) /\
+       Γ ⊢ subst_PTm (scons a VarPTm) P ≲ U.
+Proof.
+  move E : (PInd P a b c)=> u hu.
+  move : P a b c E. elim : n Γ u U / hu => n //=.
+  - move => Γ P a b c i hP _ ha _ hb _ hc _ P0 a0 b0 c0 [*]. subst.
+    exists i. repeat split => //=.
+    have : Γ ⊢ subst_PTm (scons a VarPTm) P ∈ subst_PTm (scons a VarPTm) (PUniv i) by hauto l:on use:substing_wt.
+    eauto using E_Refl, Su_Eq.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
 Lemma E_AppAbs : forall n (a : PTm (S n)) (b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
   Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
 Proof.
@@ -108,6 +125,19 @@ Proof.
   apply : E_ProjPair1; eauto.
 Qed.
 
+Lemma Suc_Inv n Γ (a : PTm n) A :
+  Γ ⊢ PSuc a ∈ A -> Γ ⊢ a ∈ PNat /\ Γ ⊢ PNat ≲ A.
+Proof.
+  move E : (PSuc a) => u hu.
+  move : a E.
+  elim : n Γ u A /hu => //=.
+  - move => n Γ a ha iha a0 [*]. subst.
+    split => //=. eapply wff_mutual in ha.
+    apply : Su_Eq.
+    apply E_Refl. by apply T_Nat'.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
 Lemma RRed_Eq n Γ (a b : PTm n) A :
   Γ ⊢ a ∈ A ->
   RRed.R a b ->
@@ -130,8 +160,13 @@ Proof.
       move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
       move {hS}.
       move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
-  - admit.
+  - hauto lq:on use:Ind_Inv, E_Conv, E_IndZero.
-  - admit.
+  - move => P a b c Γ A.
+    move /Ind_Inv.
+    move => [i][hP][ha][hb][hc]hSu.
+    apply : E_Conv; eauto.
+    apply : E_IndSuc'; eauto.
+    hauto l:on use:Suc_Inv.
   - qauto l:on use:Abs_Inv, E_Conv, regularity_sub0, E_Abs.
   - move => a0 a1 b ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
     have {}/iha iha := ih0.
@@ -172,7 +207,12 @@ Proof.
     have {}/ihA ihA := h1.
     apply : E_Conv; eauto.
     apply E_Bind'; eauto using E_Refl.
-Admitted.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on use:Suc_Inv, E_Conv, E_SucCong.
+Qed.
 
 Theorem subject_reduction n Γ (a b A : PTm n) :
   Γ ⊢ a ∈ A ->

theories/structural.v

@@ -507,6 +507,7 @@ Proof.
     move /(_ _ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
     move /(_ ltac:(qauto l:on use:morphing_up)).
     asimpl. substify. by asimpl.
+  - eauto with wt.
   - qauto l:on ctrs:Eq, LEq.
   - move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ρ hΔ hρ.
     move : ihP (hρ) (hΔ). repeat move/[apply].
@@ -734,6 +735,7 @@ Proof.
     by eauto using Su_Sig_Proj2.
     sauto lq:on use:substing_wt.
   - hauto lq:on ctrs:Wt.
+  - hauto lq:on ctrs:Wt.
   - hauto q:on use:substing_wt db:wt.
   - hauto l:on use:bind_inst db:wt.
   - move => n Γ P i b c hP _ hb _ hc _.

theories/typing.v

@@ -123,6 +123,10 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
   funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
   Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0
 
+| E_SucCong n Γ (a b : PTm n) :
+  Γ ⊢ a ≡ b ∈ PNat ->
+  Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
+
 | E_Conv n Γ (a b : PTm n) A B :
   Γ ⊢ a ≡ b ∈ A ->
   Γ ⊢ A ≲ B ->