Anti-sorry

DeBruijnSSA/BinSyntax/Syntax/Effect/Definitions.lean

@@ -341,16 +341,35 @@ variable [Φ : EffectSet φ ε] [Bot ε] [SemilatticeSup ε]
 
 theorem Term.effect_le {Γ Δ : ℕ → ε} (e : Term φ) (H : ∀i ∈ e.fvs, Γ i ≤ Δ i)
   : e.effect Γ ≤ e.effect Δ := by
-  induction e with
+  induction e generalizing Γ Δ with
   | var => exact H _ rfl
   | op f e I => exact sup_le_sup_left (I H) _
-  | let1 => sorry
+  | let1 a b Ia Ib =>
+    apply sup_le_sup (Ia (λi hi => H i (Or.inl hi))) (Ib _)
+    intro i hi
+    cases i with
+    | zero => rfl
+    | succ => apply H; apply Or.inr; rw [Set.mem_liftFv]; exact hi
   | pair a b Ia Ib
     => exact sup_le_sup (Ia (λi hi => H i (Or.inl hi))) (Ib (λi hi => H i (Or.inr hi)))
-  | let2 => sorry
+  | let2 a b Ia Ib =>
+    apply sup_le_sup  (Ia (λi hi => H i (Or.inl hi))) (Ib _)
+    intro i hi
+    cases i using Nat.cases2 with
+    | rest => apply H; apply Or.inr; rw [Set.mem_liftnFv]; exact hi
+    | _ => rfl
   | inl _ I => exact (I H)
   | inr _ I => exact (I H)
-  | case => sorry
+  | case e l r Ie Il Ir =>
+    apply sup_le_sup (sup_le_sup (Ie (λi hi => H i (Or.inl (Or.inl hi)))) (Il _)) (Ir _)
+    intro i hi
+    cases i with
+    | zero => rfl
+    | succ => apply H; apply Or.inl; apply Or.inr; rw [Set.mem_liftFv]; exact hi
+    intro i hi
+    cases i with
+    | zero => rfl
+    | succ => apply H; apply Or.inr; rw [Set.mem_liftFv]; exact hi
   | abort _ I => exact (I H)
   | _ => exact le_refl _
 
@@ -454,13 +473,31 @@ theorem Region.effect_le {Γ Δ : ℕ → ε} (r : Region φ) (H : ∀i ∈ r.fv
   : r.effect Γ ≤ r.effect Δ := by
   induction r generalizing Γ Δ with
   | br _ e => exact e.effect_le H
-  | let1 e r I => exact sup_le_sup (e.effect_le (λi hi => H i (Or.inl hi))) (I sorry)
-  | let2 e r I => exact sup_le_sup (e.effect_le (λi hi => H i (Or.inl hi))) (I sorry)
+  | let1 e r I =>
+    apply sup_le_sup (e.effect_le (λi hi => H i (Or.inl hi))) (I _)
+    intro i hi
+    cases i with
+    | zero => rfl
+    | succ => apply H; apply Or.inr; rw [Set.mem_liftFv]; exact hi
+  | let2 e r I =>
+    apply sup_le_sup (e.effect_le (λi hi => H i (Or.inl hi))) (I _)
+    intro i hi
+    cases i using Nat.cases2 with
+    | rest => apply H; apply Or.inr; rw [Set.mem_liftnFv]; exact hi
+    | _ => rfl
   | case e s t Is It =>
-    exact sup_le_sup
+    apply sup_le_sup
       (sup_le_sup (e.effect_le (λi hi => H i (Or.inl $ Or.inl hi)))
-      (Is sorry))
-      (It sorry)
+      (Is _))
+      (It _)
+    intro i hi
+    cases i with
+    | zero => rfl
+    | succ => apply H; apply Or.inl; apply Or.inr; rw [Set.mem_liftFv]; exact hi
+    intro i hi
+    cases i with
+    | zero => rfl
+    | succ => apply H; apply Or.inr; rw [Set.mem_liftFv]; exact hi
   | cfg β n G Iβ IG =>
     apply sup_le_sup (Iβ (λi hi => H i (Or.inl hi)))
     -- TODO: Fin.sup_le_sup not working here for some reason...
@@ -469,13 +506,25 @@ theorem Region.effect_le {Γ Δ : ℕ → ε} (r : Region φ) (H : ∀i ∈ r.fv
     | succ n I =>
       rw [Fin.sup_succ, Fin.sup_succ]
       apply sup_le_sup
-      apply IG 0 sorry
-      apply I
-      intro k Γ' Δ' H'
-      apply IG k.succ H'
-      intro i hi
-      apply H
-      sorry
+      apply IG 0 _
+      . intro i hi
+        cases i with
+        | zero => rfl
+        | succ =>
+          apply H; apply Or.inr; rw [<-Set.liftFv_iUnion, Set.mem_liftFv]
+          simp only [Set.mem_iUnion]
+          exact ⟨0, hi⟩
+      . apply I
+        intro k Γ' Δ' H'
+        apply IG k.succ H'
+        intro i hi
+        apply H
+        -- TODO: factor out...
+        simp only [fvs, Set.mem_union, Set.mem_iUnion] at hi
+        simp only [fvs, Set.mem_union, Set.mem_iUnion]
+        cases hi with
+        | inl h => exact Or.inl h
+        | inr h => let ⟨i, hi⟩ := h; exact Or.inr ⟨i + 1, by simp [hi]⟩
 
 theorem Region.effect_mono {Γ : ℕ → ε} {r : Region φ} {Δ : ℕ → ε}
   (H : Γ ≤ Δ) : r.effect Γ ≤ r.effect Δ := by

DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean

@@ -3,7 +3,7 @@ import Discretion.Wk.Fin
 import Discretion.Wk.Multiset
 import Discretion.Wk.Multiset
 
-import DeBruijnSSA.BinSyntax.Syntax.Subst
+import DeBruijnSSA.BinSyntax.Syntax.Subst.Term
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean

@@ -33,7 +33,7 @@ open Term
 
 
 -- TODO: fix this to fuse...
-instance instSetoid : Setoid (Region φ) := EqvGen.Setoid (Cong Rewrite)
+instance instSetoid : Setoid (Region φ) := Relation.EqvGen.setoid (Cong Rewrite)
 
 theorem eqv_let1 (e) (p : r ≈ r') : @let1 φ e r ≈ let1 e r'
   := Cong.eqv_let1 e p

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean

@@ -357,44 +357,42 @@ theorem Rewrite.cast_trg {r₀ r₁ r₁' : Region φ} (p : Rewrite r₀ r₁) (
 
 def RewriteD.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : RewriteD (r.vwk ρ) (r'.vwk ρ)
   := by cases d with
-  | let2_pair => sorry
+  | let2_pair a b r =>
+    convert (let2_pair (a.wk ρ) (b.wk ρ) (r.vwk (Nat.liftnWk 2 ρ))) using 1
+    simp [Term.wk0, Term.wk_wk, Nat.liftWk_comp_succ, Nat.liftnWk_two]
   | cfg_cfg β n G n' G' =>
     simp only [Region.vwk, wk, Fin.comp_addCases_apply]
     rw [<-Function.comp.assoc, Region.vwk_comp_lwk, Function.comp.assoc]
     constructor
-  -- | cfg_fuse β n G k σ hσ =>
-  --   simp only [Region.vwk, Region.vwk_lwk, Function.comp_apply]
-  --   constructor
-  --   assumption
-  -- | let1_case =>
-  --   simp only [Region.vwk, wk_liftWk_wk_succ]
-  --   apply cast_trg
-  --   apply let1_case
-  --   simp only [vwk_vwk]
-  --   congr <;>
-  --   funext i <;>
-  --   cases i with
-  --   | zero => rfl
-  --   | succ i => cases i <;> rfl
-  -- | let2_case =>
-  --   simp only [Region.vwk, wk_liftnWk_wk_add, wk_liftWk_wk_succ]
-  --   apply cast_trg
-  --   apply let2_case
-  --   simp only [vwk_vwk]
-  --   congr <;>
-  --   funext i <;>
-  --   cases i with
-  --   | zero => rfl
-  --   | succ i => cases i with
-  --     | zero => rfl
-  --     | succ i => cases i <;> rfl
   | let2_eta e r =>
     simp only [Region.vwk, wk, Nat.liftnWk, Nat.lt_succ_self, ↓reduceIte, Nat.zero_lt_succ,
       Nat.liftWk_comm_liftnWk_apply, vwk_liftnWk₂_vwk1, vwk_liftWk₂_vwk1]
     constructor
-  | let1_let1_case => sorry
-  | let1_let2_case => sorry
-  | let1_case_case => sorry
+  | let1_let1_case a b r s =>
+    convert (let1_let1_case
+      (a.wk ρ) (b.wk (Nat.liftWk ρ)) (r.vwk (Nat.liftnWk 3 ρ)) (s.vwk (Nat.liftnWk 3 ρ)))
+      using 1
+    simp [Nat.liftnWk_succ, Nat.liftnWk_zero]
+    simp only [BinSyntax.Region.vwk, wk, Nat.liftWk_zero, wk0, wk_wk, Nat.liftWk_comp_succ, vswap01,
+      vwk_vwk, let1.injEq, true_and]
+    congr <;> funext k <;> cases k using Nat.cases3 <;> rfl
+  | let1_let2_case a b r s =>
+    convert (let1_let2_case
+      (a.wk ρ) (b.wk (Nat.liftWk ρ)) (r.vwk (Nat.liftnWk 4 ρ)) (s.vwk (Nat.liftnWk 4 ρ)))
+      using 1
+    simp [Nat.liftnWk_succ, Nat.liftnWk_zero]
+    simp only [BinSyntax.Region.vwk, wk, Nat.liftWk_zero, wk0, wk_wk, Nat.liftWk_comp_succ, vswap02,
+      vwk_vwk, let1.injEq, true_and]
+    congr <;> funext k <;> cases k using Nat.cases4 <;> rfl
+  | let1_case_case a d ll lr rl rr =>
+    convert (let1_case_case
+      (a.wk ρ) (d.wk (Nat.liftWk ρ)) (ll.vwk (Nat.liftnWk 3 ρ)) (lr.vwk (Nat.liftnWk 3 ρ))
+      (rl.vwk (Nat.liftnWk 3 ρ)) (rr.vwk (Nat.liftnWk 3 ρ)))
+      using 1
+    simp [Nat.liftnWk_succ, Nat.liftnWk_zero]
+    simp only [BinSyntax.Region.vwk, wk, Nat.liftWk_zero, wk0, wk_wk, Nat.liftWk_comp_succ, vswap01,
+      vwk_vwk, let1.injEq, true_and]
+    congr <;> funext k <;> cases k using Nat.cases3 <;> rfl
   | _ =>
     simp only [
       Region.vwk2, Region.vwk, wk, Nat.liftWk,
@@ -436,39 +434,21 @@ def RewriteD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : Rew
           rw [Nat.add_comm n n', <-Nat.add_assoc]
           rw [Nat.add_comm]
           simp [Nat.le_of_not_lt h]
-  -- | cfg_fuse β n G k σ hσ =>
-  --   have hσk := Fintype.card_le_of_surjective _ hσ
-  --   simp only [Fintype.card_fin] at hσk
-  --   simp only [Region.lwk, Function.comp_apply]
-  --   apply cast ?left ?right
-  --   apply cfg_fuse (β.lwk (Nat.liftnWk n ρ)) _ _ _ σ
-  --   case left =>
-  --     simp only [Region.lwk, Function.comp_apply, cfg.injEq, lwk_lwk]
-  --     constructor
-  --     . congr
-  --       funext j
-  --       simp only [Function.comp_apply, Fin.toNatWk, Nat.liftnWk]
-  --       split
-  --       case isTrue h =>
-  --         have h' : j < k := Nat.lt_of_lt_of_le h hσk
-  --         simp [h']
-  --       case isFalse h =>
-  --         if h : j < k then
-  --           simp [h]
-  --           sorry
-  --         else
-  --           sorry
-  --     . sorry
-  --   case right =>
-  --     sorry
-  --   all_goals sorry
-  | let1_let1_case => sorry
-  | let1_let2_case => sorry
-  | let1_case_case => sorry
+  | let1_let1_case a b r s =>
+    convert (let1_let1_case a b (r.lwk ρ) (s.lwk ρ)) using 1
+    simp [vswap01, vwk_lwk]
+  | let1_let2_case a b r s =>
+    convert (let1_let2_case a b (r.lwk ρ) (s.lwk ρ)) using 1
+    simp [vswap02, vwk_lwk]
+  | let1_case_case a d ll lr rl rr =>
+    convert (let1_case_case a d (ll.lwk ρ) (lr.lwk ρ) (rl.lwk ρ) (rr.lwk ρ)) using 1
+    simp [vswap01, vwk_lwk]
   | _ =>
     simp only [
       Region.vwk2, Region.lwk, wk, Function.comp_apply, lwk_vwk, lwk_vwk1, Function.comp_apply]
     constructor
 
 theorem Rewrite.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Rewrite r r') : Rewrite (r.lwk ρ) (r'.lwk ρ)
   := let ⟨d⟩ := p.nonempty; (d.lwk ρ).rewrite
+
+-- TODO: vsubst, lsubst

DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean

@@ -495,7 +495,24 @@ theorem Wf.lwk1 {Γ : Ctx α ε} {L} {r : Region φ} (d : Wf Γ r (head::L))
   := d.lwk LCtx.Wkn.wk1
 
 theorem Wf.fls {r : Region φ} (h : Wf Γ r L) : r.fls ⊆ Set.Iio L.length
-  := sorry
+  := by induction h with
+  | br hℓ => simp [hℓ.length]
+  | cfg _ _ hR _  _ Iβ IG =>
+    simp only [BinSyntax.Region.fls, Set.union_subset_iff, Set.iUnion_subset_iff]
+    constructor
+    · intro x
+      simp only [Set.mem_liftnFv, Set.mem_Iio]
+      intro hx
+      have hx' := Iβ hx
+      simp only [List.length_append, hR, Set.mem_Iio] at hx'
+      omega
+    · intro i x
+      simp only [Set.mem_liftnFv, Set.mem_Iio]
+      intro hx
+      have hx' := IG i hx
+      simp only [List.length_append, hR, Set.mem_Iio] at hx'
+      omega
+  | _ => simp [*]
 
 def InS.vwk {Γ Δ : Ctx α ε} (ρ : Γ.InS Δ) {L} (r : InS φ Δ L) : InS φ Γ L
   := ⟨(r : Region φ).vwk ρ, r.prop.vwk ρ.prop⟩
@@ -629,8 +646,9 @@ def InS.lwk1 {Γ : Ctx α ε} (r : InS φ Γ (head::L)) : InS φ Γ (head::inser
   := r.lwk LCtx.InS.wk1
 
 theorem InS.lwk_equiv {Γ : Ctx α ε} {ρ ρ' : L.InS K} (r : InS φ Γ L) (h : ρ ≈ ρ')
-  : r.lwk ρ = r.lwk ρ'
-  := sorry
+  : r.lwk ρ = r.lwk ρ' := by
+  ext; apply Region.lwk_eqOn_fls
+  apply Set.EqOn.mono r.prop.fls h
 
 @[simp]
 theorem InS.coe_lwk {Γ : Ctx α ε} {ρ : L.InS K} {r : InS φ Γ L}

DeBruijnSSA/BinSyntax/Typing/Region/Structural.lean

@@ -173,7 +173,7 @@ theorem Subst.InS.coe_unpack {Γ : Ctx α ε} {R : LCtx α}
   rfl
 
 @[simp]
-theorem Subst.InS.vlift_unpack {Γ : Ctx α ε} {R : LCtx α} {ρ : Γ.InS Δ}
+theorem Subst.InS.vlift_unpack {Γ : Ctx α ε} {R : LCtx α}
   : (Subst.InS.unpack (φ := φ) (Γ := Γ) (R := R)).vlift (head := head) = unpack := by
   ext; simp [Subst.vlift]
 

lake-manifest.json

@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d",
+   "rev": "8ab24d4bb8b4c4a52af3f39027f255b1901669c9",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "df80b0dd2548c76fbdc3fe5d3a96873dfd46c0dc",
+   "rev": "3e18f1777d9adc6889ce44a51a451bbd54e691aa",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5e4ff7246e2e63e5053c64b9a7464a0bd97659fb",
+   "rev": "7cc792161e8a2752c79b224d1c7627b70d8105e7",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",