uniformity axiom

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

@@ -279,11 +279,38 @@ theorem Eqv.fixpoint_codiagonal {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   rw [fixpoint, fixpoint, vwk1_fixpoint, lwk1_fixpoint, fixpoint_seq, fixpoint]
   sorry
 
+theorem Eqv.seq_fixpoint_eq_cfg {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (h : Eqv φ (⟨A, ⊥⟩::Γ) (B::L))
+  (f : Eqv φ (⟨B, ⊥⟩::Γ) ((C.coprod B)::L))
+  : h ;; fixpoint f = cfg [B] h.lwk1 (Fin.elim1 (f.lwk1.vwk1 ;; left_exit)) := by
+  sorry
+
+theorem Eqv.seq_fixpoint_eq_wrseq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (h : Eqv φ (⟨A, ⊥⟩::Γ) (B::L))
+  (f : Eqv φ (⟨B, ⊥⟩::Γ) ((C.coprod B)::L))
+  : h ;; fixpoint f = cfg [B] (nil.wrseq h.lwk1.vwk1) (Fin.elim1 (f.lwk1.vwk1 ;; left_exit)) := by
+  sorry
+
 theorem Eqv.fixpoint_uniformity {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)) (g : Eqv φ (⟨C, ⊥⟩::Γ) ((B.coprod C)::L))
   (h : Eqv φ (⟨C, ⊥⟩::Γ) (A::L)) (hh : h.Pure)
   (hfg : h ;; f = g ;; sum nil h)
-  : h ;; (fixpoint f) = fixpoint g := sorry
+  : h ;; (fixpoint f) = fixpoint g := by
+  rw [seq_fixpoint_eq_wrseq, fixpoint]
+  have ⟨e, he⟩ := hh
+  cases he
+  rw [lwk1_ret, vwk1_ret]
+  apply uniform
+  rw [
+    <-seq_assoc, <-lwk1_ret, vwk1_lwk1, <-lwk1_seq, <-vwk1_ret, <-vwk1_seq, hfg, vwk1_seq, lwk1_seq,
+    seq_assoc, seq_assoc
+  ]
+  congr 1
+  simp only [vwk1_ret, lwk1_ret, vwk1_sum, lwk1_sum, nil_vwk1, nil_lwk1]
+  simp only [
+    left_exit_eq_coprod, sum_seq_coprod, nil_seq, ret_var_zero, seq_nil, coprod_seq,
+    br_succ_seq
+  ]
 
 theorem Eqv.pi_r_fixpoint_uniform_inner {X A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)} : pi_r ;; f = X ⋊ f ;; distl_inv ;; sum pi_r pi_r := by

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

@@ -737,3 +737,29 @@ theorem Eqv.let2_eta_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     ((ret $ (Term.Eqv.var 1 Ctx.Var.shead.step).pair (Term.Eqv.var 0 Ctx.Var.shead))
       ;; f.vwk1.vwk1)
   = f := by rw [<-let2_seq, let2_eta_nil, nil_seq]
+
+theorem Eqv.uniform_wseq {Γ : Ctx α ε} {L : LCtx α}
+  {β : Eqv φ Γ (A::L)} {e : Term.Eqv φ ((A, ⊥)::Γ) (B, ⊥)}
+  {r : Eqv φ ((B, ⊥)::Γ) (B::L)} {s : Eqv φ ((A, ⊥)::Γ) (A::L)}
+  (hrs : (ret e).wseq r = s.wseq (ret e))
+  : cfg [B] (β.wrseq (ret e)) (Fin.elim1 r) = cfg [A] β (Fin.elim1 s) := by
+  induction β using Quotient.inductionOn with
+  | h β => induction e using Quotient.inductionOn with
+  | h e => induction r using Quotient.inductionOn with
+  | h r => induction s using Quotient.inductionOn with
+  | h s =>
+    simp only [
+      br_quot, wrseq_quot, List.length_singleton, List.get_eq_getElem, List.singleton_append
+    ]
+    apply Quotient.sound
+    simp only [br_quot, wseq_quot] at hrs
+    convert InS.uniform (β := β) (e := e) (r := r) (s := s) (Quotient.exact hrs) using 2
+    <;> funext i <;> cases i using Fin.elim1 <;> rfl
+
+theorem Eqv.uniform {Γ : Ctx α ε} {L : LCtx α}
+  {β : Eqv φ Γ (A::L)} {e : Term.Eqv φ ((A, ⊥)::Γ) (B, ⊥)}
+  {r : Eqv φ ((B, ⊥)::Γ) (B::L)} {s : Eqv φ ((A, ⊥)::Γ) (A::L)}
+  (hrs : (ret e) ;; r = s ;; (ret e))
+  : cfg [B] (β.wrseq (ret e)) (Fin.elim1 r) = cfg [A] β (Fin.elim1 s) := by
+  simp only [<-wseq_eq_seq] at hrs
+  exact Eqv.uniform_wseq hrs

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -139,6 +139,12 @@ theorem Eqv.cfg_quot
   {R : LCtx α} {β : InS φ Γ (R ++ L)} {G : ∀i, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
   : cfg R ⟦β⟧ (λi => ⟦G i⟧) = ⟦InS.cfg R β G⟧ := InS.cfg_q
 
+@[simp]
+theorem Eqv.cfg1_quot
+  {β : InS φ Γ (B::L)} {G : InS φ (⟨B, ⊥⟩::Γ) (B::L)}
+  : cfg [B] ⟦β⟧ (Fin.elim1 ⟦G⟧) = ⟦InS.cfg [B] β (Fin.elim1 G)⟧ := by
+  rw [<-cfg_quot]; congr; funext i; cases i using Fin.elim1; rfl
+
 theorem Eqv.cfg_eq_quot {R : LCtx α}
   {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
   {β' : InS φ Γ (R ++ L)} {G' : ∀i, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
@@ -470,6 +476,12 @@ theorem Eqv.vwk_cfg {Γ : Ctx α ε} {L : LCtx α}
   induction β using Quotient.inductionOn
   sorry
 
+theorem Eqv.vwk_cfg1 {Γ : Ctx α ε} {L : LCtx α}
+  {B : Ty α} {β : Eqv φ Δ (B::L)} {G : Eqv φ (⟨B, ⊥⟩::Δ) (B::L)}
+  {ρ : Γ.InS Δ}
+  : Eqv.vwk ρ (cfg [B] β (Fin.elim1 G)) = cfg [B] (β.vwk ρ) (Fin.elim1 (G.vwk ρ.slift)) := by
+  rw [Eqv.vwk_cfg]; congr; funext i; cases i using Fin.elim1; rfl
+
 theorem InS.lwk_q {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K} {r : InS φ Γ L}
    : (r.q).lwk ρ = (r.lwk ρ).q := rfl
 
@@ -583,6 +595,13 @@ theorem Eqv.vsubst_cfg {Γ : Ctx α ε} {L : LCtx α}
   induction β using Quotient.inductionOn
   sorry
 
+theorem Eqv.vsubst_cfg1 {Γ : Ctx α ε} {L : LCtx α}
+  {B : Ty α} {β : Eqv φ Δ (B::L)} {G : Eqv φ (⟨B, ⊥⟩::Δ) (B::L)}
+  {σ : Term.Subst.Eqv φ Γ Δ}
+  : (Eqv.vsubst σ (Eqv.cfg [B] β (Fin.elim1 G)))
+  = (Eqv.cfg [B] (Eqv.vsubst σ β) (Fin.elim1 (Eqv.vsubst (σ.lift (le_refl _)) G)))
+  := by rw [vsubst_cfg]; congr; funext i; cases i using Fin.elim1; rfl
+
 theorem InS.lwk_id_q {Γ : Ctx α ε} {L K : LCtx α} {r : InS φ Γ L}
   (hρ : L.Wkn K id) : (r.q).lwk_id hρ = (r.lwk_id hρ).q := rfl
 

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -585,3 +585,20 @@ theorem InS.vsubst_congr {Γ Δ : Ctx α ε} {L : LCtx α}
   {σ σ' : Term.Subst.InS φ Γ Δ} (hσ : σ ≈ σ') {r r' : InS φ Δ L} (hr : r ≈ r')
   : r.vsubst σ ≈ r'.vsubst σ'
   := (vsubst_subst_equiv hσ r).trans (vsubst_congr_right _ hr)
+
+theorem InS.uniform {Γ : Ctx α ε} {L : LCtx α}
+  {β : InS φ Γ (A::L)} {e : Term.InS φ ((A, ⊥)::Γ) (B, ⊥)}
+  {r : InS φ ((B, ⊥)::Γ) (B::L)} {s : InS φ ((A, ⊥)::Γ) (A::L)}
+  (hrs : (ret e).wseq r ≈ s.wseq (ret e))
+  : cfg [B] (β.wrseq (ret e)) (Fin.elim1 r) ≈ cfg [A] β (Fin.elim1 s) := by
+  simp only [eqv_def, Set.mem_setOf_eq, coe_wseq, coe_ret] at hrs
+  have h := Uniform.uniform (P := TStep) β.prop e.prop r.prop s.prop hrs;
+  simp only [List.length_singleton, List.get_eq_getElem, List.singleton_append, eqv_def,
+    Set.mem_setOf_eq, coe_cfg, coe_wrseq, coe_ret]
+  convert h
+  rename Fin 1 => i
+  cases i using Fin.elim1
+  rfl
+  rename Fin 1 => i
+  cases i using Fin.elim1
+  rfl