From ec23c059d0b5b9a5353c9e2afd9b2c0d1b0851a2 Mon Sep 17 00:00:00 2001
From: cilinder <jure.taslak@gmail.com>
Date: Wed, 10 Apr 2024 18:47:43 -0400
Subject: [PATCH 1/4] start implementing Hamiltonian cycles via SAT

---
 LeanHoG/Invariant/HamiltonianCycle/Basic.lean |  45 +++++
 .../HamiltonianCycle/Certificate.lean         |  45 +++++
 .../Invariant/HamiltonianCycle/JsonData.lean  |  16 ++
 .../HamiltonianCycle/SatEncoding.lean         | 179 ++++++++++++++++++
 .../Invariant/HamiltonianCycle/Tactic.lean    | 123 ++++++++++++
 LeanHoG/Invariant/HamiltonianPath/Basic.lean  |  25 ---
 .../HamiltonianPath/Certificate.lean          |   2 +-
 .../HamiltonianPath/SatEncoding.lean          |   2 +
 8 files changed, 411 insertions(+), 26 deletions(-)
 create mode 100644 LeanHoG/Invariant/HamiltonianCycle/Basic.lean
 create mode 100644 LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
 create mode 100644 LeanHoG/Invariant/HamiltonianCycle/JsonData.lean
 create mode 100644 LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
 create mode 100644 LeanHoG/Invariant/HamiltonianCycle/Tactic.lean

diff --git a/LeanHoG/Invariant/HamiltonianCycle/Basic.lean b/LeanHoG/Invariant/HamiltonianCycle/Basic.lean
new file mode 100644
index 0000000..a76888b
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/Basic.lean
@@ -0,0 +1,45 @@
+
+import LeanHoG.Graph
+import LeanHoG.Walk
+
+namespace LeanHoG
+
+@[simp] def Cycle.isHamiltonian {g : Graph} {u : g.vertex} (c : Cycle g u) : Bool :=
+  ∀ (v : g.vertex), List.contains c.cycle.vertices v
+
+class HamiltonianCycle (g : Graph)  where
+  u : g.vertex
+  cycle : Cycle g u
+  isHamiltonian : cycle.isHamiltonian = true
+
+@[simp] def Graph.isHamiltonian (g : Graph) : Prop :=
+  ∃ (u : g.vertex) (c : Cycle g u), c.isHamiltonian
+
+@[simp] def Graph.isNonHamiltonian (g : Graph) : Prop := ¬ g.isHamiltonian
+
+@[simp] def Graph.isNonHamiltonian' {g : Graph} : Prop :=
+  ∀ (u : g.vertex) (c : Cycle g u), ¬c.isHamiltonian
+
+namespace HamiltonianCycle
+
+instance {g : Graph} : Repr (HamiltonianCycle g) where
+  reprPrec p n := reprPrec p.cycle n
+
+instance {g : Graph} : Repr (HamiltonianCycle g) where
+  reprPrec p n := reprPrec p.2.cycle n
+
+@[simp] theorem cycle_of_cert {g : Graph} [hp : HamiltonianCycle g] : g.isHamiltonian := by
+  let ⟨u, p, cond⟩ := hp
+  apply Exists.intro u
+  apply Exists.intro p
+  apply cond
+
+instance {G : Graph} [HamiltonianCycle G] : Decidable (G.isHamiltonian) :=
+  .isTrue cycle_of_cert
+
+theorem equivNonHamiltonianDefs (g : Graph) :
+  g.isNonHamiltonian ↔ g.isNonHamiltonian' :=
+  by simp
+
+end HamiltonianCycle
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean b/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
new file mode 100644
index 0000000..161508f
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
@@ -0,0 +1,45 @@
+import Qq
+import LeanHoG.Edge
+import LeanHoG.Graph
+import LeanHoG.Util.RB
+import LeanHoG.Util.Quote
+import LeanHoG.Invariant.HamiltonianCycle.Basic
+import LeanHoG.Invariant.HamiltonianCycle.JsonData
+
+namespace LeanHoG
+
+open Qq
+def hamiltonianCycleOfData (G : Q(Graph)) (D : HamiltonianCycleData) : Q(HamiltonianCycle $G) :=
+  -- Helper function to compute a Walk from a list of vertices
+  let rec fold (t : Q(Graph.vertex $G)) : List Q(Graph.vertex $G) →
+    ((s : Q(Graph.vertex $G)) ×' Q(Walk $G $s $t)) := fun vs =>
+    match vs with
+    | [] => panic! "given empty path, cannot construct Hamiltonian cycle"
+    | [v] =>
+      let h : Q($v = $t) := (q(Eq.refl $v) : Lean.Expr)
+      ⟨v, q($h ▸ .here $v)⟩
+    | u :: v :: vs =>
+      let ⟨s, w⟩ := fold t (v :: vs)
+      let h : Q(decide (@Graph.adjacent $G $u $s) = true) := (q(Eq.refl true) : Lean.Expr)
+      let w' := q(.step (of_decide_eq_true $h) $w)
+      ⟨u, w'⟩
+
+  have n : Q(Nat) := q(Graph.vertexSize $G)
+  let vertices : List Q(Graph.vertex $G) := D.cycle.map (finOfData n)
+  -- Construct the Hamiltonian cycle from the path
+  match vertices.getLast? with
+  | none => panic! "no vertices"
+  | some t =>
+    let ⟨s, w⟩ : ((s : Q(Graph.vertex $G)) ×' Q(Walk $G $s $t)) := fold t vertices
+    -- Check that w starts and end in the same vertex
+    let isClosed : Q($s = $t) := (q(Eq.refl true) : Lean.Expr)
+    -- Declare w to actually be a closed walk, we know this from above
+    let cw : Q(ClosedWalk $G $s) := w
+    -- Check that it is a cycle, i.e. no repeating vertices
+    sorry
+    -- let isCycle : Q(decide (ClosedWalk.isCycle $cw) = true) := (q(Eq.refl true) : Lean.Expr)
+    -- let c : Q(Cycle $G $s) := q(@Cycle.mk $G $s $cw (of_decide_eq_true $isCycle))
+    -- let isHamiltonian : Q(decide (Cycle.isHamiltonian $c) = true) := (q(Eq.refl true) : Lean.Expr)
+    -- let hc : Q(HamiltonianCycle $G) :=
+    --   q(@HamiltonianCycle.mk $G $s (Cycle.mk $cw (of_decide_eq_true (_))) (of_decide_eq_true $isHamiltonian))
+    -- hc
diff --git a/LeanHoG/Invariant/HamiltonianCycle/JsonData.lean b/LeanHoG/Invariant/HamiltonianCycle/JsonData.lean
new file mode 100644
index 0000000..5300bf3
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/JsonData.lean
@@ -0,0 +1,16 @@
+import Lean
+import LeanHoG.Graph
+
+namespace LeanHoG
+
+/--
+  JSON encoding of a Hamiltonian path.
+-/
+structure HamiltonianCycleData : Type where
+  /-- Hamiltonian cycle -/
+  cycle : List Nat
+
+deriving Lean.FromJson
+
+
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean b/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
new file mode 100644
index 0000000..8e81a84
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
@@ -0,0 +1,179 @@
+import LeanHoG.Graph
+import LeanHoG.Walk
+import LeanHoG.Invariant.ConnectedComponents.Basic
+import LeanHoG.Invariant.HamiltonianCycle.Basic
+import Lean
+
+import LeanSAT
+
+namespace LeanHoG
+namespace HamiltonianCycle
+
+open Lean LeanSAT Encode VEncCNF Meta Model PropFun
+
+/-- `Var i j = true` means: "at position j on the cycle is vertex i".
+-/
+structure Var (n : Nat) where
+  vertex : Fin n
+  pos : Fin n
+deriving DecidableEq, LeanColls.IndexType
+
+@[simp] def vertexAtPos {n : Nat} (i j : Fin n) : PropFun (Var n) :=
+  Var.mk i j
+
+@[simp] def positionHasAVertex {n : Nat} (j : Fin n) : PropPred (Var n) := fun τ =>
+  ∃ (i : Fin n), τ ⊨ vertexAtPos i j
+
+@[simp] def eachPositionHasAVertex {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (j : Fin n), positionHasAVertex j τ
+
+@[simp] def vertexIsAtSomePosition {n : Nat} (i : Fin n) : PropPred (Var n) := fun τ =>
+  ∃ (j : Fin n), τ ⊨ vertexAtPos i j
+
+@[simp] def eachVertexIsAtSomePosition {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (i : Fin n), vertexIsAtSomePosition i τ
+
+/-- The first and last position of the cycle should actually have the same vertex. -/
+@[simp] def vertexInAtMostOnePositionExceptEndpoints {n : Nat} (i : Fin n) : PropPred (Var n) := fun τ =>
+  ∀ (j k : Fin n), j ≠ k ∧ j < (n-1) ∧ k < (n-1) → τ ⊨ (vertexAtPos i j)ᶜ ⊔ (vertexAtPos i k)ᶜ
+
+/-- The first and last position of the cycle should actually have the same vertex. -/
+@[simp] def eachVertexInAtMostOnePositionExceptEndpoints {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (i : Fin n), vertexInAtMostOnePositionExceptEndpoints i τ
+
+@[simp] def atMostOneVertexAtPosition {n : Nat} (j : Fin n) : PropPred (Var n) := fun τ =>
+  ∀ (i k : Fin n), i ≠ k → τ ⊨ (vertexAtPos i j)ᶜ ⊔ (vertexAtPos k j)ᶜ
+
+@[simp] def atMostOneVertexInEachPosition {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (i : Fin n), atMostOneVertexAtPosition i τ
+
+/-- Encode that if two vertices are consecutive on the cycle, they are adjacent. -/
+@[simp] def nonAdjacentVerticesNotConsecutive {G : Graph} : PropPred (Var G.vertexSize) := fun τ =>
+  ∀ (k k': Fin G.vertexSize), k.val + 1 = k'.val →
+    ∀ (i j : Fin G.vertexSize), ¬G.adjacent i j →
+      (τ ⊨ ((vertexAtPos i k)ᶜ ⊔ (vertexAtPos j k')ᶜ))
+
+-- These constraints are just because of efficiency
+-- We declare that the starting and ending vertex must be vertex 0,
+-- since we know that the cycle must go through it anyway, we can do it
+-- without loss of generality.
+
+-- def cycleStartsAtVertex0 {G : Graph} : PropPred (Var G.vertexSize) := fun τ =>
+--   τ ⊨ (vertexAtPos 0 0)
+
+-- def cycleEndsAtVertex0 {G : Graph} : PropPred (Var G.vertexSize) := fun τ =>
+--   τ ⊨ (vertexAtPos 0 (G.vertexSize - 1))
+
+@[simp] def vertexConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> eachVertexIsAtSomePosition) ∧
+  (τ |> eachVertexInAtMostOnePositionExceptEndpoints)
+
+@[simp] def positionConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> eachPositionHasAVertex) ∧
+  (τ |> atMostOneVertexInEachPosition)
+
+@[simp] def edgeConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> nonAdjacentVerticesNotConsecutive)
+
+@[simp] def hamiltonianCycleConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> vertexConstraints G) ∧ (τ |> positionConstraints G) ∧ (τ |> edgeConstraints G)
+
+----------------------------------------------------------------------------------------
+-- Express the problem as a CNF
+
+open Encode VEncCNF LitVar
+
+abbrev VCnf (n : Nat) := VEncCNF (Var n) Unit
+
+@[simp] def verticesAtPosition {n : Nat} (j : Fin n) : List (Literal <| Var n) :=
+  List.finRange n |>.map (mkPos <| Var.mk · j)
+
+@[simp] def vertexAtPositions {n : Nat} (i : Fin n) : List (Literal <| Var n) :=
+  List.finRange n |>.map (mkPos <| Var.mk i ·)
+
+def vertexClauses (G : Graph) : VCnf G.vertexSize (vertexConstraints G) :=
+  (let U := Array.finRange G.vertexSize
+  seq[
+    for_all U fun i =>
+      addClause (List.toArray (vertexAtPositions i)),
+    for_all U fun i =>
+    for_all U fun j =>
+    for_all U fun k =>
+      VEncCNF.guard (j ≠ k ∧ j < (G.vertexSize-1) ∧ k < (G.vertexSize-1)) fun _ =>
+        addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk i k])
+  ])
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+    intro _
+    apply Iff.intro
+    intro h' i j k j_neq_k j_not_last k_not_last
+    have := h' i j k
+    simp [j_neq_k, j_not_last, k_not_last] at this
+    exact this
+    intro h' i j k
+    split
+    simp
+    next h'' => simp [h', h'']
+    simp_all only [Pi.top_apply, top]
+  )
+
+def positionClauses (G : Graph) : VCnf G.vertexSize (positionConstraints G) :=
+  (let U := Array.finRange G.vertexSize
+  seq[
+    for_all U fun j =>
+      addClause (List.toArray (verticesAtPosition j)),
+    for_all U fun j =>
+    for_all U fun i =>
+    for_all U fun k =>
+      VEncCNF.guard (i ≠ k) fun _ =>
+        addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk k j])
+  ])
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+    intro _
+    apply Iff.intro
+    intro h' i j k j_neq_k
+    have := h' i j k
+    simp [j_neq_k] at this
+    exact this
+    intro h' i j k
+    split
+    simp
+    next h'' => simp [h', h'']
+  )
+
+def edgeClauses (G : Graph) : VCnf G.vertexSize (edgeConstraints G) :=
+  ( let U := Array.finRange G.vertexSize
+    for_all U fun k =>
+    for_all U fun k' =>
+      VEncCNF.guard (k.val + 1 = k'.val) fun _ =>
+        for_all U fun i =>
+        for_all U fun j =>
+          VEncCNF.guard (¬G.adjacent i j) fun _ =>
+            addClause (#[mkNeg <| Var.mk i k, mkNeg <| Var.mk j k'])
+  )
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+    apply Iff.intro
+    intro h k k' h'' i j h'''
+    have := h k k'
+    simp [h''] at this
+    have := this i j
+    simp [h''] at this
+    rename_i this_1
+    simp_all only [↓reduceIte]
+    aesop
+  )
+
+def hamiltonianCycleCNF (G : Graph) : VCnf G.vertexSize (hamiltonianCycleConstraints G) :=
+  (seq[
+    vertexClauses G, positionClauses G, edgeClauses G
+  ])
+  |> mapProp (by aesop)
+
+
+end HamiltonianCycle
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
new file mode 100644
index 0000000..a268e91
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
@@ -0,0 +1,123 @@
+import Lean
+import Qq
+import LeanHoG.LoadGraph
+import LeanHoG.Invariant.HamiltonianCycle.SatEncoding
+import LeanHoG.Invariant.HamiltonianCycle.Certificate
+import LeanHoG.Tactic.Options
+import LeanHoG.Util.LeanSAT
+
+import LeanSAT
+
+namespace LeanHoG
+
+open HamiltonianCycle Lean Elab Qq
+
+open LeanSAT Model in
+unsafe def searchForHamiltonianCycleAux (graphName : Name) (graph : Q(Graph)) :
+  TermElabM (Expr × Expr × Solver.Res) := do
+  let G ← Meta.evalExpr' Graph ``Graph graph
+  let enc := (hamiltonianCycleCNF G).val
+  let opts ← getOptions
+  let cadicalExe := opts.get leanHoG.solverCmd.name leanHoG.solverCmd.defValue
+  let cake_lprExr := opts.get leanHoG.proofCheckerCmd.name leanHoG.proofCheckerCmd.defValue
+  let solver := SolverWithCakeLpr.SolverWithCakeLpr cadicalExe #["--no-binary", "--lrat=true"] cake_lprExr
+  let cnf := Encode.EncCNF.toICnf enc
+  let (_, s) := Encode.EncCNF.run enc
+  let res ← solver.solve cnf
+  match res with
+  | .sat assn =>
+    -- Build a Hamiltonian cycle from the solution given by the SAT solver
+    let mut cycle : Array Nat := Array.mkArray G.vertexSize 0
+    for i in List.fins G.vertexSize do
+      for j in List.fins G.vertexSize do
+        match assn.find? (s.vMap (Var.mk i j))  with
+        | none => throwError "invalid index ({i},{j})"
+        | some true => cycle := cycle.set! j i
+        | some false => continue
+    let hpQ := hamiltonianCycleOfData graph ⟨cycle.toList⟩
+    -- Add a Hamiltonian cycle instance from the constructed cycle
+    let hamiltonianCycleName := certificateName graphName "HamiltonianCycleI"
+    Lean.addAndCompile <| .defnDecl {
+      name := hamiltonianCycleName
+      levelParams := []
+      type := q(HamiltonianCycle $graph)
+      value := hpQ
+      hints := .regular 0
+      safety := .safe
+    }
+    Lean.Meta.addInstance hamiltonianCycleName .scoped 42
+    let existsHamCycle ← Meta.mkAppM ``LeanHoG.HamiltonianCycle.cycle_of_cert #[]
+    let existsType := q(Graph.isHamiltonian $graph)
+    return (existsType, existsHamCycle, res)
+
+  | .unsat =>
+    -- The formula is UNSAT, add an axiom saying so
+    throwError "non-Hamiltonicity not yet implemented"
+
+  | .error => throwError "SAT solver exited with error"
+
+
+------------------------------------------
+-- Find Hamiltonian cycle command
+------------------------------------------
+
+syntax (name := checkHamiltonian) "#check_hamiltonian " ident : command
+/-- `#check_hamiltonian G` runs a SAT solver on the encoding of the Hamiltonian cycle problem
+    on the graph `G` and if the SAT solver says the problem is unsat it runs the produced proof
+    through a verified proof checker cake_lpr. If the checker agrees with the proof, we add an axiom
+    saying there exists no satisfying assignmment for the encoding.
+-/
+@[command_elab checkHamiltonian]
+unsafe def checkHamiltonianImpl : Command.CommandElab
+  | `(#check_hamiltonian $g) => Command.liftTermElabM do
+    let graphName := g.getId
+    let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
+    let (declName, _, res) ← searchForHamiltonianCycleAux graphName graph
+    match res with
+    | .sat _ => logInfo m!"found Hamiltonian cycle {declName}"
+    | .unsat => logInfo m!"no Hamiltonian cycle found after exhaustive search"
+    | .error => throwError "SAT solver exited with error"
+
+  | _ => throwUnsupportedSyntax
+
+------------------------------------------
+-- Find Hamiltonian cycle tactic
+------------------------------------------
+-- TODO: Remove code duplication once I figure out how to do it corectly.
+
+syntax (name := checkHamiltonianTactic) "check_hamiltonian " ident (" with" (ppSpace colGt ident))? : tactic
+open LeanSAT Model in
+/-- `#check_hamiltonian G` runs a SAT solver on the encoding of the Hamiltonian cycle problem
+    on the graph `G` and if the SAT solver says the problem is unsatisfiable it runs the produced proof
+    through a verified proof checker cake_lpr. If the checker agrees with the proof, we add an axiom
+    saying there exists no satisfying assignmment for the encoding. The tactic uses the new axiom to
+    deduce that there is no Hamiltonian cycle in the graph by using theorem and adds it
+    as a hypothesis to the current context.
+
+    Can also use `#check_hamiltonian G with h` to save the hypothesis into the variable `h`.
+-/
+@[tactic checkHamiltonianTactic]
+unsafe def checkHamiltonianTacticImpl : Tactic.Tactic
+  | `(tactic|check_hamiltonian $g) =>
+    Tactic.withMainContext do
+      let graphName := g.getId
+      let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
+      let (val, type, _) ← searchForHamiltonianCycleAux graphName graph
+      Tactic.liftMetaTactic fun mvarId => do
+        let mvarIdNew ← mvarId.assert .anonymous val type
+        let (_, mvarIdNew) ← mvarIdNew.intro1P
+        return [mvarIdNew]
+
+  | `(tactic|check_hamiltonian $g with $ident) =>
+    Tactic.withMainContext do
+      let graphName := g.getId
+      let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
+      let (val, type, _) ← searchForHamiltonianCycleAux graphName graph
+      Tactic.liftMetaTactic fun mvarId => do
+        let mvarIdNew ← mvarId.assert ident.getId val type
+        let (_, mvarIdNew) ← mvarIdNew.intro1P
+        return [mvarIdNew]
+
+  | _ => throwUnsupportedSyntax
+
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianPath/Basic.lean b/LeanHoG/Invariant/HamiltonianPath/Basic.lean
index 3cc3e9e..215fde4 100644
--- a/LeanHoG/Invariant/HamiltonianPath/Basic.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/Basic.lean
@@ -106,30 +106,5 @@ example {α : Type} [DecidableEq α] (l : List α) (d : l.Nodup) : Finset.card (
 
 end HamiltonianPath
 
-@[simp] def Cycle.isHamiltonian {g : Graph} {u : g.vertex} (c : Cycle g u) : Bool :=
-  ∀ (v : g.vertex), List.contains c.cycle.vertices v
-
-class HamiltonianCycle (g : Graph)  where
-  u : g.vertex
-  cycle : Cycle g u
-  isHamiltonian : cycle.isHamiltonian = true
-
-instance {g : Graph} : Repr (HamiltonianCycle g) where
-  reprPrec p n := reprPrec p.cycle n
-
-instance {g : Graph} : Repr (HamiltonianCycle g) where
-  reprPrec p n := reprPrec p.2.cycle n
-
-@[simp] def Graph.isHamiltonian (g : Graph) : Prop :=
-  ∃ (u : g.vertex) (c : Cycle g u), c.isHamiltonian
-
-@[simp] def Graph.isNonHamiltonian (g : Graph) : Prop := ¬ g.isHamiltonian
-
-@[simp] def Graph.isNonHamiltonian' {g : Graph} : Prop :=
-  ∀ (u : g.vertex) (c : Cycle g u), ¬c.isHamiltonian
-
-theorem equivNonHamiltonianDefs (g : Graph) :
-  g.isNonHamiltonian ↔ g.isNonHamiltonian' :=
-  by simp
 
 end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianPath/Certificate.lean b/LeanHoG/Invariant/HamiltonianPath/Certificate.lean
index c4e2e7e..5fac11f 100644
--- a/LeanHoG/Invariant/HamiltonianPath/Certificate.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/Certificate.lean
@@ -13,7 +13,7 @@ def hamiltonianPathOfData (G : Q(Graph)) (D : HamiltonianPathData) : Q(Hamiltoni
   let rec fold (t : Q(Graph.vertex $G)) :
     List Q(Graph.vertex $G) → ((s : Q(Graph.vertex $G)) ×' Q(Walk $G $s $t)) := fun vs =>
     match vs with
-    | [] => panic! "Shouldn't be here"
+    | [] => panic! "given empty path, cannot construct Hamiltonian path"
     | [v] =>
       let h : Q($v = $t) := (q(Eq.refl $v) : Lean.Expr)
       ⟨v, q($h ▸ .here $v)⟩
diff --git a/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean b/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean
index d5980dd..03b88da 100644
--- a/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean
@@ -8,6 +8,7 @@ import Lean
 import LeanSAT
 
 namespace LeanHoG
+namespace HamiltonianPath
 
 open Lean LeanSAT Encode VEncCNF Meta Model PropFun
 
@@ -299,4 +300,5 @@ def tryFindHamiltonianPath [Solver IO] (G : Graph) :
     else
       return none
 
+end HamiltonianPath
 end LeanHoG

From eca26ccb2a7a722f91e7ea8447c728da5f01e16b Mon Sep 17 00:00:00 2001
From: cilinder <jure.taslak@gmail.com>
Date: Mon, 15 Apr 2024 11:18:09 -0400
Subject: [PATCH 2/4] Fix encoding of cycles, simplify tactic code, add ex

---
 Examples.lean                                 |  12 ++
 .../HamiltonianCycle/Certificate.lean         |  20 +--
 .../HamiltonianCycle/SatEncoding.lean         | 115 ++++++++++-------
 .../Invariant/HamiltonianCycle/Tactic.lean    | 120 +++++++++---------
 LeanHoG/Invariant/HamiltonianPath/Tactic.lean |   4 +-
 LeanHoG/Tactic/ParseExpr.lean                 |   1 +
 6 files changed, 149 insertions(+), 123 deletions(-)

diff --git a/Examples.lean b/Examples.lean
index b2763d8..9d57cd5 100644
--- a/Examples.lean
+++ b/Examples.lean
@@ -4,6 +4,7 @@ import LeanHoG.Widgets
 import LeanHoG.Tactic.SearchDSL
 import LeanHoG.Tactic.Basic
 import LeanHoG.Invariant.HamiltonianPath.Tactic
+import LeanHoG.Invariant.HamiltonianCycle.Tactic
 
 namespace LeanHoG
 
@@ -95,6 +96,17 @@ load_graph hog_896 "build/graphs/896.json"
 #check_traceable hog_896
 #show_hamiltonian_path hog_896
 
+-------------------------------------------
+-- Hamiltonian cycles
+-------------------------------------------
+-- NOTE: Non-Hamiltonicity not yet implemented
+
+#check_hamiltonian Cycle7
+
+theorem foo : Cycle7.isHamiltonian := by
+  check_hamiltonian Cycle7
+  decide
+
 ---------------------------------------
 -- Tactics
 ---------------------------------------
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean b/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
index 161508f..9c80b7b 100644
--- a/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
+++ b/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
@@ -32,14 +32,16 @@ def hamiltonianCycleOfData (G : Q(Graph)) (D : HamiltonianCycleData) : Q(Hamilto
   | some t =>
     let ⟨s, w⟩ : ((s : Q(Graph.vertex $G)) ×' Q(Walk $G $s $t)) := fold t vertices
     -- Check that w starts and end in the same vertex
-    let isClosed : Q($s = $t) := (q(Eq.refl true) : Lean.Expr)
+    -- Note: Have to use definitional equality instead of propositional
+    -- otherwise the types aren't correct.
+    have _isClosed : $s =Q $t := ⟨⟩
     -- Declare w to actually be a closed walk, we know this from above
-    let cw : Q(ClosedWalk $G $s) := w
+    have cw : Q(ClosedWalk $G $s) := w
+    have _eq : $cw =Q $w := ⟨⟩
     -- Check that it is a cycle, i.e. no repeating vertices
-    sorry
-    -- let isCycle : Q(decide (ClosedWalk.isCycle $cw) = true) := (q(Eq.refl true) : Lean.Expr)
-    -- let c : Q(Cycle $G $s) := q(@Cycle.mk $G $s $cw (of_decide_eq_true $isCycle))
-    -- let isHamiltonian : Q(decide (Cycle.isHamiltonian $c) = true) := (q(Eq.refl true) : Lean.Expr)
-    -- let hc : Q(HamiltonianCycle $G) :=
-    --   q(@HamiltonianCycle.mk $G $s (Cycle.mk $cw (of_decide_eq_true (_))) (of_decide_eq_true $isHamiltonian))
-    -- hc
+    have isCycle : Q(decide (ClosedWalk.isCycle $cw) = true) := (q(Eq.refl true) : Lean.Expr)
+    let c : Q(Cycle $G $s) := q(@Cycle.mk $G $s $cw (of_decide_eq_true ($isCycle)))
+    have isHamiltonian : Q(decide (Cycle.isHamiltonian $c) = true) := (q(Eq.refl true) : Lean.Expr)
+    have hc : Q(HamiltonianCycle $G) :=
+      q(@HamiltonianCycle.mk $G $s (Cycle.mk $cw (of_decide_eq_true ($isCycle))) (of_decide_eq_true $isHamiltonian))
+    hc
diff --git a/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean b/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
index 8e81a84..cb92dd3 100644
--- a/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
+++ b/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
@@ -15,41 +15,41 @@ open Lean LeanSAT Encode VEncCNF Meta Model PropFun
 -/
 structure Var (n : Nat) where
   vertex : Fin n
-  pos : Fin n
+  pos : Fin (n + 1)
 deriving DecidableEq, LeanColls.IndexType
 
-@[simp] def vertexAtPos {n : Nat} (i j : Fin n) : PropFun (Var n) :=
+@[simp] def vertexAtPos {n : Nat} (i : Fin n) (j : Fin (n+1)) : PropFun (Var n) :=
   Var.mk i j
 
-@[simp] def positionHasAVertex {n : Nat} (j : Fin n) : PropPred (Var n) := fun τ =>
+@[simp] def positionHasAVertex {n : Nat} (j : Fin (n+1)) : PropPred (Var n) := fun τ =>
   ∃ (i : Fin n), τ ⊨ vertexAtPos i j
 
 @[simp] def eachPositionHasAVertex {n : Nat} : PropPred (Var n) := fun τ =>
-  ∀ (j : Fin n), positionHasAVertex j τ
+  ∀ (j : Fin (n+1)), positionHasAVertex j τ
 
 @[simp] def vertexIsAtSomePosition {n : Nat} (i : Fin n) : PropPred (Var n) := fun τ =>
-  ∃ (j : Fin n), τ ⊨ vertexAtPos i j
+  ∃ (j : Fin (n+1)), τ ⊨ vertexAtPos i j
 
 @[simp] def eachVertexIsAtSomePosition {n : Nat} : PropPred (Var n) := fun τ =>
   ∀ (i : Fin n), vertexIsAtSomePosition i τ
 
 /-- The first and last position of the cycle should actually have the same vertex. -/
 @[simp] def vertexInAtMostOnePositionExceptEndpoints {n : Nat} (i : Fin n) : PropPred (Var n) := fun τ =>
-  ∀ (j k : Fin n), j ≠ k ∧ j < (n-1) ∧ k < (n-1) → τ ⊨ (vertexAtPos i j)ᶜ ⊔ (vertexAtPos i k)ᶜ
+  ∀ (j k : Fin (n+1)), j ≠ k ∧ j.val < n ∧ k.val < n → τ ⊨ (vertexAtPos i j)ᶜ ⊔ (vertexAtPos i k)ᶜ
 
 /-- The first and last position of the cycle should actually have the same vertex. -/
 @[simp] def eachVertexInAtMostOnePositionExceptEndpoints {n : Nat} : PropPred (Var n) := fun τ =>
   ∀ (i : Fin n), vertexInAtMostOnePositionExceptEndpoints i τ
 
-@[simp] def atMostOneVertexAtPosition {n : Nat} (j : Fin n) : PropPred (Var n) := fun τ =>
+@[simp] def atMostOneVertexAtPosition {n : Nat} (j : Fin (n+1)) : PropPred (Var n) := fun τ =>
   ∀ (i k : Fin n), i ≠ k → τ ⊨ (vertexAtPos i j)ᶜ ⊔ (vertexAtPos k j)ᶜ
 
 @[simp] def atMostOneVertexInEachPosition {n : Nat} : PropPred (Var n) := fun τ =>
-  ∀ (i : Fin n), atMostOneVertexAtPosition i τ
+  ∀ (j : Fin (n+1)), atMostOneVertexAtPosition j τ
 
 /-- Encode that if two vertices are consecutive on the cycle, they are adjacent. -/
 @[simp] def nonAdjacentVerticesNotConsecutive {G : Graph} : PropPred (Var G.vertexSize) := fun τ =>
-  ∀ (k k': Fin G.vertexSize), k.val + 1 = k'.val →
+  ∀ (k k': Fin (G.vertexSize+1)), k.val + 1 = k'.val →
     ∀ (i j : Fin G.vertexSize), ¬G.adjacent i j →
       (τ ⊨ ((vertexAtPos i k)ᶜ ⊔ (vertexAtPos j k')ᶜ))
 
@@ -58,11 +58,11 @@ deriving DecidableEq, LeanColls.IndexType
 -- since we know that the cycle must go through it anyway, we can do it
 -- without loss of generality.
 
--- def cycleStartsAtVertex0 {G : Graph} : PropPred (Var G.vertexSize) := fun τ =>
---   τ ⊨ (vertexAtPos 0 0)
+@[simp] def cycleStartsAtVertex0 (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  τ ⊨ (vertexAtPos ⟨0, h⟩ 0)
 
--- def cycleEndsAtVertex0 {G : Graph} : PropPred (Var G.vertexSize) := fun τ =>
---   τ ⊨ (vertexAtPos 0 (G.vertexSize - 1))
+@[simp] def cycleEndsAtVertex0 (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  τ ⊨ (vertexAtPos ⟨0, h⟩ G.vertexSize)
 
 @[simp] def vertexConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
   (τ |> eachVertexIsAtSomePosition) ∧
@@ -75,8 +75,11 @@ deriving DecidableEq, LeanColls.IndexType
 @[simp] def edgeConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
   (τ |> nonAdjacentVerticesNotConsecutive)
 
-@[simp] def hamiltonianCycleConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
-  (τ |> vertexConstraints G) ∧ (τ |> positionConstraints G) ∧ (τ |> edgeConstraints G)
+@[simp] def firstAndLastConstraints (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> cycleStartsAtVertex0 G h) ∧ (τ |> cycleEndsAtVertex0 G h)
+
+@[simp] def hamiltonianCycleConstraints (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> vertexConstraints G) ∧ (τ |> positionConstraints G) ∧ (τ |> edgeConstraints G) ∧ (τ |> firstAndLastConstraints G h)
 
 ----------------------------------------------------------------------------------------
 -- Express the problem as a CNF
@@ -85,49 +88,52 @@ open Encode VEncCNF LitVar
 
 abbrev VCnf (n : Nat) := VEncCNF (Var n) Unit
 
-@[simp] def verticesAtPosition {n : Nat} (j : Fin n) : List (Literal <| Var n) :=
+@[simp] def verticesAtPosition {n : Nat} (j : Fin (n+1)) : List (Literal <| Var n) :=
   List.finRange n |>.map (mkPos <| Var.mk · j)
 
 @[simp] def vertexAtPositions {n : Nat} (i : Fin n) : List (Literal <| Var n) :=
-  List.finRange n |>.map (mkPos <| Var.mk i ·)
+  List.finRange (n+1) |>.map (mkPos <| Var.mk i ·)
 
 def vertexClauses (G : Graph) : VCnf G.vertexSize (vertexConstraints G) :=
-  (let U := Array.finRange G.vertexSize
-  seq[
-    for_all U fun i =>
-      addClause (List.toArray (vertexAtPositions i)),
-    for_all U fun i =>
-    for_all U fun j =>
-    for_all U fun k =>
-      VEncCNF.guard (j ≠ k ∧ j < (G.vertexSize-1) ∧ k < (G.vertexSize-1)) fun _ =>
-        addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk i k])
+  ( let U := Array.finRange G.vertexSize
+    let V := Array.finRange (G.vertexSize+1)
+    seq[
+      for_all U fun i =>
+        addClause (List.toArray (vertexAtPositions i)),
+      for_all U fun i =>
+      for_all V fun j =>
+      for_all V fun k =>
+        VEncCNF.guard (j ≠ k ∧ j.val < (G.vertexSize) ∧ k.val < (G.vertexSize)) fun _ =>
+          addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk i k])
   ])
   |> mapProp (by
     ext τ
     simp [Clause.toPropFun]
     intro _
     apply Iff.intro
-    intro h' i j k j_neq_k j_not_last k_not_last
-    have := h' i j k
-    simp [j_neq_k, j_not_last, k_not_last] at this
-    exact this
+    intro h' i j k j_neq_k j_lt k_lt
+    have h'' := h' i j k
+    simp [j_neq_k, j_lt, k_lt] at h''
+    exact h''
     intro h' i j k
+    have := h' i j k
+    simp_all only [not_false_eq_true, implies_true]
     split
-    simp
-    next h'' => simp [h', h'']
-    simp_all only [Pi.top_apply, top]
+    · simp_all only [not_false_eq_true]
+    · simp_all only [not_and, not_lt, Pi.top_apply, top]
   )
 
 def positionClauses (G : Graph) : VCnf G.vertexSize (positionConstraints G) :=
-  (let U := Array.finRange G.vertexSize
-  seq[
-    for_all U fun j =>
-      addClause (List.toArray (verticesAtPosition j)),
-    for_all U fun j =>
-    for_all U fun i =>
-    for_all U fun k =>
-      VEncCNF.guard (i ≠ k) fun _ =>
-        addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk k j])
+  ( let U := Array.finRange G.vertexSize
+    let V := Array.finRange (G.vertexSize+1)
+    seq[
+      for_all V fun j =>
+        addClause (List.toArray (verticesAtPosition j)),
+      for_all V fun j =>
+      for_all U fun i =>
+      for_all U fun k =>
+        VEncCNF.guard (i ≠ k) fun _ =>
+          addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk k j])
   ])
   |> mapProp (by
     ext τ
@@ -138,16 +144,18 @@ def positionClauses (G : Graph) : VCnf G.vertexSize (positionConstraints G) :=
     have := h' i j k
     simp [j_neq_k] at this
     exact this
-    intro h' i j k
+    intro h' j i k
     split
     simp
-    next h'' => simp [h', h'']
+    have := h' j i k
+    next h'' => simp [h'', this]
   )
 
 def edgeClauses (G : Graph) : VCnf G.vertexSize (edgeConstraints G) :=
   ( let U := Array.finRange G.vertexSize
-    for_all U fun k =>
-    for_all U fun k' =>
+    let V := Array.finRange (G.vertexSize+1)
+    for_all V fun k =>
+    for_all V fun k' =>
       VEncCNF.guard (k.val + 1 = k'.val) fun _ =>
         for_all U fun i =>
         for_all U fun j =>
@@ -168,12 +176,21 @@ def edgeClauses (G : Graph) : VCnf G.vertexSize (edgeConstraints G) :=
     aesop
   )
 
-def hamiltonianCycleCNF (G : Graph) : VCnf G.vertexSize (hamiltonianCycleConstraints G) :=
+def firstAndLastVertexClauses (G : Graph) (h : 0 < G.vertexSize) : VCnf G.vertexSize (firstAndLastConstraints G h) :=
   (seq[
-    vertexClauses G, positionClauses G, edgeClauses G
+    addClause #[mkPos <| Var.mk ⟨0, h⟩ 0],
+    addClause #[mkPos <| Var.mk ⟨0, h⟩ G.vertexSize]
   ])
-  |> mapProp (by aesop)
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+  )
 
+def hamiltonianCycleCNF (G : Graph) (h : 0 < G.vertexSize) : VCnf G.vertexSize (hamiltonianCycleConstraints G h) :=
+  (seq[
+    vertexClauses G, positionClauses G, edgeClauses G, firstAndLastVertexClauses G h
+  ])
+  |> mapProp (by aesop)
 
 end HamiltonianCycle
 end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
index a268e91..9ae0403 100644
--- a/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
+++ b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
@@ -13,54 +13,68 @@ namespace LeanHoG
 open HamiltonianCycle Lean Elab Qq
 
 open LeanSAT Model in
-unsafe def searchForHamiltonianCycleAux (graphName : Name) (graph : Q(Graph)) :
-  TermElabM (Expr × Expr × Solver.Res) := do
+unsafe def searchForHamiltonianCycleAux (graph : Q(Graph)) :
+  TermElabM (Option Expr) := do
   let G ← Meta.evalExpr' Graph ``Graph graph
-  let enc := (hamiltonianCycleCNF G).val
-  let opts ← getOptions
-  let cadicalExe := opts.get leanHoG.solverCmd.name leanHoG.solverCmd.defValue
-  let cake_lprExr := opts.get leanHoG.proofCheckerCmd.name leanHoG.proofCheckerCmd.defValue
-  let solver := SolverWithCakeLpr.SolverWithCakeLpr cadicalExe #["--no-binary", "--lrat=true"] cake_lprExr
-  let cnf := Encode.EncCNF.toICnf enc
-  let (_, s) := Encode.EncCNF.run enc
-  let res ← solver.solve cnf
-  match res with
-  | .sat assn =>
-    -- Build a Hamiltonian cycle from the solution given by the SAT solver
-    let mut cycle : Array Nat := Array.mkArray G.vertexSize 0
-    for i in List.fins G.vertexSize do
-      for j in List.fins G.vertexSize do
-        match assn.find? (s.vMap (Var.mk i j))  with
-        | none => throwError "invalid index ({i},{j})"
-        | some true => cycle := cycle.set! j i
-        | some false => continue
-    let hpQ := hamiltonianCycleOfData graph ⟨cycle.toList⟩
-    -- Add a Hamiltonian cycle instance from the constructed cycle
-    let hamiltonianCycleName := certificateName graphName "HamiltonianCycleI"
-    Lean.addAndCompile <| .defnDecl {
-      name := hamiltonianCycleName
-      levelParams := []
-      type := q(HamiltonianCycle $graph)
-      value := hpQ
-      hints := .regular 0
-      safety := .safe
-    }
-    Lean.Meta.addInstance hamiltonianCycleName .scoped 42
-    let existsHamCycle ← Meta.mkAppM ``LeanHoG.HamiltonianCycle.cycle_of_cert #[]
-    let existsType := q(Graph.isHamiltonian $graph)
-    return (existsType, existsHamCycle, res)
-
-  | .unsat =>
-    -- The formula is UNSAT, add an axiom saying so
-    throwError "non-Hamiltonicity not yet implemented"
-
-  | .error => throwError "SAT solver exited with error"
+  if h : 0 < G.vertexSize then
+    let enc := (hamiltonianCycleCNF G h).val
+    let opts ← getOptions
+    let solverExe := opts.get leanHoG.solverCmd.name leanHoG.solverCmd.defValue
+    let checkerExe := opts.get leanHoG.proofCheckerCmd.name leanHoG.proofCheckerCmd.defValue
+    let solver := SolverWithCakeLpr.SolverWithCakeLpr solverExe #["--no-binary", "--lrat=true"] checkerExe
+    let cnf := Encode.EncCNF.toICnf enc
+    let (_, s) := Encode.EncCNF.run enc
+    let res ← solver.solve cnf
+    match res with
+    | .sat assn =>
+      -- Build a Hamiltonian cycle from the solution given by the SAT solver
+      let mut cycle : Array Nat := Array.mkArray (G.vertexSize+1) 0
+      for i in List.fins G.vertexSize do
+        for j in List.fins (G.vertexSize+1) do
+          match assn.find? (s.vMap (Var.mk i j))  with
+          | none => throwError "invalid index ({i},{j})"
+          | some true => cycle := cycle.set! j i
+          | some false => continue
+      let hpQ := hamiltonianCycleOfData graph ⟨cycle.toList⟩
+      IO.println s!"{cycle}"
+      return some hpQ
+    | .unsat =>
+      -- TODO: Not yet implemented
+      return none
+    | .error => throwError "SAT solver exited with error"
+  else
+    throwError "cannot construct Hamiltonian cycle for empty graph"
 
 
 ------------------------------------------
 -- Find Hamiltonian cycle command
 ------------------------------------------
 
+unsafe def checkHamiltonianCycleAux (graphName : Name) (graph : Q(Graph)) : TermElabM Unit := do
+  -- Check if there already exists an instance of a Hamiltonian cycle for g
+  let inst ← Qq.trySynthInstanceQ q(HamiltonianCycle $graph)
+  match inst with
+  | .some _ =>
+    logInfo "Hamiltonian cycle found"
+    pure ()
+  | _ =>
+    let hpQOpt ← searchForHamiltonianCycleAux graph
+    match hpQOpt with
+    | some hpQ =>
+      let hamiltonianCycleName := certificateName graphName "HamiltonianCycleI"
+      Lean.addAndCompile <| .defnDecl {
+        name := hamiltonianCycleName
+        levelParams := []
+        type := q(HamiltonianCycle $graph)
+        value := hpQ
+        hints := .regular 0
+        safety := .safe
+      }
+      Lean.Meta.addInstance hamiltonianCycleName .scoped 42
+      logInfo "Hamiltonian cycle found"
+    | none =>
+      logWarning s!"Hamiltonian cycle not found after exhaustive search"
+
 syntax (name := checkHamiltonian) "#check_hamiltonian " ident : command
 /-- `#check_hamiltonian G` runs a SAT solver on the encoding of the Hamiltonian cycle problem
     on the graph `G` and if the SAT solver says the problem is unsat it runs the produced proof
@@ -72,11 +86,7 @@ unsafe def checkHamiltonianImpl : Command.CommandElab
   | `(#check_hamiltonian $g) => Command.liftTermElabM do
     let graphName := g.getId
     let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-    let (declName, _, res) ← searchForHamiltonianCycleAux graphName graph
-    match res with
-    | .sat _ => logInfo m!"found Hamiltonian cycle {declName}"
-    | .unsat => logInfo m!"no Hamiltonian cycle found after exhaustive search"
-    | .error => throwError "SAT solver exited with error"
+    checkHamiltonianCycleAux graphName graph
 
   | _ => throwUnsupportedSyntax
 
@@ -93,8 +103,6 @@ open LeanSAT Model in
     saying there exists no satisfying assignmment for the encoding. The tactic uses the new axiom to
     deduce that there is no Hamiltonian cycle in the graph by using theorem and adds it
     as a hypothesis to the current context.
-
-    Can also use `#check_hamiltonian G with h` to save the hypothesis into the variable `h`.
 -/
 @[tactic checkHamiltonianTactic]
 unsafe def checkHamiltonianTacticImpl : Tactic.Tactic
@@ -102,21 +110,7 @@ unsafe def checkHamiltonianTacticImpl : Tactic.Tactic
     Tactic.withMainContext do
       let graphName := g.getId
       let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-      let (val, type, _) ← searchForHamiltonianCycleAux graphName graph
-      Tactic.liftMetaTactic fun mvarId => do
-        let mvarIdNew ← mvarId.assert .anonymous val type
-        let (_, mvarIdNew) ← mvarIdNew.intro1P
-        return [mvarIdNew]
-
-  | `(tactic|check_hamiltonian $g with $ident) =>
-    Tactic.withMainContext do
-      let graphName := g.getId
-      let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-      let (val, type, _) ← searchForHamiltonianCycleAux graphName graph
-      Tactic.liftMetaTactic fun mvarId => do
-        let mvarIdNew ← mvarId.assert ident.getId val type
-        let (_, mvarIdNew) ← mvarIdNew.intro1P
-        return [mvarIdNew]
+      checkHamiltonianCycleAux graphName graph
 
   | _ => throwUnsupportedSyntax
 
diff --git a/LeanHoG/Invariant/HamiltonianPath/Tactic.lean b/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
index c36292e..1d23441 100644
--- a/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
@@ -11,7 +11,7 @@ namespace LeanHoG
 
 open Lean Elab Qq
 
-open LeanSAT Model in
+open LeanSAT Model HamiltonianPath in
 unsafe def searchForHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) :
   TermElabM (Expr × Expr × Solver.Res) := do
   let G ← Meta.evalExpr' Graph ``Graph graph
@@ -64,7 +64,7 @@ unsafe def searchForHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) :
     addDecl decl
     logWarning m!"added axiom {declName} : {type}"
     let noExistsCert ← Qq.elabTermEnsuringTypeQ (mkIdent declName) type
-    let noExistsHamPath ← Meta.mkAppM ``LeanHoG.no_assignment_implies_no_hamiltonian_path' #[noExistsCert]
+    let noExistsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.no_assignment_implies_no_hamiltonian_path' #[noExistsCert]
     let noExistsType := q(¬ ∃ (u v : Graph.vertex $graph) (p : Path $graph u v), p.isHamiltonian)
     return (noExistsType, noExistsHamPath, res)
 
diff --git a/LeanHoG/Tactic/ParseExpr.lean b/LeanHoG/Tactic/ParseExpr.lean
index 36049c0..9447093 100644
--- a/LeanHoG/Tactic/ParseExpr.lean
+++ b/LeanHoG/Tactic/ParseExpr.lean
@@ -3,6 +3,7 @@ import LeanHoG.Graph
 import LeanHoG.Tactic.SearchDSL
 import LeanHoG.Tactic.Options
 import LeanHoG.Invariant.HamiltonianPath.Basic
+import LeanHoG.Invariant.HamiltonianCycle.Basic
 import Qq
 
 import Aesop.Util.Basic

From a9564e6069d56e1397c89b6a5c9bb8ece3d688d4 Mon Sep 17 00:00:00 2001
From: cilinder <jure.taslak@gmail.com>
Date: Mon, 15 Apr 2024 14:12:34 -0400
Subject: [PATCH 3/4] Add Hamiltonian cycle search to `find_example`

---
 Examples.lean                                 |   2 +-
 LeanHoG/Invariant/HamiltonianCycle/Basic.lean |   4 +-
 .../Invariant/HamiltonianCycle/Tactic.lean    |  30 ++++-
 LeanHoG/Invariant/HamiltonianPath/Tactic.lean | 119 ++++++++++--------
 LeanHoG/Tactic/Basic.lean                     |  42 ++-----
 LeanHoG/Tactic/SearchDSL.lean                 |  15 ++-
 6 files changed, 117 insertions(+), 95 deletions(-)

diff --git a/Examples.lean b/Examples.lean
index 9d57cd5..8b94678 100644
--- a/Examples.lean
+++ b/Examples.lean
@@ -125,7 +125,7 @@ theorem foo : Cycle7.isHamiltonian := by
 
 -- set_option leanHoG.solverCmd "cadical"
 -- set_option leanHoG.proofCheckerCmd "cake_lpr"
-example : ∃ (G : Graph), G.traceable ∧ G.vertexSize > 3 ∧ (G.minimumDegree < G.vertexSize / 2) := by
+example : ∃ (G : Graph), G.isHamiltonian ∧ G.vertexSize > 3 ∧ (G.minimumDegree < G.vertexSize / 2) := by
   find_example
 
 end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Basic.lean b/LeanHoG/Invariant/HamiltonianCycle/Basic.lean
index a76888b..25a81aa 100644
--- a/LeanHoG/Invariant/HamiltonianCycle/Basic.lean
+++ b/LeanHoG/Invariant/HamiltonianCycle/Basic.lean
@@ -12,7 +12,7 @@ class HamiltonianCycle (g : Graph)  where
   cycle : Cycle g u
   isHamiltonian : cycle.isHamiltonian = true
 
-@[simp] def Graph.isHamiltonian (g : Graph) : Prop :=
+def Graph.isHamiltonian (g : Graph) : Prop :=
   ∃ (u : g.vertex) (c : Cycle g u), c.isHamiltonian
 
 @[simp] def Graph.isNonHamiltonian (g : Graph) : Prop := ¬ g.isHamiltonian
@@ -39,7 +39,7 @@ instance {G : Graph} [HamiltonianCycle G] : Decidable (G.isHamiltonian) :=
 
 theorem equivNonHamiltonianDefs (g : Graph) :
   g.isNonHamiltonian ↔ g.isNonHamiltonian' :=
-  by simp
+  by simp [Graph.isHamiltonian]
 
 end HamiltonianCycle
 end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
index 9ae0403..31dcf5d 100644
--- a/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
+++ b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
@@ -36,7 +36,6 @@ unsafe def searchForHamiltonianCycleAux (graph : Q(Graph)) :
           | some true => cycle := cycle.set! j i
           | some false => continue
       let hpQ := hamiltonianCycleOfData graph ⟨cycle.toList⟩
-      IO.println s!"{cycle}"
       return some hpQ
     | .unsat =>
       -- TODO: Not yet implemented
@@ -50,13 +49,13 @@ unsafe def searchForHamiltonianCycleAux (graph : Q(Graph)) :
 -- Find Hamiltonian cycle command
 ------------------------------------------
 
-unsafe def checkHamiltonianCycleAux (graphName : Name) (graph : Q(Graph)) : TermElabM Unit := do
+unsafe def checkHamiltonianCycleAux (graphName : Name) (graph : Q(Graph)) : TermElabM Bool := do
   -- Check if there already exists an instance of a Hamiltonian cycle for g
   let inst ← Qq.trySynthInstanceQ q(HamiltonianCycle $graph)
   match inst with
   | .some _ =>
     logInfo "Hamiltonian cycle found"
-    pure ()
+    return true
   | _ =>
     let hpQOpt ← searchForHamiltonianCycleAux graph
     match hpQOpt with
@@ -72,8 +71,10 @@ unsafe def checkHamiltonianCycleAux (graphName : Name) (graph : Q(Graph)) : Term
       }
       Lean.Meta.addInstance hamiltonianCycleName .scoped 42
       logInfo "Hamiltonian cycle found"
+      return true
     | none =>
       logWarning s!"Hamiltonian cycle not found after exhaustive search"
+      return false
 
 syntax (name := checkHamiltonian) "#check_hamiltonian " ident : command
 /-- `#check_hamiltonian G` runs a SAT solver on the encoding of the Hamiltonian cycle problem
@@ -86,7 +87,7 @@ unsafe def checkHamiltonianImpl : Command.CommandElab
   | `(#check_hamiltonian $g) => Command.liftTermElabM do
     let graphName := g.getId
     let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-    checkHamiltonianCycleAux graphName graph
+    let _ ← checkHamiltonianCycleAux graphName graph
 
   | _ => throwUnsupportedSyntax
 
@@ -95,6 +96,19 @@ unsafe def checkHamiltonianImpl : Command.CommandElab
 ------------------------------------------
 -- TODO: Remove code duplication once I figure out how to do it corectly.
 
+unsafe def checkHamiltonianTacticAux (graphName : Name) (graph : Q(Graph)) (hypName : Name) :
+  Tactic.TacticM Unit := do
+  let isHamiltonian ← checkHamiltonianCycleAux graphName graph
+  if isHamiltonian then
+    let existsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.path_of_cert #[]
+    let existsType := q(Graph.traceable $graph)
+    Tactic.liftMetaTactic fun mvarId => do
+      let mvarIdNew ← mvarId.assert hypName existsHamPath existsType
+      let (_, mvarIdNew) ← mvarIdNew.intro1P
+      return [mvarIdNew]
+  else
+    throwError "cannot prove non-Hamiltonicity, not implemented!"
+
 syntax (name := checkHamiltonianTactic) "check_hamiltonian " ident (" with" (ppSpace colGt ident))? : tactic
 open LeanSAT Model in
 /-- `#check_hamiltonian G` runs a SAT solver on the encoding of the Hamiltonian cycle problem
@@ -110,7 +124,13 @@ unsafe def checkHamiltonianTacticImpl : Tactic.Tactic
     Tactic.withMainContext do
       let graphName := g.getId
       let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-      checkHamiltonianCycleAux graphName graph
+      checkHamiltonianTacticAux graphName graph .anonymous
+
+  | `(tactic|check_hamiltonian $g with $h) =>
+    Tactic.withMainContext do
+      let graphName := g.getId
+      let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
+      checkHamiltonianTacticAux graphName graph h.getId
 
   | _ => throwUnsupportedSyntax
 
diff --git a/LeanHoG/Invariant/HamiltonianPath/Tactic.lean b/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
index 1d23441..8457a10 100644
--- a/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
@@ -12,8 +12,8 @@ namespace LeanHoG
 open Lean Elab Qq
 
 open LeanSAT Model HamiltonianPath in
-unsafe def searchForHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) :
-  TermElabM (Expr × Expr × Solver.Res) := do
+unsafe def searchForHamiltonianPathAux (graph : Q(Graph)) :
+  TermElabM (Option Expr) := do
   let G ← Meta.evalExpr' Graph ``Graph graph
   let enc := (hamiltonianPathCNF G).val
   let opts ← getOptions
@@ -34,42 +34,51 @@ unsafe def searchForHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) :
         | some true => path := path.set! j i
         | some false => continue
     let hpQ := hamiltonianPathOfData graph ⟨path.toList⟩
-    -- Add a Hamiltonian path instance from the constructed path
-    let hamiltonianPathName := certificateName graphName "HamiltonianPathI"
-    Lean.addAndCompile <| .defnDecl {
-      name := hamiltonianPathName
-      levelParams := []
-      type := q(HamiltonianPath $graph)
-      value := hpQ
-      hints := .regular 0
-      safety := .safe
-    }
-    Lean.Meta.addInstance hamiltonianPathName .scoped 42
-    let existsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.path_of_cert #[]
-    let existsType := q(Graph.traceable $graph)
-    return (existsType, existsHamPath, res)
+    return hpQ
 
-  | .unsat =>
-    -- The formula is UNSAT, add an axiom saying so
-    let declName : Name := .str graphName "noHamiltonianPathCertificateExists"
-    let type : Q(Prop) := q(¬ (∃ (τ : PropAssignment (Var (Graph.vertexSize $graph))), τ |> hamiltonianPathConstraints $graph))
-    let decl := Declaration.axiomDecl {
-      name        := declName,
-      levelParams := [],
-      type        := type,
-      isUnsafe    := false
-    }
-    trace[Elab.axiom] "{declName} : {type}"
-    Term.ensureNoUnassignedMVars decl
-    addDecl decl
-    logWarning m!"added axiom {declName} : {type}"
-    let noExistsCert ← Qq.elabTermEnsuringTypeQ (mkIdent declName) type
-    let noExistsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.no_assignment_implies_no_hamiltonian_path' #[noExistsCert]
-    let noExistsType := q(¬ ∃ (u v : Graph.vertex $graph) (p : Path $graph u v), p.isHamiltonian)
-    return (noExistsType, noExistsHamPath, res)
+  | .unsat => return none
 
   | .error => throwError "SAT solver exited with error"
 
+open LeanSAT Model HamiltonianPath in
+unsafe def checkHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) : TermElabM Bool := do
+  -- Check if there already exists an instance of a Hamiltonian cycle for g
+  let inst ← Qq.trySynthInstanceQ q(HamiltonianPath $graph)
+  match inst with
+  | .some _ =>
+    logInfo "Hamiltonian path found"
+    return true
+  | _ =>
+    let hpQOpt ← searchForHamiltonianPathAux graph
+    match hpQOpt with
+    | some hpQ =>
+      let hamiltonianPathName := certificateName graphName "HamiltonianPathI"
+      Lean.addAndCompile <| .defnDecl {
+        name := hamiltonianPathName
+        levelParams := []
+        type := q(HamiltonianPath $graph)
+        value := hpQ
+        hints := .regular 0
+        safety := .safe
+      }
+      Lean.Meta.addInstance hamiltonianPathName .scoped 42
+      logInfo "Hamiltonian cycle found"
+      return true
+    | none => -- Graph is non Hamiltonian
+      logInfo s!"Hamiltonian path not found after exhaustive search"
+      let declName : Name := .str graphName "noHamiltonianPathCertificateExists"
+      let type : Q(Prop) := q(¬ (∃ (τ : PropAssignment (Var (Graph.vertexSize $graph))), τ |> hamiltonianPathConstraints $graph))
+      let decl := Declaration.axiomDecl {
+        name        := declName,
+        levelParams := [],
+        type        := type,
+        isUnsafe    := false
+      }
+      trace[Elab.axiom] "{declName} : {type}"
+      Term.ensureNoUnassignedMVars decl
+      addDecl decl
+      logWarning m!"added axiom {declName} : {type}"
+      return false
 
 ------------------------------------------
 -- Find Hamiltonian path command
@@ -86,11 +95,7 @@ unsafe def checkTraceableImpl : Command.CommandElab
   | `(#check_traceable $g) => Command.liftTermElabM do
     let graphName := g.getId
     let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-    let (declName, _, res) ← searchForHamiltonianPathAux graphName graph
-    match res with
-    | .sat _ => logInfo m!"found Hamiltonian path {declName}"
-    | .unsat => logInfo m!"no Hamiltonian path found after exhaustive search"
-    | .error => throwError "SAT solver exited with error"
+    let _ ← checkHamiltonianPathAux graphName graph
 
   | _ => throwUnsupportedSyntax
 
@@ -99,8 +104,30 @@ unsafe def checkTraceableImpl : Command.CommandElab
 ------------------------------------------
 -- TODO: Remove code duplication once I figure out how to do it corectly.
 
+open LeanSAT Model HamiltonianPath in
+unsafe def checkTraceableTacticAux (graphName : Name) (graph : Q(Graph)) (hypName : Name) :
+  Tactic.TacticM Unit := do
+  let isTraceable ← checkHamiltonianPathAux graphName graph
+  if isTraceable then
+    let existsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.path_of_cert #[]
+    let existsType := q(Graph.traceable $graph)
+    Tactic.liftMetaTactic fun mvarId => do
+      let mvarIdNew ← mvarId.assert hypName existsHamPath existsType
+      let (_, mvarIdNew) ← mvarIdNew.intro1P
+      return [mvarIdNew]
+  else
+    let type : Q(Prop) := q(¬ (∃ (τ : PropAssignment (Var (Graph.vertexSize $graph))), τ |> hamiltonianPathConstraints $graph))
+    let declName : Name := .str graphName "noHamiltonianPathCertificateExists"
+    let noExistsCert ← Qq.elabTermEnsuringTypeQ (mkIdent declName) type
+    let noExistsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.no_assignment_implies_no_hamiltonian_path' #[noExistsCert]
+    let noExistsType := q(¬ ∃ (u v : Graph.vertex $graph) (p : Path $graph u v), p.isHamiltonian)
+    Tactic.liftMetaTactic fun mvarId => do
+      let mvarIdNew ← mvarId.assert hypName noExistsType noExistsHamPath
+      let (_, mvarIdNew) ← mvarIdNew.intro1P
+      return [mvarIdNew]
+
 syntax (name := checkTraceableTactic) "check_traceable " ident (" with" (ppSpace colGt ident))? : tactic
-open LeanSAT Model in
+open LeanSAT Model HamiltonianPath in
 /-- `#check_traceable G` runs a SAT solver on the encoding of the Hamiltonian path problem
     on the graph `G` and if the SAT solver says the problem is unsatisfiable it runs the produced proof
     through a verified proof checker cake_lpr. If the checker agrees with the proof, we add an axiom
@@ -116,21 +143,13 @@ unsafe def checkTraceableTacticImpl : Tactic.Tactic
     Tactic.withMainContext do
       let graphName := g.getId
       let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-      let (val, type, _) ← searchForHamiltonianPathAux graphName graph
-      Tactic.liftMetaTactic fun mvarId => do
-        let mvarIdNew ← mvarId.assert .anonymous val type
-        let (_, mvarIdNew) ← mvarIdNew.intro1P
-        return [mvarIdNew]
+      checkTraceableTacticAux graphName graph .anonymous
 
   | `(tactic|check_traceable $g with $ident) =>
     Tactic.withMainContext do
       let graphName := g.getId
       let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-      let (val, type, _) ← searchForHamiltonianPathAux graphName graph
-      Tactic.liftMetaTactic fun mvarId => do
-        let mvarIdNew ← mvarId.assert ident.getId val type
-        let (_, mvarIdNew) ← mvarIdNew.intro1P
-        return [mvarIdNew]
+      checkTraceableTacticAux graphName graph ident.getId
 
   | _ => throwUnsupportedSyntax
 
diff --git a/LeanHoG/Tactic/Basic.lean b/LeanHoG/Tactic/Basic.lean
index 10cfe97..aaea95a 100644
--- a/LeanHoG/Tactic/Basic.lean
+++ b/LeanHoG/Tactic/Basic.lean
@@ -9,6 +9,7 @@ import LeanHoG.Tactic.Options
 import LeanHoG.Tactic.ParseExpr
 import LeanHoG.Invariant.HamiltonianPath.Basic
 import LeanHoG.Invariant.HamiltonianPath.Tactic
+import LeanHoG.Invariant.HamiltonianCycle.Tactic
 
 namespace LeanHoG
 
@@ -80,7 +81,8 @@ unsafe def findExampleImpl : Tactic.Tactic
       let exists_intro ← Term.mkConst ``Exists.intro
       try
         let enqs ← decomposeExistsQ goalType
-        let mentionsTracability := enqs.any (fun enq => enq.mentionsTracability)
+        let mentionsTracability := enqs.any (fun enq => enq.mentionsBoolInv .Traceable)
+        let mentionsHamiltonicity := enqs.any (fun enq => enq.mentionsBoolInv .Hamiltonian)
         let hash := hash enqs
         let query := HoGQuery.build enqs
         let graphs ← liftCommandElabM (queryDatabaseForExamplesAux [query] hash)
@@ -113,34 +115,16 @@ unsafe def findExampleImpl : Tactic.Tactic
                 -- Now try to simp which will among other things look for instance for e.g. HamiltonianPath
                 if mentionsTracability then
                   -- If we want to prove things about tracability we need to search for a Hamiltonian path
-                  let (val, type, res) ← LeanHoG.searchForHamiltonianPathAux graphIdent.getId r
-                  match res with
-                  | .unsat =>
-                    Tactic.liftMetaTactic fun mvarId => do
-                      let mvarIdNew ← mvarId.assert .anonymous val type
-                      let (_, mvarIdNew) ← mvarIdNew.intro1P
-                      return [mvarIdNew]
-                    let ctx ← mkSimpContext (← `(tactic|simp_all only [LeanHoG.Graph.no_path_not_traceable, not_false_eq_true])) false
-                    let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
-                    match result? with
-                    | none => replaceMainGoal []
-                    | some mvarId => replaceMainGoal [mvarId]
-                    Tactic.evalDecide stx
-                  | _ =>
-                    let ctx ← mkSimpContext (← `(tactic|simp_all only [LeanHoG.Graph.no_path_not_traceable, not_false_eq_true])) false
-                    let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
-                    match result? with
-                    | none => replaceMainGoal []
-                    | some mvarId => replaceMainGoal [mvarId]
-                    Tactic.evalDecide stx
-                else
-                  let ctx ← mkSimpContext (← `(tactic|simp_all)) false
-                  let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
-                  match result? with
-                  | none => replaceMainGoal []
-                  | some mvarId =>
-                    replaceMainGoal [mvarId]
-                    Tactic.evalDecide stx
+                  checkTraceableTacticAux graphIdent.getId r .anonymous
+                if mentionsHamiltonicity then
+                  checkHamiltonianTacticAux graphIdent.getId r .anonymous
+                let ctx ← mkSimpContext (← `(tactic|simp_all [LeanHoG.Graph.no_path_not_traceable, not_false_eq_true])) false
+                let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
+                match result? with
+                | none => replaceMainGoal []
+                | some mvarId =>
+                  replaceMainGoal [mvarId]
+                  Tactic.evalDecide stx
                 Lean.logInfo s!"Closed goal using {graphIdent.getId}"
               -- Visualize the graph we used to close the goal
               -- TODO: Make this an option
diff --git a/LeanHoG/Tactic/SearchDSL.lean b/LeanHoG/Tactic/SearchDSL.lean
index 204d0c8..eeb2de3 100644
--- a/LeanHoG/Tactic/SearchDSL.lean
+++ b/LeanHoG/Tactic/SearchDSL.lean
@@ -25,7 +25,7 @@ inductive BoolInvariant where
   | Regular
   | Traceable
   | TwinFree
-deriving Repr, Hashable
+deriving Repr, Hashable, DecidableEq
 
 instance : ToString BoolInvariant where
   toString := fun i =>
@@ -50,7 +50,7 @@ inductive NumericalInvariant where
   | LaplacianLargestEigenvalue
   | SecondLargestEigenvalue
   | SmallestEigenvalue
-deriving Repr, Hashable
+deriving Repr, Hashable, DecidableEq
 
 instance : ToString NumericalInvariant where
   toString := fun i =>
@@ -343,12 +343,11 @@ instance : ToString HoGEnquiry where
     | .IntegralEnquiry i => toString i
     | .FormulaEnquiry f => toString f
 
-def HoGEnquiry.mentionsTracability : HoGEnquiry → Bool
-  | .BoolEnquiry ⟨.Traceable, _⟩ => true
-  | .BoolEnquiry _ => false
-  | .NumericalEnquiry _ => false
-  | .IntegralEnquiry _ => false
-  | .FormulaEnquiry _ => false
+def HoGEnquiry.mentionsBoolInv : HoGEnquiry → BoolInvariant → Bool
+  | .BoolEnquiry ⟨inv, _⟩, inv' => inv = inv'
+  | .NumericalEnquiry _, _ => false
+  | .IntegralEnquiry _, _ => false
+  | .FormulaEnquiry _, _ => false
 
 structure InvariantQuery where
   invariantId : Nat

From eefc236b09e1d925fa8bcff3449ad1f370e3b2f5 Mon Sep 17 00:00:00 2001
From: cilinder <jure.taslak@gmail.com>
Date: Mon, 15 Apr 2024 14:34:19 -0400
Subject: [PATCH 4/4] Reorganize running invariant specific tactics a bit

---
 LeanHoG/Tactic/Basic.lean | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/LeanHoG/Tactic/Basic.lean b/LeanHoG/Tactic/Basic.lean
index aaea95a..bd4aa24 100644
--- a/LeanHoG/Tactic/Basic.lean
+++ b/LeanHoG/Tactic/Basic.lean
@@ -57,6 +57,13 @@ unsafe def downloadHoGImpl : Elab.Command.CommandElab
 -- Search tactic
 -----------------------------------------------------------------
 
+open Lean Qq in
+unsafe def solveBoolInvariantWith : BoolInvariant →
+  Meta.MetaM (Name → Q(Graph) → Name → Elab.Tactic.TacticM Unit)
+  | .Traceable => return checkTraceableTacticAux
+  | .Hamiltonian => return checkHamiltonianTacticAux
+  | inv => throwError s!"tactic for solving {inv} not implemented"
+
 syntax (name := findExample) "find_example" : tactic
 
 open Lean Qq Elab Tactic in
@@ -81,8 +88,10 @@ unsafe def findExampleImpl : Tactic.Tactic
       let exists_intro ← Term.mkConst ``Exists.intro
       try
         let enqs ← decomposeExistsQ goalType
-        let mentionsTracability := enqs.any (fun enq => enq.mentionsBoolInv .Traceable)
-        let mentionsHamiltonicity := enqs.any (fun enq => enq.mentionsBoolInv .Hamiltonian)
+        -- Find all the invariants the query mentions, for which we need special tactics
+        let mentions := List.foldl (fun ms inv =>
+          if enqs.any (fun enq => enq.mentionsBoolInv inv) then inv :: ms else ms
+        ) [] [.Traceable, .Hamiltonian]
         let hash := hash enqs
         let query := HoGQuery.build enqs
         let graphs ← liftCommandElabM (queryDatabaseForExamplesAux [query] hash)
@@ -112,12 +121,11 @@ unsafe def findExampleImpl : Tactic.Tactic
               goal.withContext do
                 let r ← Lean.Elab.Tactic.elabTermEnsuringType graphIdent goalType
                 goal.assign r
-                -- Now try to simp which will among other things look for instance for e.g. HamiltonianPath
-                if mentionsTracability then
-                  -- If we want to prove things about tracability we need to search for a Hamiltonian path
-                  checkTraceableTacticAux graphIdent.getId r .anonymous
-                if mentionsHamiltonicity then
-                  checkHamiltonianTacticAux graphIdent.getId r .anonymous
+                -- Now run the appropriate tactic for each kind of invariant we're trying to solve
+                for inv in mentions do
+                  let tac ← solveBoolInvariantWith inv
+                  tac graphIdent.getId r .anonymous
+                -- Run `simp` and `decide` on the new goal after using G as the existence target
                 let ctx ← mkSimpContext (← `(tactic|simp_all [LeanHoG.Graph.no_path_not_traceable, not_false_eq_true])) false
                 let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
                 match result? with