chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508)
This adds a number of lemmas for simplification of `Bool` and `Prop` terms. It pulls lemmas from Mathlib and adds additional lemmas where confluence or consistency suggested they are needed. It has been tested against Mathlib using some automated test infrastructure. That testing module is not yet included in this PR, but will be included as part of this. Note. There are currently some comments saying the origin of the simp rule. These will be removed prior to merging, but are added to clarify where the rule came from during review. --------- Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This commit is contained in:
Joe Hendrix
GitHub
parent
37450d47e2
commit
01104cc81e
17 changed files with 2017 additions and 137 deletions
|
|
@ -277,14 +277,13 @@ theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
|
|||
. by_cases' key < k
|
||||
cases h; apply ihr; assumption
|
||||
|
||||
theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
|
||||
theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
|
||||
: (b.insert k v).find? k' = b.find? k' := by
|
||||
let ⟨t, h⟩ := b; simp
|
||||
induction t with simp
|
||||
| leaf =>
|
||||
intros
|
||||
have_eq k k'
|
||||
contradiction
|
||||
intros le
|
||||
exact Nat.lt_of_le_of_ne le ne
|
||||
| node left key value right ihl ihr =>
|
||||
let .node hl hr bl br := h
|
||||
specialize ihl bl
|
||||
|
|
|
|||
|
|
@ -37,15 +37,6 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
|
|||
f (ite P x y) = ite P (f x) (f y) :=
|
||||
apply_dite f P (fun _ => x) (fun _ => y)
|
||||
|
||||
/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
|
||||
@[simp] theorem dite_not (P : Prop) {_ : Decidable P} (x : ¬P → α) (y : ¬¬P → α) :
|
||||
dite (¬P) x y = dite P (fun h => y (not_not_intro h)) x := by
|
||||
by_cases h : P <;> simp [h]
|
||||
|
||||
/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
|
||||
@[simp] theorem ite_not (P : Prop) {_ : Decidable P} (x y : α) : ite (¬P) x y = ite P y x :=
|
||||
dite_not P (fun _ => x) (fun _ => y)
|
||||
|
||||
@[simp] theorem dite_eq_left_iff {P : Prop} [Decidable P] {B : ¬ P → α} :
|
||||
dite P (fun _ => a) B = a ↔ ∀ h, B h = a := by
|
||||
by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
|
||||
|
|
|
|||
|
|
@ -125,16 +125,15 @@ theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
|
|||
/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
|
||||
The left-to-right direction, double negation elimination (DNE),
|
||||
is classically true but not constructively. -/
|
||||
@[scoped simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
|
||||
@[simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
|
||||
|
||||
@[simp] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
|
||||
@[simp low] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
|
||||
|
||||
theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
|
||||
theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not
|
||||
|
||||
theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
|
||||
rw [← not_forall]; exact em _
|
||||
|
||||
theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
|
||||
rw [← not_exists]; exact em _
|
||||
|
||||
|
|
@ -147,8 +146,22 @@ theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_an
|
|||
|
||||
theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
|
||||
|
||||
@[simp] theorem imp_iff_left_iff : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff
|
||||
@[simp] theorem imp_iff_right_iff : (a → b ↔ b) ↔ a ∨ b := Decidable.imp_iff_right_iff
|
||||
|
||||
@[simp] theorem and_or_imp : a ∧ b ∨ (a → c) ↔ a → b ∨ c := Decidable.and_or_imp
|
||||
|
||||
@[simp] theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
|
||||
|
||||
@[simp] theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q :=
|
||||
Iff.intro (fun (a : _ ∧ _) => (Classical.em p).rec a.left a.right)
|
||||
(fun a => And.intro (fun _ => a) (fun _ => a))
|
||||
|
||||
end Classical
|
||||
|
||||
/- Export for Mathlib compat. -/
|
||||
export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
|
||||
|
||||
/-- Extract an element from a existential statement, using `Classical.choose`. -/
|
||||
-- This enables projection notation.
|
||||
@[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P
|
||||
|
|
|
|||
|
|
@ -677,7 +677,7 @@ You can prove theorems about the resulting element by induction on `h`, since
|
|||
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
|
||||
h₁ ▸ h₂
|
||||
|
||||
theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
|
||||
@[simp] theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
|
||||
rfl
|
||||
|
||||
/--
|
||||
|
|
@ -1403,9 +1403,9 @@ theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro Fals
|
|||
|
||||
theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro
|
||||
|
||||
@[simp] theorem imp_self : (a → a) ↔ True := iff_true_intro id
|
||||
@[simp high] theorem imp_self : (a → a) ↔ True := iff_true_intro id
|
||||
|
||||
theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
|
||||
@[simp] theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
|
||||
|
||||
theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip
|
||||
|
||||
|
|
|
|||
|
|
@ -29,6 +29,8 @@ instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ x, p x) :
|
|||
| _, isTrue hf => isTrue ⟨_, hf⟩
|
||||
| isFalse ht, isFalse hf => isFalse fun | ⟨true, h⟩ => absurd h ht | ⟨false, h⟩ => absurd h hf
|
||||
|
||||
@[simp] theorem default_bool : default = false := rfl
|
||||
|
||||
instance : LE Bool := ⟨(. → .)⟩
|
||||
instance : LT Bool := ⟨(!. && .)⟩
|
||||
|
||||
|
|
@ -48,85 +50,202 @@ theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide
|
|||
|
||||
theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
|
||||
|
||||
@[simp] theorem decide_eq_true {b : Bool} : decide (b = true) = b := by cases b <;> simp
|
||||
@[simp] theorem decide_eq_false {b : Bool} : decide (b = false) = !b := by cases b <;> simp
|
||||
@[simp] theorem decide_true_eq {b : Bool} : decide (true = b) = b := by cases b <;> simp
|
||||
@[simp] theorem decide_false_eq {b : Bool} : decide (false = b) = !b := by cases b <;> simp
|
||||
@[simp] theorem decide_eq_true {b : Bool} [Decidable (b = true)] : decide (b = true) = b := by cases b <;> simp
|
||||
@[simp] theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b := by cases b <;> simp
|
||||
@[simp] theorem decide_true_eq {b : Bool} [Decidable (true = b)] : decide (true = b) = b := by cases b <;> simp
|
||||
@[simp] theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
|
||||
|
||||
/-! ### and -/
|
||||
|
||||
@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
|
||||
@[simp] theorem and_self_left : ∀(a b : Bool), (a && (a && b)) = (a && b) := by decide
|
||||
@[simp] theorem and_self_right : ∀(a b : Bool), ((a && b) && b) = (a && b) := by decide
|
||||
|
||||
@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
|
||||
@[simp] theorem and_not_self : ∀ (x : Bool), (x && !x) = false := by decide
|
||||
|
||||
/-
|
||||
Added for confluence with `not_and_self` `and_not_self` on term
|
||||
`(b && !b) = true` due to reductions:
|
||||
|
||||
1. `(b = true ∨ !b = true)` via `Bool.and_eq_true`
|
||||
2. `false = true` via `Bool.and_not_self`
|
||||
-/
|
||||
@[simp] theorem eq_true_and_eq_false_self : ∀(b : Bool), (b = true ∧ b = false) ↔ False := by decide
|
||||
@[simp] theorem eq_false_and_eq_true_self : ∀(b : Bool), (b = false ∧ b = true) ↔ False := by decide
|
||||
|
||||
theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by decide
|
||||
|
||||
theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z)) := by decide
|
||||
|
||||
theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y) := by decide
|
||||
|
||||
theorem and_or_distrib_left : ∀ (x y z : Bool), (x && (y || z)) = ((x && y) || (x && z)) := by
|
||||
decide
|
||||
/-
|
||||
Bool version `and_iff_left_iff_imp`.
|
||||
|
||||
theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = ((x && z) || (y && z)) := by
|
||||
decide
|
||||
|
||||
theorem and_xor_distrib_left : ∀ (x y z : Bool), (x && xor y z) = xor (x && y) (x && z) := by decide
|
||||
|
||||
theorem and_xor_distrib_right : ∀ (x y z : Bool), (xor x y && z) = xor (x && z) (y && z) := by
|
||||
decide
|
||||
|
||||
/-- De Morgan's law for boolean and -/
|
||||
theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide
|
||||
|
||||
theorem and_eq_true_iff : ∀ (x y : Bool), (x && y) = true ↔ x = true ∧ y = true := by decide
|
||||
|
||||
theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by decide
|
||||
Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` via
|
||||
`Bool.coe_iff_coe` and `a → b` via `Bool.and_eq_true` and
|
||||
`and_iff_left_iff_imp`.
|
||||
-/
|
||||
@[simp] theorem and_iff_left_iff_imp : ∀(a b : Bool), ((a && b) = a) ↔ (a → b) := by decide
|
||||
@[simp] theorem and_iff_right_iff_imp : ∀(a b : Bool), ((a && b) = b) ↔ (b → a) := by decide
|
||||
@[simp] theorem iff_self_and : ∀(a b : Bool), (a = (a && b)) ↔ (a → b) := by decide
|
||||
@[simp] theorem iff_and_self : ∀(a b : Bool), (b = (a && b)) ↔ (b → a) := by decide
|
||||
|
||||
/-! ### or -/
|
||||
|
||||
@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide
|
||||
@[simp] theorem or_self_left : ∀(a b : Bool), (a || (a || b)) = (a || b) := by decide
|
||||
@[simp] theorem or_self_right : ∀(a b : Bool), ((a || b) || b) = (a || b) := by decide
|
||||
|
||||
@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide
|
||||
@[simp] theorem or_not_self : ∀ (x : Bool), (x || !x) = true := by decide
|
||||
|
||||
/-
|
||||
Added for confluence with `not_or_self` `or_not_self` on term
|
||||
`(b || !b) = true` due to reductions:
|
||||
1. `(b = true ∨ !b = true)` via `Bool.or_eq_true`
|
||||
2. `true = true` via `Bool.or_not_self`
|
||||
-/
|
||||
@[simp] theorem eq_true_or_eq_false_self : ∀(b : Bool), (b = true ∨ b = false) ↔ True := by decide
|
||||
@[simp] theorem eq_false_or_eq_true_self : ∀(b : Bool), (b = false ∨ b = true) ↔ True := by decide
|
||||
|
||||
/-
|
||||
Bool version `or_iff_left_iff_imp`.
|
||||
|
||||
Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` via
|
||||
`Bool.coe_iff_coe` and `a → b` via `Bool.or_eq_true` and
|
||||
`and_iff_left_iff_imp`.
|
||||
-/
|
||||
@[simp] theorem or_iff_left_iff_imp : ∀(a b : Bool), ((a || b) = a) ↔ (b → a) := by decide
|
||||
@[simp] theorem or_iff_right_iff_imp : ∀(a b : Bool), ((a || b) = b) ↔ (a → b) := by decide
|
||||
@[simp] theorem iff_self_or : ∀(a b : Bool), (a = (a || b)) ↔ (b → a) := by decide
|
||||
@[simp] theorem iff_or_self : ∀(a b : Bool), (b = (a || b)) ↔ (a → b) := by decide
|
||||
|
||||
theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
|
||||
|
||||
theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z)) := by decide
|
||||
|
||||
theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y) := by decide
|
||||
|
||||
theorem or_and_distrib_left : ∀ (x y z : Bool), (x || (y && z)) = ((x || y) && (x || z)) := by
|
||||
decide
|
||||
/-! ### distributivity -/
|
||||
|
||||
theorem or_and_distrib_right : ∀ (x y z : Bool), ((x && y) || z) = ((x || z) && (y || z)) := by
|
||||
decide
|
||||
theorem and_or_distrib_left : ∀ (x y z : Bool), (x && (y || z)) = (x && y || x && z) := by decide
|
||||
theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = (x && z || y && z) := by decide
|
||||
|
||||
theorem or_and_distrib_left : ∀ (x y z : Bool), (x || y && z) = ((x || y) && (x || z)) := by decide
|
||||
theorem or_and_distrib_right : ∀ (x y z : Bool), (x && y || z) = ((x || z) && (y || z)) := by decide
|
||||
|
||||
/-- De Morgan's law for boolean and -/
|
||||
@[simp] theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide
|
||||
|
||||
/-- De Morgan's law for boolean or -/
|
||||
theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by decide
|
||||
@[simp] theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by decide
|
||||
|
||||
theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
|
||||
theorem and_eq_true_iff (x y : Bool) : (x && y) = true ↔ x = true ∧ y = true :=
|
||||
Iff.of_eq (and_eq_true x y)
|
||||
|
||||
theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
|
||||
theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by decide
|
||||
|
||||
/-
|
||||
New simp rule that replaces `Bool.and_eq_false_eq_eq_false_or_eq_false` in
|
||||
Mathlib due to confluence:
|
||||
|
||||
Consider the term: `¬((b && c) = true)`:
|
||||
|
||||
1. Reduces to `((b && c) = false)` via `Bool.not_eq_true`
|
||||
2. Reduces to `¬(b = true ∧ c = true)` via `Bool.and_eq_true`.
|
||||
|
||||
|
||||
1. Further reduces to `b = false ∨ c = false` via `Bool.and_eq_false_eq_eq_false_or_eq_false`.
|
||||
2. Further reduces to `b = true → c = false` via `not_and` and `Bool.not_eq_true`.
|
||||
-/
|
||||
@[simp] theorem and_eq_false_imp : ∀ (x y : Bool), (x && y) = false ↔ (x = true → y = false) := by decide
|
||||
|
||||
@[simp] theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
|
||||
|
||||
@[simp] theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
|
||||
|
||||
/-! ### eq/beq/bne -/
|
||||
|
||||
/--
|
||||
These two rules follow trivially by simp, but are needed to avoid non-termination
|
||||
in false_eq and true_eq.
|
||||
-/
|
||||
@[simp] theorem false_eq_true : (false = true) = False := by simp
|
||||
@[simp] theorem true_eq_false : (true = false) = False := by simp
|
||||
|
||||
-- The two lemmas below normalize terms with a constant to the
|
||||
-- right-hand side but risk non-termination if `false_eq_true` and
|
||||
-- `true_eq_false` are disabled.
|
||||
@[simp low] theorem false_eq (b : Bool) : (false = b) = (b = false) := by
|
||||
cases b <;> simp
|
||||
|
||||
@[simp low] theorem true_eq (b : Bool) : (true = b) = (b = true) := by
|
||||
cases b <;> simp
|
||||
|
||||
@[simp] theorem true_beq : ∀b, (true == b) = b := by decide
|
||||
@[simp] theorem false_beq : ∀b, (false == b) = !b := by decide
|
||||
@[simp] theorem beq_true : ∀b, (b == true) = b := by decide
|
||||
@[simp] theorem beq_false : ∀b, (b == false) = !b := by decide
|
||||
|
||||
@[simp] theorem true_bne : ∀(b : Bool), (true != b) = !b := by decide
|
||||
@[simp] theorem false_bne : ∀(b : Bool), (false != b) = b := by decide
|
||||
@[simp] theorem bne_true : ∀(b : Bool), (b != true) = !b := by decide
|
||||
@[simp] theorem bne_false : ∀(b : Bool), (b != false) = b := by decide
|
||||
|
||||
@[simp] theorem not_beq_self : ∀ (x : Bool), ((!x) == x) = false := by decide
|
||||
@[simp] theorem beq_not_self : ∀ (x : Bool), (x == !x) = false := by decide
|
||||
|
||||
@[simp] theorem not_bne_self : ∀ (x : Bool), ((!x) != x) = true := by decide
|
||||
@[simp] theorem bne_not_self : ∀ (x : Bool), (x != !x) = true := by decide
|
||||
|
||||
/-
|
||||
Added for equivalence with `Bool.not_beq_self` and needed for confluence
|
||||
due to `beq_iff_eq`.
|
||||
-/
|
||||
@[simp] theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False := by decide
|
||||
@[simp] theorem eq_not_self : ∀(b : Bool), (b = (!b)) ↔ False := by decide
|
||||
|
||||
@[simp] theorem beq_self_left : ∀(a b : Bool), (a == (a == b)) = b := by decide
|
||||
@[simp] theorem beq_self_right : ∀(a b : Bool), ((a == b) == b) = a := by decide
|
||||
@[simp] theorem bne_self_left : ∀(a b : Bool), (a != (a != b)) = b := by decide
|
||||
@[simp] theorem bne_self_right : ∀(a b : Bool), ((a != b) != b) = a := by decide
|
||||
|
||||
@[simp] theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
|
||||
|
||||
@[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
|
||||
|
||||
@[simp] theorem bne_left_inj : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
|
||||
@[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide
|
||||
|
||||
/-! ### coercision related normal forms -/
|
||||
|
||||
@[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
|
||||
|
||||
@[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide
|
||||
|
||||
@[simp] theorem coe_iff_coe : ∀(a b : Bool), (a ↔ b) ↔ a = b := by decide
|
||||
|
||||
@[simp] theorem coe_true_iff_false : ∀(a b : Bool), (a ↔ b = false) ↔ a = (!b) := by decide
|
||||
@[simp] theorem coe_false_iff_true : ∀(a b : Bool), (a = false ↔ b) ↔ (!a) = b := by decide
|
||||
@[simp] theorem coe_false_iff_false : ∀(a b : Bool), (a = false ↔ b = false) ↔ (!a) = (!b) := by decide
|
||||
|
||||
/-! ### xor -/
|
||||
|
||||
@[simp] theorem false_xor : ∀ (x : Bool), xor false x = x := by decide
|
||||
theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne
|
||||
|
||||
@[simp] theorem xor_false : ∀ (x : Bool), xor x false = x := by decide
|
||||
theorem xor_false : ∀ (x : Bool), xor x false = x := bne_false
|
||||
|
||||
@[simp] theorem true_xor : ∀ (x : Bool), xor true x = !x := by decide
|
||||
theorem true_xor : ∀ (x : Bool), xor true x = !x := true_bne
|
||||
|
||||
@[simp] theorem xor_true : ∀ (x : Bool), xor x true = !x := by decide
|
||||
theorem xor_true : ∀ (x : Bool), xor x true = !x := bne_true
|
||||
|
||||
@[simp] theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := by decide
|
||||
theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := not_bne_self
|
||||
|
||||
@[simp] theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := by decide
|
||||
theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := bne_not_self
|
||||
|
||||
theorem not_xor : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by decide
|
||||
|
||||
theorem xor_not : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by decide
|
||||
|
||||
@[simp] theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := by decide
|
||||
theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := not_bne_not
|
||||
|
||||
theorem xor_self : ∀ (x : Bool), xor x x = false := by decide
|
||||
|
||||
|
|
@ -136,13 +255,11 @@ theorem xor_left_comm : ∀ (x y z : Bool), xor x (xor y z) = xor y (xor x z) :=
|
|||
|
||||
theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y := by decide
|
||||
|
||||
theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := by decide
|
||||
theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := bne_assoc
|
||||
|
||||
@[simp]
|
||||
theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := by decide
|
||||
theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := bne_left_inj
|
||||
|
||||
@[simp]
|
||||
theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := by decide
|
||||
theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := bne_right_inj
|
||||
|
||||
/-! ### le/lt -/
|
||||
|
||||
|
|
@ -227,16 +344,147 @@ theorem toNat_lt (b : Bool) : b.toNat < 2 :=
|
|||
|
||||
@[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by
|
||||
cases b <;> simp
|
||||
@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by
|
||||
@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by
|
||||
cases b <;> simp
|
||||
|
||||
end Bool
|
||||
/-! ### ite -/
|
||||
|
||||
@[simp] theorem if_true_left (p : Prop) [h : Decidable p] (f : Bool) :
|
||||
(ite p true f) = (p || f) := by cases h with | _ p => simp [p]
|
||||
|
||||
@[simp] theorem if_false_left (p : Prop) [h : Decidable p] (f : Bool) :
|
||||
(ite p false f) = (!p && f) := by cases h with | _ p => simp [p]
|
||||
|
||||
@[simp] theorem if_true_right (p : Prop) [h : Decidable p] (t : Bool) :
|
||||
(ite p t true) = (!(p : Bool) || t) := by cases h with | _ p => simp [p]
|
||||
|
||||
@[simp] theorem if_false_right (p : Prop) [h : Decidable p] (t : Bool) :
|
||||
(ite p t false) = (p && t) := by cases h with | _ p => simp [p]
|
||||
|
||||
@[simp] theorem ite_eq_true_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
|
||||
(ite p t f = true) = ite p (t = true) (f = true) := by
|
||||
cases h with | _ p => simp [p]
|
||||
|
||||
@[simp] theorem ite_eq_false_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
|
||||
(ite p t f = false) = ite p (t = false) (f = false) := by
|
||||
cases h with | _ p => simp [p]
|
||||
|
||||
/-
|
||||
`not_ite_eq_true_eq_true` and related theorems below are added for
|
||||
non-confluence. A motivating example is
|
||||
`¬((if u then b else c) = true)`.
|
||||
|
||||
This reduces to:
|
||||
1. `¬((if u then (b = true) else (c = true))` via `ite_eq_true_distrib`
|
||||
2. `(if u then b c) = false)` via `Bool.not_eq_true`.
|
||||
|
||||
Similar logic holds for `¬((if u then b else c) = false)` and related
|
||||
lemmas.
|
||||
-/
|
||||
|
||||
@[simp]
|
||||
theorem not_ite_eq_true_eq_true (p : Prop) [h : Decidable p] (b c : Bool) :
|
||||
¬(ite p (b = true) (c = true)) ↔ (ite p (b = false) (c = false)) := by
|
||||
cases h with | _ p => simp [p]
|
||||
|
||||
@[simp]
|
||||
theorem not_ite_eq_false_eq_false (p : Prop) [h : Decidable p] (b c : Bool) :
|
||||
¬(ite p (b = false) (c = false)) ↔ (ite p (b = true) (c = true)) := by
|
||||
cases h with | _ p => simp [p]
|
||||
|
||||
@[simp]
|
||||
theorem not_ite_eq_true_eq_false (p : Prop) [h : Decidable p] (b c : Bool) :
|
||||
¬(ite p (b = true) (c = false)) ↔ (ite p (b = false) (c = true)) := by
|
||||
cases h with | _ p => simp [p]
|
||||
|
||||
@[simp]
|
||||
theorem not_ite_eq_false_eq_true (p : Prop) [h : Decidable p] (b c : Bool) :
|
||||
¬(ite p (b = false) (c = true)) ↔ (ite p (b = true) (c = false)) := by
|
||||
cases h with | _ p => simp [p]
|
||||
|
||||
/-
|
||||
Added for confluence between `if_true_left` and `ite_false_same` on
|
||||
`if b = true then True else b = true`
|
||||
-/
|
||||
@[simp] theorem eq_false_imp_eq_true : ∀(b:Bool), (b = false → b = true) ↔ (b = true) := by decide
|
||||
|
||||
/-
|
||||
Added for confluence between `if_true_left` and `ite_false_same` on
|
||||
`if b = false then True else b = false`
|
||||
-/
|
||||
@[simp] theorem eq_true_imp_eq_false : ∀(b:Bool), (b = true → b = false) ↔ (b = false) := by decide
|
||||
|
||||
|
||||
/-! ### cond -/
|
||||
|
||||
theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := by
|
||||
theorem cond_eq_ite {α} (b : Bool) (t e : α) : cond b t e = if b then t else e := by
|
||||
cases b <;> simp
|
||||
|
||||
theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := cond_eq_ite b x y
|
||||
|
||||
@[simp] theorem cond_not (b : Bool) (t e : α) : cond (!b) t e = cond b e t := by
|
||||
cases b <;> rfl
|
||||
|
||||
@[simp] theorem cond_self (c : Bool) (t : α) : cond c t t = t := by cases c <;> rfl
|
||||
|
||||
/-
|
||||
This is a simp rule in Mathlib, but results in non-confluence that is
|
||||
difficult to fix as decide distributes over propositions.
|
||||
|
||||
A possible fix would be to completely simplify away `cond`, but that
|
||||
is not taken since it could result in major rewriting of code that is
|
||||
otherwise purely about `Bool`.
|
||||
-/
|
||||
theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) :
|
||||
cond (decide p) t e = if p then t else e := by
|
||||
simp [cond_eq_ite]
|
||||
|
||||
@[simp] theorem cond_eq_ite_iff (a : Bool) (p : Prop) [h : Decidable p] (x y u v : α) :
|
||||
(cond a x y = ite p u v) ↔ ite a x y = ite p u v := by
|
||||
simp [Bool.cond_eq_ite]
|
||||
|
||||
@[simp] theorem ite_eq_cond_iff (p : Prop) [h : Decidable p] (a : Bool) (x y u v : α) :
|
||||
(ite p x y = cond a u v) ↔ ite p x y = ite a u v := by
|
||||
simp [Bool.cond_eq_ite]
|
||||
|
||||
@[simp] theorem cond_eq_true_distrib : ∀(c t f : Bool),
|
||||
(cond c t f = true) = ite (c = true) (t = true) (f = true) := by
|
||||
decide
|
||||
|
||||
@[simp] theorem cond_eq_false_distrib : ∀(c t f : Bool),
|
||||
(cond c t f = false) = ite (c = true) (t = false) (f = false) := by decide
|
||||
|
||||
protected theorem cond_true {α : Type u} {a b : α} : cond true a b = a := cond_true a b
|
||||
protected theorem cond_false {α : Type u} {a b : α} : cond false a b = b := cond_false a b
|
||||
|
||||
@[simp] theorem cond_true_left : ∀(c f : Bool), cond c true f = ( c || f) := by decide
|
||||
@[simp] theorem cond_false_left : ∀(c f : Bool), cond c false f = (!c && f) := by decide
|
||||
@[simp] theorem cond_true_right : ∀(c t : Bool), cond c t true = (!c || t) := by decide
|
||||
@[simp] theorem cond_false_right : ∀(c t : Bool), cond c t false = ( c && t) := by decide
|
||||
|
||||
@[simp] theorem cond_true_same : ∀(c b : Bool), cond c c b = (c || b) := by decide
|
||||
@[simp] theorem cond_false_same : ∀(c b : Bool), cond c b c = (c && b) := by decide
|
||||
|
||||
/-# decidability -/
|
||||
|
||||
protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true
|
||||
|
||||
@[simp] theorem decide_and (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
|
||||
decide (p ∧ q) = (p && q) := by
|
||||
cases dp with | _ p => simp [p]
|
||||
|
||||
@[simp] theorem decide_or (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q] :
|
||||
decide (p ∨ q) = (p || q) := by
|
||||
cases dp with | _ p => simp [p]
|
||||
|
||||
@[simp] theorem decide_iff_dist (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] :
|
||||
decide (p ↔ q) = (decide p == decide q) := by
|
||||
cases dp with | _ p => simp [p]
|
||||
|
||||
end Bool
|
||||
|
||||
export Bool (cond_eq_if)
|
||||
|
||||
/-! ### decide -/
|
||||
|
||||
@[simp] theorem false_eq_decide_iff {p : Prop} [h : Decidable p] : false = decide p ↔ ¬p := by
|
||||
|
|
|
|||
|
|
@ -687,7 +687,7 @@ decreasing_by decreasing_with
|
|||
|
||||
@[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
(reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
|
||||
rw [reverseInduction]; simp; rfl
|
||||
rw [reverseInduction]; simp
|
||||
|
||||
@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
(i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
|
||||
|
|
|
|||
|
|
@ -69,7 +69,7 @@ theorem mem_cons_self (a : α) (l : List α) : a ∈ a :: l := .head ..
|
|||
theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
|
||||
|
||||
theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
|
||||
cases l <;> simp
|
||||
cases l <;> simp [-not_or]
|
||||
|
||||
/-! ### append -/
|
||||
|
||||
|
|
@ -451,9 +451,9 @@ theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
|
|||
induction as with
|
||||
| nil => simp [filter]
|
||||
| cons a as ih =>
|
||||
by_cases h : p a <;> simp [*, or_and_right]
|
||||
· exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
|
||||
· exact (or_iff_right fun ⟨rfl, h'⟩ => h h').symm
|
||||
by_cases h : p a
|
||||
· simp_all [or_and_left]
|
||||
· simp_all [or_and_right]
|
||||
|
||||
theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
|
||||
simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
|
||||
|
|
|
|||
|
|
@ -256,25 +256,24 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
|
|||
|
||||
theorem testBit_one_zero : testBit 1 0 = true := by trivial
|
||||
|
||||
theorem not_decide_mod_two_eq_one (x : Nat)
|
||||
: (!decide (x % 2 = 1)) = decide (x % 2 = 0) := by
|
||||
cases Nat.mod_two_eq_zero_or_one x <;> (rename_i p; simp [p])
|
||||
|
||||
theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
|
||||
testBit (2^n - (x + 1)) i = (decide (i < n) && ! testBit x i) := by
|
||||
induction i generalizing n x with
|
||||
| zero =>
|
||||
simp only [testBit_zero, zero_eq, Bool.and_eq_true, decide_eq_true_eq,
|
||||
Bool.not_eq_true']
|
||||
match n with
|
||||
| 0 => simp
|
||||
| n+1 =>
|
||||
-- just logic + omega:
|
||||
simp only [zero_lt_succ, decide_True, Bool.true_and]
|
||||
rw [← decide_not, decide_eq_decide]
|
||||
simp [not_decide_mod_two_eq_one]
|
||||
omega
|
||||
| succ i ih =>
|
||||
simp only [testBit_succ]
|
||||
match n with
|
||||
| 0 =>
|
||||
simp only [Nat.pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
|
||||
rw [decide_eq_false] <;> simp
|
||||
simp [decide_eq_false]
|
||||
| n+1 =>
|
||||
rw [Nat.two_pow_succ_sub_succ_div_two, ih]
|
||||
· simp [Nat.succ_lt_succ_iff]
|
||||
|
|
|
|||
|
|
@ -11,6 +11,18 @@ import Init.Core
|
|||
import Init.NotationExtra
|
||||
set_option linter.missingDocs true -- keep it documented
|
||||
|
||||
/-! ## cast and equality -/
|
||||
|
||||
@[simp] theorem eq_mp_eq_cast (h : α = β) : Eq.mp h = cast h := rfl
|
||||
@[simp] theorem eq_mpr_eq_cast (h : α = β) : Eq.mpr h = cast h.symm := rfl
|
||||
|
||||
@[simp] theorem cast_cast : ∀ (ha : α = β) (hb : β = γ) (a : α),
|
||||
cast hb (cast ha a) = cast (ha.trans hb) a
|
||||
| rfl, rfl, _ => rfl
|
||||
|
||||
@[simp] theorem eq_true_eq_id : Eq True = id := by
|
||||
funext _; simp only [true_iff, id.def, eq_iff_iff]
|
||||
|
||||
/-! ## not -/
|
||||
|
||||
theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))
|
||||
|
|
@ -104,10 +116,62 @@ theorem and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := by rw [@or
|
|||
|
||||
theorem or_imp : (a ∨ b → c) ↔ (a → c) ∧ (b → c) :=
|
||||
Iff.intro (fun h => ⟨h ∘ .inl, h ∘ .inr⟩) (fun ⟨ha, hb⟩ => Or.rec ha hb)
|
||||
theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp
|
||||
|
||||
/-
|
||||
`not_or` is made simp for confluence with `¬((b || c) = true)`:
|
||||
|
||||
Critical pair:
|
||||
1. `¬(b = true ∨ c = true)` via `Bool.or_eq_true`.
|
||||
2. `(b || c = false)` via `Bool.not_eq_true` which then
|
||||
reduces to `b = false ∧ c = false` via Mathlib simp lemma
|
||||
`Bool.or_eq_false_eq_eq_false_and_eq_false`.
|
||||
|
||||
Both reduce to `b = false ∧ c = false` via `not_or`.
|
||||
-/
|
||||
@[simp] theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp
|
||||
|
||||
theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
|
||||
|
||||
|
||||
/-! ## Ite -/
|
||||
|
||||
@[simp]
|
||||
theorem if_false_left [h : Decidable p] :
|
||||
ite p False q ↔ ¬p ∧ q := by cases h <;> (rename_i g; simp [g])
|
||||
|
||||
@[simp]
|
||||
theorem if_false_right [h : Decidable p] :
|
||||
ite p q False ↔ p ∧ q := by cases h <;> (rename_i g; simp [g])
|
||||
|
||||
/-
|
||||
`if_true_left` and `if_true_right` are lower priority because
|
||||
they introduce disjunctions and we prefer `if_false_left` and
|
||||
`if_false_right` if they overlap.
|
||||
-/
|
||||
|
||||
@[simp low]
|
||||
theorem if_true_left [h : Decidable p] :
|
||||
ite p True q ↔ ¬p → q := by cases h <;> (rename_i g; simp [g])
|
||||
|
||||
@[simp low]
|
||||
theorem if_true_right [h : Decidable p] :
|
||||
ite p q True ↔ p → q := by cases h <;> (rename_i g; simp [g])
|
||||
|
||||
/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
|
||||
@[simp] theorem dite_not [hn : Decidable (¬p)] [h : Decidable p] (x : ¬p → α) (y : ¬¬p → α) :
|
||||
dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x := by
|
||||
cases h <;> (rename_i g; simp [g])
|
||||
|
||||
/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
|
||||
@[simp] theorem ite_not (p : Prop) [Decidable p] (x y : α) : ite (¬p) x y = ite p y x :=
|
||||
dite_not (fun _ => x) (fun _ => y)
|
||||
|
||||
@[simp] theorem ite_true_same (p q : Prop) [h : Decidable p] : (if p then p else q) = (¬p → q) := by
|
||||
cases h <;> (rename_i g; simp [g])
|
||||
|
||||
@[simp] theorem ite_false_same (p q : Prop) [h : Decidable p] : (if p then q else p) = (p ∧ q) := by
|
||||
cases h <;> (rename_i g; simp [g])
|
||||
|
||||
/-! ## exists and forall -/
|
||||
|
||||
section quantifiers
|
||||
|
|
@ -268,7 +332,14 @@ end quantifiers
|
|||
|
||||
/-! ## decidable -/
|
||||
|
||||
theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
|
||||
@[simp] theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
|
||||
|
||||
/-- Excluded middle. Added as alias for Decidable.em -/
|
||||
abbrev Decidable.or_not_self := em
|
||||
|
||||
/-- Excluded middle commuted. Added as alias for Decidable.em -/
|
||||
theorem Decidable.not_or_self (p : Prop) [h : Decidable p] : ¬p ∨ p := by
|
||||
cases h <;> simp [*]
|
||||
|
||||
theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not
|
||||
|
||||
|
|
@ -310,7 +381,7 @@ theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a :=
|
|||
theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) :=
|
||||
⟨not_imp_symm, not_imp_symm⟩
|
||||
|
||||
theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
|
||||
@[simp] theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
|
||||
have := @imp_not_self (¬a); rwa [not_not] at this
|
||||
|
||||
theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ b ↔ (¬a → b) :=
|
||||
|
|
@ -389,8 +460,12 @@ theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔
|
|||
rw [← not_and_iff_or_not_not, not_not]
|
||||
|
||||
theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b :=
|
||||
⟨fun H => (Decidable.em a).imp_right fun ha' => H.1 fun ha => (ha' ha).elim,
|
||||
fun H => H.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb⟩
|
||||
Iff.intro
|
||||
(fun h => (Decidable.em a).imp_right fun ha' => h.mp fun ha => (ha' ha).elim)
|
||||
(fun ab => ab.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb)
|
||||
|
||||
theorem Decidable.imp_iff_left_iff [Decidable a] : (b ↔ a → b) ↔ a ∨ b :=
|
||||
propext (@Iff.comm (a → b) b) ▸ (@Decidable.imp_iff_right_iff a b _)
|
||||
|
||||
theorem Decidable.and_or_imp [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
|
||||
if ha : a then by simp only [ha, true_and, true_imp_iff]
|
||||
|
|
@ -435,3 +510,53 @@ protected theorem Decidable.not_forall_not {p : α → Prop} [Decidable (∃ x,
|
|||
protected theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] :
|
||||
(¬∃ x, ¬p x) ↔ ∀ x, p x := by
|
||||
simp only [not_exists, Decidable.not_not]
|
||||
|
||||
export Decidable (not_imp_self)
|
||||
|
||||
/-
|
||||
`decide_implies` simp justification.
|
||||
|
||||
We have a critical pair from `decide (¬(p ∧ q))`:
|
||||
|
||||
1. `decide (p → ¬q)` via `not_and`
|
||||
2. `!decide (p ∧ q)` via `decide_not` This further refines to
|
||||
`!(decide p) || !(decide q)` via `Bool.decide_and` (in Mathlib) and
|
||||
`Bool.not_and` (made simp in Mathlib).
|
||||
|
||||
We introduce `decide_implies` below and then both normalize to
|
||||
`!(decide p) || !(decide q)`.
|
||||
-/
|
||||
@[simp]
|
||||
theorem decide_implies (u v : Prop)
|
||||
[duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v}
|
||||
: decide (u → v) = dite u (fun h => @decide v (dv h)) (fun _ => true) :=
|
||||
if h : u then by
|
||||
simp [h]
|
||||
else by
|
||||
simp [h]
|
||||
|
||||
/-
|
||||
`decide_ite` is needed to resolve critical pair with
|
||||
|
||||
We have a critical pair from `decide (ite p b c = true)`:
|
||||
|
||||
1. `ite p b c` via `decide_coe`
|
||||
2. `decide (ite p (b = true) (c = true))` via `Bool.ite_eq_true_distrib`.
|
||||
|
||||
We introduce `decide_ite` so both normalize to `ite p b c`.
|
||||
-/
|
||||
@[simp]
|
||||
theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop)
|
||||
[dpq : Decidable (ite u p q)] [dp : Decidable p] [dq : Decidable q] :
|
||||
decide (ite u p q) = ite u (decide p) (decide q) := by
|
||||
cases du <;> simp [*]
|
||||
|
||||
/- Confluence for `ite_true_same` and `decide_ite`. -/
|
||||
@[simp] theorem ite_true_decide_same (p : Prop) [h : Decidable p] (b : Bool) :
|
||||
(if p then decide p else b) = (decide p || b) := by
|
||||
cases h <;> (rename_i pt; simp [pt])
|
||||
|
||||
/- Confluence for `ite_false_same` and `decide_ite`. -/
|
||||
@[simp] theorem ite_false_decide_same (p : Prop) [h : Decidable p] (b : Bool) :
|
||||
(if p then b else decide p) = (decide p && b) := by
|
||||
cases h <;> (rename_i pt; simp [pt])
|
||||
|
|
|
|||
|
|
@ -15,12 +15,15 @@ theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)
|
|||
theorem eq_true (h : p) : p = True :=
|
||||
propext ⟨fun _ => trivial, fun _ => h⟩
|
||||
|
||||
-- Adding this attribute needs `eq_true`.
|
||||
attribute [simp] cast_heq
|
||||
|
||||
theorem eq_false (h : ¬ p) : p = False :=
|
||||
propext ⟨fun h' => absurd h' h, fun h' => False.elim h'⟩
|
||||
|
||||
theorem eq_false' (h : p → False) : p = False := eq_false h
|
||||
|
||||
theorem eq_true_of_decide {p : Prop} {_ : Decidable p} (h : decide p = true) : p = True :=
|
||||
theorem eq_true_of_decide {p : Prop} [Decidable p] (h : decide p = true) : p = True :=
|
||||
eq_true (of_decide_eq_true h)
|
||||
|
||||
theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) : p = False :=
|
||||
|
|
@ -124,6 +127,7 @@ end SimprocHelperLemmas
|
|||
@[simp] theorem not_true_eq_false : (¬ True) = False := by decide
|
||||
|
||||
@[simp] theorem not_iff_self : ¬(¬a ↔ a) | H => iff_not_self H.symm
|
||||
attribute [simp] iff_not_self
|
||||
|
||||
/-! ## and -/
|
||||
|
||||
|
|
@ -173,6 +177,11 @@ theorem or_iff_left_of_imp (hb : b → a) : (a ∨ b) ↔ a := Iff.intro (Or.r
|
|||
@[simp] theorem or_iff_left_iff_imp : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp
|
||||
@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp]
|
||||
|
||||
@[simp] theorem iff_self_or (a b : Prop) : (a ↔ a ∨ b) ↔ (b → a) :=
|
||||
propext (@Iff.comm _ a) ▸ @or_iff_left_iff_imp a b
|
||||
@[simp] theorem iff_or_self (a b : Prop) : (b ↔ a ∨ b) ↔ (a → b) :=
|
||||
propext (@Iff.comm _ b) ▸ @or_iff_right_iff_imp a b
|
||||
|
||||
/-# Bool -/
|
||||
|
||||
@[simp] theorem Bool.or_false (b : Bool) : (b || false) = b := by cases b <;> rfl
|
||||
|
|
@ -199,9 +208,9 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
|
|||
@[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
|
||||
@[simp] theorem Bool.not_true : (!true) = false := by decide
|
||||
@[simp] theorem Bool.not_false : (!false) = true := by decide
|
||||
@[simp] theorem Bool.not_beq_true (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
|
||||
@[simp] theorem Bool.not_beq_true (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
|
||||
@[simp] theorem Bool.not_beq_false (b : Bool) : (!(b == false)) = (b == true) := by cases b <;> rfl
|
||||
@[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
|
||||
@[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
|
||||
@[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
|
||||
|
||||
@[simp] theorem Bool.beq_to_eq (a b : Bool) :
|
||||
|
|
@ -212,11 +221,14 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
|
|||
@[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
|
||||
@[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide
|
||||
|
||||
@[simp] theorem decide_eq_true_eq {_ : Decidable p} : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true
|
||||
@[simp] theorem decide_not {h : Decidable p} : decide (¬ p) = !decide p := by cases h <;> rfl
|
||||
@[simp] theorem not_decide_eq_true {h : Decidable p} : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *]
|
||||
@[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p :=
|
||||
propext <| Iff.intro of_decide_eq_true decide_eq_true
|
||||
@[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
|
||||
cases g <;> (rename_i gp; simp [gp]; rfl)
|
||||
@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by
|
||||
cases h <;> (rename_i hp; simp [decide, hp])
|
||||
|
||||
@[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
|
||||
@[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
|
||||
|
||||
@[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
|
||||
@[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
|
||||
|
|
@ -228,11 +240,29 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
|
|||
@[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
|
||||
|
||||
@[simp] theorem decide_False : decide False = false := rfl
|
||||
@[simp] theorem decide_True : decide True = true := rfl
|
||||
@[simp] theorem decide_True : decide True = true := rfl
|
||||
|
||||
@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
|
||||
simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]
|
||||
|
||||
/-
|
||||
Added for critical pair for `¬((a != b) = true)`
|
||||
|
||||
1. `(a != b) = false` via `Bool.not_eq_true`
|
||||
2. `¬(a ≠ b)` via `bne_iff_ne`
|
||||
|
||||
These will both normalize to `a = b` with the first via `bne_eq_false_iff_eq`.
|
||||
-/
|
||||
@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α]
|
||||
(a b : α) : (a == b) = false ↔ a ≠ b := by
|
||||
rw [ne_eq, ← beq_iff_eq a b]
|
||||
cases a == b <;> decide
|
||||
|
||||
@[simp] theorem bne_eq_false_iff_eq [BEq α] [LawfulBEq α] (a b : α) :
|
||||
(a != b) = false ↔ a = b := by
|
||||
rw [bne, ← beq_iff_eq a b]
|
||||
cases a == b <;> decide
|
||||
|
||||
/-# Nat -/
|
||||
|
||||
@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ prelude
|
|||
import Lean.Elab.Tactic.ElabTerm
|
||||
import Lean.Elab.Command
|
||||
import Lean.Elab.Tactic.Meta
|
||||
import Lean.Meta.CheckTactic
|
||||
|
||||
/-!
|
||||
Commands to validate tactic results.
|
||||
|
|
@ -18,15 +19,6 @@ open Lean.Meta CheckTactic
|
|||
open Lean.Elab.Tactic
|
||||
open Lean.Elab.Command
|
||||
|
||||
private def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
|
||||
let u ← mkFreshLevelMVar
|
||||
let type ← mkFreshExprMVar (some (.sort u))
|
||||
let val ← mkFreshExprMVar (some type)
|
||||
let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
|
||||
if !(← isDefEq goalType extType) then
|
||||
throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
|
||||
pure (val, type, u)
|
||||
|
||||
@[builtin_command_elab Lean.Parser.checkTactic]
|
||||
def elabCheckTactic : CommandElab := fun stx => do
|
||||
let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
|
||||
|
|
@ -34,11 +26,10 @@ def elabCheckTactic : CommandElab := fun stx => do
|
|||
runTermElabM $ fun _vars => do
|
||||
let u ← Lean.Elab.Term.elabTerm t none
|
||||
let type ← inferType u
|
||||
let lvl ← mkFreshLevelMVar
|
||||
let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type u
|
||||
let checkGoalType ← mkCheckGoalType u type
|
||||
let mvar ← mkFreshExprMVar (.some checkGoalType)
|
||||
let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
|
||||
let expTerm ← Lean.Elab.Term.elabTerm result (.some type)
|
||||
let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
|
||||
match goals with
|
||||
| [] =>
|
||||
throwErrorAt stx
|
||||
|
|
@ -51,7 +42,6 @@ def elabCheckTactic : CommandElab := fun stx => do
|
|||
| _ => do
|
||||
throwErrorAt stx
|
||||
m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
|
||||
pure ()
|
||||
|
||||
@[builtin_command_elab Lean.Parser.checkTacticFailure]
|
||||
def elabCheckTacticFailure : CommandElab := fun stx => do
|
||||
|
|
@ -60,8 +50,7 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
|
|||
runTermElabM $ fun _vars => do
|
||||
let val ← Lean.Elab.Term.elabTerm t none
|
||||
let type ← inferType val
|
||||
let lvl ← mkFreshLevelMVar
|
||||
let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type val
|
||||
let checkGoalType ← mkCheckGoalType val type
|
||||
let mvar ← mkFreshExprMVar (.some checkGoalType)
|
||||
let act := Lean.Elab.runTactic mvar.mvarId! tactic.raw
|
||||
match ← try (Term.withoutErrToSorry (some <$> act)) catch _ => pure none with
|
||||
|
|
@ -73,12 +62,12 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
|
|||
pure m!"{indentExpr val}"
|
||||
let msg ←
|
||||
match gls with
|
||||
| [] => pure m!"{tactic} expected to fail on {val}, but closed goal."
|
||||
| [] => pure m!"{tactic} expected to fail on {t}, but closed goal."
|
||||
| [g] =>
|
||||
pure <| m!"{tactic} expected to fail on {val}, but returned: {←ppGoal g}"
|
||||
pure <| m!"{tactic} expected to fail on {t}, but returned: {←ppGoal g}"
|
||||
| gls =>
|
||||
let app m g := do pure <| m ++ (←ppGoal g)
|
||||
let init := m!"{tactic} expected to fail on {val}, but returned goals:"
|
||||
let init := m!"{tactic} expected to fail on {t}, but returned goals:"
|
||||
gls.foldlM (init := init) app
|
||||
throwErrorAt stx msg
|
||||
|
||||
|
|
|
|||
|
|
@ -47,3 +47,4 @@ import Lean.Meta.CoeAttr
|
|||
import Lean.Meta.Iterator
|
||||
import Lean.Meta.LazyDiscrTree
|
||||
import Lean.Meta.LitValues
|
||||
import Lean.Meta.CheckTactic
|
||||
|
|
|
|||
24
src/Lean/Meta/CheckTactic.lean
Normal file
24
src/Lean/Meta/CheckTactic.lean
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
/-
|
||||
Copyright (c) 2024 Lean FRO. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joe Hendrix
|
||||
-/
|
||||
prelude
|
||||
import Lean.Meta.Basic
|
||||
|
||||
namespace Lean.Meta.CheckTactic
|
||||
|
||||
def mkCheckGoalType (val type : Expr) : MetaM Expr := do
|
||||
let lvl ← mkFreshLevelMVar
|
||||
pure <| mkApp2 (mkConst ``CheckGoalType [lvl]) type val
|
||||
|
||||
def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
|
||||
let u ← mkFreshLevelMVar
|
||||
let type ← mkFreshExprMVar (some (.sort u))
|
||||
let val ← mkFreshExprMVar (some type)
|
||||
let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
|
||||
if !(← isDefEq goalType extType) then
|
||||
throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
|
||||
pure (val, type, u)
|
||||
|
||||
end Lean.Meta.CheckTactic
|
||||
|
|
@ -5,32 +5,4 @@
|
|||
?a = ?a
|
||||
with
|
||||
Ordering.eq = Ordering.lt
|
||||
[Meta.Tactic.simp.unify] @forall_exists_index:1000, failed to unify
|
||||
∀ (h : ∃ x, ?p x), ?q h
|
||||
with
|
||||
False → False
|
||||
[Meta.Tactic.simp.unify] @forall_eq:1000, failed to unify
|
||||
∀ (a : ?α), a = ?a' → ?p a
|
||||
with
|
||||
False → False
|
||||
[Meta.Tactic.simp.unify] @forall_eq':1000, failed to unify
|
||||
∀ (a : ?α), ?a' = a → ?p a
|
||||
with
|
||||
False → False
|
||||
[Meta.Tactic.simp.unify] @forall_eq_or_imp:1000, failed to unify
|
||||
∀ (a : ?α), a = ?a' ∨ ?q a → ?p a
|
||||
with
|
||||
False → False
|
||||
[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff:1000, failed to unify
|
||||
∀ (b : ?β) (a : ?α), ?f a = b → ?p b
|
||||
with
|
||||
False → False
|
||||
[Meta.Tactic.simp.unify] @forall_eq_apply_imp_iff:1000, failed to unify
|
||||
∀ (b : ?β) (a : ?α), b = ?f a → ?p b
|
||||
with
|
||||
False → False
|
||||
[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff₂:1000, failed to unify
|
||||
∀ (b : ?β) (a : ?α), ?p a → ?f a = b → ?q b
|
||||
with
|
||||
False → False
|
||||
[Meta.Tactic.simp.rewrite] @imp_self:1000, False → False ==> True
|
||||
[Meta.Tactic.simp.rewrite] @imp_self:10000, False → False ==> True
|
||||
|
|
|
|||
389
tests/lean/bool_simp.lean
Normal file
389
tests/lean/bool_simp.lean
Normal file
|
|
@ -0,0 +1,389 @@
|
|||
variable (p q : Prop)
|
||||
variable (b c d : Bool)
|
||||
variable (u v w : Prop) [Decidable u] [Decidable v] [Decidable w]
|
||||
|
||||
-- Specific regressions found when introducing Boolean normalization
|
||||
#check_simp (b != !c) = false ~> b = !c
|
||||
#check_simp ¬(u → v ∨ w) ~> u ∧ ¬v ∧ ¬w
|
||||
#check_simp decide (u ∧ (v → False)) ~> decide u && !decide v
|
||||
#check_simp decide (cond true b c = true) ~> b
|
||||
#check_simp decide (ite u b c = true) ~> ite u b c
|
||||
#check_simp true ≠ (b || c) ~> b = false ∧ c = false
|
||||
#check_simp ¬((!b = false) ∧ (c = false)) ~> b = true → c = true
|
||||
#check_simp (((!b) && c) ≠ false) ~> b = false ∧ c = true
|
||||
#check_simp (cond b false c ≠ false) ~> b = false ∧ c
|
||||
#check_simp (b && c) = false ~> b → c = false
|
||||
#check_simp (b && c) ≠ false ~> b ∧ c
|
||||
#check_simp decide (u → False) ~> !decide u
|
||||
#check_simp decide (¬u) ~> !decide u
|
||||
#check_simp (b = true) ≠ (c = false) ~> b = c
|
||||
#check_simp (b != c) != (false != d) ~> b != (c != d)
|
||||
#check_simp (b == false) ≠ (c != d) ~> b = (c != d)
|
||||
#check_simp (b = true) ≠ (c = false) ~> b = c
|
||||
#check_simp ¬b = !c ~> b = c
|
||||
#check_simp (b == c) = false ~> ¬(b = c)
|
||||
#check_simp (true ≠ if u then b else c) ~> (if u then b = false else c = false)
|
||||
#check_simp (u ∧ v → False) ~> u → v → False
|
||||
#check_simp (u = (v ≠ w)) ~> (u ↔ ¬(v ↔ w))
|
||||
#check_simp ((b = false) = (c = false)) ~> (!b) = (!c)
|
||||
#check_simp True ≠ (c = false) ~> c = true
|
||||
#check_simp u ∧ u ∧ v ~> u ∧ v
|
||||
#check_simp b || (b || c) ~> b || c
|
||||
#check_simp ((b ≠ c) : Bool) ~> !(decide (b = c))
|
||||
#check_simp ((u ≠ v) : Bool) ~> !((u : Bool) == (v : Bool))
|
||||
#check_simp decide (u → False) ~> !(decide u)
|
||||
#check_simp decide (¬u) ~> !u
|
||||
-- Specific regressions done
|
||||
|
||||
-- Round trip isomorphisms
|
||||
#check_simp (decide (b : Prop)) ~> b
|
||||
#check_simp ((u : Bool) : Prop) ~> u
|
||||
|
||||
/- # not -/
|
||||
|
||||
variable [Decidable u]
|
||||
|
||||
-- Ground
|
||||
#check_simp (¬True) ~> False
|
||||
#check_simp (¬true) ~> False
|
||||
#check_simp (!True) ~> false
|
||||
#check_simp (!true) ~> false
|
||||
|
||||
#check_simp (¬False) ~> True
|
||||
#check_simp (!False) ~> true
|
||||
#check_simp (¬false) ~> True
|
||||
#check_simp (!false) ~> true
|
||||
|
||||
/- # Coercions and not -/
|
||||
|
||||
#check_simp ¬p !~>
|
||||
#check_simp !b !~>
|
||||
|
||||
#check_simp (¬u : Prop) !~>
|
||||
#check_simp (¬u : Bool) ~> !u
|
||||
#check_simp (!u : Prop) ~> ¬u
|
||||
#check_simp (!u : Bool) !~>
|
||||
#check_simp (¬b : Prop) ~> b = false
|
||||
#check_simp (¬b : Bool) ~> !b
|
||||
#check_simp (!b : Prop) ~> b = false
|
||||
#check_simp (!b : Bool) !~>
|
||||
|
||||
#check_simp (¬¬u) ~> u
|
||||
|
||||
/- # and -/
|
||||
|
||||
-- Validate coercions
|
||||
#check_simp (u ∧ v : Prop) !~>
|
||||
#check_simp (u ∧ v : Bool) ~> u && v
|
||||
#check_simp (u && v : Prop) ~> u ∧ v
|
||||
#check_simp (u && v : Bool) !~>
|
||||
#check_simp (b ∧ c : Prop) !~>
|
||||
#check_simp (b ∧ c : Bool) ~> b && c
|
||||
#check_simp (b && c : Prop) ~> b ∧ c
|
||||
#check_simp (b && c : Bool) !~>
|
||||
|
||||
-- Partial evaluation
|
||||
#check_simp (True ∧ v : Prop) ~> v
|
||||
#check_simp (True ∧ v : Bool) ~> (v : Bool)
|
||||
#check_simp (True && v : Prop) ~> v
|
||||
#check_simp (True && v : Bool) ~> (v : Bool)
|
||||
#check_simp (true ∧ c : Prop) ~> (c : Prop)
|
||||
#check_simp (true ∧ c : Bool) ~> c
|
||||
#check_simp (true && c : Prop) ~> (c : Prop)
|
||||
#check_simp (true && c : Bool) ~> c
|
||||
|
||||
#check_simp (u ∧ True : Prop) ~> u
|
||||
#check_simp (u ∧ True : Bool) ~> (u : Bool)
|
||||
#check_simp (u && True : Prop) ~> u
|
||||
#check_simp (u && True : Bool) ~> (u : Bool)
|
||||
#check_simp (b ∧ true : Prop) ~> (b : Prop)
|
||||
#check_simp (b ∧ true : Bool) ~> b
|
||||
#check_simp (b && true : Prop) ~> (b : Prop)
|
||||
#check_simp (b && true : Bool) ~> b
|
||||
|
||||
#check_simp (False ∧ v : Prop) ~> False
|
||||
#check_simp (False ∧ v : Bool) ~> false
|
||||
#check_simp (False && v : Prop) ~> False
|
||||
#check_simp (False && v : Bool) ~> false
|
||||
#check_simp (false ∧ c : Prop) ~> False
|
||||
#check_simp (false ∧ c : Bool) ~> false
|
||||
#check_simp (false && c : Prop) ~> False
|
||||
#check_simp (false && c : Bool) ~> false
|
||||
|
||||
#check_simp (u ∧ False : Prop) ~> False
|
||||
#check_simp (u ∧ False : Bool) ~> false
|
||||
#check_simp (u && False : Prop) ~> False
|
||||
#check_simp (u && False : Bool) ~> false
|
||||
#check_simp (b ∧ false : Prop) ~> False
|
||||
#check_simp (b ∧ false : Bool) ~> false
|
||||
#check_simp (b && false : Prop) ~> False
|
||||
#check_simp (b && false : Bool) ~> false
|
||||
|
||||
-- Idempotence
|
||||
#check_simp (u ∧ u) ~> u
|
||||
#check_simp (u && u) ~> (u : Bool)
|
||||
#check_simp (b ∧ b) ~> (b : Prop)
|
||||
#check_simp (b && b) ~> b
|
||||
|
||||
-- Cancelation
|
||||
#check_simp (u ∧ ¬u) ~> False
|
||||
#check_simp (¬u ∧ u) ~> False
|
||||
#check_simp (b && ¬b) ~> false
|
||||
#check_simp (¬b && b) ~> false
|
||||
|
||||
-- Check we swap operators, but do apply deMorgan etc
|
||||
#check_simp ¬(u ∧ v) ~> u → ¬v
|
||||
#check_simp decide (¬(u ∧ v)) ~> !u || !v
|
||||
#check_simp !(u ∧ v) ~> !u || !v
|
||||
#check_simp ¬(b ∧ c) ~> b → c = false
|
||||
#check_simp !(b ∧ c) ~> !b || !c
|
||||
#check_simp ¬(u && v) ~> u → ¬ v
|
||||
#check_simp ¬(b && c) ~> b = true → c = false
|
||||
#check_simp !(u && v) ~> !u || !v
|
||||
#check_simp !(b && c) ~> !b || !c
|
||||
#check_simp ¬u ∧ ¬v !~>
|
||||
#check_simp ¬b ∧ ¬c ~> ((b = false) ∧ (c = false))
|
||||
#check_simp ¬u && ¬v ~> (!u && !v)
|
||||
#check_simp ¬b && ¬c ~> (!b && !c)
|
||||
|
||||
-- Some ternary test cases
|
||||
#check_simp (u ∧ (v ∧ w) : Prop) !~>
|
||||
#check_simp (u ∧ (v ∧ w) : Bool) ~> (u && (v && w))
|
||||
#check_simp ((u ∧ v) ∧ w : Prop) !~>
|
||||
#check_simp ((u ∧ v) ∧ w : Bool) ~> ((u && v) && w)
|
||||
#check_simp (b && (c && d) : Prop) ~> (b ∧ c ∧ d)
|
||||
#check_simp (b && (c && d) : Bool) !~>
|
||||
#check_simp ((b && c) && d : Prop) ~> ((b ∧ c) ∧ d)
|
||||
#check_simp ((b && c) && d : Bool) !~>
|
||||
|
||||
/- # or -/
|
||||
|
||||
-- Validate coercions
|
||||
#check_simp p ∨ q !~>
|
||||
#check_simp q ∨ p !~>
|
||||
#check_simp (u ∨ v : Prop) !~>
|
||||
#check_simp (u ∨ v : Bool) ~> u || v
|
||||
#check_simp (u || v : Prop) ~> u ∨ v
|
||||
#check_simp (u || v : Bool) !~>
|
||||
#check_simp (b ∨ c : Prop) !~>
|
||||
#check_simp (b ∨ c : Bool) ~> b || c
|
||||
#check_simp (b || c : Prop) ~> b ∨ c
|
||||
#check_simp (b || c : Bool) !~>
|
||||
|
||||
-- Partial evaluation
|
||||
#check_simp (True ∨ v : Prop) ~> True
|
||||
#check_simp (True ∨ v : Bool) ~> true
|
||||
#check_simp (True || v : Prop) ~> True
|
||||
#check_simp (True || v : Bool) ~> true
|
||||
#check_simp (true ∨ c : Prop) ~> True
|
||||
#check_simp (true ∨ c : Bool) ~> true
|
||||
#check_simp (true || c : Prop) ~> True
|
||||
#check_simp (true || c : Bool) ~> true
|
||||
|
||||
#check_simp (u ∨ True : Prop) ~> True
|
||||
#check_simp (u ∨ True : Bool) ~> true
|
||||
#check_simp (u || True : Prop) ~> True
|
||||
#check_simp (u || True : Bool) ~> true
|
||||
#check_simp (b ∨ true : Prop) ~> True
|
||||
#check_simp (b ∨ true : Bool) ~> true
|
||||
#check_simp (b || true : Prop) ~> True
|
||||
#check_simp (b || true : Bool) ~> true
|
||||
|
||||
#check_simp (False ∨ v : Prop) ~> v
|
||||
#check_simp (False ∨ v : Bool) ~> (v : Bool)
|
||||
#check_simp (False || v : Prop) ~> v
|
||||
#check_simp (False || v : Bool) ~> (v : Bool)
|
||||
#check_simp (false ∨ c : Prop) ~> (c : Prop)
|
||||
#check_simp (false ∨ c : Bool) ~> c
|
||||
#check_simp (false || c : Prop) ~> (c : Prop)
|
||||
#check_simp (false || c : Bool) ~> c
|
||||
|
||||
#check_simp (u ∨ False : Prop) ~> u
|
||||
#check_simp (u ∨ False : Bool) ~> (u : Bool)
|
||||
#check_simp (u || False : Prop) ~> u
|
||||
#check_simp (u || False : Bool) ~> (u : Bool)
|
||||
#check_simp (b ∨ false : Prop) ~> (b : Prop)
|
||||
#check_simp (b ∨ false : Bool) ~> b
|
||||
#check_simp (b || false : Prop) ~> (b : Prop)
|
||||
#check_simp (b || false : Bool) ~> b
|
||||
|
||||
-- Idempotence
|
||||
#check_simp (u ∨ u) ~> u
|
||||
#check_simp (u || u) ~> (u : Bool)
|
||||
#check_simp (b ∨ b) ~> (b : Prop)
|
||||
#check_simp (b || b) ~> b
|
||||
|
||||
-- Complement
|
||||
-- Note. We may want to revisit this.
|
||||
-- Decidable excluded middle currently does not simplify.
|
||||
#check_simp ( u ∨ ¬u) !~>
|
||||
#check_simp (¬u ∨ u) !~>
|
||||
#check_simp ( b || ¬b) ~> true
|
||||
#check_simp (¬b || b) ~> true
|
||||
|
||||
-- Check we swap operators, but do apply deMorgan etc
|
||||
#check_simp ¬(u ∨ v) ~> ¬u ∧ ¬v
|
||||
#check_simp !(u ∨ v) ~> !u && !v
|
||||
#check_simp ¬(b ∨ c) ~> b = false ∧ c =false
|
||||
#check_simp !(b ∨ c) ~> !b && !c
|
||||
#check_simp ¬(u || v) ~> ¬u ∧ ¬v
|
||||
#check_simp ¬(b || c) ~> b = false ∧ c = false
|
||||
#check_simp !(u || v) ~> !u && !v
|
||||
#check_simp !(b || c) ~> !b && !c
|
||||
#check_simp ¬u ∨ ¬v !~>
|
||||
#check_simp (¬b) ∨ (¬c) ~> b = false ∨ c = false
|
||||
#check_simp ¬u || ¬v ~> (!u || !v)
|
||||
#check_simp ¬b || ¬c ~> (!b || !c)
|
||||
|
||||
-- Some ternary test cases
|
||||
#check_simp (u ∨ (v ∨ w) : Prop) !~>
|
||||
#check_simp (u ∨ (v ∨ w) : Bool) ~> (u || (v || w))
|
||||
#check_simp ((u ∨ v) ∨ w : Prop) !~>
|
||||
#check_simp ((u ∨ v) ∨ w : Bool) ~> ((u || v) || w)
|
||||
#check_simp (b || (c || d) : Prop) ~> (b ∨ c ∨ d)
|
||||
#check_simp (b || (c || d) : Bool) !~>
|
||||
#check_simp ((b || c) || d : Prop) ~> ((b ∨ c) ∨ d)
|
||||
#check_simp ((b || c) || d : Bool) !~>
|
||||
|
||||
/- # and/or -/
|
||||
|
||||
-- We don't currently do automatic simplification across and/or/not
|
||||
-- This tests for non-unexpected reductions.
|
||||
|
||||
#check_simp p ∧ (p ∨ q) !~>
|
||||
#check_simp (p ∨ q) ∧ p !~>
|
||||
|
||||
#check_simp u ∧ (v ∨ w) !~>
|
||||
#check_simp u ∨ (v ∧ w) !~>
|
||||
#check_simp (v ∨ w) ∧ u !~>
|
||||
#check_simp (v ∧ w) ∨ u !~>
|
||||
#check_simp b && (c || d) !~>
|
||||
#check_simp b || (c && d) !~>
|
||||
#check_simp (c || d) && b !~>
|
||||
#check_simp (c && d) || b !~>
|
||||
|
||||
/- # implication -/
|
||||
|
||||
#check_simp (b → c) !~>
|
||||
#check_simp (u → v) !~>
|
||||
#check_simp p → q !~>
|
||||
#check_simp decide (u → ¬v) ~> !u || !v
|
||||
|
||||
/- # iff -/
|
||||
|
||||
#check_simp (u = v : Prop) ~> u ↔ v
|
||||
#check_simp (u = v : Bool) ~> u == v
|
||||
#check_simp (u ↔ v : Prop) !~>
|
||||
#check_simp (u ↔ v : Bool) ~> u == v
|
||||
#check_simp (u == v : Prop) ~> u ↔ v
|
||||
#check_simp (u == v : Bool) !~>
|
||||
|
||||
#check_simp (b = c : Prop) !~>
|
||||
#check_simp (b = c : Bool) !~>
|
||||
#check_simp (b ↔ c : Prop) ~> b = c
|
||||
#check_simp (b ↔ c : Bool) ~> decide (b = c)
|
||||
#check_simp (b == c : Prop) ~> b = c
|
||||
#check_simp (b == c : Bool) !~>
|
||||
|
||||
-- Partial evaluation
|
||||
#check_simp (True = v : Prop) ~> v
|
||||
#check_simp (True = v : Bool) ~> (v : Bool)
|
||||
#check_simp (True ↔ v : Prop) ~> v
|
||||
#check_simp (True ↔ v : Bool) ~> (v : Bool)
|
||||
#check_simp (True == v : Prop) ~> v
|
||||
#check_simp (True == v : Bool) ~> (v : Bool)
|
||||
#check_simp (true = c : Prop) ~> c = true
|
||||
#check_simp (true = c : Bool) ~> c
|
||||
#check_simp (true ↔ c : Prop) ~> c = true
|
||||
#check_simp (true ↔ c : Bool) ~> c
|
||||
#check_simp (true == c : Prop) ~> (c : Prop)
|
||||
#check_simp (true == c : Bool) ~> c
|
||||
|
||||
#check_simp (v = True : Prop) ~> v
|
||||
#check_simp (v = True : Bool) ~> (v : Bool)
|
||||
#check_simp (v ↔ True : Prop) ~> v
|
||||
#check_simp (v ↔ True : Bool) ~> (v : Bool)
|
||||
#check_simp (v == True : Prop) ~> v
|
||||
#check_simp (v == True : Bool) ~> (v : Bool)
|
||||
#check_simp (c = true : Prop) !~>
|
||||
#check_simp (c = true : Bool) ~> c
|
||||
#check_simp (c ↔ true : Prop) ~> c = true
|
||||
#check_simp (c ↔ true : Bool) ~> c
|
||||
#check_simp (c == true : Prop) ~> c = true
|
||||
#check_simp (c == true : Bool) ~> c
|
||||
|
||||
#check_simp (True = v : Prop) ~> v
|
||||
#check_simp (True = v : Bool) ~> (v : Bool)
|
||||
#check_simp (True ↔ v : Prop) ~> v
|
||||
#check_simp (True ↔ v : Bool) ~> (v : Bool)
|
||||
#check_simp (True == v : Prop) ~> v
|
||||
#check_simp (True == v : Bool) ~> (v : Bool)
|
||||
#check_simp (true = c : Prop) ~> c = true
|
||||
#check_simp (true = c : Bool) ~> c
|
||||
#check_simp (true ↔ c : Prop) ~> c = true
|
||||
#check_simp (true ↔ c : Bool) ~> c
|
||||
#check_simp (true == c : Prop) ~> (c : Prop)
|
||||
#check_simp (true == c : Bool) ~> c
|
||||
|
||||
#check_simp (v = False : Prop) ~> ¬v
|
||||
#check_simp (v = False : Bool) ~> !v
|
||||
#check_simp (v ↔ False : Prop) ~> ¬v
|
||||
#check_simp (v ↔ False : Bool) ~> !v
|
||||
#check_simp (v == False : Prop) ~> ¬v
|
||||
#check_simp (v == False : Bool) ~> !v
|
||||
#check_simp (c = false : Prop) !~>
|
||||
#check_simp (c = false : Bool) ~> !c
|
||||
#check_simp (c ↔ false : Prop) ~> c = false
|
||||
#check_simp (c ↔ false : Bool) ~> !c
|
||||
#check_simp (c == false : Prop) ~> c = false
|
||||
#check_simp (c == false : Bool) ~> !c
|
||||
|
||||
#check_simp (False = v : Prop) ~> ¬v
|
||||
#check_simp (False = v : Bool) ~> !v
|
||||
#check_simp (False ↔ v : Prop) ~> ¬v
|
||||
#check_simp (False ↔ v : Bool) ~> !v
|
||||
#check_simp (False == v : Prop) ~> ¬v
|
||||
#check_simp (False == v : Bool) ~> !v
|
||||
#check_simp (false = c : Prop) ~> c = false
|
||||
#check_simp (false = c : Bool) ~> !c
|
||||
#check_simp (false ↔ c : Prop) ~> c = false
|
||||
#check_simp (false ↔ c : Bool) ~> !c
|
||||
#check_simp (false == c : Prop) ~> c = false
|
||||
#check_simp (false == c : Bool) ~> !c
|
||||
|
||||
-- Ternary (expand these)
|
||||
|
||||
#check_simp (u == (v = w)) ~> u == (v == w)
|
||||
#check_simp (u == (v == w)) !~>
|
||||
|
||||
/- # bne -/
|
||||
|
||||
#check_simp p ≠ q ~> ¬(p ↔ q)
|
||||
#check_simp (b != c : Bool) !~>
|
||||
#check_simp ¬(p = q) ~> ¬(p ↔ q)
|
||||
#check_simp b ≠ c ~> b ≠ c
|
||||
#check_simp ¬(b = c) !~>
|
||||
#check_simp ¬(b ↔ c) ~> ¬(b = c)
|
||||
#check_simp (b != c : Prop) ~> b ≠ c
|
||||
#check_simp u ≠ v ~> ¬(u ↔ v)
|
||||
#check_simp ¬(u = v) ~> ¬(u ↔ v)
|
||||
#check_simp ¬(u ↔ v) !~>
|
||||
#check_simp ((u:Bool) != v : Bool) !~>
|
||||
#check_simp ((u:Bool) != v : Prop) ~> ¬(u ↔ v)
|
||||
|
||||
/- # equality and and/or interactions -/
|
||||
|
||||
#check_simp (u == (v ∨ w)) ~> u == (v || w)
|
||||
#check_simp (u == (v || w)) !~>
|
||||
#check_simp ((u ∧ v) == w) ~> (u && v) == w
|
||||
|
||||
/- # ite/cond -/
|
||||
|
||||
#check_simp if b then c else d !~>
|
||||
#check_simp if b then p else q !~>
|
||||
#check_simp if u then p else q !~>
|
||||
#check_simp if u then b else c !~>
|
||||
#check_simp if u then u else q ~> ¬u → q
|
||||
#check_simp if u then q else u ~> u ∧ q
|
||||
#check_simp if u then q else q ~> q
|
||||
#check_simp cond b c d !~>
|
||||
0
tests/lean/bool_simp.lean.expected.out
Normal file
0
tests/lean/bool_simp.lean.expected.out
Normal file
1100
tests/playground/bool_exhaust_test.lean
Normal file
1100
tests/playground/bool_exhaust_test.lean
Normal file
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue