Draft uniformity

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

@@ -269,15 +269,6 @@ theorem Eqv.fixpoint_naturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::L))
   : fixpoint (f ;; sum g nil) = (fixpoint f) ;; g := by rw [fixpoint_seq]
 
--- TODO: this is derivable, probably: see Proposition 16 in Unifying Guarded and Unguarded Iteration
--- by Goncharov et al
-theorem Eqv.fixpoint_dinaturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod C)::L))
-  (g : Eqv φ (⟨C, ⊥⟩::Γ) ((B.coprod A)::L))
-  : fixpoint (f ;; coprod inj_l g) = f ;; coprod nil (fixpoint (g ;; coprod inj_l f))
-  := by
-  sorry
-
 theorem Eqv.fixpoint_codiagonal {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) (((B.coprod A).coprod A)::L))
   : fixpoint (fixpoint f) = fixpoint (f ;; coprod nil inj_r) := by
@@ -426,6 +417,35 @@ theorem Eqv.fixpoint_strong_left {X A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   simp only [<-vwk1_fixpoint]
   rfl
 
+-- TODO: this is derivable, probably: see Proposition 16 in Unifying Guarded and Unguarded Iteration
+-- by Goncharov et al
+theorem Eqv.fixpoint_dinaturality_seq_cfg {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod C)::L))
+  (g : Eqv φ (⟨C, ⊥⟩::Γ) ((B.coprod A)::L))
+  : fixpoint (f ;; coprod inj_l g)
+  = cfg [A] (f.lwk1 ;; (inj_l.coprod g.lwk1 ;; left_exit))
+            (Fin.elim1 (f.lwk1 ;; (inj_l.coprod g.lwk1 ;; left_exit)).vwk1) := by
+  rw [fixpoint_iter_cfg]
+  simp only [
+    lwk1_seq, vwk1_seq, lwk1_coprod, vwk1_coprod, vwk1_inj_l, lwk1_inj_l, lwk1_vwk1,
+    seq_assoc
+  ]
+  rfl
+
+-- theorem Eqv.fixpoint_dinaturality_left_loop {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+--   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod C)::L))
+--   (g : Eqv φ (⟨C, ⊥⟩::Γ) ((B.coprod A)::L))
+--   : fixpoint (f ;; coprod inj_l g)
+--   = cfg [A] f.lwk1
+--             (Fin.elim1 (f.lwk1 ;; (inj_l.coprod g.lwk1 ;; left_exit)).vwk1) := by
+--   sorry
+
+theorem Eqv.fixpoint_dinaturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod C)::L))
+  (g : Eqv φ (⟨C, ⊥⟩::Γ) ((B.coprod A)::L))
+  : fixpoint (f ;; coprod inj_l g) = f ;; coprod nil (fixpoint (g ;; coprod inj_l f))
+  := by sorry
+
 end Region
 
 end BinSyntax

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -45,7 +45,7 @@ theorem Subst.Eqv.ext {σ τ : Subst.Eqv φ Γ L K} (h : ∀i, σ.get i = τ.get
   induction τ using Quotient.inductionOn
   exact Subst.Eqv.ext_quot h
 
-theorem Subst.Eqv.ext_iff {σ τ : Subst.Eqv φ Γ L K} : σ = τ ↔ ∀i, σ.get i = τ.get i := by
+theorem Subst.Eqv.ext_iff' {σ τ : Subst.Eqv φ Γ L K} : σ = τ ↔ ∀i, σ.get i = τ.get i := by
   refine ⟨λh i => h ▸ rfl, Subst.Eqv.ext⟩
 
 theorem Subst.Eqv.get_toSubst {Γ : Ctx α ε} {L K : LCtx α} {σ : L.InS K}
@@ -84,6 +84,13 @@ theorem Subst.Eqv.vliftn₂_eq_vlift_vlift {Γ : Ctx α ε} {L K : LCtx α} (σ
   induction σ using Quotient.inductionOn;
   simp [Subst.InS.vliftn₂_eq_vlift_vlift]
 
+def Subst.Eqv.extend {Γ : Ctx α ε} {L K R : LCtx α} (σ : Eqv φ Γ L K) : Eqv φ Γ (L ++ R) (K ++ R)
+  := Quotient.liftOn σ (λσ => ⟦σ.extend⟧) sorry
+
+@[simp]
+theorem Subst.Eqv.extend_quot {Γ : Ctx α ε} {L K R : LCtx α} {σ : Subst.InS φ Γ L K}
+  : extend (R := R) ⟦σ⟧ = ⟦σ.extend⟧ := rfl
+
 @[simp]
 theorem InS.lsubst_q {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K} {r : InS φ Γ L}
    : (r.q).lsubst ⟦σ⟧ = (r.lsubst σ).q := rfl
@@ -394,3 +401,15 @@ theorem Eqv.ucfg'_eq_cfg
 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
+
+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
+
+theorem Eqv.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
+  {σ : Subst.Eqv φ Γ R R'} {β : Eqv φ Γ (R ++ L)}
+  {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (R ++ L)}
+  : cfg R' (β.lsubst σ.extend) (λi => (G i).lsubst σ.extend.vlift)
+  = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG G).vlift)
+  := sorry

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -608,3 +608,10 @@ theorem InS.codiagonal {Γ : Ctx α ε} {L : LCtx α}
   : cfg [A] β (Fin.elim1 (cfg [A] nil (Fin.elim1 G.vwk1)))
   ≈ cfg [A] β (Fin.elim1 (G.lsubst nil.lsubst0)) := by
   sorry
+
+theorem InS.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
+  {σ : Subst.InS φ Γ R R'} {β : InS φ Γ (R ++ L)}
+  {G : (i : Fin R'.length) → InS φ (⟨R'.get i, ⊥⟩::Γ) (R ++ L)}
+  : cfg R' (β.lsubst σ.extend) (λi => (G i).lsubst σ.extend.vlift)
+  = cfg R β (λi => (σ.cfg i).lsubst (CFG.toSubst G).vlift)
+  := sorry

DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean

@@ -137,7 +137,6 @@ inductive TStep : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) →
   | rewrite {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → Rewrite r r' → TStep Γ L r r'
   | reduce {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → Reduce r r' → TStep Γ L r r'
   | initial {Γ L} : Γ.IsInitial → r.Wf Γ L → r'.Wf Γ L → TStep Γ L r r'
-  -- TODO: replace "terminal" with general term rewriting... can be much nicer, maybe...
   | let1_equiv {Γ L} : Term.Uniform Term.TStep Γ ⟨A, e⟩ a a' → r.Wf (⟨A, ⊥⟩::Γ) L
     → TStep Γ L (let1 a r) (let1 a' r)
 

DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean

@@ -57,12 +57,18 @@ inductive Uniform (P : Ctx α ε → LCtx α → Region φ → Region φ → Pro
       → β.Wf Γ (R ++ L)
       → (∀i : Fin n, (G i).Wf ((R.get (i.cast hR.symm), ⊥)::Γ) (R ++ L)) →
       Uniform P Γ L (cfg β n G) (ucfg' n β G)
+  | dinaturality {Γ : Ctx α ε} {L R R' : LCtx α} {β : Region φ}
+    {G : Fin R'.length → Region φ} {σ : Subst φ}
+    : σ.Wf Γ R R'
+      → β.Wf Γ (R ++ L)
+      → (∀i : Fin R'.length, (G i).Wf ((R'.get i, ⊥)::Γ) (R ++ L))
+      → Uniform P Γ L
+        (cfg
+          (β.lsubst (σ.extend R.length R'.length)) R'.length
+          (λi => (G i).lsubst (σ.extend R.length R'.length).vlift))
+        (cfg β R.length
+          (λi => (σ i).lsubst (Subst.fromFCFG (R.length + L.length) G).vlift))
   | refl : r.Wf Γ L → Uniform P Γ L r r
-  -- TODO: this should be a theorem, later
-  -- | let1_equiv {a a' : Term φ} {r : Region φ}
-  --   : Term.Uniform Term.TStep Γ ⟨A, e⟩ a a'
-  --   → r.Wf (⟨A, ⊥⟩::Γ) L
-  --   → Uniform P Γ L (Region.let1 a r) (Region.let1 a' r)
   | rel : P Γ L x y → Uniform P Γ L x y
   | symm : Uniform P Γ L x y → Uniform P Γ L y x
   | trans : Uniform P Γ L x y → Uniform P Γ L y z → Uniform P Γ L x z
@@ -147,9 +153,10 @@ theorem Uniform.wf {P : Ctx α ε → LCtx α → Region φ → Region φ → Pr
       intro i; cases i using Fin.elim1;
       apply dG.lsubst Wf.nil.lsubst0
   | ucfg hR dβ dG => exact ⟨Wf.cfg _ _ hR dβ dG, Wf.ucfg' _ _ hR dβ dG⟩
+  | dinaturality hσ dβ dG => exact ⟨
+      Wf.cfg _ _ rfl (dβ.lsubst hσ.extend) (λi => (dG i).lsubst hσ.extend.vlift),
+      Wf.cfg _ _ rfl dβ (λi => (hσ i).lsubst (Subst.Wf.fromFCFG' rfl dG (by simp)).vlift)⟩
   | refl h => exact ⟨h, h⟩
-  -- | let1_equiv da dr => exact ⟨dr.let1 (da.left TStep.wf),
-  --                              dr.let1 (da.right TStep.wf)⟩
   | rel h => exact toWf h
   | symm _ I => exact I.symm
   | trans _ _ Il Ir => exact ⟨Il.1, Ir.2⟩
@@ -168,6 +175,70 @@ theorem Uniform.wf_iff {P : Ctx α ε → LCtx α → Region φ → Region φ 
   (toWf : ∀{Γ L r r'}, P Γ L r r' → r.Wf Γ L ∧ r'.Wf Γ L)
   : (Uniform P Γ L r r) ↔ r.Wf Γ L := ⟨Uniform.left toWf, Uniform.refl⟩
 
+theorem vwk_dinaturality_left {Γ : Ctx α ε} {L R R' : LCtx α} {β : Region φ}
+  {G : Fin R'.length → Region φ} {σ : Subst φ}
+  (hσ : σ.Wf Γ R R')
+  (dβ : β.Wf Γ (R ++ L))
+  (dG : (∀i : Fin R'.length, (G i).Wf ((R'.get i, ⊥)::Γ) (R ++ L)))
+  : (cfg
+          (β.lsubst (σ.extend R.length R'.length)) R'.length
+          (λi => (G i).lsubst (σ.extend R.length R'.length).vlift)).vwk ρ
+    = (cfg ((β.vwk ρ).lsubst
+      (Subst.extend (vwk (Nat.liftWk ρ) ∘ σ) R.length R'.length)) R'.length
+    (λi => ((G i).vwk (Nat.liftWk ρ)).lsubst
+      (Subst.extend (vwk (Nat.liftWk ρ) ∘ σ) R.length R'.length).vlift)) := by
+  simp only [vwk_cfg, vwk_lsubst]
+  congr
+  · funext ℓ
+    simp only [Function.comp_apply, Subst.extend]
+    split <;> rfl
+  · funext i
+    congr
+    funext ℓ
+    simp only [Function.comp_apply, Subst.extend, Subst.vlift]
+    split
+    · sorry
+    · rfl
+  -- · rw [Region.lsubst_eqOn_fls]
+  --   intro ℓ hℓ
+  --   have hℓ' : ℓ < R.length := by
+  --     rw [fls_vwk] at hℓ;
+  --     exact dβ.fls hℓ
+  --   simp [Subst.extend, hℓ']
+  -- · funext i
+  --   rw [Region.lsubst_eqOn_fls]
+  --   intro ℓ hℓ
+  --   have hℓ' : ℓ < R.length := sorry
+  --   simp only [Subst.vlift, vwk1, Function.comp_apply, Subst.extend, hℓ', ↓reduceIte, vwk_vwk]
+  --   congr
+  --   funext k; cases k <;> rfl
+
+theorem vwk_dinaturality_right {Γ : Ctx α ε} {L R R' : LCtx α} {β : Region φ}
+  {G : Fin R'.length → Region φ} {σ : Subst φ}
+  (hσ : σ.Wf Γ R R')
+  (dβ : β.Wf Γ (R ++ L))
+  (dG : (∀i : Fin R'.length, (G i).Wf ((R'.get i, ⊥)::Γ) (R ++ L)))
+  : (cfg β R.length
+          (λi => (σ i).lsubst (Subst.fromFCFG (R.length + L.length) G).vlift)).vwk ρ
+    = (cfg (β.vwk ρ) R.length
+          (λi => ((σ i).vwk (Nat.liftWk ρ)).lsubst
+            (Subst.fromFCFG (R.length + L.length) (vwk (Nat.liftWk ρ) ∘ G)).vlift)) := by
+  simp only [vwk_cfg, vwk_lsubst]
+  congr
+  funext i
+  congr
+  funext ℓ
+  simp only [Function.comp_apply, Subst.fromFCFG, Subst.vlift]
+  split
+  · sorry
+  · rfl
+  -- rw [Region.lsubst_eqOn_fls]
+  -- intro ℓ hℓ
+  -- have hℓ' : ℓ < R'.length := sorry
+  -- simp only [Subst.vlift, vwk1, Function.comp_apply, Subst.fromFCFG, hℓ', ↓reduceDIte, vwk_vwk]
+  -- congr
+  -- funext k; cases k <;> rfl
+
 theorem Uniform.vwk {P Q : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ Δ L r r'}
   (toVwk : ∀{Γ Δ L ρ r r'}, Γ.Wkn Δ ρ → P Δ L r r' → Q Γ L (r.vwk ρ) (r'.vwk ρ))
   (hρ : Γ.Wkn Δ ρ)
@@ -203,8 +274,15 @@ theorem Uniform.vwk {P Q : Ctx α ε → LCtx α → Region φ → Region φ →
     simp only [vwk1, vwk_vwk]
     congr; funext k; cases k <;> rfl
   | ucfg hR dβ dG =>
-    simp only [vwk_cfg]
-    sorry
+    simp only [vwk_cfg, vwk_ucfg']
+    exact ucfg hR (dβ.vwk hρ) (λi => (dG i).vwk hρ.slift)
+  | dinaturality hσ dβ dG =>
+    rename_i L R R' β G σ
+    rw [vwk_dinaturality_left hσ dβ dG, vwk_dinaturality_right hσ dβ dG]
+    exact dinaturality
+      (σ := (Region.vwk (Nat.liftWk ρ)) ∘ σ)
+      (λi => (hσ i).vwk hρ.slift) (dβ.vwk hρ)
+      (λi => (dG i).vwk hρ.slift)
 
 theorem Uniform.lwk {P Q : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L K r r'}
   (toLwk : ∀{Γ L K ρ r r'}, L.Wkn K ρ → P Γ L r r' → Q Γ K (r.lwk ρ) (r'.lwk ρ))
@@ -238,7 +316,11 @@ theorem Uniform.lwk {P Q : Ctx α ε → LCtx α → Region φ → Region φ →
       simp only [lwk_lift_wseq] at Ih
       exact Ih
   | codiagonal => sorry
-  | ucfg hR dβ dG => sorry
+  | ucfg hR dβ dG =>
+    simp only [lwk_cfg, lwk_ucfg']
+    exact ucfg hR (dβ.lwk (hR ▸ hρ.liftn_append)) (λi => (dG i).lwk (hR ▸ hρ.liftn_append))
+  | dinaturality =>
+    sorry
 
 theorem Uniform.vsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ Δ L r r'}
   (toVsubst : ∀{Γ Δ L σ r r'}, σ.Wf Γ Δ → P Δ L r r' → Q Γ L (r.vsubst σ) (r'.vsubst σ))
@@ -269,7 +351,11 @@ theorem Uniform.vsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
       simp only [vsubst_lift_wseq] at Ih
       exact Ih
   | codiagonal => sorry
-  | ucfg hR dβ dG => sorry
+  | ucfg hR dβ dG =>
+    simp only [vsubst_cfg, vsubst_ucfg']
+    exact ucfg hR (dβ.vsubst hσ) (λi => (dG i).vsubst hσ.slift)
+  | dinaturality =>
+    sorry
 
 theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L K r r'}
   (toLsubst : ∀{Γ L K σ r r'}, σ.Wf Γ L K → P Γ L r r' → Q Γ K (r.lsubst σ) (r'.lsubst σ))
@@ -305,7 +391,12 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
       simp only [lsubst_vlift_lift_wseq] at Ih
       exact Ih
   | codiagonal => sorry
-  | ucfg hR dβ dG => sorry
+  | ucfg hR dβ dG =>
+    simp only [lsubst_cfg, lsubst_ucfg']
+    exact ucfg hR (dβ.lsubst (hσ.liftn_append' hR.symm))
+      (λi => (dG i).lsubst (hσ.liftn_append' hR.symm).vlift)
+  | dinaturality =>
+    sorry
 
 theorem Uniform.vsubst_flatten {P : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ Δ L r r'}
   (toVsubst : ∀{Γ Δ L σ r r'}, σ.Wf Γ Δ → P Δ L r r' → Uniform P Γ L (r.vsubst σ) (r'.vsubst σ))

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -621,7 +621,7 @@ theorem Subst.Eqv.ext {σ τ : Subst.Eqv φ Γ Δ} (h : ∀i, get σ i = get τ
   induction τ using Quotient.inductionOn
   exact ext_quot h
 
-theorem Subst.Eqv.ext_iff {σ τ : Subst.Eqv φ Γ Δ}
+theorem Subst.Eqv.ext_iff' {σ τ : Subst.Eqv φ Γ Δ}
   : σ = τ ↔ ∀i, get σ i = get τ i := ⟨λh => by simp [h], ext⟩
 
 -- TODO: rewrite to use get, eliminating a sorry implicitly?

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -7,13 +7,6 @@ namespace Region
 
 variable {φ : Type u} {ε : Type v} [Φ: EffectSet φ ε] [SemilatticeSup ε] [OrderBot ε]
 
-def lsubst0 (r : Region φ) : Subst φ
-  | 0 => r
-  | ℓ + 1 => br ℓ (Term.var 0)
-
-def alpha (ℓ : ℕ) (r : Region φ) : Subst φ
-  := Function.update Subst.id ℓ r
-
 def ret (e : Term φ) := br 0 e
 
 theorem vwk_ret (e : Term φ) : vwk ρ (ret e) = ret (Term.wk ρ e) := rfl