Removed yet more rules

imbrem · Sep 11, 2024 · 00a3cce · 00a3cce
1 parent ba7a23c
commit 00a3cce
Show file tree

Hide file tree

Showing 6 changed files with 120 additions and 120 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
@@ -1198,10 +1198,10 @@ theorem Eqv.cfg_case {Γ : Ctx α ε} {L : LCtx α}
 --           (by rw [List.append_assoc])))
 --   := sorry
 
-theorem Eqv.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
-  (β : Eqv φ Γ L)
-  : β.cfg [] (λi => i.elim0) = β
-  := by induction β using Quotient.inductionOn with | h β => exact Eqv.sound $ β.cfg_zero
+-- theorem Eqv.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
+--   (β : Eqv φ Γ L)
+--   : β.cfg [] (λi => i.elim0) = β
+--   := by induction β using Quotient.inductionOn with | h β => exact Eqv.sound $ β.cfg_zero
 
 -- TODO: case_eta
 

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
@@ -343,51 +343,51 @@ theorem InS.cfg_case {Γ : Ctx α ε} {L : LCtx α}
     ≈ InS.case e (r.cfg R (λi => (G i).vwk1)) (s.cfg R (λi => (G i).vwk1))
   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
-theorem InS.cfg_cfg_eqv_cfg' {Γ : Ctx α ε} {L : LCtx α}
-  (R S : LCtx α) (β : InS φ Γ (R ++ (S ++ L)))
-  (G : (i : Fin R.length) → InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ (S ++ L)))
-  (G' : (i : Fin S.length) → InS φ (⟨S.get i, ⊥⟩::Γ) (S ++ L))
-    : (β.cfg R G).cfg S G'
-    ≈ (β.cast rfl (by rw [List.append_assoc])).cfg'
-      (R.length + S.length) (R ++ S) (by rw [List.length_append])
-      (Fin.addCases
-        (λi => (G i).cast (by
-          simp only [List.get_eq_getElem, Fin.cast, Fin.coe_castAdd]
-          rw [List.getElem_append]
-          -- TODO: put in discretion
-          ) (by rw [List.append_assoc]))
-        (λi => ((G' i).lwk (LCtx.InS.add_left_append (S ++ L) R)).cast (by
-          simp only [List.get_eq_getElem, Fin.cast, Fin.coe_natAdd]
-          rw [List.getElem_append_right]
-          simp
-          omega
-          omega
-          -- TODO: put in discretion
-        )
-          (by rw [List.append_assoc])))
-  := Uniform.rel $
-  TStep.rewrite InS.coe_wf InS.coe_wf (by
-    simp only [Set.mem_setOf_eq, coe_cfg, id_eq, coe_cfg', coe_cast]
-    apply Rewrite.cast_trg
-    apply Rewrite.cfg_cfg
-    congr
-    funext i
-    if h : i < R.length then
-      have hi : i = Fin.castAdd S.length ⟨i, h⟩ := rfl
-      rw [hi]
-      simp only [Fin.addCases_left]
-      rfl
-    else
-      let hi := Fin.natAdd_subNat_cast (le_of_not_lt h)
-      rw [<-hi]
-      simp only [Fin.addCases_right]
-      rfl
-    )
-
-theorem InS.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
-  (β : InS φ Γ L)
-  : β.cfg [] (λi => i.elim0) ≈ β
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
+-- theorem InS.cfg_cfg_eqv_cfg' {Γ : Ctx α ε} {L : LCtx α}
+--   (R S : LCtx α) (β : InS φ Γ (R ++ (S ++ L)))
+--   (G : (i : Fin R.length) → InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ (S ++ L)))
+--   (G' : (i : Fin S.length) → InS φ (⟨S.get i, ⊥⟩::Γ) (S ++ L))
+--     : (β.cfg R G).cfg S G'
+--     ≈ (β.cast rfl (by rw [List.append_assoc])).cfg'
+--       (R.length + S.length) (R ++ S) (by rw [List.length_append])
+--       (Fin.addCases
+--         (λi => (G i).cast (by
+--           simp only [List.get_eq_getElem, Fin.cast, Fin.coe_castAdd]
+--           rw [List.getElem_append]
+--           -- TODO: put in discretion
+--           ) (by rw [List.append_assoc]))
+--         (λi => ((G' i).lwk (LCtx.InS.add_left_append (S ++ L) R)).cast (by
+--           simp only [List.get_eq_getElem, Fin.cast, Fin.coe_natAdd]
+--           rw [List.getElem_append_right]
+--           simp
+--           omega
+--           omega
+--           -- TODO: put in discretion
+--         )
+--           (by rw [List.append_assoc])))
+--   := Uniform.rel $
+--   TStep.rewrite InS.coe_wf InS.coe_wf (by
+--     simp only [Set.mem_setOf_eq, coe_cfg, id_eq, coe_cfg', coe_cast]
+--     apply Rewrite.cast_trg
+--     apply Rewrite.cfg_cfg
+--     congr
+--     funext i
+--     if h : i < R.length then
+--       have hi : i = Fin.castAdd S.length ⟨i, h⟩ := rfl
+--       rw [hi]
+--       simp only [Fin.addCases_left]
+--       rfl
+--     else
+--       let hi := Fin.natAdd_subNat_cast (le_of_not_lt h)
+--       rw [<-hi]
+--       simp only [Fin.addCases_right]
+--       rfl
+--     )
+
+-- theorem InS.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
+--   (β : InS φ Γ L)
+--   : β.cfg [] (λi => i.elim0) ≈ β
+--   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let2_eta {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.InS φ Γ ⟨Ty.prod A B, ea⟩)

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean
@@ -143,26 +143,26 @@ def RWD.cfg_case_op {Γ : ℕ → ε} (e : Term φ) (r s n G)
     (cfg (case e r s) n G)
   := single $ BCongD.rel $ StepD.cfg_case_op e r s n G
 
-def RWD.cfg_cfg {Γ : ℕ → ε} (β : Region φ) (n G n' G')
-  : RWD StepD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
-  := single $ BCongD.rel $ StepD.cfg_cfg β n G n' G'
+-- def RWD.cfg_cfg {Γ : ℕ → ε} (β : Region φ) (n G n' G')
+--   : RWD StepD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
+--   := single $ BCongD.rel $ StepD.cfg_cfg β n G n' G'
 
-def RWD.cfg_cfg_op {Γ : ℕ → ε} (β : Region φ) (n G n' G')
-  : RWD StepD Γ (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
-    (cfg (cfg β n G) n' G')
-  := single $ BCongD.rel $ StepD.cfg_cfg_op β n G n' G'
+-- def RWD.cfg_cfg_op {Γ : ℕ → ε} (β : Region φ) (n G n' G')
+--   : RWD StepD Γ (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
+--     (cfg (cfg β n G) n' G')
+--   := single $ BCongD.rel $ StepD.cfg_cfg_op β n G n' G'
 
-def RWD.cfg_zero {Γ : ℕ → ε} (β : Region φ) (G)
-  : RWD StepD Γ (cfg β 0 G) β := single $ BCongD.rel $ StepD.cfg_zero β G
+-- def RWD.cfg_zero {Γ : ℕ → ε} (β : Region φ) (G)
+--   : RWD StepD Γ (cfg β 0 G) β := single $ BCongD.rel $ StepD.cfg_zero β G
 
-def RWD.cfg_zero_op {Γ : ℕ → ε} (β : Region φ) (G)
-  : RWD StepD Γ β (cfg β 0 G) := single $ BCongD.rel $ StepD.cfg_zero_op β G
+-- def RWD.cfg_zero_op {Γ : ℕ → ε} (β : Region φ) (G)
+--   : RWD StepD Γ β (cfg β 0 G) := single $ BCongD.rel $ StepD.cfg_zero_op β G
 
-def RWD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n) /-(hρ : Function.Bijective ρ)-/
-  : RWD StepD Γ
-    (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
-    (cfg β k (G ∘ ρ))
-  := single $ BCongD.rel $ StepD.wk_cfg β n G k ρ
+-- def RWD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n) /-(hρ : Function.Bijective ρ)-/
+--   : RWD StepD Γ
+--     (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
+--     (cfg β k (G ∘ ρ))
+--   := single $ BCongD.rel $ StepD.wk_cfg β n G k ρ
 
 -- def RWD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G')
 --   : RWD StepD Γ

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean
@@ -143,9 +143,9 @@ theorem eqv_cfg_case {e r s n G}
     ≈ case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
   := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_case e r s n G
 
-theorem eqv_cfg_cfg {β n G n' G'}
-  : @cfg φ (cfg β n G) n' G' ≈ cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G'))
-  := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_cfg β n G n' G'
+-- theorem eqv_cfg_cfg {β n G n' G'}
+--   : @cfg φ (cfg β n G) n' G' ≈ cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G'))
+--   := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_cfg β n G n' G'
 
 -- theorem eqv_cfg_fuse {β n G k} (ρ : Fin k → Fin n) (hρ : Function.Surjective ρ)
 --   : @cfg φ (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G)

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
@@ -55,9 +55,9 @@ inductive RewriteD : Region φ → Region φ → Type _
   | cfg_case (e r s n G) :
     RewriteD (cfg (case e r s) n G)
       (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
-  | cfg_cfg (β n G n' G') :
-    RewriteD (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
-  | cfg_zero (β G) : RewriteD (cfg β 0 G) β
+  -- | cfg_cfg (β n G n' G') :
+  --   RewriteD (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
+  -- | cfg_zero (β G) : RewriteD (cfg β 0 G) β
   -- | cfg_fuse (β n G k) (ρ : Fin k → Fin n) (hρ : Function.Surjective ρ) :
   --   RewriteD
   --     (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
@@ -232,9 +232,9 @@ inductive Rewrite : Region φ → Region φ → Prop
   | cfg_case (e r s n G) :
     Rewrite (cfg (case e r s) n G)
       (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
-  | cfg_cfg (β n G n' G') :
-    Rewrite (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
-  | cfg_zero (β G) : Rewrite (cfg β 0 G) β
+  -- | cfg_cfg (β n G n' G') :
+  --   Rewrite (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
+  -- | cfg_zero (β G) : Rewrite (cfg β 0 G) β
   -- | cfg_fuse (β n G k) (ρ : Fin k → Fin n) (hρ : Function.Surjective ρ) :
   --   Rewrite
   --     (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
@@ -407,17 +407,17 @@ def RewriteD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (p : RewriteD r r')
     simp only [BinSyntax.Region.vsubst, Function.comp_apply, vsubst_lift₂_vwk1, case.injEq,
       cfg.injEq, heq_eq_eq, true_and]
     constructor <;> rfl
-  | cfg_cfg β n G n' G' =>
-    convert (cfg_cfg (β.vsubst σ) n (λi => (G i).vsubst σ.lift) n' (λi => (G' i).vsubst σ.lift))
-      using 1
-    simp only [BinSyntax.Region.vsubst, Function.comp_apply, vsubst_lift₂_vwk1, cfg.injEq,
-      heq_eq_eq, true_and]
-    funext i
-    simp only [Fin.addCases, Function.comp_apply, eq_rec_constant]
-    split
-    · rfl
-    · simp [vsubst_lwk]
-  | cfg_zero _ G => exact (cfg_zero (r'.vsubst σ) (λi => (G i).vsubst σ.lift))
+  -- | cfg_cfg β n G n' G' =>
+  --   convert (cfg_cfg (β.vsubst σ) n (λi => (G i).vsubst σ.lift) n' (λi => (G' i).vsubst σ.lift))
+  --     using 1
+  --   simp only [BinSyntax.Region.vsubst, Function.comp_apply, vsubst_lift₂_vwk1, cfg.injEq,
+  --     heq_eq_eq, true_and]
+  --   funext i
+  --   simp only [Fin.addCases, Function.comp_apply, eq_rec_constant]
+  --   split
+  --   · rfl
+  --   · simp [vsubst_lwk]
+  -- | cfg_zero _ G => exact (cfg_zero (r'.vsubst σ) (λi => (G i).vsubst σ.lift))
   | let1_eta e r =>
     convert (let1_eta (e.subst σ) (r.vsubst σ.lift)) using 1
     simp [Term.subst, Region.vsubst_lift₂_vwk1]
@@ -518,26 +518,26 @@ def RewriteD.lsubst {r r' : Region φ} (σ : Subst φ) (p : RewriteD r r')
     constructor <;>
     funext i <;>
     simp [vwk1_lsubst_vlift]
-  | cfg_cfg β n G n' G' =>
-    convert (cfg_cfg (β.lsubst ((σ.liftn n').liftn n)) n
-      (λi => (G i).lsubst ((σ.liftn n').liftn n).vlift) n'
-      (λi => (G' i).lsubst (σ.liftn n').vlift)) using 1
-    simp only [BinSyntax.Region.lsubst, Function.comp_apply, let1.injEq, cfg.injEq, heq_eq_eq,
-      true_and, Subst.liftn_add]
-    funext i
-    simp only [Fin.addCases, Function.comp_apply, eq_rec_constant]
-    split; rfl
-    simp only [Subst.vlift, ← lsubst_fromLwk, lsubst_lsubst]
-    congr
-    funext k
-    simp only [Subst.comp, BinSyntax.Region.lsubst, Subst.vlift, Function.comp_apply, Subst.liftn,
-      add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right, vsubst0_var0_vwk1,
-      Subst.vwk1_comp_fromLwk, lsubst_fromLwk]
-    split; rfl
-    simp [vwk1_lwk]
-  | cfg_zero β G =>
-    convert (cfg_zero (r'.lsubst σ) (λi => (G i).lsubst σ.vlift)) using 1
-    simp
+  -- | cfg_cfg β n G n' G' =>
+  --   convert (cfg_cfg (β.lsubst ((σ.liftn n').liftn n)) n
+  --     (λi => (G i).lsubst ((σ.liftn n').liftn n).vlift) n'
+  --     (λi => (G' i).lsubst (σ.liftn n').vlift)) using 1
+  --   simp only [BinSyntax.Region.lsubst, Function.comp_apply, let1.injEq, cfg.injEq, heq_eq_eq,
+  --     true_and, Subst.liftn_add]
+  --   funext i
+  --   simp only [Fin.addCases, Function.comp_apply, eq_rec_constant]
+  --   split; rfl
+  --   simp only [Subst.vlift, ← lsubst_fromLwk, lsubst_lsubst]
+  --   congr
+  --   funext k
+  --   simp only [Subst.comp, BinSyntax.Region.lsubst, Subst.vlift, Function.comp_apply, Subst.liftn,
+  --     add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right, vsubst0_var0_vwk1,
+  --     Subst.vwk1_comp_fromLwk, lsubst_fromLwk]
+  --   split; rfl
+  --   simp [vwk1_lwk]
+  -- | cfg_zero β G =>
+  --   convert (cfg_zero (r'.lsubst σ) (λi => (G i).lsubst σ.vlift)) using 1
+  --   simp
   | let1_eta e r =>
     convert (let1_eta e (r.lsubst σ.vlift)) using 1
     simp [vwk1_lsubst_vlift]

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean
@@ -263,24 +263,24 @@ def StepD.cfg_case_op {Γ : ℕ → ε} (e : Term φ) (r s n G)
     (cfg (case e r s) n G)
   := StepD.rw_op $ RewriteD.cfg_case e r s n G
 
-@[match_pattern]
-def StepD.cfg_cfg {Γ : ℕ → ε} (β : Region φ) (n G n' G')
-  : StepD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
-  := StepD.rw $ RewriteD.cfg_cfg β n G n' G'
+-- @[match_pattern]
+-- def StepD.cfg_cfg {Γ : ℕ → ε} (β : Region φ) (n G n' G')
+--   : StepD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
+--   := StepD.rw $ RewriteD.cfg_cfg β n G n' G'
 
-@[match_pattern]
-def StepD.cfg_cfg_op {Γ : ℕ → ε} (β : Region φ) (n G n' G')
-  : StepD Γ (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
-    (cfg (cfg β n G) n' G')
-  := StepD.rw_op $ RewriteD.cfg_cfg β n G n' G'
+-- @[match_pattern]
+-- def StepD.cfg_cfg_op {Γ : ℕ → ε} (β : Region φ) (n G n' G')
+--   : StepD Γ (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
+--     (cfg (cfg β n G) n' G')
+--   := StepD.rw_op $ RewriteD.cfg_cfg β n G n' G'
 
-@[match_pattern]
-def StepD.cfg_zero {Γ : ℕ → ε} (β : Region φ) (G)
-  : StepD Γ (cfg β 0 G) β := StepD.rw $ RewriteD.cfg_zero β G
+-- @[match_pattern]
+-- def StepD.cfg_zero {Γ : ℕ → ε} (β : Region φ) (G)
+--   : StepD Γ (cfg β 0 G) β := StepD.rw $ RewriteD.cfg_zero β G
 
-@[match_pattern]
-def StepD.cfg_zero_op {Γ : ℕ → ε} (β : Region φ) (G)
-  : StepD Γ β (cfg β 0 G) := StepD.rw_op $ RewriteD.cfg_zero β G
+-- @[match_pattern]
+-- def StepD.cfg_zero_op {Γ : ℕ → ε} (β : Region φ) (G)
+--   : StepD Γ β (cfg β 0 G) := StepD.rw_op $ RewriteD.cfg_zero β G
 
 @[match_pattern]
 def StepD.let2_eta {Γ : ℕ → ε} (e) (r : Region φ)