From 47a1c00a6d1657d649b9cb66420ec5b72e84c532 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 22 Aug 2014 16:36:47 -0700 Subject: [PATCH] refactor(library/standard): collect notation in general_notation --- library/standard/data/bool.lean | 6 +- library/standard/data/int/basic.lean | 52 ++++++------- library/standard/data/list/basic.lean | 8 +- library/standard/data/nat/basic.lean | 29 ++++--- library/standard/data/nat/default.lean | 4 +- library/standard/data/nat/div.lean | 29 +++---- library/standard/data/nat/order.lean | 36 +++------ library/standard/data/nat/sub.lean | 14 ++-- library/standard/data/prod.lean | 8 +- library/standard/data/set.lean | 9 ++- library/standard/data/subtype.lean | 14 ++-- library/standard/data/sum.lean | 21 +++-- library/standard/general_notation.lean | 76 ++++++++++++++++++- library/standard/hott/fibrant.lean | 4 +- library/standard/logic/axioms/classical.lean | 4 +- library/standard/logic/axioms/hilbert.lean | 26 ++++--- library/standard/logic/connectives/basic.lean | 18 ++--- library/standard/logic/connectives/eq.lean | 41 +++++----- .../logic/connectives/identities.lean | 43 +++++++++++ library/standard/tools/tools.md | 3 +- tests/lean/run/class4.lean | 14 ++-- tests/lean/slow/nat_wo_hints.lean | 4 +- 22 files changed, 285 insertions(+), 178 deletions(-) create mode 100644 library/standard/logic/connectives/identities.lean diff --git a/library/standard/data/bool.lean b/library/standard/data/bool.lean index 6a969a770..a811f5562 100644 --- a/library/standard/data/bool.lean +++ b/library/standard/data/bool.lean @@ -49,7 +49,7 @@ bool_rec (bool_rec ff tt b) tt a theorem bor_tt_left (a : bool) : bor tt a = tt := refl (bor tt a) -infixl `||`:65 := bor +infixl `||` := bor theorem bor_tt_right (a : bool) : a || tt = tt := cases_on a (refl (ff || tt)) (refl (tt || tt)) @@ -87,7 +87,7 @@ bool_rec definition band (a b : bool) := bool_rec ff (bool_rec ff tt b) a -infixl `&&`:75 := band +infixl `&&` := band theorem band_ff_left (a : bool) : ff && a = ff := refl (ff && a) @@ -132,7 +132,7 @@ band_eq_tt_elim_left (trans (band_comm b a) H) definition bnot (a : bool) := bool_rec tt ff a -prefix `!`:85 := bnot +notation `!` x:max := bnot x theorem bnot_bnot (a : bool) : !!a = a := cases_on a (refl (!!ff)) (refl (!!tt)) diff --git a/library/standard/data/int/basic.lean b/library/standard/data/int/basic.lean index 6e09ffd81..cbe899f4f 100644 --- a/library/standard/data/int/basic.lean +++ b/library/standard/data/int/basic.lean @@ -189,7 +189,7 @@ representative_map_idempotent_equiv proj_rel @proj_congr a -- ## Definition of ℤ and basic theorems and definitions definition int := image proj -notation `ℤ`:max := int +notation `ℤ` := int definition psub : ℕ × ℕ → ℤ := fun_image proj definition rep : ℤ → ℕ × ℕ := subtype.elt_of @@ -221,15 +221,12 @@ eq_abs quotient H definition to_nat : ℤ → ℕ := rec_constant quotient (fun v, dist (pr1 v) (pr2 v)) --- TODO: set binding strength: is this right? -notation `|`:40 x:40 `|` := to_nat x - theorem to_nat_comp (n m : ℕ) : (to_nat (psub (pair n m))) = dist n m := have H : ∀v w : ℕ × ℕ, rel v w → dist (pr1 v) (pr2 v) = dist (pr1 w) (pr2 w), from take v w H, dist_eq_intro H, have H2 : ∀v : ℕ × ℕ, (to_nat (psub v)) = dist (pr1 v) (pr2 v), from take v, (comp_constant quotient H (rel_refl v)), -(by simp) ◂ H2 (pair n m) +iff_mp (by simp) H2 (pair n m) -- add_rewrite to_nat_comp --local @@ -263,20 +260,20 @@ calc definition neg : ℤ → ℤ := quotient_map quotient flip --- TODO: is this good? -prefix `-`:80 := neg +-- TODO: is this good? Note: replacing 100 by max makes it bind stronger than application. +notation `-` x:100 := neg x -theorem neg_comp (n m : ℕ) : -psub (pair n m) = psub (pair m n) := -have H : ∀a, -psub a = psub (flip a), +theorem neg_comp (n m : ℕ) : -(psub (pair n m)) = psub (pair m n) := +have H : ∀a, -(psub a) = psub (flip a), from take a, comp_quotient_map quotient @rel_flip (rel_refl _), calc - -psub (pair n m) = psub (flip (pair n m)) : H (pair n m) + -(psub (pair n m)) = psub (flip (pair n m)) : H (pair n m) ... = psub (pair m n) : by simp -- add_rewrite neg_comp --local theorem neg_zero : -0 = 0 := -calc -psub (pair 0 0) = psub (pair 0 0) : neg_comp 0 0 +calc -(psub (pair 0 0)) = psub (pair 0 0) : neg_comp 0 0 theorem neg_neg (a : ℤ) : -(-a) = a := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, @@ -285,7 +282,7 @@ by simp -- add_rewrite neg_neg neg_zero theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b := -(by simp) ◂ congr_arg neg H +iff_mp (by simp) (congr_arg neg H) theorem neg_move {a b : ℤ} (H : -a = b) : -b = a := subst H (neg_neg a) @@ -296,7 +293,7 @@ by simp theorem pos_eq_neg {n m : ℕ} (H : n = -m) : n = 0 ∧ m = 0 := have H2 : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl (n), -have H3 : psub (pair n 0) = psub (pair 0 m), from (by simp) ◂ H, +have H3 : psub (pair n 0) = psub (pair 0 m), from iff_mp (by simp) H, have H4 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H3, have H5 : n + m = 0, from calc @@ -329,8 +326,8 @@ or_imp_or (or_swap (proj_zero_or (rep a))) a = psub (rep a) : symm (psub_rep a) ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))} ... = psub (pair 0 (pr2 (rep a))) : {H2} - ... = -psub (pair (pr2 (rep a)) 0) : by simp - ... = -of_nat (pr2 (rep a)) : refl _)) + ... = -(psub (pair (pr2 (rep a)) 0)) : by simp + ... = -(of_nat (pr2 (rep a))) : refl _)) opaque_hint (hiding int) @@ -342,35 +339,35 @@ or_elim (cases a) (assume H, obtain (n : ℕ) (H3 : a = -n), from H, subst (symm H3) (H2 n)) ---reverse equalities, rename -theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat (succ n)) := +theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - (of_nat (succ n))) := or_elim (cases a) (assume H : (∃n : ℕ, a = of_nat n), or_intro_left _ H) (assume H, - obtain (n : ℕ) (H2 : a = -of_nat n), from H, + obtain (n : ℕ) (H2 : a = -(of_nat n)), from H, discriminate (assume H3 : n = 0, have H4 : a = of_nat 0, from calc - a = - of_nat n : H2 - ... = - of_nat 0 : {H3} + a = -(of_nat n) : H2 + ... = -(of_nat 0) : {H3} ... = of_nat 0 : neg_zero, or_intro_left _ (exists_intro 0 H4)) (take k : ℕ, assume H3 : n = succ k, - have H4 : a = - of_nat (succ k), from subst H3 H2, + have H4 : a = -(of_nat (succ k)), from subst H3 H2, or_intro_right _ (exists_intro k H4))) theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ) - (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-of_nat (succ n))) : P a := + (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-(of_nat (succ n)))) : P a := or_elim (cases_succ a) (assume H, obtain (n : ℕ) (H3 : a = of_nat n), from H, subst (symm H3) (H1 n)) - (assume H, obtain (n : ℕ) (H3 : a = -of_nat (succ n)), from H, subst (symm H3) (H2 n)) + (assume H, obtain (n : ℕ) (H3 : a = -(of_nat (succ n))), from H, subst (symm H3) (H2 n)) theorem of_nat_eq_neg_of_nat {n m : ℕ} (H : n = - m) : n = 0 ∧ m = 0 := have H2 : n = psub (pair 0 m), from calc n = -m : H - ... = -psub (pair m 0) : refl (-m) + ... = -(psub (pair m 0)) : refl (-m) ... = psub (pair 0 m) : by simp, have H3 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H2, have H4 : n + m = 0, from @@ -451,9 +448,6 @@ have H : dist (xa + xb) (ya + yb) ≤ dist xa ya + dist xb yb, from dist_add_le_add_dist xa xb ya yb, by simp --- TODO: add this to eq --- notation A `=` B `:` C := @eq C A B - -- TODO: note, we have to add #nat to get the right interpretation theorem add_of_nat (n m : nat) : of_nat n + of_nat m = #nat n + m := -- this is of_nat (n + m) have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl n, @@ -466,7 +460,7 @@ by simp -- ## sub definition sub (a b : ℤ) : ℤ := a + -b -infixl `-`:65 := int.sub +infixl `-` := int.sub theorem sub_def (a b : ℤ) : a - b = a + -b := refl (a - b) @@ -938,14 +932,14 @@ iff_intro -- ---------------------------------------------- definition lt (a b : ℤ) := a + 1 ≤ b -infix `<` := int.lt +infix `<` := int.lt definition ge (a b : ℤ) := b ≤ a infix `>=` := int.ge infix `≥` := int.ge definition gt (a b : ℤ) := b < a -infix `>` := int.gt +infix `>` := int.gt theorem lt_def (a b : ℤ) : a < b ↔ a + 1 ≤ b := iff_refl (a < b) diff --git a/library/standard/data/list/basic.lean b/library/standard/data/list/basic.lean index f65d3608c..1ea3de80f 100644 --- a/library/standard/data/list/basic.lean +++ b/library/standard/data/list/basic.lean @@ -27,7 +27,7 @@ inductive list (T : Type) : Type := nil {} : list T, cons : T → list T → list T -infix `::` : 65 := cons +infix `::` := cons section @@ -189,7 +189,7 @@ list_cases_on l definition mem (x : T) : list T → Prop := list_rec false (fun y l H, x = y ∨ H) -infix `∈` : 50 := mem +infix `∈` := mem -- TODO: constructively, equality is stronger. Use that? theorem mem_nil (x : T) : x ∈ nil ↔ false := iff_refl _ @@ -202,7 +202,7 @@ list_induction_on s (or_intro_right _) assume IH : x ∈ s ++ t → x ∈ s ∨ x ∈ t, assume H1 : x ∈ (y :: s) ++ t, have H2 : x = y ∨ x ∈ s ++ t, from H1, - have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from imp_or_right H2 IH, + have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from or_imp_or_right H2 IH, iff_elim_right (or_assoc _ _ _) H3) theorem mem_or_imp_concat (x : T) (s t : list T) : x ∈ s ∨ x ∈ t → x ∈ s ++ t := @@ -286,6 +286,6 @@ theorem nth_succ (x0 : T) (l : list T) (n : ℕ) : nth x0 l (succ n) = nth x0 (t end -- declare global notation outside the section -infixl `++` : 65 := concat +infixl `++` := concat end list diff --git a/library/standard/data/nat/basic.lean b/library/standard/data/nat/basic.lean index e97057cac..421f03432 100644 --- a/library/standard/data/nat/basic.lean +++ b/library/standard/data/nat/basic.lean @@ -2,24 +2,20 @@ --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn -import logic data.num tools.tactic struc.binary -using num tactic binary eq_ops -using decidable (hiding induction_on rec_on) -using relation -- for subst_iff - --- TODO: this should go in tools, I think -namespace helper_tactics - definition apply_refl := apply @refl - tactic_hint apply_refl -end helper_tactics -using helper_tactics - - -- data.nat.basic -- ============== -- -- Basic operations on the natural numbers. +import logic data.num tools.tactic struc.binary tools.helper_tactics + +using num tactic binary eq_ops +using decidable (hiding induction_on rec_on) +using relation -- for subst_iff + +using helper_tactics + + -- Definition of the type -- ---------------------- @@ -28,7 +24,7 @@ inductive nat : Type := zero : nat, succ : nat → nat -notation `ℕ`:max := nat +notation `ℕ` := nat theorem nat_rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x @@ -160,7 +156,7 @@ general m definition add (x y : ℕ) : ℕ := plus x y -infixl `+` : 65 := add +infixl `+` := add theorem add_zero_right (n : ℕ) : n + 0 = n @@ -295,7 +291,7 @@ nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m -infixl `*`:70 := mul +infixl `*` := mul theorem mul_zero_right (n:ℕ) : n * 0 = 0 @@ -414,4 +410,5 @@ discriminate -- add_rewrite mul_succ_left mul_succ_right -- add_rewrite mul_comm mul_assoc mul_left_comm -- add_rewrite mul_distr_right mul_distr_left + end nat diff --git a/library/standard/data/nat/default.lean b/library/standard/data/nat/default.lean index 56f86e115..89b96899f 100644 --- a/library/standard/data/nat/default.lean +++ b/library/standard/data/nat/default.lean @@ -1,7 +1,5 @@ ----------------------------------------------------------------------------------------------------- -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jeremy Avigad ----------------------------------------------------------------------------------------------------- -import data.nat.sub +import .basic .order .sub .div diff --git a/library/standard/data/nat/div.lean b/library/standard/data/nat/div.lean index 1e42ab7fa..79d724866 100644 --- a/library/standard/data/nat/div.lean +++ b/library/standard/data/nat/div.lean @@ -8,15 +8,10 @@ -- This is a continuation of the development of the natural numbers, with a general way of -- defining recursive functions, and definitions of div, mod, and gcd. +-- TODO: replace the two uses of "not_or" by a constructive version + import logic .sub struc.relation data.prod - --- TODO: show decidability of le and remove these -import logic.classes.decidable -import logic.axioms.classical -import logic.axioms.prop_decidable - import logic.axioms.funext -- is this really needed? - import tools.fake_simplifier using nat relation relation.iff_ops prod @@ -25,7 +20,7 @@ using fake_simplifier decidable namespace nat -- A general recursion principle --- ============================= +-- ----------------------------- -- -- Data: -- @@ -161,7 +156,7 @@ show lhs = rhs, from lhs = 0 : if_pos H1 _ _ ... = rhs : symm (if_pos H1 _ _)) (assume H1 : ¬ (y = 0 ∨ x < y), - have H2 : y ≠ 0 ∧ ¬ x < y, from not_or _ _ ◂ H1, + have H2 : y ≠ 0 ∧ ¬ x < y, from sorry, -- subst (not_or _ _) H1, have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2), have xgey : x ≥ y, from not_lt_imp_ge (and_elim_right H2), have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, @@ -177,7 +172,7 @@ rec_measure_spec (div_aux_rec y) (div_aux_decreasing y) x definition idivide (x : ℕ) (y : ℕ) : ℕ := div_aux y x -infixl `div`:70 := idivide -- copied from Isabelle +infixl `div` := idivide -- copied from Isabelle theorem div_zero (x : ℕ) : x div 0 = 0 := trans (div_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _) @@ -237,7 +232,7 @@ show lhs = rhs, from lhs = x : if_pos H1 _ _ ... = rhs : symm (if_pos H1 _ _)) (assume H1 : ¬ (y = 0 ∨ x < y), - have H2 : y ≠ 0 ∧ ¬ x < y, from not_or _ _ ◂ H1, + have H2 : y ≠ 0 ∧ ¬ x < y, from sorry, -- subst (not_or _ _) H1, have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2), have xgey : x ≥ y, from not_lt_imp_ge (and_elim_right H2), have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, @@ -253,7 +248,7 @@ rec_measure_spec (mod_aux_rec y) (mod_aux_decreasing y) x definition modulo (x : ℕ) (y : ℕ) : ℕ := mod_aux y x -infixl `mod`:70 := modulo +infixl `mod` := modulo theorem mod_zero (x : ℕ) : x mod 0 = x := trans (mod_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _) @@ -298,7 +293,7 @@ theorem mod_mul_self_right (m n : ℕ) : (m * n) mod n = 0 := case_zero_pos n (by simp) (take n, assume npos : n > 0, - (by simp) ◂ (mod_add_mul_self_right 0 m npos)) + subst (by simp) (mod_add_mul_self_right 0 m npos)) -- add_rewrite mod_mul_self_right @@ -425,19 +420,19 @@ case n (by simp) (take n, have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1), from mod_mul_mul 1 1 (succ_pos n), - (by simp) ◂ H) + subst (by simp) H) -- add_rewrite mod_self theorem div_one (n : ℕ) : n div 1 = n := have H : n div 1 * 1 + n mod 1 = n, from symm (div_mod_eq n 1), -(by simp) ◂ H +subst (by simp) H -- add_rewrite div_one theorem pos_div_self {n : ℕ} (H : n > 0) : n div n = 1 := have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul 1 1 H, -(by simp) ◂ H1 +subst (by simp) H1 -- add_rewrite pos_div_self @@ -446,7 +441,7 @@ have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul 1 1 H, definition dvd (x y : ℕ) : Prop := y mod x = 0 -infix `|`:50 := dvd +infix `|` := dvd theorem dvd_iff_mod_eq_zero (x y : ℕ) : x | y ↔ y mod x = 0 := refl _ diff --git a/library/standard/data/nat/order.lean b/library/standard/data/nat/order.lean index 51e1fce20..87f122705 100644 --- a/library/standard/data/nat/order.lean +++ b/library/standard/data/nat/order.lean @@ -2,6 +2,11 @@ --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +-- data.nat.order +-- ============== +-- +-- The ordering on the natural numbers + import .basic logic.classes.decidable import tools.fake_simplifier @@ -9,27 +14,16 @@ using nat eq_ops tactic using fake_simplifier using decidable (decidable inl inr) --- TODO: move these to logic.connectives -theorem or_imp_or_left {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) : c ∨ b := -or_imp_or H1 H2 (λx, x) - -theorem or_imp_or_right {a b c : Prop} (H1 : a ∨ b) (H2 : b → c) : a ∨ c := -or_imp_or H1 (λx, x) H2 - namespace nat --- data.nat.order --- ============== --- --- The ordering on the natural numbers -- Less than or equal -- ------------------ definition le (n m : ℕ) : Prop := exists k : nat, n + k = m -infix `<=`:50 := le -infix `≤`:50 := le +infix `<=` := le +infix `≤` := le theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m := exists_intro k H @@ -265,14 +259,14 @@ general n -- ge and gt will be transparent, so we don't need to reprove theorems for le and lt for them definition lt (n m : ℕ) := succ n ≤ m -infix `<` : 50 := lt +infix `<` := lt abbreviation ge (n m : ℕ) := m ≤ n -infix `>=` : 50 := ge -infix `≥` : 50 := ge +infix `>=` := ge +infix `≥` := ge abbreviation gt (n m : ℕ) := m < n -infix `>` : 50 := gt +infix `>` := gt theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := refl (n < m) @@ -467,6 +461,7 @@ strong_induction_on a ( show P (succ n), from Hind n (take m, assume H1 : m ≤ n, H _ (le_imp_lt_succ H1)))) + -- Positivity -- --------- -- @@ -474,8 +469,6 @@ strong_induction_on a ( -- ### basic --- See also succ_pos. - theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 → P y) : P y := case y H0 (take y', H1 _ (succ_pos _)) @@ -527,8 +520,6 @@ discriminate theorem mul_pos_imp_pos_right {m n : ℕ} (H : n * m > 0) : m > 0 := mul_pos_imp_pos_left ((mul_comm n m) ▸ H) --- See also mul_eq_one below. - -- ### interaction of mul with le and lt theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m := @@ -601,7 +592,4 @@ or_elim (le_or_gt n 1) theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 := mul_eq_one_left ((mul_comm n m) ▸ H) ---- theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1 ---- := and_intro (mul_eq_one_left H) (mul_eq_one_right H) - end nat diff --git a/library/standard/data/nat/sub.lean b/library/standard/data/nat/sub.lean index ebd40a1f5..1c2da2036 100644 --- a/library/standard/data/nat/sub.lean +++ b/library/standard/data/nat/sub.lean @@ -2,26 +2,26 @@ --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +-- data.nat.sub +-- ============ +-- +-- Subtraction on the natural numbers, as well as min, max, and distance. + import data.nat.order import tools.fake_simplifier using nat eq_ops tactic using helper_tactics - using fake_simplifier namespace nat --- data.nat.basic2 --- =============== --- --- More basic operations on the natural numbers. -- subtraction -- ----------- definition sub (n m : ℕ) : nat := nat_rec n (fun m x, pred x) m -infixl `-` : 65 := sub +infixl `-` := sub theorem sub_zero_right (n : ℕ) : n - 0 = n @@ -491,7 +491,7 @@ by simp -- add_rewrite dist_mul_right dist_mul_left dist_comm ---needed to prove |a| * |b| = |a * b| in int +--needed to prove of_nat a * of_nat b = of_nat (a * b) in int theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) := have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from take k l : ℕ, diff --git a/library/standard/data/prod.lean b/library/standard/data/prod.lean index 688317da8..c6b46155f 100644 --- a/library/standard/data/prod.lean +++ b/library/standard/data/prod.lean @@ -2,6 +2,11 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura, Jeremy Avigad +-- data.prod +-- ========= + +-- The cartesian product. + import logic.classes.inhabited logic.connectives.eq logic.classes.decidable using inhabited decidable @@ -9,8 +14,7 @@ using inhabited decidable inductive prod (A B : Type) : Type := pair : A → B → prod A B -precedence `×`:30 -infixr × := prod +infixr `×` := prod -- notation for n-ary tuples notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t diff --git a/library/standard/data/set.lean b/library/standard/data/set.lean index 382abfacf..4a36d7ecc 100644 --- a/library/standard/data/set.lean +++ b/library/standard/data/set.lean @@ -10,13 +10,13 @@ using eq_ops bool namespace set definition set (T : Type) := T → bool definition mem {T : Type} (x : T) (s : set T) := (s x) = tt -infix `∈`:50 := mem +infix `∈` := mem section parameter {T : Type} definition empty : set T := λx, ff -notation `∅`:max := empty +notation `∅` := empty theorem mem_empty (x : T) : ¬ (x ∈ ∅) := assume H : x ∈ ∅, absurd H ff_ne_tt @@ -26,7 +26,7 @@ definition univ : set T := λx, tt theorem mem_univ (x : T) : x ∈ univ := refl _ definition inter (A B : set T) : set T := λx, A x && B x -infixl `∩`:70 := inter +infixl `∩` := inter theorem mem_inter (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) := iff_intro @@ -43,7 +43,7 @@ theorem inter_assoc (A B C : set T) : (A ∩ B) ∩ C = A ∩ (B ∩ C) := funext (λx, band_assoc (A x) (B x) (C x)) definition union (A B : set T) : set T := λx, A x || B x -infixl `∪`:65 := union +infixl `∪` := union theorem mem_union (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) := iff_intro @@ -61,4 +61,5 @@ theorem union_assoc (A B C : set T) : (A ∪ B) ∪ C = A ∪ (B ∪ C) := funext (λx, bor_assoc (A x) (B x) (C x)) end + end set diff --git a/library/standard/data/subtype.lean b/library/standard/data/subtype.lean index 81989f500..0a30c05b1 100644 --- a/library/standard/data/subtype.lean +++ b/library/standard/data/subtype.lean @@ -9,7 +9,7 @@ using decidable inductive subtype {A : Type} (P : A → Prop) : Type := tag : Πx : A, P x → subtype P -notation `{` binders `|` r:(scoped P, subtype P) `}` := r +notation `{` binders `,` r:(scoped P, subtype P) `}` := r namespace subtype @@ -18,12 +18,12 @@ section parameter {P : A → Prop} -- TODO: make this a coercion? - definition elt_of (a : {x | P x}) : A := subtype_rec (λ x y, x) a - theorem has_property (a : {x | P x}) : P (elt_of a) := subtype_rec (λ x y, y) a + definition elt_of (a : {x, P x}) : A := subtype_rec (λ x y, x) a + theorem has_property (a : {x, P x}) : P (elt_of a) := subtype_rec (λ x y, y) a theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := refl a - theorem subtype_destruct {Q : {x | P x} → Prop} (a : {x | P x}) + theorem subtype_destruct {Q : {x, P x} → Prop} (a : {x, P x}) (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a := subtype_rec H a @@ -35,13 +35,13 @@ section theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 := (show ∀(H2 : P a2), tag a1 H1 = tag a2 H2, from subst H3 (take H2, tag_irrelevant H1 H2)) H2 - theorem subtype_eq {a1 a2 : {x | P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 := + theorem subtype_eq {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 := subtype_destruct a1 (take x1 H1, subtype_destruct a2 (take x2 H2 H, tag_eq H)) - theorem subtype_inhabited {a : A} (H : P a) : inhabited {x | P x} := + theorem subtype_inhabited {a : A} (H : P a) : inhabited {x, P x} := inhabited_mk (tag a H) - theorem subtype_eq_decidable (a1 a2 : {x | P x}) + theorem subtype_eq_decidable (a1 a2 : {x, P x}) (H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) := have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from iff_intro (assume H, subst H rfl) (assume H, subtype_eq H), diff --git a/library/standard/data/sum.lean b/library/standard/data/sum.lean index b576c4ae1..feec304d0 100644 --- a/library/standard/data/sum.lean +++ b/library/standard/data/sum.lean @@ -2,6 +2,11 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura, Jeremy Avigad +-- data.sum +-- ======== + +-- The sum type, aka disjoint union. + import logic.connectives.prop logic.classes.inhabited logic.classes.decidable using inhabited decidable @@ -13,13 +18,17 @@ inductive sum (A B : Type) : Type := inl : A → sum A B, inr : B → sum A B -infixr `+`:25 := sum +infixr `⊎` := sum -abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B) +namespace sum_plus_notation +infixr `+`:25 := sum -- conflicts with notation for addition +end sum_plus_notation + +abbreviation rec_on {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B) (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s := sum_rec H1 H2 s -abbreviation cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B) +abbreviation cases_on {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B) (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s := sum_rec H1 H2 s @@ -47,13 +56,13 @@ have H1 : f (inr A b1), from rfl, have H2 : f (inr A b2), from subst H H1, H2 -theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) := +theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) := inhabited_mk (inl B (default A)) -theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A + B) := +theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) := inhabited_mk (inr A (default B)) -theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B) +theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A ⊎ B) (H1 : ∀a1 a2, decidable (inl B a1 = inl B a2)) (H2 : ∀b1 b2, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) := rec_on s1 diff --git a/library/standard/general_notation.lean b/library/standard/general_notation.lean index d11bc579e..f3c89026d 100644 --- a/library/standard/general_notation.lean +++ b/library/standard/general_notation.lean @@ -2,8 +2,80 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura, Jeremy Avigad --- General notation --- ---------------- +-- general_notation +-- ================ + +-- General operations +-- ------------------ notation `assume` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r + + +-- Global declarations of right binding strength +-- --------------------------------------------- + +-- If a module reassigns these, it will be incompatible with other modules that adhere to these +-- conventions. + +-- ### Logical operations and relations + +precedence `¬`:40 +precedence `/\`:35 -- infixr +precedence `∧`:35 -- infixr +precedence `\/`:30 -- infixr +precedence `∨`:30 -- infixr +precedence `<->`:25 +precedence `↔`:25 + +precedence `=`:50 +precedence `≠`:50 +precedence `rfl`:max -- shorthand for reflexivity + +precedence `⁻¹`:100 +precedence `⬝`:75 -- infixr +precedence `▸`:75 -- infixr + +-- ### types and type constructors + +precedence `ℕ`:max +precedence `ℤ`:max + +precedence `⊎`:25 -- infixr +precedence `×`:30 -- infixr + +-- ### arithmetic operations + +precedence `+`:65 -- infixl +precedence `-`:65 -- infixl; for negation, follow by rbp 100 +precedence `*`:70 -- infixl +precedence `div`:70 -- infixl +precedence `mod`:70 -- infixl + +precedence `<=`:50 +precedence `≤`:50 +precedence `<`:50 +precedence `>=`:50 +precedence `≥`:50 +precedence `>`:50 + +-- ### boolean operations + +precedence `&&`:70 -- infixl +precedence `||`:65 -- infixl +precedence `!`:85 -- boolean negation, follow by rbp 100 + +-- ### set operations + +precedence `∈`:50 +precedence `∅`:max +precedence `∩`:70 +precedence `∪`:65 + +-- ### other symbols + +-- uncomment when inductive type syntax has changed + +precedence `|`:55 -- used for absolute value, subtypes, divisibility +precedence `++`:65 -- list append +precedence `::`:65 -- list cons \ No newline at end of file diff --git a/library/standard/hott/fibrant.lean b/library/standard/hott/fibrant.lean index 8df3460d9..16a357af7 100644 --- a/library/standard/hott/fibrant.lean +++ b/library/standard/hott/fibrant.lean @@ -15,7 +15,7 @@ namespace fibrant axiom unit_fibrant : fibrant unit axiom nat_fibrant : fibrant nat axiom bool_fibrant : fibrant bool -axiom sum_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A + B) +axiom sum_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A ⊎ B) axiom prod_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A × B) axiom sigma_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) : fibrant (Σx : A, B x) @@ -30,6 +30,6 @@ instance prod_fibrant instance sigma_fibrant instance pi_fibrant -theorem test_fibrant : fibrant (nat × (nat + nat)) := _ +theorem test_fibrant : fibrant (nat × (nat ⊎ nat)) := _ end fibrant \ No newline at end of file diff --git a/library/standard/logic/axioms/classical.lean b/library/standard/logic/axioms/classical.lean index d5217a8ba..bb8ddcad0 100644 --- a/library/standard/logic/axioms/classical.lean +++ b/library/standard/logic/axioms/classical.lean @@ -50,7 +50,7 @@ case (λ x, (¬¬x) = x) a theorem not_not_elim {a : Prop} (H : ¬¬a) : a := -(not_not_eq a) ◂ H +(not_not_eq a) ▸ H theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b := or_elim (prop_complete a) @@ -125,7 +125,7 @@ propext (assume Ha : a, or_inr (H Ha)) (assume Hna : ¬a, or_inl Hna))) (assume (H : ¬a ∨ b) (Ha : a), - resolve_right H ((not_not_eq a)⁻¹ ◂ Ha)) + resolve_right H ((not_not_eq a)⁻¹ ▸ Ha)) theorem not_implies (a b : Prop) : (¬(a → b)) = (a ∧ ¬b) := calc (¬(a → b)) = (¬(¬a ∨ b)) : {imp_or a b} diff --git a/library/standard/logic/axioms/hilbert.lean b/library/standard/logic/axioms/hilbert.lean index 3d0870051..1f4c9ab90 100644 --- a/library/standard/logic/axioms/hilbert.lean +++ b/library/standard/logic/axioms/hilbert.lean @@ -2,29 +2,33 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Leonardo de Moura, Jeremy Avigad -import logic.connectives.eq logic.connectives.quantifiers -import logic.classes.inhabited logic.classes.nonempty -import data.subtype data.sum - -using subtype inhabited nonempty - -- logic.axioms.hilbert -- ==================== -- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the -- constructive one). +import logic.connectives.eq logic.connectives.quantifiers +import logic.classes.inhabited logic.classes.nonempty +import data.subtype data.sum + +using subtype inhabited nonempty + + +-- the axiom +-- --------- + axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) : - {x : A | (∃x : A, P x) → P x} + {x : A, (∃x : A, P x) → P x} -- In the presence of classical logic, we could prove this from the weaker --- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : { x : A | P x } +-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x} theorem nonempty_imp_exists_true {A : Type} (H : nonempty A) : ∃x : A, true := nonempty_elim H (take x, exists_intro x trivial) theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A := -let u : {x : A | (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in +let u : {x : A, (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in inhabited_mk (elt_of u) theorem exists_imp_inhabited {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A := @@ -35,13 +39,13 @@ nonempty_imp_inhabited (obtain w Hw, from H, nonempty_intro w) -- ---------------------------- definition epsilon {A : Type} {H : nonempty A} (P : A → Prop) : A := -let u : {x : A | (∃y, P y) → P x} := +let u : {x : A, (∃y, P y) → P x} := strong_indefinite_description P H in elt_of u theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) : P (@epsilon A H P) := -let u : {x : A | (∃y, P y) → P x} := +let u : {x : A, (∃y, P y) → P x} := strong_indefinite_description P H in has_property u Hex diff --git a/library/standard/logic/connectives/basic.lean b/library/standard/logic/connectives/basic.lean index 7caec4ea0..9f3f0eb46 100644 --- a/library/standard/logic/connectives/basic.lean +++ b/library/standard/logic/connectives/basic.lean @@ -22,7 +22,7 @@ inductive true : Prop := trivial : true abbreviation not (a : Prop) := a → false -prefix `¬`:40 := not +prefix `¬` := not -- not @@ -65,8 +65,8 @@ assume Hnb Ha, Hnb (Hab Ha) inductive and (a b : Prop) : Prop := and_intro : a → b → and a b -infixr `/\`:35 := and -infixr `∧`:35 := and +infixr `/\` := and +infixr `∧` := and theorem and_elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c := and_rec H2 H1 @@ -103,8 +103,8 @@ inductive or (a b : Prop) : Prop := or_intro_left : a → or a b, or_intro_right : b → or a b -infixr `\/`:30 := or -infixr `∨`:30 := or +infixr `\/` := or +infixr `∨` := or theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb @@ -131,12 +131,12 @@ or_elim H1 (assume Ha : a, or_inl (H2 Ha)) (assume Hb : b, or_inr (H3 Hb)) -theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c := +theorem or_imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c := or_elim H1 (assume H2 : a, or_inl (H H2)) (assume H2 : c, or_inr H2) -theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b := +theorem or_imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b := or_elim H1 (assume H2 : c, or_inl H2) (assume H2 : a, or_inr (H H2)) @@ -146,8 +146,8 @@ or_elim H1 -- --- definition iff (a b : Prop) := (a → b) ∧ (b → a) -infix `<->`:25 := iff -infix `↔`:25 := iff +infix `<->` := iff +infix `↔` := iff theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2 diff --git a/library/standard/logic/connectives/eq.lean b/library/standard/logic/connectives/eq.lean index 23d593b21..32076e8f4 100644 --- a/library/standard/logic/connectives/eq.lean +++ b/library/standard/logic/connectives/eq.lean @@ -1,21 +1,23 @@ ----------------------------------------------------------------------------------------------------- -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Leonardo de Moura, Jeremy Avigad ----------------------------------------------------------------------------------------------------- + +-- logic.connectives.eq +-- ==================== + +-- Equality. import .basic + -- eq -- -- inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a -infix `=`:50 := eq - --- TODO: try this out -- shorthand for "refl _" -notation `rfl`:max := refl _ +infix `=` := eq +notation `rfl` := refl _ theorem eq_id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (refl a) := rfl @@ -48,16 +50,17 @@ theorem eq_rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : theorem eq_rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec b H = b := eq_rec_on_id H b -theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c) (u : P a) : +theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c) + (u : P a) : eq_rec_on H2 (eq_rec_on H1 u) = eq_rec_on (trans H1 H2) u := (show ∀(H2 : b = c), eq_rec_on H2 (eq_rec_on H1 u) = eq_rec_on (trans H1 H2) u, from eq_rec_on H2 (take (H2 : b = b), eq_rec_on_id H2 _)) H2 namespace eq_ops - postfix `⁻¹`:100 := symm - infixr `⬝`:75 := trans - infixr `▸`:75 := subst + postfix `⁻¹` := symm + infixr `⬝` := trans + infixr `▸` := subst end eq_ops using eq_ops @@ -67,7 +70,8 @@ H ▸ refl (f a) theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b := H ▸ refl (f a) -theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b := +theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : + f a = g b := H1 ▸ H2 ▸ refl (f a) theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x := @@ -79,26 +83,23 @@ congr_arg not H theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b := H1 ▸ H2 -infixl `<|`:100 := eqmp -infixl `◂`:100 := eqmp - theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a := -H1⁻¹ ◂ H2 +H1⁻¹ ▸ H2 theorem eqt_elim {a : Prop} (H : a = true) : a := -H⁻¹ ◂ trivial +H⁻¹ ▸ trivial theorem eqf_elim {a : Prop} (H : a = false) : ¬a := -assume Ha : a, H ◂ Ha +assume Ha : a, H ▸ Ha theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c := assume Ha, H2 (H1 Ha) theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c := -assume Ha, H2 ◂ (H1 Ha) +assume Ha, H2 ▸ (H1 Ha) theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c := -assume Ha, H2 (H1 ◂ Ha) +assume Ha, H2 (H1 ▸ Ha) theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b := iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) @@ -108,7 +109,7 @@ iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) -- -- definition ne [inline] {A : Type} (a b : A) := ¬(a = b) -infix `≠`:50 := ne +infix `≠` := ne theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := H diff --git a/library/standard/logic/connectives/identities.lean b/library/standard/logic/connectives/identities.lean new file mode 100644 index 000000000..330d9e23d --- /dev/null +++ b/library/standard/logic/connectives/identities.lean @@ -0,0 +1,43 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Authors: Jeremy Avigad + +-- logic.connectives.identities +-- ============================ + +-- Useful logical identities. In the absence of propositional extensionality, some of the +-- calculations use the type class support provided by logic.connectives.instances + +import logic.connectives.instances + +using relation + +-- TODO: delete when calc bug is fixed +calc_subst subst_iff + +theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := +calc + (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _ + ... ↔ a ∨ (c ∨ b) : {or_comm b c} + ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _) + +theorem or_left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) := +calc + a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff_symm (or_assoc _ _ _) + ... ↔ (b ∨ a) ∨ c : {or_comm a b} + ... ↔ b ∨ (a ∨ c) : or_assoc _ _ _ + +theorem and_right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b := +calc + (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and_assoc _ _ _ + ... ↔ a ∧ (c ∧ b) : {and_comm b c} + ... ↔ (a ∧ c) ∧ b : iff_symm (and_assoc _ _ _) + +theorem and_left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) := +calc + a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff_symm (and_assoc _ _ _) + ... ↔ (b ∧ a) ∧ c : {and_comm a b} + ... ↔ b ∧ (a ∧ c) : and_assoc _ _ _ + +-- TODO: delete when calc bug is fixed +calc_subst subst diff --git a/library/standard/tools/tools.md b/library/standard/tools/tools.md index 488a085dc..ea78c23f0 100644 --- a/library/standard/tools/tools.md +++ b/library/standard/tools/tools.md @@ -3,4 +3,5 @@ tools Various additional tools. -* [tactic](tactic.lean) : reflected syntax for tactics \ No newline at end of file +* [tactic](tactic.lean) : reflected syntax for tactics +* [helper_tactics](helper_tactics.lean) : useful tactics \ No newline at end of file diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index 51fc12148..3bd556d79 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -65,23 +65,23 @@ theorem not_zero_add_right [instance] (x y : nat) (H : not_zero y) : not_zero (x theorem not_zero_succ [instance] (x : nat) : not_zero (succ x) := not_zero_intro (not_is_zero_succ x) -variable div : Π (x y : nat) {H : not_zero y}, nat +variable dvd : Π (x y : nat) {H : not_zero y}, nat variables a b : nat set_option pp.implicit true opaque_hint (hiding [module]) -check div a (succ b) -check (λ H : not_zero b, div a b) +check dvd a (succ b) +check (λ H : not_zero b, dvd a b) check (succ zero) check a + (succ zero) -check div a (a + (succ b)) +check dvd a (a + (succ b)) opaque_hint (exposing [module]) -check div a (a + (succ b)) +check dvd a (a + (succ b)) opaque_hint (hiding add) -check div a (a + (succ b)) +check dvd a (a + (succ b)) opaque_hint (exposing add) -check div a (a + (succ b)) +check dvd a (a + (succ b)) diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 523f18dac..9c17b227d 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -592,7 +592,7 @@ theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ := resolve_left (le_imp_succ_le_or_eq H1) H2 theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m -:= imp_or_left (le_imp_succ_le_or_eq H) +:= or_imp_or_left (le_imp_succ_le_or_eq H) (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m @@ -912,7 +912,7 @@ theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 := case y H0 (take y', H1 _ (succ_pos _)) theorem zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 -:= imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) +:= or_imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 := subst (symm H) (succ_pos m)