Tap

imbrem · Sep 4, 2024 · 12ed655 · 12ed655
1 parent 0559ce9
commit 12ed655
Show file tree

Hide file tree

Showing 3 changed files with 130 additions and 7 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
@@ -316,6 +316,39 @@ theorem Term.comp_wk (ρ σ)
 theorem Term.wk_comp (ρ σ)
   : @wk φ (ρ ∘ σ) = wk ρ ∘ wk σ := (comp_wk ρ σ).symm
 
+theorem Term.wk_injective {ρ} (hρ : Function.Injective ρ) : Function.Injective (wk (φ := φ) ρ) := by
+  intro a a' heq
+  induction a generalizing a' ρ <;> cases a'
+  case var.var =>
+    simp only [wk, var.injEq] at heq
+    simp [hρ heq]
+  case op.op _ _ I _ _ =>
+    simp only [wk, op.injEq] at heq
+    simp [heq.1, I hρ heq.2]
+  case let1.let1 _ Ia Ib _ _ =>
+    simp only [wk, let1.injEq] at heq
+    simp [Ia hρ heq.1, Ib (Nat.liftWk_injective_of_injective hρ) heq.2]
+  case pair.pair _ Ia Ib _ _ =>
+    simp only [wk, pair.injEq] at heq
+    simp [Ia hρ heq.1, Ib hρ heq.2]
+  case let2.let2 _ Ia Ib _ _ =>
+    simp only [wk, let2.injEq] at heq
+    simp [Ia hρ heq.1, Ib (Nat.liftnWk_injective_of_injective hρ) heq.2]
+  case inl.inl _ I _ =>
+    simp only [wk, inl.injEq] at heq
+    simp [I hρ heq]
+  case inr.inr _ I _ =>
+    simp only [wk, inr.injEq] at heq
+    simp [I hρ heq]
+  case case.case _ Ie Il Ir _ _ _ =>
+    simp only [wk, case.injEq] at heq
+    have hρ' := Nat.liftWk_injective_of_injective hρ
+    simp [Ie hρ heq.1, Il hρ' heq.2.1, Ir hρ' heq.2.2]
+  case abort.abort _ I _ =>
+    simp only [wk, abort.injEq] at heq
+    simp [I hρ heq]
+  all_goals (cases heq <;> rfl)
+
 def Term.wk0 : Term φ → Term φ := wk Nat.succ
 
 def Term.wk1 : Term φ → Term φ := wk (Nat.liftWk Nat.succ)
@@ -330,6 +363,21 @@ def Term.swap01 : Term φ → Term φ := wk (Nat.swap0 1)
 
 def Term.swap02 : Term φ → Term φ := wk (Nat.swap0 2)
 
+theorem Term.wk0_injective : Function.Injective (@Term.wk0 φ)
+  := Term.wk_injective Nat.succ_injective
+
+theorem Term.wk1_injective : Function.Injective (@Term.wk1 φ)
+  := Term.wk_injective (Nat.liftWk_injective_of_injective Nat.succ_injective)
+
+theorem Term.wk2_injective : Function.Injective (@Term.wk2 φ)
+  := Term.wk_injective (Nat.liftnWk_injective_of_injective Nat.succ_injective)
+
+theorem Term.wk3_injective : Function.Injective (@Term.wk3 φ)
+  := Term.wk_injective (Nat.liftnWk_injective_of_injective Nat.succ_injective)
+
+theorem Term.wk4_injective : Function.Injective (@Term.wk4 φ)
+  := Term.wk_injective (Nat.liftnWk_injective_of_injective Nat.succ_injective)
+
 theorem Term.wk0_let1 (e r : Term φ) : (let1 e r).wk0 = let1 e.wk0 r.wk1 := rfl
 
 theorem Term.wk1_let1 (e r : Term φ) : (let1 e r).wk1 = let1 e.wk1 r.wk2

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean
@@ -41,7 +41,19 @@ theorem Term.Subst.fvs_liftn_def {σ : Term.Subst φ} {i n}
 
 theorem Term.Subst.biUnion_fvs_lift {σ : Term.Subst φ} {s : Set ℕ}
   : ⋃i ∈ s, (σ.lift.fvs i).liftFv = ⋃i ∈ s.liftFv, σ.fvs i := by
-  sorry
+  ext k
+  simp only [Set.mem_iUnion, Set.mem_liftFv, exists_prop', nonempty_prop]
+  constructor
+  · intro ⟨i, hi, hk⟩
+    cases i with
+    | zero => simp [Subst.fvs] at hk
+    | succ i =>
+      simp only [fvs, lift_succ, fvs_wk, Nat.succ_eq_add_one, Set.mem_image, add_left_inj,
+        exists_eq_right] at hk
+      exact ⟨_, hi, hk⟩
+  · intro ⟨i, hi, hk⟩
+    exact ⟨i + 1, hi, by simp only [fvs, lift_succ, fvs_wk, Nat.succ_eq_add_one, Set.mem_image,
+      add_left_inj, exists_eq_right]; exact hk⟩
 
 theorem Term.Subst.biUnion_fvs_liftn {σ : Term.Subst φ} {s : Set ℕ}
   : ⋃i ∈ s, ((σ.liftn n).fvs i).liftnFv n = ⋃i ∈ s.liftnFv n, σ.fvs i := by
@@ -132,14 +144,77 @@ theorem Region.fvs_vsubst0_le (t : Region φ) (s : Term φ)
   · rw [Set.union_comm]
   · simp
 
-theorem Term.subst_eqOn_fvs {t : Term φ} {σ σ' : Subst φ} (h : t.fvs.EqOn σ σ')
-  : t.subst σ = t.subst σ' := by sorry
+theorem Term.Subst.eqOn_lift_iff {σ σ' : Term.Subst φ} {s : Set ℕ}
+  : s.EqOn σ.lift σ'.lift ↔ s.liftFv.EqOn σ σ' := by
+  constructor <;> intro h n hn
+  · rw [Set.mem_liftFv] at hn
+    have h := h hn
+    simp only [lift_succ] at h
+    sorry
+  · sorry
+
+theorem Term.Subst.eqOn_liftn_iff {σ σ' : Term.Subst φ} {s : Set ℕ}
+  : s.EqOn (σ.liftn n) (σ'.liftn n) ↔ (s.liftnFv n).EqOn σ σ' := sorry
+
+theorem Term.subst_eq_iff {t : Term φ} {σ σ' : Subst φ}
+  : t.subst σ = t.subst σ' ↔ t.fvs.EqOn σ σ' := by induction t generalizing σ σ' with
+  | _ => simp [Subst.eqOn_lift_iff, Subst.eqOn_liftn_iff, and_assoc, *]
+
+theorem Term.subst_eqOn_fvs_iff {t : Term φ} {σ σ' : Subst φ}
+  : t.fvs.EqOn σ σ' ↔ t.subst σ = t.subst σ' := subst_eq_iff.symm
+
+theorem Term.subst_eqOn_fvs {t : Term φ} {σ σ' : Subst φ}
+  : t.fvs.EqOn σ σ' → t.subst σ = t.subst σ' := subst_eq_iff.mpr
 
 theorem Term.subst_eqOn_fvi {t : Term φ} {σ σ' : Subst φ} (h : (Set.Iio t.fvi).EqOn σ σ')
   : t.subst σ = t.subst σ' := t.subst_eqOn_fvs (h.mono t.fvs_fvi)
 
+theorem Region.vsubst_eq_iff {r : Region φ} {σ σ' : Term.Subst φ}
+  : r.vsubst σ = r.vsubst σ' ↔ r.fvs.EqOn σ σ' := by induction r generalizing σ σ' with
+  | _ => simp [
+    Term.subst_eq_iff, and_assoc, Term.Subst.eqOn_lift_iff, Term.Subst.eqOn_liftn_iff,
+    funext_iff, Set.eqOn_iUnion, *
+  ]
+
 theorem Region.vsubst_eqOn_fvs {r : Region φ} {σ σ' : Term.Subst φ} (h : r.fvs.EqOn σ σ')
-  : r.vsubst σ = r.vsubst σ' := by sorry
+  : r.vsubst σ = r.vsubst σ' := by induction r generalizing σ σ' with
+  | br => simp [Term.subst_eqOn_fvs h]
+  | let1 _ _ I =>
+    simp only [vsubst, let1.injEq]
+    constructor
+    exact Term.subst_eqOn_fvs (h.mono (by simp))
+    apply I
+    rw [Term.Subst.eqOn_lift_iff]
+    exact h.mono (by simp)
+  | let2 _ _ I =>
+    simp only [vsubst, let2.injEq]
+    constructor
+    exact Term.subst_eqOn_fvs (h.mono (by simp))
+    apply I
+    rw [Term.Subst.eqOn_liftn_iff]
+    exact h.mono (by simp)
+  | case _ _ _ Il Ir =>
+    simp only [vsubst, case.injEq]
+    constructor
+    exact Term.subst_eqOn_fvs (h.mono (by simp [Set.union_assoc]))
+    constructor
+    apply Il
+    rw [Term.Subst.eqOn_lift_iff]
+    exact h.mono (by apply Set.subset_union_of_subset_left; simp)
+    apply Ir
+    rw [Term.Subst.eqOn_lift_iff]
+    exact h.mono (by apply Set.subset_union_of_subset_right; simp)
+  | cfg _ _ _ Iβ IG =>
+    simp only [vsubst, cfg.injEq, heq_eq_eq, true_and]
+    constructor
+    exact Iβ (h.mono (by simp))
+    ext k
+    apply IG
+    rw [Term.Subst.eqOn_lift_iff]
+    apply h.mono
+    apply Set.subset_union_of_subset_right
+    apply Set.subset_iUnion_of_subset
+    rfl
 
 theorem Region.vsubst_eqOn_fvi {r : Region φ} {σ σ' : Term.Subst φ} (h : (Set.Iio r.fvi).EqOn σ σ')
   : r.vsubst σ = r.vsubst σ' := r.vsubst_eqOn_fvs (h.mono r.fvs_fvi)

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad85095b6112bb3a7ad6c068fd0844d1e35706f2",
+   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3a97fe99a8c8180b83efac3be780aa9342a2529c",
+   "rev": "df80b0dd2548c76fbdc3fe5d3a96873dfd46c0dc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3c270bec05c94350f961c5fae7399fa815527418",
+   "rev": "5e4ff7246e2e63e5053c64b9a7464a0bd97659fb",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",