feat: Bool.and, Bool.or, and Bool.not propagation in grind (#6861)
This PR adds propagation rules for `Bool.and`, `Bool.or`, and `Bool.not` to the `grind` tactic.
This commit is contained in:
Leonardo de Moura
GitHub
parent
5b1c6b558a
commit
e922edfc21
5 changed files with 168 additions and 49 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -678,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`.
|
||||
|
|
@ -837,6 +851,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
|
||||
|
|
|
|||
19
tests/lean/run/grind_bool_prop.lean
Normal file
19
tests/lean/run/grind_bool_prop.lean
Normal file
|
|
@ -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)
|
||||
|
|
@ -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]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue