From 7ecadafd7b246d44ce749d8d5d2198bb2f65b4d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2025 16:26:16 -0800 Subject: [PATCH 1/7] chore: cleanup test --- tests/lean/run/grind_split_issue.lean | 31 ++++++--------------------- 1 file changed, 6 insertions(+), 25 deletions(-) diff --git a/tests/lean/run/grind_split_issue.lean b/tests/lean/run/grind_split_issue.lean index 7073ed6b39c1..4d7f7f90e1e9 100644 --- a/tests/lean/run/grind_split_issue.lean +++ b/tests/lean/run/grind_split_issue.lean @@ -5,45 +5,26 @@ inductive X : Nat → Prop /-- error: `grind` failed -case grind.1.1 +case grind.1 c : Nat q : X c 0 -s✝ : Nat -h✝² : 0 = s✝ -h✝¹ : HEq ⋯ ⋯ s : Nat -h✝ : c = s +h✝ : 0 = s h : HEq ⋯ ⋯ ⊢ False [grind] Diagnostics [facts] Asserted facts [prop] X c 0 - [prop] X c 0 - [prop] X c c → X c 0 - [prop] X c c - [prop] 0 = s✝ - [prop] HEq ⋯ ⋯ - [prop] c = s + [prop] 0 = s [prop] HEq ⋯ ⋯ [eqc] True propositions [prop] X c 0 - [prop] X c c → X c 0 - [prop] X c c - [prop] X c s✝ [prop] X c s [eqc] Equivalence classes - [eqc] {c, s} - [eqc] {s✝, 0} - [ematch] E-matching patterns - [thm] X.f: [X #1 #0] - [thm] X.g: [X #2 #1] + [eqc] {s, 0} [grind] Issues - [issue] #2 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)` -[grind] Counters - [thm] E-Matching instances - [thm] X.f ↦ 2 - [thm] X.g ↦ 2 + [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)` -/ #guard_msgs (error) in example {c : Nat} (q : X c 0) : False := by - grind [X] + grind [cases X] From 73a7199b1a28a27badb285403b0929922be1461c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2025 17:29:33 -0800 Subject: [PATCH 2/7] feat: add `isEqBoolTrue` and `isEqBoolFalse` --- src/Lean/Meta/Tactic/Grind/Types.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 4ef28132e9da..45458a9839e4 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -570,13 +570,19 @@ def getGeneration (e : Expr) : GoalM Nat := do /-- Returns `true` if `e` is in the equivalence class of `True`. -/ def isEqTrue (e : Expr) : GoalM Bool := do - let n ← getENode e - return isSameExpr n.root (← getTrueExpr) + return isSameExpr (← getENode e).root (← getTrueExpr) /-- Returns `true` if `e` is in the equivalence class of `False`. -/ def isEqFalse (e : Expr) : GoalM Bool := do - let n ← getENode e - return isSameExpr n.root (← getFalseExpr) + return isSameExpr (← getENode e).root (← getFalseExpr) + +/-- Returns `true` if `e` is in the equivalence class of `Bool.true`. -/ +def isEqBoolTrue (e : Expr) : GoalM Bool := do + return isSameExpr (← getENode e).root (← getBoolTrueExpr) + +/-- Returns `true` if `e` is in the equivalence class of `Bool.false`. -/ +def isEqBoolFalse (e : Expr) : GoalM Bool := do + return isSameExpr (← getENode e).root (← getBoolFalseExpr) /-- Returns `true` if `a` and `b` are in the same equivalence class. -/ def isEqv (a b : Expr) : GoalM Bool := do From dc279d97f4aaf954beafc9d7f4c55ce160ebce9d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2025 17:36:18 -0800 Subject: [PATCH 3/7] feat: add `mkEqBoolTrueProof` and `mkEqBoolFalseProof` --- src/Lean/Meta/Tactic/Grind/Types.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 45458a9839e4..48ddf0508c41 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -843,6 +843,20 @@ It assumes `a` and `False` are in the same equivalence class. def mkEqFalseProof (a : Expr) : GoalM Expr := do mkEqProof a (← getFalseExpr) +/-- +Returns a proof that `a = Bool.true`. +It assumes `a` and `Bool.true` are in the same equivalence class. +-/ +def mkEqBoolTrueProof (a : Expr) : GoalM Expr := do + mkEqProof a (← getBoolTrueExpr) + +/-- +Returns a proof that `a = Bool.false`. +It assumes `a` and `Bool.false` are in the same equivalence class. +-/ +def mkEqBoolFalseProof (a : Expr) : GoalM Expr := do + mkEqProof a (← getBoolFalseExpr) + /-- Marks current goal as inconsistent without assigning `mvarId`. -/ def markAsInconsistent : GoalM Unit := do unless (← get).inconsistent do From cd942687366514c5239964a961db5ab708616b79 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2025 17:55:58 -0800 Subject: [PATCH 4/7] chore: cleanup --- src/Lean/Meta/Tactic/Grind/Propagate.lean | 40 +++++++++++------------ 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean index 39d5b5a38e79..0ef4b89c19bb 100644 --- a/src/Lean/Meta/Tactic/Grind/Propagate.lean +++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean @@ -27,16 +27,16 @@ builtin_grind_propagator propagateAndUp ↑And := fun e => do let_expr And a b := e | return () if (← isEqTrue a) then -- a = True → (a ∧ b) = b - pushEq e b <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_left) a b (← mkEqTrueProof a) + pushEq e b <| mkApp3 (mkConst ``Grind.and_eq_of_eq_true_left) a b (← mkEqTrueProof a) else if (← isEqTrue b) then -- b = True → (a ∧ b) = a - pushEq e a <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_right) a b (← mkEqTrueProof b) + pushEq e a <| mkApp3 (mkConst ``Grind.and_eq_of_eq_true_right) a b (← mkEqTrueProof b) else if (← isEqFalse a) then -- a = False → (a ∧ b) = False - pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_left) a b (← mkEqFalseProof a) + pushEqFalse e <| mkApp3 (mkConst ``Grind.and_eq_of_eq_false_left) a b (← mkEqFalseProof a) else if (← isEqFalse b) then -- b = False → (a ∧ b) = False - pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_right) a b (← mkEqFalseProof b) + pushEqFalse e <| mkApp3 (mkConst ``Grind.and_eq_of_eq_false_right) a b (← mkEqFalseProof b) /-- Propagates truth values downwards for a conjunction `a ∧ b` when the @@ -46,8 +46,8 @@ builtin_grind_propagator propagateAndDown ↓And := fun e => do if (← isEqTrue e) then let_expr And a b := e | return () let h ← mkEqTrueProof e - pushEqTrue a <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_left) a b h - pushEqTrue b <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_right) a b h + pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_and_eq_true_left) a b h + pushEqTrue b <| mkApp3 (mkConst ``Grind.eq_true_of_and_eq_true_right) a b h /-- Propagates equalities for a disjunction `a ∨ b` based on the truth values @@ -63,16 +63,16 @@ builtin_grind_propagator propagateOrUp ↑Or := fun e => do let_expr Or a b := e | return () if (← isEqFalse a) then -- a = False → (a ∨ b) = b - pushEq e b <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_left) a b (← mkEqFalseProof a) + pushEq e b <| mkApp3 (mkConst ``Grind.or_eq_of_eq_false_left) a b (← mkEqFalseProof a) else if (← isEqFalse b) then -- b = False → (a ∨ b) = a - pushEq e a <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_right) a b (← mkEqFalseProof b) + pushEq e a <| mkApp3 (mkConst ``Grind.or_eq_of_eq_false_right) a b (← mkEqFalseProof b) else if (← isEqTrue a) then -- a = True → (a ∨ b) = True - pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_left) a b (← mkEqTrueProof a) + pushEqTrue e <| mkApp3 (mkConst ``Grind.or_eq_of_eq_true_left) a b (← mkEqTrueProof a) else if (← isEqTrue b) then -- b = True → (a ∧ b) = True - pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_right) a b (← mkEqTrueProof b) + pushEqTrue e <| mkApp3 (mkConst ``Grind.or_eq_of_eq_true_right) a b (← mkEqTrueProof b) /-- Propagates truth values downwards for a disjuction `a ∨ b` when the @@ -82,8 +82,8 @@ builtin_grind_propagator propagateOrDown ↓Or := fun e => do if (← isEqFalse e) then let_expr Or a b := e | return () let h ← mkEqFalseProof e - pushEqFalse a <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_left) a b h - pushEqFalse b <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_right) a b h + pushEqFalse a <| mkApp3 (mkConst ``Grind.eq_false_of_or_eq_false_left) a b h + pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_or_eq_false_right) a b h /-- Propagates equalities for a negation `Not a` based on the truth value of `a`. @@ -96,12 +96,12 @@ builtin_grind_propagator propagateNotUp ↑Not := fun e => do let_expr Not a := e | return () if (← isEqFalse a) then -- a = False → (Not a) = True - pushEqTrue e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_false) a (← mkEqFalseProof a) + pushEqTrue e <| mkApp2 (mkConst ``Grind.not_eq_of_eq_false) a (← mkEqFalseProof a) else if (← isEqTrue a) then -- a = True → (Not a) = False - pushEqFalse e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_true) a (← mkEqTrueProof a) + pushEqFalse e <| mkApp2 (mkConst ``Grind.not_eq_of_eq_true) a (← mkEqTrueProof a) else if (← isEqv e a) then - closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a) + closeGoal <| mkApp2 (mkConst ``Grind.false_of_not_eq_self) a (← mkEqProof e a) /-- Propagates truth values downwards for a negation expression `Not a` based on the truth value of `Not a`. @@ -113,19 +113,19 @@ This function performs the following: builtin_grind_propagator propagateNotDown ↓Not := fun e => do let_expr Not a := e | return () if (← isEqFalse e) then - pushEqTrue a <| mkApp2 (mkConst ``Lean.Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e) + pushEqTrue a <| mkApp2 (mkConst ``Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e) else if (← isEqTrue e) then - pushEqFalse a <| mkApp2 (mkConst ``Lean.Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e) + pushEqFalse a <| mkApp2 (mkConst ``Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e) else if (← isEqv e a) then - closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a) + closeGoal <| mkApp2 (mkConst ``Grind.false_of_not_eq_self) a (← mkEqProof e a) /-- Propagates `Eq` upwards -/ builtin_grind_propagator propagateEqUp ↑Eq := fun e => do let_expr Eq _ a b := e | return () if (← isEqTrue a) then - pushEq e b <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a) + pushEq e b <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a) else if (← isEqTrue b) then - pushEq e a <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b) + pushEq e a <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b) else if (← isEqv a b) then pushEqTrue e <| mkEqTrueCore e (← mkEqProof a b) let aRoot ← getRootENode a From 88aa74a77db96b7fcf66076d52d20ed20ad9b3ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2025 17:56:25 -0800 Subject: [PATCH 5/7] feat: helper theorems for `Bool` propagation --- src/Init/Grind/Lemmas.lean | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean index bd45d450117c..e7aef53b6caa 100644 --- a/src/Init/Grind/Lemmas.lean +++ b/src/Init/Grind/Lemmas.lean @@ -69,6 +69,37 @@ 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₂)] +/-! Bool.and -/ + +theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h] +theorem Bool.and_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a && b) = a := by simp [h] +theorem Bool.and_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a && b) = false := by simp [h] +theorem Bool.and_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a && b) = false := by simp [h] + +theorem Bool.eq_true_of_and_eq_true_left {a b : Bool} (h : (a && b) = true) : a = true := by simp_all +theorem Bool.eq_true_of_and_eq_true_right {a b : Bool} (h : (a && b) = true) : b = true := by simp_all + +/-! Bool.or -/ + +theorem Bool.or_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a || b) = true := by simp [h] +theorem Bool.or_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a || b) = true := by simp [h] +theorem Bool.or_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a || b) = b := by simp [h] +theorem Bool.or_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a || b) = a := by simp [h] +theorem Bool.eq_false_of_or_eq_false_left {a b : Bool} (h : (a || b) = false) : a = false := by + cases a <;> simp_all +theorem Bool.eq_false_of_or_eq_false_right {a b : Bool} (h : (a || b) = false) : b = false := by + cases a <;> simp_all + +/-! Bool.not -/ + +theorem Bool.not_eq_of_eq_true {a : Bool} (h : a = true) : (!a) = false := by simp [h] +theorem Bool.not_eq_of_eq_false {a : Bool} (h : a = false) : (!a) = true := by simp [h] +theorem Bool.eq_false_of_not_eq_true {a : Bool} (h : (!a) = true) : a = false := by simp_all +theorem Bool.eq_true_of_not_eq_false {a : Bool} (h : (!a) = false) : a = true := by simp_all + +theorem Bool.false_of_not_eq_self {a : Bool} (h : (!a) = a) : False := by + by_cases a <;> simp_all + /- The following two helper theorems are used to case-split `a = b` representing `iff`. -/ theorem of_eq_eq_true {a b : Prop} (h : (a = b) = True) : (¬a ∨ b) ∧ (¬b ∨ a) := by by_cases a <;> by_cases b <;> simp_all From dfa3949f169d4e3296144fd1379eeefac86e1719 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2025 17:56:58 -0800 Subject: [PATCH 6/7] chore: helper functions --- src/Lean/Meta/Tactic/Grind/Types.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 48ddf0508c41..85f97eb6a92d 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -684,6 +684,14 @@ def pushEqTrue (a proof : Expr) : GoalM Unit := do def pushEqFalse (a proof : Expr) : GoalM Unit := do pushEq a (← getFalseExpr) proof +/-- Pushes `a = Bool.true` with `proof` to `newEqs`. -/ +def pushEqBoolTrue (a proof : Expr) : GoalM Unit := do + pushEq a (← getBoolTrueExpr) proof + +/-- Pushes `a = Bool.false` with `proof` to `newEqs`. -/ +def pushEqBoolFalse (a proof : Expr) : GoalM Unit := do + pushEq a (← getBoolFalseExpr) proof + /-- Records that `parent` is a parent of `child`. This function actually stores the information in the root (aka canonical representative) of `child`. From 852c523720350d5df49ca97a16308bfdd92b9c3a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2025 18:21:11 -0800 Subject: [PATCH 7/7] feat: propagate `Bool.and`, `Bool.or`, and `Bool.and` --- src/Lean/Meta/Tactic/Grind/Propagate.lean | 60 +++++++++++++++++++++++ tests/lean/run/grind_bool_prop.lean | 19 +++++++ 2 files changed, 79 insertions(+) create mode 100644 tests/lean/run/grind_bool_prop.lean diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean index 0ef4b89c19bb..5d62ae873419 100644 --- a/src/Lean/Meta/Tactic/Grind/Propagate.lean +++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean @@ -223,4 +223,64 @@ builtin_grind_propagator propagateDecideUp ↑decide := fun e => do else if (← isEqFalse p) then pushEq e (← getBoolFalseExpr) <| mkApp3 (mkConst ``Grind.decide_eq_false) p h (← mkEqFalseProof p) +/-- `Bool` version of `propagateAndUp` -/ +builtin_grind_propagator propagateBoolAndUp ↑Bool.and := fun e => do + let_expr Bool.and a b := e | return () + if (← isEqBoolTrue a) then + pushEq e b <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_true_left) a b (← mkEqBoolTrueProof a) + else if (← isEqBoolTrue b) then + pushEq e a <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_true_right) a b (← mkEqBoolTrueProof b) + else if (← isEqBoolFalse a) then + pushEqBoolFalse e <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_false_left) a b (← mkEqBoolFalseProof a) + else if (← isEqBoolFalse b) then + pushEqBoolFalse e <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_false_right) a b (← mkEqBoolFalseProof b) + +/-- `Bool` version of `propagateAndDown` -/ +builtin_grind_propagator propagateBoolAndDown ↓Bool.and := fun e => do + if (← isEqBoolTrue e) then + let_expr Bool.and a b := e | return () + let h ← mkEqBoolTrueProof e + pushEqBoolTrue a <| mkApp3 (mkConst ``Grind.Bool.eq_true_of_and_eq_true_left) a b h + pushEqBoolTrue b <| mkApp3 (mkConst ``Grind.Bool.eq_true_of_and_eq_true_right) a b h + +/-- `Bool` version of `propagateOrUp` -/ +builtin_grind_propagator propagateBoolOrUp ↑Bool.or := fun e => do + let_expr Bool.or a b := e | return () + if (← isEqBoolFalse a) then + pushEq e b <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_false_left) a b (← mkEqBoolFalseProof a) + else if (← isEqBoolFalse b) then + pushEq e a <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_false_right) a b (← mkEqBoolFalseProof b) + else if (← isEqBoolTrue a) then + pushEqBoolTrue e <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_true_left) a b (← mkEqBoolTrueProof a) + else if (← isEqBoolTrue b) then + pushEqBoolTrue e <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_true_right) a b (← mkEqBoolTrueProof b) + +/-- `Bool` version of `propagateOrDown` -/ +builtin_grind_propagator propagateBoolOrDown ↓Bool.or := fun e => do + if (← isEqBoolFalse e) then + let_expr Bool.or a b := e | return () + let h ← mkEqBoolFalseProof e + pushEqBoolFalse a <| mkApp3 (mkConst ``Grind.Bool.eq_false_of_or_eq_false_left) a b h + pushEqBoolFalse b <| mkApp3 (mkConst ``Grind.Bool.eq_false_of_or_eq_false_right) a b h + +/-- `Bool` version of `propagateNotUp` -/ +builtin_grind_propagator propagateBoolNotUp ↑Bool.not := fun e => do + let_expr Bool.not a := e | return () + if (← isEqBoolFalse a) then + pushEqBoolTrue e <| mkApp2 (mkConst ``Grind.Bool.not_eq_of_eq_false) a (← mkEqBoolFalseProof a) + else if (← isEqBoolTrue a) then + pushEqBoolFalse e <| mkApp2 (mkConst ``Grind.Bool.not_eq_of_eq_true) a (← mkEqBoolTrueProof a) + else if (← isEqv e a) then + closeGoal <| mkApp2 (mkConst ``Grind.Bool.false_of_not_eq_self) a (← mkEqProof e a) + +/-- `Bool` version of `propagateNotDown` -/ +builtin_grind_propagator propagateBoolNotDown ↓Bool.not := fun e => do + let_expr Bool.not a := e | return () + if (← isEqBoolFalse e) then + pushEqBoolTrue a <| mkApp2 (mkConst ``Grind.Bool.eq_true_of_not_eq_false) a (← mkEqBoolFalseProof e) + else if (← isEqBoolTrue e) then + pushEqBoolFalse a <| mkApp2 (mkConst ``Grind.Bool.eq_false_of_not_eq_true) a (← mkEqBoolTrueProof e) + else if (← isEqv e a) then + closeGoal <| mkApp2 (mkConst ``Grind.Bool.false_of_not_eq_self) a (← mkEqProof e a) + end Lean.Meta.Grind diff --git a/tests/lean/run/grind_bool_prop.lean b/tests/lean/run/grind_bool_prop.lean new file mode 100644 index 000000000000..275064a4fc27 --- /dev/null +++ b/tests/lean/run/grind_bool_prop.lean @@ -0,0 +1,19 @@ +example (f : Bool → Nat) : f (a && b) = 0 → a = false → f false = 0 := by grind (splits := 0) +example (f : Bool → Nat) : f (a && b) = 0 → b = false → f false = 0 := by grind (splits := 0) +example (f : Bool → Nat) : f (a && b) = 0 → a = true → f b = 0 := by grind (splits := 0) +example (f : Bool → Nat) : f (a && b) = 0 → b = true → f a = 0 := by grind (splits := 0) +example (f : Bool → Nat) : (a && b) = c → c = true → f a = 0 → f true = 0 := by grind (splits := 0) +example (f : Bool → Nat) : (a && b) = c → c = true → f b = 0 → f true = 0 := by grind (splits := 0) + +example (f : Bool → Nat) : f (a || b) = 0 → a = false → f b = 0 := by grind (splits := 0) +example (f : Bool → Nat) : f (a || b) = 0 → b = false → f a = 0 := by grind (splits := 0) +example (f : Bool → Nat) : f (a || b) = 0 → a = true → f true = 0 := by grind (splits := 0) +example (f : Bool → Nat) : f (a || b) = 0 → b = true → f true = 0 := by grind (splits := 0) +example (f : Bool → Nat) : (a || b) = c → c = false → f a = 0 → f false = 0 := by grind (splits := 0) +example (f : Bool → Nat) : (a || b) = c → c = false → f b = 0 → f false = 0 := by grind (splits := 0) + +example (f : Bool → Nat) : f (!a) = 0 → a = true → f false = 0 := by grind (splits := 0) +example (f : Bool → Nat) : f (!a) = 0 → a = false → f true = 0 := by grind (splits := 0) +example (f : Bool → Nat) : (!a) = c → c = true → f a = 0 → f false = 0 := by grind (splits := 0) +example (f : Bool → Nat) : (!a) = c → c = false → f a = 0 → f true = 0 := by grind (splits := 0) +example : (!a) = c → c = a → False := by grind (splits := 0)