Region foundations

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -551,7 +551,16 @@ theorem Eqv.ucfg'_quot
 
 theorem Eqv.cfg_eq_ucfg'
   {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
-  : cfg R β G = ucfg' R β G := sorry
+  : cfg R β G = ucfg' R β G := by
+  induction β using Quotient.inductionOn
+  induction G using Eqv.choiceInduction
+  rw [cfg_quot, ucfg'_quot]
+  apply Quotient.sound
+  apply Uniform.rel
+  apply TStep.reduce
+  apply InS.coe_wf
+  apply InS.coe_wf
+  apply Reduce.ucfg'
 
 theorem Eqv.cfg_br_ge {Γ : Ctx α ε} {L : LCtx α}
   {ℓ} {a : Term.Eqv φ Γ ⟨A, ⊥⟩}
@@ -626,12 +635,20 @@ theorem Eqv.cfgSubst_get_ge  {Γ : Ctx α ε} {L : LCtx α}
 def Subst.Eqv.fromFCFG {Γ : Ctx α ε} {L K : LCtx α}
   (G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) K)
   : Subst.Eqv φ Γ L K
-  := Quotient.liftOn (Quotient.finChoice G) (λG => ⟦Region.CFG.toSubst G⟧) sorry
+  := Quotient.liftOn (Quotient.finChoice G) (λG => ⟦Region.CFG.toSubst G⟧)
+      (λ_ _ h => Quotient.sound <| λi => by simp [h i])
 
 def Subst.Eqv.fromFCFG_append {Γ : Ctx α ε} {L K R : LCtx α}
   (G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) (K ++ R))
   : Subst.Eqv φ Γ (L ++ R) (K ++ R)
-  := Quotient.liftOn (Quotient.finChoice G) (λG => ⟦Region.CFG.toSubst_append G⟧) sorry
+  := Quotient.liftOn (Quotient.finChoice G) (λG => ⟦Region.CFG.toSubst_append G⟧)
+      (λ_ _ h => Quotient.sound <| λi => by
+        simp only [CFG.get_toSubst_append]
+        split
+        · apply InS.cast_congr
+          apply h
+        · rfl
+        )
 
 -- theorem Eqv.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
 --   {σ : Subst.Eqv φ Γ R (R' ++ L)} {β : Eqv φ Γ (R ++ L)}
@@ -679,7 +696,8 @@ theorem Subst.Eqv.initial_eq {Γ : Ctx α ε} {L : LCtx α} {σ σ' : Subst.Eqv
   exact i.elim0
 
 def Eqv.csubst {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ ((A, ⊥)::Γ) L) : Subst.Eqv φ Γ [A] L
-  := Quotient.liftOn r (λr => ⟦r.csubst⟧) sorry
+  := Quotient.liftOn r (λr => ⟦r.csubst⟧)
+    (λ_ _ h => Quotient.sound <| λi => by cases i using Fin.elim1; exact h)
 
 @[simp]
 theorem Eqv.csubst_quot {Γ : Ctx α ε} {L : LCtx α} {r : InS φ ((A, ⊥)::Γ) L}

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -17,6 +17,11 @@ theorem InS.eqv_def {Γ : Ctx α ε} {L : LCtx α} {r r' : InS φ Γ L}
   : r ≈ r' ↔ Uniform (φ := φ) TStep Γ L r r'
   := by rfl
 
+theorem InS.cast_congr {Γ Γ' : Ctx α ε} {L L' : LCtx α}
+  {r r' : InS φ Γ L} {hΓ : Γ = Γ'} {hL : L = L'}
+  (h : r ≈ r') : r.cast hΓ hL ≈ r'.cast hΓ hL
+  := by cases hΓ; cases hL; exact h
+
 theorem InS.let1_body_congr {Γ : Ctx α ε} {L : LCtx α}
   {r r' : InS φ _ L} (a : Term.InS φ Γ ⟨A, e⟩)
     : r ≈ r' → InS.let1 a r ≈ InS.let1 a r' := Uniform.let1 a.prop

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

@@ -110,57 +110,6 @@ def ReduceD.cast_src {r₀ r₀' r₁ : Region φ} (h : r₀' = r₀) (p : Reduc
 def ReduceD.cast {r₀ r₀' r₁ r₁' : Region φ} (h₀ : r₀ = r₀') (h₁ : r₁ = r₁')
   (p : ReduceD r₀ r₁) : ReduceD r₀' r₁' := h₁ ▸ h₀ ▸ p
 
-def ReduceD.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : ReduceD r r') : ReduceD (r.vwk ρ) (r'.vwk ρ)
-  := by cases d with
-  | dead_cfg_left β n G m G' =>
-    simp only [Region.vwk, wk, Function.comp_apply, vwk_lwk, Fin.comp_addCases_apply]
-    rw [<-Function.comp.assoc, vwk_comp_lwk, Function.comp.assoc]
-    apply dead_cfg_left
-  | ucfg' β n G =>
-    convert ucfg' (β.vwk ρ) n (λi => (G i).vwk (Nat.liftWk ρ))
-    simp only [Region.ucfg', vwk_lsubst]
-    congr
-    funext i
-    simp only [Function.comp_apply, cfgSubst']
-    split
-    · simp only [BinSyntax.Region.vwk, wk, Nat.liftWk_zero, cfg.injEq, heq_eq_eq, true_and]
-      funext i
-      simp only [vwk1, vwk_vwk]
-      congr
-      funext i
-      cases i <;> rfl
-    · rfl
-  | _ =>
-    simp only [Region.vwk, wk, Function.comp_apply, vwk_lwk]
-    constructor
-
-theorem Reduce.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Reduce (r.vwk ρ) (r'.vwk ρ)
-  := let ⟨d⟩ := p.nonempty; (d.vwk ρ).reduce
-
-def ReduceD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : ReduceD r r') : ReduceD (r.lwk ρ) (r'.lwk ρ)
-  := by cases d with
-  | dead_cfg_left β n G m G' =>
-    apply cast_src _
-    apply dead_cfg_left
-      (β := β.lwk (Nat.liftnWk m ρ))
-      (n := n) (G := (Region.lwk (Nat.liftnWk (n + m) ρ)) ∘ G)
-      (m := m) (G' := (Region.lwk (Nat.liftnWk m ρ)) ∘ G')
-    simp only [
-      Region.lwk, lwk_lwk, Region.lwk_addCases, <-Function.comp.assoc, Region.comp_lwk,
-      Nat.liftnWk_comp_add_right
-    ]
-  | wk_cfg β n G k σ =>
-    simp only [Region.lwk, Region.lwk_lwk, Function.comp_apply, Fin.liftnWk_comp_toNatWk]
-    simp only [<-Region.lwk_lwk]
-    apply wk_cfg
-  | ucfg' β n G => sorry
-  | _ =>
-    simp only [Region.lwk, wk, Function.comp_apply, lwk_vwk]
-    constructor
-
-theorem Reduce.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Reduce (r.lwk ρ) (r'.lwk ρ)
-  := let ⟨d⟩ := p.nonempty; (d.lwk ρ).reduce
-
 def ReduceD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (d : ReduceD r r')
   : ReduceD (r.vsubst σ) (r'.vsubst σ) := by cases d with
   | case_inl e r s => exact case_inl (e.subst σ) (r.vsubst σ.lift) (s.vsubst σ.lift)
@@ -276,8 +225,15 @@ def ReduceD.lsubst {r r' : Region φ} (σ : Subst φ) (d : ReduceD r r')
         split
         rfl
         simp only [vsubst_fromWk, lwk_vwk, vwk_vwk]
-        sorry
-      · sorry
+        apply congrFun
+        simp only [<-vsubst_fromWk]
+        apply congrArg
+        funext k
+        cases k <;> rfl
+      · simp only [<-vsubst_fromWk, vsubst_vsubst]
+        congr
+        funext k
+        cases k <;> rfl
     · simp only [BinSyntax.Region.lsubst, Subst.vlift, Function.comp_apply, vsubst0_var0_vwk1, ←
       lsubst_fromLwk, lsubst_lsubst]
       apply Eq.symm
@@ -289,6 +245,22 @@ theorem Reduce.lsubst
   {r r' : Region φ} (σ : Subst φ) (p : Reduce r r') : Reduce (r.lsubst σ) (r'.lsubst σ)
   := let ⟨d⟩ := p.nonempty; (d.lsubst σ).reduce
 
+def ReduceD.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : ReduceD r r') : ReduceD (r.vwk ρ) (r'.vwk ρ)
+  := by
+  simp only [<-Region.vsubst_fromWk]
+  exact ReduceD.vsubst _ d
+
+theorem Reduce.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Reduce (r.vwk ρ) (r'.vwk ρ)
+  := let ⟨d⟩ := p.nonempty; (d.vwk ρ).reduce
+
+def ReduceD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : ReduceD r r') : ReduceD (r.lwk ρ) (r'.lwk ρ)
+  := by
+  simp only [<-Region.lsubst_fromLwk]
+  exact ReduceD.lsubst _ d
+
+theorem Reduce.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Reduce (r.lwk ρ) (r'.lwk ρ)
+  := let ⟨d⟩ := p.nonempty; (d.lwk ρ).reduce
+
 -- theorem ReduceD.effect_le {Γ : ℕ → ε} {r r' : Region φ} (p : ReduceD r r')
 --   : r'.effect Γ ≤ r.effect Γ := by
 --   cases p with

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

@@ -355,102 +355,6 @@ theorem Rewrite.cast_trg {r₀ r₁ r₁' : Region φ} (p : Rewrite r₀ r₁) (
 --   | let1_case_case => sorry
 --   | _ => simp [vwk2, fvs_vwk, fvs_vwk1, Term.fvs_wk, Set.liftnFv_iUnion, Set.union_assoc]
 
-def RewriteD.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : RewriteD (r.vwk ρ) (r'.vwk ρ)
-  := by cases d with
-  | 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
-  | 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 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,
-      vwk_liftWk₂_vwk1, wk_liftWk_wk_succ, vwk_liftnWk₂_liftWk_vwk2, vwk_liftnWk₂_vwk1,
-      wk_liftnWk_wk_add, Nat.liftWk_comm_liftnWk_apply, Function.comp_apply, Term.wk0]
-    constructor
-
-theorem Rewrite.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Rewrite r r') : Rewrite (r.vwk ρ) (r'.vwk ρ)
-  := let ⟨d⟩ := p.nonempty; (d.vwk ρ).rewrite
-
-def RewriteD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : RewriteD (r.lwk ρ) (r'.lwk ρ)
-  := by cases d with
-  | cfg_br_lt ℓ e n G hℓ =>
-    simp only [Region.lwk, Nat.liftnWk, hℓ, ↓reduceIte]
-    apply cfg_br_lt
-  | cfg_cfg β n G n' G' =>
-    simp only [Region.lwk]
-    apply cast_trg
-    apply cfg_cfg
-    congr
-    · rw [Nat.liftnWk_add]; rfl
-    · funext i
-      simp only [Fin.comp_addCases_apply]
-      simp only [Fin.addCases]
-      split
-      · simp [Nat.liftnWk_add, *]
-      · simp only [Function.comp_apply, eq_rec_constant, Region.lwk_lwk]
-        congr
-        funext k
-        simp only [Function.comp_apply, Nat.liftnWk]
-        split
-        case isTrue h =>
-          rw [ite_cond_eq_true]
-          simp_arith [Nat.succ_le_of_lt h]
-        case isFalse h =>
-          rw [ite_cond_eq_false]
-          rw [Nat.sub_add_eq]
-          simp only [add_tsub_cancel_right]
-          rw [Nat.add_comm n n', <-Nat.add_assoc]
-          rw [Nat.add_comm]
-          simp [Nat.le_of_not_lt h]
-  | 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
-
 def RewriteD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (p : RewriteD r r')
   : RewriteD (r.vsubst σ) (r'.vsubst σ) := by cases p with
   | let1_op f a r =>
@@ -686,6 +590,22 @@ theorem Rewrite.lsubst {r r' : Region φ} (σ : Subst φ) (p : Rewrite r r')
   : Rewrite (r.lsubst σ) (r'.lsubst σ)
   := let ⟨d⟩ := p.nonempty; (d.lsubst σ).rewrite
 
+def RewriteD.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : RewriteD (r.vwk ρ) (r'.vwk ρ)
+  := by
+  simp only [<-Region.vsubst_fromWk]
+  exact RewriteD.vsubst _ d
+
+theorem Rewrite.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Rewrite r r') : Rewrite (r.vwk ρ) (r'.vwk ρ)
+  := let ⟨d⟩ := p.nonempty; (d.vwk ρ).rewrite
+
+def RewriteD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : RewriteD (r.lwk ρ) (r'.lwk ρ)
+  := by
+  simp only [<-Region.lsubst_fromLwk]
+  exact RewriteD.lsubst _ d
+
+theorem Rewrite.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Rewrite r r') : Rewrite (r.lwk ρ) (r'.lwk ρ)
+  := let ⟨d⟩ := p.nonempty; (d.lwk ρ).rewrite
+
 end Region
 
 end BinSyntax

DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean

@@ -94,6 +94,17 @@ def Region.CFG.toSubst {Γ : Ctx α ε} {L K : LCtx α} (cfg : Region.CFG φ Γ
     Region.Subst.fromFCFG K.length (cfg : Fin L.length → Region φ),
     λi => by simp⟩
 
+@[simp]
+theorem Region.CFG.coe_toSubst {Γ : Ctx α ε} {L K : LCtx α} {cfg : Region.CFG φ Γ L K}
+  : (cfg.toSubst : Region.Subst φ) = Region.Subst.fromFCFG K.length (cfg : Fin L.length → Region φ)
+  := rfl
+
+@[simp]
+theorem Region.CFG.get_toSubst {Γ : Ctx α ε} {L K : LCtx α}
+  (cfg : Region.CFG φ Γ L K) (i : Fin L.length)
+  : cfg.toSubst.get i = cfg i
+  := by ext; simp
+
 theorem Region.Subst.Wf.fromFCFG {Γ : Ctx α ε} {L K : LCtx α}
   {G : Fin L.length → Region φ} (hG : ∀i : Fin L.length, (G i).Wf (⟨L.get i, ⊥⟩::Γ) K)
   : Wf Γ L K (Region.Subst.fromFCFG K.length G)
@@ -184,6 +195,28 @@ def Region.CFG.toSubst_append {Γ : Ctx α ε} {L K : LCtx α} (cfg : Region.CFG
     Region.Subst.fromFCFG K.length (cfg : Fin L.length → Region φ),
     Region.Subst.Wf.fromFCFG_append (λi => (cfg i).prop)⟩
 
+@[simp]
+theorem Region.CFG.coe_toSubst_append {Γ : Ctx α ε} {L K : LCtx α} {cfg : Region.CFG φ Γ L (K ++ R)}
+  : (cfg.toSubst_append : Region.Subst φ)
+  = Region.Subst.fromFCFG K.length (cfg : Fin L.length → Region φ)
+  := rfl
+
+@[simp]
+theorem Region.CFG.get_toSubst_append {Γ : Ctx α ε} {L K : LCtx α}
+  (cfg : Region.CFG φ Γ L (K ++ R)) (i : Fin (L ++ R).length)
+  : cfg.toSubst_append.get i =
+  if h : i < L.length then (cfg ⟨i, h⟩).cast
+    (by simp only [List.get_eq_getElem]; rw [List.getElem_append_left]) rfl
+  else Region.InS.br ((i - L.length) + K.length) (Term.InS.var 0 Ctx.Var.shead) ⟨
+    by have h := i.prop; simp only [List.length_append] at *; omega,
+    by
+      have h := i.prop;
+      simp only [List.length_append] at h
+      rw [List.get_eq_getElem, List.getElem_append_right, List.getElem_append_right]
+      simp
+      all_goals omega⟩
+  := by ext; simp only [Subst.InS.coe_get, coe_toSubst_append, Subst.fromFCFG]; split <;> rfl
+
 theorem Region.Subst.Wf.extend_out (hσ : σ.Wf Γ L K) : σ.Wf Γ L (K ++ R) := λi => (hσ i).extend
 
 theorem Region.Subst.Wf.extend (hσ : σ.Wf Γ L K)
@@ -226,12 +259,6 @@ theorem Region.CFG.ext (G G' : Region.CFG φ Γ L K)
 theorem Region.Subst.InS.extend_in_extend_out {R} (σ : Region.Subst.InS φ Γ L K)
   : σ.extend_out.extend_in = σ.extend (R := R) := by ext; rfl
 
-@[simp]
-theorem Region.CFG.coe_toSubst {Γ : Ctx α ε} {L K : LCtx α}
-  {cfg : Region.CFG φ Γ L K}
-  : (cfg.toSubst : Region.Subst φ) = Region.Subst.fromFCFG K.length (cfg : Fin L.length → Region φ)
-  := rfl
-
 theorem Region.Subst.toSubst_cfg {Γ : Ctx α ε} {L K : LCtx α} {σ : Region.Subst.InS φ Γ L K}
   : σ.cfg.toSubst = σ.clip
   := rfl