Inverse weakening

DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean

@@ -109,8 +109,8 @@ def Region.RewriteD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
   | cfg_let2 a β n G, _ => sorry
   | cfg_case e r s n G, _ => sorry
   | cfg_cfg β n G n' G', _ => sorry
-  | cfg_zero β G, _ => sorry
-  | cfg_fuse β n G k ρ hρ, _ => sorry
+  | cfg_zero β G, WfD.cfg _ [] rfl dβ dG => dβ
+  | cfg_fuse β n G k ρ hρ, WfD.cfg _ R hR dβ dG => sorry
   | let2_eta r, _ => sorry
 
 def Region.RewriteD.wfD_inv {Γ : Ctx α ε} {r r' : Region φ} {L}
@@ -132,22 +132,57 @@ def Region.RewriteD.wfD_inv {Γ : Ctx α ε} {r r' : Region φ} {L}
   | cfg_let2 a β n G, _ => sorry
   | cfg_case e r s n G, _ => sorry
   | cfg_cfg β n G n' G', _ => sorry
-  | cfg_zero β G, _ => sorry
-  | cfg_fuse β n G k ρ hρ, _ => sorry
+  | cfg_zero β G, dβ => WfD.cfg 0 [] rfl dβ (λi => i.elim0)
+  | cfg_fuse β n G k ρ hρ, WfD.cfg _ R hR dβ dG => sorry
   | let2_eta r, _ => sorry
 
 def Region.ReduceD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
-  : ReduceD Γ.effect r r' → r.WfD Γ L → r'.WfD Γ L
-  | let1_beta e r he, _ => sorry
-  | case_inl e r s, _ => sorry
-  | case_inr e r s, _ => sorry
-  | wk_cfg β n G k ρ, _ => sorry
-  | dead_cfg_left β n G m G', _ => sorry
+  : ReduceD r r' → r.WfD Γ L → r'.WfD Γ L
+  | case_inl e r s, WfD.case (Term.WfD.inl de) dr ds => dr.let1 de
+  | case_inr e r s, WfD.case (Term.WfD.inr de) dr ds => ds.let1 de
+  | wk_cfg β n G k ρ, WfD.cfg _ R hR dβ dG =>
+    sorry
+  | dead_cfg_left β n G m G', WfD.cfg _ R hR dβ dG =>
+    sorry
 
 def Region.StepD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
   : StepD Γ.effect r r' → r.WfD Γ L → r'.WfD Γ L
+  | let1_beta e r he
+    => λ | _ => sorry
   | reduce p => p.wfD
   | rw p => p.wfD
-  | rw_symm p => p.wfD_inv
+  | rw_op p => p.wfD_inv
+
+def Region.BCongD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
+  : BCongD StepD Γ.effect r r' → r.WfD Γ L → r'.WfD Γ L
+  | step s, d => s.wfD d
+  | let1 e p, WfD.let1 de dr => ((Γ.effect_append_bot ▸ p).wfD dr).let1 de
+  | let2 e p, WfD.let2 de dr => ((Γ.effect_append_bot₂ ▸ p).wfD dr).let2 de
+  | case_left e p s, WfD.case de dr ds => ((Γ.effect_append_bot ▸ p).wfD dr).case de ds
+  | case_right e r p, WfD.case de dr ds => dr.case de ((Γ.effect_append_bot ▸ p).wfD ds)
+  | cfg_entry p n G, WfD.cfg _ R hR dβ dG => (p.wfD dβ).cfg _ R hR dG
+  | cfg_block β n G i p, WfD.cfg _ R hR dβ dG => dβ.cfg _ R hR (λk => by
+    if h : i = k then
+      cases h
+      simp only [Function.update_same]
+      exact wfD (Γ.effect_append_bot ▸ p) (dG i)
+    else
+      rw [Function.update_noteq (Ne.symm h)]
+      exact dG k)
+
+-- TODO: fix this...
+set_option linter.unusedVariables false in
+def Region.RWD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
+  : RWD StepD Γ.effect r r' → r.WfD Γ L → r'.WfD Γ L
+  | RWD.refl _, d => d
+  | RWD.cons p s, d => s.wfD (p.wfD d)
+
+inductive Region.TStepD : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) → Type _
+  -- TODO: do we need to require r.WfD for rw?
+  | step {Γ L r r'} : r.WfD Γ L → StepD Γ.effect r r' → Region.TStepD Γ L r r'
+  | step_op {Γ L r r'} : r.WfD Γ L → StepD Γ.effect r r' → Region.TStepD Γ L r r'
+  | initial {Γ L} : Γ.IsInitial → r.WfD Γ L → r'.WfD Γ L → Region.TStepD Γ L r r'
+  | terminal {Γ L} : e.WfD Γ ⟨Ty.unit, ⊥⟩ → e'.WfD Γ ⟨Ty.unit, ⊥⟩ → r.WfD (⟨Ty.unit, ⊥⟩::Γ) L
+    → Region.TStepD Γ L (Region.let1 e r) (Region.let1 e' r)
 
 end BinSyntax

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -260,14 +260,13 @@ def RewriteD.lsubst_alpha {r₀ r₀'}
     cases k <;> rfl
   -- | let1_eta r => sorry
 
-def ReduceD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}
-  (p : ReduceD Γ r₀ r₀') (k) (r₁ : Region φ)
-  : ReduceD Γ (r₀.lsubst (alpha k r₁)) (r₀'.lsubst (alpha k r₁)) :=
+def ReduceD.lsubst_alpha {r₀ r₀'}
+  (p : ReduceD r₀ r₀') (k) (r₁ : Region φ)
+  : ReduceD (r₀.lsubst (alpha k r₁)) (r₀'.lsubst (alpha k r₁)) :=
   match p with
-  | let1_beta e r he => cast_trg (let1_beta e _ he) (by rw [vsubst_subst0_lsubst_vlift])
-  | case_inl e r s => case_inl e _ _
-  | case_inr e r s => case_inr e _ _
-  | wk_cfg β n G k ρ => by
+  | case_inl e r _ => case_inl e _ _
+  | case_inr e r _ => case_inr e _ _
+  | wk_cfg β n G k _ => by
     rw [
       lsubst_cfg, lsubst_cfg,
       lsubst_liftn_lwk_toNatWk,
@@ -280,7 +279,7 @@ def ReduceD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}
     apply wk_cfg
     rw [Subst.vlift_liftn_comm]
     rfl
-  | dead_cfg_left β n G m G' =>
+  | dead_cfg_left β n G m _ =>
     cast_src (by
       simp only [lsubst_cfg, Fin.comp_addCases, liftn_alpha, vlift_alpha, lsubst_lwk, lwk_lsubst]
       congr
@@ -309,9 +308,10 @@ def StepD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀' : Region φ}
   (p : StepD Γ r₀ r₀') (k) (r₁ : Region φ)
   : StepD Γ (r₀.lsubst (alpha k r₁)) (r₀'.lsubst (alpha k r₁)) :=
   match p with
+  | let1_beta e _ he => cast_trg (let1_beta e _ he) (by rw [vsubst_subst0_lsubst_vlift])
   | reduce p => reduce (p.lsubst_alpha k r₁)
   | rw p => rw (p.lsubst_alpha k r₁)
-  | rw_symm p => rw_symm (p.lsubst_alpha k r₁)
+  | rw_op p => rw_op (p.lsubst_alpha k r₁)
 
 -- TODO: factor out as more general lifting lemma
 def BCongD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}
@@ -339,8 +339,10 @@ def BCongD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}
     apply RWD.cfg_entry
     apply lsubst_alpha p _ _
   | BCongD.cfg_block β n G i p => by
+    have h : β.cfg n G = β.cfg n (Function.update G i (G i)) := by simp
+    rw [h]
     simp only [lsubst_alpha_cfg, Function.comp_update]
-    apply RWD.cfg_block
+    apply RWD.cfg_block'
     apply lsubst_alpha p _ _
 
 -- TODO: factor out as more general lifting lemma

DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean

@@ -22,6 +22,7 @@ def Term.fv : Term φ → Multiset ℕ
   | pair x y => x.fv + y.fv
   | inl a => a.fv
   | inr a => a.fv
+  | abort a => a.fv
   | _ => 0
 
 theorem Term.fv_wk (ρ : ℕ → ℕ) (t : Term φ) : (t.wk ρ).fv = t.fv.map ρ := by
@@ -35,8 +36,28 @@ def Term.fvi : Term φ → ℕ
   | pair x y => Nat.max x.fvi y.fvi
   | inl a => a.fvi
   | inr a => a.fvi
+  | abort a => a.fvi
   | _ => 0
 
+theorem Term.fvi_var_le_iff {x n : ℕ} : (@var φ x).fvi ≤ n ↔ x < n := by simp [Nat.succ_le_iff]
+
+theorem Term.fvi_op_le_iff {o : φ} {t : Term φ} {n} : (op o t).fvi ≤ n ↔ t.fvi ≤ n := Iff.rfl
+
+theorem Term.fvi_pair_le_iff {l r : Term φ} {n} : (pair l r).fvi ≤ n ↔ l.fvi ≤ n ∧ r.fvi ≤ n
+  := by simp
+
+theorem Term.fvi_pair_le_left {l r : Term φ} {n} : (pair l r).fvi ≤ n → l.fvi ≤ n
+  := by simp only [fvi, max_le_iff, and_imp]; exact λl _ => l
+
+theorem Term.fvi_pair_le_right {l r : Term φ} {n} : (pair l r).fvi ≤ n → r.fvi ≤ n
+  := by simp only [fvi, max_le_iff, and_imp]; exact λ_ r => r
+
+theorem Term.fvi_inl_le_iff {t : Term φ} {n : ℕ} : t.inl.fvi ≤ n ↔ t.fvi ≤ n := Iff.rfl
+
+theorem Term.fvi_inr_le_iff {t : Term φ} {n : ℕ} : t.inr.fvi ≤ n ↔ t.fvi ≤ n := Iff.rfl
+
+theorem Term.fvi_abort_le_iff {t : Term φ} {n : ℕ} : t.abort.fvi ≤ n ↔ t.fvi ≤ n := Iff.rfl
+
 theorem Term.fvi_zero_iff_fv_zero (t : Term φ) : t.fvi = 0 ↔ t.fv = 0 := by
   induction t <;> simp [*]
 
@@ -48,6 +69,7 @@ def Term.fvc (x : ℕ) : Term φ → ℕ
   | pair y z => y.fvc x + z.fvc x
   | inl y => y.fvc x
   | inr y => y.fvc x
+  | abort y => y.fvc x
   | _ => 0
 
 theorem Term.fvc_eq_fv_count (x : ℕ) (t : Term φ) : t.fvc x = t.fv.count x := by
@@ -286,6 +308,60 @@ def Region.fvi : Region φ → ℕ
   | let2 e t => Nat.max e.fvi (t.fvi - 2)
   | cfg β _ f => Nat.max β.fvi (Finset.sup Finset.univ (λi => (f i).fvi - 1))
 
+theorem Region.fvi_br_le_iff {n : ℕ} {e : Term φ} : (br n e).fvi ≤ n ↔ e.fvi ≤ n := Iff.rfl
+
+theorem Region.fvi_case_le_iff {e} {s t : Region φ} {n : ℕ}
+  : (case e s t).fvi ≤ n ↔ e.fvi ≤ n ∧ s.fvi ≤ n + 1 ∧ t.fvi ≤ n + 1
+  := by simp
+
+theorem Region.fvi_case_le_disc {e} {s t : Region φ} {n : ℕ}
+  : (case e s t).fvi ≤ n → e.fvi ≤ n
+  := by rw [fvi_case_le_iff]; exact λ⟨he, _, _⟩ => he
+
+theorem Region.fvi_case_le_left {e} {s t : Region φ} {n : ℕ}
+  : (case e s t).fvi ≤ n → s.fvi ≤ n + 1
+  := by rw [fvi_case_le_iff]; exact λ⟨_, hs, _⟩ => hs
+
+theorem Region.fvi_case_le_right {e} {s t : Region φ} {n : ℕ}
+  : (case e s t).fvi ≤ n → t.fvi ≤ n + 1
+  := by rw [fvi_case_le_iff]; exact λ⟨_, _, ht⟩ => ht
+
+theorem Region.fvi_let1_le_iff {e : Term φ} {t} {n : ℕ}
+  : (let1 e t).fvi ≤ n ↔ e.fvi ≤ n ∧ t.fvi ≤ n + 1
+  := by simp
+
+theorem Region.fvi_let1_le_bind {e : Term φ} {t} {n : ℕ}
+  : (let1 e t).fvi ≤ n → e.fvi ≤ n
+  := by rw [fvi_let1_le_iff]; exact λ⟨he, _⟩ => he
+
+theorem Region.fvi_let1_le_rest {e : Term φ} {t} {n : ℕ}
+  : (let1 e t).fvi ≤ n → t.fvi ≤ n + 1
+  := by rw [fvi_let1_le_iff]; exact λ⟨_, ht⟩ => ht
+
+theorem Region.fvi_let2_le_iff {e : Term φ} {t} {n : ℕ}
+  : (let2 e t).fvi ≤ n ↔ e.fvi ≤ n ∧ t.fvi ≤ n + 2
+  := by simp
+
+theorem Region.fvi_let2_le_bind {e : Term φ} {t} {n : ℕ}
+  : (let2 e t).fvi ≤ n → e.fvi ≤ n
+  := by rw [fvi_let2_le_iff]; exact λ⟨he, _⟩ => he
+
+theorem Region.fvi_let2_le_rest {e : Term φ} {t} {n : ℕ}
+  : (let2 e t).fvi ≤ n → t.fvi ≤ n + 2
+  := by rw [fvi_let2_le_iff]; exact λ⟨_, ht⟩ => ht
+
+theorem Region.fvi_cfg_le_iff {β : Region φ} {k : ℕ} {f : Fin k → Region φ}
+  : (cfg β k f).fvi ≤ n ↔ β.fvi ≤ n ∧ ∀i, (f i).fvi ≤ n + 1
+  := by simp
+
+theorem Region.fvi_cfg_le_entry {β : Region φ} {n : ℕ} {f : Fin k → Region φ}
+  : (cfg β k f).fvi ≤ n → β.fvi ≤ n
+  := by rw [fvi_cfg_le_iff]; exact λ⟨hβ, _⟩ => hβ
+
+theorem Region.fvi_cfg_le_blocks {β : Region φ} {n : ℕ} {f : Fin k → Region φ}
+  : (cfg β k f).fvi ≤ n → ∀i, (f i).fvi ≤ n + 1
+  := by rw [fvi_cfg_le_iff]; exact λ⟨_, hf⟩ i => hf i
+
 /-- Get the count of how often a free variable occurs in this region -/
 @[simp]
 def Region.fvc (x : ℕ) : Region φ → ℕ