feat: proofs for theory propagation in grind order

This PR implements proof construction for theory propagation in `grind order`.

src/Init/Grind/Order.lean

@@ -143,6 +143,11 @@ private theorem add_lt_add_of_lt_of_le {α} [LE α] [LT α] [Std.LawfulOrderLT
 
 /-! Theorems for propagating constraints to `True` -/
 
+theorem le_eq_true_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α]
+    (a b : α) : a < b → (a ≤ b) = True := by
+  simp; intro h
+  exact Std.le_of_lt h
+
 theorem le_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
     (a b : α) (k₁ k₂ : Int) : k₁.ble' k₂ → a ≤ b + k₁ → (a ≤ b + k₂) = True := by
   simp; intro h₁ h₂
@@ -184,6 +189,13 @@ theorem lt_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPr
 
 /-! Theorems for propagating constraints to `False` -/
 
+theorem le_eq_false_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α]
+    (a b : α) : a < b → (b ≤ a) = False := by
+  simp; intro h₁ h₂
+  have := lt_le_trans h₁ h₂
+  have := Preorder.lt_irrefl a
+  contradiction
+
 theorem le_eq_false_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
     (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).blt' 0 → a ≤ b + k₁ → (b ≤ a + k₂) = False := by
   intro h₁; simp; intro h₂ h₃

src/Lean/Meta/Tactic/Grind/Order/OrderM.lean

@@ -54,4 +54,7 @@ def getProof (u v : NodeId) : OrderM ProofInfo := do
 def getCnstr? (e : Expr) : OrderM (Option (Cnstr NodeId)) :=
   return (← getStruct).cnstrs.find? { expr := e }
 
+def isRing : OrderM Bool :=
+  return (← getStruct).ringId?.isSome
+
 end Lean.Meta.Grind.Order

src/Lean/Meta/Tactic/Grind/Order/Proof.lean

@@ -17,20 +17,35 @@ def mkLePreorderPrefix (declName : Name) : OrderM Expr := do
   return mkApp3 (mkConst declName [s.u]) s.type s.leInst s.isPreorderInst
 
 /--
-Returns `declName α leInst ltInst lawfulOrderLtInst isPreorderInst`
+Returns `declName α leInst ltInst lawfulOrderLtInst`
 -/
 def mkLeLtPrefix (declName : Name) : OrderM Expr := do
   let s ← getStruct
-  return mkApp5 (mkConst declName [s.u]) s.type s.leInst s.ltInst?.get! s.lawfulOrderLTInst?.get! s.isPreorderInst
+  return mkApp4 (mkConst declName [s.u]) s.type s.leInst s.ltInst?.get! s.lawfulOrderLTInst?.get!
+
+/--
+Returns `declName α leInst ltInst lawfulOrderLtInst isPreorderInst`
+-/
+def mkLeLtPreorderPrefix (declName : Name) : OrderM Expr := do
+  let s ← getStruct
+  return mkApp (← mkLeLtPrefix declName) s.isPreorderInst
 
 /--
 Returns `declName α leInst ltInst lawfulOrderLtInst isPreorderInst ringInst ordRingInst`
 -/
 def mkOrdRingPrefix (declName : Name) : OrderM Expr := do
   let s ← getStruct
-  let h ← mkLeLtPrefix declName
+  let h ← mkLeLtPreorderPrefix declName
   return mkApp2 h s.ringInst?.get! s.orderedRingInst?.get!
 
+def mkTransCoreProof (u v w : Expr) (strict₁ strict₂ : Bool) (h₁ h₂ : Expr) : OrderM Expr := do
+  let h ← match strict₁, strict₂ with
+    | false, false => mkLePreorderPrefix ``Grind.Order.le_trans
+    | false, true  => mkLeLtPreorderPrefix ``Grind.Order.le_lt_trans
+    | true,  false => mkLeLtPreorderPrefix ``Grind.Order.lt_le_trans
+    | true,  true  => mkLeLtPreorderPrefix ``Grind.Order.lt_trans
+  return mkApp5 h u v w h₁ h₂
+
 /--
 Assume `p₁` is `{ w := u, k := k₁, proof := p₁ }` and `p₂` is `{ w := w, k := k₂, proof := p₂ }`
 `p₁` is the proof for edge `u → w` and `p₂` the proof for edge `w -> v`.
@@ -41,15 +56,20 @@ Remark: for orders that do not support offsets.
 def mkTransCore (p₁ : ProofInfo) (p₂ : ProofInfo) (v : NodeId) : OrderM ProofInfo := do
   let { w := u, k.strict := s₁, proof := h₁, .. } := p₁
   let { w, k.strict := s₂, proof := h₂, .. } := p₂
-  let h ← match s₁, s₂ with
-    | false, false => mkLePreorderPrefix ``Grind.Order.le_trans
-    | false, true  => mkLeLtPrefix ``Grind.Order.le_lt_trans
-    | true,  false => mkLeLtPrefix ``Grind.Order.lt_le_trans
-    | true,  true  => mkLeLtPrefix ``Grind.Order.lt_trans
   let ns := (← getStruct).nodes
-  let h := mkApp5 h ns[u]! ns[w]! ns[v]! h₁ h₂
+  let h ← mkTransCoreProof ns[u]! ns[w]! ns[v]! s₁ s₂ h₁ h₂
   return { w := p₁.w, k.strict := s₁ || s₂, proof := h }
 
+def mkTransOffsetProof (u v w : Expr) (k₁ k₂ : Weight) (h₁ h₂ : Expr) : OrderM Expr := do
+  let h ← match k₁.strict, k₂.strict with
+    | false, false => mkOrdRingPrefix ``Grind.Order.le_trans_k
+    | false, true  => mkOrdRingPrefix ``Grind.Order.le_lt_trans_k
+    | true,  false => mkOrdRingPrefix ``Grind.Order.lt_le_trans_k
+    | true,  true  => mkOrdRingPrefix ``Grind.Order.lt_trans_k
+  let k  := k₁.k + k₂.k
+  let h := mkApp6 h u v w (toExpr k₁.k) (toExpr k₂.k) (toExpr k)
+  return mkApp3 h h₁ h₂ eagerReflBoolTrue
+
 /--
 Assume `p₁` is `{ w := u, k := k₁, proof := p₁ }` and `p₂` is `{ w := w, k := k₂, proof := p₂ }`
 `p₁` is the proof for edge `u -(k₁)→ w` and `p₂` the proof for edge `w -(k₂)-> v`.
@@ -58,18 +78,11 @@ Then, this function returns a proof for edge `u -(k₁+k₂) -> v`.
 Remark: for orders that support offsets.
 -/
 def mkTransOffset (p₁ : ProofInfo) (p₂ : ProofInfo) (v : NodeId) : OrderM ProofInfo := do
-  let { w := u, k.k := k₁, k.strict := s₁, proof := h₁, .. } := p₁
-  let { w, k.k := k₂, k.strict := s₂, proof := h₂, .. } := p₂
-  let h ← match s₁, s₂ with
-    | false, false => mkOrdRingPrefix ``Grind.Order.le_trans_k
-    | false, true  => mkOrdRingPrefix ``Grind.Order.le_lt_trans_k
-    | true,  false => mkOrdRingPrefix ``Grind.Order.lt_le_trans_k
-    | true,  true  => mkOrdRingPrefix ``Grind.Order.lt_trans_k
-  let k  := k₁ + k₂
+  let { w := u, k:= k₁, proof := h₁, .. } := p₁
+  let { w, k := k₂, proof := h₂, .. } := p₂
   let ns := (← getStruct).nodes
-  let h := mkApp6 h ns[u]! ns[w]! ns[v]! (toExpr k₁) (toExpr k₂) (toExpr k)
-  let h := mkApp3 h h₁ h₂ eagerReflBoolTrue
-  return { w := p₁.w, k.k := k, k.strict := s₁ || s₂, proof := h }
+  let h ← mkTransOffsetProof ns[u]! ns[w]! ns[v]! k₁ k₂ h₁ h₂
+  return { w := p₁.w, k.k := k₁.k + k₂.k, k.strict := k₁.strict || k₂.strict, proof := h }
 
 /--
 Assume `p₁` is `{ w := u, k := k₁, proof := p₁ }` and `p₂` is `{ w := w, k := k₂, proof := p₂ }`
@@ -79,10 +92,88 @@ Then, this function returns a proof for edge `u -(k₁+k₂) -> v`.
 Remark: if the order does not support offset `k₁` and `k₂` are zero.
 -/
 public def mkTrans (p₁ : ProofInfo) (p₂ : ProofInfo) (v : NodeId) : OrderM ProofInfo := do
-  let s ← getStruct
-  if s.orderedRingInst?.isSome then
+  if (← isRing) then
     mkTransOffset p₁ p₂ v
   else
     mkTransCore p₁ p₂ v
 
+def mkPropagateEqTrueProofCore (u v : Expr) (k : Weight) (huv : Expr) (k' : Weight) : OrderM Expr := do
+  if k.strict == k'.strict then
+    mkEqTrue huv
+  else
+    assert! k.strict && !k'.strict
+    let h ← mkLeLtPrefix ``Grind.Order.le_eq_true_of_lt
+    return mkApp3 h u v huv
+
+def mkPropagateEqTrueProofOffset (u v : Expr) (k : Weight) (huv : Expr) (k' : Weight) : OrderM Expr := do
+  let declName := match k'.strict, k.strict with
+    | false, false => ``Grind.Order.le_eq_true_of_le_k
+    | false, true  => ``Grind.Order.le_eq_true_of_lt_k
+    | true,  false => ``Grind.Order.lt_eq_true_of_le_k
+    | true,  true  => ``Grind.Order.lt_eq_true_of_lt_k
+  let h ← mkOrdRingPrefix declName
+  return mkApp6 h u v (toExpr k.k) (toExpr k'.k) eagerReflBoolTrue huv
+
+/--
+Given a path `u --(k)--> v` justified by proof `huv`,
+construct a proof of `e = True` where `e` is a term corresponding to the edge `u --(k') --> v`
+-/
+public def mkPropagateEqTrueProof (u v : Expr) (k : Weight) (huv : Expr) (k' : Weight) : OrderM Expr := do
+  if (← isRing) then
+    mkPropagateEqTrueProofOffset u v k huv k'
+  else
+    mkPropagateEqTrueProofCore u v k huv k'
+
+/--
+`u < v → (v ≤ u) = False
+-/
+def mkPropagateEqFalseProofCore (u v : Expr) (huv : Expr) : OrderM Expr := do
+  let h ← mkLeLtPreorderPrefix ``Grind.Order.le_eq_false_of_lt
+  return mkApp3 h u v huv
+
+def mkPropagateEqFalseProofOffset (u v : Expr) (k : Weight) (huv : Expr) (k' : Weight) : OrderM Expr := do
+  let declName := match k'.strict, k.strict with
+    | false, false => ``Grind.Order.le_eq_false_of_le_k
+    | false, true  => ``Grind.Order.le_eq_false_of_lt_k
+    | true,  false => ``Grind.Order.lt_eq_false_of_le_k
+    | true,  true  => ``Grind.Order.lt_eq_false_of_lt_k
+  let h ← mkOrdRingPrefix declName
+  return mkApp6 h u v (toExpr k.k) (toExpr k'.k) eagerReflBoolTrue huv
+
+/--
+Given a path `u --(k)--> v` justified by proof `huv`,
+construct a proof of `e = False` where `e` is a term corresponding to the edge `u --(k') --> v`
+-/
+public def mkPropagateEqFalseProof (u v : Expr) (k : Weight) (huv : Expr) (k' : Weight) : OrderM Expr := do
+  if (← isRing) then
+    mkPropagateEqFalseProofOffset u v k huv k'
+  else
+    mkPropagateEqFalseProofCore u v huv
+
+def mkUnsatProofCore (u v : Expr) (k₁ : Weight) (h₁ : Expr) (k₂ : Weight) (h₂ : Expr) : OrderM Expr := do
+  let h ← mkTransCoreProof u v u k₁.strict k₂.strict h₁ h₂
+  assert! k₁.strict || k₂.strict
+  let hf ← mkLeLtPreorderPrefix ``Grind.Order.lt_unsat
+  return mkApp2 hf u h
+
+def mkUnsatProofOffset (u v : Expr) (k₁ : Weight) (h₁ : Expr) (k₂ : Weight) (h₂ : Expr) : OrderM Expr := do
+  let h ← mkTransOffsetProof u v u k₁ k₂ h₁ h₂
+  let declName := if k₁.strict || k₂.strict then
+    ``Grind.Order.lt_unsat_k
+  else
+    ``Grind.Order.le_unsat_k
+  let hf ← mkOrdRingPrefix declName
+  return mkApp4 hf u (toExpr (k₁.k + k₂.k)) eagerReflBoolTrue h
+
+/--
+Returns a proof of `False` using a negative cycle composed of
+- `u --(k₁)--> v` with proof `h₁`
+- `v --(k₂)--> u` with proof `h₂`
+-/
+def mkUnsatProof (u v : Expr) (k₁ : Weight) (h₁ : Expr) (k₂ : Weight) (h₂ : Expr) : OrderM Expr := do
+  if (← isRing) then
+    mkUnsatProofOffset u v k₁ h₁ k₂ h₂
+  else
+    mkUnsatProofCore u v k₁ h₁ k₂ h₂
+
 end Lean.Meta.Grind.Order