Began ucfg work

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -1171,10 +1171,10 @@ theorem Eqv.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
 
 -- TODO: factor out to discretion as general helper...
 
-theorem Eqv.choiceInduction {ι : Type _} {Γs : ι → Ctx α ε} {L : LCtx α}
-  (motive : ((i : ι) → Eqv φ (Γs i) L) → Prop)
-  (choice : ∀G : (i : ι) → InS φ (Γs i) L, motive (λi => ⟦G i⟧))
-  : ∀G : (i : ι) → Eqv φ (Γs i) L, motive G
+theorem Eqv.choiceInduction {ι : Type _} {Γs : ι → Ctx α ε} {Ls : ι → LCtx α}
+  (motive : ((i : ι) → Eqv φ (Γs i) (Ls i)) → Prop)
+  (choice : ∀G : (i : ι) → InS φ (Γs i) (Ls i), motive (λi => ⟦G i⟧))
+  : ∀G : (i : ι) → Eqv φ (Γs i) (Ls i), motive G
   := λG => by
   generalize hG : Quotient.choice G = G'
   induction G' using Quotient.inductionOn with

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -82,7 +82,14 @@ theorem Subst.InS.extend_congr {Γ : Ctx α ε} {L K R : LCtx α}
     simp only [List.get_eq_getElem, get, Set.mem_setOf_eq, extend, Subst.extend]
     split
     case isTrue h' =>
-      sorry
+      have h := InS.lwk_congr_right (ρ := ⟨_, LCtx.Wkn.id_right_append (added := R)⟩) (h ⟨i, h'⟩)
+      convert h using 2
+      rw [List.getElem_append_left]
+      rfl
+      rw [List.getElem_append_left]
+      rfl
+      exact InS.hext (by rw [List.getElem_append_left]; rfl) rfl (by simp)
+      exact InS.hext (by rw [List.getElem_append_left]; rfl) rfl (by simp)
     case _ => rfl
 
 theorem Subst.InS.extend_in_congr {Γ : Ctx α ε} {L K R : LCtx α}
@@ -91,7 +98,13 @@ theorem Subst.InS.extend_in_congr {Γ : Ctx α ε} {L K R : LCtx α}
     simp only [List.get_eq_getElem, get, Set.mem_setOf_eq, extend_in, Subst.extend]
     split
     case isTrue h' =>
-      sorry
+      convert h ⟨i, h'⟩ using 2
+      rw [List.getElem_append_left]
+      rfl
+      rw [List.getElem_append_left]
+      rfl
+      exact InS.hext (by rw [List.getElem_append_left]; rfl) rfl (by simp)
+      exact InS.hext (by rw [List.getElem_append_left]; rfl) rfl (by simp)
     case _ => rfl
 
 open Subst.InS
@@ -381,9 +394,15 @@ theorem Eqv.lsubst_cfg {Γ : Ctx α ε} {L : LCtx α}
       Subst.Eqv.liftn_append_quot, Subst.Eqv.vlift_quot, Quotient.finChoice_eq, Eqv.cfg_inner_quot]
     rfl
 
+theorem Subst.InS.vsubst_congr {Γ Δ : Ctx α ε} {L K : LCtx α}
+  {ρ ρ' : Term.Subst.InS φ Γ Δ} {σ σ' : Subst.InS φ Δ L K}
+  (hρ : ρ ≈ ρ') (hσ : σ ≈ σ') : σ.vsubst ρ ≈ σ'.vsubst ρ'
+  := λi => Region.InS.vsubst_congr (Term.Subst.InS.slift_congr hρ) (hσ i)
+
 def Subst.Eqv.vsubst {Γ Δ : Ctx α ε} {L K : LCtx α}
   (ρ : Term.Subst.Eqv φ Γ Δ) (σ : Subst.Eqv φ Δ L K) : Subst.Eqv φ Γ L K
-  := Quotient.liftOn₂ ρ σ (λρ σ => ⟦σ.vsubst ρ⟧) sorry
+  := Quotient.liftOn₂ ρ σ (λρ σ => ⟦σ.vsubst ρ⟧)
+    (λ_ _ _ _ hρ hσ => Quotient.sound <| Subst.InS.vsubst_congr hρ hσ)
 
 @[simp]
 theorem Subst.Eqv.vsubst_quot {Γ Δ : Ctx α ε} {L K : LCtx α}
@@ -400,40 +419,73 @@ theorem Eqv.vsubst_lsubst {Γ Δ : Ctx α ε}
   induction r using Quotient.inductionOn
   simp [InS.vsubst_lsubst]
 
+theorem InS.cfgSubstCongr {Γ : Ctx α ε} {L : LCtx α}
+  {R : LCtx α} {G G' : ∀i, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} (hG : G ≈ G')
+  : cfgSubst R G ≈ cfgSubst R G' := λi => by
+  simp only [List.get_eq_getElem, get_cfgSubst]
+  apply InS.cfg_congr
+  rfl
+  intro i
+  apply InS.vwk_congr_right
+  exact (hG i)
+
 def Eqv.cfgSubstInner {Γ : Ctx α ε} {L : LCtx α}
   (R : LCtx α)
   (G : Quotient (α := ∀i : Fin R.length, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)) inferInstance)
   : Subst.Eqv φ Γ (R ++ L) L
-  := Quotient.liftOn G (λG => ⟦InS.cfgSubst R G⟧) sorry
+  := Quotient.liftOn G (λG => ⟦InS.cfgSubst R G⟧) (λ_ _ h => Quotient.sound <| InS.cfgSubstCongr h)
 
 def Eqv.cfgSubst {Γ : Ctx α ε} {L : LCtx α}
   (R : LCtx α) (G : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
   : Subst.Eqv φ Γ (R ++ L) L
   := cfgSubstInner R (Quotient.finChoice G)
 
+@[simp]
 theorem Eqv.cfgSubst_quot {Γ : Ctx α ε} {L : LCtx α}
   {R : LCtx α} {G : ∀i : Fin R.length, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
-  : cfgSubst R (λi => ⟦G i⟧) = ⟦InS.cfgSubst R G⟧ := sorry
+  : cfgSubst R (λi => ⟦G i⟧) = ⟦InS.cfgSubst R G⟧ := by
+  simp [cfgSubst, Quotient.finChoice_eq, cfgSubstInner]
+
+theorem InS.cfgSubstCongr' {Γ : Ctx α ε} {L : LCtx α}
+  {R : LCtx α} {G G' : ∀i, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} (hG : G ≈ G')
+  : cfgSubst' R G ≈ cfgSubst' R G' := λi => by
+  simp only [List.get_eq_getElem, get_cfgSubst']
+  split
+  · apply InS.cfg_congr
+    rfl
+    intro i
+    apply InS.vwk_congr_right
+    exact (hG i)
+  · rfl
 
 def Eqv.cfgSubstInner' {Γ : Ctx α ε} {L : LCtx α}
   (R : LCtx α)
   (G : Quotient (α := ∀i : Fin R.length, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)) inferInstance)
   : Subst.Eqv φ Γ (R ++ L) L
-  := Quotient.liftOn G (λG => ⟦InS.cfgSubst' R G⟧) sorry
+  := Quotient.liftOn G (λG => ⟦InS.cfgSubst' R G⟧)
+    (λ_ _ h => Quotient.sound <| InS.cfgSubstCongr' h)
 
 def Eqv.cfgSubst' {Γ : Ctx α ε} {L : LCtx α}
   (R : LCtx α) (G : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
   : Subst.Eqv φ Γ (R ++ L) L
   := cfgSubstInner' R (Quotient.finChoice G)
 
+@[simp]
 theorem Eqv.cfgSubst'_quot {Γ : Ctx α ε} {L : LCtx α}
   {R : LCtx α} {G : ∀i : Fin R.length, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
-  : cfgSubst' R (λi => ⟦G i⟧) = ⟦InS.cfgSubst' R G⟧ := sorry
+  : cfgSubst' R (λi => ⟦G i⟧) = ⟦InS.cfgSubst' R G⟧ := by
+  simp [cfgSubst', Quotient.finChoice_eq, cfgSubstInner']
 
 theorem Eqv.cfgSubst_get {Γ : Ctx α ε} {L : LCtx α}
   {R : LCtx α} {G : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} {i : Fin (R ++ L).length}
   : (cfgSubst R G).get i = cfg R (br i (Term.Eqv.var 0 Ctx.Var.shead) (by simp)) (λi => (G i).vwk1)
-  := sorry
+  := by
+  induction G using Eqv.choiceInduction
+  rw [cfgSubst_quot]
+  simp only [List.get_eq_getElem, Subst.Eqv.get_quot, InS.get_cfgSubst, Term.Eqv.var, br_quot, vwk1,
+    vwk_quot]
+  rw [<-cfg_quot]
+  rfl
 
 theorem Eqv.cfgSubst'_get {Γ : Ctx α ε} {L : LCtx α}
   {R : LCtx α} {G : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} {i : Fin (R ++ L).length}
@@ -449,7 +501,13 @@ theorem Eqv.cfgSubst'_get {Γ : Ctx α ε} {L : LCtx α}
           have hi : i < R.length + L.length := List.length_append _ _ ▸ i.prop;
           omega
         )
-  := sorry
+  := by
+  induction G using Eqv.choiceInduction
+  rw [cfgSubst'_quot]
+  simp only [List.get_eq_getElem, Subst.Eqv.get_quot, InS.get_cfgSubst', vwk1_quot]
+  split
+  · rw [<-cfg_quot]; rfl
+  · rfl
 
 theorem Eqv.cfgSubst'_get_ge  {Γ : Ctx α ε} {L : LCtx α}
   {R : LCtx α} {G : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} {i : Fin (R ++ L).length}
@@ -467,7 +525,11 @@ theorem Eqv.cfgSubst'_get_ge  {Γ : Ctx α ε} {L : LCtx α}
 theorem Eqv.vlift_cfgSubst {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
   (G : ∀i : Fin R.length, Eqv φ ((R.get i, ⊥)::Γ) (R ++ L))
   : (Eqv.cfgSubst R G).vlift = Eqv.cfgSubst R (λi => (G i).vwk1 (inserted := inserted)) := by
-  sorry
+  induction G using Eqv.choiceInduction
+  rw [cfgSubst_quot]
+  simp only [Subst.Eqv.vlift_quot, InS.vlift_cfgSubst]
+  rw [<-cfgSubst_quot]
+  rfl
 
 def Eqv.ucfg
   (R : LCtx α)

DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean

@@ -660,7 +660,31 @@ theorem Region.lwk_eqOn_fls (r : Region φ) (ρ ρ' : ℕ → ℕ) (h : r.fls.Eq
     apply Set.subset_iUnion_of_subset
     rfl
 
--- theorem Region.fls_fli {r : Region φ} : r.fls ⊆ Set.Iio r.fli := by sorry
+@[simp]
+def Region.fli : Region φ → ℕ
+  | br ℓ _ => ℓ + 1
+  | case _ s t => Nat.max s.fli t.fli
+  | let1 _ t => t.fli
+  | let2 _ t => t.fli
+  | cfg β n f => Nat.max (β.fli - n) (Finset.sup Finset.univ (λi => (f i).fli - n))
+
+theorem Region.fls_fli {r : Region φ} : r.fls ⊆ Set.Iio r.fli := by induction r with
+  | br => simp
+  | cfg β n G hβ hG =>
+    simp only [fls, fli, Set.Iio_max, Set.Iio_finset_univ_sup]
+    apply Set.union_subset_union
+    intro ℓ hℓ
+    simp [Set.mem_liftnFv] at hℓ
+    convert hβ hℓ using 0
+    simp only [Set.mem_Iio]
+    omega
+    apply Set.iUnion_mono
+    intro i ℓ hℓ
+    simp [Set.mem_liftnFv] at hℓ
+    convert hG i hℓ using 0
+    simp only [gt_iff_lt, Set.mem_Iio]
+    omega
+  | _ => simp only [fls, fli, Set.Iio_max, Set.union_subset_union, *]
 
 end Definitions
 

DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean

@@ -4,6 +4,7 @@ import Discretion.Wk.Multiset
 import Discretion.Wk.Multiset
 
 import DeBruijnSSA.BinSyntax.Syntax.Subst.Term
+import DeBruijnSSA.BinSyntax.Syntax.Subst.Region
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 
@@ -220,13 +221,41 @@ theorem Region.vsubst_eqOn_fvs {r : Region φ} {σ σ' : Term.Subst φ} (h : r.f
 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)
 
--- theorem Region.lsubst_eqOn_fls {r : Region φ} {σ σ' : Subst φ} (h : r.fls.EqOn σ σ')
---   : r.lsubst σ = r.lsubst σ' := by sorry
-
--- TODO: {Terminator, Region}.Subst.{fv, fl}
-
--- TODO: fv_subst, fv_vsubst
-
--- TODO: fl_lsubst
+theorem Region.lsubst_eqOn_fls {r : Region φ} {σ σ' : Subst φ} (h : r.fls.EqOn σ σ')
+  : r.lsubst σ = r.lsubst σ' := by induction r generalizing σ σ' with
+  | br ℓ a => simp [h rfl]
+  | let1 _ _ I => simp [I (σ := σ.vlift) (σ' := σ'.vlift) (λx hx => by simp [Subst.vlift, h hx])]
+  | let2 _ _ I => simp [
+    I (σ := σ.vliftn 2) (σ' := σ'.vliftn 2) (λx hx => by simp [Subst.vliftn_two, Subst.vlift, h hx])
+  ]
+  | case _ _ _ Il Ir => simp [
+    Il (σ := σ.vlift) (σ' := σ'.vlift) (λx hx => by simp [Subst.vlift, h (Or.inl hx)]),
+    Ir (σ := σ.vlift) (σ' := σ'.vlift) (λx hx => by simp [Subst.vlift, h (Or.inr hx)])
+  ]
+  | cfg _ n _ Iβ IG =>
+    simp only [lsubst, cfg.injEq, heq_eq_eq, true_and]
+    constructor
+    · rw [Iβ]
+      intro x hx
+      simp only [Subst.vlift, Function.comp_apply, Subst.liftn]
+      split; rfl
+      rw [h]
+      apply Or.inl
+      rw [Set.mem_liftnFv]
+      convert hx; omega
+    · funext i
+      rw [IG]
+      intro x hx
+      simp only [Subst.vlift, Function.comp_apply, Subst.liftn]
+      split; rfl
+      rw [h]
+      apply Or.inr
+      simp only [Set.mem_iUnion]
+      exact ⟨i, by rw [Set.mem_liftnFv]; convert hx; omega⟩
+
+theorem Region.lsubst_eqOn_fli {r : Region φ} {σ σ' : Subst φ} (h : (Set.Iio r.fli).EqOn σ σ')
+  : r.lsubst σ = r.lsubst σ' := r.lsubst_eqOn_fls (h.mono r.fls_fli)
 
 end Subst
+
+end BinSyntax