diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean index a1b4d39562..038d736998 100644 --- a/library/algebra/binary.lean +++ b/library/algebra/binary.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad General properties of binary operations. -/ -open eq.ops function +open function namespace binary section diff --git a/library/algebra/field.lean b/library/algebra/field.lean index cd2bdec726..481ea64afb 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -7,7 +7,7 @@ Structures with multiplicative and additive components, including division rings The development is modeled after Isabelle's library. -/ import algebra.ring -open eq eq.ops +open eq variable {A : Type} @@ -386,7 +386,7 @@ section discrete_field sorry -- by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero] theorem ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 := - assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H + assume Ha : a = 0, absurd (symm Ha ▸ one_div_zero) H theorem eq_zero_of_one_div_eq_zero (H : 1 / a = 0) : a = 0 := decidable.by_cases diff --git a/library/algebra/monotone.lean b/library/algebra/monotone.lean index 3c31127861..7281abfb8c 100644 --- a/library/algebra/monotone.lean +++ b/library/algebra/monotone.lean @@ -9,7 +9,7 @@ TODO: we will probably eventually want versions restricted to smaller domains, "nondecreasing_on" etc. Maybe we can do this with subtypes. -/ import .order -open eq eq.ops function +open eq function variables {A B C : Type} @@ -82,7 +82,7 @@ section take a₁ a₂, suppose a₁ ≤ a₂, show f a₁ ≥ f a₂, from or.elim (lt_or_eq_of_le this) (suppose a₁ < a₂, le_of_lt (H this)) - (suppose a₁ = a₂, le_of_eq (congr_arg f this⁻¹)) + (suppose a₁ = a₂, le_of_eq (congr_arg f (symm this))) end section diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 804b802b80..ccfe8041e1 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -6,7 +6,7 @@ Author: Jeremy Avigad Weak orders "≤", strict orders "<", and structures that include both. -/ import logic.eq logic.connectives algebra.binary algebra.priority -open eq eq.ops function +open eq function variables {A : Type} @@ -171,7 +171,7 @@ section strong_order_pair have le_ac : a ≤ c, from le.trans (le_of_lt' _ _ lt_ab) le_bc, have ne_ac : a ≠ c, from assume eq_ac : a = c, - have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, + have le_ba : b ≤ a, from symm eq_ac ▸ le_bc, have eq_ab : a = b, from le.antisymm (le_of_lt' _ _ lt_ab) le_ba, show false, from ne_of_lt' lt_ab eq_ab, show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac) @@ -218,7 +218,7 @@ section (assume H : b ≤ a, or.elim (iff.mp le_iff_lt_or_eq H) (assume H1, or.inr (or.inr H1)) - (assume H1, or.inr (or.inl (H1⁻¹)))) + (assume H1, or.inr (or.inl (symm H1)))) theorem lt.by_cases {a b : A} {P : Prop} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := @@ -305,11 +305,11 @@ section theorem lt.cases_of_lt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a < b) : lt.cases a b t_lt t_eq t_gt = t_lt := - if_neg (ne_of_lt H) ⬝ if_pos H + trans (if_neg (ne_of_lt H)) (if_pos H) theorem lt.cases_of_gt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a > b) : lt.cases a b t_lt t_eq t_gt = t_gt := - if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H) + trans (if_neg (ne.symm (ne_of_lt H))) (if_neg (lt.asymm H)) definition min (a b : A) : A := if a ≤ b then a else b definition max (a b : A) : A := if a ≤ b then b else a diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index 575d4a8a38..cba3feea57 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Lewis -/ import algebra.ordered_ring algebra.field -open eq eq.ops +open eq structure linear_ordered_field [class] (A : Type) extends linear_ordered_ring A, field A @@ -476,14 +476,14 @@ section discrete_linear_ordered_field have H1 : 0 < 1 / (1 / a), from one_div_pos_of_pos H, have H2 : 1 / a ≠ 0, from (assume H3 : 1 / a = 0, - have H4 : 1 / (1 / a) = 0, from H3⁻¹ ▸ div_zero 1, + have H4 : 1 / (1 / a) = 0, from symm H3 ▸ div_zero 1, absurd H4 (ne.symm (ne_of_lt H1))), (division_ring.one_div_one_div (ne_zero_of_one_div_ne_zero H2)) ▸ H1 theorem neg_of_one_div_neg (H : 1 / a < 0) : a < 0 := have H1 : 0 < - (1 / a), from neg_pos_of_neg H, have Ha : a ≠ 0, from ne_zero_of_one_div_ne_zero (ne_of_lt H), - have H2 : 0 < 1 / (-a), from (division_ring.one_div_neg_eq_neg_one_div Ha)⁻¹ ▸ H1, + have H2 : 0 < 1 / (-a), from symm (division_ring.one_div_neg_eq_neg_one_div Ha) ▸ H1, have H3 : 0 < -a, from pos_of_one_div_pos H2, neg_of_neg_pos H3 diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index be073f6055..ac29e5a9bb 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -7,7 +7,7 @@ Partially ordered additive groups, modeled on Isabelle's library. These classes if necessary. -/ import algebra.group algebra.order algebra.monotone -open eq eq.ops -- note: ⁻¹ will be overloaded +open eq variables {A B : Type} @@ -297,7 +297,7 @@ section iff.intro le_of_neg_le_neg neg_le_neg theorem nonneg_of_neg_nonpos {a : A} (H : -a ≤ 0) : 0 ≤ a := - le_of_neg_le_neg (neg_zero⁻¹ ▸ H) + le_of_neg_le_neg (symm neg_zero ▸ H) theorem neg_nonpos_of_nonneg {a : A} (H : 0 ≤ a) : -a ≤ 0 := neg_zero ▸ neg_le_neg H @@ -306,7 +306,7 @@ section iff.intro nonneg_of_neg_nonpos neg_nonpos_of_nonneg theorem nonpos_of_neg_nonneg {a : A} (H : 0 ≤ -a) : a ≤ 0 := - le_of_neg_le_neg (neg_zero⁻¹ ▸ H) + le_of_neg_le_neg (symm neg_zero ▸ H) theorem neg_nonneg_of_nonpos {a : A} (H : a ≤ 0) : 0 ≤ -a := neg_zero ▸ neg_le_neg H @@ -325,7 +325,7 @@ section iff.intro lt_of_neg_lt_neg neg_lt_neg theorem pos_of_neg_neg {a : A} (H : -a < 0) : 0 < a := - lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H) + lt_of_neg_lt_neg (symm neg_zero ▸ H) theorem neg_neg_of_pos {a : A} (H : 0 < a) : -a < 0 := neg_zero ▸ neg_lt_neg H @@ -334,7 +334,7 @@ section iff.intro pos_of_neg_neg neg_neg_of_pos theorem neg_of_neg_pos {a : A} (H : 0 < -a) : a < 0 := - lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H) + lt_of_neg_lt_neg (symm neg_zero ▸ H) theorem neg_pos_of_neg {a : A} (H : a < 0) : 0 < -a := neg_zero ▸ neg_lt_neg H @@ -852,7 +852,7 @@ section sorry -- by rewrite [-neg_sub, abs_neg] theorem ne_zero_of_abs_ne_zero {a : A} (H : abs a ≠ 0) : a ≠ 0 := - assume Ha, H (Ha⁻¹ ▸ abs_zero) + assume Ha, H (symm Ha ▸ abs_zero) /- these assume a linear order -/ @@ -893,7 +893,7 @@ section le.antisymm H1 (nonneg_of_neg_nonpos H2) theorem abs_eq_zero_iff_eq_zero (a : A) : abs a = 0 ↔ a = 0 := - iff.intro eq_zero_of_abs_eq_zero (assume H, congr_arg abs H ⬝ abs_zero) + iff.intro eq_zero_of_abs_eq_zero (assume H, trans (congr_arg abs H) abs_zero) theorem eq_of_abs_sub_eq_zero {a b : A} (H : abs (a - b) = 0) : a = b := have a - b = 0, from eq_zero_of_abs_eq_zero H, @@ -904,8 +904,8 @@ section theorem abs.by_cases {P : A → Prop} {a : A} (H1 : P a) (H2 : P (-a)) : P (abs a) := or.elim (le.total 0 a) - (assume H : 0 ≤ a, (abs_of_nonneg H)⁻¹ ▸ H1) - (assume H : a ≤ 0, (abs_of_nonpos H)⁻¹ ▸ H2) + (assume H : 0 ≤ a, symm (abs_of_nonneg H) ▸ H1) + (assume H : a ≤ 0, symm (abs_of_nonpos H) ▸ H2) theorem abs_le_of_le_of_neg_le (H1 : a ≤ b) (H2 : -a ≤ b) : abs a ≤ b := abs.by_cases H1 H2 diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 186183e9e2..d1334254ad 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -8,7 +8,7 @@ order and an associated strict order. Our numeric structures (int, rat, and real of "linear_ordered_comm_ring". This development is modeled after Isabelle's library. -/ import algebra.ordered_group algebra.ring -open eq eq.ops +open eq variable {A : Type} diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index c9845fc005..31f9f51112 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -7,7 +7,7 @@ Structures with multiplicative and additive components, including semirings, rin The development is modeled after Isabelle's library. -/ import algebra.group -open eq eq.ops +open eq variable {A : Type} @@ -85,7 +85,7 @@ section comm_semiring has_dvd.mk algebra.dvd theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b := - exists.intro _ H⁻¹ + exists.intro _ (eq.symm H) theorem dvd_of_mul_right_eq {a b c : A} (H : a * c = b) : a ∣ b := dvd.intro H @@ -100,7 +100,7 @@ section comm_semiring exists.elim H₁ H₂ theorem exists_eq_mul_left_of_dvd {a b : A} (H : a ∣ b) : ∃c, b = c * a := - dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (H1 ⬝ mul.comm a c)) + dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul.comm a c))) theorem dvd.elim_left {P : Prop} {a b : A} (H₁ : a ∣ b) (H₂ : ∀c, b = c * a → P) : P := exists.elim (exists_eq_mul_left_of_dvd H₁) (take c, assume H₃ : b = c * a, H₂ c H₃) @@ -120,7 +120,7 @@ section comm_semiring -/ theorem eq_zero_of_zero_dvd {a : A} (H : 0 ∣ a) : a = 0 := - dvd.elim H (take c, assume H' : a = 0 * c, H' ⬝ zero_mul c) + dvd.elim H (take c, assume H' : a = 0 * c, eq.trans H' (zero_mul c)) theorem dvd_zero [simp] : a ∣ 0 := dvd.intro (mul_zero a) @@ -157,7 +157,7 @@ section comm_semiring -/ theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b ∣ c) : a ∣ c := - dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (eq.symm (Habdc ⬝ mul.assoc a b d))) + dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (eq.symm (eq.trans Habdc (mul.assoc a b d)))) theorem dvd_of_mul_left_dvd {a b c : A} (H : a * b ∣ c) : b ∣ c := sorry -- dvd_of_mul_right_dvd begin rewrite mul.comm at H, apply H end diff --git a/library/data/hlist.lean b/library/data/hlist.lean index 3a98df3b0f..c610c306e1 100644 --- a/library/data/hlist.lean +++ b/library/data/hlist.lean @@ -40,9 +40,8 @@ definition append : Π {l₁ l₂}, hlist B l₁ → hlist B l₂ → hlist B (l lemma append_nil_left : ∀ {l} (h : hlist B l), append nil h = h := sorry -- by intros; reflexivity -open eq.ops lemma eq_rec_on_cons : ∀ {a₁ a₂ l₁ l₂} (b : B a₁) (h : hlist B l₁) (e : a₁::l₁ = a₂::l₂), - e ▹ cons b h = cons (head_eq_of_cons_eq e ▹ b) (tail_eq_of_cons_eq e ▹ h) := + eq.rec_on e (cons b h) = cons (eq.rec_on (head_eq_of_cons_eq e) b) (eq.rec_on (tail_eq_of_cons_eq e) h) := sorry /- begin @@ -51,7 +50,7 @@ end -/ local attribute list.append [reducible] -lemma append_nil_right : ∀ {l} (h : hlist B l), append h nil = (list.append_nil_right l)⁻¹ ▹ h +lemma append_nil_right : ∀ {l} (h : hlist B l), append h nil = eq.rec_on (eq.symm (list.append_nil_right l)) h := sorry /- | [] nil := by esimp diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index b773535630..b84b21e511 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -6,7 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn Basic properties of lists. -/ import logic data.nat.order data.nat.sub -open eq.ops nat function tactic +open nat function tactic namespace list variable {T : Type} diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 408cb9bc40..c73a80b50b 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -754,7 +754,6 @@ end perm_inter /- extensionality -/ section ext -open eq.ops theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a, a ∈ l₁ ↔ a ∈ l₂) → l₁ ~ l₂ := sorry diff --git a/library/data/list/set.lean b/library/data/list/set.lean index 674d09da23..38451c80fb 100644 --- a/library/data/list/set.lean +++ b/library/data/list/set.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura Set-like operations on lists -/ import data.list.basic data.list.comb -open nat function decidable eq.ops +open nat function decidable namespace list section erase @@ -186,7 +186,7 @@ disjoint.comm (disjoint_nil_left l) lemma disjoint_cons_of_not_mem_of_disjoint {a : A} {l₁ l₂} : a ∉ l₂ → disjoint l₁ l₂ → disjoint (a::l₁) l₂ := λ nainl₂ d x (xinal₁ : x ∈ a::l₁), or.elim (eq_or_mem_of_mem_cons xinal₁) - (λ xeqa : x = a, xeqa⁻¹ ▸ nainl₂) + (λ xeqa : x = a, eq.symm xeqa ▸ nainl₂) (λ xinl₁ : x ∈ l₁, disjoint_left d xinl₁) lemma disjoint_of_disjoint_append_left_left : ∀ {l₁ l₂ l : list A}, disjoint (l₁++l₂) l → disjoint l₁ l @@ -262,7 +262,7 @@ theorem disjoint_of_nodup_append : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) have nxinl₂ : x ∉ l₂, from not_mem_of_not_mem_append_right this, take a, suppose a ∈ x::xs, or.elim (eq_or_mem_of_mem_cons this) - (suppose a = x, this⁻¹ ▸ nxinl₂) + (suppose a = x, eq.symm this ▸ nxinl₂) (suppose ainxs : a ∈ xs, have nodup (x::(xs++l₂)), from d, have nodup (xs++l₂), from nodup_of_nodup_cons this, @@ -770,7 +770,7 @@ theorem mem_insert_iff (x a : A) (l : list A) : x ∈ insert a l ↔ x = a ∨ x iff.intro eq_or_mem_of_mem_insert (assume H, or.elim H - (assume H' : x = a, H'⁻¹ ▸ mem_insert a l) + (assume H' : x = a, eq.symm H' ▸ mem_insert a l) (assume H' : x ∈ l, mem_insert_of_mem a H')) theorem nodup_insert (a : A) {l : list A} : nodup l → nodup (insert a l) := diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index fe878b9bee..e5a3829beb 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -6,7 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad Basic operations on the natural numbers. -/ import ..num algebra.ring -open binary eq.ops +open binary namespace nat @@ -173,7 +173,7 @@ nat.induction_on n -/ theorem eq_zero_of_add_eq_zero_left {n m : ℕ} (H : n + m = 0) : m = 0 := -eq_zero_of_add_eq_zero_right (nat.add_comm m n ⬝ H) +eq_zero_of_add_eq_zero_right (eq.trans (nat.add_comm m n) H) theorem eq_zero_and_eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 := and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H) diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 49e1d6f2b0..4bb5f9e339 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura Definitions and properties of div and mod. Much of the development follows Isabelle's library. -/ import .sub -open eq.ops well_founded decidable prod +open well_founded decidable prod namespace nat @@ -30,16 +30,16 @@ theorem div_def (x y : nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y congr_fun (fix_eq div.F x) y protected theorem div_zero [simp] (a : ℕ) : a / 0 = 0 := -div_def a 0 ⬝ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0)) +eq.trans (div_def a 0) $ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0)) theorem div_eq_zero_of_lt {a b : ℕ} (h : a < b) : a / b = 0 := -div_def a b ⬝ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h)) +eq.trans (div_def a b) $ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h)) protected theorem zero_div [simp] (b : ℕ) : 0 / b = 0 := -div_def 0 b ⬝ if_neg (and.rec not_le_of_gt) +eq.trans (div_def 0 b) $ if_neg (and.rec not_le_of_gt) theorem div_eq_succ_sub_div {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a / b = succ ((a - b) / b) := -div_def a b ⬝ if_pos (and.intro h₁ h₂) +eq.trans (div_def a b) $ if_pos (and.intro h₁ h₂) theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) / z = succ (x / z) := sorry @@ -100,16 +100,16 @@ theorem mod_def (x y : nat) : mod x y = if 0 < y ∧ y ≤ x then mod (x - y) y congr_fun (fix_eq mod.F x) y theorem mod_zero [simp] (a : ℕ) : a % 0 = a := -mod_def a 0 ⬝ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0)) +eq.trans (mod_def a 0) $ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0)) theorem mod_eq_of_lt {a b : ℕ} (h : a < b) : a % b = a := -mod_def a b ⬝ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h)) +eq.trans (mod_def a b) $ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h)) theorem zero_mod [simp] (b : ℕ) : 0 % b = 0 := -mod_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0))) +eq.trans (mod_def 0 b) $ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0))) theorem mod_eq_sub_mod {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a % b = (a - b) % b := -mod_def a b ⬝ if_pos (and.intro h₁ h₂) +eq.trans (mod_def a b) $ if_pos (and.intro h₁ h₂) theorem add_mod_self [simp] (x z : ℕ) : (x + z) % z = x % z := sorry @@ -153,13 +153,13 @@ nat.case_strong_induction_on x by_cases -- (succ x < y) (assume H1 : succ x < y, have succ x % y = succ x, from mod_eq_of_lt H1, - show succ x % y < y, from this⁻¹ ▸ H1) + show succ x % y < y, from eq.symm this ▸ H1) (assume H1 : ¬ succ x < y, have y ≤ succ x, from le_of_not_gt H1, have h : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H this, have succ x - y < succ x, from sub_lt (succ_pos x) H, have succ x - y ≤ x, from le_of_lt_succ this, - show succ x % y < y, from h⁻¹ ▸ IH _ this)) + show succ x % y < y, from eq.symm h ▸ IH _ this)) theorem mod_one (n : ℕ) : n % 1 = 0 := have H1 : n % 1 < 1, from (mod_lt n) (succ_pos 0), @@ -208,7 +208,7 @@ end -/ theorem mod_eq_sub_div_mul (x y : ℕ) : x % y = x - x / y * y := -nat.eq_sub_of_add_eq (add.comm (x / y * y) (x % y) ▸ eq_div_mul_add_mod x y)⁻¹ +nat.eq_sub_of_add_eq (eq.symm (add.comm (x / y * y) (x % y) ▸ eq_div_mul_add_mod x y)) theorem mod_add_mod (m n k : ℕ) : (m % n + k) % n = (m + k) % n := sorry -- by rewrite [eq_div_mul_add_mod m n at {2}, add.assoc, add.comm (m / n * n), add_mul_mod_self] @@ -363,7 +363,7 @@ theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n % m = 0) : m ∣ n := dvd.intro (mul.comm (n / m) m ▸ div_mul_cancel_of_mod_eq_zero H) theorem mod_eq_zero_of_dvd {m n : ℕ} (H : m ∣ n) : n % m = 0 := -dvd.elim H (take z, assume H1 : n = m * z, H1⁻¹ ▸ mul_mod_right m z) +dvd.elim H (take z, assume H1 : n = m * z, eq.symm H1 ▸ mul_mod_right m z) theorem dvd_iff_mod_eq_zero (m n : ℕ) : m ∣ n ↔ n % m = 0 := iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero @@ -396,11 +396,11 @@ nat.dvd_of_dvd_add_left (add.comm n₁ n₂ ▸ H) theorem dvd_sub {m n₁ n₂ : ℕ} (H1 : m ∣ n₁) (H2 : m ∣ n₂) : m ∣ n₁ - n₂ := by_cases (assume H3 : n₁ ≥ n₂, - have H4 : n₁ = n₁ - n₂ + n₂, from (nat.sub_add_cancel H3)⁻¹, + have H4 : n₁ = n₁ - n₂ + n₂, from eq.symm (nat.sub_add_cancel H3), show m ∣ n₁ - n₂, from nat.dvd_of_dvd_add_right (H4 ▸ H1) H2) (assume H3 : ¬ (n₁ ≥ n₂), have H4 : n₁ - n₂ = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_ge H3)), - show m ∣ n₁ - n₂, from H4⁻¹ ▸ dvd_zero _) + show m ∣ n₁ - n₂, from eq.symm H4 ▸ dvd_zero _) theorem dvd.antisymm {m n : ℕ} : m ∣ n → n ∣ m → m = n := sorry @@ -442,8 +442,8 @@ theorem dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : k * m ∣ k * dvd.elim H (take l, assume H1 : k * n = k * m * l, - have H2 : n = m * l, from eq_of_mul_eq_mul_left kpos (H1 ⬝ mul.assoc k m l), - dvd.intro H2⁻¹) + have H2 : n = m * l, from eq_of_mul_eq_mul_left kpos (eq.trans H1 $ mul.assoc k m l), + dvd.intro (eq.symm H2)) theorem dvd_of_mul_dvd_mul_right {m n k : ℕ} (kpos : k > 0) (H : m * k ∣ n * k) : m ∣ n := nat.dvd_of_mul_dvd_mul_left kpos (mul.comm n k ▸ mul.comm m k ▸ H) @@ -452,12 +452,12 @@ lemma dvd_of_eq_mul (i j n : nat) : n = j*i → j ∣ n := sorry -- begin intros, subst n, apply dvd_mul_right end theorem div_dvd_div {k m n : ℕ} (H1 : k ∣ m) (H2 : m ∣ n) : m / k ∣ n / k := -have H3 : m = m / k * k, from (nat.div_mul_cancel H1)⁻¹, -have H4 : n = n / k * k, from (nat.div_mul_cancel (dvd.trans H1 H2))⁻¹, +have H3 : m = m / k * k, from eq.symm (nat.div_mul_cancel H1), +have H4 : n = n / k * k, from eq.symm (nat.div_mul_cancel (dvd.trans H1 H2)), or.elim (eq_zero_or_pos k) (assume H5 : k = 0, - have H6: n / k = 0, from (congr_arg _ H5 ⬝ nat.div_zero n), - H6⁻¹ ▸ dvd_zero (m / k)) + have H6: n / k = 0, from (eq.trans (congr_arg _ H5) $ nat.div_zero n), + eq.symm H6 ▸ dvd_zero (m / k)) (assume H5 : k > 0, nat.dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2)) diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean index dd4fd7283f..77e60719a0 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura Definitions and properties of gcd, lcm, and coprime. -/ import .div -open eq.ops well_founded decidable prod +open well_founded decidable prod namespace nat @@ -39,7 +39,7 @@ calc gcd n 1 = gcd 1 (n % 1) : gcd_succ n 0 theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (x % y) | 0 := gcd_zero_right _ -| (succ y) := gcd_succ x y ⬝ (if_neg (succ_ne_zero y))⁻¹ +| (succ y) := eq.trans (gcd_succ x y) $ eq.symm (if_neg (succ_ne_zero y)) theorem gcd_self : Π (n : ℕ), gcd n n = n @@ -55,7 +55,7 @@ theorem gcd_zero_left : Π (n : ℕ), gcd 0 n = n ... = gcd (succ n₁) 0 : sorry -- by rewrite zero_mod theorem gcd_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m % n) := -gcd_def m n ⬝ if_neg (ne_zero_of_pos H) +eq.trans (gcd_def m n) $ if_neg (ne_zero_of_pos H) theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m % n) := sorry @@ -114,7 +114,7 @@ dvd.antisymm (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k))) theorem gcd_one_left (m : ℕ) : gcd 1 m = 1 := -gcd.comm 1 m ⬝ gcd_one_right m +eq.trans (gcd.comm 1 m) $ gcd_one_right m theorem gcd_mul_left (m n k : ℕ) : gcd (m * n) (m * k) = m * gcd n k := sorry @@ -150,7 +150,7 @@ pos_of_dvd_of_pos (gcd_dvd_right m n) npos theorem eq_zero_of_gcd_eq_zero_left {m n : ℕ} (H : gcd m n = 0) : m = 0 := or.elim (eq_zero_or_pos m) (assume H1, H1) - (assume H1 : m > 0, absurd H⁻¹ (ne_of_lt (gcd_pos_of_pos_left _ H1))) + (assume H1 : m > 0, absurd (eq.symm H) (ne_of_lt (gcd_pos_of_pos_left _ H1))) theorem eq_zero_of_gcd_eq_zero_right {m n : ℕ} (H : gcd m n = 0) : n = 0 := eq_zero_of_gcd_eq_zero_left (gcd.comm m n ▸ H) @@ -229,7 +229,7 @@ calc theorem dvd_lcm_left (m n : ℕ) : m ∣ lcm m n := have H : lcm m n = m * (n / gcd m n), from nat.mul_div_assoc _ $ gcd_dvd_right m n, -dvd.intro H⁻¹ +dvd.intro (eq.symm H) theorem dvd_lcm_right (m n : ℕ) : n ∣ lcm m n := lcm.comm n m ▸ dvd_lcm_left n m @@ -349,8 +349,8 @@ show false, from not_lt_of_ge `d ≤ 1` `d > 1` theorem exists_coprime {m n : ℕ} (H : gcd m n > 0) : exists m' n', coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n := -have H1 : m = (m / gcd m n) * gcd m n, from (nat.div_mul_cancel (gcd_dvd_left m n))⁻¹, -have H2 : n = (n / gcd m n) * gcd m n, from (nat.div_mul_cancel (gcd_dvd_right m n))⁻¹, +have H1 : m = (m / gcd m n) * gcd m n, from eq.symm (nat.div_mul_cancel (gcd_dvd_left m n)), +have H2 : n = (n / gcd m n) * gcd m n, from eq.symm (nat.div_mul_cancel (gcd_dvd_right m n)), exists.intro _ (exists.intro _ (and.intro (coprime_div_gcd_div_gcd H) (and.intro H1 H2))) theorem coprime_mul {m n k : ℕ} (H1 : coprime m k) (H2 : coprime n k) : coprime (m * n) k := diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 8c68781d2e..a311578ddd 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -6,7 +6,6 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad The order relation on the natural numbers. -/ import .basic algebra.ordered_ring -open eq.ops namespace nat @@ -222,7 +221,7 @@ theorem succ_pos (n : ℕ) : 0 < succ n := zero_lt_succ n theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n := -(or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H)))⁻¹ +eq.symm (or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H))) theorem exists_eq_succ_of_lt {n : ℕ} : Π {m : ℕ}, n < m → ∃k, m = succ k | 0 H := absurd H $ not_lt_zero n @@ -298,7 +297,7 @@ protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m nat.rec (λm h, absurd h $ not_lt_zero _) (λn' (IH : ∀ {m : ℕ}, m < n' → P m) m l, or.by_cases (lt_or_eq_of_le (le_of_lt_succ l)) - IH (λ e, eq.rec (H n' @IH) e⁻¹)) (succ n) n $ lt_succ_self n + IH (λ e, eq.rec (H n' @IH) (eq.symm e))) (succ n) n $ lt_succ_self n protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n := @@ -402,7 +401,7 @@ theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 := eq_one_of_mul_eq_one_right (mul.comm n m ▸ H) theorem eq_one_of_mul_eq_self_left {n m : ℕ} (Hpos : n > 0) (H : m * n = n) : m = 1 := -eq_of_mul_eq_mul_right Hpos (H ⬝ eq.symm (one_mul n)) +eq_of_mul_eq_mul_right Hpos (eq.trans H (eq.symm (one_mul n))) theorem eq_one_of_mul_eq_self_right {n m : ℕ} (Hpos : m > 0) (H : m * n = m) : n = 1 := eq_one_of_mul_eq_self_left Hpos (mul.comm m n ▸ H) @@ -410,7 +409,7 @@ eq_one_of_mul_eq_self_left Hpos (mul.comm m n ▸ H) theorem eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 := dvd.elim H (take m, suppose 1 = n * m, - eq_one_of_mul_eq_one_right this⁻¹) + eq_one_of_mul_eq_one_right (eq.symm this)) /- min and max -/ open decidable diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 206979971f..9b7ca3b586 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -6,7 +6,6 @@ Authors: Floris van Doorn, Jeremy Avigad Subtraction on the natural numbers, as well as min, max, and distance. -/ import .order -open eq.ops namespace nat @@ -145,7 +144,7 @@ add.comm m (n - m) ▸ add_sub_of_ge theorem sub.cases {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k) : P (n - m) := or.elim (le.total n m) - (assume H3 : n ≤ m, (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 H3)) + (assume H3 : n ≤ m, eq.symm (sub_eq_zero_of_le H3) ▸ (H1 H3)) (assume H3 : m ≤ n, H2 (n - m) (add_sub_of_le H3)) theorem exists_sub_eq_of_le {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n := @@ -182,30 +181,30 @@ sub.cases (take k : ℕ, assume H1 : m + k = n, assume H2 : k = 0, - have H3 : n = m, from add_zero m ▸ H2 ▸ H1⁻¹, + have H3 : n = m, from add_zero m ▸ H2 ▸ eq.symm H1, H3 ▸ le.refl n) theorem sub_sub.cases {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) := or.elim (le.total n m) (assume H3 : n ≤ m, - (sub_eq_zero_of_le H3)⁻¹ ▸ (H2 (m - n) (add_sub_of_le H3)⁻¹)) + eq.symm (sub_eq_zero_of_le H3) ▸ H2 (m - n) (eq.symm (add_sub_of_le H3))) (assume H3 : m ≤ n, - (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 (n - m) (add_sub_of_le H3)⁻¹)) + eq.symm (sub_eq_zero_of_le H3) ▸ (H1 (n - m) (eq.symm (add_sub_of_le H3)))) protected theorem sub_eq_of_add_eq {n m k : ℕ} (H : n + m = k) : k - n = m := have H2 : k - n + n = m + n, from calc k - n + n = k : nat.sub_add_cancel (le.intro H) - ... = n + m : H⁻¹ + ... = n + m : eq.symm H ... = m + n : add.comm n m, add.right_cancel H2 protected theorem eq_sub_of_add_eq {a b c : ℕ} (H : a + c = b) : a = b - c := -(nat.sub_eq_of_add_eq (add.comm a c ▸ H))⁻¹ +eq.symm (nat.sub_eq_of_add_eq (add.comm a c ▸ H)) protected theorem sub_eq_of_eq_add {a b c : ℕ} (H : a = c + b) : a - b = c := -nat.sub_eq_of_add_eq (add.comm c b ▸ H⁻¹) +nat.sub_eq_of_add_eq (add.comm c b ▸ eq.symm H) protected theorem sub_le_sub_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n - k ≤ m - k := sorry @@ -361,10 +360,10 @@ theorem dist_eq_sub_of_gt {n m : ℕ} (H : n > m) : dist n m = n - m := dist_eq_sub_of_ge (le_of_lt H) theorem dist_zero_right (n : ℕ) : dist n 0 = n := -dist_eq_sub_of_ge (zero_le n) ⬝ nat.sub_zero n +eq.trans (dist_eq_sub_of_ge (zero_le n)) (nat.sub_zero n) theorem dist_zero_left (n : ℕ) : dist 0 n = n := -dist_eq_sub_of_le (zero_le n) ⬝ nat.sub_zero n +eq.trans (dist_eq_sub_of_le (zero_le n)) (nat.sub_zero n) theorem dist.intro {n m k : ℕ} (H : n + m = k) : dist k n = m := calc diff --git a/library/data/num.lean b/library/data/num.lean index 795e7de080..fca5569bc8 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ import data.bool -open bool eq.ops decidable +open bool decidable namespace pos_num theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff := diff --git a/library/data/prod.lean b/library/data/prod.lean index 311abb062e..f30944a812 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura, Jeremy Avigad -/ import logic.eq -open inhabited decidable eq.ops +open inhabited decidable namespace prod variables {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B} {u : A × B} diff --git a/library/data/sum.lean b/library/data/sum.lean index ed6e2d4d79..813f797ec2 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad The sum type, aka disjoint union. -/ import logic.connectives -open inhabited eq.ops +open inhabited notation A ⊎ B := sum A B diff --git a/library/init/classical.lean b/library/init/classical.lean index 2e265cdee5..c4006bc839 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -73,7 +73,6 @@ Prove excluded middle using Hilbert's choice The proof follows Diaconescu proof that shows that the axiom of choice implies the excluded middle. -/ section diaconescu -open eq.ops parameter p : Prop private definition U (x : Prop) : Prop := x = true ∨ p @@ -93,7 +92,7 @@ or.elim u_def (assume Hut : u = true, or.elim v_def (assume Hvf : v = false, - have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false, + have Hne : ¬(u = v), from eq.symm Hvf ▸ eq.symm Hut ▸ true_ne_false, or.inl Hne) (assume Hp : p, or.inr Hp)) (assume Hp : p, or.inr Hp) @@ -126,11 +125,10 @@ or.elim (em a) definition eq_true_or_eq_false := prop_complete section aux -open eq.ops theorem cases_true_false (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a := or.elim (prop_complete a) - (assume Ht : a = true, Ht⁻¹ ▸ H1) - (assume Hf : a = false, Hf⁻¹ ▸ H2) + (assume Ht : a = true, eq.symm Ht ▸ H1) + (assume Hf : a = false, eq.symm Hf ▸ H2) theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a := cases_true_false P H1 H2 a diff --git a/library/init/logic.lean b/library/init/logic.lean index e4d9ea68b0..67d4b6e776 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -87,15 +87,12 @@ namespace eq theorem mpr {a b : Type} : (a = b) → b → a := assume H₁ H₂, eq.rec_on (eq.symm H₁) H₂ - - namespace ops - notation H `⁻¹` := symm H --input with \sy or \-1 or \inv - notation H1 ⬝ H2 := trans H1 H2 - notation H1 ▸ H2 := subst H1 H2 - notation H1 ▹ H2 := eq.rec H2 H1 - end ops end eq +notation H1 ▸ H2 := eq.subst H1 H2 + +open eq + theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ := eq.subst H₁ (eq.subst H₂ rfl) @@ -107,21 +104,19 @@ congr rfl section variables {A : Type} {a b c: A} - open eq.ops theorem trans_rel_left (R : A → A → Prop) (H₁ : R a b) (H₂ : b = c) : R a c := H₂ ▸ H₁ theorem trans_rel_right (R : A → A → Prop) (H₁ : a = b) (H₂ : R b c) : R a c := - H₁⁻¹ ▸ H₂ + symm H₁ ▸ H₂ end section variable {p : Prop} - open eq.ops theorem of_eq_true (H : p = true) : p := - H⁻¹ ▸ trivial + symm H ▸ trivial theorem not_of_eq_false (H : p = false) : ¬p := assume Hp, H ▸ Hp @@ -148,7 +143,6 @@ definition ne.def [defeq] {A : Type} (a b : A) : ne a b = ¬ (a = b) := rfl notation a ≠ b := ne a b namespace ne - open eq.ops variable {A : Type} variables {a b : A} @@ -159,13 +153,12 @@ namespace ne theorem irrefl (H : a ≠ a) : false := H rfl theorem symm (H : a ≠ b) : b ≠ a := - assume (H₁ : b = a), H (H₁⁻¹) + assume (H₁ : b = a), H (symm H₁) end ne theorem false_of_ne {A : Type} {a : A} : a ≠ a → false := ne.irrefl section - open eq.ops variables {p : Prop} theorem ne_false_of_self : p → p ≠ false := @@ -216,31 +209,30 @@ definition type_eq_of_heq (H : a == b) : A = B := heq.rec_on H (eq.refl A) end -open eq.ops -theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : H ▹ p == p := +theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p := eq.drec_on H (heq.refl p) -theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : e ▹ p₁ = p₂), p₁ == p₂ +theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : eq.rec_on e p₁ = p₂), p₁ == p₂ | a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁) -theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a' = a) (h₂ : p₁ = e ▹ p₂), p₁ == p₂ +theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂ | a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁) theorem of_heq_true {a : Prop} (H : a == true) : a := of_eq_true (eq_of_heq H) -theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), p₁ ▹ (p₂ ▹ a : B) = (p₂ ⬝ p₁) ▹ a +theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), eq.rec_on p₁ (eq.rec_on p₂ a : B) = eq.rec_on (eq.trans p₂ p₁) a | A A A (eq.refl A) (eq.refl A) a := calc - eq.refl A ▹ eq.refl A ▹ a = eq.refl A ▹ a : rfl - ... = (eq.refl A ⬝ eq.refl A) ▹ a : eq.subst (proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A)) rfl + eq.rec_on (eq.refl A) (eq.rec_on (eq.refl A) a) = eq.rec_on (eq.refl A) a : rfl + ... = eq.rec_on (eq.trans (eq.refl A) (eq.refl A)) a : eq.subst (proof_irrel (eq.refl A) (eq.trans (eq.refl A) (eq.refl A))) rfl -theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, p ▹ a₁ = a₂ → a₁ = p⁻¹ ▹ a₂ := +theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, eq.rec_on p a₁ = a₂ → a₁ = eq.rec_on (eq.symm p) a₂ := eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl) -theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), type_eq_of_heq h ▹ a₁ = a₂ +theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), eq.rec_on (type_eq_of_heq h) a₁ = a₂ | A A a a (heq.refl a) := rfl -theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = (type_eq_of_heq h)⁻¹ ▹ a₂ := +theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ := eq_rec_eq_eq_rec (eq_rec_of_heq_left h) attribute heq.refl [refl] @@ -720,7 +712,6 @@ match H a a with | ff n := absurd rfl n end -open eq.ops theorem decidable_eq_inr_neg {A : Type} [H : decidable_eq A] {a b : A} : Π n : a ≠ b, H a b = ff n := assume n, match H a b with diff --git a/library/init/nat.lean b/library/init/nat.lean index 89c83afa17..c39f47e71f 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -5,7 +5,7 @@ Authors: Floris van Doorn, Leonardo de Moura -/ prelude import init.relation init.num -open eq.ops decidable or +open decidable or notation `ℕ` := nat diff --git a/library/init/simplifier.lean b/library/init/simplifier.lean index 76b7572536..a799c8b288 100644 --- a/library/init/simplifier.lean +++ b/library/init/simplifier.lean @@ -16,7 +16,6 @@ attribute eq_self_iff_true [simp] end prove namespace unit_simp -open eq.ops -- TODO(dhs): prove these lemmas elsewhere and only gather the -- [simp] attributes here diff --git a/library/logic/cast.lean b/library/logic/cast.lean index ef4775a2ba..a08fbaf862 100644 --- a/library/logic/cast.lean +++ b/library/logic/cast.lean @@ -5,9 +5,7 @@ Author: Leonardo de Moura Casts and heterogeneous equality. See also init.datatypes and init.logic. -/ - import logic.eq logic.quantifiers -open eq.ops namespace heq universe variable u @@ -75,7 +73,7 @@ section --TODO: generalize to eq.rec. This is a special case of rec_on_comp in eq.lean theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) : - cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a := + cast Hbc (cast Hab a) = cast (eq.trans Hab Hbc) a := sorry -- by subst Hab theorem pi_eq (H : P = P') : (Π x, P x) = (Π x, P' x) := diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 6eff31c662..e0e1bd101b 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -5,8 +5,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Haitao Zhang The propositional connectives. See also init.datatypes and init.logic. -/ -open eq.ops - variables {a b c d : Prop} /- implies -/ diff --git a/library/logic/eq.lean b/library/logic/eq.lean index 58558f7ec8..46e46b0ace 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -5,9 +5,6 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn Additional declarations/theorems about equality. See also init.datatypes and init.logic. -/ - -open eq.ops - namespace eq variables {A B : Type} {a a' a₁ a₂ a₃ a₄ : A} @@ -24,7 +21,7 @@ namespace eq eq.drec_on H rfl theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : eq.rec_on H₁ b = eq.rec_on H₂ b := - rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹ + trans (rec_on_constant H₁ b) (symm (rec_on_constant H₂ b)) theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) : eq.drec_on H b = eq.drec_on H' b := @@ -87,7 +84,7 @@ section H₁ ▸ H₂ theorem eqmpr (H₁ : a = b) (H₂ : b) : a := - H₁⁻¹ ▸ H₂ + symm H₁ ▸ H₂ theorem imp_trans (H₁ : a → b) (H₂ : b → c) : a → c := assume Ha, H₂ (H₁ Ha) diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index f19148701d..a58c615e4a 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -56,7 +56,7 @@ iff.intro (exists_imp_exists (λ x, or.inr))) section - open decidable eq.ops + open decidable variables {A : Type} (P : A → Prop) (a : A) [H : decidable (P a)] include H diff --git a/tests/lean/eta_bug.lean.expected.out b/tests/lean/eta_bug.lean.expected.out index 34610ad026..9f16993599 100644 --- a/tests/lean/eta_bug.lean.expected.out +++ b/tests/lean/eta_bug.lean.expected.out @@ -1 +1 @@ -λ A x y H₁ H₂, H₂ ▹ H₁ +λ A x y H₁ H₂, eq.rec H₁ H₂ diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean index f28ba98be9..341e856e0b 100644 --- a/tests/lean/have1.lean +++ b/tests/lean/have1.lean @@ -1,10 +1,10 @@ import logic -open bool eq.ops tactic eq - +open bool tactic eq +notation H `⁻¹` := symm H --input with \sy or \-1 or \inv +notation H1 ⬝ H2 := trans H1 H2 constants a b c : bool axiom H1 : a = b axiom H2 : b = c - check have e1 : a = b, from H1, have e2 : a = c, from sorry, -- by apply trans; apply e1; apply H2, have e3 : c = a, from e2⁻¹, diff --git a/tests/lean/run/541a.lean b/tests/lean/run/541a.lean index 3d2da8e534..4508fdc011 100644 --- a/tests/lean/run/541a.lean +++ b/tests/lean/run/541a.lean @@ -1,5 +1,5 @@ import data.list data.nat -open nat list eq.ops +open nat list section diff --git a/tests/lean/run/div_wf.lean b/tests/lean/run/div_wf.lean index 39ddc8414b..b443a84662 100644 --- a/tests/lean/run/div_wf.lean +++ b/tests/lean/run/div_wf.lean @@ -1,5 +1,5 @@ import data.nat data.prod -open nat well_founded decidable prod eq.ops +open nat well_founded decidable prod -- Auxiliary lemma used to justify recursive call private definition lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x := diff --git a/tests/lean/run/eq20.lean b/tests/lean/run/eq20.lean index da8f0b3db0..c035069766 100644 --- a/tests/lean/run/eq20.lean +++ b/tests/lean/run/eq20.lean @@ -17,8 +17,6 @@ section theorem filter_cons (a : A) (l : list A) : filter (a :: l) = if p a then a :: filter l else filter l := rfl - open eq.ops - theorem filter_cons_of_pos {a : A} (l : list A) (h : p a) : filter (a :: l) = a :: filter l := if_pos h ▸ filter_cons a l diff --git a/tests/lean/run/fib_wrec.lean b/tests/lean/run/fib_wrec.lean index 5045abb935..92282fbfbf 100644 --- a/tests/lean/run/fib_wrec.lean +++ b/tests/lean/run/fib_wrec.lean @@ -1,5 +1,5 @@ import data.nat -open nat eq.ops +open nat definition fib.F (n : nat) : (Π (m : nat), m < n → nat) → nat := nat.cases_on n diff --git a/tests/lean/run/gcd.lean b/tests/lean/run/gcd.lean index 9be031c208..77780ae804 100644 --- a/tests/lean/run/gcd.lean +++ b/tests/lean/run/gcd.lean @@ -1,5 +1,5 @@ import data.nat data.prod -open nat well_founded decidable prod eq.ops +open nat well_founded decidable prod namespace playground diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean index c23283ab2e..5371206775 100644 --- a/tests/lean/run/list_elab1.lean +++ b/tests/lean/run/list_elab1.lean @@ -10,7 +10,7 @@ -- Basic properties of Lists. import data.nat -open nat eq.ops +open nat inductive List (T : Type) : Type := | nil {} : List T | cons : T → List T → List T diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean index 4d0cf80d7e..6e0fa196a4 100644 --- a/tests/lean/run/nat_bug2.lean +++ b/tests/lean/run/nat_bug2.lean @@ -1,5 +1,4 @@ import logic -open eq.ops namespace experiment inductive nat : Type := | zero : nat diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean index db3c094f35..f32efce6d6 100644 --- a/tests/lean/run/nat_bug4.lean +++ b/tests/lean/run/nat_bug4.lean @@ -1,5 +1,4 @@ import logic -open eq.ops namespace experiment inductive nat : Type := | zero : nat diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean index 85d889fe9d..c19385c013 100644 --- a/tests/lean/run/nat_bug6.lean +++ b/tests/lean/run/nat_bug6.lean @@ -1,5 +1,4 @@ import logic -open eq.ops namespace experiment inductive nat : Type := | zero : nat diff --git a/tests/lean/run/nateq.lean b/tests/lean/run/nateq.lean index cd3ac3cbc4..17f8bc8461 100644 --- a/tests/lean/run/nateq.lean +++ b/tests/lean/run/nateq.lean @@ -1,5 +1,5 @@ import data.nat.basic data.bool -open bool nat eq.ops +open bool nat attribute nat.rec_on [reducible] definition is_eq (a b : nat) : bool := diff --git a/tests/lean/run/tree3.lean b/tests/lean/run/tree3.lean index 65827e2a93..7b686b9d0e 100644 --- a/tests/lean/run/tree3.lean +++ b/tests/lean/run/tree3.lean @@ -1,5 +1,5 @@ import logic data.prod -open eq.ops prod tactic +open prod tactic inductive tree (A : Type) := | leaf : A → tree A diff --git a/tests/lean/run/tree_height.lean b/tests/lean/run/tree_height.lean index e9f7ca7de4..69831c788c 100644 --- a/tests/lean/run/tree_height.lean +++ b/tests/lean/run/tree_height.lean @@ -1,5 +1,5 @@ import logic data.nat -open eq.ops nat algebra +open nat algebra inductive tree (A : Type) := | leaf : A → tree A diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean index 52a8293ca1..6ab53969ac 100644 --- a/tests/lean/show1.lean +++ b/tests/lean/show1.lean @@ -1,10 +1,10 @@ import logic -open bool eq.ops tactic - +open bool eq tactic +notation H `⁻¹` := symm H --input with \sy or \-1 or \inv +notation H1 ⬝ H2 := trans H1 H2 constants a b c : bool axiom H1 : a = b axiom H2 : b = c - check show a = c, from H1 ⬝ H2 print "------------" check have e1 : a = b, from H1,