Tap

DeBruijnSSA/BinSyntax/Acyclic.lean

@@ -180,8 +180,8 @@ theorem SAcyclic'.acyclic' (h : SAcyclic' D r) : Acyclic' D r := by
     apply Acyclic'.antitone _ (IG i)
     apply Set.union_subset_iff.mpr
     constructor
-    . simp
-    . intro x hx'
+    · simp
+    · intro x hx'
       right
       cases hx'.lt_or_eq with
       | inl h => exact lt_of_lt_of_le h (le_refl _)
@@ -331,19 +331,19 @@ theorem SAcyclic'.of_sacyclic {r : Region φ} (h : SAcyclic r) (hD : ∀x ∈ r.
   | let2 e _ Is => exact SAcyclic'.let2 e (Is (λi hi => hD i (by simp [hi])))
   | cfg hβ hG hG' Iβ IG =>
     apply SAcyclic'.cfg
-    . apply Iβ
+    · apply Iβ
       simp only [Set.mem_image, not_exists, not_and]
       intro i hi j hj c
       cases c
       apply hD j
       simp [Multiset.mem_liftnFv, hi]
       exact hj
-    . intro i
+    · intro i
       apply IG
       intro j hj
       simp only [Set.mem_union, Set.mem_image, not_or, not_exists, not_and]
       constructor
-      . intro x hx c
+      · intro x hx c
         cases c
         apply hD x
         simp only [fl, Multiset.mem_add, Multiset.mem_liftnFv]
@@ -352,7 +352,7 @@ theorem SAcyclic'.of_sacyclic {r : Region φ} (h : SAcyclic r) (hD : ∀x ∈ r.
         simp only [Finset.mem_univ, Multiset.mem_liftnFv, true_and]
         exact ⟨_, hj⟩
         exact hx
-      . exact Nat.not_lt_of_le $ (SAcyclic.cfg hβ hG hG').successors_ge i j hj
+      · exact Nat.not_lt_of_le $ (SAcyclic.cfg hβ hG hG').successors_ge i j hj
 
 -- TODO: relationship between SAcyclic and SACyclic'
 
@@ -410,20 +410,20 @@ theorem Acyclic'.of_acyclic {r : Region φ} (h : Acyclic r) (hD : ∀x ∈ r.fl,
   | let2 e _ Is => exact Acyclic'.let2 e (Is (λi hi => hD i (by simp [hi])))
   | cfg _ _ hG Iβ IG =>
     apply Acyclic'.cfg
-    . apply Iβ
+    · apply Iβ
       intro i hi
       simp only [Set.mem_image, not_exists, not_and]
       intro j hj hj'
       cases hj'
       apply hD j
       simp [Multiset.mem_liftnFv, hi]
       exact hj
-    . intro i
+    · intro i
       apply IG
       intro j hj
       simp only [Set.mem_union, Set.mem_image, not_or, not_exists, not_and]
       constructor
-      . intro x hx c
+      · intro x hx c
         cases c
         apply hD x
         simp only [fl, Multiset.mem_add, Multiset.mem_liftnFv]
@@ -432,7 +432,7 @@ theorem Acyclic'.of_acyclic {r : Region φ} (h : Acyclic r) (hD : ∀x ∈ r.fl,
         simp only [Finset.mem_univ, Multiset.mem_liftnFv, true_and]
         exact ⟨_, hj⟩
         exact hx
-      . intro c
+      · intro c
         have c' := Ancestors.of_split hj c
         apply hG ⟨j, c'.lt⟩ c'
 

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

@@ -33,39 +33,52 @@ theorem Eqv.Pure.distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 
 -- TODO: "naturality"
 
-def Eqv.control {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+def Eqv.left_exit {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) (B::A::L) :=
   case (var 0 Ctx.Var.shead)
     (br 1 (var 0 (by simp)) ⟨by simp, le_refl _⟩)
     (ret (var 0 (by simp)))
 
+theorem Eqv.left_exit_def {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : left_exit (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = ⟦InS.left_exit⟧ := rfl
+
 @[simp]
-theorem Eqv.vwk1_control {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  : (control (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = control
+theorem Eqv.vwk1_left_exit {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : (left_exit (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = left_exit
   := rfl
 
 @[simp]
-theorem Eqv.vwk2_control {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  : (control (φ := φ) (A := A) (B := B) (Γ := (X::Γ)) (L := L)).vwk2 (inserted := inserted)
-  = control
+theorem Eqv.vwk2_left_exit {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : (left_exit (φ := φ) (A := A) (B := B) (Γ := (X::Γ)) (L := L)).vwk2 (inserted := inserted)
+  = left_exit
   := rfl
 
 def Eqv.fixpoint {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
-  : Eqv φ (⟨A, ⊥⟩::Γ) (B::L) := cfg [A] nil (λ| ⟨0, _⟩ => f.vwk1.lwk1 ;; control)
+  : Eqv φ (⟨A, ⊥⟩::Γ) (B::L) := cfg [A] nil (Fin.elim1 (f.vwk1.lwk1 ;; left_exit))
+
+theorem Eqv.fixpoint_quot {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (f : InS φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
+  : fixpoint ⟦f⟧ = ⟦f.fixpoint⟧ := by
+  simp only [fixpoint, nil, List.append_eq, List.nil_append, List.length_singleton,
+    List.get_eq_getElem, List.singleton_append, Fin.zero_eta, Fin.isValue, Fin.val_zero,
+    List.getElem_cons_zero, vwk1_quot, lwk1_quot, left_exit_def, seq_quot]
+  apply Eqv.cfg_eq_quot rfl
+  intro i
+  cases i using Fin.elim1; rfl
 
 theorem Eqv.fixpoint_iter_cfg {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
-  : fixpoint f = cfg [A] (f.lwk1 ;; control) (λ| ⟨0, _⟩ => f.vwk1.lwk1 ;; control) := by
+  : fixpoint f = cfg [A] (f.lwk1 ;; left_exit) (Fin.elim1 (f.vwk1.lwk1 ;; left_exit)) := by
   rw [fixpoint, <-ret_nil, ret, cfg_br_lt (hℓ' := by simp)]
   congr
-  simp only [List.singleton_append, List.length_singleton, Nat.zero_eq, Fin.zero_eta, Fin.isValue,
-    List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, List.append_eq, List.nil_append,
-    vwk_id_eq, let1_beta]
+  simp only [List.cons_append, List.nil_append, List.length_cons, List.length_nil, Nat.reduceAdd,
+    Nat.zero_eq, Fin.zero_eta, Fin.isValue, List.get_eq_getElem, Fin.val_zero,
+    List.getElem_cons_zero, List.append_eq, Fin.elim1_zero, vwk_id_eq, let1_beta]
   rw [lwk1_vwk1, seq, vsubst_lsubst, seq]
   congr
-  . rw [vsubst_alpha0]
+  · rw [vsubst_alpha0]
     rfl
-  . induction f using Quotient.inductionOn
+  · induction f using Quotient.inductionOn
     simp only [Term.Eqv.nil, var, subst0_quot, lwk1_quot, vwk1_quot, vsubst_quot]
     apply congrArg
     ext
@@ -80,7 +93,7 @@ theorem Eqv.fixpoint_iter_cfg {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 theorem Eqv.seq_cont {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::D::L))
   (h : Eqv φ (⟨C, ⊥⟩::Γ) (C::D::L))
-  : cfg [C] (f.lwk1 ;; g) (λ⟨0, _⟩ => h.vwk1) = f ;; cfg [C] g (λ⟨0, _⟩ => h.vwk1)
+  : cfg [C] (f.lwk1 ;; g) (Fin.elim1 h.vwk1) = f ;; cfg [C] g (Fin.elim1 h.vwk1)
   := sorry
 
 theorem Eqv.ret_var_zero_eq_nil_vwk1 {A : Ty α} {Γ : Ctx α ε} {L : LCtx α}
@@ -91,24 +104,23 @@ theorem Eqv.fixpoint_iter {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
   : fixpoint f = f ;; coprod nil (fixpoint f) := by
   apply Eq.trans f.fixpoint_iter_cfg
-  rw [lwk1_vwk1, <-vwk1_control]
-  simp only [<-vwk1_seq (left := f.lwk1) (right := control)]
+  rw [lwk1_vwk1, <-vwk1_left_exit]
+  simp only [<-vwk1_seq (left := f.lwk1) (right := left_exit)]
   rw [seq_cont]
   congr
   conv =>
     lhs
     lhs
-    rw [control]
+    rw [left_exit]
   rw [cfg_case, cfg_br_ge (ℓ := 1) (hℓ' := by simp)]
   simp only [List.length_singleton, Nat.sub_self, coprod]
   congr
   rw [fixpoint, vwk1_cfg]
   congr
   funext i
-  cases i using Fin.cases with
-  | zero =>
-    simp only [vwk1_seq, vwk1_control, vwk2_seq, vwk2_control, lwk1_vwk1, vwk1_vwk2]
-  | succ i => exact i.elim0
+  cases i using Fin.elim1 with
+  | zero => simp only [
+      Fin.elim1_zero, vwk1_seq, vwk1_left_exit, vwk2_seq, vwk2_left_exit, lwk1_vwk1, vwk1_vwk2]
 
 theorem Eqv.fixpoint_naturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))

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

@@ -76,8 +76,8 @@ theorem Eqv.rtimes_rtimes {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   apply congrArg
   rw [vwk1_seq, vwk1_seq, seq_assoc]
   congr 1
-  . simp [vwk1, vwk_vwk]
-  . sorry
+  · simp [vwk1, vwk_vwk]
+  · sorry
 
 theorem Eqv.vwk_lift_rtimes {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   {r : Eqv φ (⟨A, ⊥⟩::Δ) (B::L)} {ρ : Γ.InS Δ}

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -138,6 +138,13 @@ 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
 
+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)}
+  (hβ : β = ⟦β'⟧) (hG : ∀i, G i = ⟦G' i⟧)
+  : cfg R β G = ⟦InS.cfg R β' G'⟧ := by
+  rw [hβ, funext hG, cfg_quot]
+
 def Eqv.induction
   {motive : (Γ : Ctx α ε) → (L : LCtx α) → Eqv φ Γ L → Prop}
   (br : ∀{Γ L A} (ℓ) (a : Term.Eqv φ Γ ⟨A, ⊥⟩) (hℓ : L.Trg ℓ A), motive Γ L (Eqv.br ℓ a hℓ))

DeBruijnSSA/BinSyntax/Syntax.lean

@@ -301,12 +301,12 @@ theorem TRegion.IsTerminator.eq_cfg (k : ℕ) {r : TRegion φ} (h : r.IsTerminat
     simp only [toTerminator, tsub_zero, ↓reduceDIte, Terminator.lwk_id',
     cfg.injEq, heq_eq_eq, true_and]
     constructor
-    . simp only [Nat.sub_zero, Nat.not_lt_zero, ↓reduceDIte, Terminator.lsubst_id_apply',
+    · simp only [Nat.sub_zero, Nat.not_lt_zero, ↓reduceDIte, Terminator.lsubst_id_apply',
       Terminator.lwk_id']
       induction k with
       | zero => rfl
       | succ k I => rw [<-I]
-    . funext i; exact i.elim0
+    · funext i; exact i.elim0
 
 def Region.isBlock : Region φ → Bool
   | br _ _ => true
@@ -350,8 +350,8 @@ theorem TRegion.coe_toRegion_append_cfg (r : TRegion φ) (G' : TCFG φ)
     funext i
     simp only [Fin.addCases]
     split
-    . rfl
-    . simp only [Function.comp_apply, eq_rec_constant, TRegion.toRegion_lwk]
+    · rfl
+    · simp only [Function.comp_apply, eq_rec_constant, TRegion.toRegion_lwk]
   | _ => simp [Region.append_cfg, *]
 
 @[simp]
@@ -420,8 +420,8 @@ theorem TRegion.toRegion_toTerminator (r : TRegion φ) (k : ℕ)
     congr
     funext i
     split
-    . rw [I]
-    . rfl
+    · rw [I]
+    · rfl
 
 theorem Region.IsTerminator.toTRegion_eq_cfg (k : ℕ) {r : Region φ} (h : r.IsTerminator)
   : r.toTRegion = TRegion.cfg (r.toTerminator k) 0 Fin.elim0 := by

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -101,7 +101,8 @@ theorem lsubst_alpha_case (k) (e : Term φ) (s t r : Region φ)
   := by
   simp only [append_def, lsubst, vlift_alpha, vwk_vwk, vwk1, ← Nat.liftWk_comp]
 
-theorem case_append (e : Term φ) (s t r : Region φ) : case e s t ++ r = case e (s ++ r.vwk1) (t ++ r.vwk1)
+theorem case_append (e : Term φ) (s t r : Region φ)
+  : case e s t ++ r = case e (s ++ r.vwk1) (t ++ r.vwk1)
   := by simp only [append_def, lsubst, vlift_alpha, vwk_vwk, vwk1, ← Nat.liftWk_comp]
 
 theorem lsubst_alpha_cfg (β n G k) (r : Region φ)
@@ -158,6 +159,16 @@ theorem vsubst_lift_lsubst_alpha_vwk1 {r₀ r₁ : Region φ} {ρ : Term.Subst 
   | zero => rfl
   | succ k => simp [Term.Subst.comp, Term.subst_fromWk, Term.wk_wk, Term.Subst.liftn]
 
+theorem vwk_lift_append {r₀ r₁ : Region φ}
+  : (r₀ ++ r₁).vwk (Nat.liftWk ρ)
+  = r₀.vwk (Nat.liftWk ρ) ++ r₁.vwk (Nat.liftWk ρ) := by
+  simp only [append_def, vwk_liftWk_lsubst_alpha_vwk1]
+
+theorem vsubst_lift_append {r₀ r₁ : Region φ} {ρ : Term.Subst φ}
+  : (r₀ ++ r₁).vsubst ρ.lift
+  = r₀.vsubst ρ.lift ++ r₁.vsubst ρ.lift := by
+  simp only [append_def, vsubst_lift_lsubst_alpha_vwk1]
+
 -- def RewriteD.lsubst_alpha {r₀ r₀'}
 --   (p : RewriteD r₀ r₀') (n) (r₁ : Region φ)
 --   : RewriteD (r₀.lsubst (alpha n r₁)) (r₀'.lsubst (alpha n r₁)) := match p with
@@ -590,7 +601,27 @@ def right_exit : Region φ :=
     (br 0 (Term.var 0))
     (br 1 (Term.var 0))
 
-def fixpoint (r : Region φ) : Region φ := cfg nil 1 (λ_ => r.vwk1.lwk1 ++ left_exit)
+def fixpoint (r : Region φ) : Region φ := cfg nil 1 (Fin.elim1 (r.vwk1.lwk1 ++ left_exit))
+
+theorem vwk_lift_fixpoint (r : Region φ)
+  : r.fixpoint.vwk (Nat.liftWk ρ) = (r.vwk $ Nat.liftWk ρ).fixpoint := by
+  simp only [fixpoint, vwk]
+  congr
+  funext i
+  cases i using Fin.elim1 with
+  | zero =>
+    rw [Fin.elim1_zero, vwk_lift_append, vwk_lwk1, vwk_liftWk₂_vwk1]
+    rfl
+
+theorem vsubst_lift_fixpoint (r : Region φ) {ρ : Term.Subst φ}
+  : r.fixpoint.vsubst ρ.lift = (r.vsubst ρ.lift).fixpoint := by
+  simp only [fixpoint, vsubst]
+  congr
+  funext i
+  cases i using Fin.elim1 with
+  | zero =>
+    rw [Fin.elim1_zero, vsubst_lift_append, vsubst_lwk1, vsubst_lift₂_vwk1]
+    rfl
 
 def ite (b : Term φ) (r r' : Region φ) : Region φ := case b (r.vwk Nat.succ) (r'.vwk Nat.succ)
 

DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean

@@ -97,8 +97,8 @@ theorem Region.fvs_vsubst0_le (t : Region φ) (s : Term φ)
   : (t.vsubst s.subst0).fvs ⊆ s.fvs ∪ t.fvs.liftFv := by
   rw [fvs_vsubst0]
   split
-  . rw [Set.union_comm]
-  . simp
+  · rw [Set.union_comm]
+  · simp
 
 
 -- TODO: {Terminator, Region}.Subst.{fv, fl}

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

@@ -417,13 +417,13 @@ def RewriteD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : Rew
     apply cast_trg
     apply cfg_cfg
     congr
-    . rw [Nat.liftnWk_add]; rfl
-    . funext i
+    · 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]
+      · 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]