ucfg lore

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean

@@ -561,7 +561,9 @@ theorem Eqv.wthen_cfg {B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   = cfg R
     ((f.lwk (LCtx.InS.add_left_append _ _).slift).wthen g)
     (λi => (G i))
-  := sorry
+  := by
+  simp only [wthen, cfg_eq_ucfg, ucfg, lsubst_lsubst]
+  sorry
 
 theorem Eqv.wrseq_cfg {B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ Γ (B::L)) (g : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ C::L))

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -129,4 +129,74 @@ theorem Eqv.vsubst_lsubst {Γ Δ : Ctx α ε}
   induction r using Quotient.inductionOn
   simp [InS.vsubst_lsubst]
 
-end Region
+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
+
+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)
+
+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
+
+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
+
+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)
+
+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
+
+theorem Eqv.cfgSubst_eq_cfgSubst' {Γ : Ctx α ε} {L : LCtx α}
+  {R : LCtx α} {G : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : cfgSubst R G = cfgSubst' R G := sorry
+
+def Eqv.ucfg
+  (R : LCtx α)
+  (β : Eqv φ Γ (R ++ L)) (G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
+  : Eqv φ Γ L := β.lsubst (cfgSubst R G)
+
+theorem Eqv.ucfg_quot
+  {R : LCtx α} {β : InS φ Γ (R ++ L)} {G : ∀i, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : ucfg R ⟦β⟧ (λi => ⟦G i⟧) = ⟦InS.ucfg R β G⟧ := sorry
+
+def Eqv.ucfg'
+  (R : LCtx α)
+  (β : Eqv φ Γ (R ++ L)) (G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
+  : Eqv φ Γ L := β.lsubst (cfgSubst' R G)
+
+theorem Eqv.ucfg'_quot
+  {R : LCtx α} {β : InS φ Γ (R ++ L)} {G : ∀i, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : ucfg' R ⟦β⟧ (λi => ⟦G i⟧) = ⟦InS.ucfg' R β G⟧ := sorry
+
+theorem Eqv.ucfg_eq_ucfg'
+  {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : ucfg R β G = ucfg' R β G := by rw [ucfg, ucfg', cfgSubst_eq_cfgSubst']
+
+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
+
+theorem Eqv.cfg_eq_ucfg
+  {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : cfg R β G = ucfg R β G := by rw [cfg_eq_ucfg', ucfg_eq_ucfg']
+
+theorem Eqv.ucfg'_eq_cfg
+  {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : ucfg' R β G = cfg R β G := Eqv.cfg_eq_ucfg'.symm
+
+theorem Eqv.ucfg_eq_cfg
+  {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : ucfg R β G = cfg R β G := Eqv.cfg_eq_ucfg.symm

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -410,6 +410,24 @@ theorem vsubst_lift_fixpoint (r : Region φ) {ρ : Term.Subst φ}
 
 def ite (b : Term φ) (r r' : Region φ) : Region φ := case b (r.vwk Nat.succ) (r'.vwk Nat.succ)
 
--- end Region
+def cfgSubst (n : ℕ) (G : Fin n → Region φ) : Subst φ
+  := λℓ => cfg (br ℓ (Term.var 0)) n (λi => (G i).vwk1)
 
--- end BinSyntax
+def cfgSubst' (n : ℕ) (G : Fin n → Region φ) : Subst φ
+  := λℓ => if ℓ < n then cfg (br ℓ (Term.var 0)) n (λi => (G i).vwk1) else br (ℓ - n) (Term.var 0)
+
+def ucfg (n : ℕ) (β : Region φ) (G : Fin n → Region φ) : Region φ
+  := β.lsubst (cfgSubst n G)
+
+def ucfg' (n : ℕ) (β : Region φ) (G : Fin n → Region φ) : Region φ
+  := β.lsubst (cfgSubst' n G)
+
+-- TODO: vsubst_ucfg
+
+-- TODO: vwk_ucfg
+
+-- TODO: lsubst_ucfg
+
+-- TODO: lwk_ucfg
+
+-- TODO: likewise for prime...

DeBruijnSSA/BinSyntax/Typing/Ctx.lean

@@ -266,6 +266,14 @@ theorem InS.coe_slift {head : Ty α × ε} {Γ Δ} (hρ : InS Γ Δ)
   : (InS.slift (head := head) hρ : ℕ → ℕ) = Nat.liftWk hρ
   := rfl
 
+theorem InS.lift_congr {lo hi : Ty α × ε} {ρ ρ' : InS Γ Δ} (h : lo ≤ hi) (hρ : ρ ≈ ρ')
+  : ρ.lift h ≈ ρ'.lift h
+  := λ | 0, _ => rfl | n + 1, hi => by simp [hρ n (Nat.lt_of_succ_lt_succ hi)]
+
+theorem InS.slift_congr {head : Ty α × ε} {ρ ρ' : InS Γ Δ} (hρ : ρ ≈ ρ')
+  : ρ.slift (head := head) ≈ ρ'.slift
+  := lift_congr (le_refl _) hρ
+
 @[simp]
 theorem InS.lift_wk0 {head inserted} {Γ : Ctx α ε}
   : wk0.lift (le_refl _) = (wk1 : InS (head::inserted::Γ) (head::Γ))
@@ -381,6 +389,14 @@ theorem InS.coe_sliftn₂ {left right : Ty α × ε} (h : InS Γ Δ)
   : (InS.sliftn₂ (left := left) (right := right) h : ℕ → ℕ) = Nat.liftnWk 2 h
   := rfl
 
+theorem InS.liftn₂_congr {ρ ρ' : InS Γ Δ} (h : lo ≤ hi) (h' : lo' ≤ hi') (hρ : ρ ≈ ρ')
+  : ρ.liftn₂ h h' ≈ ρ'.liftn₂ h h'
+  := by simp only [<-InS.lift_lift]; exact lift_congr h (lift_congr h' hρ)
+
+theorem InS.sliftn₂_congr {left right : Ty α × ε} {ρ ρ' : InS Γ Δ} (hρ : ρ ≈ ρ')
+  : ρ.sliftn₂ (left := left) (right := right) ≈ ρ'.sliftn₂
+  := liftn₂_congr (le_refl _) (le_refl _) hρ
+
 @[simp]
 theorem InS.lift_wk1 {left right inserted} {Γ : Ctx α ε}
   : wk1.lift (le_refl _) = (wk2 : InS (left::right::inserted::Γ) (left::right::Γ))

DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean

@@ -514,8 +514,16 @@ theorem InS.vwk_cfg {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {L} {R : LCtx α}
 
 theorem InS.vwk_equiv {Γ Δ : Ctx α ε} {ρ ρ' : Γ.InS Δ} {L} (r : InS φ Δ L) (h : ρ ≈ ρ')
   : r.vwk ρ = r.vwk ρ'
-  := by induction r using InS.induction with
-  | _ => sorry
+  := by induction r using InS.induction generalizing Γ with
+  | br ℓ a hℓ => simp [a.wk_equiv h]
+  | let1 a r Ir => simp [a.wk_equiv h, Ir (Ctx.InS.slift_congr h)]
+  | let2 a r Ir => simp [a.wk_equiv h, Ir (Ctx.InS.sliftn₂_congr h)]
+  | case a s t Is It => simp [a.wk_equiv h, Is (Ctx.InS.slift_congr h), It (Ctx.InS.slift_congr h)]
+  | cfg R dβ dG Iβ IG =>
+    simp only [vwk_cfg, Iβ h, List.get_eq_getElem]
+    congr
+    funext i
+    simp [IG i (Ctx.InS.slift_congr h)]
 
 @[simp]
 theorem InS.coe_vwk {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {L} {r : InS φ Δ L}

DeBruijnSSA/BinSyntax/Typing/Region/Compose.lean

@@ -338,3 +338,61 @@ theorem InS.vsubst_lift_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   : r.fixpoint.vsubst (σ.lift (le_refl _)) = (r.vsubst (σ.lift (le_refl _))).fixpoint := by
   ext
   simp only [coe_fixpoint, coe_vsubst, Term.Subst.InS.coe_lift, Region.vsubst_lift_fixpoint]
+
+def InS.cfgSubst {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
+  (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : Subst.InS φ Γ (R ++ L) L := ⟨
+    Region.cfgSubst R.length (λi => G i),
+    λℓ => Wf.cfg (hR := rfl)
+      (Wf.br ⟨ℓ.prop, by simp⟩ (Term.Wf.var Ctx.Var.shead))
+      (λi => (G i).prop.vwk1)⟩
+
+@[simp]
+theorem InS.coe_cfgSubst {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
+  (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : (InS.cfgSubst R G : Region.Subst φ) = Region.cfgSubst R.length (λi => G i) := rfl
+
+def InS.cfgSubst' {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
+  (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : Subst.InS φ Γ (R ++ L) L := ⟨
+    Region.cfgSubst' R.length (λi => G i),
+    λℓ => if h : ℓ < R.length then by
+        simp only [Region.cfgSubst', h, ↓reduceIte]
+        exact Wf.cfg (hR := rfl)
+          (Wf.br ⟨ℓ.prop, by simp⟩ (Term.Wf.var Ctx.Var.shead))
+          (λi => (G i).prop.vwk1)
+      else by
+        simp only [Region.cfgSubst', h, ↓reduceIte]
+        apply Wf.br _ (Term.Wf.var Ctx.Var.shead)
+        constructor
+        · simp only [List.get_eq_getElem]
+          rw [List.getElem_append_right]
+          exact h
+        · rw [Nat.sub_lt_iff_lt_add (Nat.le_of_not_lt h)]
+          have h := ℓ.prop
+          simp at h
+          exact h
+    ⟩
+
+@[simp]
+theorem InS.coe_cfgSubst' {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
+  (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : (InS.cfgSubst' R G : Region.Subst φ) = Region.cfgSubst' R.length (λi => G i) := rfl
+
+def InS.ucfg {Γ : Ctx α ε} {L : LCtx α}
+  (R : LCtx α) (β : InS φ Γ (R ++ L)) (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : InS φ Γ L := β.lsubst (InS.cfgSubst R G)
+
+@[simp]
+theorem InS.coe_ucfg {Γ : Ctx α ε} {L : LCtx α}
+  (R : LCtx α) (β : InS φ Γ (R ++ L)) (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : (InS.ucfg R β G : Region φ) = Region.ucfg R.length β (λi => (G i)) := rfl
+
+def InS.ucfg' {Γ : Ctx α ε} {L : LCtx α}
+  (R : LCtx α) (β : InS φ Γ (R ++ L)) (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : InS φ Γ L := β.lsubst (InS.cfgSubst' R G)
+
+@[simp]
+theorem InS.coe_ucfg' {Γ : Ctx α ε} {L : LCtx α}
+  (R : LCtx α) (β : InS φ Γ (R ++ L)) (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
+  : (InS.ucfg' R β G : Region φ) = Region.ucfg' R.length β (λi => (G i)) := rfl

DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean

@@ -210,6 +210,18 @@ theorem Region.InS.vsubst_lsubst {Γ Δ : Ctx α ε}
   : (r.lsubst σ).vsubst ρ = (r.vsubst ρ).lsubst (σ.vsubst ρ)
   := by ext; simp [Region.vsubst_lsubst]
 
+def LCtx.InS.toSubst {Γ : Ctx α ε} {L K : LCtx α} (ρ : L.InS K) : Region.Subst.InS φ Γ L K
+  := ⟨Region.Subst.fromLwk ρ, λℓ => Region.Wf.br (ρ.prop ℓ ℓ.prop) (Term.Wf.var Ctx.Var.shead)⟩
+
+@[simp]
+theorem LCtx.InS.coe_toSubst {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K}
+  : (ρ.toSubst (φ := φ) (Γ := Γ) : Region.Subst φ) = Region.Subst.fromLwk ρ
+  := rfl
+
+def Region.InS.lsubst_toSubst {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K} {r : Region.InS φ Γ L}
+  : r.lsubst (ρ.toSubst) = r.lwk ρ
+  := by ext; simp [Region.lsubst_fromLwk]
+
 end RegionSubst
 
 end BinSyntax

DeBruijnSSA/BinSyntax/Typing/Region/VSubst.lean

@@ -66,3 +66,6 @@ theorem Region.InS.vsubst_vsubst {Γ Δ Ξ : Ctx α ε}
   {σ : Term.Subst.InS φ Γ Δ} {τ : Term.Subst.InS φ Δ Ξ}
   (r : InS φ Ξ L) : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ)
   := by ext; simp [Region.vsubst_vsubst]
+
+theorem Region.InS.vsubst_toSubst {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {L} {r : InS φ Δ L}
+  : r.vsubst ρ.toSubst = r.vwk ρ := by ext; simp [Region.vsubst_fromWk]

DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean

@@ -292,3 +292,14 @@ def Subst.InS.fromWk {Γ Δ : Ctx α ε} (h : Γ.InS Δ) : Subst.InS φ Γ Δ
 theorem Subst.InS.coe_fromWk {Γ Δ : Ctx α ε} (h : Γ.InS Δ)
   : ((fromWk h : Subst.InS φ Γ Δ) : Subst φ) = Subst.fromWk h
   := rfl
+
+def _root_.BinSyntax.Ctx.InS.toSubst {Γ Δ : Ctx α ε} (h : Γ.InS Δ) : Subst.InS φ Γ Δ
+  := ⟨Subst.fromWk h, λx => by have h := h.prop x.val x.prop; simp at h; simp [h]⟩
+
+@[simp]
+theorem _root_.BinSyntax.Ctx.InS.coe_toSubst {Γ Δ : Ctx α ε} {h : Γ.InS Δ}
+  : ((h.toSubst : Subst.InS φ Γ Δ) : Subst φ) = Subst.fromWk h
+  := rfl
+
+theorem InS.subst_toSubst {Γ Δ : Ctx α ε} {h : Γ.InS Δ} {a : InS φ Δ V}
+  : a.subst h.toSubst = a.wk h := by ext; simp [Term.subst_fromWk]