Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: more lemmas and perf update #329

Merged
merged 9 commits into from
Nov 1, 2023
Merged

feat: more lemmas and perf update #329

Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
85ba850
feat: more lemmas and perf update
fgdorais Oct 27, 2023
a3484a1
chore: add doc explanations
fgdorais Oct 27, 2023
660104b
fix: match mathlib lemmas
fgdorais Oct 29, 2023
096c077
fix: enforce naming convention
fgdorais Oct 30, 2023
8c4014c
fix: missing simps
fgdorais Oct 31, 2023
4049ef2
style
digama0 Nov 1, 2023
47140c7
use implication for bool LE
digama0 Nov 1, 2023
4378329
chore: remove deprecated section
digama0 Nov 1, 2023
d75c82f
chore: remove simp from not_xor
digama0 Nov 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
51 changes: 34 additions & 17 deletions Std/Data/Bool.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,17 +29,21 @@ 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

instance : LE Bool := leOfOrd
instance : LT Bool := ltOfOrd
instance : Max Bool := maxOfLe
instance : Min Bool := minOfLe
instance : LE Bool := ⟨(!. || .)⟩
digama0 marked this conversation as resolved.
Show resolved Hide resolved
instance : LT Bool := ⟨(!. && .)⟩

instance (x y : Bool) : Decidable (x ≤ y) := inferInstanceAs (Decidable (!x || y))
instance (x y : Bool) : Decidable (x < y) := inferInstanceAs (Decidable (!x && y))

instance : Max Bool := ⟨(. || .)⟩
instance : Min Bool := ⟨(. && .)⟩

/-! ### and -/

@[simp] theorem and_not_self_left : ∀ (x : Bool), (!x && x) = false := by
@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by
decide

@[simp] theorem and_not_self_right : ∀ (x : Bool), (x && !x) = false := by
@[simp] theorem and_not_self : ∀ (x : Bool), (x && !x) = false := by
decide

theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by
Expand Down Expand Up @@ -72,6 +76,9 @@ theorem and_eq_true_iff : ∀ (x y : Bool), (x && y) = true ↔ x = true ∧ y =
theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by
decide

/-! non infix aliases -/
alias and_not_self_left := Bool.not_and_self
alias and_not_self_right := Bool.and_not_self
alias and_false_left := Bool.false_and
alias and_false_right := Bool.and_false
alias and_true_left := Bool.true_and
Expand All @@ -80,10 +87,10 @@ alias not_and := Bool.and_deMorgan

/-! ### or -/

@[simp] theorem or_not_self_left : ∀ (x : Bool), (!x || x) = true := by
@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by
decide

@[simp] theorem or_not_self_right : ∀ (x : Bool), (x || !x) = true := by
@[simp] theorem or_not_self : ∀ (x : Bool), (x || !x) = true := by
decide

theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by
Expand All @@ -110,6 +117,9 @@ theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y =
theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by
decide

/-! non infix aliases -/
digama0 marked this conversation as resolved.
Show resolved Hide resolved
alias or_not_self_left := Bool.not_or_self
alias or_not_self_right := Bool.or_not_self
alias or_false_left := Bool.false_or
alias or_false_right := Bool.or_false
alias or_true_left := Bool.true_or
Expand All @@ -118,31 +128,31 @@ alias not_or := Bool.or_deMorgan

/-! ### xor -/

@[simp] theorem xor_false_left : ∀ (x : Bool), xor false x = x := by
@[simp] theorem false_xor : ∀ (x : Bool), xor false x = x := by
decide

@[simp] theorem xor_false_right : ∀ (x : Bool), xor x false = x := by
@[simp] theorem xor_false : ∀ (x : Bool), xor x false = x := by
decide

@[simp] theorem xor_true_left : ∀ (x : Bool), xor true x = !x := by
@[simp] theorem true_xor : ∀ (x : Bool), xor true x = !x := by
decide

@[simp] theorem xor_true_right : ∀ (x : Bool), xor x true = !x := by
@[simp] theorem xor_true : ∀ (x : Bool), xor x true = !x := by
decide

@[simp] theorem xor_not_self_left : ∀ (x : Bool), xor (!x) x = true := by
@[simp] theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := by
decide

@[simp] theorem xor_not_self_right : ∀ (x : Bool), xor x (!x) = true := by
@[simp] theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := by
decide

@[simp] theorem xor_not_left : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by
theorem not_xor : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by
decide

@[simp] theorem xor_not_right : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by
theorem xor_not : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by
decide

theorem xor_not_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := by
theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := by
decide
digama0 marked this conversation as resolved.
Show resolved Hide resolved

theorem xor_self : ∀ (x : Bool), xor x x = false := by
Expand All @@ -160,6 +170,13 @@ theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y :
theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := by
decide

/-! non infix aliases -/
alias xor_not_self_left := Bool.not_xor_self
alias xor_not_self_right := Bool.xor_not_self
alias xor_not_left := Bool.not_xor
alias xor_not_right := Bool.xor_not
alias xor_not_not := Bool.not_xor_not

/-! ### le/lt -/

@[simp] protected theorem le_true : ∀ (x : Bool), x ≤ true := by
Expand Down