diff --git a/doc/lean/calc.org b/doc/lean/calc.org index 782711e216..cf3da91e66 100644 --- a/doc/lean/calc.org +++ b/doc/lean/calc.org @@ -17,7 +17,7 @@ Each =_i= is a proof for =_{i-1} op_i _i=. Recall that proofs are also expressions in Lean. The =_i= may also be of the form ={ }=, where == is a proof for some equality =a = b=. The form ={ }= is just syntax sugar -for =subst (refl _{i-1})= +for =eq.subst (refl _{i-1})= That is, we are claiming we can obtain =_i= by replacing =a= with =b= in =_{i-1}=. @@ -38,7 +38,7 @@ Here is an example ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } ... = 1 + d : add_comm - ... = e : symm Ax4. + ... = e : eq.symm Ax4. #+END_SRC diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index 61eacb2f1e..629a7b8800 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -103,8 +103,8 @@ for =n = n=. In Lean, =eq.refl= is the reflexivity theorem. The command =axiom= postulates that a given proposition holds. The following commands postulate two axioms =Ax1= and =Ax2= that state that =n = m= and -=m = o=. =Ax1= and =Ax2= are not just names. For example, =trans Ax1 Ax2= is a proof that -=n = o=, where =trans= is the transitivity theorem. +=m = o=. =Ax1= and =Ax2= are not just names. For example, =eq.trans Ax1 Ax2= is a proof that +=n = o=, where =eq.trans= is the transitivity theorem. #+BEGIN_SRC lean import data.nat @@ -112,14 +112,14 @@ The following commands postulate two axioms =Ax1= and =Ax2= that state that =n = variables m n o : nat axiom Ax1 : n = m axiom Ax2 : m = o - check trans Ax1 Ax2 + check eq.trans Ax1 Ax2 #+END_SRC -The expression =trans Ax1 Ax2= is just a function application like any other. +The expression =eq.trans Ax1 Ax2= is just a function application like any other. Moreover, in Lean, _propositions are types_. Any proposition =P= can be used as a type. The elements of type =P= can be viewed as the proofs of =P=. Moreover, in Lean, _proof checking is type checking_. For example, the Lean type checker -will reject the type incorrect term =trans Ax2 Ax1=. +will reject the type incorrect term =eq.trans Ax2 Ax1=. Because we use _proposition as types_, we must support _empty types_. For example, the type =false= must be empty, since we don't have a proof for =false=. @@ -142,14 +142,14 @@ propositions, and =variable= for everything else. Similarly, a theorem is just a definition. The following command defines a new theorem called =nat_trans3=, and then use it to prove something else. In this -example, =symm= is the symmetry theorem. +example, =eq.symm= is the symmetry theorem. #+BEGIN_SRC lean import data.nat open nat theorem nat_trans3 (a b c d : nat) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d := - trans (trans H1 (symm H2)) H3 + eq.trans (eq.trans H1 (eq.symm H2)) H3 -- Example using nat_trans3 variables x y z w : nat @@ -178,7 +178,7 @@ implicit arguments. open nat theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d := - trans (trans H1 (symm H2)) H3 + eq.trans (eq.trans H1 (eq.symm H2)) H3 -- Example using nat_trans3 variables x y z w : nat @@ -196,13 +196,13 @@ is quite simple, we are just instructing Lean to automatically insert the placeh Sometimes, Lean will not be able to infer the parameters automatically. The annotation =@f= instructs Lean that we want to provide the implicit arguments for =f= explicitly. -The theorems =eq.refl=, =trans= and =symm= all have implicit arguments. +The theorems =eq.refl=, =eq.trans= and =eq.symm= all have implicit arguments. #+BEGIN_SRC lean import logic check @eq.refl - check @symm - check @trans + check @eq.symm + check @eq.trans #+END_SRC We can also instruct Lean to display all implicit arguments when it prints expressions. @@ -215,14 +215,14 @@ This is useful when debugging non-trivial problems. variables a b c : nat axiom H1 : a = b axiom H2 : b = c - check trans H1 H2 + check eq.trans H1 H2 set_option pp.implicit true -- Now, Lean will display all implicit arguments - check trans H1 H2 + check eq.trans H1 H2 #+END_SRC -In the previous example, the =check= command stated that =trans H1 H2= +In the previous example, the =check= command stated that =eq.trans H1 H2= has type =@eq ℕ a c=. The expression =a = c= is just notational convenience. We have seen many occurrences of =Type=. @@ -249,15 +249,15 @@ In the command above, Lean reports that =Type.{l_1}= that lives in universe =l_1= has type =Type.{succ l_1}=. That is, its type lives in the universe =l_1 + 1=. -Definitions such as =eq.refl=, =symm= and =trans= are all universe +Definitions such as =eq.refl=, =eq.symm= and =eq.trans= are all universe polymorphic. #+BEGIN_SRC lean import logic set_option pp.universes true check @eq.refl - check @symm - check @trans + check @eq.symm + check @eq.trans #+END_SRC Whenever we declare a new constant, Lean automatically infers the @@ -634,7 +634,7 @@ In Lean, the dependent functions is written as =forall a : A, B a=, =Pi a : A, B a=, =∀ x : A, B a=, or =Π x : A, B a=. We usually use =forall= and =∀= for propositions, and =Pi= and =Π= for everything else. In the previous examples, we have seen many examples of -dependent functions. The theorems =eq.refl=, =trans= and =symm=, and the +dependent functions. The theorems =eq.refl=, =eq.trans= and =eq.symm=, and the equality are all dependent functions. The universal quantifier is just a dependent function. @@ -672,12 +672,12 @@ abstraction. In the following example, we create a proof term showing that for a variable f : nat → nat axiom fzero : ∀ x, f x = 0 - check λ x y, trans (fzero x) (symm (fzero y)) + check λ x y, eq.trans (fzero x) (eq.symm (fzero y)) #+END_SRC We can view the proof term above as a simple function or "recipe" for showing that =f x = f y= for any =x= and =y=. The function "invokes" =fzero= for creating -proof terms for =f x = 0= and =f y = 0=. Then, it uses symmetry =symm= to create +proof terms for =f x = 0= and =f y = 0=. Then, it uses symmetry =eq.symm= to create a proof term for =0 = f y=. Finally, transitivity is used to combine the proofs for =f x = 0= and =0 = f y=. @@ -696,7 +696,7 @@ for =∃ a : nat, a = w= using open nat theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d := - trans (trans H1 (symm H2)) H3 + eq.trans (eq.trans H1 (eq.symm H2)) H3 variables x y z w : nat axiom Hxy : x = y @@ -760,7 +760,7 @@ of two even numbers is an even number. exists_intro (w1 + w2) (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} - ... = 2*(w1 + w2) : symm mul_distr_left))) + ... = 2*(w1 + w2) : eq.symm mul_distr_left))) #+END_SRC @@ -780,5 +780,5 @@ With this macro we can write the example above in a more natural way exists_intro (w1 + w2) (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} - ... = 2*(w1 + w2) : symm mul_distr_left) + ... = 2*(w1 + w2) : eq.symm mul_distr_left) #+END_SRC diff --git a/library/data/bool.lean b/library/data/bool.lean index 47fb6d15d7..26a90426af 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -40,7 +40,7 @@ assume H : ff = tt, absurd theorem decidable_eq [instance] (a b : bool) : decidable (a = b) := rec (rec (inl (eq.refl ff)) (inr ff_ne_tt) b) - (rec (inr (ne_symm ff_ne_tt)) (inl (eq.refl tt)) b) + (rec (inr (ne.symm ff_ne_tt)) (inl (eq.refl tt)) b) a definition bor (a b : bool) := @@ -128,7 +128,7 @@ or_elim (dichotomy a) (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 (trans (band_comm b a) H) +band_eq_tt_elim_left (eq.trans (band_comm b a) H) definition bnot (a : bool) := rec tt ff a diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index ac1526b199..4a95fbf531 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -109,8 +109,8 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from have H3 : pr1 (proj (flip a)) = pr1 (flip (proj a)), from calc pr1 (proj (flip a)) = 0 : proj_le_pr1 H2 - ... = pr2 (proj a) : symm (proj_ge_pr2 H) - ... = pr1 (flip (proj a)) : symm (flip_pr1 (proj a)), + ... = pr2 (proj a) : (proj_ge_pr2 H)⁻¹ + ... = pr1 (flip (proj a)) : (flip_pr1 (proj a))⁻¹, have H4 : pr2 (proj (flip a)) = pr2 (flip (proj a)), from calc pr2 (proj (flip a)) = pr2 (flip a) - pr1 (flip a) : proj_le_pr2 H2 @@ -124,8 +124,8 @@ or_elim le_total (assume H : pr1 a ≤ pr2 a, have H2 : pr2 (flip a) ≤ pr1 (flip a), from P_flip H, calc - proj (flip a) = flip (flip (proj (flip a))) : symm (flip_flip (proj (flip a))) - ... = flip (proj (flip (flip a))) : {symm (special (flip a) H2)} + proj (flip a) = flip (flip (proj (flip a))) : (flip_flip (proj (flip a)))⁻¹ + ... = flip (proj (flip (flip a))) : {(special (flip a) H2)⁻¹} ... = flip (proj a) : {flip_flip a}) theorem proj_rel (a : ℕ × ℕ) : rel a (proj a) := @@ -161,7 +161,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from have H6 : pr2 (proj a) = pr2 (proj b), from calc pr2 (proj a) = 0 : proj_ge_pr2 H2 - ... = pr2 (proj b) : {symm (proj_ge_pr2 H4)}, + ... = pr2 (proj b) : {(proj_ge_pr2 H4)⁻¹}, prod_eq H5 H6, or_elim le_total (assume H2 : pr2 a ≤ pr1 a, special a b H2 H) @@ -200,8 +200,8 @@ theorem destruct (a : ℤ) : ∃n m : ℕ, a = psub (pair n m) := exists_intro (pr1 (rep a)) (exists_intro (pr2 (rep a)) (calc - a = psub (rep a) : symm (psub_rep a) - ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))})) + a = psub (rep a) : (psub_rep a)⁻¹ + ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹})) definition of_nat (n : ℕ) : ℤ := psub (pair n 0) @@ -233,7 +233,7 @@ calc theorem of_nat_inj {n m : ℕ} (H : of_nat n = of_nat m) : n = m := calc - n = to_nat (of_nat n) : symm (to_nat_of_nat n) + n = to_nat (of_nat n) : (to_nat_of_nat n)⁻¹ ... = to_nat (of_nat m) : {H} ... = m : to_nat_of_nat m @@ -242,7 +242,7 @@ obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, have H2 : dist xa ya = 0, from calc dist xa ya = (to_nat (psub (pair xa ya))) : by simp - ... = (to_nat a) : {symm Ha} + ... = (to_nat a) : {Ha⁻¹} ... = 0 : H, have H3 : xa = ya, from dist_eq_zero H2, calc @@ -281,7 +281,7 @@ theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b := iff_mp (by simp) (congr_arg neg H) theorem neg_move {a b : ℤ} (H : -a = b) : -b = a := -subst H (neg_neg a) +H ▸ neg_neg a theorem to_nat_neg (a : ℤ) : (to_nat (-a)) = (to_nat a) := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, @@ -308,19 +308,19 @@ theorem cases (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - n) : have Hrep : proj (rep a) = rep a, from @idempotent_image_fix _ proj proj_idempotent a, or_imp_or (or_swap (proj_zero_or (rep a))) (assume H : pr2 (proj (rep a)) = 0, - have H2 : pr2 (rep a) = 0, from subst Hrep H, + have H2 : pr2 (rep a) = 0, from Hrep ▸ H, exists_intro (pr1 (rep a)) (calc - a = psub (rep a) : symm (psub_rep a) - ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))} + a = psub (rep a) : (psub_rep a)⁻¹ + ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹} ... = psub (pair (pr1 (rep a)) 0) : {H2} ... = of_nat (pr1 (rep a)) : rfl)) (assume H : pr1 (proj (rep a)) = 0, - have H2 : pr1 (rep a) = 0, from subst Hrep H, + have H2 : pr1 (rep a) = 0, from Hrep ▸ H, exists_intro (pr2 (rep a)) (calc - a = psub (rep a) : symm (psub_rep a) - ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))} + a = psub (rep a) : (psub_rep a)⁻¹ + ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹} ... = psub (pair 0 (pr2 (rep a))) : {H2} ... = -(psub (pair (pr2 (rep a)) 0)) : by simp ... = -(of_nat (pr2 (rep a))) : rfl)) @@ -331,8 +331,8 @@ opaque_hint (hiding int) theorem int_by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) : P a := or_elim (cases a) - (assume H, obtain (n : ℕ) (H3 : a = n), from H, subst (symm H3) (H1 n)) - (assume H, obtain (n : ℕ) (H3 : a = -n), from H, subst (symm H3) (H2 n)) + (assume H, obtain (n : ℕ) (H3 : a = n), from H, H3⁻¹ ▸ H1 n) + (assume H, obtain (n : ℕ) (H3 : a = -n), from H, H3⁻¹ ▸ H2 n) ---reverse equalities, rename theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - (of_nat (succ n))) := @@ -350,14 +350,14 @@ or_elim (cases a) or_inl (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 H3 ▸ H2, or_inr (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 := 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 n), from H, H3⁻¹ ▸ H1 n) + (assume H, obtain (n : ℕ) (H3 : a = -(of_nat (succ n))), from H, 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 @@ -421,7 +421,7 @@ have H0 : 0 = psub (pair 0 0), from rfl, by simp theorem add_zero_left (a : ℤ) : 0 + a = a := -subst (add_comm a 0) (add_zero_right a) +add_comm a 0 ▸ add_zero_right a theorem add_inverse_right (a : ℤ) : a + -a = 0 := have H : ∀n, psub (pair n n) = 0, from eq_zero_intro, @@ -429,7 +429,7 @@ obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, by simp theorem add_inverse_left (a : ℤ) : -a + a = 0 := -subst (add_comm a (-a)) (add_inverse_right a) +add_comm a (-a) ▸ add_inverse_right a theorem neg_add_distr (a b : ℤ) : -(a + b) = -a + -b := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, @@ -470,16 +470,16 @@ add_comm (-a) b -- opaque_hint (hiding int.sub) theorem sub_neg_right (a b : ℤ) : a - (-b) = a + b := -subst (neg_neg b) (eq.refl (a - (-b))) +neg_neg b ▸ eq.refl (a - (-b)) theorem sub_neg_neg (a b : ℤ) : -a - (-b) = b - a := -subst (neg_neg b) (add_comm (-a) (-(-b))) +neg_neg b ▸ add_comm (-a) (-(-b)) theorem sub_self (a : ℤ) : a - a = 0 := add_inverse_right a theorem sub_zero_right (a : ℤ) : a - 0 = a := -subst (symm neg_zero) (add_zero_right a) +neg_zero⁻¹ ▸ add_zero_right a theorem sub_zero_left (a : ℤ) : 0 - a = -a := add_zero_left (-a) @@ -497,12 +497,12 @@ calc theorem sub_sub_assoc (a b c : ℤ) : a - b - c = a - (b + c) := calc a - b - c = a + (-b + -c) : add_assoc a (-b) (-c) - ... = a + -(b + c) : {symm (neg_add_distr b c)} + ... = a + -(b + c) : {(neg_add_distr b c)⁻¹} theorem sub_add_assoc (a b c : ℤ) : a - b + c = a - (b - c) := calc a - b + c = a + (-b + c) : add_assoc a (-b) c - ... = a + -(b - c) : {symm (neg_sub b c)} + ... = a + -(b - c) : {(neg_sub b c)⁻¹} theorem add_sub_assoc (a b c : ℤ) : a + b - c = a + (b - c) := add_assoc a b (-c) @@ -514,10 +514,10 @@ calc ... = a : add_zero_right a theorem add_sub_inverse2 (a b : ℤ) : a + b - a = b := -subst (add_comm b a) (add_sub_inverse b a) +add_comm b a ▸ add_sub_inverse b a theorem sub_add_inverse (a b : ℤ) : a - b + b = a := -subst (add_right_comm a b (-b)) (add_sub_inverse a b) +add_right_comm a b (-b) ▸ add_sub_inverse a b -- add_rewrite add_zero_left add_zero_right -- add_rewrite add_comm add_assoc add_left_comm @@ -534,22 +534,22 @@ subst (add_right_comm a b (-b)) (add_sub_inverse a b) theorem add_cancel_right {a b c : ℤ} (H : a + c = b + c) : a = b := calc - a = a + c - c : symm (add_sub_inverse a c) + a = a + c - c : (add_sub_inverse a c)⁻¹ ... = b + c - c : {H} ... = b : add_sub_inverse b c theorem add_cancel_left {a b c : ℤ} (H : a + b = a + c) : b = c := -add_cancel_right (subst (subst H (add_comm a b)) (add_comm a c)) +add_cancel_right ((H ▸ (add_comm a b)) ▸ add_comm a c) theorem add_eq_zero_right {a b : ℤ} (H : a + b = 0) : -a = b := -have H2 : a + -a = a + b, from subst (symm (add_inverse_right a)) (symm H), +have H2 : a + -a = a + b, from (add_inverse_right a)⁻¹ ▸ H⁻¹, show -a = b, from add_cancel_left H2 theorem add_eq_zero_left {a b : ℤ} (H : a + b = 0) : -b = a := neg_move (add_eq_zero_right H) theorem add_eq_self {a b : ℤ} (H : a + b = a) : b = 0 := -add_cancel_left (trans H (symm (add_zero_right a))) +add_cancel_left (H ⬝ (add_zero_right a)⁻¹) theorem sub_inj_left {a b c : ℤ} (H : a - b = a - c) : b = c := neg_inj (add_cancel_left H) @@ -561,14 +561,14 @@ theorem sub_eq_zero {a b : ℤ} (H : a - b = 0) : a = b := neg_inj (add_eq_zero_right H) theorem add_imp_sub_right {a b c : ℤ} (H : a + b = c) : c - b = a := -have H2 : c - b + b = a + b, from trans (sub_add_inverse c b) (symm H), +have H2 : c - b + b = a + b, from (sub_add_inverse c b) ⬝ H⁻¹, add_cancel_right H2 theorem add_imp_sub_left {a b c : ℤ} (H : a + b = c) : c - a = b := -add_imp_sub_right (subst (add_comm a b) H) +add_imp_sub_right (add_comm a b ▸ H) theorem sub_imp_add {a b c : ℤ} (H : a - b = c) : c + b = a := -subst (neg_neg b) (add_imp_sub_right H) +neg_neg b ▸ add_imp_sub_right H theorem sub_imp_sub {a b c : ℤ} (H : a - b = c) : a - c = b := have H2 : c + b = a, from sub_imp_add H, add_imp_sub_left H2 @@ -576,11 +576,11 @@ have H2 : c + b = a, from sub_imp_add H, add_imp_sub_left H2 theorem sub_add_add_right (a b c : ℤ) : a + c - (b + c) = a - b := calc a + c - (b + c) = a + (c - (b + c)) : add_sub_assoc a c (b + c) - ... = a + (c - b - c) : {symm (sub_sub_assoc c b c)} + ... = a + (c - b - c) : {(sub_sub_assoc c b c)⁻¹} ... = a + -b : {add_sub_inverse2 c (-b)} theorem sub_add_add_left (a b c : ℤ) : c + a - (c + b) = a - b := -subst (add_comm b c) (subst (add_comm a c) (sub_add_add_right a b c)) +add_comm b c ▸ add_comm a c ▸ sub_add_add_right a b c -- TODO: fix this theorem dist_def (n m : ℕ) : dist n m = (to_nat (of_nat n - m)) := @@ -631,7 +631,7 @@ theorem mul_comp (n m k l : ℕ) : have H : ∀u v, psub u * psub v = psub (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v)), from comp_quotient_map_binary_refl @rel_refl quotient @rel_mul, -trans (H (pair n m) (pair k l)) (by simp) +H (pair n m) (pair k l) ⬝ by simp -- add_rewrite mul_comp @@ -660,7 +660,7 @@ have H0 : 0 = psub (pair 0 0), from rfl, by simp theorem mul_zero_left (a : ℤ) : 0 * a = 0 := -subst (mul_comm a 0) (mul_zero_right a) +mul_comm a 0 ▸ mul_zero_right a theorem mul_one_right (a : ℤ) : a * 1 = a := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, @@ -668,7 +668,7 @@ have H1 : 1 = psub (pair 1 0), from rfl, by simp theorem mul_one_left (a : ℤ) : 1 * a = a := -subst (mul_comm a 1) (mul_one_right a) +mul_comm a 1 ▸ mul_one_right a theorem mul_neg_right (a b : ℤ) : a * -b = -(a * b) := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, @@ -676,7 +676,7 @@ obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b, by simp theorem mul_neg_left (a b : ℤ) : -a * b = -(a * b) := -subst (mul_comm b a) (subst (mul_comm b (-a)) (mul_neg_right b a)) +mul_comm b a ▸ mul_comm b (-a) ▸ mul_neg_right b a -- add_rewrite mul_neg_right mul_neg_left @@ -727,7 +727,7 @@ by simp theorem mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 := have H2 : (to_nat a) * (to_nat b) = 0, from calc - (to_nat a) * (to_nat b) = (to_nat (a * b)) : symm (mul_to_nat a b) + (to_nat a) * (to_nat b) = (to_nat (a * b)) : (mul_to_nat a b)⁻¹ ... = (to_nat 0) : {H} ... = 0 : to_nat_of_nat 0, have H3 : (to_nat a) = 0 ∨ (to_nat b) = 0, from mul_eq_zero H2, @@ -744,7 +744,7 @@ theorem mul_cancel_left {a b c : ℤ} (H1 : a ≠ 0) (H2 : a * b = a * c) : b = resolve_right (mul_cancel_left_or H2) H1 theorem mul_cancel_right_or {a b c : ℤ} (H : b * a = c * a) : a = 0 ∨ b = c := -mul_cancel_left_or (subst (subst H (mul_comm b a)) (mul_comm c a)) +mul_cancel_left_or ((H ▸ (mul_comm b a)) ▸ mul_comm c a) theorem mul_cancel_right {a b c : ℤ} (H1 : c ≠ 0) (H2 : a * c = b * c) : a = b := resolve_right (mul_cancel_right_or H2) H1 @@ -763,9 +763,7 @@ not_intro absurd H3 H) theorem mul_ne_zero_right {a b : ℤ} (H : a * b ≠ 0) : b ≠ 0 := -mul_ne_zero_left (subst (mul_comm a b) H) - - +mul_ne_zero_left (mul_comm a b ▸ H) -- set_opaque rel true -- set_opaque rep true diff --git a/library/data/int/order.lean b/library/data/int/order.lean index b35875261e..4f83ec6986 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -36,11 +36,11 @@ theorem le_of_nat (n m : ℕ) : (of_nat n ≤ of_nat m) ↔ (n ≤ m) := iff_intro (assume H : of_nat n ≤ of_nat m, obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le_elim H, - have H2 : n + k = m, from of_nat_inj (trans (symm (add_of_nat n k)) Hk), + have H2 : n + k = m, from of_nat_inj ((add_of_nat n k)⁻¹ ⬝ Hk), nat.le_intro H2) (assume H : n ≤ m, obtain (k : ℕ) (Hk : n + k = m), from nat.le_elim H, - have H2 : of_nat n + of_nat k = of_nat m, from subst Hk (add_of_nat n k), + have H2 : of_nat n + of_nat k = of_nat m, from Hk ▸ add_of_nat n k, le_intro H2) theorem le_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := @@ -48,8 +48,8 @@ obtain (n : ℕ) (Hn : a + n = b), from le_elim H1, obtain (m : ℕ) (Hm : b + m = c), from le_elim H2, have H3 : a + of_nat (n + m) = c, from calc - a + of_nat (n + m) = a + (of_nat n + m) : {symm (add_of_nat n m)} - ... = a + n + m : symm (add_assoc a n m) + a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹} + ... = a + n + m : (add_assoc a n m)⁻¹ ... = b + m : {Hn} ... = c : Hm, le_intro H3 @@ -59,18 +59,18 @@ obtain (n : ℕ) (Hn : a + n = b), from le_elim H1, obtain (m : ℕ) (Hm : b + m = a), from le_elim H2, have H3 : a + of_nat (n + m) = a + 0, from calc - a + of_nat (n + m) = a + (of_nat n + m) : {symm (add_of_nat n m)} - ... = a + n + m : symm (add_assoc a n m) + a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹} + ... = a + n + m : (add_assoc a n m)⁻¹ ... = b + m : {Hn} ... = a : Hm - ... = a + 0 : symm (add_zero_right a), + ... = a + 0 : (add_zero_right a)⁻¹, have H4 : of_nat (n + m) = of_nat 0, from add_cancel_left H3, have H5 : n + m = 0, from of_nat_inj H4, have H6 : n = 0, from nat.add_eq_zero_left H5, show a = b, from calc - a = a + of_nat 0 : symm (add_zero_right a) - ... = a + n : {symm H6} + a = a + of_nat 0 : (add_zero_right a)⁻¹ + ... = a + n : {H6⁻¹} ... = b : Hn -- ### interaction with add @@ -90,22 +90,22 @@ have H2 : c + a + n = c + b, from le_intro H2 theorem add_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a + c ≤ b + c := -subst (add_comm c b) (subst (add_comm c a) (add_le_left H c)) +add_comm c b ▸ add_comm c a ▸ add_le_left H c theorem add_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : c ≤ d) : a + c ≤ b + d := le_trans (add_le_right H1 c) (add_le_left H2 b) theorem add_le_cancel_right {a b c : ℤ} (H : a + c ≤ b + c) : a ≤ b := have H1 : a + c + -c ≤ b + c + -c, from add_le_right H (-c), -have H2 : a + c - c ≤ b + c - c, from subst (add_neg_right _ _) (subst (add_neg_right _ _) H1), -subst (add_sub_inverse b c) (subst (add_sub_inverse a c) H2) +have H2 : a + c - c ≤ b + c - c, from add_neg_right _ _ ▸ add_neg_right _ _ ▸ H1, +add_sub_inverse b c ▸ add_sub_inverse a c ▸ H2 theorem add_le_cancel_left {a b c : ℤ} (H : c + a ≤ c + b) : a ≤ b := -add_le_cancel_right (subst (add_comm c b) (subst (add_comm c a) H)) +add_le_cancel_right (add_comm c b ▸ add_comm c a ▸ H) theorem add_le_inv {a b c d : ℤ} (H1 : a + b ≤ c + d) (H2 : c ≤ a) : b ≤ d := obtain (n : ℕ) (Hn : c + n = a), from le_elim H2, -have H3 : c + (n + b) ≤ c + d, from subst (add_assoc c n b) (subst (symm Hn) H1), +have H3 : c + (n + b) ≤ c + d, from add_assoc c n b ▸ Hn⁻¹ ▸ H1, have H4 : n + b ≤ d, from add_le_cancel_left H3, show b ≤ d, from le_trans (le_add_of_nat_left b n) H4 @@ -118,8 +118,8 @@ discriminate (assume H2 : n = 0, have H3 : a = b, from calc - a = a + 0 : symm (add_zero_right a) - ... = a + n : {symm H2} + a = a + 0 : (add_zero_right a)⁻¹ + ... = a + n : {H2⁻¹} ... = b : Hn, or_inr H3) (take k : ℕ, @@ -138,45 +138,44 @@ obtain (n : ℕ) (Hn : a + n = b), from le_elim H, have H2 : b - n = a, from add_imp_sub_right Hn, have H3 : -b + n = -a, from calc - -b + n = -b + -(-n) : {symm (neg_neg n)} - ... = -(b + -n) : symm (neg_add_distr b (-n)) + -b + n = -b + -(-n) : {(neg_neg n)⁻¹} + ... = -(b + -n) : (neg_add_distr b (-n))⁻¹ ... = -(b - n) : {add_neg_right _ _} ... = -a : {H2}, le_intro H3 theorem neg_le_zero {a : ℤ} (H : 0 ≤ a) : -a ≤ 0 := -subst neg_zero (le_neg H) +neg_zero ▸ (le_neg H) theorem zero_le_neg {a : ℤ} (H : a ≤ 0) : 0 ≤ -a := -subst neg_zero (le_neg H) +neg_zero ▸ (le_neg H) theorem le_neg_inv {a b : ℤ} (H : -a ≤ -b) : b ≤ a := -subst (neg_neg b) (subst (neg_neg a) (le_neg H)) +neg_neg b ▸ neg_neg a ▸ le_neg H theorem le_sub_of_nat (a : ℤ) (n : ℕ) : a - n ≤ a := le_intro (sub_add_inverse a n) theorem sub_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a - c ≤ b - c := -subst (add_neg_right _ _) (subst (add_neg_right _ _) (add_le_right H (-c))) +add_neg_right _ _ ▸ add_neg_right _ _ ▸ add_le_right H _ theorem sub_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c - b ≤ c - a := -subst (add_neg_right _ _) (subst (add_neg_right _ _) (add_le_left (le_neg H) c)) +add_neg_right _ _ ▸ add_neg_right _ _ ▸ add_le_left (le_neg H) _ theorem sub_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : d ≤ c) : a - c ≤ b - d := -subst (add_neg_right _ _) (subst (add_neg_right _ _) (add_le H1 (le_neg H2))) +add_neg_right _ _ ▸ add_neg_right _ _ ▸ add_le H1 (le_neg H2) theorem sub_le_right_inv {a b c : ℤ} (H : a - c ≤ b - c) : a ≤ b := -add_le_cancel_right (subst (symm (add_neg_right _ _)) (subst (symm (add_neg_right _ _)) H)) +add_le_cancel_right ((add_neg_right _ _)⁻¹ ▸ (add_neg_right _ _)⁻¹ ▸ H) theorem sub_le_left_inv {a b c : ℤ} (H : c - a ≤ c - b) : b ≤ a := le_neg_inv (add_le_cancel_left - (subst (symm (add_neg_right _ _)) (subst (symm (add_neg_right _ _)) H))) + ((add_neg_right _ _)⁻¹ ▸ (add_neg_right _ _)⁻¹ ▸ H)) theorem le_iff_sub_nonneg (a b : ℤ) : a ≤ b ↔ 0 ≤ b - a := iff_intro - (assume H, subst (sub_self _) (sub_le_right H a)) - (assume H, subst (sub_add_inverse _ _) (subst (add_zero_left _) (add_le_right H a))) - + (assume H, sub_self _ ▸ sub_le_right H a) + (assume H, sub_add_inverse _ _ ▸ add_zero_left _ ▸ add_le_right H a) -- Less than, Greater than, Greater than or equal -- ---------------------------------------------- @@ -206,7 +205,7 @@ theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n := le_intro (show a + 1 + n = a + succ n, by simp) theorem lt_intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b := -subst H (lt_add_succ a n) +H ▸ lt_add_succ a n theorem lt_elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b := obtain (n : ℕ) (Hn : a + 1 + n = b), from le_elim H, @@ -231,7 +230,7 @@ not_intro absurd H4 succ_ne_zero) theorem lt_imp_ne {a b : ℤ} (H : a < b) : a ≠ b := -not_intro (assume H2 : a = b, absurd (subst H2 H) (lt_irrefl b)) +not_intro (assume H2 : a = b, absurd (H2 ▸ H) (lt_irrefl b)) theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) := calc @@ -293,10 +292,10 @@ le_imp_not_gt (lt_imp_le H) -- ### interaction with addition theorem add_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b := -subst (symm (add_assoc c a 1)) (add_le_left H c) +(add_assoc c a 1)⁻¹ ▸ add_le_left H c theorem add_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a + c < b + c := -subst (add_comm c b) (subst (add_comm c a) (add_lt_left H c)) +add_comm c b ▸ add_comm c a ▸ add_lt_left H c theorem add_le_lt {a b c d : ℤ} (H1 : a ≤ c) (H2 : b < d) : a + b < c + d := le_lt_trans (add_le_right H1 b) (add_lt_left H2 c) @@ -308,11 +307,10 @@ theorem add_lt {a b c d : ℤ} (H1 : a < c) (H2 : b < d) : a + b < c + d := add_lt_le H1 (lt_imp_le H2) theorem add_lt_cancel_left {a b c : ℤ} (H : c + a < c + b) : a < b := -add_le_cancel_left (subst (add_assoc c a 1) (show c + a + 1 ≤ c + b, from H)) +add_le_cancel_left (add_assoc c a 1 ▸ H) theorem add_lt_cancel_right {a b c : ℤ} (H : a + c < b + c) : a < b := -add_lt_cancel_left (subst (add_comm b c) (subst (add_comm a c) H)) - +add_lt_cancel_left (add_comm b c ▸ add_comm a c ▸ H) -- ### interaction with neg and sub @@ -320,35 +318,35 @@ theorem lt_neg {a b : ℤ} (H : a < b) : -b < -a := have H2 : -(a + 1) + 1 = -a, by simp, have H3 : -b ≤ -(a + 1), from le_neg H, have H4 : -b + 1 ≤ -(a + 1) + 1, from add_le_right H3 1, -subst H2 H4 +H2 ▸ H4 theorem neg_lt_zero {a : ℤ} (H : 0 < a) : -a < 0 := -subst neg_zero (lt_neg H) +neg_zero ▸ lt_neg H theorem zero_lt_neg {a : ℤ} (H : a < 0) : 0 < -a := -subst neg_zero (lt_neg H) +neg_zero ▸ lt_neg H theorem lt_neg_inv {a b : ℤ} (H : -a < -b) : b < a := -subst (neg_neg b) (subst (neg_neg a) (lt_neg H)) +neg_neg b ▸ neg_neg a ▸ lt_neg H theorem lt_sub_of_nat_succ (a : ℤ) (n : ℕ) : a - succ n < a := lt_intro (sub_add_inverse a (succ n)) theorem sub_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a - c < b - c := -subst (add_neg_right _ _) (subst (add_neg_right _ _) (add_lt_right H (-c))) +add_neg_right _ _ ▸ add_neg_right _ _ ▸ add_lt_right H _ theorem sub_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c - b < c - a := -subst (add_neg_right _ _) (subst (add_neg_right _ _) (add_lt_left (lt_neg H) c)) +add_neg_right _ _ ▸ add_neg_right _ _ ▸ add_lt_left (lt_neg H) _ theorem sub_lt {a b c d : ℤ} (H1 : a < b) (H2 : d < c) : a - c < b - d := -subst (add_neg_right _ _) (subst (add_neg_right _ _) (add_lt H1 (lt_neg H2))) +add_neg_right _ _ ▸ add_neg_right _ _ ▸ add_lt H1 (lt_neg H2) theorem sub_lt_right_inv {a b c : ℤ} (H : a - c < b - c) : a < b := -add_lt_cancel_right (subst (symm (add_neg_right _ _)) (subst (symm (add_neg_right _ _)) H)) +add_lt_cancel_right ((add_neg_right _ _)⁻¹ ▸ (add_neg_right _ _)⁻¹ ▸ H) theorem sub_lt_left_inv {a b c : ℤ} (H : c - a < c - b) : b < a := lt_neg_inv (add_lt_cancel_left - (subst (symm (add_neg_right _ _)) (subst (symm (add_neg_right _ _)) H))) + ((add_neg_right _ _)⁻¹ ▸ (add_neg_right _ _)⁻¹ ▸ H)) -- ### totality of lt and le @@ -369,7 +367,7 @@ int_by_cases a show of_nat n ≤ m ∨ of_nat n > m, by simp) -- from (by simp) ◂ (le_or_gt n m)) (take m : ℕ, show n ≤ -succ m ∨ n > -succ m, from - have H0 : -succ m < -m, from lt_neg (subst (symm (of_nat_succ m)) (self_lt_succ m)), + have H0 : -succ m < -m, from lt_neg ((of_nat_succ m)⁻¹ ▸ self_lt_succ m), have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n), or_inr H)) (take n : ℕ, @@ -409,17 +407,17 @@ resolve_right (le_or_gt a b) H theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n := obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le_elim H, -exists_intro n (trans (symm Hn) (add_zero_left n)) +exists_intro n (Hn⁻¹ ⬝ add_zero_left n) theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n := have H2 : -a ≥ 0, from zero_le_neg H, obtain (n : ℕ) (Hn : -a = n), from pos_imp_exists_nat H2, -have H3 : a = -n, from symm (neg_move Hn), +have H3 : a = -n, from (neg_move Hn)⁻¹, exists_intro n H3 theorem to_nat_nonneg_eq {a : ℤ} (H : a ≥ 0) : (to_nat a) = a := obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H, -subst (symm Hn) (congr_arg of_nat (to_nat_of_nat n)) +Hn⁻¹ ▸ congr_arg of_nat (to_nat_of_nat n) theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 := iff_mp (iff_symm (le_of_nat _ _)) zero_le @@ -430,7 +428,7 @@ have aux : ∀x, decidable (0 ≤ x), from have H : 0 ≤ x ↔ of_nat (to_nat x) = x, from iff_intro (assume H1, to_nat_nonneg_eq H1) - (assume H1, subst H1 (of_nat_nonneg (to_nat x))), + (assume H1, H1 ▸ of_nat_nonneg (to_nat x)), decidable_iff_equiv _ (iff_symm H), decidable_iff_equiv (aux _) (iff_symm (le_iff_sub_nonneg a b)) @@ -445,12 +443,12 @@ calc (to_nat a) = (to_nat ( -n)) : {Hn} ... = (to_nat n) : {to_nat_neg n} ... = n : {to_nat_of_nat n} - ... = -a : symm (neg_move (symm Hn)) + ... = -a : (neg_move (Hn⁻¹))⁻¹ theorem to_nat_cases (a : ℤ) : a = (to_nat a) ∨ a = - (to_nat a) := or_imp_or (le_total 0 a) - (assume H : a ≥ 0, symm (to_nat_nonneg_eq H)) - (assume H : a ≤ 0, symm (neg_move (symm (to_nat_negative H)))) + (assume H : a ≥ 0, (to_nat_nonneg_eq H)⁻¹) + (assume H : a ≤ 0, (neg_move ((to_nat_negative H)⁻¹))⁻¹) -- ### interaction of mul with le and lt @@ -465,15 +463,15 @@ have H2 : a * b + of_nat ((to_nat a) * n) = a * c, from le_intro H2 theorem mul_le_right_nonneg {a b c : ℤ} (Hb : b ≥ 0) (H : a ≤ c) : a * b ≤ c * b := -subst (mul_comm b c) (subst (mul_comm b a) (mul_le_left_nonneg Hb H)) +mul_comm b c ▸ mul_comm b a ▸ mul_le_left_nonneg Hb H theorem mul_le_left_nonpos {a b c : ℤ} (Ha : a ≤ 0) (H : b ≤ c) : a * c ≤ a * b := have H2 : -a * b ≤ -a * c, from mul_le_left_nonneg (zero_le_neg Ha) H, -have H3 : -(a * b) ≤ -(a * c), from subst (mul_neg_left a c) (subst (mul_neg_left a b) H2), +have H3 : -(a * b) ≤ -(a * c), from mul_neg_left a c ▸ mul_neg_left a b ▸ H2, le_neg_inv H3 theorem mul_le_right_nonpos {a b c : ℤ} (Hb : b ≤ 0) (H : c ≤ a) : a * b ≤ c * b := -subst (mul_comm b c) (subst (mul_comm b a) (mul_le_left_nonpos Hb H)) +mul_comm b c ▸ mul_comm b a ▸ mul_le_left_nonpos Hb H ---this theorem can be made more general by replacing either Ha with 0 ≤ a or Hb with 0 ≤ d... theorem mul_le_nonneg {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b ≤ d) @@ -485,20 +483,20 @@ theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb : b ≤ 0) (Hc : c ≤ le_trans (mul_le_right_nonpos Hb Hc) (mul_le_left_nonpos (le_trans Hc Ha) Hd) theorem mul_lt_left_pos {a b c : ℤ} (Ha : a > 0) (H : b < c) : a * b < a * c := -have H2 : a * b < a * b + a, from subst (add_zero_right (a * b)) (add_lt_left Ha (a * b)), -have H3 : a * b + a ≤ a * c, from subst (by simp) (mul_le_left_nonneg (lt_imp_le Ha) H), +have H2 : a * b < a * b + a, from add_zero_right (a * b) ▸ add_lt_left Ha (a * b), +have H3 : a * b + a ≤ a * c, from (by simp) ▸ mul_le_left_nonneg (lt_imp_le Ha) H, lt_le_trans H2 H3 theorem mul_lt_right_pos {a b c : ℤ} (Hb : b > 0) (H : a < c) : a * b < c * b := -subst (mul_comm b c) (subst (mul_comm b a) (mul_lt_left_pos Hb H)) +mul_comm b c ▸ mul_comm b a ▸ mul_lt_left_pos Hb H theorem mul_lt_left_neg {a b c : ℤ} (Ha : a < 0) (H : b < c) : a * c < a * b := have H2 : -a * b < -a * c, from mul_lt_left_pos (zero_lt_neg Ha) H, -have H3 : -(a * b) < -(a * c), from subst (mul_neg_left a c) (subst (mul_neg_left a b) H2), +have H3 : -(a * b) < -(a * c), from mul_neg_left a c ▸ mul_neg_left a b ▸ H2, lt_neg_inv H3 theorem mul_lt_right_neg {a b c : ℤ} (Hb : b < 0) (H : c < a) : a * b < c * b := -subst (mul_comm b c) (subst (mul_comm b a) (mul_lt_left_neg Hb H)) +mul_comm b c ▸ mul_comm b a ▸ mul_lt_left_neg Hb H theorem mul_le_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b < d) : a * b < c * d := @@ -526,17 +524,17 @@ or_elim (le_or_gt b a) (assume H2 : a < b, H2) theorem mul_lt_cancel_right_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : a * c < b * c) : a < b := -mul_lt_cancel_left_nonneg Hc (subst (mul_comm b c) (subst (mul_comm a c) H)) +mul_lt_cancel_left_nonneg Hc (mul_comm b c ▸ mul_comm a c ▸ H) theorem mul_lt_cancel_left_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : c * b < c * a) : a < b := have H2 : -(c * a) < -(c * b), from lt_neg H, have H3 : -c * a < -c * b, - from subst (symm (mul_neg_left c b)) (subst (symm (mul_neg_left c a)) H2), + from (mul_neg_left c b)⁻¹ ▸ (mul_neg_left c a)⁻¹ ▸ H2, have H4 : -c ≥ 0, from zero_le_neg Hc, mul_lt_cancel_left_nonneg H4 H3 theorem mul_lt_cancel_right_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : b * c < a * c) : a < b := -mul_lt_cancel_left_nonpos Hc (subst (mul_comm b c) (subst (mul_comm a c) H)) +mul_lt_cancel_left_nonpos Hc (mul_comm b c ▸ mul_comm a c ▸ H) theorem mul_le_cancel_left_pos {a b c : ℤ} (Hc : c > 0) (H : c * a ≤ c * b) : a ≤ b := or_elim (le_or_gt a b) @@ -546,31 +544,31 @@ or_elim (le_or_gt a b) absurd H3 (le_imp_not_gt H)) theorem mul_le_cancel_right_pos {a b c : ℤ} (Hc : c > 0) (H : a * c ≤ b * c) : a ≤ b := -mul_le_cancel_left_pos Hc (subst (mul_comm b c) (subst (mul_comm a c) H)) +mul_le_cancel_left_pos Hc (mul_comm b c ▸ mul_comm a c ▸ H) theorem mul_le_cancel_left_neg {a b c : ℤ} (Hc : c < 0) (H : c * b ≤ c * a) : a ≤ b := have H2 : -(c * a) ≤ -(c * b), from le_neg H, have H3 : -c * a ≤ -c * b, - from subst (symm (mul_neg_left c b)) (subst (symm (mul_neg_left c a)) H2), + from (mul_neg_left c b)⁻¹ ▸ (mul_neg_left c a)⁻¹ ▸ H2, have H4 : -c > 0, from zero_lt_neg Hc, mul_le_cancel_left_pos H4 H3 theorem mul_le_cancel_right_neg {a b c : ℤ} (Hc : c < 0) (H : b * c ≤ a * c) : a ≤ b := -mul_le_cancel_left_neg Hc (subst (mul_comm b c) (subst (mul_comm a c) H)) +mul_le_cancel_left_neg Hc (mul_comm b c ▸ mul_comm a c ▸ H) theorem mul_eq_one_left {a b : ℤ} (H : a * b = 1) : a = 1 ∨ a = - 1 := have H2 : (to_nat a) * (to_nat b) = 1, from calc - (to_nat a) * (to_nat b) = (to_nat (a * b)) : symm (mul_to_nat a b) + (to_nat a) * (to_nat b) = (to_nat (a * b)) : (mul_to_nat a b)⁻¹ ... = (to_nat 1) : {H} ... = 1 : to_nat_of_nat 1, have H3 : (to_nat a) = 1, from mul_eq_one_left H2, or_imp_or (to_nat_cases a) - (assume H4 : a = (to_nat a), subst H3 H4) - (assume H4 : a = - (to_nat a), subst H3 H4) + (assume H4 : a = (to_nat a), H3 ▸ H4) + (assume H4 : a = - (to_nat a), H3 ▸ H4) theorem mul_eq_one_right {a b : ℤ} (H : a * b = 1) : b = 1 ∨ b = - 1 := -mul_eq_one_left (subst (mul_comm a b) H) +mul_eq_one_left (mul_comm a b ▸ H) -- sign function @@ -612,8 +610,8 @@ or_elim (em (a = 0)) have H : sign (a * b) * (to_nat (a * b)) = sign a * sign b * (to_nat (a * b)), from calc sign (a * b) * (to_nat (a * b)) = a * b : mul_sign_to_nat (a * b) - ... = sign a * (to_nat a) * b : {symm (mul_sign_to_nat a)} - ... = sign a * (to_nat a) * (sign b * (to_nat b)) : {symm (mul_sign_to_nat b)} + ... = sign a * (to_nat a) * b : {(mul_sign_to_nat a)⁻¹} + ... = sign a * (to_nat a) * (sign b * (to_nat b)) : {(mul_sign_to_nat b)⁻¹} ... = sign a * sign b * (to_nat (a * b)) : by simp, have H2 : (to_nat (a * b)) ≠ 0, from take H2', mul_ne_zero Ha Hb (to_nat_eq_zero H2'), diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 0f08220506..8f07abc57a 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -224,12 +224,12 @@ induction_on l or_elim H (assume H1 : x = y, exists_intro nil - (exists_intro l (subst H1 rfl))) + (exists_intro l (H1 ▸ rfl))) (assume H1 : x ∈ l, obtain s (H2 : ∃t : list T, l = s ++ (x :: t)), from IH H1, obtain t (H3 : l = s ++ (x :: t)), from H2, have H4 : y :: l = (y :: s) ++ (x :: t), - from subst H3 rfl, + from H3 ▸ rfl, exists_intro _ (exists_intro _ H4))) -- Find diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 4d07c81fd2..4cc73d8961 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -111,7 +111,7 @@ have general : ∀n, decidable (n = m), from (λ m iH, inr succ_ne_zero)) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), take n, rec_on n - (inr (ne_symm succ_ne_zero)) + (inr (ne.symm succ_ne_zero)) (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), have d1 : decidable (n' = m'), from iH1 n', decidable.rec_on d1 @@ -358,12 +358,12 @@ discriminate (take (l : ℕ), assume (Hl : m = succ l), have Heq : succ (k * succ l + l) = n * m, from - symm (calc + (calc n * m = n * succ l : {Hl} ... = succ k * succ l : {Hk} ... = k * succ l + succ l : mul_succ_left - ... = succ (k * succ l + l) : add_succ_right), - absurd (trans Heq H) succ_ne_zero)) + ... = succ (k * succ l + l) : add_succ_right)⁻¹, + absurd (Heq ⬝ H) succ_ne_zero)) ---other inversion theorems appear below diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 4ad9a954e9..8edd2566c2 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -75,7 +75,7 @@ case_strong_induction_on m have H1 : f' 0 x = default, from rfl, have H2 : ¬ measure x < 0, from not_lt_zero, have H3 : restrict default measure f 0 x = default, from if_neg H2, - show f' 0 x = restrict default measure f 0 x, from trans H1 (symm H3)) + show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹) (take m, assume IH: ∀n, n ≤ m → ∀x, f' n x = restrict default measure f n x, take x : dom, @@ -108,7 +108,7 @@ case_strong_induction_on m ... = rec_val x (f' m') : if_pos self_lt_succ ... = rec_val x f : rec_decreasing _ _ _ H3a, show f' (succ m) x = restrict default measure f (succ m) x, - from trans H2 (symm H3)) + from H2 ⬝ H3⁻¹) (assume H1 : ¬ measure x < succ m, have H2 : f' (succ m) x = default, from calc @@ -117,7 +117,7 @@ case_strong_induction_on m have H3 : restrict default measure f (succ m) x = default, from if_neg H1, show f' (succ m) x = restrict default measure f (succ m) x, - from trans H2 (symm H3))) + from H2 ⬝ H3⁻¹)) theorem rec_measure_spec {dom codom : Type} {default : codom} {measure : dom → ℕ} (rec_val : dom → (dom → codom) → codom) @@ -172,7 +172,7 @@ show lhs = rhs, from calc lhs = succ (g1 (x - y)) : if_neg H1 ... = succ (g2 (x - y)) : {H _ H4} - ... = rhs : symm (if_neg H1)) + ... = rhs : (if_neg H1)⁻¹) theorem div_aux_spec (y : ℕ) (x : ℕ) : div_aux y x = if (y = 0 ∨ x < y) then 0 else succ (div_aux y (x - y)) := @@ -183,12 +183,12 @@ definition idivide (x : ℕ) (y : ℕ) : ℕ := div_aux y x infixl `div` := idivide theorem div_zero {x : ℕ} : x div 0 = 0 := -trans (div_aux_spec _ _) (if_pos (or_inl rfl)) +div_aux_spec _ _ ⬝ if_pos (or_inl rfl) -- add_rewrite div_zero theorem div_less {x y : ℕ} (H : x < y) : x div y = 0 := -trans (div_aux_spec _ _) (if_pos (or_inr H)) +div_aux_spec _ _ ⬝ if_pos (or_inr H) -- add_rewrite div_less @@ -202,9 +202,9 @@ have H3 : ¬ (y = 0 ∨ x < y), from not_intro (assume H4 : y = 0 ∨ x < y, or_elim H4 - (assume H5 : y = 0, not_elim lt_irrefl (subst H5 H1)) + (assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1)) (assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)), -trans (div_aux_spec _ _) (if_neg H3) +div_aux_spec _ _ ⬝ if_neg H3 theorem div_add_self_right {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := have H1 : z ≤ x + z, by simp, @@ -248,7 +248,7 @@ show lhs = rhs, from calc lhs = g1 (x - y) : if_neg H1 ... = g2 (x - y) : H _ H4 - ... = rhs : symm (if_neg H1)) + ... = rhs : (if_neg H1)⁻¹) theorem mod_aux_spec (y : ℕ) (x : ℕ) : mod_aux y x = if (y = 0 ∨ x < y) then x else mod_aux y (x - y) := @@ -259,12 +259,12 @@ definition modulo (x : ℕ) (y : ℕ) : ℕ := mod_aux y x infixl `mod` := modulo theorem mod_zero {x : ℕ} : x mod 0 = x := -trans (mod_aux_spec _ _) (if_pos (or_inl rfl)) +mod_aux_spec _ _ ⬝ if_pos (or_inl rfl) -- add_rewrite mod_zero theorem mod_lt_eq {x y : ℕ} (H : x < y) : x mod y = x := -trans (mod_aux_spec _ _) (if_pos (or_inr H)) +mod_aux_spec _ _ ⬝ if_pos (or_inr H) -- add_rewrite mod_lt_eq @@ -280,7 +280,7 @@ have H3 : ¬ (y = 0 ∨ x < y), from or_elim H4 (assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1)) (assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)), -(mod_aux_spec _ _) ⬝ (if_neg H3) +mod_aux_spec _ _ ⬝ if_neg H3 -- need more of these, add as rewrite rules theorem mod_add_self_right {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z := @@ -327,15 +327,15 @@ case_strong_induction_on x have H3 : succ x mod y = (succ x - y) mod y, from mod_rec H H2, have H4 : succ x - y < succ x, from sub_lt succ_pos H, have H5 : succ x - y ≤ x, from lt_succ_imp_le H4, - show succ x mod y < y, from subst (symm H3) (IH _ H5))) + show succ x mod y < y, from H3⁻¹ ▸ IH _ H5)) theorem div_mod_eq {x y : ℕ} : x = x div y * y + x mod y := case_zero_pos y (show x = x div 0 * 0 + x mod 0, from - symm (calc + (calc x div 0 * 0 + x mod 0 = 0 + x mod 0 : {mul_zero_right} ... = x mod 0 : add_zero_left - ... = x : mod_zero)) + ... = x : mod_zero)⁻¹) (take y, assume H : y > 0, show x = x div y * y + x mod y, from @@ -355,14 +355,14 @@ case_zero_pos y have H4 : succ x mod y = (succ x - y) mod y, from mod_rec H H2, have H5 : succ x - y < succ x, from sub_lt succ_pos H, have H6 : succ x - y ≤ x, from lt_succ_imp_le H5, - symm (calc + (calc succ x div y * y + succ x mod y = succ ((succ x - y) div y) * y + succ x mod y : {H3} ... = ((succ x - y) div y) * y + y + succ x mod y : {mul_succ_left} ... = ((succ x - y) div y) * y + y + (succ x - y) mod y : {H4} ... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add_right_comm ... = succ x - y + y : {(IH _ H6)⁻¹} - ... = succ x : add_sub_ge_left H2)))) + ... = succ x : add_sub_ge_left H2)⁻¹))) theorem mod_le {x y : ℕ} : x mod y ≤ x := div_mod_eq⁻¹ ▸ le_add_left @@ -380,7 +380,7 @@ calc theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y) (H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 := -have H4 : q1 * y + r2 = q2 * y + r2, from subst (remainder_unique H H1 H2 H3) H3, +have H4 : q1 * y + r2 = q2 * y + r2, from (remainder_unique H H1 H2 H3) ▸ H3, have H5 : q1 * y = q2 * y, from add_cancel_right H4, have H6 : y > 0, from le_lt_trans zero_le H1, show q1 = q2, from mul_cancel_right H6 H5 @@ -455,10 +455,10 @@ theorem dvd_iff_mod_eq_zero {x y : ℕ} : x | y ↔ y mod x = 0 := refl _ theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x := -symm (calc +(calc x = x div y * y + x mod y : div_mod_eq ... = x div y * y + 0 : {mp dvd_iff_mod_eq_zero H} - ... = x div y * y : add_zero_right) + ... = x div y * y : add_zero_right)⁻¹ -- add_rewrite dvd_imp_div_mul_eq @@ -538,7 +538,7 @@ have H4 : k = k div n * (n div m) * m, from k = k div n * n : by simp ... = k div n * (n div m * m) : {H3} ... = k div n * (n div m) * m : mul_assoc⁻¹, -mp (dvd_iff_exists_mul⁻¹) (exists_intro (k div n * (n div m)) (symm H4)) +mp (dvd_iff_exists_mul⁻¹) (exists_intro (k div n * (n div m)) (H4⁻¹)) theorem dvd_add {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 + n2) := have H : (n1 div m + n2 div m) * m = n1 + n2, by simp, @@ -548,9 +548,9 @@ theorem dvd_add_cancel_left {m n1 n2 : ℕ} : m | (n1 + n2) → m | n1 → m | n case_zero_pos m (assume H1 : 0 | n1 + n2, assume H2 : 0 | n1, - have H3 : n1 + n2 = 0, from subst zero_dvd_iff H1, - have H4 : n1 = 0, from subst zero_dvd_iff H2, - have H5 : n2 = 0, from mp (by simp) (subst H4 H3), + have H3 : n1 + n2 = 0, from zero_dvd_iff ▸ H1, + have H4 : n1 = 0, from zero_dvd_iff ▸ H2, + have H5 : n2 = 0, from mp (by simp) (H4 ▸ H3), show 0 | n2, by simp) (take m, assume mpos : m > 0, @@ -611,11 +611,11 @@ show lhs = rhs, from (assume H1 : y ≠ 0, have ypos : y > 0, from ne_zero_imp_pos H1, have H2 : gcd_aux_measure p' = x mod y, from pr2_pair _ _, - have H3 : gcd_aux_measure p' < gcd_aux_measure p, from subst (symm H2) (mod_lt ypos), + have H3 : gcd_aux_measure p' < gcd_aux_measure p, from H2⁻¹ ▸ mod_lt ypos, calc lhs = g1 p' : if_neg H1 ... = g2 p' : H _ H3 - ... = rhs : symm (if_neg H1)) + ... = rhs : (if_neg H1)⁻¹) theorem gcd_aux_spec (p : ℕ × ℕ) : gcd_aux p = let x := pr1 p, y := pr2 p in @@ -675,7 +675,7 @@ gcd_induct m n have H : gcd n (m mod n) | (m div n * n + m mod n), from dvd_add (dvd_trans (and.elim_left IH) dvd_mul_self_right) (and.elim_right IH), have H1 : gcd n (m mod n) | m, from div_mod_eq⁻¹ ▸ H, - have gcd_eq : gcd n (m mod n) = gcd m n, from symm (gcd_pos _ npos), + have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_pos _ npos)⁻¹, show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and.elim_left IH))) theorem gcd_dvd_left (m n : ℕ) : (gcd m n | m) := and.elim_left (gcd_dvd _ _) @@ -694,7 +694,7 @@ gcd_induct m n assume H2 : k | n, have H3 : k | m div n * n + m mod n, from div_mod_eq ▸ H1, have H4 : k | m mod n, from dvd_add_cancel_left H3 (dvd_trans H2 (by simp)), - have gcd_eq : gcd n (m mod n) = gcd m n, from symm (gcd_pos _ npos), - show k | gcd m n, from subst gcd_eq (IH H2 H4)) + have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_pos _ npos)⁻¹, + show k | gcd m n, from gcd_eq ▸ IH H2 H4) end nat diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index e90076fc06..3408538264 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -205,7 +205,7 @@ discriminate from calc pred n = pred (succ k) : {Hn} ... = k : pred_succ, - have H3 : k ≤ m, from subst H2 H, + have H3 : k ≤ m, from H2 ▸ H, have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3, show n ≤ m ∨ n = succ m, from or_imp_or H4 @@ -395,7 +395,7 @@ induction_on n m = k + l : Hl⁻¹ ... = k + 0 : {H2} ... = k : add_zero_right, - have H4 : m < succ k, from subst H3 self_lt_succ, + have H4 : m < succ k, from H3 ▸ self_lt_succ, or_inr H4) (take l2 : ℕ, assume H2 : l = succ l2, @@ -481,7 +481,7 @@ theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 := or_elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 := -ne_symm (lt_imp_ne H) +ne.symm (lt_imp_ne H) theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l := lt_imp_eq_succ H diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 560e68f1e6..a41a0975d5 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -52,7 +52,7 @@ induction_on m ... = n - succ k : sub_succ_right⁻¹) theorem sub_self {n : ℕ} : n - n = 0 := -induction_on n sub_zero_right (take k IH, trans sub_succ_succ IH) +induction_on n sub_zero_right (take k IH, sub_succ_succ ⬝ IH) theorem sub_add_add_right {n k m : ℕ} : (n + k) - (m + k) = n - m := induction_on k @@ -273,7 +273,7 @@ sub_split assume H1 : m + k = n, assume H2 : k = 0, have H3 : n = m, from add_zero_right ▸ H2 ▸ H1⁻¹, - subst H3 le_refl) + H3 ▸ le_refl) theorem sub_sub_split {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) := diff --git a/library/data/option.lean b/library/data/option.lean index dbd779df1a..d654eb9210 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -44,7 +44,7 @@ theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a rec_on o₁ (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂)))) (take a₁ : A, rec_on o₂ - (inr (ne_symm (none_ne_some a₁))) + (inr (ne.symm (none_ne_some a₁))) (take a₂ : A, decidable.rec_on (H a₁ a₂) (assume Heq : a₁ = a₂, inl (Heq ▸ rfl)) (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne)))) diff --git a/library/data/prod.lean b/library/data/prod.lean index 5b554092df..1f687c91f7 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -42,8 +42,10 @@ section theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p := destruct p (λx y, eq.refl (x, y)) + open eq_ops + theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) := - subst H1 (subst H2 rfl) + H1 ▸ H2 ▸ rfl theorem prod_eq {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 := destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2)) @@ -55,7 +57,7 @@ section (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) := have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from iff_intro - (assume H, subst H (and.intro rfl rfl)) + (assume H, H ▸ and.intro rfl rfl) (assume H, and.elim H (assume H4 H5, prod_eq H4 H5)), decidable_iff_equiv _ (iff_symm H3) diff --git a/library/data/quotient/aux.lean b/library/data/quotient/aux.lean index cb9b1f2871..e2c32022b3 100644 --- a/library/data/quotient/aux.lean +++ b/library/data/quotient/aux.lean @@ -30,7 +30,7 @@ prod.destruct a (take x y, rfl) theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a)) : P (pr2 (flip a)) (pr1 (flip a)) := -(symm (flip_pr1 a)) ▸ (symm (flip_pr2 a)) ▸ H +(flip_pr1 a)⁻¹ ▸ (flip_pr2 a)⁻¹ ▸ H theorem flip_inj {A B : Type} {a b : A × B} (H : flip a = flip b) : a = b := have H2 : flip (flip a) = flip (flip b), from congr_arg flip H, @@ -85,16 +85,16 @@ have Hx : pr1 (flip (map_pair2 f a b)) = pr1 (map_pair2 f (flip a) (flip b)), f calc pr1 (flip (map_pair2 f a b)) = pr2 (map_pair2 f a b) : flip_pr1 _ ... = f (pr2 a) (pr2 b) : map_pair2_pr2 f a b - ... = f (pr1 (flip a)) (pr2 b) : {symm (flip_pr1 a)} - ... = f (pr1 (flip a)) (pr1 (flip b)) : {symm (flip_pr1 b)} - ... = pr1 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr1 f _ _), + ... = f (pr1 (flip a)) (pr2 b) : {(flip_pr1 a)⁻¹} + ... = f (pr1 (flip a)) (pr1 (flip b)) : {(flip_pr1 b)⁻¹} + ... = pr1 (map_pair2 f (flip a) (flip b)) : (map_pair2_pr1 f _ _)⁻¹, have Hy : pr2 (flip (map_pair2 f a b)) = pr2 (map_pair2 f (flip a) (flip b)), from calc pr2 (flip (map_pair2 f a b)) = pr1 (map_pair2 f a b) : flip_pr2 _ ... = f (pr1 a) (pr1 b) : map_pair2_pr1 f a b - ... = f (pr2 (flip a)) (pr1 b) : {symm (flip_pr2 a)} - ... = f (pr2 (flip a)) (pr2 (flip b)) : {symm (flip_pr2 b)} - ... = pr2 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr2 f _ _), + ... = f (pr2 (flip a)) (pr1 b) : {flip_pr2 a} + ... = f (pr2 (flip a)) (pr2 (flip b)) : {flip_pr2 b} + ... = pr2 (map_pair2 f (flip a) (flip b)) : (map_pair2_pr2 f _ _)⁻¹, pair_eq Hx Hy -- add_rewrite flip_pr1 flip_pr2 flip_pair @@ -107,12 +107,12 @@ have Hx : pr1 (map_pair2 f v w) = pr1 (map_pair2 f w v), from calc pr1 (map_pair2 f v w) = f (pr1 v) (pr1 w) : map_pair2_pr1 f v w ... = f (pr1 w) (pr1 v) : Hcomm _ _ - ... = pr1 (map_pair2 f w v) : symm (map_pair2_pr1 f w v), + ... = pr1 (map_pair2 f w v) : (map_pair2_pr1 f w v)⁻¹, have Hy : pr2 (map_pair2 f v w) = pr2 (map_pair2 f w v), from calc pr2 (map_pair2 f v w) = f (pr2 v) (pr2 w) : map_pair2_pr2 f v w ... = f (pr2 w) (pr2 v) : Hcomm _ _ - ... = pr2 (map_pair2 f w v) : symm (map_pair2_pr2 f w v), + ... = pr2 (map_pair2 f w v) : (map_pair2_pr2 f w v)⁻¹, pair_eq Hx Hy theorem map_pair2_assoc {A : Type} {f : A → A → A} @@ -125,8 +125,8 @@ have Hx : pr1 (map_pair2 f (map_pair2 f u v) w) = = f (pr1 (map_pair2 f u v)) (pr1 w) : map_pair2_pr1 f _ _ ... = f (f (pr1 u) (pr1 v)) (pr1 w) : {map_pair2_pr1 f _ _} ... = f (pr1 u) (f (pr1 v) (pr1 w)) : Hassoc (pr1 u) (pr1 v) (pr1 w) - ... = f (pr1 u) (pr1 (map_pair2 f v w)) : {symm (map_pair2_pr1 f _ _)} - ... = pr1 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr1 f _ _), + ... = f (pr1 u) (pr1 (map_pair2 f v w)) : {(map_pair2_pr1 f _ _)⁻¹} + ... = pr1 (map_pair2 f u (map_pair2 f v w)) : (map_pair2_pr1 f _ _)⁻¹, have Hy : pr2 (map_pair2 f (map_pair2 f u v) w) = pr2 (map_pair2 f u (map_pair2 f v w)), from calc @@ -134,8 +134,8 @@ have Hy : pr2 (map_pair2 f (map_pair2 f u v) w) = = f (pr2 (map_pair2 f u v)) (pr2 w) : map_pair2_pr2 f _ _ ... = f (f (pr2 u) (pr2 v)) (pr2 w) : {map_pair2_pr2 f _ _} ... = f (pr2 u) (f (pr2 v) (pr2 w)) : Hassoc (pr2 u) (pr2 v) (pr2 w) - ... = f (pr2 u) (pr2 (map_pair2 f v w)) : {symm (map_pair2_pr2 f _ _)} - ... = pr2 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr2 f _ _), + ... = f (pr2 u) (pr2 (map_pair2 f v w)) : {map_pair2_pr2 f _ _} + ... = pr2 (map_pair2 f u (map_pair2 f v w)) : (map_pair2_pr2 f _ _)⁻¹, pair_eq Hx Hy theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a : A, f a e = a) diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean index 4a705f3155..7adc991def 100644 --- a/library/data/quotient/basic.lean +++ b/library/data/quotient/basic.lean @@ -79,13 +79,13 @@ iff_elim_right (R_iff Q r s) (and.intro (H1 r) (and.intro (H1 s) H2)) theorem rep_eq {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {a b : B} (H : R (rep a) (rep b)) : a = b := calc - a = abs (rep a) : symm (abs_rep Q a) + a = abs (rep a) : eq.symm (abs_rep Q a) ... = abs (rep b) : {eq_abs Q H} ... = b : abs_rep Q b theorem R_rep_abs {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {a : A} (H : R a a) : R a (rep (abs a)) := -have H3 : abs a = abs (rep (abs a)), from symm (abs_rep Q (abs a)), +have H3 : abs a = abs (rep (abs a)), from eq.symm (abs_rep Q (abs a)), R_intro Q H (refl_rep Q (abs a)) H3 theorem quotient_imp_symm {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} @@ -94,7 +94,7 @@ take a b : A, assume H : R a b, have Ha : R a a, from refl_left Q H, have Hb : R b b, from refl_right Q H, -have Hab : abs b = abs a, from symm (eq_abs Q H), +have Hab : abs b = abs a, from eq.symm (eq_abs Q H), R_intro Q Hb Ha Hab theorem quotient_imp_trans {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} @@ -104,7 +104,7 @@ assume Hab : R a b, assume Hbc : R b c, have Ha : R a a, from refl_left Q Hab, have Hc : R c c, from refl_right Q Hbc, -have Hac : abs a = abs c, from trans (eq_abs Q Hab) (eq_abs Q Hbc), +have Hac : abs a = abs c, from eq.trans (eq_abs Q Hab) (eq_abs Q Hbc), R_intro Q Ha Hc Hac @@ -124,9 +124,9 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} have H2 [fact] : R a (rep (abs a)), from R_rep_abs Q Ha, calc rec Q f (abs a) = eq.rec_on _ (f (rep (abs a))) : rfl - ... = eq.rec_on _ (eq.rec_on _ (f a)) : {symm (H _ _ H2)} + ... = eq.rec_on _ (eq.rec_on _ (f a)) : {(H _ _ H2)⁻¹} ... = eq.rec_on _ (f a) : eq.rec_on_compose (eq_abs Q H2) _ _ - ... = f a : eq.rec_on_id (trans (eq_abs Q H2) (abs_rep Q (abs a))) _ + ... = f a : eq.rec_on_id (eq.trans (eq_abs Q H2) (abs_rep Q (abs a))) _ definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C := @@ -139,7 +139,7 @@ theorem comp_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : have H2 : R a (rep (abs a)), from R_rep_abs Q Ha, calc rec_constant Q f (abs a) = f (rep (abs a)) : rfl - ... = f a : {symm (H _ _ H2)} + ... = f a : {(H _ _ H2)⁻¹} definition rec_binary {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : Type} (f : A → A → C) (b c : B) : C := @@ -153,7 +153,7 @@ have H2 : R a (rep (abs a)), from R_rep_abs Q Ha, have H3 : R b (rep (abs b)), from R_rep_abs Q Hb, calc rec_binary Q f (abs a) (abs b) = f (rep (abs a)) (rep (abs b)) : rfl - ... = f a b : {symm (H _ _ _ _ H2 H3)} + ... = f a b : {(H _ _ _ _ H2 H3)⁻¹} theorem comp_binary_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) (Hrefl : reflexive R) {C : Type} {f : A → A → C} @@ -172,7 +172,7 @@ theorem comp_quotient_map {A B : Type} {R : A → A → Prop} {abs : A → B} {r have H2 : R a (rep (abs a)), from R_rep_abs Q Ha, have H3 : R (f a) (f (rep (abs a))), from H _ _ H2, have H4 : abs (f a) = abs (f (rep (abs a))), from eq_abs Q H3, -symm H4 +H4⁻¹ definition quotient_map_binary {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) (f : A → A → A) (b c : B) : B := @@ -185,7 +185,7 @@ theorem comp_quotient_map_binary {A B : Type} {R : A → A → Prop} {abs : A have Ha2 : R a (rep (abs a)), from R_rep_abs Q Ha, have Hb2 : R b (rep (abs b)), from R_rep_abs Q Hb, have H2 : R (f a b) (f (rep (abs a)) (rep (abs b))), from H _ _ _ _ Ha2 Hb2, -symm (eq_abs Q H2) +(eq_abs Q H2)⁻¹ theorem comp_quotient_map_binary_refl {A B : Type} {R : A → A → Prop} (Hrefl : reflexive R) {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {f : A → A → A} @@ -231,18 +231,20 @@ theorem image_tag {A B : Type} {f : A → B} (u : image f) : ∃a H, tag (f a) H obtain a (H : fun_image f a = u), from fun_image_surj u, exists_intro a (exists_intro (exists_intro a rfl) H) +open eq_ops + theorem fun_image_eq {A B : Type} (f : A → B) (a a' : A) : (f a = f a') ↔ (fun_image f a = fun_image f a') := iff_intro (assume H : f a = f a', tag_eq H) (assume H : fun_image f a = fun_image f a', - subst (subst (congr_arg elt_of H) (elt_of_fun_image f a)) (elt_of_fun_image f a')) + (congr_arg elt_of H ▸ elt_of_fun_image f a) ▸ elt_of_fun_image f a') theorem idempotent_image_elt_of {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) (u : image f) : fun_image f (elt_of u) = u := obtain (a : A) (Ha : fun_image f a = u), from fun_image_surj u, calc - fun_image f (elt_of u) = fun_image f (elt_of (fun_image f a)) : {symm Ha} + fun_image f (elt_of u) = fun_image f (elt_of (fun_image f a)) : {Ha⁻¹} ... = fun_image f (f a) : {elt_of_fun_image f a} ... = fun_image f a : {iff_elim_left (fun_image_eq f (f a) a) (H a)} ... = u : Ha @@ -251,7 +253,7 @@ theorem idempotent_image_fix {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) : f (elt_of u) = elt_of u := obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u, calc - f (elt_of u) = f (f a) : {symm Ha} + f (elt_of u) = f (f a) : {Ha⁻¹} ... = f a : H a ... = elt_of u : Ha @@ -262,17 +264,17 @@ calc theorem representative_map_idempotent {A : Type} {R : A → A → Prop} {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) : f (f a) = f a := -symm (and.elim_right (and.elim_right (iff_elim_left (H2 a (f a)) (H1 a)))) +(and.elim_right (and.elim_right (iff_elim_left (H2 a (f a)) (H1 a))))⁻¹ theorem representative_map_idempotent_equiv {A : Type} {R : A → A → Prop} {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) (a : A) : f (f a) = f a := -symm (H2 a (f a) (H1 a)) +(H2 a (f a) (H1 a))⁻¹ theorem representative_map_refl_rep {A : Type} {R : A → A → Prop} {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) : R (f a) (f a) := -subst (representative_map_idempotent H1 H2 a) (H1 (f a)) +representative_map_idempotent H1 H2 a ▸ H1 (f a) theorem representative_map_image_fix {A : Type} {R : A → A → Prop} {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') (b : image f) : @@ -289,14 +291,14 @@ intro have H : elt_of (abs (elt_of u)) = elt_of u, from calc elt_of (abs (elt_of u)) = f (elt_of u) : elt_of_fun_image _ _ - ... = f (f a) : {symm Ha} + ... = f (f a) : {Ha⁻¹} ... = f a : representative_map_idempotent H1 H2 a ... = elt_of u : Ha, show abs (elt_of u) = u, from subtype_eq H) (take u : image f, show R (elt_of u) (elt_of u), from obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u, - subst Ha (@representative_map_refl_rep A R f H1 H2 a)) + Ha ▸ (@representative_map_refl_rep A R f H1 H2 a)) (take a a', subst (fun_image_eq f a a') (H2 a a')) @@ -307,7 +309,7 @@ theorem representative_map_equiv_inj {A : Type} {R : A → A → Prop} have symmR : symmetric R, from rel_symm R, have transR : transitive R, from rel_trans R, show R a b, from - have H2 : R a (f b), from subst H3 (H1 a), + have H2 : R a (f b), from H3 ▸ (H1 a), have H3 : R (f b) b, from symmR (H1 b), transR H2 H3 diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 59b92a69bc..3d7b7e0eaa 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -38,7 +38,7 @@ section assume (H2' : eq.rec_on H1' b1 = b2'), show dpair a1 b1 = dpair a1 b2', from calc - dpair a1 b1 = dpair a1 (eq.rec_on H1' b1) : {symm (eq.rec_on_id H1' b1)} + dpair a1 b1 = dpair a1 (eq.rec_on H1' b1) : {eq.symm (eq.rec_on_id H1' b1)} ... = dpair a1 b2' : {H2'}) H1) b2 H1 H2 diff --git a/library/data/subtype.lean b/library/data/subtype.lean index c70977178d..4672fc8479 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -34,7 +34,7 @@ section destruct a (take (x : A) (H1 : P x) (H2 : P x), rfl) theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 := - subst H3 (take H2, tag_irrelevant H1 H2) H2 + eq.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 := destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H)) @@ -45,7 +45,7 @@ section theorem eq_decidable [protected] [instance] (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), + iff_intro (assume H, eq.subst H rfl) (assume H, subtype_eq H), decidable_iff_equiv _ (iff_symm H1) end diff --git a/library/data/sum.lean b/library/data/sum.lean index 35b0c4c4aa..e0b260b5e8 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -9,7 +9,7 @@ import logic.core.prop logic.classes.inhabited logic.classes.decidable -open inhabited decidable +open inhabited decidable eq_ops -- TODO: take this outside the namespace when the inductive package handles it better inductive sum (A B : Type) : Type := @@ -40,19 +40,19 @@ rec H1 H2 s theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 := let f := λs, rec_on s (λa, a1 = a) (λb, false) in have H1 : f (inl B a1), from rfl, -have H2 : f (inl B a2), from subst H H1, +have H2 : f (inl B a2), from H ▸ H1, H2 theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false := let f := λs, rec_on s (λa', a = a') (λb, false) in have H1 : f (inl B a), from rfl, -have H2 : f (inr A b), from subst H H1, +have H2 : f (inr A b), from H ▸ H1, H2 theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 := let f := λs, rec_on s (λa, false) (λb, b1 = b) in have H1 : f (inr A b1), from rfl, -have H2 : f (inr A b2), from subst H H1, +have H2 : f (inr A b2), from H ▸ H1, H2 theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) := @@ -76,7 +76,7 @@ rec_on s1 rec_on s2 (take a2, have H3 : (inr A b1 = inl B a2) ↔ false, - from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim H4), + from iff_intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4), show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3)) (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2)) diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index 16f9dcc1c6..47760a71ff 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.lean @@ -53,4 +53,4 @@ theorem iff_congruence [instance] (P : Prop → Prop) : congruence iff iff P := congruence.mk (take (a b : Prop), assume H : a ↔ b, - show P a ↔ P b, from eq_to_iff (subst (iff_to_eq H) (eq.refl (P a)))) + show P a ↔ P b, from eq_to_iff (iff_to_eq H ▸ eq.refl (P a))) diff --git a/library/logic/core/cast.lean b/library/logic/core/cast.lean index a773ad0f79..d08c87cfc3 100644 --- a/library/logic/core/cast.lean +++ b/library/logic/core/cast.lean @@ -54,7 +54,7 @@ theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Prop} (H1 have Haux1 : ∀ H : A = A, P A (cast H a), from assume H : A = A, (cast_eq H a)⁻¹ ▸ H2, obtain (Heq : A = B) (Hw : cast Heq a = b), from H1, -have Haux2 : P B (cast Heq a), from subst Heq Haux1 Heq, +have Haux2 : P B (cast Heq a), from eq.subst Heq Haux1 Heq, Hw ▸ Haux2 theorem hsymm {A B : Type} {a : A} {b : B} (H : a == b) : b == a := @@ -79,7 +79,7 @@ hsubst H (eq.refl A) theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a := have H1 : ∀ (H : A = A) (a : A), cast H a == a, from assume H a, eq_to_heq (cast_eq H a), -subst H H1 H a +eq.subst H H1 H a theorem cast_eq_to_heq {A B : Type} {a : A} {b : B} {H : A = B} (H1 : cast H a = b) : a == b := calc a == cast H a : hsymm (cast_heq H a) @@ -95,20 +95,20 @@ theorem dcongr_arg {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = have e1 : ∀ (H : B a = B a), cast H (f a) = f a, from assume H, cast_eq H (f a), have e2 : ∀ (H : B a = B b), cast H (f a) = f b, from - subst H e1, + H ▸ e1, have e3 : cast (congr_arg B H) (f a) = f b, from e2 (congr_arg B H), cast_eq_to_heq e3 theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) := -subst H (eq.refl (Π x, B x)) +H ▸ (eq.refl (Π x, B x)) theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) : cast (pi_eq H) f a == f a := have H1 : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from assume H, eq_to_heq (congr_fun (cast_eq H f) a), have H2 : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from - subst H H1, + H ▸ H1, H2 (pi_eq H) theorem cast_pull {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) : diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean index 5b45bdd561..11911955cf 100644 --- a/library/logic/core/connectives.lean +++ b/library/logic/core/connectives.lean @@ -144,9 +144,10 @@ iff_mp (iff_symm H) trivial theorem iff_false_elim {a : Prop} (H : a ↔ false) : ¬a := assume Ha : a, iff_mp H Ha -theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b := -iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb) +open eq_ops +theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b := +iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) -- comm and assoc for and / or -- --------------------------- diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean index 20690eb221..3faec157c1 100644 --- a/library/logic/core/eq.lean +++ b/library/logic/core/eq.lean @@ -18,34 +18,34 @@ refl : eq a a infix `=` := eq notation `rfl` := eq.refl _ -theorem eq_id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) := rfl +namespace eq +theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) := +rfl -theorem eq_irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 := rfl +theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 := +rfl theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b := -eq.rec H2 H1 +rec H2 H1 theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H2 H1 -calc_subst subst -calc_refl eq.refl -calc_trans trans - theorem symm {A : Type} {a b : A} (H : a = b) : b = a := -subst H (eq.refl a) +subst H (refl a) +end eq + +calc_subst eq.subst +calc_refl eq.refl +calc_trans eq.trans namespace eq_ops - postfix `⁻¹` := symm - infixr `⬝` := trans - infixr `▸` := subst + postfix `⁻¹` := eq.symm + infixr `⬝` := eq.trans + infixr `▸` := eq.subst end eq_ops open eq_ops -theorem true_ne_false : ¬true = false := -assume H : true = false, - subst H trivial - namespace eq -- eq_rec with arguments swapped, for transporting an element of a dependent type definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 := @@ -78,9 +78,6 @@ H1 ▸ H2 ▸ eq.refl (f a) theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x := take x, congr_fun H x -theorem not_congr {a b : Prop} (H : a = b) : (¬a) = (¬b) := -congr_arg not H - theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b := H1 ▸ H2 @@ -102,23 +99,28 @@ 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) - -- ne -- -- definition ne [inline] {A : Type} (a b : A) := ¬(a = b) infix `≠` := ne -theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := H +namespace ne +theorem intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := +H -theorem ne_elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false := H1 H2 +theorem elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false := +H1 H2 -theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := H rfl +theorem irrefl {A : Type} {a : A} (H : a ≠ a) : false := +H rfl -theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H rfl - -theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a := +theorem symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a := assume H1 : b = a, H (H1⁻¹) +end ne + +theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := +H rfl theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := H1⁻¹ ▸ H2 @@ -134,3 +136,7 @@ assume Heq : p = false, Heq ▸ Hp theorem p_ne_true {p : Prop} (Hnp : ¬p) : p ≠ true := assume Heq : p = true, absurd trivial (Heq ▸ Hnp) + +theorem true_ne_false : ¬true = false := +assume H : true = false, + H ▸ trivial diff --git a/library/logic/core/examples/instances_test.lean b/library/logic/core/examples/instances_test.lean index a41e99b30f..6be183692c 100644 --- a/library/logic/core/examples/instances_test.lean +++ b/library/logic/core/examples/instances_test.lean @@ -40,9 +40,8 @@ theorem test6 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a H1 ⬝ (H2⁻¹ ⬝ H3) theorem test7 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d := -trans H1 (trans (symm H2) H3) +H1 ⬝ H2⁻¹ ⬝ H3 theorem test8 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d := -trans H1 (trans (symm H2) H3) - +H1 ⬝ H2⁻¹ ⬝ H3 end diff --git a/library/logic/core/instances.lean b/library/logic/core/instances.lean index ff32e8c420..f027bdf393 100644 --- a/library/logic/core/instances.lean +++ b/library/logic/core/instances.lean @@ -80,10 +80,10 @@ theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive (@eq T) := relation.is_reflexive.mk (@eq.refl T) theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric (@eq T) := -relation.is_symmetric.mk (@symm T) +relation.is_symmetric.mk (@eq.symm T) theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive (@eq T) := -relation.is_transitive.mk (@trans T) +relation.is_transitive.mk (@eq.trans T) -- TODO: this is only temporary, needed to inform Lean that is_equivalence is a class theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) := diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean index bcaec8ce6c..858989c3fa 100644 --- a/tests/lean/have1.lean +++ b/tests/lean/have1.lean @@ -1,5 +1,5 @@ import logic -open bool eq_ops tactic +open bool eq_ops tactic eq variables a b c : bool axiom H1 : a = b diff --git a/tests/lean/run/bug5.lean b/tests/lean/run/bug5.lean index 76307d1737..a38fdde426 100644 --- a/tests/lean/run/bug5.lean +++ b/tests/lean/run/bug5.lean @@ -1,4 +1,4 @@ import logic theorem symm2 {A : Type} {a b : A} (H : a = b) : b = a -:= subst H (eq.refl a) +:= eq.subst H (eq.refl a) diff --git a/tests/lean/run/bug6.lean b/tests/lean/run/bug6.lean index 9e76e438b3..73943ac540 100644 --- a/tests/lean/run/bug6.lean +++ b/tests/lean/run/bug6.lean @@ -1,4 +1,5 @@ import logic +open eq section parameter {A : Type} theorem T {a b : A} (H : a = b) : b = a diff --git a/tests/lean/run/choice_ctx.lean b/tests/lean/run/choice_ctx.lean index 479d9110d5..e3f5242940 100644 --- a/tests/lean/run/choice_ctx.lean +++ b/tests/lean/run/choice_ctx.lean @@ -1,6 +1,6 @@ import data.nat.basic open nat - +open eq set_option pp.coercion true namespace foo diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index 66984cc80b..e65640b49f 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -4,7 +4,7 @@ inductive nat : Type := zero : nat, succ : nat → nat -abbreviation refl := @eq.refl +open eq namespace nat definition add (x y : nat) @@ -38,12 +38,12 @@ theorem is_zero_to_eq (x : nat) (H : is_zero x) : x = zero (assume Hz : x = zero, Hz) (assume Hs : (∃ n, x = succ n), exists_elim Hs (λ (w : nat) (Hw : x = succ w), - absurd H (subst (symm Hw) (not_is_zero_succ w)))) + absurd H (eq.subst (symm Hw) (not_is_zero_succ w)))) theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n := or_elim (dichotomy x) (assume Hz : x = zero, - absurd (subst (symm Hz) is_zero_zero) H) + absurd (eq.subst (symm Hz) is_zero_zero) H) (assume Hs, Hs) theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y) diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean index e0ecee89b0..e4a7484a15 100644 --- a/tests/lean/run/cody1.lean +++ b/tests/lean/run/cody1.lean @@ -20,6 +20,6 @@ notation `δ` := delta. theorem false_aux : ¬ (δ (i delta)) := assume H : δ (i delta), have H' : r (i delta) (i delta), - from eq.rec H (symm retract), + from eq.rec H (eq.symm retract), H H'. end diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean index 5b0ba77470..557290cfe7 100644 --- a/tests/lean/run/cody2.lean +++ b/tests/lean/run/cody2.lean @@ -1,5 +1,5 @@ import logic - +open eq abbreviation subsets (P : Type) := P → Prop. section @@ -22,4 +22,4 @@ theorem delta_aux : ¬ (δ (i delta)) check delta_aux. -end \ No newline at end of file +end diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean index 7d6e6220b7..8f40722304 100644 --- a/tests/lean/run/elab_bug1.lean +++ b/tests/lean/run/elab_bug1.lean @@ -5,7 +5,7 @@ ---------------------------------------------------------------------------------------------------- import logic struc.function - +open eq open function namespace congruence diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean index f7fe6c1399..2c7bbb7869 100644 --- a/tests/lean/run/matrix.lean +++ b/tests/lean/run/matrix.lean @@ -6,7 +6,7 @@ variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add A m1 m2 H1 = @add A m1 m2 H2 := rfl - +open eq theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' := subst H1 (subst H2 H) diff --git a/tests/lean/run/matrix2.lean b/tests/lean/run/matrix2.lean index b6a8f2842a..a5c767b2dc 100644 --- a/tests/lean/run/matrix2.lean +++ b/tests/lean/run/matrix2.lean @@ -3,7 +3,7 @@ import logic variable matrix.{l} : Type.{l} → Type.{l} variable same_dim {A : Type} : matrix A → matrix A → Prop variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A - +open eq theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' := subst H1 (subst H2 H) diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean index ce758d21c4..26f83232cc 100644 --- a/tests/lean/run/nat_bug.lean +++ b/tests/lean/run/nat_bug.lean @@ -1,5 +1,6 @@ import logic open decidable +open eq inductive nat : Type := zero : nat, diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean index 32fe496230..fd7de826c6 100644 --- a/tests/lean/run/nat_bug4.lean +++ b/tests/lean/run/nat_bug4.lean @@ -11,7 +11,7 @@ definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m infixl `*`:75 := mul axiom mul_succ_right (n m : nat) : n * succ m = n * m + n - +open eq theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m := subst (mul_succ_right _ _) (eq.refl (n * succ l + m)) end nat diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean index f374cc10b5..1b9e0aa14b 100644 --- a/tests/lean/run/nat_bug5.lean +++ b/tests/lean/run/nat_bug5.lean @@ -1,5 +1,5 @@ import logic -open eq_ops +open eq_ops eq inductive nat : Type := zero : nat, diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean index fae9bfa415..5e8bb28db4 100644 --- a/tests/lean/run/nat_bug6.lean +++ b/tests/lean/run/nat_bug6.lean @@ -17,5 +17,5 @@ variable P : nat → Prop print "===========================" theorem tst (n : nat) (H : P (n * zero)) : P zero -:= subst (mul_zero_right _) H +:= eq.subst (mul_zero_right _) H end nat diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean index fddd53e0c0..d90a5f1a24 100644 --- a/tests/lean/run/nat_bug7.lean +++ b/tests/lean/run/nat_bug7.lean @@ -9,7 +9,7 @@ definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y infixl `+`:65 := add axiom add_right_comm (n m k : nat) : n + m + k = n + k + m - +open eq print "===========================" theorem bug (a b c d : nat) : a + b + c + d = a + c + b + d := subst (add_right_comm _ _ _) (eq.refl (a + b + c + d)) diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index 656901fb37..1be746bd82 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -14,4 +14,4 @@ theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (decidable_eq (pr2 (pair x sorry theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) := -trans (gcd_def _ _) (if_neg succ_ne_zero) +eq.trans (gcd_def _ _) (if_neg succ_ne_zero) diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean index 6f752e6d79..b2be19116f 100644 --- a/tests/lean/run/over_subst.lean +++ b/tests/lean/run/over_subst.lean @@ -26,6 +26,6 @@ end int open int open nat - +open eq theorem add_lt_left {a b : int} (H : a < b) (c : int) : c + a < c + b := subst (symm (add_assoc c a one)) (add_le_left H c) diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean index 454cb35650..8dd6c8a2a0 100644 --- a/tests/lean/run/sum_bug.lean +++ b/tests/lean/run/sum_bug.lean @@ -18,7 +18,7 @@ infixr `+`:25 := sum 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 - +open eq theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 := let f := λs, rec_on s (λa, a1 = a) (λb, false) in diff --git a/tests/lean/run/tactic15.lean b/tests/lean/run/tactic15.lean index 956ac914e4..877ee06e56 100644 --- a/tests/lean/run/tactic15.lean +++ b/tests/lean/run/tactic15.lean @@ -3,7 +3,7 @@ open tactic variable A : Type.{1} variable f : A → A → A - +open eq theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a (f b b) = f b (f c c) := by apply (subst H1); trace "trying again... "; diff --git a/tests/lean/run/tactic16.lean b/tests/lean/run/tactic16.lean index d8233ef2f6..3797719dbf 100644 --- a/tests/lean/run/tactic16.lean +++ b/tests/lean/run/tactic16.lean @@ -3,7 +3,7 @@ open tactic variable A : Type.{1} variable f : A → A → A - +open eq theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a (f b b) = f b (f c c) := by discard (apply (subst H1)) 3; -- discard the first 3 solutions produced by apply trace "after subst H1"; diff --git a/tests/lean/run/tactic18.lean b/tests/lean/run/tactic18.lean index 13a8772610..12fbe08cf4 100644 --- a/tests/lean/run/tactic18.lean +++ b/tests/lean/run/tactic18.lean @@ -6,6 +6,6 @@ variable f : A → A → A theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c := by apply (@congr A A); - apply (subst H2); + apply (eq.subst H2); apply eq.refl; assumption diff --git a/tests/lean/run/tactic19.lean b/tests/lean/run/tactic19.lean index e4384b68cd..9ca23e9d9d 100644 --- a/tests/lean/run/tactic19.lean +++ b/tests/lean/run/tactic19.lean @@ -3,6 +3,6 @@ open tactic theorem tst {A : Type} {f : A → A → A} {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c := by apply congr; - apply (subst H2); + apply (eq.subst H2); apply eq.refl; assumption diff --git a/tests/lean/run/tactic20.lean b/tests/lean/run/tactic20.lean index 8411865397..9f7e5ac0a9 100644 --- a/tests/lean/run/tactic20.lean +++ b/tests/lean/run/tactic20.lean @@ -4,4 +4,4 @@ open tactic definition assump := eassumption theorem tst {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c -:= by apply trans; assump; assump +:= by apply eq.trans; assump; assump diff --git a/tests/lean/run/trans.lean b/tests/lean/run/trans.lean index 86dd0b2014..9666b17687 100644 --- a/tests/lean/run/trans.lean +++ b/tests/lean/run/trans.lean @@ -2,7 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura import logic - +open eq abbreviation refl := @eq.refl definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean index fe3147b2f7..e0688bcf8f 100644 --- a/tests/lean/show1.lean +++ b/tests/lean/show1.lean @@ -8,7 +8,7 @@ axiom H2 : b = c check show a = c, from H1 ⬝ H2 print "------------" check have e1 [fact] : a = b, from H1, - have e2 : a = c, by apply trans; apply e1; apply H2, + have e2 : a = c, by apply eq.trans; apply e1; apply H2, have e3 : c = a, from e2⁻¹, have e4 [fact] : b = a, from e1⁻¹, show b = c, from e1⁻¹ ⬝ e2 diff --git a/tests/lean/show1.lean.expected.out b/tests/lean/show1.lean.expected.out index 8072899486..d136ca2716 100644 --- a/tests/lean/show1.lean.expected.out +++ b/tests/lean/show1.lean.expected.out @@ -1,8 +1,8 @@ -show eq a c, from trans H1 H2 : eq a c +show eq a c, from eq.trans H1 H2 : eq a c ------------ have e1 [fact] : eq a b, from H1, -have e2 : eq a c, from trans e1 H2, -have e3 : eq c a, from symm e2, -have e4 [fact] : eq b a, from symm e1, -show eq b c, from trans (symm e1) e2 : +have e2 : eq a c, from eq.trans e1 H2, +have e3 : eq c a, from eq.symm e2, +have e4 [fact] : eq b a, from eq.symm e1, +show eq b c, from eq.trans (eq.symm e1) e2 : eq b c diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean index 2be0119311..6a77b4758a 100644 --- a/tests/lean/slow/list_elab2.lean +++ b/tests/lean/slow/list_elab2.lean @@ -14,7 +14,7 @@ import logic data.nat open nat -- open congr -open eq_ops +open eq_ops eq inductive list (T : Type) : Type := nil {} : list T, diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean index a40f5bc6a1..325afacc7c 100644 --- a/tests/lean/slow/nat_bug2.lean +++ b/tests/lean/slow/nat_bug2.lean @@ -4,7 +4,7 @@ -- Author: Floris van Doorn ---------------------------------------------------------------------------------------------------- import logic struc.binary -open tactic binary eq_ops +open tactic binary eq_ops eq open decidable abbreviation refl := @eq.refl @@ -98,7 +98,7 @@ theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) (λ m iH, inr (succ_ne_zero m))) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), take n, rec_on n - (inr (ne_symm (succ_ne_zero m'))) + (inr (ne.symm (succ_ne_zero m'))) (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), have d1 : decidable (n' = m'), from iH1 n', decidable.rec_on d1 @@ -960,7 +960,7 @@ theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k n * m = n * 0 : H ... = 0 : mul_zero_right n, have H3 : n = 0 ∨ m = 0, from mul_eq_zero H2, - resolve_right H3 (ne_symm (lt_ne Hn))) + resolve_right H3 (ne.symm (lt_ne Hn))) (take (l : ℕ), assume (IH : ∀ m, n * m = n * l → m = l), take (m : ℕ), diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 8d2fb35f5d..ac81534283 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -4,7 +4,7 @@ -- Author: Floris van Doorn ---------------------------------------------------------------------------------------------------- import logic struc.binary -open tactic binary eq_ops +open tactic binary eq_ops eq open decidable inductive nat : Type := @@ -93,7 +93,7 @@ theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) (λ m iH, inr (succ_ne_zero m))) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), take n, rec_on n - (inr (ne_symm (succ_ne_zero m'))) + (inr (ne.symm (succ_ne_zero m'))) (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), have d1 : decidable (n' = m'), from iH1 n', decidable.rec_on d1 @@ -965,7 +965,7 @@ theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k n * m = n * 0 : H ... = 0 : mul_zero_right n, have H3 : n = 0 ∨ m = 0, from mul_eq_zero H2, - resolve_right H3 (ne_symm (lt_ne Hn))) + resolve_right H3 (ne.symm (lt_ne Hn))) (take (l : ℕ), assume (IH : ∀ m, n * m = n * l → m = l), take (m : ℕ),