Eqv.wthen_cfg

imbrem · Jul 29, 2024 · e2b9e2b · e2b9e2b
1 parent 2850ff0
commit e2b9e2b
Show file tree

Hide file tree

Showing 11 changed files with 650 additions and 78 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean
@@ -562,8 +562,49 @@ theorem Eqv.wthen_cfg {B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     ((f.lwk (LCtx.InS.add_left_append _ _).slift).wthen g)
     (λi => (G i))
   := by
-  simp only [wthen, cfg_eq_ucfg, ucfg, lsubst_lsubst]
-  sorry
+  simp only [wthen, cfg_eq_ucfg, ucfg, lsubst_lsubst, <-lsubst_toSubst]
+  congr
+  ext i
+  simp only [
+    Subst.Eqv.get_comp, Subst.Eqv.get_toSubst, lsubst_br,
+    LCtx.InS.coe_slift, LCtx.InS.coe_add_left_append
+  ]
+  cases i using Fin.cases with
+  | zero =>
+    simp only [
+      Subst.Eqv.get_vlift, vwk_id_eq, cfgSubst_get, Fin.val_zero, Nat.liftWk, vwk1_cfg, vsubst_cfg,
+      lsubst_cfg, vwk1_br, vsubst_br, lsubst_br
+    ]
+    congr
+    · simp [-Subst.Eqv.liftn_append_singleton]
+    · funext i
+      cases i using Fin.elim1
+      simp only [Fin.elim1_zero, vwk1_vwk2]
+      simp only [
+        vwk1_lwk0, vsubst_lwk0, Subst.Eqv.liftn_append_singleton, Subst.Eqv.vlift_slift,
+        lsubst_slift_lwk0, <-vlift_cfgSubst, Subst.Eqv.vwk1_lsubst_vlift
+      ]
+      congr
+      simp only [vwk1, vwk_vwk]
+      simp only [<-vsubst_toSubst, vsubst_vsubst]
+      congr
+      ext
+      funext k
+      cases k <;> rfl
+  | succ i =>
+    simp only [List.singleton_append, List.append_eq, List.nil_append, List.get_eq_getElem,
+      List.length_cons, Fin.val_succ, List.getElem_cons_succ, List.length_singleton,
+      Nat.liftWk_succ, Set.mem_setOf_eq, Subst.Eqv.get_vlift]
+    rw [cfgSubst_get_ge (by simp), cfgSubst_get_ge (by simp)]
+    simp only [add_tsub_cancel_right, vwk1_br,
+      Term.Eqv.wk1_var0, vwk_id_br,
+      Term.Eqv.wk_id_var, vsubst_br, Term.Eqv.var0_subst0, List.append_eq, List.nil_append,
+      Nat.liftWk_succ, LCtx.InS.coe_slift, LCtx.InS.coe_add_left_append, id_eq,
+      Term.Eqv.wk_res_var, lsubst_br, Nat.add_succ_sub_one, Nat.add_zero,
+      Int.reduceNeg, eq_mpr_eq_cast, cast_eq, Subst.Eqv.get_vlift, vwk_id_eq]
+    rw [cfgSubst_get_ge (by simp), vwk1_br, vsubst_br]
+    simp
+    rfl
 
 theorem Eqv.wrseq_cfg {B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ Γ (B::L)) (g : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ C::L))
@@ -604,49 +645,6 @@ theorem Eqv.seq_cfg {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     ((f.lwk LCtx.InS.shf.slift ;; g.shf).ushf)
     (λi => (G i).vwk1)
   := by simp only [<-wseq_eq_seq, wseq_cfg]
-  -- induction f using Eqv.arrow_induction with
-  -- | br ℓ a hl =>
-  --   cases ℓ with
-  --   | zero =>
-  --     stop
-  --     -- simp only [List.append_eq, List.nil_append, br_zero_eq_ret, wk_res_self, lwk1_ret, ret_seq,
-  --     --   List.length_singleton, List.get_eq_getElem, List.singleton_append, vwk1_cfg, vsubst_cfg]
-  --     congr
-  --     sorry
-  --     funext i
-  --     induction (G i) using Quotient.inductionOn
-  --     induction a using Quotient.inductionOn
-  --     apply Eqv.eq_of_reg_eq
-  --     simp only [Set.mem_setOf_eq, InS.coe_vwk, Ctx.InS.coe_wk1, Fin.isValue, Fin.val_zero,
-  --       List.getElem_cons_zero, InS.coe_vsubst, Term.Subst.InS.coe_lift, Term.InS.coe_subst0,
-  --       Ctx.InS.coe_wk2, Region.vwk_vwk]
-  --     simp only [<-Region.vsubst_fromWk, Region.vsubst_vsubst]
-  --     congr
-  --     funext i
-  --     cases i <;> rfl
-  --   | succ ℓ => sorry
-  -- | let1 a r Ir =>
-  --   rw [let1_seq, vwk1_cfg]
-  --   simp only [vwk1_vwk2]
-  --   rw [Ir, <-cfg_let1]
-  --   congr
-  --   sorry
-  -- | let2 a r Ir =>
-  --   simp only [let2_seq, vwk1_cfg, vwk1_vwk2]
-  --   rw [Ir, <-cfg_let2]
-  --   congr
-  --   sorry
-  -- | case a l r Il Ir =>
-  --   simp only [case_seq, vwk1_cfg, vwk1_vwk2, Il, Ir]
-  --   rw [<-cfg_case]
-  --   congr
-  --   sorry
-  -- | cfg β dβ dG Iβ IG =>
-  --   conv =>
-  --     rhs
-  --     simp only [lwk_cfg, seq, lsubst_cfg, ushf_eq_cast, cast_cfg]
-  --     rw [cfg_cfg_eq_cfg']
-  --   sorry
 
 theorem Eqv.seq_cont {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::D::L))

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
@@ -354,6 +354,45 @@ theorem Eqv.vwk_id_eq
   : Eqv.vwk_id hρ r = r := by
   induction r using Quotient.inductionOn; rfl
 
+@[simp]
+theorem Eqv.vwk_id_br {Γ Δ : Ctx α ε} {L : LCtx α} {ℓ : ℕ} {A : Ty α} {hΓ : Γ.Wkn Δ id}
+  (a : Term.Eqv φ Δ ⟨A, ⊥⟩) (hℓ : L.Trg ℓ A)
+  : Eqv.vwk_id hΓ (br ℓ a hℓ) = br ℓ (a.wk_id hΓ) hℓ := by
+  induction a using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.vwk_id_let1 {Γ Δ : Ctx α ε} {L : LCtx α} {A : Ty α} {e : ε} {hΓ : Γ.Wkn Δ id}
+  (a : Term.Eqv φ Δ ⟨A, e⟩) (r : Eqv φ (⟨A, ⊥⟩::Δ) L)
+  : Eqv.vwk_id hΓ (let1 a r) = let1 (a.wk_id hΓ) (Eqv.vwk_id hΓ.slift_id r) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.vwk_id_let2 {Γ Δ : Ctx α ε} {L : LCtx α} {A B : Ty α} {e : ε} {hΓ : Γ.Wkn Δ id}
+  (a : Term.Eqv φ Δ ⟨Ty.prod A B, e⟩) (r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Δ) L)
+  : Eqv.vwk_id hΓ (let2 a r) = let2 (a.wk_id hΓ) (Eqv.vwk_id hΓ.slift_id₂ r) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.vwk_id_case {Γ Δ : Ctx α ε} {L : LCtx α} {A B : Ty α} {e : ε} {hΓ : Γ.Wkn Δ id}
+  (a : Term.Eqv φ Δ ⟨Ty.coprod A B, e⟩) (r : Eqv φ (⟨A, ⊥⟩::Δ) L) (s : Eqv φ (⟨B, ⊥⟩::Δ) L)
+  : Eqv.vwk_id hΓ (case a r s)
+  = case (a.wk_id hΓ) (Eqv.vwk_id hΓ.slift_id r) (Eqv.vwk_id hΓ.slift_id s) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  induction s using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.vwk_id_cfg {Γ Δ : Ctx α ε} {L : LCtx α} {R : LCtx α} {hΓ : Γ.Wkn Δ id}
+  (dβ : Eqv φ Δ (R ++ L)) (dG : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Δ) (R ++ L))
+  : Eqv.vwk_id hΓ (cfg R dβ dG) = cfg R (Eqv.vwk_id hΓ dβ)
+  (λi => Eqv.vwk_id hΓ.slift_id (dG i)) := by sorry
+
 theorem Eqv.shf_vwk {Γ : Ctx α ε} {L R : LCtx α} {Y : Ty α}
   {ρ : Ctx.InS Γ Δ}
   {d : Eqv φ Δ (R ++ (Y::L))}
@@ -489,6 +528,10 @@ theorem Eqv.vsubst_vsubst {Γ Δ Ξ : Ctx α ε} {L : LCtx α} {r : Eqv φ Ξ L}
   induction r using Quotient.inductionOn
   simp [InS.vsubst_vsubst]
 
+theorem Eqv.vsubst_toSubst {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {L} {r : Eqv φ Δ L}
+  : r.vsubst ⟦ρ.toSubst⟧ = r.vwk ρ
+  := by induction r using Quotient.inductionOn; simp [InS.vsubst_toSubst]
+
 @[simp]
 theorem Eqv.vsubst_br {Γ : Ctx α ε} {L : LCtx α}
   {σ : Term.Subst.Eqv φ Γ Δ} {ℓ} {a : Term.Eqv φ Δ ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A}
@@ -671,10 +714,33 @@ def Eqv.lwk0
   {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ Γ L)
   : Eqv φ Γ (head::L) := Eqv.lwk LCtx.InS.wk0 r
 
--- @[simp]
--- theorem Eqv.lwk0_quot
---   {Γ : Ctx α ε} {L : LCtx α} {r : InS φ Γ L}
---   : Eqv.lwk0 ⟦r⟧ = ⟦r.lwk0⟧ := rfl
+theorem Eqv.vwk1_lwk0 {Γ : Ctx α ε} {L : LCtx α}
+  {r : Eqv φ (head::Γ) L}
+  : (r.lwk0 (head := head')).vwk1 (inserted := inserted) = r.vwk1.lwk0
+  := by rw [lwk0, vwk1, vwk_lwk]; rfl
+
+theorem Eqv.lwk0_vwk1 {Γ : Ctx α ε} {L : LCtx α}
+  {r : Eqv φ (head::Γ) L}
+  : r.vwk1.lwk0 = (r.lwk0 (head := head')).vwk1 (inserted := inserted) := by rw [vwk1_lwk0]
+
+theorem Eqv.vsubst_lwk0 {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ} {r : Eqv φ Δ L}
+  : r.lwk0.vsubst σ = (r.vsubst σ).lwk0 (head := head) := by
+  induction σ using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  apply Eqv.eq_of_reg_eq
+  simp [Region.vsubst_lwk]
+
+theorem Eqv.lwk0_vsubst {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ} {r : Eqv φ Δ L}
+  : (r.vsubst σ).lwk0 (head := head) = r.lwk0.vsubst σ := by
+  induction σ using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  apply Eqv.eq_of_reg_eq
+  simp [Region.vsubst_lwk]
+
+@[simp]
+theorem Eqv.lwk0_quot
+  {Γ : Ctx α ε} {L : LCtx α} {r : InS φ Γ L}
+  : Eqv.lwk0 (head := head) ⟦r⟧ = ⟦r.lwk0⟧ := rfl
 
 def Eqv.lwk1
   {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ Γ (head::L))