Tap

DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean

@@ -225,7 +225,9 @@ theorem TStep.vwk {Γ Δ : Ctx α ε} {L r r' ρ} (hρ : Γ.Wkn Δ ρ)
     ((p.wk_eff (λi hi => by
       have hi : i < Δ.length := d.fvs hi
       have hρ := hρ i hi
-      simp [Ctx.effect, hρ.length, hi, hρ.get.2]
+      simp only [Function.comp_apply, Ctx.effect, hρ.length, ↓reduceDIte, List.get_eq_getElem, hi,
+        ge_iff_le]
+      exact hρ.get.2
       )).vwk ρ)
   -- | TStep.step_op d d' p => TStep.step_op (d.vwk hρ) (d'.vwk hρ)
   --   ((p.wk_eff (λi hi => by
@@ -832,6 +834,11 @@ def Eqv.lwk_id {Γ : Ctx α ε} {L K : LCtx α} (hρ : L.Wkn K id) (r : Eqv φ 
     (λr => InS.q (r.lwk_id hρ))
     (λ_ _ h => Quotient.sound sorry)
 
+def Eqv.vsubst {Γ Δ : Ctx α ε} {L : LCtx α} (σ : Term.Subst.InS φ Γ Δ) (r : Eqv φ Δ L)
+  : Eqv φ Γ L := Quotient.liftOn r
+    (λr => InS.q (r.vsubst σ))
+    (λ_ _ h => Quotient.sound sorry)
+
 @[simp]
 theorem InS.vwk_q {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Γ.InS Δ} {r : InS φ Δ L}
    : (r.q).vwk ρ = (r.vwk ρ).q := rfl
@@ -1186,7 +1193,8 @@ theorem InS.cfg_br_lt {Γ : Ctx α ε} {L : LCtx α}
   (R : LCtx α)  (G : (i : Fin R.length) → InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
   (hℓ : (R ++ L).Trg ℓ A) (hℓ' : ℓ < R.length)
   : (InS.br ℓ a hℓ).cfg R G
-  ≈ (let1 a $ (G ⟨ℓ, hℓ'⟩).vwk_id (by simp [List.get_append ℓ hℓ' ▸ hℓ.get])).cfg R G
+  ≈ (let1 a $ (G ⟨ℓ, hℓ'⟩).vwk_id (by simp only [Ctx.Wkn.lift_id_iff,
+    Prod.mk_le_mk, le_refl, and_true, Ctx.Wkn.id]; exact List.get_append ℓ hℓ' ▸ hℓ.get)).cfg R G
   := EqvGen.rel _ _ $ Wf.Cong.rel $
   TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
 
@@ -1195,7 +1203,8 @@ theorem Eqv.cfg_br_lt {Γ : Ctx α ε} {L : LCtx α}
   (R : LCtx α)  (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
   (hℓ : (R ++ L).Trg ℓ A) (hℓ' : ℓ < R.length)
   : (InS.br ℓ a hℓ).q.cfg R G
-  = (let1 a $ (G ⟨ℓ, hℓ'⟩).vwk_id (by simp [List.get_append ℓ hℓ' ▸ hℓ.get])).cfg R G
+  = (let1 a $ (G ⟨ℓ, hℓ'⟩).vwk_id (by simp only [Ctx.Wkn.lift_id_iff,
+    Prod.mk_le_mk, le_refl, and_true, Ctx.Wkn.id]; exact List.get_append ℓ hℓ' ▸ hℓ.get)).cfg R G
   := by
   simp only [cfg]
   generalize hG : Quotient.finChoice G = G'
@@ -1448,16 +1457,34 @@ theorem InS.dead_cfg_left {Γ : Ctx α ε} {L : LCtx α}
   (R S : LCtx α) (β : InS φ Γ (S ++ L))
   (G : (i : Fin R.length) → InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ S ++ L))
   (G' : (i : Fin S.length) → InS φ (⟨S.get i, ⊥⟩::Γ) (S ++ L))
-  : (β.lwk ⟨(· + R.length), sorry⟩).cfg' (R.length + S.length) (R ++ S) (by rw [List.length_append])
+  : (β.lwk ((LCtx.InS.add_left_append (S ++ L) R).cast rfl (by rw [List.append_assoc]))).cfg'
+    (R.length + S.length) (R ++ S) (by rw [List.length_append])
       (Fin.addCases
         (λi => (G i).cast sorry rfl)
-        (λi => ((G' i).cast sorry rfl).lwk ⟨(· + R.length), sorry⟩))
+        (λi => ((G' i).cast sorry rfl).lwk
+          ((LCtx.InS.add_left_append (S ++ L) R).cast rfl (by rw [List.append_assoc]))))
     ≈ β.cfg S G'
   := sorry
 
 -- TODO: Eqv.dead_cfg_left; after Eqv.lwk
 
--- TODO: let1 β
+theorem InS.let1_beta {Γ : Ctx α ε} {L : LCtx α}
+  (a : Term.InS φ Γ ⟨A, ⊥⟩)
+  (r : InS φ (⟨A, ⊥⟩::Γ) L)
+    : let1 a r ≈ r.vsubst a.subst0
+  := EqvGen.rel _ _ $ Wf.Cong.rel $
+  TStep.step InS.coe_wf InS.coe_wf (by
+    constructor
+    sorry
+  )
+
+theorem Eqv.let1_beta {Γ : Ctx α ε} {L : LCtx α}
+  (a : Term.InS φ Γ ⟨A, ⊥⟩)
+  (r : Eqv φ (⟨A, ⊥⟩::Γ) L)
+    : let1 a r = r.vsubst a.subst0
+  := by
+  induction r using Quotient.inductionOn
+  exact Eqv.sound (InS.let1_beta a _)
 
 theorem InS.initial {Γ : Ctx α ε} {L : LCtx α} (hi : Γ.IsInitial) (r r' : InS φ Γ L) : r ≈ r'
   := EqvGen.rel _ _ $ Wf.Cong.rel (TStep.initial hi r.2 r'.2)

DeBruijnSSA/BinSyntax/Subst.lean

@@ -294,7 +294,10 @@ def Terminator.Subst.WfD.vliftn_append_cons' (V) {Ξ : Ctx α ε} (hn : n = Ξ.l
   := hn ▸ hσ.vliftn_append_cons V Ξ
 
 def LCtx.Trg.subst (hσ : σ.WfD Γ L K) (h : L.Trg n A) : (σ n).WfD (⟨A, ⊥⟩::Γ)  K
-  := (hσ ⟨n, h.length⟩).vwk_id (Ctx.Wkn.id.lift_id (by simp [h.get]))
+  := (hσ ⟨n, h.length⟩).vwk_id (Ctx.Wkn.id.lift_id (by
+    simp only [List.get_eq_getElem, Prod.mk_le_mk, le_refl, and_true]
+    exact h.get
+  ))
 
 def LCtx.Trg.subst0
   {a : Term φ} (hσ : σ.WfD Γ L K) (h : L.Trg n A) (ha : a.WfD Γ ⟨A, ⊥⟩)
@@ -394,7 +397,10 @@ def Region.Subst.WfD.vliftn_append_cons' (V) {Ξ : Ctx α ε} (hn : n = Ξ.lengt
   := hn ▸ hσ.vliftn_append_cons V Ξ
 
 def LCtx.Trg.rsubst (hσ : σ.WfD Γ L K) (h : L.Trg n A) : (σ n).WfD (⟨A, ⊥⟩::Γ)  K
-  := (hσ ⟨n, h.length⟩).vwk_id (Ctx.Wkn.id.lift_id (by simp [h.get]))
+  := (hσ ⟨n, h.length⟩).vwk_id (Ctx.Wkn.id.lift_id (by
+    simp only [List.get_eq_getElem, Prod.mk_le_mk, le_refl, and_true]
+    exact h.get
+    ))
 
 def LCtx.Trg.rsubst0
   {a : Term φ} (hσ : σ.WfD Γ L K) (h : L.Trg n A) (ha : a.WfD Γ ⟨A, ⊥⟩)

DeBruijnSSA/BinSyntax/Syntax.lean

@@ -298,10 +298,10 @@ theorem Terminator.toTerminator_toRegion (k : ℕ) (r : Terminator φ)
 theorem TRegion.IsTerminator.eq_cfg (k : ℕ) {r : TRegion φ} (h : r.IsTerminator)
   : r = TRegion.cfg (r.toTerminator k) 0 Fin.elim0 := by cases h with
   | cfg r _ =>
-    simp only [toTerminator, tsub_zero, ↓reduceDite, Terminator.lwk_id',
+    simp only [toTerminator, tsub_zero, ↓reduceDIte, Terminator.lwk_id',
     cfg.injEq, heq_eq_eq, true_and]
     constructor
-    . simp only [Nat.sub_zero, Nat.not_lt_zero, ↓reduceDite, Terminator.lsubst_id_apply',
+    . simp only [Nat.sub_zero, Nat.not_lt_zero, ↓reduceDIte, Terminator.lsubst_id_apply',
       Terminator.lwk_id']
       induction k with
       | zero => rfl
@@ -447,15 +447,15 @@ theorem Region.IsTRegion.eq_toTRegion {r : Region φ} (h : r.IsTRegion) : r = r.
     induction hr with
     | br =>
       simp only [num_defs, append_cfg, add_zero, Nat.liftnWk_id', lwk_id, Terminator.toRegion,
-        Fin.addCases, ↓reduceDite, Nat.add_zero, Function.comp_apply, lwk_id',
+        Fin.addCases, ↓reduceDIte, Nat.add_zero, Function.comp_apply, lwk_id',
         eq_rec_constant]
       rw [Region.cfg_cast_eq _ (0 + n) n _ (by simp)]
       congr
       funext i
       simp [Fin.subNat, <-I]
     | case _ _ _ hs ht =>
       simp only [append_cfg, num_defs, Nat.add_zero, add_zero, Nat.liftnWk_id', lwk_id,
-        Terminator.toRegion, <- hs.eq_coe, <- ht.eq_coe, Fin.addCases, ↓reduceDite,
+        Terminator.toRegion, <- hs.eq_coe, <- ht.eq_coe, Fin.addCases, ↓reduceDIte,
         Function.comp_apply, lwk_id', eq_rec_constant, zero_add, true_and]
       rw [Region.cfg_cast_eq _ (0 + n) n _ (by simp)]
       congr

DeBruijnSSA/BinSyntax/Typing.lean

@@ -12,8 +12,6 @@ section Basic
 
 -- Can we even do centrality? Propositional parametrization?
 
-variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [PartialOrder ε] [Bot ε]
-
 inductive Ty (α : Type u) where
   | base : α → Ty α
   | prod : Ty α → Ty α → Ty α
@@ -22,6 +20,8 @@ inductive Ty (α : Type u) where
   | empty : Ty α
   deriving Repr, DecidableEq
 
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [PartialOrder ε] [Bot ε]
+
 inductive Ty.IsInitial : Ty α → Prop
   | prod_left : ∀{A}, IsInitial A → IsInitial (prod A B)
   | prod_right : ∀{B}, IsInitial B → IsInitial (prod A B)
@@ -122,7 +122,8 @@ theorem Ctx.Var.shead {head : Ty α × ε} {Γ : Ctx α ε}
   : Var (head::Γ) 0 head := Var.head (le_refl _) Γ
 
 theorem Ctx.Var.step {Γ : Ctx α ε} (h : Var Γ n V) : Var (V'::Γ) (n+1) V
-  := ⟨by simp [h.length], by simp [h.get]⟩
+  := ⟨by simp [h.length], by simp only [List.length_cons, List.get_eq_getElem,
+    List.getElem_cons_succ, ge_iff_le]; exact h.get⟩
 
 theorem Ctx.Var.tail {Γ : Ctx α ε} {n} (h : Var (V'::Γ) (n+1) V) : Var Γ n V
   := ⟨Nat.lt_of_succ_lt_succ h.length, h.get⟩
@@ -439,7 +440,7 @@ theorem Term.Wf.unit' {Γ : Ctx α ε} {e} : Wf (φ := φ) Γ Term.unit ⟨Ty.un
 -- def Term.WfD.toInfTy {Γ : Ctx α ε} {a : Term φ} {A e} (h : WfD Γ a ⟨A, e⟩) : WfD Γ a ⟨a.infTy Γ, e⟩
 --   := match h with
 --   | var dv => var (by
---     constructor <;> simp only [infTy, dv.length, ↓reduceDite]
+--     constructor <;> simp only [infTy, dv.length, ↓reduceDIte]
 --     exact ⟨le_refl _, dv.get.2⟩
 --     )
 --   | op df de => op ⟨df.src, le_refl _, df.effect⟩ de
@@ -1265,7 +1266,8 @@ theorem Ctx.Var.exists_of_mem {Γ : Ctx α ε} {V} (h : V ∈ Γ)
   | head => exact ⟨0, by simp, rfl⟩
   | tail _ _ I =>
     have ⟨n, hn, hn'⟩ := I;
-    exact ⟨n + 1, hn.step, by simp [hn']⟩
+    exact ⟨n + 1, hn.step, by simp only [List.length_cons, List.get_eq_getElem,
+      List.getElem_cons_succ]; exact hn'⟩
 
 theorem Ctx.mem_wk {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ ρ) (hV : V ∈ Δ) : ∃V', V' ∈ Γ ∧ V' ≤ V
   :=
@@ -1281,7 +1283,9 @@ theorem Ctx.IsInitial.wk {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ 
 
 theorem Ctx.Wkn.effect {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ ρ) (i : ℕ) (hi : i < Δ.length)
   : (Γ.effect (ρ i)) ≤ Δ.effect i
-  := by simp [Ctx.effect, (h i hi).length, hi, (h i hi).get.2]
+  := by
+    simp only [Ctx.effect, (h i hi).length, ↓reduceDIte, List.get_eq_getElem, hi]
+    exact (h i hi).get.2
 
 -- theorem Ctx.EWkn.id_len_le : Γ.EWkn Δ _root_.id → Δ.length ≤ Γ.length := by
 --   apply List.NEWkn.id_len_le
@@ -1477,6 +1481,15 @@ theorem LCtx.InS.coe_comp {L K J : LCtx α} (ρ : LCtx.InS K J) (σ : LCtx.InS L
   : (ρ.comp σ : ℕ → ℕ) = (ρ : ℕ → ℕ) ∘ (σ : ℕ → ℕ)
   := rfl
 
+theorem LCtx.Wkn.add_left_append (original added : LCtx α)
+  : original.Wkn (added ++ original) (· + added.length)
+  := λi hi => ⟨
+    by rw [List.length_append]; simp [i.add_comm, hi],
+    by rw [List.get_append_right] <;> simp [hi]⟩
+
+def LCtx.InS.add_left_append (original added : LCtx α) : InS original (added ++ original)
+  := ⟨(· + added.length), Wkn.add_left_append original added⟩
+
 theorem LCtx.Trg.wk (h : L.Wkn K ρ) (hK : L.Trg n A) : K.Trg (ρ n) A where
   length := (h n hK.length).1
   get := le_trans hK.get (h n hK.length).2
@@ -1765,7 +1778,8 @@ def Term.WfD.var1_pure {head ty} {Γ : Ctx α ε} {effect}
 theorem Term.WfD.effect_le
   {Γ : Ctx α ε} {a : Term φ} {A e} (h : WfD Γ a ⟨A, e⟩) : a.effect Γ.effect ≤ e
   := match h with
-  | var dv => by simp [Ctx.effect, effect, dv.length, dv.get.right]
+  | var dv => by
+    simp only [effect, Ctx.effect, dv.length, ↓reduceDIte, List.get_eq_getElem]; exact dv.get.2
   | op df de => sup_le_iff.mpr ⟨df.effect, de.effect_le⟩
   | pair dl dr => sup_le_iff.mpr ⟨dl.effect_le, dr.effect_le⟩
   | inl dl => dl.effect_le

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
+   "scope": "leanprover-community",
+   "rev": "bba0af6e930ebcbabfacf021b21dd881d58aaa9d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "aea83a8a13ae4144e9e5d86f8749238f17814ef3",
+   "scope": "leanprover-community",
+   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.38",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "scope": "leanprover-community",
+   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "c1c6ecdf30249cdfe66419b059d1b7b0db99fa73",
+   "scope": "",
+   "rev": "4f76c653e261de1da9ba36bac58f4ca0eb22cc38",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +74,8 @@
   {"url": "https://github.com/imbrem/discretion.git",
    "type": "git",
    "subDir": null,
-   "rev": "fba46d9dbcddaeceb2cc3c780c44b2b3ea3eff86",
+   "scope": "",
+   "rev": "8c5bf49a5e24f490f37b8a75ddbece8f7a9ab237",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc3
+leanprover/lean4:v4.10.0-rc1