From bc6ebf34bead5d9b2ad87a3e3b65275d7a5000bb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Oct 2014 16:51:10 -0700 Subject: [PATCH] feat(library/data/bool): do not use `!` as notation for bnot, rename band/bor -> and/or --- library/data/bool.lean | 80 +++++++++---------- library/data/set.lean | 30 +++---- library/general_notation.lean | 1 - .../lean/interactive/alias.input.expected.out | 24 +++--- 4 files changed, 66 insertions(+), 69 deletions(-) diff --git a/library/data/bool.lean b/library/data/bool.lean index 266fbb753..47efaea2d 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -1,7 +1,7 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura - +import general_notation import logic.core.connectives logic.core.decidable logic.core.inhabited open eq_ops eq decidable @@ -35,104 +35,102 @@ namespace bool ... = false : cond_ff _ _) true_ne_false - definition bor (a b : bool) := + definition or (a b : bool) := rec_on a (rec_on b ff tt) tt - theorem bor_tt_left (a : bool) : bor tt a = tt := + theorem or_tt_left (a : bool) : or tt a = tt := rfl - infixl `||` := bor + infixl `||` := or - theorem bor_tt_right (a : bool) : a || tt = tt := + theorem or_tt_right (a : bool) : a || tt = tt := cases_on a rfl rfl - theorem bor_ff_left (a : bool) : ff || a = a := + theorem or_ff_left (a : bool) : ff || a = a := cases_on a rfl rfl - theorem bor_ff_right (a : bool) : a || ff = a := + theorem or_ff_right (a : bool) : a || ff = a := cases_on a rfl rfl - theorem bor_id (a : bool) : a || a = a := + theorem or_id (a : bool) : a || a = a := cases_on a rfl rfl - theorem bor_comm (a b : bool) : a || b = b || a := + theorem or_comm (a b : bool) : a || b = b || a := cases_on a (cases_on b rfl rfl) (cases_on b rfl rfl) - theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) := + theorem or_assoc (a b c : bool) : (a || b) || c = a || (b || c) := cases_on a - (calc (ff || b) || c = b || c : {bor_ff_left b} - ... = ff || (b || c) : bor_ff_left (b || c)⁻¹) - (calc (tt || b) || c = tt || c : {bor_tt_left b} - ... = tt : bor_tt_left c - ... = tt || (b || c) : bor_tt_left (b || c)⁻¹) + (calc (ff || b) || c = b || c : {or_ff_left b} + ... = ff || (b || c) : or_ff_left (b || c)⁻¹) + (calc (tt || b) || c = tt || c : {or_tt_left b} + ... = tt : or_tt_left c + ... = tt || (b || c) : or_tt_left (b || c)⁻¹) - theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt := + theorem or_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt := rec_on a (assume H : ff || b = tt, - have Hb : b = tt, from (bor_ff_left b) ▸ H, + have Hb : b = tt, from (or_ff_left b) ▸ H, or.inr Hb) (assume H, or.inl rfl) - definition band (a b : bool) := + definition and (a b : bool) := rec_on a ff (rec_on b ff tt) - infixl `&&` := band + infixl `&&` := and - theorem band_ff_left (a : bool) : ff && a = ff := + theorem and_ff_left (a : bool) : ff && a = ff := rfl - theorem band_tt_left (a : bool) : tt && a = a := + theorem and_tt_left (a : bool) : tt && a = a := cases_on a rfl rfl - theorem band_ff_right (a : bool) : a && ff = ff := + theorem and_ff_right (a : bool) : a && ff = ff := cases_on a rfl rfl - theorem band_tt_right (a : bool) : a && tt = a := + theorem and_tt_right (a : bool) : a && tt = a := cases_on a rfl rfl - theorem band_id (a : bool) : a && a = a := + theorem and_id (a : bool) : a && a = a := cases_on a rfl rfl - theorem band_comm (a b : bool) : a && b = b && a := + theorem and_comm (a b : bool) : a && b = b && a := cases_on a (cases_on b rfl rfl) (cases_on b rfl rfl) - theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) := + theorem and_assoc (a b c : bool) : (a && b) && c = a && (b && c) := cases_on a - (calc (ff && b) && c = ff && c : {band_ff_left b} - ... = ff : band_ff_left c - ... = ff && (b && c) : band_ff_left (b && c)⁻¹) - (calc (tt && b) && c = b && c : {band_tt_left b} - ... = tt && (b && c) : band_tt_left (b && c)⁻¹) + (calc (ff && b) && c = ff && c : {and_ff_left b} + ... = ff : and_ff_left c + ... = ff && (b && c) : and_ff_left (b && c)⁻¹) + (calc (tt && b) && c = b && c : {and_tt_left b} + ... = tt && (b && c) : and_tt_left (b && c)⁻¹) - theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt := + theorem and_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt := or.elim (dichotomy a) (assume H0 : a = ff, absurd - (calc ff = ff && b : (band_ff_left _)⁻¹ + (calc ff = ff && b : (and_ff_left _)⁻¹ ... = a && b : {H0⁻¹} ... = tt : H) ff_ne_tt) (assume H1 : a = tt, H1) - theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt := - band_eq_tt_elim_left (band_comm b a ⬝ H) + theorem and_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt := + and_eq_tt_elim_left (and_comm b a ⬝ H) - definition bnot (a : bool) := + definition not (a : bool) := rec_on a tt ff - notation `!` x:max := bnot x - - theorem bnot_bnot (a : bool) : !!a = a := + theorem bnot_bnot (a : bool) : not (not a) = a := cases_on a rfl rfl - theorem bnot_false : !ff = tt := + theorem bnot_false : not ff = tt := rfl - theorem bnot_true : !tt = ff := + theorem bnot_true : not tt = ff := rfl protected theorem is_inhabited [instance] : inhabited bool := diff --git a/library/data/set.lean b/library/data/set.lean index c54f68047..a88363832 100644 --- a/library/data/set.lean +++ b/library/data/set.lean @@ -45,26 +45,26 @@ infixl `∩` := inter theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) := iff.intro - (assume H, and.intro (band_eq_tt_elim_left H) (band_eq_tt_elim_right H)) + (assume H, and.intro (and_eq_tt_elim_left H) (and_eq_tt_elim_right H)) (assume H, have e1 : A x = tt, from and.elim_left H, have e2 : B x = tt, from and.elim_right H, - show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ band_tt_left tt) + show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ and_tt_left tt) theorem inter_id {T : Type} (A : set T) : A ∩ A ∼ A := -take x, band_id (A x) ▸ iff.rfl +take x, and_id (A x) ▸ iff.rfl theorem inter_empty_right {T : Type} (A : set T) : A ∩ ∅ ∼ ∅ := -take x, band_ff_right (A x) ▸ iff.rfl +take x, and_ff_right (A x) ▸ iff.rfl theorem inter_empty_left {T : Type} (A : set T) : ∅ ∩ A ∼ ∅ := -take x, band_ff_left (A x) ▸ iff.rfl +take x, and_ff_left (A x) ▸ iff.rfl theorem inter_comm {T : Type} (A B : set T) : A ∩ B ∼ B ∩ A := -take x, band_comm (A x) (B x) ▸ iff.rfl +take x, and_comm (A x) (B x) ▸ iff.rfl theorem inter_assoc {T : Type} (A B C : set T) : (A ∩ B) ∩ C ∼ A ∩ (B ∩ C) := -take x, band_assoc (A x) (B x) (C x) ▸ iff.rfl +take x, and_assoc (A x) (B x) (C x) ▸ iff.rfl definition union {T : Type} (A B : set T) : set T := λx, A x || B x @@ -72,26 +72,26 @@ infixl `∪` := union theorem mem_union {T : Type} (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) := iff.intro - (assume H, bor_to_or H) + (assume H, or_to_or H) (assume H, or.elim H (assume Ha : A x = tt, - show A x || B x = tt, from Ha⁻¹ ▸ bor_tt_left (B x)) + show A x || B x = tt, from Ha⁻¹ ▸ or_tt_left (B x)) (assume Hb : B x = tt, - show A x || B x = tt, from Hb⁻¹ ▸ bor_tt_right (A x))) + show A x || B x = tt, from Hb⁻¹ ▸ or_tt_right (A x))) theorem union_id {T : Type} (A : set T) : A ∪ A ∼ A := -take x, bor_id (A x) ▸ iff.rfl +take x, or_id (A x) ▸ iff.rfl theorem union_empty_right {T : Type} (A : set T) : A ∪ ∅ ∼ A := -take x, bor_ff_right (A x) ▸ iff.rfl +take x, or_ff_right (A x) ▸ iff.rfl theorem union_empty_left {T : Type} (A : set T) : ∅ ∪ A ∼ A := -take x, bor_ff_left (A x) ▸ iff.rfl +take x, or_ff_left (A x) ▸ iff.rfl theorem union_comm {T : Type} (A B : set T) : A ∪ B ∼ B ∪ A := -take x, bor_comm (A x) (B x) ▸ iff.rfl +take x, or_comm (A x) (B x) ▸ iff.rfl theorem union_assoc {T : Type} (A B C : set T) : (A ∪ B) ∪ C ∼ A ∪ (B ∪ C) := -take x, bor_assoc (A x) (B x) (C x) ▸ iff.rfl +take x, or_assoc (A x) (B x) (C x) ▸ iff.rfl end set diff --git a/library/general_notation.lean b/library/general_notation.lean index 6ffd9c480..79df60cb6 100644 --- a/library/general_notation.lean +++ b/library/general_notation.lean @@ -65,7 +65,6 @@ precedence `>`:50 precedence `&&`:70 -- infixl precedence `||`:65 -- infixl -precedence `!`:85 -- boolean negation, follow by rbp 100 -- ### set operations diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out index 7c6b70f4a..658e32983 100644 --- a/tests/lean/interactive/alias.input.expected.out +++ b/tests/lean/interactive/alias.input.expected.out @@ -3,26 +3,26 @@ -- BEGINWAIT -- ENDWAIT -- BEGINFINDP -bool.bor_tt_left|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt +bool.and_tt_left|∀ (a : bool), eq (bool.and bool.tt a) a +bool.and_tt_right|∀ (a : bool), eq (bool.and a bool.tt) a bool.tt|bool -bool.bor_tt_right|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt -bool.band_tt_left|∀ (a : bool), eq (bool.band bool.tt a) a -bool.band_tt_right|∀ (a : bool), eq (bool.band a bool.tt) a +bool.or_tt_left|∀ (a : bool), eq (bool.or bool.tt a) bool.tt +bool.and_eq_tt_elim_left|eq (bool.and ?a ?b) bool.tt → eq ?a bool.tt +bool.and_eq_tt_elim_right|eq (bool.and ?a ?b) bool.tt → eq ?b bool.tt bool.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t +bool.or_tt_right|∀ (a : bool), eq (bool.or a bool.tt) bool.tt bool.ff_ne_tt|not (eq bool.ff bool.tt) -bool.band_eq_tt_elim_left|eq (bool.band ?a ?b) bool.tt → eq ?a bool.tt -bool.band_eq_tt_elim_right|eq (bool.band ?a ?b) bool.tt → eq ?b bool.tt -- ENDFINDP -- BEGINWAIT -- ENDWAIT -- BEGINFINDP tt|bool -bor_tt_left|∀ (a : bool), eq (bor tt a) tt -bor_tt_right|∀ (a : bool), eq (bor a tt) tt -band_tt_left|∀ (a : bool), eq (band tt a) a -band_tt_right|∀ (a : bool), eq (band a tt) a +and_tt_left|∀ (a : bool), eq (and tt a) a +and_tt_right|∀ (a : bool), eq (and a tt) a +or_tt_left|∀ (a : bool), eq (or tt a) tt +and_eq_tt_elim_left|eq (and ?a ?b) tt → eq ?a tt +and_eq_tt_elim_right|eq (and ?a ?b) tt → eq ?b tt cond_tt|∀ (t e : ?A), eq (cond tt t e) t +or_tt_right|∀ (a : bool), eq (or a tt) tt ff_ne_tt|not (eq ff tt) -band_eq_tt_elim_left|eq (band ?a ?b) tt → eq ?a tt -band_eq_tt_elim_right|eq (band ?a ?b) tt → eq ?b tt -- ENDFINDP