Skip to content

Commit

Permalink
feat: literal values in grind
Browse files Browse the repository at this point in the history
  • Loading branch information
leodemoura committed Dec 27, 2024
1 parent 14a47c6 commit 198e417
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 2 deletions.
15 changes: 13 additions & 2 deletions src/Lean/Meta/Tactic/Grind/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,15 @@ private def closeGoalWithTrueEqFalse : GoalM Unit := do
let falseProof ← mkEqMP trueEqFalse (mkConst ``True.intro)
closeGoal falseProof

/-- Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class. -/
private def closeGoalWithValuesEq (lhs rhs : Expr) : GoalM Unit := do
let p ← mkEq lhs rhs
let hp ← mkEqProof lhs rhs
let d ← mkDecide p
let pEqFalse := mkApp3 (mkConst ``eq_false_of_decide) p d.appArg! (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``false))
let falseProof ← mkEqMP pEqFalse hp
closeGoal falseProof

private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
trace[grind.eq] "{lhs} {if isHEq then "" else "="} {rhs}"
let lhsNode ← getENode lhs
Expand All @@ -119,8 +128,8 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
let mut valueInconsistency := false
let mut trueEqFalse := false
if lhsRoot.interpreted && rhsRoot.interpreted then
markAsInconsistent
if lhsNode.root.isTrue || rhsNode.root.isTrue then
markAsInconsistent
trueEqFalse := true
else
valueInconsistency := true
Expand All @@ -135,7 +144,9 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
unless (← isInconsistent) do
if lhsRoot.ctor && rhsRoot.ctor then
propagateCtor lhsRoot.self rhsRoot.self
-- TODO: propagate value inconsistency
unless (← isInconsistent) do
if valueInconsistency then
closeGoalWithValuesEq lhsRoot.self rhsRoot.self
trace[grind.debug] "after addEqStep, {← ppState}"
checkInvariants
where
Expand Down
21 changes: 21 additions & 0 deletions tests/lean/run/grind_t1.lean
Original file line number Diff line number Diff line change
Expand Up @@ -34,3 +34,24 @@ example (h : x = y) (h₁ : a :: b = x) (h₂ : c :: d = y) : b = d := by

example (a b : Sum Nat Bool) : a = .inl x → b = .inl y → x ≠ y → a = b → False := by
grind

example (a b : Nat) : a = 1 → b = 2 → a = b → False := by
grind

example (a b c : Int) : a = 1 → c = -2 → a = b → c = b → False := by
grind

example (a b : Char) : a = 'h' → b = 'w' → a = b → False := by
grind

example (a b : String) : a = "hello" → b = "world" → a = b → False := by
grind

example (a b c : String) : a = c → a = "hello" → c = "world" → c = b → False := by
grind

example (a b c : BitVec 32) : a = c → a = 1#32 → c = 2#32 → c = b → False := by
grind

example (a b c : UInt32) : a = c → a = 1 → c = 200 → c = b → False := by
grind

0 comments on commit 198e417

Please sign in to comment.