max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library): remove eq.ops namespace

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-31 12:50:11 -07:00
parent 1aeda0e74b
commit f461b53a7f
43 changed files with 121 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/binary.lean
View file

@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
General properties of binary operations.
-/
open eq.ops function
open function
namespace binary
section

4
library/algebra/field.lean
View file

@ -7,7 +7,7 @@ Structures with multiplicative and additive components, including division rings
The development is modeled after Isabelle's library.
-/
import algebra.ring
open eq eq.ops
open eq
variable {A : Type}
@ -386,7 +386,7 @@ section discrete_field
sorry -- by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]
theorem ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H
assume Ha : a = 0, absurd (symm Ha ▸ one_div_zero) H
theorem eq_zero_of_one_div_eq_zero (H : 1 / a = 0) : a = 0 :=
decidable.by_cases

4
library/algebra/monotone.lean
View file

@ -9,7 +9,7 @@ TODO: we will probably eventually want versions restricted to smaller domains,
"nondecreasing_on" etc. Maybe we can do this with subtypes.
-/
import .order
open eq eq.ops function
open eq function
variables {A B C : Type}
@ -82,7 +82,7 @@ section
take a₁ a₂, suppose a₁ ≤ a₂,
show f a₁ ≥ f a₂, from or.elim (lt_or_eq_of_le this)
(suppose a₁ < a₂, le_of_lt (H this))
(suppose a₁ = a₂, le_of_eq (congr_arg f this⁻¹))
(suppose a₁ = a₂, le_of_eq (congr_arg f (symm this)))
end
section

10
library/algebra/order.lean
View file

@ -6,7 +6,7 @@ Author: Jeremy Avigad
Weak orders "≤", strict orders "<", and structures that include both.
-/
import logic.eq logic.connectives algebra.binary algebra.priority
open eq eq.ops function
open eq function
variables {A : Type}
@ -171,7 +171,7 @@ section strong_order_pair
have le_ac : a ≤ c, from le.trans (le_of_lt' _ _ lt_ab) le_bc,
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have le_ba : b ≤ a, from symm eq_ac ▸ le_bc,
have eq_ab : a = b, from le.antisymm (le_of_lt' _ _ lt_ab) le_ba,
show false, from ne_of_lt' lt_ab eq_ab,
show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
@ -218,7 +218,7 @@ section
(assume H : b ≤ a,
or.elim (iff.mp le_iff_lt_or_eq H)
(assume H1, or.inr (or.inr H1))
(assume H1, or.inr (or.inl (H1⁻¹))))
(assume H1, or.inr (or.inl (symm H1))))
theorem lt.by_cases {a b : A} {P : Prop}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
@ -305,11 +305,11 @@ section
theorem lt.cases_of_lt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a < b) :
lt.cases a b t_lt t_eq t_gt = t_lt :=
if_neg (ne_of_lt H) ⬝ if_pos H
trans (if_neg (ne_of_lt H)) (if_pos H)
theorem lt.cases_of_gt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a > b) :
lt.cases a b t_lt t_eq t_gt = t_gt :=
if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H)
trans (if_neg (ne.symm (ne_of_lt H))) (if_neg (lt.asymm H))
definition min (a b : A) : A := if a ≤ b then a else b
definition max (a b : A) : A := if a ≤ b then b else a

6
library/algebra/ordered_field.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Lewis
-/
import algebra.ordered_ring algebra.field
open eq eq.ops
open eq
structure linear_ordered_field [class] (A : Type) extends linear_ordered_ring A, field A
@ -476,14 +476,14 @@ section discrete_linear_ordered_field
have H1 : 0 < 1 / (1 / a), from one_div_pos_of_pos H,
have H2 : 1 / a ≠ 0, from
(assume H3 : 1 / a = 0,
have H4 : 1 / (1 / a) = 0, from H3⁻¹ ▸ div_zero 1,
have H4 : 1 / (1 / a) = 0, from symm H3 ▸ div_zero 1,
absurd H4 (ne.symm (ne_of_lt H1))),
(division_ring.one_div_one_div (ne_zero_of_one_div_ne_zero H2)) ▸ H1
theorem neg_of_one_div_neg (H : 1 / a < 0) : a < 0 :=
have H1 : 0 < - (1 / a), from neg_pos_of_neg H,
have Ha : a ≠ 0, from ne_zero_of_one_div_ne_zero (ne_of_lt H),
have H2 : 0 < 1 / (-a), from (division_ring.one_div_neg_eq_neg_one_div Ha)⁻¹ ▸ H1,
have H2 : 0 < 1 / (-a), from symm (division_ring.one_div_neg_eq_neg_one_div Ha) ▸ H1,
have H3 : 0 < -a, from pos_of_one_div_pos H2,
neg_of_neg_pos H3

18
library/algebra/ordered_group.lean
View file

@ -7,7 +7,7 @@ Partially ordered additive groups, modeled on Isabelle's library. These classes
if necessary.
-/
import algebra.group algebra.order algebra.monotone
open eq eq.ops -- note: ⁻¹ will be overloaded
open eq
variables {A B : Type}
@ -297,7 +297,7 @@ section
iff.intro le_of_neg_le_neg neg_le_neg
theorem nonneg_of_neg_nonpos {a : A} (H : -a ≤ 0) : 0 ≤ a :=
le_of_neg_le_neg (neg_zero⁻¹ ▸ H)
le_of_neg_le_neg (symm neg_zero ▸ H)
theorem neg_nonpos_of_nonneg {a : A} (H : 0 ≤ a) : -a ≤ 0 :=
neg_zero ▸ neg_le_neg H
@ -306,7 +306,7 @@ section
iff.intro nonneg_of_neg_nonpos neg_nonpos_of_nonneg
theorem nonpos_of_neg_nonneg {a : A} (H : 0 ≤ -a) : a ≤ 0 :=
le_of_neg_le_neg (neg_zero⁻¹ ▸ H)
le_of_neg_le_neg (symm neg_zero ▸ H)
theorem neg_nonneg_of_nonpos {a : A} (H : a ≤ 0) : 0 ≤ -a :=
neg_zero ▸ neg_le_neg H
@ -325,7 +325,7 @@ section
iff.intro lt_of_neg_lt_neg neg_lt_neg
theorem pos_of_neg_neg {a : A} (H : -a < 0) : 0 < a :=
lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H)
lt_of_neg_lt_neg (symm neg_zero ▸ H)
theorem neg_neg_of_pos {a : A} (H : 0 < a) : -a < 0 :=
neg_zero ▸ neg_lt_neg H
@ -334,7 +334,7 @@ section
iff.intro pos_of_neg_neg neg_neg_of_pos
theorem neg_of_neg_pos {a : A} (H : 0 < -a) : a < 0 :=
lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H)
lt_of_neg_lt_neg (symm neg_zero ▸ H)
theorem neg_pos_of_neg {a : A} (H : a < 0) : 0 < -a :=
neg_zero ▸ neg_lt_neg H
@ -852,7 +852,7 @@ section
sorry -- by rewrite [-neg_sub, abs_neg]
theorem ne_zero_of_abs_ne_zero {a : A} (H : abs a ≠ 0) : a ≠ 0 :=
assume Ha, H (Ha⁻¹ ▸ abs_zero)
assume Ha, H (symm Ha ▸ abs_zero)
/- these assume a linear order -/
@ -893,7 +893,7 @@ section
le.antisymm H1 (nonneg_of_neg_nonpos H2)
theorem abs_eq_zero_iff_eq_zero (a : A) : abs a = 0 ↔ a = 0 :=
iff.intro eq_zero_of_abs_eq_zero (assume H, congr_arg abs H ⬝ abs_zero)
iff.intro eq_zero_of_abs_eq_zero (assume H, trans (congr_arg abs H) abs_zero)
theorem eq_of_abs_sub_eq_zero {a b : A} (H : abs (a - b) = 0) : a = b :=
have a - b = 0, from eq_zero_of_abs_eq_zero H,
@ -904,8 +904,8 @@ section
theorem abs.by_cases {P : A → Prop} {a : A} (H1 : P a) (H2 : P (-a)) : P (abs a) :=
or.elim (le.total 0 a)
(assume H : 0 ≤ a, (abs_of_nonneg H)⁻¹ ▸ H1)
(assume H : a ≤ 0, (abs_of_nonpos H)⁻¹ ▸ H2)
(assume H : 0 ≤ a, symm (abs_of_nonneg H) ▸ H1)
(assume H : a ≤ 0, symm (abs_of_nonpos H) ▸ H2)
theorem abs_le_of_le_of_neg_le (H1 : a ≤ b) (H2 : -a ≤ b) : abs a ≤ b :=
abs.by_cases H1 H2

2
library/algebra/ordered_ring.lean
View file

@ -8,7 +8,7 @@ order and an associated strict order. Our numeric structures (int, rat, and real
of "linear_ordered_comm_ring". This development is modeled after Isabelle's library.
-/
import algebra.ordered_group algebra.ring
open eq eq.ops
open eq
variable {A : Type}

10
library/algebra/ring.lean
View file

@ -7,7 +7,7 @@ Structures with multiplicative and additive components, including semirings, rin
The development is modeled after Isabelle's library.
-/
import algebra.group
open eq eq.ops
open eq
variable {A : Type}
@ -85,7 +85,7 @@ section comm_semiring
has_dvd.mk algebra.dvd
theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b :=
exists.intro _ H⁻¹
exists.intro _ (eq.symm H)
theorem dvd_of_mul_right_eq {a b c : A} (H : a * c = b) : a ∣ b := dvd.intro H
@ -100,7 +100,7 @@ section comm_semiring
exists.elim H₁ H₂
theorem exists_eq_mul_left_of_dvd {a b : A} (H : a ∣ b) : ∃c, b = c * a :=
dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (H1 ⬝ mul.comm a c))
dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul.comm a c)))
theorem dvd.elim_left {P : Prop} {a b : A} (H₁ : a ∣ b) (H₂ : ∀c, b = c * a → P) : P :=
exists.elim (exists_eq_mul_left_of_dvd H₁) (take c, assume H₃ : b = c * a, H₂ c H₃)
@ -120,7 +120,7 @@ section comm_semiring
-/
theorem eq_zero_of_zero_dvd {a : A} (H : 0 ∣ a) : a = 0 :=
dvd.elim H (take c, assume H' : a = 0 * c, H' ⬝ zero_mul c)
dvd.elim H (take c, assume H' : a = 0 * c, eq.trans H' (zero_mul c))
theorem dvd_zero [simp] : a ∣ 0 := dvd.intro (mul_zero a)
@ -157,7 +157,7 @@ section comm_semiring
-/
theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b ∣ c) : a ∣ c :=
dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (eq.symm (Habdc ⬝ mul.assoc a b d)))
dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (eq.symm (eq.trans Habdc (mul.assoc a b d))))
theorem dvd_of_mul_left_dvd {a b c : A} (H : a * b ∣ c) : b ∣ c :=
sorry -- dvd_of_mul_right_dvd begin rewrite mul.comm at H, apply H end

5
library/data/hlist.lean
View file

@ -40,9 +40,8 @@ definition append : Π {l₁ l₂}, hlist B l₁ → hlist B l₂ → hlist B (l
lemma append_nil_left : ∀ {l} (h : hlist B l), append nil h = h :=
sorry -- by intros; reflexivity
open eq.ops
lemma eq_rec_on_cons : ∀ {a₁ a₂ l₁ l₂} (b : B a₁) (h : hlist B l₁) (e : a₁::l₁ = a₂::l₂),
e ▹ cons b h = cons (head_eq_of_cons_eq e ▹ b) (tail_eq_of_cons_eq e ▹ h) :=
eq.rec_on e (cons b h) = cons (eq.rec_on (head_eq_of_cons_eq e) b) (eq.rec_on (tail_eq_of_cons_eq e) h) :=
sorry
/-
begin
@ -51,7 +50,7 @@ end
-/
local attribute list.append [reducible]
lemma append_nil_right : ∀ {l} (h : hlist B l), append h nil = (list.append_nil_right l)⁻¹ ▹ h
lemma append_nil_right : ∀ {l} (h : hlist B l), append h nil = eq.rec_on (eq.symm (list.append_nil_right l)) h
:= sorry
/-
| [] nil := by esimp

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

@ -6,7 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn
Basic properties of lists.
-/
import logic data.nat.order data.nat.sub
open eq.ops nat function tactic
open nat function tactic
namespace list
variable {T : Type}

1
library/data/list/perm.lean
View file

@ -754,7 +754,6 @@ end perm_inter
/- extensionality -/
section ext
open eq.ops
theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a, a ∈ l₁ ↔ a ∈ l₂) → l₁ ~ l₂
:= sorry

8
library/data/list/set.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura
Set-like operations on lists
-/
import data.list.basic data.list.comb
open nat function decidable eq.ops
open nat function decidable
namespace list
section erase
@ -186,7 +186,7 @@ disjoint.comm (disjoint_nil_left l)
lemma disjoint_cons_of_not_mem_of_disjoint {a : A} {l₁ l₂} : a ∉ l₂ → disjoint l₁ l₂ → disjoint (a::l₁) l₂ :=
λ nainl₂ d x (xinal₁ : x ∈ a::l₁),
or.elim (eq_or_mem_of_mem_cons xinal₁)
(λ xeqa : x = a, xeqa⁻¹ ▸ nainl₂)
(λ xeqa : x = a, eq.symm xeqa ▸ nainl₂)
(λ xinl₁ : x ∈ l₁, disjoint_left d xinl₁)
lemma disjoint_of_disjoint_append_left_left : ∀ {l₁ l₂ l : list A}, disjoint (l₁++l₂) l → disjoint l₁ l
@ -262,7 +262,7 @@ theorem disjoint_of_nodup_append : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂)
have nxinl₂ : x ∉ l₂, from not_mem_of_not_mem_append_right this,
take a, suppose a ∈ x::xs,
or.elim (eq_or_mem_of_mem_cons this)
(suppose a = x, this⁻¹ ▸ nxinl₂)
(suppose a = x, eq.symm this ▸ nxinl₂)
(suppose ainxs : a ∈ xs,
have nodup (x::(xs++l₂)), from d,
have nodup (xs++l₂), from nodup_of_nodup_cons this,
@ -770,7 +770,7 @@ theorem mem_insert_iff (x a : A) (l : list A) : x ∈ insert a l ↔ x = a ∨ x
iff.intro
eq_or_mem_of_mem_insert
(assume H, or.elim H
(assume H' : x = a, H'⁻¹ ▸ mem_insert a l)
(assume H' : x = a, eq.symm H' ▸ mem_insert a l)
(assume H' : x ∈ l, mem_insert_of_mem a H'))
theorem nodup_insert (a : A) {l : list A} : nodup l → nodup (insert a l) :=

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

@ -6,7 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
Basic operations on the natural numbers.
-/
import ..num algebra.ring
open binary eq.ops
open binary
namespace nat
@ -173,7 +173,7 @@ nat.induction_on n
-/
theorem eq_zero_of_add_eq_zero_left {n m : ℕ} (H : n + m = 0) : m = 0 :=
eq_zero_of_add_eq_zero_right (nat.add_comm m n ⬝ H)
eq_zero_of_add_eq_zero_right (eq.trans (nat.add_comm m n) H)
theorem eq_zero_and_eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 :=
and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H)

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

@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
Definitions and properties of div and mod. Much of the development follows Isabelle's library.
-/
import .sub
open eq.ops well_founded decidable prod
open well_founded decidable prod
namespace nat
@ -30,16 +30,16 @@ theorem div_def (x y : nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y
congr_fun (fix_eq div.F x) y
protected theorem div_zero [simp] (a : ℕ) : a / 0 = 0 :=
div_def a 0 ⬝ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0))
eq.trans (div_def a 0) $ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0))
theorem div_eq_zero_of_lt {a b : ℕ} (h : a < b) : a / b = 0 :=
div_def a b ⬝ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h))
eq.trans (div_def a b) $ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h))
protected theorem zero_div [simp] (b : ℕ) : 0 / b = 0 :=
div_def 0 b ⬝ if_neg (and.rec not_le_of_gt)
eq.trans (div_def 0 b) $ if_neg (and.rec not_le_of_gt)
theorem div_eq_succ_sub_div {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a / b = succ ((a - b) / b) :=
div_def a b ⬝ if_pos (and.intro h₁ h₂)
eq.trans (div_def a b) $ if_pos (and.intro h₁ h₂)
theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) / z = succ (x / z) :=
sorry
@ -100,16 +100,16 @@ theorem mod_def (x y : nat) : mod x y = if 0 < y ∧ y ≤ x then mod (x - y) y
congr_fun (fix_eq mod.F x) y
theorem mod_zero [simp] (a : ℕ) : a % 0 = a :=
mod_def a 0 ⬝ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0))
eq.trans (mod_def a 0) $ if_neg (not_and_of_not_left (0 ≤ a) (lt.irrefl 0))
theorem mod_eq_of_lt {a b : ℕ} (h : a < b) : a % b = a :=
mod_def a b ⬝ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h))
eq.trans (mod_def a b) $ if_neg (not_and_of_not_right (0 < b) (not_le_of_gt h))
theorem zero_mod [simp] (b : ℕ) : 0 % b = 0 :=
mod_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0)))
eq.trans (mod_def 0 b) $ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0)))
theorem mod_eq_sub_mod {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a % b = (a - b) % b :=
mod_def a b ⬝ if_pos (and.intro h₁ h₂)
eq.trans (mod_def a b) $ if_pos (and.intro h₁ h₂)
theorem add_mod_self [simp] (x z : ℕ) : (x + z) % z = x % z :=
sorry
@ -153,13 +153,13 @@ nat.case_strong_induction_on x
by_cases -- (succ x < y)
(assume H1 : succ x < y,
have succ x % y = succ x, from mod_eq_of_lt H1,
show succ x % y < y, from this⁻¹ ▸ H1)
show succ x % y < y, from eq.symm this ▸ H1)
(assume H1 : ¬ succ x < y,
have y ≤ succ x, from le_of_not_gt H1,
have h : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H this,
have succ x - y < succ x, from sub_lt (succ_pos x) H,
have succ x - y ≤ x, from le_of_lt_succ this,
show succ x % y < y, from h⁻¹ ▸ IH _ this))
show succ x % y < y, from eq.symm h ▸ IH _ this))
theorem mod_one (n : ℕ) : n % 1 = 0 :=
have H1 : n % 1 < 1, from (mod_lt n) (succ_pos 0),
@ -208,7 +208,7 @@ end
-/
theorem mod_eq_sub_div_mul (x y : ℕ) : x % y = x - x / y * y :=
nat.eq_sub_of_add_eq (add.comm (x / y * y) (x % y) ▸ eq_div_mul_add_mod x y)⁻¹
nat.eq_sub_of_add_eq (eq.symm (add.comm (x / y * y) (x % y) ▸ eq_div_mul_add_mod x y))
theorem mod_add_mod (m n k : ℕ) : (m % n + k) % n = (m + k) % n :=
sorry -- by rewrite [eq_div_mul_add_mod m n at {2}, add.assoc, add.comm (m / n * n), add_mul_mod_self]
@ -363,7 +363,7 @@ theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n % m = 0) : m ∣ n :=
dvd.intro (mul.comm (n / m) m ▸ div_mul_cancel_of_mod_eq_zero H)
theorem mod_eq_zero_of_dvd {m n : ℕ} (H : m ∣ n) : n % m = 0 :=
dvd.elim H (take z, assume H1 : n = m * z, H1⁻¹ ▸ mul_mod_right m z)
dvd.elim H (take z, assume H1 : n = m * z, eq.symm H1 ▸ mul_mod_right m z)
theorem dvd_iff_mod_eq_zero (m n : ℕ) : m ∣ n ↔ n % m = 0 :=
iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero
@ -396,11 +396,11 @@ nat.dvd_of_dvd_add_left (add.comm n₁ n₂ ▸ H)
theorem dvd_sub {m n₁ n₂ : ℕ} (H1 : m ∣ n₁) (H2 : m ∣ n₂) : m ∣ n₁ - n₂ :=
by_cases
(assume H3 : n₁ ≥ n₂,
have H4 : n₁ = n₁ - n₂ + n₂, from (nat.sub_add_cancel H3)⁻¹,
have H4 : n₁ = n₁ - n₂ + n₂, from eq.symm (nat.sub_add_cancel H3),
show m ∣ n₁ - n₂, from nat.dvd_of_dvd_add_right (H4 ▸ H1) H2)
(assume H3 : ¬ (n₁ ≥ n₂),
have H4 : n₁ - n₂ = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_ge H3)),
show m ∣ n₁ - n₂, from H4⁻¹ ▸ dvd_zero _)
show m ∣ n₁ - n₂, from eq.symm H4 ▸ dvd_zero _)
theorem dvd.antisymm {m n : ℕ} : m ∣ n → n ∣ m → m = n :=
sorry
@ -442,8 +442,8 @@ theorem dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : k * m ∣ k *
dvd.elim H
(take l,
assume H1 : k * n = k * m * l,
have H2 : n = m * l, from eq_of_mul_eq_mul_left kpos (H1 ⬝ mul.assoc k m l),
dvd.intro H2⁻¹)
have H2 : n = m * l, from eq_of_mul_eq_mul_left kpos (eq.trans H1 $ mul.assoc k m l),
dvd.intro (eq.symm H2))
theorem dvd_of_mul_dvd_mul_right {m n k : ℕ} (kpos : k > 0) (H : m * k ∣ n * k) : m ∣ n :=
nat.dvd_of_mul_dvd_mul_left kpos (mul.comm n k ▸ mul.comm m k ▸ H)
@ -452,12 +452,12 @@ lemma dvd_of_eq_mul (i j n : nat) : n = j*i → j ∣ n :=
sorry -- begin intros, subst n, apply dvd_mul_right end
theorem div_dvd_div {k m n : ℕ} (H1 : k ∣ m) (H2 : m ∣ n) : m / k ∣ n / k :=
have H3 : m = m / k * k, from (nat.div_mul_cancel H1)⁻¹,
have H4 : n = n / k * k, from (nat.div_mul_cancel (dvd.trans H1 H2))⁻¹,
have H3 : m = m / k * k, from eq.symm (nat.div_mul_cancel H1),
have H4 : n = n / k * k, from eq.symm (nat.div_mul_cancel (dvd.trans H1 H2)),
or.elim (eq_zero_or_pos k)
(assume H5 : k = 0,
have H6: n / k = 0, from (congr_arg _ H5 ⬝ nat.div_zero n),
H6⁻¹ ▸ dvd_zero (m / k))
have H6: n / k = 0, from (eq.trans (congr_arg _ H5) $ nat.div_zero n),
eq.symm H6 ▸ dvd_zero (m / k))
(assume H5 : k > 0,
nat.dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2))

16
library/data/nat/gcd.lean
View file

@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
Definitions and properties of gcd, lcm, and coprime.
-/
import .div
open eq.ops well_founded decidable prod
open well_founded decidable prod
namespace nat
@ -39,7 +39,7 @@ calc gcd n 1 = gcd 1 (n % 1) : gcd_succ n 0
theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (x % y)
| 0 := gcd_zero_right _
| (succ y) := gcd_succ x y ⬝ (if_neg (succ_ne_zero y))⁻¹
| (succ y) := eq.trans (gcd_succ x y) $ eq.symm (if_neg (succ_ne_zero y))
theorem gcd_self : Π (n : ℕ), gcd n n = n
@ -55,7 +55,7 @@ theorem gcd_zero_left : Π (n : ℕ), gcd 0 n = n
... = gcd (succ n₁) 0 : sorry -- by rewrite zero_mod
theorem gcd_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m % n) :=
gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
eq.trans (gcd_def m n) $ if_neg (ne_zero_of_pos H)
theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m % n) :=
sorry
@ -114,7 +114,7 @@ dvd.antisymm
(dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
theorem gcd_one_left (m : ℕ) : gcd 1 m = 1 :=
gcd.comm 1 m ⬝ gcd_one_right m
eq.trans (gcd.comm 1 m) $ gcd_one_right m
theorem gcd_mul_left (m n k : ℕ) : gcd (m * n) (m * k) = m * gcd n k :=
sorry
@ -150,7 +150,7 @@ pos_of_dvd_of_pos (gcd_dvd_right m n) npos
theorem eq_zero_of_gcd_eq_zero_left {m n : ℕ} (H : gcd m n = 0) : m = 0 :=
or.elim (eq_zero_or_pos m)
(assume H1, H1)
(assume H1 : m > 0, absurd H⁻¹ (ne_of_lt (gcd_pos_of_pos_left _ H1)))
(assume H1 : m > 0, absurd (eq.symm H) (ne_of_lt (gcd_pos_of_pos_left _ H1)))
theorem eq_zero_of_gcd_eq_zero_right {m n : ℕ} (H : gcd m n = 0) : n = 0 :=
eq_zero_of_gcd_eq_zero_left (gcd.comm m n ▸ H)
@ -229,7 +229,7 @@ calc
theorem dvd_lcm_left (m n : ℕ) : m ∣ lcm m n :=
have H : lcm m n = m * (n / gcd m n), from nat.mul_div_assoc _ $ gcd_dvd_right m n,
dvd.intro H⁻¹
dvd.intro (eq.symm H)
theorem dvd_lcm_right (m n : ℕ) : n ∣ lcm m n :=
lcm.comm n m ▸ dvd_lcm_left n m
@ -349,8 +349,8 @@ show false, from not_lt_of_ge `d ≤ 1` `d > 1`
theorem exists_coprime {m n : ℕ} (H : gcd m n > 0) :
exists m' n', coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n :=
have H1 : m = (m / gcd m n) * gcd m n, from (nat.div_mul_cancel (gcd_dvd_left m n))⁻¹,
have H2 : n = (n / gcd m n) * gcd m n, from (nat.div_mul_cancel (gcd_dvd_right m n))⁻¹,
have H1 : m = (m / gcd m n) * gcd m n, from eq.symm (nat.div_mul_cancel (gcd_dvd_left m n)),
have H2 : n = (n / gcd m n) * gcd m n, from eq.symm (nat.div_mul_cancel (gcd_dvd_right m n)),
exists.intro _ (exists.intro _ (and.intro (coprime_div_gcd_div_gcd H) (and.intro H1 H2)))
theorem coprime_mul {m n k : ℕ} (H1 : coprime m k) (H2 : coprime n k) : coprime (m * n) k :=

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

@ -6,7 +6,6 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
The order relation on the natural numbers.
-/
import .basic algebra.ordered_ring
open eq.ops
namespace nat
@ -222,7 +221,7 @@ theorem succ_pos (n : ℕ) : 0 < succ n :=
zero_lt_succ n
theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
(or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H)))⁻¹
eq.symm (or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H)))
theorem exists_eq_succ_of_lt {n : ℕ} : Π {m : ℕ}, n < m → ∃k, m = succ k
| 0 H := absurd H $ not_lt_zero n
@ -298,7 +297,7 @@ protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m
nat.rec (λm h, absurd h $ not_lt_zero _)
(λn' (IH : ∀ {m : ℕ}, m < n' → P m) m l,
or.by_cases (lt_or_eq_of_le (le_of_lt_succ l))
IH (λ e, eq.rec (H n' @IH) e⁻¹)) (succ n) n $ lt_succ_self n
IH (λ e, eq.rec (H n' @IH) (eq.symm e))) (succ n) n $ lt_succ_self n
protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) :
P n :=
@ -402,7 +401,7 @@ theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 :=
eq_one_of_mul_eq_one_right (mul.comm n m ▸ H)
theorem eq_one_of_mul_eq_self_left {n m : ℕ} (Hpos : n > 0) (H : m * n = n) : m = 1 :=
eq_of_mul_eq_mul_right Hpos (H ⬝ eq.symm (one_mul n))
eq_of_mul_eq_mul_right Hpos (eq.trans H (eq.symm (one_mul n)))
theorem eq_one_of_mul_eq_self_right {n m : ℕ} (Hpos : m > 0) (H : m * n = m) : n = 1 :=
eq_one_of_mul_eq_self_left Hpos (mul.comm m n ▸ H)
@ -410,7 +409,7 @@ eq_one_of_mul_eq_self_left Hpos (mul.comm m n ▸ H)
theorem eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 :=
dvd.elim H
(take m, suppose 1 = n * m,
eq_one_of_mul_eq_one_right this⁻¹)
eq_one_of_mul_eq_one_right (eq.symm this))
/- min and max -/
open decidable

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

@ -6,7 +6,6 @@ Authors: Floris van Doorn, Jeremy Avigad
Subtraction on the natural numbers, as well as min, max, and distance.
-/
import .order
open eq.ops
namespace nat
@ -145,7 +144,7 @@ add.comm m (n - m) ▸ add_sub_of_ge
theorem sub.cases {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k)
: P (n - m) :=
or.elim (le.total n m)
(assume H3 : n ≤ m, (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 H3))
(assume H3 : n ≤ m, eq.symm (sub_eq_zero_of_le H3) ▸ (H1 H3))
(assume H3 : m ≤ n, H2 (n - m) (add_sub_of_le H3))
theorem exists_sub_eq_of_le {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
@ -182,30 +181,30 @@ sub.cases
(take k : ℕ,
assume H1 : m + k = n,
assume H2 : k = 0,
have H3 : n = m, from add_zero m ▸ H2 ▸ H1⁻¹,
have H3 : n = m, from add_zero m ▸ H2 ▸ eq.symm H1,
H3 ▸ le.refl n)
theorem sub_sub.cases {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0)
(H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) :=
or.elim (le.total n m)
(assume H3 : n ≤ m,
(sub_eq_zero_of_le H3)⁻¹ ▸ (H2 (m - n) (add_sub_of_le H3)⁻¹))
eq.symm (sub_eq_zero_of_le H3) ▸ H2 (m - n) (eq.symm (add_sub_of_le H3)))
(assume H3 : m ≤ n,
(sub_eq_zero_of_le H3)⁻¹ ▸ (H1 (n - m) (add_sub_of_le H3)⁻¹))
eq.symm (sub_eq_zero_of_le H3) ▸ (H1 (n - m) (eq.symm (add_sub_of_le H3))))
protected theorem sub_eq_of_add_eq {n m k : ℕ} (H : n + m = k) : k - n = m :=
have H2 : k - n + n = m + n, from
calc
k - n + n = k : nat.sub_add_cancel (le.intro H)
... = n + m : H⁻¹
... = n + m : eq.symm H
... = m + n : add.comm n m,
add.right_cancel H2
protected theorem eq_sub_of_add_eq {a b c : ℕ} (H : a + c = b) : a = b - c :=
(nat.sub_eq_of_add_eq (add.comm a c ▸ H))⁻¹
eq.symm (nat.sub_eq_of_add_eq (add.comm a c ▸ H))
protected theorem sub_eq_of_eq_add {a b c : ℕ} (H : a = c + b) : a - b = c :=
nat.sub_eq_of_add_eq (add.comm c b ▸ H⁻¹)
nat.sub_eq_of_add_eq (add.comm c b ▸ eq.symm H)
protected theorem sub_le_sub_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n - k ≤ m - k :=
sorry
@ -361,10 +360,10 @@ theorem dist_eq_sub_of_gt {n m : ℕ} (H : n > m) : dist n m = n - m :=
dist_eq_sub_of_ge (le_of_lt H)
theorem dist_zero_right (n : ℕ) : dist n 0 = n :=
dist_eq_sub_of_ge (zero_le n) ⬝ nat.sub_zero n
eq.trans (dist_eq_sub_of_ge (zero_le n)) (nat.sub_zero n)
theorem dist_zero_left (n : ℕ) : dist 0 n = n :=
dist_eq_sub_of_le (zero_le n) ⬝ nat.sub_zero n
eq.trans (dist_eq_sub_of_le (zero_le n)) (nat.sub_zero n)
theorem dist.intro {n m k : ℕ} (H : n + m = k) : dist k n = m :=
calc

2
library/data/num.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import data.bool
open bool eq.ops decidable
open bool decidable
namespace pos_num
theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff :=

2
library/data/prod.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Jeremy Avigad
-/
import logic.eq
open inhabited decidable eq.ops
open inhabited decidable
namespace prod
variables {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B} {u : A × B}

2
library/data/sum.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
The sum type, aka disjoint union.
-/
import logic.connectives
open inhabited eq.ops
open inhabited
notation A ⊎ B := sum A B

8
library/init/classical.lean
View file

@ -73,7 +73,6 @@ Prove excluded middle using Hilbert's choice
The proof follows Diaconescu proof that shows that the axiom of choice implies the excluded middle.
-/
section diaconescu
open eq.ops
parameter p : Prop
private definition U (x : Prop) : Prop := x = true ∨ p
@ -93,7 +92,7 @@ or.elim u_def
(assume Hut : u = true,
or.elim v_def
(assume Hvf : v = false,
have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
have Hne : ¬(u = v), from eq.symm Hvf ▸ eq.symm Hut ▸ true_ne_false,
or.inl Hne)
(assume Hp : p, or.inr Hp))
(assume Hp : p, or.inr Hp)
@ -126,11 +125,10 @@ or.elim (em a)
definition eq_true_or_eq_false := prop_complete
section aux
open eq.ops
theorem cases_true_false (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
or.elim (prop_complete a)
(assume Ht : a = true, Ht⁻¹ ▸ H1)
(assume Hf : a = false, Hf⁻¹ ▸ H2)
(assume Ht : a = true, eq.symm Ht ▸ H1)
(assume Hf : a = false, eq.symm Hf ▸ H2)
theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
cases_true_false P H1 H2 a

41
library/init/logic.lean
View file

@ -87,15 +87,12 @@ namespace eq
theorem mpr {a b : Type} : (a = b) → b → a :=
assume H₁ H₂, eq.rec_on (eq.symm H₁) H₂
namespace ops
notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
notation H1 ⬝ H2 := trans H1 H2
notation H1 ▸ H2 := subst H1 H2
notation H1 ▹ H2 := eq.rec H2 H1
end ops
end eq
notation H1 ▸ H2 := eq.subst H1 H2
open eq
theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
eq.subst H₁ (eq.subst H₂ rfl)
@ -107,21 +104,19 @@ congr rfl
section
variables {A : Type} {a b c: A}
open eq.ops
theorem trans_rel_left (R : A → A → Prop) (H₁ : R a b) (H₂ : b = c) : R a c :=
H₂ ▸ H₁
theorem trans_rel_right (R : A → A → Prop) (H₁ : a = b) (H₂ : R b c) : R a c :=
H₁⁻¹ ▸ H₂
symm H₁ ▸ H₂
end
section
variable {p : Prop}
open eq.ops
theorem of_eq_true (H : p = true) : p :=
H⁻¹ ▸ trivial
symm H ▸ trivial
theorem not_of_eq_false (H : p = false) : ¬p :=
assume Hp, H ▸ Hp
@ -148,7 +143,6 @@ definition ne.def [defeq] {A : Type} (a b : A) : ne a b = ¬ (a = b) := rfl
notation a ≠ b := ne a b
namespace ne
open eq.ops
variable {A : Type}
variables {a b : A}
@ -159,13 +153,12 @@ namespace ne
theorem irrefl (H : a ≠ a) : false := H rfl
theorem symm (H : a ≠ b) : b ≠ a :=
assume (H₁ : b = a), H (H₁⁻¹)
assume (H₁ : b = a), H (symm H₁)
end ne
theorem false_of_ne {A : Type} {a : A} : a ≠ a → false := ne.irrefl
section
open eq.ops
variables {p : Prop}
theorem ne_false_of_self : p → p ≠ false :=
@ -216,31 +209,30 @@ definition type_eq_of_heq (H : a == b) : A = B :=
heq.rec_on H (eq.refl A)
end
open eq.ops
theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : H ▹ p == p :=
theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p :=
eq.drec_on H (heq.refl p)
theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : e ▹ p₁ = p₂), p₁ == p₂
theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : eq.rec_on e p₁ = p₂), p₁ == p₂
| a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁)
theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a' = a) (h₂ : p₁ = e ▹ p₂), p₁ == p₂
theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
| a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁)
theorem of_heq_true {a : Prop} (H : a == true) : a :=
of_eq_true (eq_of_heq H)
theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), p₁ ▹ (p₂ ▹ a : B) = (p₂ ⬝ p₁) ▹ a
theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), eq.rec_on p₁ (eq.rec_on p₂ a : B) = eq.rec_on (eq.trans p₂ p₁) a
| A A A (eq.refl A) (eq.refl A) a := calc
eq.refl A ▹ eq.refl A ▹ a = eq.refl A ▹ a : rfl
... = (eq.refl A ⬝ eq.refl A) ▹ a : eq.subst (proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A)) rfl
eq.rec_on (eq.refl A) (eq.rec_on (eq.refl A) a) = eq.rec_on (eq.refl A) a : rfl
... = eq.rec_on (eq.trans (eq.refl A) (eq.refl A)) a : eq.subst (proof_irrel (eq.refl A) (eq.trans (eq.refl A) (eq.refl A))) rfl
theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, p ▹ a₁ = a₂ → a₁ = p⁻¹ ▹ a₂ :=
theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, eq.rec_on p a₁ = a₂ → a₁ = eq.rec_on (eq.symm p) a₂ :=
eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl)
theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), type_eq_of_heq h ▹ a₁ = a₂
theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), eq.rec_on (type_eq_of_heq h) a₁ = a₂
| A A a a (heq.refl a) := rfl
theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = (type_eq_of_heq h)⁻¹ ▹ a₂ :=
theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
attribute heq.refl [refl]
@ -720,7 +712,6 @@ match H a a with
| ff n := absurd rfl n
end
open eq.ops
theorem decidable_eq_inr_neg {A : Type} [H : decidable_eq A] {a b : A} : Π n : a ≠ b, H a b = ff n :=
assume n,
match H a b with

2
library/init/nat.lean
View file

@ -5,7 +5,7 @@ Authors: Floris van Doorn, Leonardo de Moura
-/
prelude
import init.relation init.num
open eq.ops decidable or
open decidable or
notation `ℕ` := nat

1
library/init/simplifier.lean
View file

@ -16,7 +16,6 @@ attribute eq_self_iff_true [simp]
end prove
namespace unit_simp
open eq.ops
-- TODO(dhs): prove these lemmas elsewhere and only gather the
-- [simp] attributes here

4
library/logic/cast.lean
View file

@ -5,9 +5,7 @@ Author: Leonardo de Moura
Casts and heterogeneous equality. See also init.datatypes and init.logic.
-/
import logic.eq logic.quantifiers
open eq.ops
namespace heq
universe variable u
@ -75,7 +73,7 @@ section
--TODO: generalize to eq.rec. This is a special case of rec_on_comp in eq.lean
theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
cast Hbc (cast Hab a) = cast (eq.trans Hab Hbc) a :=
sorry -- by subst Hab
theorem pi_eq (H : P = P') : (Π x, P x) = (Π x, P' x) :=

2
library/logic/connectives.lean
View file

@ -5,8 +5,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Haitao Zhang
The propositional connectives. See also init.datatypes and init.logic.
-/
open eq.ops
variables {a b c d : Prop}
/- implies -/

7
library/logic/eq.lean
View file

@ -5,9 +5,6 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
Additional declarations/theorems about equality. See also init.datatypes and init.logic.
-/
open eq.ops
namespace eq
variables {A B : Type} {a a' a₁ a₂ a₃ a₄ : A}
@ -24,7 +21,7 @@ namespace eq
eq.drec_on H rfl
theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : eq.rec_on H₁ b = eq.rec_on H₂ b :=
rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹
trans (rec_on_constant H₁ b) (symm (rec_on_constant H₂ b))
theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) :
eq.drec_on H b = eq.drec_on H' b :=
@ -87,7 +84,7 @@ section
H₁ ▸ H₂
theorem eqmpr (H₁ : a = b) (H₂ : b) : a :=
H₁⁻¹ ▸ H₂
symm H₁ ▸ H₂
theorem imp_trans (H₁ : a → b) (H₂ : b → c) : a → c :=
assume Ha, H₂ (H₁ Ha)

2
library/logic/quantifiers.lean
View file

@ -56,7 +56,7 @@ iff.intro
(exists_imp_exists (λ x, or.inr)))
section
open decidable eq.ops
open decidable
variables {A : Type} (P : A → Prop) (a : A) [H : decidable (P a)]
include H

2
tests/lean/eta_bug.lean.expected.out
View file

@ -1 +1 @@
λ A x y H₁ H₂, H₂ ▹ H₁
λ A x y H₁ H₂, eq.rec H₁ H₂

6
tests/lean/have1.lean
View file

@ -1,10 +1,10 @@
import logic
open bool eq.ops tactic eq
open bool tactic eq
notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
notation H1 ⬝ H2 := trans H1 H2
constants a b c : bool
axiom H1 : a = b
axiom H2 : b = c
check have e1 : a = b, from H1,
have e2 : a = c, from sorry, -- by apply trans; apply e1; apply H2,
have e3 : c = a, from e2⁻¹,

2
tests/lean/run/541a.lean
View file

@ -1,5 +1,5 @@
import data.list data.nat
open nat list eq.ops
open nat list
section

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

@ -1,5 +1,5 @@
import data.nat data.prod
open nat well_founded decidable prod eq.ops
open nat well_founded decidable prod
-- Auxiliary lemma used to justify recursive call
private definition lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=

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

@ -17,8 +17,6 @@ section
theorem filter_cons (a : A) (l : list A) : filter (a :: l) = if p a then a :: filter l else filter l :=
rfl
open eq.ops
theorem filter_cons_of_pos {a : A} (l : list A) (h : p a) : filter (a :: l) = a :: filter l :=
if_pos h ▸ filter_cons a l

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

@ -1,5 +1,5 @@
import data.nat
open nat eq.ops
open nat
definition fib.F (n : nat) : (Π (m : nat), m < n → nat) → nat :=
nat.cases_on n

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

@ -1,5 +1,5 @@
import data.nat data.prod
open nat well_founded decidable prod eq.ops
open nat well_founded decidable prod
namespace playground

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

@ -10,7 +10,7 @@
-- Basic properties of Lists.
import data.nat
open nat eq.ops
open nat
inductive List (T : Type) : Type :=
| nil {} : List T
| cons : T → List T → List T

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

@ -1,5 +1,4 @@
import logic
open eq.ops
namespace experiment
inductive nat : Type :=
| zero : nat

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

@ -1,5 +1,4 @@
import logic
open eq.ops
namespace experiment
inductive nat : Type :=
| zero : nat

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

@ -1,5 +1,4 @@
import logic
open eq.ops
namespace experiment
inductive nat : Type :=
| zero : nat

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

@ -1,5 +1,5 @@
import data.nat.basic data.bool
open bool nat eq.ops
open bool nat
attribute nat.rec_on [reducible]
definition is_eq (a b : nat) : bool :=

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

@ -1,5 +1,5 @@
import logic data.prod
open eq.ops prod tactic
open prod tactic
inductive tree (A : Type) :=
| leaf : A → tree A

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

@ -1,5 +1,5 @@
import logic data.nat
open eq.ops nat algebra
open nat algebra
inductive tree (A : Type) :=
| leaf : A → tree A

6
tests/lean/show1.lean
View file

@ -1,10 +1,10 @@
import logic
open bool eq.ops tactic
open bool eq tactic
notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
notation H1 ⬝ H2 := trans H1 H2
constants a b c : bool
axiom H1 : a = b
axiom H2 : b = c
check show a = c, from H1 ⬝ H2
print "------------"
check have e1 : a = b, from H1,