michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library): add 'eq' and 'ne' namespaces

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-04 18:41:06 -07:00
parent 2bc6f92d33
commit 68d9bef860
52 changed files with 315 additions and 307 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/lean/calc.org
View file

@ -17,7 +17,7 @@ Each =<proof>_i= is a proof for =<expr>_{i-1} op_i <expr>_i=.
Recall that proofs are also expressions in Lean. The =<proof>_i=
may also be of the form ={ <pr> }=, where =<pr>= is a proof
for some equality =a = b=. The form ={ <pr> }= is just syntax sugar
for =subst <pr> (refl <expr>_{i-1})=
for =eq.subst <pr> (refl <expr>_{i-1})=
That is, we are claiming we can obtain =<expr>_i= by replacing =a= with =b=
in =<expr>_{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

46
doc/lean/tutorial.org
View file

@ -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

4
library/data/bool.lean
View file

@ -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

94
library/data/int/basic.lean
View file

@ -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

144
library/data/int/order.lean
View file

@ -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'),

4
library/data/list/basic.lean
View file

@ -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

8
library/data/nat/basic.lean
View file

@ -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

58
library/data/nat/div.lean
View file

@ -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

6
library/data/nat/order.lean
View file

@ -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

4
library/data/nat/sub.lean
View file

@ -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) :=

2
library/data/option.lean
View file

@ -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))))

6
library/data/prod.lean
View file

@ -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)

26
library/data/quotient/aux.lean
View file

@ -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)

40
library/data/quotient/basic.lean
View file

@ -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

2
library/data/sigma.lean
View file

@ -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

4
library/data/subtype.lean
View file

@ -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

10
library/data/sum.lean
View file

@ -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))

2
library/logic/axioms/classical.lean
View file

@ -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)))

10
library/logic/core/cast.lean
View file

@ -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) :

5
library/logic/core/connectives.lean
View file

@ -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
-- ---------------------------

56
library/logic/core/eq.lean
View file

@ -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

5
library/logic/core/examples/instances_test.lean
View file

@ -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

4
library/logic/core/instances.lean
View file

@ -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) :=

2
tests/lean/have1.lean
View file

@ -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

2
tests/lean/run/bug5.lean
View file

@ -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)

1
tests/lean/run/bug6.lean
View file

@ -1,4 +1,5 @@
import logic
open eq
section
parameter {A : Type}
theorem T {a b : A} (H : a = b) : b = a

2
tests/lean/run/choice_ctx.lean
View file

@ -1,6 +1,6 @@
import data.nat.basic
open nat
open eq
set_option pp.coercion true
namespace foo

6
tests/lean/run/class4.lean
View file

@ -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)

2
tests/lean/run/cody1.lean
View file

@ -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

4
tests/lean/run/cody2.lean
View file

@ -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
end

2
tests/lean/run/elab_bug1.lean
View file

@ -5,7 +5,7 @@
----------------------------------------------------------------------------------------------------
import logic struc.function
open eq
open function
namespace congruence

2
tests/lean/run/matrix.lean
View file

@ -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)

2
tests/lean/run/matrix2.lean
View file

@ -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)

1
tests/lean/run/nat_bug.lean
View file

@ -1,5 +1,6 @@
import logic
open decidable
open eq
inductive nat : Type :=
zero : nat,

2
tests/lean/run/nat_bug4.lean
View file

@ -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

2
tests/lean/run/nat_bug5.lean
View file

@ -1,5 +1,5 @@
import logic
open eq_ops
open eq_ops eq
inductive nat : Type :=
zero : nat,

2
tests/lean/run/nat_bug6.lean
View file

@ -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

2
tests/lean/run/nat_bug7.lean
View file

@ -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))

2
tests/lean/run/occurs_check_bug1.lean
View file

@ -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)

2
tests/lean/run/over_subst.lean
View file

@ -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)

2
tests/lean/run/sum_bug.lean
View file

@ -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

2
tests/lean/run/tactic15.lean
View file

@ -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... ";

2
tests/lean/run/tactic16.lean
View file

@ -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";

2
tests/lean/run/tactic18.lean
View file

@ -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

2
tests/lean/run/tactic19.lean
View file

@ -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

2
tests/lean/run/tactic20.lean
View file

@ -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

2
tests/lean/run/trans.lean
View file

@ -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

2
tests/lean/show1.lean
View file

@ -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

10
tests/lean/show1.lean.expected.out
View file

@ -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

2
tests/lean/slow/list_elab2.lean
View file

@ -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,

6
tests/lean/slow/nat_bug2.lean
View file

@ -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 : ℕ),

6
tests/lean/slow/nat_wo_hints.lean
View file

@ -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 : ℕ),