From 769fe4ebf6177ea90e257066cd44732ab9c20f3c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Feb 2025 15:40:07 -0800 Subject: [PATCH] feat: add `Grind.mkDiseqProof?` (#7231) This PR implements functions for constructing disequality proofs in `grind`. --- src/Init/Grind/Lemmas.lean | 5 ++ src/Lean/Meta/Tactic/Grind.lean | 1 + src/Lean/Meta/Tactic/Grind/Core.lean | 4 +- src/Lean/Meta/Tactic/Grind/Diseq.lean | 87 +++++++++++++++++++++++++++ src/Lean/Meta/Tactic/Grind/Types.lean | 3 +- tests/lean/run/grind_diseq_api.lean | 80 ++++++++++++++++++++++++ 6 files changed, 177 insertions(+), 3 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Grind/Diseq.lean create mode 100644 tests/lean/run/grind_diseq_api.lean diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean index 054ff33f99..ae15e08473 100644 --- a/src/Init/Grind/Lemmas.lean +++ b/src/Init/Grind/Lemmas.lean @@ -69,6 +69,11 @@ theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by s theorem eq_congr {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*] theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)] +/-! Ne -/ + +theorem ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := by simp [*] +theorem ne_of_ne_of_eq_right {α : Sort u} {a b c : α} (h₁ : a = c) (h₂ : b ≠ c) : b ≠ a := by simp [*] + /-! Bool.and -/ theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h] diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index 39e34f16b9..b34c31d885 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -28,6 +28,7 @@ import Lean.Meta.Tactic.Grind.Arith import Lean.Meta.Tactic.Grind.Ext import Lean.Meta.Tactic.Grind.MatchCond import Lean.Meta.Tactic.Grind.MatchDiscrOnly +import Lean.Meta.Tactic.Grind.Diseq namespace Lean diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index f01c7ecf0a..4723e1b149 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -226,11 +226,11 @@ where propagateBeta lams₁ fns₁ propagateBeta lams₂ fns₂ resetParentsOf lhsRoot.self + propagateOffsetEq rhsRoot lhsRoot + propagateCutsatEq rhsRoot lhsRoot copyParentsTo parents rhsNode.root unless (← isInconsistent) do updateMT rhsRoot.self - propagateOffsetEq rhsRoot lhsRoot - propagateCutsatEq rhsRoot lhsRoot unless (← isInconsistent) do for parent in parents do propagateUp parent diff --git a/src/Lean/Meta/Tactic/Grind/Diseq.lean b/src/Lean/Meta/Tactic/Grind/Diseq.lean new file mode 100644 index 0000000000..6c2d63312d --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Diseq.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Grind.Lemmas +import Lean.Meta.Tactic.Grind.Types + +namespace Lean.Meta.Grind + +/-- +Returns `true` if type of `t` is definitionally equal to `α` +-/ +private def hasType (t α : Expr) : MetaM Bool := + withDefault do isDefEq (← inferType t) α + +/-- +Returns `some (c = d)` if +- `c = d` and `False` are in the same equivalence class, and +- `a` (`b`) and `c` are in the same equivalence class, and +- `b` (`a`) and `d` are in the same equivalence class. +Otherwise return `none`. + +Remark `a` and `b` are assumed to have the same type. +-/ +private def getDiseqFor? (a b : Expr) : GoalM (Option Expr) := do + /- + In Z3, we use the congruence table to find equalities more efficiently, + but this optimization would be more complicated here because equalities have + the type as an implicit argument, and `grind`s congruence table assumes it is + hash-consed and canonicalized. So, we use the "slower" approach of visiting + parents. + -/ + let aRoot ← getRoot a + let bRoot ← getRoot b + let aParents ← getParents aRoot + let bParents ← getParents bRoot + if aParents.size ≤ bParents.size then + go aParents + else + go bParents +where + go (parents : ParentSet) : GoalM (Option Expr) := do + for parent in parents do + let_expr Eq α c d := parent | continue + if (← isEqFalse parent) then + -- Remark: we expect `hasType` test to seldom fail, but it can happen because of + -- heterogeneous equalities + if (← isEqv a c <&&> isEqv b d <&&> hasType a α) then + return some parent + if (← isEqv a d <&&> isEqv b c <&&> hasType a α) then + return some parent + return none + +/-- +Returns `true` if `a` and `b` are known to be disequal. +See `getDiseqFor?` +-/ +def isDiseq (a b : Expr) : GoalM Bool := do + return (← getDiseqFor? a b).isSome + +/-- +Returns a proof for `true` if `a` and `b` are known to be disequal. +See `getDiseqFor?` +-/ +def mkDiseqProof? (a b : Expr) : GoalM (Option Expr) := do + let some eq ← getDiseqFor? a b | return none + let_expr f@Eq α c d := eq | unreachable! + let u := f.constLevels! + let h ← mkOfEqFalse (← mkEqFalseProof eq) + let (c, d, h) ← if (← isEqv a c <&&> isEqv b d) then + pure (c, d, h) + else + pure (d, c, mkApp4 (mkConst ``Ne.symm u) α c d h) + -- We have `a = c` and `b = d` + let h ← if isSameExpr a c then + pure h + else + pure <| mkApp6 (mkConst ``Grind.ne_of_ne_of_eq_left u) α a c d (← mkEqProof a c) h + -- `h : a ≠ d + if isSameExpr b d then + return h + else + return mkApp6 (mkConst ``Grind.ne_of_ne_of_eq_right u) α b a d (← mkEqProof b d) h + +end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index d660d34d33..ae4bf58f0f 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Init.Grind.Tactics import Init.Data.Queue +import Std.Data.TreeSet import Lean.Util.ShareCommon import Lean.HeadIndex import Lean.Meta.Basic @@ -396,7 +397,7 @@ instance : BEq (CongrKey enodes) where abbrev CongrTable (enodes : ENodeMap) := PHashSet (CongrKey enodes) -- Remark: we cannot use pointer addresses here because we have to traverse the tree. -abbrev ParentSet := RBTree Expr Expr.quickComp +abbrev ParentSet := Std.TreeSet Expr Expr.quickComp abbrev ParentMap := PHashMap ENodeKey ParentSet /-- diff --git a/tests/lean/run/grind_diseq_api.lean b/tests/lean/run/grind_diseq_api.lean new file mode 100644 index 0000000000..7429dae319 --- /dev/null +++ b/tests/lean/run/grind_diseq_api.lean @@ -0,0 +1,80 @@ +import Lean + +opaque a : Nat +opaque b : Nat + +-- Prints the equivalence class containing a `f` application +open Lean Meta Grind in +def fallback : Fallback := do + let a ← shareCommon <| mkConst ``a + let b ← shareCommon <| mkConst ``b + let some h ← mkDiseqProof? a b | + throwError "terms are not diseq" + check h + trace[Meta.debug] "{h} : {← inferType h}" + assert! (← isDiseq a b) + assert! (← isDiseq b a) + let some h' ← mkDiseqProof? b a | + throwError "terms are not diseq" + let h' ← mkAppM ``Ne.symm #[h'] + assert! (← isDefEq h h') + (← get).mvarId.admit + +set_option trace.Meta.debug true + +/-- +info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1)) : a ≠ b +-/ +#guard_msgs (info) in +example (x y : Nat) : a = x → y ≠ x → b = y → False := by + grind on_failure fallback + +/-- +info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h h_1) : a ≠ b +-/ +#guard_msgs (info) in +example (x y : Nat) : a = x → x ≠ y → b = y → False := by + grind on_failure fallback + +/-- +info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_3 (Lean.Grind.ne_of_ne_of_eq_left (Eq.trans h (Eq.symm h_1)) h_2) : a ≠ b +-/ +#guard_msgs (info) in +example (x y z : Nat) : a = x → z = x → z ≠ y → b = y → False := by + grind on_failure fallback + +/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/ +#guard_msgs (info) in +example (x : Nat) : a = x → b ≠ x → False := by + grind on_failure fallback + +/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h h_1 : a ≠ b -/ +#guard_msgs (info) in +example (x : Nat) : a = x → x ≠ b → False := by + grind on_failure fallback + + +/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h h_1 : a ≠ b -/ +#guard_msgs (info) in +example (x : Nat) : b = x → a ≠ x → False := by + grind on_failure fallback + +/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h (Ne.symm h_1) : a ≠ b -/ +#guard_msgs (info) in +example (x : Nat) : b = x → x ≠ a → False := by + grind on_failure fallback + +/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/ +#guard_msgs (info) in +example (x : Nat) : a = x → b ≠ x → False := by + grind on_failure fallback + +/-- info: [Meta.debug] h : ¬a = b -/ +#guard_msgs (info) in +example : a ≠ b → False := by + grind on_failure fallback + +/-- info: [Meta.debug] Ne.symm h : a ≠ b -/ +#guard_msgs (info) in +example : b ≠ a → False := by + grind on_failure fallback