Finish morphing_SemWt

theories/fp_red.v

@@ -2969,6 +2969,14 @@ Module DJoin.
     R (PBind p A0 B0) (PBind p A1 B1).
   Proof. hauto q:on use:REReds.BindCong. Qed.
 
+  Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 :
+    R P0 P1 ->
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1).
+  Proof. hauto q:on use:REReds.IndCong. Qed.
+
   Lemma FromRedSNs n (a b : PTm n) :
     rtc TRedSN a b ->
     R a b.
@@ -3129,6 +3137,15 @@ Module DJoin.
     hauto q:on ctrs:rtc inv:option use:REReds.cong.
   Qed.
 
+  Lemma cong' n m (a b : PTm (S n)) c d (ρ : fin n -> PTm m) :
+    R a b ->
+    R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) b).
+  Proof.
+    rewrite /R. move => [ab [h2 h3]] [cd [h0 h1]].
+    exists (subst_PTm (scons cd ρ) ab).
+    hauto q:on ctrs:rtc inv:option use:REReds.cong'.
+  Qed.
+
   Lemma pair_inj n (a0 a1 b0 b1 : PTm n) :
     SN (PPair a0 b0) ->
     SN (PPair a1 b1) ->

theories/logrel.v

@@ -683,32 +683,56 @@ Proof.
   hauto q:on solve+:(by asimpl).
 Qed.
 
-(* Definition smorphing_ok {n m} Δ Γ (ρ : fin n -> PTm m) := *)
+Definition smorphing_ok {n m} (Δ : fin m -> PTm m) Γ (ρ : fin n -> PTm m) :=
-(*   forall i ξ k PA, ρ_ok Δ ξ -> Δ *)
+  forall ξ, ρ_ok Δ ξ -> ρ_ok Γ (funcomp (subst_PTm ξ) ρ).
 
-(*  Δ ⊨ ρ i ∈ subst_PTm ρ (Γ i). *)
+Lemma smorphing_ren n m p Ξ Δ Γ
+  (ρ : fin n -> PTm m) (ξ : fin m -> fin p) :
+  renaming_ok Ξ Δ ξ -> smorphing_ok Δ Γ ρ ->
+  smorphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ).
+Proof.
+  move => hξ hρ τ.
+  move /ρ_ok_renaming : hξ => /[apply].
+  move => h.
+  rewrite /smorphing_ok in hρ.
+  asimpl.
+  Check (funcomp τ ξ).
+  set u := funcomp _ _.
+  have : u = funcomp (subst_PTm (funcomp τ ξ)) ρ.
+  subst u. extensionality i. by asimpl.
+  move => ->. by apply hρ.
+Qed.
 
-(* Lemma morphing_SemWt : forall n Γ (a A : PTm n), *)
+Lemma smorphing_ext n m Δ Γ (ρ : fin n -> PTm m) (a : PTm m) (A : PTm n)  :
-(*     Γ ⊨ a ∈ A -> forall m Δ (ρ : fin n -> PTm m), *)
+  smorphing_ok Δ Γ ρ ->
-(*       smorphing_ok Δ Γ ρ -> Δ ⊨ subst_PTm ρ a ∈ subst_PTm ρ A. *)
+  Δ ⊨ a ∈ subst_PTm ρ A ->
-(* Proof. *)
+  smorphing_ok
-(*   move => n Γ a A ha m Δ ρ. *)
+  Δ (funcomp (ren_PTm shift) (scons A Γ)) (scons a ρ).
-(*   rewrite /smorphing_ok => hρ. *)
+Proof.
-(*   move => ξ hξ. *)
+  move => h ha τ. move => /[dup] hτ.
-(*   asimpl. *)
+  move : ha => /[apply].
-(*   suff : ρ_ok Γ (funcomp (subst_PTm ξ) ρ) by hauto l:on. *)
+  move => [k][PA][h0]h1.
-(*   move : hξ hρ. clear. *)
+  apply h in hτ.
-(*   move => hξ hρ i k PA. *)
+  move => i.
-(*   specialize (hρ i). *)
+  destruct i as [i|].
-(*   move => h. *)
+  - move => k0 PA0. asimpl. rewrite {2}/funcomp. asimpl.
-(*   replace (funcomp (subst_PTm ξ) ρ i ) with *)
+    move : hτ => /[apply].
-(*     (subst_PTm ξ (ρ i)); last by asimpl. *)
+    by asimpl.
-(*   move : hρ  hξ => /[apply]. *)
+  - move => k0 PA0. asimpl. rewrite {2}/funcomp. asimpl.
-(*   move => [k0][PA0][h0]h1. *)
+    move => *. suff : PA0 = PA by congruence.
-(*   move : h0. asimpl => ?. *)
+    move : h0. asimpl.
-(*   have ? : PA0 = PA by eauto using InterpUniv_Functional'.  subst. *)
+    eauto using InterpUniv_Functional'.
-(*   done. *)
+Qed.
-(* Qed. *)
+
+
+Lemma morphing_SemWt : forall n Γ (a A : PTm n),
+    Γ ⊨ a ∈ A -> forall m Δ (ρ : fin n -> PTm m),
+      smorphing_ok Δ Γ ρ -> Δ ⊨ subst_PTm ρ a ∈ subst_PTm ρ A.
+Proof.
+  move => n Γ a A ha m Δ ρ hρ τ hτ.
+  have {}/hρ {}/ha := hτ.
+  asimpl. eauto.
+Qed.
 
 Lemma weakening_Sem n Γ (a : PTm n) A B i
   (h0 : Γ ⊨ B ∈ PUniv i)
@@ -1229,85 +1253,6 @@ Proof.
   hauto lq:on use: DJoin.cong,  DJoin.ProjCong.
 Qed.
 
-Lemma SE_ProjPair1 n Γ (a b : PTm n) A B i :
-  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊨ a ∈ A ->
-  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B ->
-  Γ ⊨ PProj PL (PPair a b) ≡ a ∈ A.
-Proof.
-  move => h0 h1 h2.
-  apply SemWt_SemEq; eauto using ST_Proj1, ST_Pair.
-  apply DJoin.FromRRed0. apply RRed.ProjPair.
-Qed.
-
-Lemma SE_ProjPair2 n Γ (a b : PTm n) A B i :
-  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊨ a ∈ A ->
-  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B ->
-  Γ ⊨ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B.
-Proof.
-  move => h0 h1 h2.
-  apply SemWt_SemEq; eauto using ST_Proj2, ST_Pair.
-  apply : ST_Conv_E. apply : ST_Proj2; eauto. apply : ST_Pair; eauto.
-  hauto l:on use:SBind_inst.
-  apply DJoin.cong. apply DJoin.FromRRed0. apply RRed.ProjPair.
-  apply DJoin.FromRRed0. apply RRed.ProjPair.
-Qed.
-
-Lemma SE_PairEta n Γ (a : PTm n) A B i :
-  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊨ a ∈ PBind PSig A B ->
-  Γ ⊨ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B.
-Proof.
-  move => h0 h. apply SemWt_SemEq; eauto.
-  apply : ST_Pair; eauto using ST_Proj1, ST_Proj2.
-  rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
-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 ->
-  Γ ⊨ a0 ≡ a1 ∈ A ->
-  Γ ⊨ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B.
-Proof.
-  move => hPi.
-  move => /SemEq_SemWt [hb0][hb1]hb /SemEq_SemWt [ha0][ha1]ha.
-  apply SemWt_SemEq; eauto using DJoin.AppCong, ST_App.
-  apply : ST_Conv_E; eauto using ST_App, DJoin.cong, DJoin.symmetric, SBind_inst.
-Qed.
-
-Lemma SSu_Eq n Γ (A B : PTm n) i :
-  Γ ⊨ A ≡ B ∈ PUniv i ->
-  Γ ⊨ A ≲ B.
-Proof. move /SemEq_SemWt => h.
-       qauto l:on use:SemWt_SemLEq, Sub.FromJoin.
-Qed.
-
-Lemma SSu_Transitive n Γ (A B C : PTm n) :
-  Γ ⊨ A ≲ B ->
-  Γ ⊨ B ≲ C ->
-  Γ ⊨ A ≲ C.
-Proof.
-  move => ha hb.
-  apply SemLEq_SemWt in ha, hb.
-  have ? : SN B by hauto l:on use:SemWt_SN.
-  move : ha => [ha0 [i [ha1 ha2]]]. move : hb => [hb0 [j [hb1 hb2]]].
-  qauto l:on use:SemWt_SemLEq, Sub.transitive.
-Qed.
-
-Lemma ST_Univ' n Γ i j :
-  i < j ->
-  Γ ⊨ PUniv i : PTm n ∈ PUniv j.
-Proof.
-  move => ?.
-  apply SemWt_Univ. move => ρ hρ. eexists. by apply InterpUniv_Univ.
-Qed.
-
-Lemma ST_Univ n Γ i :
-  Γ ⊨ PUniv i : PTm n ∈ PUniv (S i).
-Proof.
-  apply ST_Univ'. lia.
-Qed.
 
 Lemma ST_Nat n Γ i :
   Γ ⊨ PNat : PTm n ∈ PUniv i.
@@ -1336,6 +1281,7 @@ Proof.
   eauto using S_Suc.
 Qed.
 
+
 Lemma sn_unmorphing' n : (forall (a : PTm n) (s : SN a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SN b).
 Proof. hauto l:on use:sn_unmorphing. Qed.
 
@@ -1433,6 +1379,114 @@ Proof.
     hauto lq:on inv:option use:RPar.refl.
 Qed.
 
+Lemma SE_SucCong 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.
+  hauto q:on use:REReds.suc_inv, REReds.SucCong.
+Qed.
+
+
+
+Lemma SE_IndCong n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i :
+  funcomp (ren_PTm shift) (scons PNat Γ) ⊨ P0 ≡ P1 ∈ PUniv i ->
+  Γ ⊨ a0 ≡ a1 ∈ PNat ->
+  Γ ⊨ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
+  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.
+Proof.
+  move /SemEq_SemWt=>[hP0][hP1]hPe.
+  move /SemEq_SemWt=>[ha0][ha1]hae.
+  move /SemEq_SemWt=>[hb0][hb1]hbe.
+  move /SemEq_SemWt=>[hc0][hc1]hce.
+  apply SemWt_SemEq; eauto using ST_Ind, DJoin.IndCong.
+  apply ST_Conv_E with (A := subst_PTm (scons a1 VarPTm) P1) (i := i);
+    last by eauto using DJoin.cong', DJoin.symmetric.
+  apply : ST_Ind; eauto. eapply ST_Conv_E with (i := i); eauto.
+
+
+Lemma SE_ProjPair1 n Γ (a b : PTm n) A B i :
+  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B ->
+  Γ ⊨ PProj PL (PPair a b) ≡ a ∈ A.
+Proof.
+  move => h0 h1 h2.
+  apply SemWt_SemEq; eauto using ST_Proj1, ST_Pair.
+  apply DJoin.FromRRed0. apply RRed.ProjPair.
+Qed.
+
+Lemma SE_ProjPair2 n Γ (a b : PTm n) A B i :
+  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B ->
+  Γ ⊨ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B.
+Proof.
+  move => h0 h1 h2.
+  apply SemWt_SemEq; eauto using ST_Proj2, ST_Pair.
+  apply : ST_Conv_E. apply : ST_Proj2; eauto. apply : ST_Pair; eauto.
+  hauto l:on use:SBind_inst.
+  apply DJoin.cong. apply DJoin.FromRRed0. apply RRed.ProjPair.
+  apply DJoin.FromRRed0. apply RRed.ProjPair.
+Qed.
+
+Lemma SE_PairEta n Γ (a : PTm n) A B i :
+  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊨ a ∈ PBind PSig A B ->
+  Γ ⊨ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B.
+Proof.
+  move => h0 h. apply SemWt_SemEq; eauto.
+  apply : ST_Pair; eauto using ST_Proj1, ST_Proj2.
+  rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
+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 ->
+  Γ ⊨ a0 ≡ a1 ∈ A ->
+  Γ ⊨ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B.
+Proof.
+  move => hPi.
+  move => /SemEq_SemWt [hb0][hb1]hb /SemEq_SemWt [ha0][ha1]ha.
+  apply SemWt_SemEq; eauto using DJoin.AppCong, ST_App.
+  apply : ST_Conv_E; eauto using ST_App, DJoin.cong, DJoin.symmetric, SBind_inst.
+Qed.
+
+Lemma SSu_Eq n Γ (A B : PTm n) i :
+  Γ ⊨ A ≡ B ∈ PUniv i ->
+  Γ ⊨ A ≲ B.
+Proof. move /SemEq_SemWt => h.
+       qauto l:on use:SemWt_SemLEq, Sub.FromJoin.
+Qed.
+
+Lemma SSu_Transitive n Γ (A B C : PTm n) :
+  Γ ⊨ A ≲ B ->
+  Γ ⊨ B ≲ C ->
+  Γ ⊨ A ≲ C.
+Proof.
+  move => ha hb.
+  apply SemLEq_SemWt in ha, hb.
+  have ? : SN B by hauto l:on use:SemWt_SN.
+  move : ha => [ha0 [i [ha1 ha2]]]. move : hb => [hb0 [j [hb1 hb2]]].
+  qauto l:on use:SemWt_SemLEq, Sub.transitive.
+Qed.
+
+Lemma ST_Univ' n Γ i j :
+  i < j ->
+  Γ ⊨ PUniv i : PTm n ∈ PUniv j.
+Proof.
+  move => ?.
+  apply SemWt_Univ. move => ρ hρ. eexists. by apply InterpUniv_Univ.
+Qed.
+
+Lemma ST_Univ n Γ i :
+  Γ ⊨ PUniv i : PTm n ∈ PUniv (S i).
+Proof.
+  apply ST_Univ'. lia.
+Qed.
+
 Lemma SSu_Univ n Γ i j :
   i <= j ->
   Γ ⊨ PUniv i : PTm n ≲ PUniv j.