From 2691d497bff6f94f59f058c12ea550ada073de43 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 18 Oct 2024 19:57:06 +0200
Subject: [PATCH 1/7] represent verified implication Graph in Lean

---
 equational_theories/ImpGraphCorrect.lean | 142 +++++++++++++++++++++++
 1 file changed, 142 insertions(+)
 create mode 100644 equational_theories/ImpGraphCorrect.lean

diff --git a/equational_theories/ImpGraphCorrect.lean b/equational_theories/ImpGraphCorrect.lean
new file mode 100644
index 000000000..baeccd0e5
--- /dev/null
+++ b/equational_theories/ImpGraphCorrect.lean
@@ -0,0 +1,142 @@
+import equational_theories.Generated
+import equational_theories.Equations.LawsComplete
+
+namespace ImpGraph
+
+def Graph := Nat
+
+instance : OrOp Graph := inferInstanceAs (OrOp Nat)
+instance : AndOp Graph := inferInstanceAs (AndOp Nat)
+instance : BEq Graph := inferInstanceAs (BEq Nat)
+instance : Lean.ToExpr Graph := inferInstanceAs (Lean.ToExpr Nat)
+instance : DecidableEq Graph := inferInstanceAs (DecidableEq Nat)
+
+def Graph.singleton (i j : Fin 4694) : Graph :=
+  Nat.shiftLeft 1 (i.val * 4694 + j.val)
+
+def Graph.empty : Graph := (0 : Nat)
+
+def Graph.isEmpty (g : Graph) : Bool :=
+  g == .empty
+
+def Graph.get (g : Graph) (i j : Fin 4694) : Bool :=
+  -- Bool.not (Nat.beq (Nat.land g (Graph.singleton i j)) 0)
+  !(g &&& (Graph.singleton i j)).isEmpty
+
+theorem Nat_or_eq_zero (n m : Nat) : ((n ||| m) == 0) = (n == 0 && m == 0) := by
+  sorry
+
+@[simp] theorem Graph.union_get (g1 g2 : Graph) (i j : Fin 4694) :
+  (g1 ||| g2).get i j = (g1.get i j || g2.get i j) := by
+  simp [Graph, get, Graph.isEmpty, Graph.empty, Nat.and_distrib_right, Nat_or_eq_zero]
+
+def Graph.models (g : Graph) (P : (i j : Nat) → Prop) :=
+  ∀ i j, g.get i j → P i j
+
+@[simp]
+theorem Graph.empty_models (P : (i j : Nat) → Prop) : Graph.empty.models P :=
+  sorry
+
+@[simp]
+theorem Graph.singleton_models (P : (i j : Nat) → Prop) (i j : Fin 4694)  :
+    (Graph.singleton i j).models P ↔ P i j := by
+  simp [models, singleton, get]
+  sorry
+
+theorem Graph.union_models (g1 g2 : Graph) (P : (i j : Nat) → Prop) :
+    g1.models P → g2.models P → (g1 ||| g2).models P := by
+  simp [models]; tauto
+
+open Lean Elab in
+elab "defineImpGraph%" : term => do
+  let rs ← Result.extractTheorems
+  let rs := rs[:20] -- use this to speed up testing
+  let mut pairs := #[]
+  let mut graph : Graph := .empty
+  for r in rs do
+    if let .implication ⟨lhs, rhs⟩ := r.variant then
+      -- logInfo m!"{lhs} => {rhs}"
+      let some n1 := lhs.replace "Equation" "" |>.toNat? | throwError "Cannot parse {lhs}"
+      let some n2 := rhs.replace "Equation" "" |>.toNat? | throwError "Cannot parse {rhs}"
+      unless n1 ≤ 4694 do continue
+      unless n2 ≤ 4694 do continue
+      let i := n1-1
+      let j := n2-1
+      pairs := pairs.push (n1-1,n2-1)
+      graph := graph ||| .singleton i j
+
+  return mkNatLit graph
+
+def impGraph : Graph := defineImpGraph%
+
+/-- info: 2 -/
+#guard_msgs in
+#eval Nat.log2 impGraph / (8*1024*1024) -- size in MB
+
+/-- info: true -/
+#guard_msgs in
+#eval impGraph.get 591 590 -- Equation592 => Equation591
+
+def lawImplication (i j : Nat) := (laws[i].implies laws[j])
+
+inductive ImpEntries where
+  | empty
+  | node : ImpEntries → ImpEntries → ImpEntries
+  | leaf : (i j : Nat) → lawImplication i j → ImpEntries
+
+def ImpEntries.graph : ImpEntries → Graph
+  | .empty => .empty
+  | .node ie1 ie2 => ie1.graph ||| ie2.graph
+  | .leaf i j _ =>
+    if i < 4694 && j < 4694 then
+      .singleton i j
+    else
+      .empty
+
+open Lean Elab in
+elab "defineImpEntries%" : term => do
+  let rs ← Result.extractTheorems
+  let rs := rs[:20] -- use this to speed up testing
+  let mut entries : Array Expr := #[]
+  for r in rs do
+    if let .implication ⟨lhs, rhs⟩ := r.variant then
+      let some n1 := lhs.replace "Equation" "" |>.toNat? | throwError "Cannot parse {lhs}"
+      let some n2 := rhs.replace "Equation" "" |>.toNat? | throwError "Cannot parse {rhs}"
+      unless n1 ≤ 4694 do continue
+      unless n2 ≤ 4694 do continue
+      let i := n1-1
+      let j := n2-1
+      let lawThmName : Name := Name.mkSimple s!"Law{n1}_implies_Law{n2}"
+      entries := entries.push <|
+        mkApp3 (mkConst ``ImpEntries.leaf) (toExpr i) (toExpr j) (mkConst lawThmName)
+
+  let rec go (lb ub : Nat) (h1 : lb < ub) (h2 : ub ≤ entries.size) : Lean.Expr :=
+    if h : lb + 1 = ub then
+      entries[lb]
+    else
+      let mid := (lb + ub)/2
+      mkApp2 (mkConst ``ImpEntries.node)
+        (go lb mid (by omega) (by omega)) (go mid ub (by omega) h2)
+  if h : 0 < entries.size then
+    return go 0 entries.size h (Nat.le_refl _)
+  else
+    return mkConst ``ImpEntries.empty
+
+def impEntries : ImpEntries := defineImpEntries%
+
+theorem impGraph_from_impEntries : impGraph = impEntries.graph := by
+  native_decide
+
+
+theorem ImpEntries.graph_correct (ie : ImpEntries) : ie.graph.models lawImplication := by
+  induction ie using graph.induct
+  · simp [graph]
+  · simp [graph]
+    apply Graph.union_models <;> assumption
+  · simp_all [graph, Nat.mod_eq_of_lt]
+  · simp [graph, Nat.mod_eq_of_lt, *]
+
+
+theorem impGraph_correct : impGraph.models (fun i j => laws[i].implies laws[j]) := by
+  rw [impGraph_from_impEntries]
+  exact ImpEntries.graph_correct _

From 20365b862f32292ee651ac51164bac7a6fde5f2b Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 18 Oct 2024 20:00:42 +0200
Subject: [PATCH 2/7] Remove handbreaks

---
 equational_theories.lean                 | 1 +
 equational_theories/ImpGraphCorrect.lean | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/equational_theories.lean b/equational_theories.lean
index f092cd2cf..61569e123 100644
--- a/equational_theories.lean
+++ b/equational_theories.lean
@@ -24,3 +24,4 @@ import equational_theories.Confluence4
 import equational_theories.Conjectures
 import equational_theories.ManuallyProved
 import equational_theories.ThreeC2
+import equational_theories.ImpGraphCorrect
diff --git a/equational_theories/ImpGraphCorrect.lean b/equational_theories/ImpGraphCorrect.lean
index baeccd0e5..688a7c991 100644
--- a/equational_theories/ImpGraphCorrect.lean
+++ b/equational_theories/ImpGraphCorrect.lean
@@ -50,7 +50,7 @@ theorem Graph.union_models (g1 g2 : Graph) (P : (i j : Nat) → Prop) :
 open Lean Elab in
 elab "defineImpGraph%" : term => do
   let rs ← Result.extractTheorems
-  let rs := rs[:20] -- use this to speed up testing
+  -- let rs := rs[:20] -- use this to speed up testing
   let mut pairs := #[]
   let mut graph : Graph := .empty
   for r in rs do
@@ -96,7 +96,7 @@ def ImpEntries.graph : ImpEntries → Graph
 open Lean Elab in
 elab "defineImpEntries%" : term => do
   let rs ← Result.extractTheorems
-  let rs := rs[:20] -- use this to speed up testing
+  -- let rs := rs[:20] -- use this to speed up testing
   let mut entries : Array Expr := #[]
   for r in rs do
     if let .implication ⟨lhs, rhs⟩ := r.variant then

From 4a63a0dd1e15593de78b1c008d3b4ce5c09e2f3c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 18 Oct 2024 23:39:19 +0200
Subject: [PATCH 3/7] Add handbreaks again, runs far too slow it seems after
 all

---
 equational_theories/ImpGraphCorrect.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/equational_theories/ImpGraphCorrect.lean b/equational_theories/ImpGraphCorrect.lean
index 688a7c991..baeccd0e5 100644
--- a/equational_theories/ImpGraphCorrect.lean
+++ b/equational_theories/ImpGraphCorrect.lean
@@ -50,7 +50,7 @@ theorem Graph.union_models (g1 g2 : Graph) (P : (i j : Nat) → Prop) :
 open Lean Elab in
 elab "defineImpGraph%" : term => do
   let rs ← Result.extractTheorems
-  -- let rs := rs[:20] -- use this to speed up testing
+  let rs := rs[:20] -- use this to speed up testing
   let mut pairs := #[]
   let mut graph : Graph := .empty
   for r in rs do
@@ -96,7 +96,7 @@ def ImpEntries.graph : ImpEntries → Graph
 open Lean Elab in
 elab "defineImpEntries%" : term => do
   let rs ← Result.extractTheorems
-  -- let rs := rs[:20] -- use this to speed up testing
+  let rs := rs[:20] -- use this to speed up testing
   let mut entries : Array Expr := #[]
   for r in rs do
     if let .implication ⟨lhs, rhs⟩ := r.variant then

From d64aa82ee481878a6ef0c866d388a688e992c727 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 19 Oct 2024 12:53:20 +0200
Subject: [PATCH 4/7] Tweaks

---
 equational_theories/ImpGraphCorrect.lean | 27 +++++++++++++++++-------
 1 file changed, 19 insertions(+), 8 deletions(-)

diff --git a/equational_theories/ImpGraphCorrect.lean b/equational_theories/ImpGraphCorrect.lean
index baeccd0e5..d806f54c9 100644
--- a/equational_theories/ImpGraphCorrect.lean
+++ b/equational_theories/ImpGraphCorrect.lean
@@ -34,23 +34,33 @@ def Graph.models (g : Graph) (P : (i j : Nat) → Prop) :=
   ∀ i j, g.get i j → P i j
 
 @[simp]
-theorem Graph.empty_models (P : (i j : Nat) → Prop) : Graph.empty.models P :=
-  sorry
+theorem Graph.empty_isEmpty : Graph.empty.isEmpty := rfl
 
 @[simp]
-theorem Graph.singleton_models (P : (i j : Nat) → Prop) (i j : Fin 4694)  :
-    (Graph.singleton i j).models P ↔ P i j := by
-  simp [models, singleton, get]
+theorem Graph.empty_models (P : (i j : Nat) → Prop) : Graph.empty.models P := by
+  simp [Graph, models, empty, get, isEmpty]
+
+theorem Graph.singleton_and (i j i' j' : Fin 4694) :
+  (singleton i j &&& singleton i' j') = (if i = i' ∧ j = j' then singleton i j else empty) := by
   sorry
 
+theorem Graph.singleton_models (P : (i j : Nat) → Prop) (i j : Fin 4694) (h : P i j) :
+    (Graph.singleton i j).models P := by
+  intro i' j'
+  simp [Graph, models, get, empty]
+  rw [Graph.singleton_and]
+  split <;> simp_all
+
 theorem Graph.union_models (g1 g2 : Graph) (P : (i j : Nat) → Prop) :
     g1.models P → g2.models P → (g1 ||| g2).models P := by
   simp [models]; tauto
 
+/-- While developing, only look at the first n results. -/
+def handBreak : Nat := 20
+
 open Lean Elab in
 elab "defineImpGraph%" : term => do
   let rs ← Result.extractTheorems
-  let rs := rs[:20] -- use this to speed up testing
   let mut pairs := #[]
   let mut graph : Graph := .empty
   for r in rs do
@@ -64,6 +74,7 @@ elab "defineImpGraph%" : term => do
       let j := n2-1
       pairs := pairs.push (n1-1,n2-1)
       graph := graph ||| .singleton i j
+      if pairs.size = handBreak then break
 
   return mkNatLit graph
 
@@ -96,7 +107,6 @@ def ImpEntries.graph : ImpEntries → Graph
 open Lean Elab in
 elab "defineImpEntries%" : term => do
   let rs ← Result.extractTheorems
-  let rs := rs[:20] -- use this to speed up testing
   let mut entries : Array Expr := #[]
   for r in rs do
     if let .implication ⟨lhs, rhs⟩ := r.variant then
@@ -109,6 +119,7 @@ elab "defineImpEntries%" : term => do
       let lawThmName : Name := Name.mkSimple s!"Law{n1}_implies_Law{n2}"
       entries := entries.push <|
         mkApp3 (mkConst ``ImpEntries.leaf) (toExpr i) (toExpr j) (mkConst lawThmName)
+      if entries.size = handBreak then break
 
   let rec go (lb ub : Nat) (h1 : lb < ub) (h2 : ub ≤ entries.size) : Lean.Expr :=
     if h : lb + 1 = ub then
@@ -133,7 +144,7 @@ theorem ImpEntries.graph_correct (ie : ImpEntries) : ie.graph.models lawImplicat
   · simp [graph]
   · simp [graph]
     apply Graph.union_models <;> assumption
-  · simp_all [graph, Nat.mod_eq_of_lt]
+  · simp_all [graph, Nat.mod_eq_of_lt, Graph.singleton_models]
   · simp [graph, Nat.mod_eq_of_lt, *]
 
 

From ae4749b3819ebcaf967ecde57d16a5fc4348a6a6 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 19 Oct 2024 13:05:25 +0200
Subject: [PATCH 5/7] Remove some sorries

---
 equational_theories/ImpGraphCorrect.lean | 32 +++++++++++++++++++++---
 1 file changed, 29 insertions(+), 3 deletions(-)

diff --git a/equational_theories/ImpGraphCorrect.lean b/equational_theories/ImpGraphCorrect.lean
index d806f54c9..c93232924 100644
--- a/equational_theories/ImpGraphCorrect.lean
+++ b/equational_theories/ImpGraphCorrect.lean
@@ -24,7 +24,20 @@ def Graph.get (g : Graph) (i j : Fin 4694) : Bool :=
   !(g &&& (Graph.singleton i j)).isEmpty
 
 theorem Nat_or_eq_zero (n m : Nat) : ((n ||| m) == 0) = (n == 0 && m == 0) := by
-  sorry
+  apply Bool.coe_iff_coe.mp
+  simp
+  constructor
+  · intro h
+    constructor
+    · apply Nat.eq_of_testBit_eq
+      intro i
+      replace h : (n ||| m).testBit i = Nat.testBit 0 i := by simp [h]
+      simp_all
+    · apply Nat.eq_of_testBit_eq
+      intro i
+      replace h : (n ||| m).testBit i = Nat.testBit 0 i := by simp [h]
+      simp_all
+  · simp_all
 
 @[simp] theorem Graph.union_get (g1 g2 : Graph) (i j : Fin 4694) :
   (g1 ||| g2).get i j = (g1.get i j || g2.get i j) := by
@@ -40,9 +53,19 @@ theorem Graph.empty_isEmpty : Graph.empty.isEmpty := rfl
 theorem Graph.empty_models (P : (i j : Nat) → Prop) : Graph.empty.models P := by
   simp [Graph, models, empty, get, isEmpty]
 
+/-- `testBit 1 i` is false iff the index `i` does not equal 0. -/
+theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
+    Nat.testBit 1 i = false ↔ i ≠ 0 := by
+  rw [← Bool.bool_iff_false , Nat.testBit_one_eq_true_iff_self_eq_zero,]
+
 theorem Graph.singleton_and (i j i' j' : Fin 4694) :
-  (singleton i j &&& singleton i' j') = (if i = i' ∧ j = j' then singleton i j else empty) := by
-  sorry
+   (singleton i j &&& singleton i' j') = (if i = i' ∧ j = j' then singleton i j else empty) := by
+  apply Nat.eq_of_testBit_eq
+  intro b
+  split <;> simp_all [Graph, empty, singleton,
+    Nat.testBit_one_eq_true_iff_self_eq_zero, testBit_one_eq_true_iff_self_eq_zero]
+  omega
+
 
 theorem Graph.singleton_models (P : (i j : Nat) → Prop) (i j : Fin 4694) (h : P i j) :
     (Graph.singleton i j).models P := by
@@ -80,9 +103,11 @@ elab "defineImpGraph%" : term => do
 
 def impGraph : Graph := defineImpGraph%
 
+/-
 /-- info: 2 -/
 #guard_msgs in
 #eval Nat.log2 impGraph / (8*1024*1024) -- size in MB
+-/
 
 /-- info: true -/
 #guard_msgs in
@@ -135,6 +160,7 @@ elab "defineImpEntries%" : term => do
 
 def impEntries : ImpEntries := defineImpEntries%
 
+#time
 theorem impGraph_from_impEntries : impGraph = impEntries.graph := by
   native_decide
 

From dfda33f10fb4f4e9266169a3313ac65c9230848a Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 19 Oct 2024 13:13:21 +0200
Subject: [PATCH 6/7] Remove handbreak again, seems to work fine here

---
 equational_theories/ImpGraphCorrect.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/equational_theories/ImpGraphCorrect.lean b/equational_theories/ImpGraphCorrect.lean
index c93232924..4784dcd37 100644
--- a/equational_theories/ImpGraphCorrect.lean
+++ b/equational_theories/ImpGraphCorrect.lean
@@ -79,12 +79,12 @@ theorem Graph.union_models (g1 g2 : Graph) (P : (i j : Nat) → Prop) :
   simp [models]; tauto
 
 /-- While developing, only look at the first n results. -/
-def handBreak : Nat := 20
+def handBreak : Nat := 2000
 
 open Lean Elab in
 elab "defineImpGraph%" : term => do
   let rs ← Result.extractTheorems
-  let mut pairs := #[]
+  let mut n := 0
   let mut graph : Graph := .empty
   for r in rs do
     if let .implication ⟨lhs, rhs⟩ := r.variant then
@@ -95,12 +95,13 @@ elab "defineImpGraph%" : term => do
       unless n2 ≤ 4694 do continue
       let i := n1-1
       let j := n2-1
-      pairs := pairs.push (n1-1,n2-1)
+      n := n + 1
       graph := graph ||| .singleton i j
-      if pairs.size = handBreak then break
+      if n = handBreak then break
 
   return mkNatLit graph
 
+#time
 def impGraph : Graph := defineImpGraph%
 
 /-

From 0437ed433970828071e8662d831ce631feac9dd1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 19 Oct 2024 13:47:06 +0200
Subject: [PATCH 7/7] Put in handbreak until I have changed the data structure
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

as a single large bitvec doesn’t work well with lean yet.
---
 equational_theories/ImpGraphCorrect.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/equational_theories/ImpGraphCorrect.lean b/equational_theories/ImpGraphCorrect.lean
index 4784dcd37..021fc8aab 100644
--- a/equational_theories/ImpGraphCorrect.lean
+++ b/equational_theories/ImpGraphCorrect.lean
@@ -79,7 +79,7 @@ theorem Graph.union_models (g1 g2 : Graph) (P : (i j : Nat) → Prop) :
   simp [models]; tauto
 
 /-- While developing, only look at the first n results. -/
-def handBreak : Nat := 2000
+def handBreak : Nat := 20
 
 open Lean Elab in
 elab "defineImpGraph%" : term => do