lsubst_pack_append_unpack sorry

imbrem · Sep 22, 2024 · 3e97a01 · 3e97a01
1 parent 8a5372b
commit 3e97a01
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 18 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean
@@ -592,7 +592,7 @@ theorem Eqv.lsubst_vlift_slift_seq {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx
     | zero => rfl
     | succ k =>
       simp only [Function.comp_apply, Subst.lift, vwk2_vwk1]
-      simp only [Region.vwk1_lwk, vsubst_lwk]
+      simp only [Region.vwk1_lwk, Region.vsubst_lwk]
       congr
       simp only [Region.vwk1, Region.vwk_vwk]
       simp only [<-Region.vsubst_fromWk, Region.vsubst_vsubst]

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
@@ -859,19 +859,19 @@ 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
+theorem Eqv.vsubst_lwk {Γ Δ : Ctx α ε} {L K : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ} {r : Eqv φ Δ L}
+  {ρ : L.InS K}
+  : (r.lwk ρ).vsubst σ = (r.vsubst σ).lwk ρ := by
   induction σ using Quotient.inductionOn
   induction r using Quotient.inductionOn
   apply Eqv.eq_of_reg_eq
   simp [Region.vsubst_lwk]
 
+theorem Eqv.vsubst_lwk0 {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ} {r : Eqv φ Δ L}
+  : r.lwk0.vsubst σ = (r.vsubst σ).lwk0 (head := head) := 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]
+  : (r.vsubst σ).lwk0 (head := head) = r.lwk0.vsubst σ := by rw [vsubst_lwk0]
 
 @[simp]
 theorem Eqv.lwk0_quot

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
@@ -285,15 +285,13 @@ theorem Eqv.lsubst_pack_append_unpack {Γ : Ctx α ε} {L R : LCtx α}
           Term.Eqv.inj_l, Term.Eqv.inj_r, vwk2, Nat.liftnWk, case_inl, case_inr, let1_beta, lwk_lwk,
           vwk1_lwk]
         congr
-        sorry
-        -- generalize Term.Eqv.pack_app (φ := φ) = P
-        -- induction P using Quotient.inductionOn
-        -- simp only [unpack_def]
-        -- apply eq_of_reg_eq
-        -- simp [<-Region.vsubst_fromWk, Region.vsubst_vsubst]
-        -- congr
-        -- funext k; cases k using Nat.cases2 <;> simp [Nat.liftnWk, Term.Subst.comp]
-        -- sorry
+        simp only [<-Ctx.InS.lift_wk1, vwk_lwk, vwk_lift_unpack, vsubst_lwk, vsubst_lift_unpack]
+        congr 1
+        conv =>
+          lhs; rhs; rw [<-vwk1_unpack, vwk1, <-vsubst_fromWk, vsubst_vsubst, vsubst_id']
+          · skip
+          · tactic => ext i; apply Term.Eqv.eq_of_term_eq; cases i using Fin.cases <;> rfl
+        rw [vsubst_lift_unpack]
     · simp only [Eqv.nil_vwk1, Term.Eqv.seq_inj_r, Term.Eqv.wk1_inr, Term.Eqv.wk1_inj_r,
       vwk1_br, Term.Eqv.wk1_nil, vwk1_case, Term.Eqv.wk1_var0, List.length_cons, Fin.zero_eta,
       List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, vwk2_br, Term.Eqv.wk2_nil]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "87c93626b51f79de48f5fdca516f3a0b2deb9cfd",
+   "rev": "ba3db161926d69d9d7b6629b38a98630a32204bb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,