From 066b0fcdf94428324967b76cf770c3df2e069ae6 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 24 Jul 2015 11:56:18 -0400 Subject: [PATCH] feat(library): clean up "sorry"s in library Breaking changes: pnat was redefined to use subtype instead of a custom inductive type, which affects the notation for pnat 2 and 3 --- library/algebra/binary.lean | 6 + library/data/empty.lean | 4 +- library/data/fin.lean | 9 +- library/data/finset/basic.lean | 35 +-- library/data/int/basic.lean | 526 ++++++++++++-------------------- library/data/int/order.lean | 28 +- library/data/list/comb.lean | 2 +- library/data/nat/basic.lean | 16 +- library/data/nat/div.lean | 57 ++-- library/data/nat/gcd.lean | 123 +++----- library/data/nat/order.lean | 203 +++++------- library/data/nat/sub.lean | 9 +- library/data/pnat.lean | 142 ++++----- library/data/quotient/util.lean | 100 ++---- library/data/rat/basic.lean | 22 +- library/data/real/basic.lean | 111 +++++-- library/data/real/complete.lean | 14 +- library/data/real/division.lean | 11 +- library/data/real/order.lean | 18 +- library/data/subtype.lean | 12 +- library/init/logic.lean | 275 ++++++++--------- library/init/measurable.lean | 6 +- library/init/nat.lean | 240 ++++++--------- library/logic/connectives.lean | 284 +++++++++-------- library/logic/eq.lean | 5 +- library/logic/identities.lean | 96 ++---- library/logic/instances.lean | 36 +-- library/logic/quantifiers.lean | 80 ++--- 28 files changed, 1005 insertions(+), 1465 deletions(-) diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean index 9ed32fb22..bb733c147 100644 --- a/library/algebra/binary.lean +++ b/library/algebra/binary.lean @@ -58,6 +58,12 @@ namespace binary (a*b)*c = a*(b*c) : H_assoc ... = a*(c*b) : H_comm ... = (a*c)*b : H_assoc + + theorem comm4 (a b c d : A) : a*b*(c*d) = a*c*(b*d) := + calc + a*b*(c*d) = a*b*c*d : H_assoc + ... = a*c*b*d : right_comm H_comm H_assoc + ... = a*c*(b*d) : H_assoc end section diff --git a/library/data/empty.lean b/library/data/empty.lean index 0ed1583e2..1cda7d48d 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -6,8 +6,8 @@ Author: Jeremy Avigad, Floris van Doorn import logic.cast namespace empty - protected theorem elim (A : Type) (H : empty) : A := - empty.rec (λe, A) H + protected theorem elim (A : Type) : empty → A := + empty.rec (λe, A) protected theorem subsingleton [instance] : subsingleton empty := subsingleton.intro (λ a b, !empty.elim a) diff --git a/library/data/fin.lean b/library/data/fin.lean index e3a0f3df2..3b9795606 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -26,8 +26,8 @@ lemma veq_of_eq : ∀ {i j : fin n}, i = j → (val i) = j | (mk iv ilt) (mk jv jlt) := assume Peq, show iv = jv, from fin.no_confusion Peq (λ Pe Pqe, Pe) -lemma eq_iff_veq : ∀ {i j : fin n}, (val i) = j ↔ i = j := -take i j, iff.intro eq_of_veq veq_of_eq +lemma eq_iff_veq {i j : fin n} : (val i) = j ↔ i = j := +iff.intro eq_of_veq veq_of_eq definition val_inj := @eq_of_veq n @@ -37,10 +37,7 @@ section open decidable protected definition has_decidable_eq [instance] (n : nat) : ∀ (i j : fin n), decidable (i = j) | (mk ival ilt) (mk jval jlt) := - match nat.has_decidable_eq ival jval with - | inl veq := inl (by substvars) - | inr vne := inr (by intro h; injection h; contradiction) - end + decidable_of_decidable_of_iff (nat.has_decidable_eq ival jval) eq_iff_veq end lemma dinj_lt (n : nat) : dinj (λ i, i < n) fin.mk := diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index e5cc033c6..1b91a6b87 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -28,10 +28,10 @@ private definition eqv.refl (l : nodup_list A) : l ~ l := !perm.refl private definition eqv.symm {l₁ l₂ : nodup_list A} : l₁ ~ l₂ → l₂ ~ l₁ := -assume p, perm.symm p +perm.symm private definition eqv.trans {l₁ l₂ l₃ : nodup_list A} : l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ := -assume p₁ p₂, perm.trans p₁ p₂ +perm.trans definition finset.nodup_list_setoid [instance] (A : Type) : setoid (nodup_list A) := setoid.mk (@eqv A) (mk_equivalence (@eqv A) (@eqv.refl A) (@eqv.symm A) (@eqv.trans A)) @@ -123,7 +123,7 @@ theorem not_mem_empty [simp] (a : A) : a ∉ ∅ := λ aine : a ∈ ∅, aine theorem mem_empty_iff [simp] (x : A) : x ∈ ∅ ↔ false := -iff.mpr !iff_false_iff_not !not_mem_empty +iff_false_intro !not_mem_empty theorem mem_empty_eq (x : A) : x ∈ ∅ = false := propext !mem_empty_iff @@ -177,30 +177,18 @@ quot.induction_on s theorem eq_or_mem_of_mem_insert {x a : A} {s : finset A} : x ∈ insert a s → x = a ∨ x ∈ s := quot.induction_on s (λ l : nodup_list A, λ H, list.eq_or_mem_of_mem_insert H) -theorem mem_of_mem_insert_of_ne {x a : A} {s : finset A} : x ∈ insert a s → x ≠ a → x ∈ s := -λ xin xne, or.elim (eq_or_mem_of_mem_insert xin) (by contradiction) id +theorem mem_of_mem_insert_of_ne {x a : A} {s : finset A} (xin : x ∈ insert a s) : x ≠ a → x ∈ s := +or_resolve_right (eq_or_mem_of_mem_insert xin) theorem mem_insert_eq (x a : A) (s : finset A) : x ∈ insert a s = (x = a ∨ x ∈ s) := -propext (iff.intro - (!eq_or_mem_of_mem_insert) - (suppose x = a ∨ x ∈ s, or.elim this - (suppose x = a, eq.subst (eq.symm this) !mem_insert) - (suppose x ∈ s, !mem_insert_of_mem this))) +propext (iff.intro !eq_or_mem_of_mem_insert + (or.rec (λH', (eq.substr H' !mem_insert)) !mem_insert_of_mem)) theorem insert_empty_eq (a : A) : '{a} = singleton a := rfl theorem insert_eq_of_mem {a : A} {s : finset A} (H : a ∈ s) : insert a s = s := -ext - take x, - begin - rewrite [!mem_insert_eq], - show x = a ∨ x ∈ s ↔ x ∈ s, from - iff.intro - (assume H1, or.elim H1 - (suppose x = a, eq.subst (eq.symm this) H) - (suppose x ∈ s, this)) - (suppose x ∈ s, or.inr this) - end +ext (λ x, eq.substr (mem_insert_eq x a s) + (or_iff_right_of_imp (λH1, eq.substr H1 H))) theorem card_insert_of_mem {a : A} {s : finset A} : a ∈ s → card (insert a s) = card s := quot.induction_on s @@ -212,9 +200,8 @@ quot.induction_on s theorem card_insert_le (a : A) (s : finset A) : card (insert a s) ≤ card s + 1 := -decidable.by_cases - (suppose a ∈ s, by rewrite [card_insert_of_mem this]; apply le_succ) - (suppose a ∉ s, by rewrite [card_insert_of_not_mem this]) +if H : a ∈ s then by rewrite [card_insert_of_mem H]; apply le_succ +else by rewrite [card_insert_of_not_mem H] lemma ne_empty_of_card_eq_succ {s : finset A} {n : nat} : card s = succ n → s ≠ ∅ := by intros; substvars; contradiction diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 7213e3f8e..a4773c0e5 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -45,49 +45,39 @@ namespace int attribute int.of_nat [coercion] +notation `-[1+` n `]` := int.neg_succ_of_nat n -- for pretty-printing output + /- definitions of basic functions -/ -definition neg_of_nat (m : ℕ) : ℤ := -nat.cases_on m 0 (take m', neg_succ_of_nat m') +definition neg_of_nat : ℕ → ℤ +| 0 := 0 +| (succ m) := -[1+ m] definition sub_nat_nat (m n : ℕ) : ℤ := -nat.cases_on (n - m) - (of_nat (m - n)) -- m ≥ n - (take k, neg_succ_of_nat k) -- m < n, and n - m = succ k +match n - m with + | 0 := m - n -- m ≥ n + | (succ k) := -[1+ k] -- m < n, and n - m = succ k +end definition neg (a : ℤ) : ℤ := - int.cases_on a - (take m, -- a = of_nat m - nat.cases_on m 0 (take m', neg_succ_of_nat m')) - (take m, of_nat (succ m)) -- a = neg_succ_of_nat m +int.cases_on a neg_of_nat succ -definition add (a b : ℤ) : ℤ := - int.cases_on a - (take m, -- a = of_nat m - int.cases_on b - (take n, of_nat (m + n)) -- b = of_nat n - (take n, sub_nat_nat m (succ n))) -- b = neg_succ_of_nat n - (take m, -- a = neg_succ_of_nat m - int.cases_on b - (take n, sub_nat_nat n (succ m)) -- b = of_nat n - (take n, neg_of_nat (succ m + succ n))) -- b = neg_succ_of_nat n +definition add : ℤ → ℤ → ℤ +| (of_nat m) (of_nat n) := m + n +| (of_nat m) -[1+ n] := sub_nat_nat m (succ n) +| -[1+ m] (of_nat n) := sub_nat_nat n (succ m) +| -[1+ m] -[1+ n] := neg_of_nat (succ m + succ n) -definition mul (a b : ℤ) : ℤ := - int.cases_on a - (take m, -- a = of_nat m - int.cases_on b - (take n, of_nat (m * n)) -- b = of_nat n - (take n, neg_of_nat (m * succ n))) -- b = neg_succ_of_nat n - (take m, -- a = neg_succ_of_nat m - int.cases_on b - (take n, neg_of_nat (succ m * n)) -- b = of_nat n - (take n, of_nat (succ m * succ n))) -- b = neg_succ_of_nat n +definition mul : ℤ → ℤ → ℤ +| (of_nat m) (of_nat n) := m * n +| (of_nat m) -[1+ n] := neg_of_nat (m * succ n) +| -[1+ m] (of_nat n) := neg_of_nat (succ m * n) +| -[1+ m] -[1+ n] := succ m * succ n /- notation -/ protected definition prio : num := num.pred std.priority.default -notation `-[1+` n `]` := int.neg_succ_of_nat n -- for pretty-printing output prefix [priority int.prio] - := int.neg infix [priority int.prio] + := int.add infix [priority int.prio] * := int.mul @@ -95,30 +85,25 @@ infix [priority int.prio] * := int.mul /- some basic functions and properties -/ theorem of_nat.inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n := -by injection H; assumption +int.no_confusion H imp.id theorem of_nat_eq_of_nat (m n : ℕ) : of_nat m = of_nat n ↔ m = n := iff.intro of_nat.inj !congr_arg theorem neg_succ_of_nat.inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n := -by injection H; assumption +int.no_confusion H imp.id theorem neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl -definition has_decidable_eq [instance] : decidable_eq ℤ := -take a b, -int.cases_on a - (take m, - int.cases_on b - (take n, - if H : m = n then inl (congr_arg of_nat H) else inr (take H1, H (of_nat.inj H1))) - (take n', inr (by contradiction))) - (take m', - int.cases_on b - (take n, inr (by contradiction)) - (take n', - (if H : m' = n' then inl (congr_arg neg_succ_of_nat H) else - inr (take H1, H (neg_succ_of_nat.inj H1))))) +private definition has_decidable_eq₂ : Π (a b : ℤ), decidable (a = b) +| (of_nat m) (of_nat n) := decidable_of_decidable_of_iff + (nat.has_decidable_eq m n) (iff.symm (of_nat_eq_of_nat m n)) +| (of_nat m) -[1+ n] := inr (by contradiction) +| -[1+ m] (of_nat n) := inr (by contradiction) +| -[1+ m] -[1+ n] := if H : m = n then + inl (congr_arg neg_succ_of_nat H) else inr (not.mto neg_succ_of_nat.inj H) + +definition has_decidable_eq [instance] : decidable_eq ℤ := has_decidable_eq₂ theorem of_nat_add (n m : nat) : of_nat (n + m) = of_nat n + of_nat m := rfl @@ -127,30 +112,23 @@ theorem of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := rfl theorem of_nat_mul (n m : ℕ) : of_nat (n * m) = of_nat n * of_nat m := rfl theorem sub_nat_nat_of_ge {m n : ℕ} (H : m ≥ n) : sub_nat_nat m n = of_nat (m - n) := -have H1 : n - m = 0, from sub_eq_zero_of_le H, -calc - sub_nat_nat m n = nat.cases_on 0 (of_nat (m - n)) _ : H1 ▸ rfl - ... = of_nat (m - n) : rfl +show sub_nat_nat m n = nat.cases_on 0 (m - n) _, from (sub_eq_zero_of_le H) ▸ rfl section local attribute sub_nat_nat [reducible] theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) : - sub_nat_nat m n = neg_succ_of_nat (pred (n - m)) := + sub_nat_nat m n = -[1+ pred (n - m)] := have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_lt H))⁻¹, -calc - sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (of_nat (m - n)) - (take k, neg_succ_of_nat k) : H1 ▸ rfl - ... = neg_succ_of_nat (pred (n - m)) : rfl +show sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (m - n) _, from H1 ▸ rfl end -definition nat_abs (a : ℤ) : ℕ := int.cases_on a (take n, n) (take n', succ n') +definition nat_abs (a : ℤ) : ℕ := int.cases_on a function.id succ -theorem nat_abs_of_nat (n : ℕ) : nat_abs (of_nat n) = n := rfl +theorem nat_abs_of_nat (n : ℕ) : nat_abs n = n := rfl -theorem nat_abs_eq_zero {a : ℤ} : nat_abs a = 0 → a = 0 := -int.cases_on a - (take m, suppose nat_abs (of_nat m) = 0, congr_arg of_nat this) - (take m', suppose nat_abs (neg_succ_of_nat m') = 0, absurd this (succ_ne_zero _)) +theorem nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0 +| (of_nat m) H := congr_arg of_nat H +| -[1+ m'] H := absurd H !succ_ne_zero /- int is a quotient of ordered pairs of natural numbers -/ @@ -162,24 +140,23 @@ protected theorem equiv.refl [refl] {p : ℕ × ℕ} : p ≡ p := !add.comm protected theorem equiv.symm [symm] {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p := calc - pr1 q + pr2 p = pr2 p + pr1 q : !add.comm + pr1 q + pr2 p = pr2 p + pr1 q : add.comm ... = pr1 p + pr2 q : H⁻¹ - ... = pr2 q + pr1 p : !add.comm + ... = pr2 q + pr1 p : add.comm protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r := -have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from - calc - pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by rewrite [*add.assoc, add.comm (pr₂ q)] +add.cancel_right (calc + pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : add.right_comm ... = pr2 p + pr1 q + pr2 r : {H1} ... = pr2 p + (pr1 q + pr2 r) : add.assoc ... = pr2 p + (pr2 q + pr1 r) : {H2} - ... = pr2 p + pr1 r + pr2 q : by rewrite [add.assoc, add.comm (pr₂ q)], -show pr1 p + pr2 r = pr2 p + pr1 r, from add.cancel_right H3 + ... = pr2 p + pr2 q + pr1 r : add.assoc + ... = pr2 p + pr1 r + pr2 q : add.right_comm) protected theorem equiv_equiv : is_equivalence int.equiv := is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans -protected theorem equiv_cases {p q : ℕ × ℕ} (H : int.equiv p q) : +protected theorem equiv_cases {p q : ℕ × ℕ} (H : p ≡ q) : (pr1 p ≥ pr2 p ∧ pr1 q ≥ pr2 q) ∨ (pr1 p < pr2 p ∧ pr1 q < pr2 q) := or.elim (@le_or_gt (pr2 p) (pr1 p)) (suppose pr1 p ≥ pr2 p, @@ -199,109 +176,83 @@ theorem abstr_of_ge {p : ℕ × ℕ} (H : pr1 p ≥ pr2 p) : abstr p = of_nat (p sub_nat_nat_of_ge H theorem abstr_of_lt {p : ℕ × ℕ} (H : pr1 p < pr2 p) : - abstr p = neg_succ_of_nat (pred (pr2 p - pr1 p)) := + abstr p = -[1+ pred (pr2 p - pr1 p)] := sub_nat_nat_of_lt H -definition repr (a : ℤ) : ℕ × ℕ := int.cases_on a (take m, (m, 0)) (take m, (0, succ m)) +definition repr : ℤ → ℕ × ℕ +| (of_nat m) := (m, 0) +| -[1+ m] := (0, succ m) -theorem abstr_repr (a : ℤ) : abstr (repr a) = a := -int.cases_on a (take m, (sub_nat_nat_of_ge (zero_le m))) (take m, rfl) +theorem abstr_repr : Π (a : ℤ), abstr (repr a) = a +| (of_nat m) := (sub_nat_nat_of_ge (zero_le m)) +| -[1+ m] := rfl theorem repr_sub_nat_nat (m n : ℕ) : repr (sub_nat_nat m n) ≡ (m, n) := -or.elim (@le_or_gt n m) - (suppose m ≥ n, - have repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge this ▸ rfl, - this⁻¹ ▸ - (calc - m - n + n = m : sub_add_cancel `m ≥ n` - ... = 0 + m : zero_add)) - (suppose H : m < n, - have repr (sub_nat_nat m n) = (0, succ (pred (n - m))), from sub_nat_nat_of_lt H ▸ rfl, - this⁻¹ ▸ - (calc - 0 + n = n : zero_add - ... = n - m + m : sub_add_cancel (le_of_lt H) - ... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_lt H))⁻¹)) +lt_ge_by_cases + (take H : m < n, + have H1 : repr (sub_nat_nat m n) = (0, n - m), by + rewrite [sub_nat_nat_of_lt H, -(succ_pred_of_pos (sub_pos_of_lt H))], + H1⁻¹ ▸ (!zero_add ⬝ (sub_add_cancel (le_of_lt H))⁻¹)) + (take H : m ≥ n, + have H1 : repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge H ▸ rfl, + H1⁻¹ ▸ ((sub_add_cancel H) ⬝ !zero_add⁻¹)) theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p := !prod.eta ▸ !repr_sub_nat_nat theorem abstr_eq {p q : ℕ × ℕ} (Hequiv : p ≡ q) : abstr p = abstr q := or.elim (int.equiv_cases Hequiv) - (assume H2, - have H3 : pr1 p ≥ pr2 p, from and.elim_left H2, - have H4 : pr1 q ≥ pr2 q, from and.elim_right H2, - have H5 : pr1 p = pr1 q - pr2 q + pr2 p, from - calc - pr1 p = pr1 p + pr2 q - pr2 q : add_sub_cancel - ... = pr2 p + pr1 q - pr2 q : Hequiv - ... = pr2 p + (pr1 q - pr2 q) : add_sub_assoc H4 - ... = pr1 q - pr2 q + pr2 p : add.comm, - have H6 : pr1 p - pr2 p = pr1 q - pr2 q, from - calc - pr1 p - pr2 p = pr1 q - pr2 q + pr2 p - pr2 p : H5 - ... = pr1 q - pr2 q : add_sub_cancel, - abstr_of_ge H3 ⬝ congr_arg of_nat H6 ⬝ (abstr_of_ge H4)⁻¹) - (assume H2, - have H3 : pr1 p < pr2 p, from and.elim_left H2, - have H4 : pr1 q < pr2 q, from and.elim_right H2, - have H5 : pr2 p = pr2 q - pr1 q + pr1 p, from - calc - pr2 p = pr2 p + pr1 q - pr1 q : add_sub_cancel - ... = pr1 p + pr2 q - pr1 q : Hequiv - ... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (le_of_lt H4) - ... = pr2 q - pr1 q + pr1 p : add.comm, - have H6 : pr2 p - pr1 p = pr2 q - pr1 q, from - calc - pr2 p - pr1 p = pr2 q - pr1 q + pr1 p - pr1 p : H5 - ... = pr2 q - pr1 q : add_sub_cancel, - abstr_of_lt H3 ⬝ congr_arg neg_succ_of_nat (congr_arg pred H6)⬝ (abstr_of_lt H4)⁻¹) + (and.rec (assume (Hp : pr1 p ≥ pr2 p) (Hq : pr1 q ≥ pr2 q), + have H : pr1 p - pr2 p = pr1 q - pr2 q, from + calc pr1 p - pr2 p + = pr1 p + pr2 q - pr2 q - pr2 p : add_sub_cancel + ... = pr2 p + pr1 q - pr2 q - pr2 p : Hequiv + ... = pr2 p + (pr1 q - pr2 q) - pr2 p : add_sub_assoc Hq + ... = pr1 q - pr2 q + pr2 p - pr2 p : add.comm + ... = pr1 q - pr2 q : add_sub_cancel, + abstr_of_ge Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_ge Hq)⁻¹)) + (and.rec (assume (Hp : pr1 p < pr2 p) (Hq : pr1 q < pr2 q), + have H : pr2 p - pr1 p = pr2 q - pr1 q, from + calc pr2 p - pr1 p + = pr2 p + pr1 q - pr1 q - pr1 p : add_sub_cancel + ... = pr1 p + pr2 q - pr1 q - pr1 p : Hequiv + ... = pr1 p + (pr2 q - pr1 q) - pr1 p : add_sub_assoc (le_of_lt Hq) + ... = pr2 q - pr1 q + pr1 p - pr1 p : add.comm + ... = pr2 q - pr1 q : add_sub_cancel, + abstr_of_lt Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_lt Hq)⁻¹)) -theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ ((p ≡ p) ∧ (q ≡ q) ∧ (abstr p = abstr q)) := -iff.intro - (assume H : int.equiv p q, - and.intro !equiv.refl (and.intro !equiv.refl (abstr_eq H))) - (assume H : int.equiv p p ∧ int.equiv q q ∧ abstr p = abstr q, - have H1 : abstr p = abstr q, from and.elim_right (and.elim_right H), - equiv.trans (H1 ▸ equiv.symm (repr_abstr p)) (repr_abstr q)) +theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ (abstr p = abstr q) := +iff.intro abstr_eq (assume H, equiv.trans (H ▸ equiv.symm (repr_abstr p)) (repr_abstr q)) + +theorem equiv_iff3 (p q : ℕ × ℕ) : (p ≡ q) ↔ ((p ≡ p) ∧ (q ≡ q) ∧ (abstr p = abstr q)) := +iff.trans !equiv_iff (iff.symm + (iff.trans (and_iff_right !equiv.refl) (and_iff_right !equiv.refl))) theorem eq_abstr_of_equiv_repr {a : ℤ} {p : ℕ × ℕ} (Hequiv : repr a ≡ p) : a = abstr p := -calc - a = abstr (repr a) : abstr_repr - ... = abstr p : abstr_eq Hequiv +!abstr_repr⁻¹ ⬝ abstr_eq Hequiv theorem eq_of_repr_equiv_repr {a b : ℤ} (H : repr a ≡ repr b) : a = b := -calc - a = abstr (repr a) : abstr_repr - ... = abstr (repr b) : abstr_eq H - ... = b : abstr_repr +eq_abstr_of_equiv_repr H ⬝ !abstr_repr section local attribute abstr [reducible] local attribute dist [reducible] -theorem nat_abs_abstr (p : ℕ × ℕ) : nat_abs (abstr p) = dist (pr1 p) (pr2 p) := -let m := pr1 p, n := pr2 p in -or.elim (@le_or_gt n m) - (assume H : m ≥ n, - calc - nat_abs (abstr (m, n)) = nat_abs (of_nat (m - n)) : int.abstr_of_ge H - ... = dist m n : dist_eq_sub_of_ge H) +theorem nat_abs_abstr : Π (p : ℕ × ℕ), nat_abs (abstr p) = dist (pr1 p) (pr2 p) +| (m, n) := lt_ge_by_cases (assume H : m < n, calc - nat_abs (abstr (m, n)) = nat_abs (neg_succ_of_nat (pred (n - m))) : int.abstr_of_lt H - ... = succ (pred (n - m)) : rfl + nat_abs (abstr (m, n)) = nat_abs (-[1+ pred (n - m)]) : int.abstr_of_lt H ... = n - m : succ_pred_of_pos (sub_pos_of_lt H) ... = dist m n : dist_eq_sub_of_le (le_of_lt H)) + (assume H : m ≥ n, (abstr_of_ge H)⁻¹ ▸ (dist_eq_sub_of_ge H)⁻¹) end -theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) := -int.cases_on a - (take n, or.inl (exists.intro n rfl)) - (take n', or.inr (exists.intro (succ n') rfl)) - theorem cases_of_nat_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - (of_nat (succ n))) := int.cases_on a (take m, or.inl (exists.intro _ rfl)) (take m, or.inr (exists.intro _ rfl)) +theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) := +or.imp_right (Exists.rec (take n, (exists.intro _))) !cases_of_nat_succ + theorem by_cases_of_nat {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (- of_nat n)) : P a := @@ -324,87 +275,55 @@ or.elim (cases_of_nat_succ a) definition padd (p q : ℕ × ℕ) : ℕ × ℕ := (pr1 p + pr1 q, pr2 p + pr2 q) -theorem repr_add (a b : ℤ) : repr (add a b) ≡ padd (repr a) (repr b) := -int.cases_on a - (take m, - int.cases_on b - (take n, !equiv.refl) - (take n', - have H1 : int.equiv (repr (add (of_nat m) (neg_succ_of_nat n'))) (m, succ n'), - from !repr_sub_nat_nat, - have H2 : padd (repr (of_nat m)) (repr (neg_succ_of_nat n')) = (m, 0 + succ n'), - from rfl, - (!zero_add ▸ H2)⁻¹ ▸ H1)) - (take m', - int.cases_on b - (take n, - have H1 : int.equiv (repr (add (neg_succ_of_nat m') (of_nat n))) (n, succ m'), - from !repr_sub_nat_nat, - have H2 : padd (repr (neg_succ_of_nat m')) (repr (of_nat n)) = (0 + n, succ m'), - from rfl, - (!zero_add ▸ H2)⁻¹ ▸ H1) - (take n',!repr_sub_nat_nat)) +theorem repr_add : Π (a b : ℤ), repr (add a b) ≡ padd (repr a) (repr b) +| (of_nat m) (of_nat n) := !equiv.refl +| (of_nat m) -[1+ n] := (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat +| -[1+ m] (of_nat n) := (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat +| -[1+ m] -[1+ n] := !repr_sub_nat_nat theorem padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' := -calc - pr1 (padd p q) + pr2 (padd p' q') = pr1 p + pr2 p' + (pr1 q + pr2 q') : - by rewrite [↑padd, *add.assoc, add.left_comm (pr₁ q)] +calc pr1 p + pr1 q + (pr2 p' + pr2 q') + = pr1 p + pr2 p' + (pr1 q + pr2 q') : add.comm4 ... = pr2 p + pr1 p' + (pr1 q + pr2 q') : {Ha} ... = pr2 p + pr1 p' + (pr2 q + pr1 q') : {Hb} - ... = pr2 (padd p q) + pr1 (padd p' q') : by rewrite [↑padd, *add.assoc, add.left_comm (pr₁ p')] + ... = pr2 p + pr2 q + (pr1 p' + pr1 q') : add.comm4 theorem padd_comm (p q : ℕ × ℕ) : padd p q = padd q p := -calc - padd p q = (pr1 p + pr1 q, pr2 p + pr2 q) : rfl - ... = (pr1 q + pr1 p, pr2 p + pr2 q) : add.comm +calc (pr1 p + pr1 q, pr2 p + pr2 q) + = (pr1 q + pr1 p, pr2 p + pr2 q) : add.comm ... = (pr1 q + pr1 p, pr2 q + pr2 p) : add.comm - ... = padd q p : rfl theorem padd_assoc (p q r : ℕ × ℕ) : padd (padd p q) r = padd p (padd q r) := -calc - padd (padd p q) r = (pr1 p + pr1 q + pr1 r, pr2 p + pr2 q + pr2 r) : rfl - ... = (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : add.assoc +calc (pr1 p + pr1 q + pr1 r, pr2 p + pr2 q + pr2 r) + = (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : add.assoc ... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : add.assoc - ... = padd p (padd q r) : rfl theorem add.comm (a b : ℤ) : a + b = b + a := -begin - apply eq_of_repr_equiv_repr, - apply equiv.trans, - apply repr_add, - apply equiv.symm, - apply eq.subst (padd_comm (repr b) (repr a)), - apply repr_add -end +eq_of_repr_equiv_repr (equiv.trans !repr_add + (equiv.symm (!padd_comm ▸ !repr_add))) theorem add.assoc (a b c : ℤ) : a + b + c = a + (b + c) := -assert H1 : repr (a + b + c) ≡ padd (padd (repr a) (repr b)) (repr c), from - equiv.trans (repr_add (a + b) c) (padd_congr !repr_add !equiv.refl), -assert H2 : repr (a + (b + c)) ≡ padd (repr a) (padd (repr b) (repr c)), from - equiv.trans (repr_add a (b + c)) (padd_congr !equiv.refl !repr_add), -begin - apply eq_of_repr_equiv_repr, - apply equiv.trans, - apply H1, - apply eq.subst (padd_assoc _ _ _)⁻¹, - apply equiv.symm, - apply H2 -end +eq_of_repr_equiv_repr (calc + repr (a + b + c) + ≡ padd (repr (a + b)) (repr c) : repr_add + ... ≡ padd (padd (repr a) (repr b)) (repr c) : padd_congr !repr_add !equiv.refl + ... = padd (repr a) (padd (repr b) (repr c)) : !padd_assoc + ... ≡ padd (repr a) (repr (b + c)) : padd_congr !equiv.refl !repr_add + ... ≡ repr (a + (b + c)) : repr_add) -theorem add_zero (a : ℤ) : a + 0 = a := int.cases_on a (take m, rfl) (take m', rfl) +theorem add_zero : Π (a : ℤ), a + 0 = a := int.rec (λm, rfl) (λm, rfl) -theorem zero_add (a : ℤ) : 0 + a = a := add.comm a 0 ▸ add_zero a +theorem zero_add (a : ℤ) : 0 + a = a := !add.comm ▸ !add_zero /- negation -/ definition pneg (p : ℕ × ℕ) : ℕ × ℕ := (pr2 p, pr1 p) -- note: this is =, not just ≡ -theorem repr_neg (a : ℤ) : repr (- a) = pneg (repr a) := -int.cases_on a - (take m, - nat.cases_on m rfl (take m', rfl)) - (take m', rfl) +theorem repr_neg : Π (a : ℤ), repr (- a) = pneg (repr a) +| 0 := rfl +| (succ m) := rfl +| -[1+ m] := rfl theorem pneg_congr {p p' : ℕ × ℕ} (H : p ≡ p') : pneg p ≡ pneg p' := eq.symm H @@ -423,8 +342,13 @@ theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) := show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add.comm ▸ rfl theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p := -show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p, -from sorry -- by simp +calc pr1 p + pr1 q + pr2 q + pr2 p + = pr1 p + (pr1 q + pr2 q) + pr2 p : nat.add.assoc + ... = pr1 p + (pr1 q + pr2 q + pr2 p) : nat.add.assoc + ... = pr1 p + (pr2 q + pr1 q + pr2 p) : nat.add.comm + ... = pr1 p + (pr2 q + pr2 p + pr1 q) : add.right_comm + ... = pr1 p + (pr2 p + pr2 q + pr1 q) : nat.add.comm + ... = pr2 p + pr2 q + pr1 q + pr1 p : nat.add.comm theorem add.left_inv (a : ℤ) : -a + a = 0 := have H : repr (-a + a) ≡ repr 0, from @@ -450,28 +374,20 @@ calc ... = pabs (repr a) : nat_abs_abstr theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b := -have H : nat_abs (a + b) = pabs (padd (repr a) (repr b)), from - calc - nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr - ... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add, -have H1 : nat_abs a = pabs (repr a), from !nat_abs_eq_pabs_repr, -have H2 : nat_abs b = pabs (repr b), from !nat_abs_eq_pabs_repr, -have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b), - from !dist_add_add_le_add_dist_dist, -H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3 +calc + nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr + ... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add + ... ≤ pabs (repr a) + pabs (repr b) : dist_add_add_le_add_dist_dist + ... = pabs (repr a) + nat_abs b : nat_abs_eq_pabs_repr + ... = nat_abs a + nat_abs b : nat_abs_eq_pabs_repr section local attribute nat_abs [reducible] -theorem nat_abs_mul (a b : ℤ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) := -int.cases_on a - (take m, - int.cases_on b - (take n, rfl) - (take n', !nat_abs_neg ▸ rfl)) - (take m', - int.cases_on b - (take n, !nat_abs_neg ▸ rfl) - (take n', rfl)) +theorem nat_abs_mul : Π (a b : ℤ), nat_abs (a * b) = (nat_abs a) * (nat_abs b) +| (of_nat m) (of_nat n) := rfl +| (of_nat m) -[1+ n] := !nat_abs_neg ▸ rfl +| -[1+ m] (of_nat n) := !nat_abs_neg ▸ rfl +| -[1+ m] -[1+ n] := rfl end /- multiplication -/ @@ -483,65 +399,41 @@ theorem repr_neg_of_nat (m : ℕ) : repr (neg_of_nat m) = (0, m) := nat.cases_on m rfl (take m', rfl) -- note: we have =, not just ≡ -theorem repr_mul (a b : ℤ) : repr (mul a b) = pmul (repr a) (repr b) := -int.cases_on a - (take m, - int.cases_on b - (take n, - (calc - pmul (repr m) (repr n) = (m * n + 0 * 0, m * 0 + 0 * n) : rfl - ... = (m * n + 0 * 0, m * 0 + 0) : zero_mul)⁻¹) - (take n', - (calc - pmul (repr m) (repr (neg_succ_of_nat n')) = - (m * 0 + 0 * succ n', m * succ n' + 0 * 0) : rfl - ... = (m * 0 + 0, m * succ n' + 0 * 0) : zero_mul - ... = repr (mul m (neg_succ_of_nat n')) : repr_neg_of_nat)⁻¹)) - (take m', - int.cases_on b - (take n, - (calc - pmul (repr (neg_succ_of_nat m')) (repr n) = - (0 * n + succ m' * 0, 0 * 0 + succ m' * n) : rfl - ... = (0 + succ m' * 0, 0 * 0 + succ m' * n) : zero_mul - ... = (0 + succ m' * 0, succ m' * n) : {!nat.zero_add} - ... = repr (mul (neg_succ_of_nat m') n) : repr_neg_of_nat)⁻¹) - (take n', - (calc - pmul (repr (neg_succ_of_nat m')) (repr (neg_succ_of_nat n')) = - (0 + succ m' * succ n', 0 * succ n') : rfl - ... = (succ m' * succ n', 0 * succ n') : nat.zero_add - ... = (succ m' * succ n', 0) : zero_mul - ... = repr (mul (neg_succ_of_nat m') (neg_succ_of_nat n')) : rfl)⁻¹)) +theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b) +| (of_nat m) (of_nat n) := calc + (m * n + 0 * 0, m * 0 + 0) = (m * n + 0 * 0, m * 0 + 0 * n) : zero_mul +| (of_nat m) -[1+ n] := calc + repr (m * -[1+ n]) = (m * 0 + 0, m * succ n + 0 * 0) : repr_neg_of_nat + ... = (m * 0 + 0 * succ n, m * succ n + 0 * 0) : zero_mul +| -[1+ m] (of_nat n) := calc + repr (-[1+ m] * n) = (0 + succ m * 0, succ m * n) : repr_neg_of_nat + ... = (0 + succ m * 0, 0 + succ m * n) : nat.zero_add + ... = (0 * n + succ m * 0, 0 + succ m * n) : zero_mul +| -[1+ m] -[1+ n] := calc + (succ m * succ n, 0) = (succ m * succ n, 0 * succ n) : zero_mul + ... = (0 + succ m * succ n, 0 * succ n) : nat.zero_add theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ} (H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm) -: xa * xn + ya * yn + (xb * ym + yb * xm) = xa * yn + ya * xn + (xb * xm + yb * ym) := -have H3 : xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn)) - = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)), from - calc - xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn)) - = xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm)) - : sorry -- by simp - ... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : sorry -- by simp - ... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : sorry -- by simp - ... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym)) - : sorry -- by simp - ... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)) - : sorry, -- by simp, -nat.add.cancel_right H3 +: xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) := +nat.add.cancel_right (calc + xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn)) + = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : add.comm4 + ... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : nat.add.comm + ... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : !congr_arg2 add.comm4 add.comm4 + ... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) + : by rewrite[-+mul.left_distrib,-+mul.right_distrib]; exact H1 ▸ H2 ▸ rfl + ... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : !congr_arg2 add.comm4 add.comm4 + ... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : !nat.add.comm ▸ !nat.add.comm ▸ rfl + ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*xm+yb*ym)) : add.comm4 + ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xm+yb*ym + (xb*xn+yb*yn)) : nat.add.comm + ... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : add.comm4) -theorem pmul_congr {p p' q q' : ℕ × ℕ} (H1 : p ≡ p') (H2 : q ≡ q') : pmul p q ≡ pmul p' q' := -equiv_mul_prep H1 H2 +theorem pmul_congr {p p' q q' : ℕ × ℕ} : p ≡ p' → q ≡ q' → pmul p q ≡ pmul p' q' := equiv_mul_prep theorem pmul_comm (p q : ℕ × ℕ) : pmul p q = pmul q p := -calc - (pr1 p * pr1 q + pr2 p * pr2 q, pr1 p * pr2 q + pr2 p * pr1 q) = - (pr1 q * pr1 p + pr2 p * pr2 q, pr1 p * pr2 q + pr2 p * pr1 q) : mul.comm - ... = (pr1 q * pr1 p + pr2 q * pr2 p, pr1 p * pr2 q + pr2 p * pr1 q) : mul.comm - ... = (pr1 q * pr1 p + pr2 q * pr2 p, pr2 q * pr1 p + pr2 p * pr1 q) : mul.comm - ... = (pr1 q * pr1 p + pr2 q * pr2 p, pr2 q * pr1 p + pr1 q * pr2 p) : mul.comm - ... = (pr1 q * pr1 p + pr2 q * pr2 p, pr1 q * pr2 p + pr2 q * pr1 p) : nat.add.comm +show (_,_) = (_,_), from !congr_arg2 + (!congr_arg2 !mul.comm !mul.comm) (!nat.add.comm ⬝ (!congr_arg2 !mul.comm !mul.comm)) theorem mul.comm (a b : ℤ) : a * b = b * a := eq_of_repr_equiv_repr @@ -550,10 +442,14 @@ eq_of_repr_equiv_repr ... = pmul (repr b) (repr a) : pmul_comm ... = repr (b * a) : repr_mul) ▸ !equiv.refl) -theorem pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) := -begin - unfold pmul, apply sorry -- simp -end +private theorem pmul_assoc_prep {p1 p2 q1 q2 r1 r2 : ℕ} : + ((p1*q1+p2*q2)*r1+(p1*q2+p2*q1)*r2, (p1*q1+p2*q2)*r2+(p1*q2+p2*q1)*r1) = + (p1*(q1*r1+q2*r2)+p2*(q1*r2+q2*r1), p1*(q1*r2+q2*r1)+p2*(q1*r1+q2*r2)) := +by rewrite[+mul.left_distrib,+mul.right_distrib,*mul.assoc]; + exact (congr_arg2 pair (!add.comm4 ⬝ (!congr_arg !nat.add.comm)) + (!add.comm4 ⬝ (!congr_arg !nat.add.comm))) + +theorem pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) := pmul_assoc_prep theorem mul.assoc (a b c : ℤ) : (a * b) * c = a * (b * c) := eq_of_repr_equiv_repr @@ -564,54 +460,41 @@ eq_of_repr_equiv_repr ... = pmul (repr a) (repr (b * c)) : repr_mul ... = repr (a * (b * c)) : repr_mul) ▸ !equiv.refl) -set_option pp.coercions true +theorem mul_one : Π (a : ℤ), a * 1 = a +| (of_nat m) := !zero_add -- zero_add happens to be def. = to this thm +| -[1+ m] := !nat.zero_add ▸ rfl -theorem mul_one (a : ℤ) : a * 1 = a := -eq_of_repr_equiv_repr (int.equiv_of_eq - ((calc - repr (a * 1) = pmul (repr a) (repr 1) : repr_mul - ... = (pr1 (repr a), pr2 (repr a)) : - begin - esimp [pmul, nat.of_num, num.to.int, repr], - rewrite [+mul_zero, +mul_one, nat.zero_add] - end - ... = repr a : prod.eta))) theorem one_mul (a : ℤ) : 1 * a = a := mul.comm a 1 ▸ mul_one a +private theorem mul_distrib_prep {a1 a2 b1 b2 c1 c2 : ℕ} : + ((a1+b1)*c1+(a2+b2)*c2, (a1+b1)*c2+(a2+b2)*c1) = + (a1*c1+a2*c2+(b1*c1+b2*c2), a1*c2+a2*c1+(b1*c2+b2*c1)) := +by rewrite[+mul.right_distrib] ⬝ (!congr_arg2 !add.comm4 !add.comm4) + theorem mul.right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c := eq_of_repr_equiv_repr (calc repr ((a + b) * c) = pmul (repr (a + b)) (repr c) : repr_mul ... ≡ pmul (padd (repr a) (repr b)) (repr c) : pmul_congr !repr_add equiv.refl - ... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : sorry -- by simp - ... = padd (repr (a * c)) (pmul (repr b) (repr c)) : {(repr_mul a c)⁻¹} + ... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : mul_distrib_prep + ... = padd (repr (a * c)) (pmul (repr b) (repr c)) : repr_mul ... = padd (repr (a * c)) (repr (b * c)) : repr_mul - ... ≡ repr (a * c + b * c) : equiv.symm !repr_add) + ... ≡ repr (a * c + b * c) : repr_add) theorem mul.left_distrib (a b c : ℤ) : a * (b + c) = a * b + a * c := calc - a * (b + c) = (b + c) * a : mul.comm a (b + c) - ... = b * a + c * a : mul.right_distrib b c a - ... = a * b + c * a : {mul.comm b a} - ... = a * b + a * c : {mul.comm c a} + a * (b + c) = (b + c) * a : mul.comm + ... = b * a + c * a : mul.right_distrib + ... = a * b + c * a : mul.comm + ... = a * b + a * c : mul.comm theorem zero_ne_one : (0 : int) ≠ 1 := -assume H : 0 = 1, -show false, from succ_ne_zero 0 ((of_nat.inj H)⁻¹) +assume H : 0 = 1, !succ_ne_zero (of_nat.inj H)⁻¹ theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 := -have H2 : (nat_abs a) * (nat_abs b) = nat.zero, from - calc - (nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : (nat_abs_mul a b)⁻¹ - ... = (nat_abs 0) : {H} - ... = nat.zero : nat_abs_of_nat nat.zero, -have H3 : (nat_abs a) = nat.zero ∨ (nat_abs b) = nat.zero, - from eq_zero_or_eq_zero_of_mul_eq_zero H2, -or_of_or_of_imp_of_imp H3 - (assume H : (nat_abs a) = nat.zero, nat_abs_eq_zero H) - (assume H : (nat_abs b) = nat.zero, nat_abs_eq_zero H) +or.imp nat_abs_eq_zero nat_abs_eq_zero (eq_zero_or_eq_zero_of_mul_eq_zero (H ▸ (nat_abs_mul a b)⁻¹)) section migrate_algebra open [classes] algebra @@ -628,7 +511,7 @@ section migrate_algebra add_comm := add.comm, mul := mul, mul_assoc := mul.assoc, - one := (of_num 1), + one := 1, one_mul := one_mul, mul_one := mul_one, left_distrib := mul.left_distrib, @@ -647,17 +530,14 @@ section migrate_algebra end migrate_algebra /- additional properties -/ - -theorem of_nat_sub {m n : ℕ} (H : #nat m ≥ n) : of_nat (#nat m - n) = of_nat m - of_nat n := -have H1 : m = (#nat m - n + n), from (nat.sub_add_cancel H)⁻¹, -have H2 : m = (#nat m - n) + n, from congr_arg of_nat H1, -(sub_eq_of_eq_add H2)⁻¹ +theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : m - n = sub m n := +(sub_eq_of_eq_add (!congr_arg (nat.sub_add_cancel H)⁻¹))⁻¹ theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 := by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add] -definition succ (a : ℤ) := a + (nat.succ zero) -definition pred (a : ℤ) := a - (nat.succ zero) +definition succ (a : ℤ) := a + (succ zero) +definition pred (a : ℤ) := a - (succ zero) theorem pred_succ (a : ℤ) : pred (succ a) = a := !sub_add_cancel theorem succ_pred (a : ℤ) : succ (pred a) = a := !add_sub_cancel theorem neg_succ (a : ℤ) : -succ a = pred (-a) := @@ -675,18 +555,12 @@ theorem succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ definition rec_nat_on [unfold 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := -begin - induction z with n n, - {exact nat.rec_on n H0 Hsucc}, - {induction n with m ih, - exact Hpred H0, - exact Hpred ih} -end +int.rec (nat.rec H0 Hsucc) (λn, nat.rec H0 Hpred (nat.succ n)) z --the only computation rule of rec_nat_on which is not definitional theorem rec_nat_on_neg {P : ℤ → Type} (n : nat) (H0 : P zero) (Hsucc : Π⦃n : nat⦄, P n → P (succ n)) (Hpred : Π⦃n : nat⦄, P (-n) → P (-nat.succ n)) : rec_nat_on (-nat.succ n) H0 Hsucc Hpred = Hpred (rec_nat_on (-n) H0 Hsucc Hpred) := -nat.rec_on n rfl (λn H, rfl) +nat.rec rfl (λn H, rfl) n end int diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 105358872..b081aed7c 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -14,8 +14,8 @@ open int eq.ops namespace int private definition nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (take n, false) -definition le (a b : ℤ) : Prop := nonneg (sub b a) -definition lt (a b : ℤ) : Prop := le (add a 1) b +definition le (a b : ℤ) : Prop := nonneg (b - a) +definition lt (a b : ℤ) : Prop := le (a + 1) b infix [priority int.prio] - := int.sub infix [priority int.prio] <= := int.le @@ -28,27 +28,25 @@ definition decidable_le [instance] (a b : ℤ) : decidable (a ≤ b) := decidabl definition decidable_lt [instance] (a b : ℤ) : decidable (a < b) := decidable_nonneg _ private theorem nonneg.elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n := -int.cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H) +int.cases_on a (take n H, exists.intro n rfl) (take n', false.elim) private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) := int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial) theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b := -have b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹, -have nonneg n, from true.intro, -show nonneg (b - a), from `b - a = n`⁻¹ ▸ this +have n = b - a, from eq_add_neg_of_add_eq (!add.comm ▸ H), +show nonneg (b - a), from this ▸ trivial theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b := obtain (n : ℕ) (H1 : b - a = n), from nonneg.elim H, exists.intro n (!add.comm ▸ iff.mpr !add_eq_iff_eq_add_neg (H1⁻¹)) theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a := -or.elim (nonneg_or_nonneg_neg (b - a)) - (assume H, or.inl H) +or.imp_right (assume H : nonneg (-(b - a)), - have -(b - a) = a - b, from neg_sub b a, - have nonneg (a - b), from this ▸ H, - or.inr this) + have -(b - a) = a - b, from !neg_sub, + show nonneg (a - b), from this ▸ H) -- too bad: can't do it in one step + (nonneg_or_nonneg_neg (b - a)) theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : #nat m ≤ n) : of_nat m ≤ of_nat n := obtain (k : ℕ) (Hk : m + k = n), from nat.le.elim H, @@ -133,12 +131,8 @@ theorem lt.irrefl (a : ℤ) : ¬ a < a := (suppose a < a, obtain (n : ℕ) (Hn : a + succ n = a), from lt.elim this, have a + succ n = a + 0, from - calc - a + succ n = a : Hn - ... = a + 0 : by rewrite [add_zero], - have nat.succ n = 0, from add.left_cancel this, - have nat.succ n = 0, from of_nat.inj this, - absurd this !succ_ne_zero) + Hn ⬝ !add_zero⁻¹, + !succ_ne_zero (of_nat.inj (add.left_cancel this))) theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b := (suppose a = b, absurd (this ▸ H) (lt.irrefl b)) diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index 7b3a15476..383b719fd 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -461,7 +461,7 @@ lemma mem_of_dinj_of_mem_dmap (Pdi : dinj p f) : lemma not_mem_dmap_of_dinj_of_not_mem (Pdi : dinj p f) {l : list A} {a} (Pa : p a) : a ∉ l → (f a Pa) ∉ dmap p f l := -not_imp_not_of_imp (mem_of_dinj_of_mem_dmap Pdi Pa) +not.mto (mem_of_dinj_of_mem_dmap Pdi Pa) end dmap diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 792c8c5c1..bcc27be72 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -65,7 +65,7 @@ theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : ∃k : ℕ, n = succ exists.intro _ (or_resolve_right !eq_zero_or_eq_succ_pred H) theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m := -nat.no_confusion H (λe, e) +nat.no_confusion H imp.id abbreviation eq_of_succ_eq_succ := @succ.inj @@ -93,8 +93,7 @@ have stronger : P a ∧ P (succ a), from theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) (H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m := -have general : ∀m, P n m, from nat.induction_on n - (take m : ℕ, H1 m) +have general : ∀m, P n m, from nat.induction_on n H1 (take k : ℕ, assume IH : ∀m, P k m, take m : ℕ, @@ -146,11 +145,14 @@ nat.induction_on k ... = n + succ (m + l) : add_succ ... = n + (m + succ l) : add_succ) -theorem add.left_comm [simp] (n m k : ℕ) : n + (m + k) = m + (n + k) := -left_comm add.comm add.assoc n m k +theorem add.left_comm [simp] : Π (n m k : ℕ), n + (m + k) = m + (n + k) := +left_comm add.comm add.assoc -theorem add.right_comm (n m k : ℕ) : n + m + k = n + k + m := -right_comm add.comm add.assoc n m k +theorem add.right_comm : Π (n m k : ℕ), n + m + k = n + k + m := +right_comm add.comm add.assoc + +theorem add.comm4 : Π {n m k l : ℕ}, n + m + (k + l) = n + k + (m + l) := +comm4 add.comm add.assoc theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k := nat.induction_on n diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 5dfaa4e0f..4330e31d9 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -13,13 +13,13 @@ namespace nat /- div -/ -- auxiliary lemma used to justify div -private definition div_rec_lemma {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x := -and.rec_on H (λ ypos ylex, sub_lt (lt_of_lt_of_le ypos ylex) ypos) +private definition div_rec_lemma {x y : nat} : 0 < y ∧ y ≤ x → x - y < x := +and.rec (λ ypos ylex, sub_lt (lt_of_lt_of_le ypos ylex) ypos) private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero -definition divide (x y : nat) := fix div.F x y +definition divide := fix div.F notation a div b := divide a b theorem divide_def (x y : nat) : divide x y = if 0 < y ∧ y ≤ x then divide (x - y) y + 1 else 0 := @@ -32,7 +32,7 @@ theorem div_eq_zero_of_lt {a b : ℕ} (h : a < b) : a div b = 0 := divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_gt h)) theorem zero_div (b : ℕ) : 0 div b = 0 := -divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0))) +divide_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 div b = succ ((a - b) div b) := divide_def a b ⬝ if_pos (and.intro h₁ h₂) @@ -53,9 +53,10 @@ nat.induction_on y ... = x div z + zero : add_zero) (take y, assume IH : (x + y * z) div z = x div z + y, calc - (x + succ y * z) div z = (x + y * z + z) div z : by rewrite [-add_one, mul.right_distrib, one_mul, add.assoc] + (x + succ y * z) div z = (x + (y * z + z)) div z : succ_mul + ... = (x + y * z + z) div z : add.assoc ... = succ ((x + y * z) div z) : !add_div_self H - ... = x div z + succ y : by rewrite [IH]) + ... = succ (x div z + y) : IH) theorem add_mul_div_self_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) div y = x div y + z := !mul.comm ▸ add_mul_div_self H @@ -75,7 +76,7 @@ theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n := private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x -definition modulo (x y : nat) := fix mod.F x y +definition modulo := fix mod.F notation a mod b := modulo a b notation a `≡` b `[mod`:100 c `]`:0 := a mod c = b mod c @@ -166,12 +167,11 @@ by_cases_zero_pos y (take x, assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y, show succ x = succ x div y * y + succ x mod y, from - by_cases -- (succ x < y) - (assume H1 : succ x < y, - assert H2 : succ x div y = 0, from div_eq_zero_of_lt H1, - assert H3 : succ x mod y = succ x, from mod_eq_of_lt H1, - by rewrite [H2, H3, zero_mul, zero_add]) - (assume H1 : ¬ succ x < y, + if H1 : succ x < y then + have H2 : succ x div y = 0, from div_eq_zero_of_lt H1, + have H3 : succ x mod y = succ x, from mod_eq_of_lt H1, + H2⁻¹ ▸ H3⁻¹ ▸ !zero_mul⁻¹ ▸ !zero_add⁻¹ + else have H2 : y ≤ succ x, from le_of_not_gt H1, have H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2, have H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2, @@ -184,7 +184,7 @@ by_cases_zero_pos y ... = ((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 : sub_add_cancel H2)⁻¹))) + ... = succ x : sub_add_cancel H2)⁻¹)) theorem mod_eq_sub_div_mul (x y : ℕ) : x mod y = x - x div y * y := eq_sub_of_add_eq (!add.comm ▸ !eq_div_mul_add_mod)⁻¹ @@ -244,10 +244,9 @@ have H6 : y > 0, from lt_of_le_of_lt !zero_le H1, show q1 = q2, from eq_of_mul_eq_mul_right H6 H5 theorem mul_div_mul_left {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y := -by_cases - (suppose y = 0, by rewrite [this, mul_zero, *div_zero]) - (suppose y ≠ 0, - have ypos : y > 0, from pos_of_ne_zero this, +if H : y = 0 then H⁻¹ ▸ !mul_zero⁻¹ ▸ !div_zero⁻¹ ▸ !div_zero +else + have ypos : y > 0, from pos_of_ne_zero H, have zypos : z * y > 0, from mul_pos zpos ypos, have H1 : (z * x) mod (z * y) < z * y, from !mod_lt zypos, have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (!mod_lt ypos) zpos, @@ -256,20 +255,17 @@ by_cases ((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : eq_div_mul_add_mod ... = z * (x div y * y + x mod y) : eq_div_mul_add_mod ... = z * (x div y * y) + z * (x mod y) : mul.left_distrib - ... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm)) + ... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm) theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) div (y * z) = x div y := !mul.comm ▸ !mul.comm ▸ !mul_div_mul_left zpos theorem mul_mod_mul_left (z x y : ℕ) : (z * x) mod (z * y) = z * (x mod y) := or.elim (eq_zero_or_pos z) - (assume H : z = 0, - calc - (z * x) mod (z * y) = (0 * x) mod (z * y) : by subst z - ... = 0 mod (z * y) : zero_mul + (assume H : z = 0, H⁻¹ ▸ calc + (0 * x) mod (z * y) = 0 mod (z * y) : zero_mul ... = 0 : zero_mod - ... = 0 * (x mod y) : zero_mul - ... = z * (x mod y) : by subst z) + ... = 0 * (x mod y) : zero_mul) (assume zpos : z > 0, or.elim (eq_zero_or_pos y) (assume H : y = 0, by rewrite [H, mul_zero, *mod_zero]) @@ -288,12 +284,8 @@ theorem mul_mod_mul_right (x z y : ℕ) : (x * z) mod (y * z) = (x mod y) * z := mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ !mul_mod_mul_left theorem mod_self (n : ℕ) : n mod n = 0 := -nat.cases_on n (by unfold modulo) - (take n, - assert (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1), - from !mul_mod_mul_left, - assert (succ n) mod (succ n) = succ n * (1 mod 1), by rewrite [*mul_one at this]; exact this, - by rewrite this) +nat.cases_on n !zero_mod + (take n, !mul_zero ▸ !mul_one ▸ !mul_mod_mul_left) theorem mul_mod_eq_mod_mul_mod (m n k : nat) : (m * n) mod k = ((m mod k) * n) mod k := calc @@ -309,8 +301,7 @@ assert n div 1 * 1 + n mod 1 = n, from !eq_div_mul_add_mod⁻¹, begin rewrite [-this at {2}, mul_one, mod_one] end theorem div_self {n : ℕ} (H : n > 0) : n div n = 1 := -assert (n * 1) div (n * 1) = 1, from !mul_div_mul_left H, -by rewrite [-this, *mul_one] +!mul_one ▸ (!mul_div_mul_left H) theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : m div n * n = m := by rewrite [eq_div_mul_add_mod m n at {2}, H, add_zero] diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean index 05af88c68..82164cf08 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -22,47 +22,37 @@ local infixl `≺`:50 := pair_nat.lt private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) := !mod_lt (succ_pos y₁) -definition gcd.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat := -prod.cases_on p₁ (λx y, nat.cases_on y - (λ f, x) - (λ y₁ (f : Πp₂, p₂ ≺ (x, succ y₁) → nat), f (succ y₁, x mod succ y₁) !gcd.lt.dec)) +definition gcd.F : Π (p₁ : nat × nat), (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat +| (x, 0) f := x +| (x, succ y) f := f (succ y, x mod succ y) !gcd.lt.dec -definition gcd (x y : nat) := fix gcd.F (pair x y) +definition gcd (x y : nat) := fix gcd.F (x, y) -theorem gcd_zero_right (x : nat) : gcd x 0 = x := -well_founded.fix_eq gcd.F (x, 0) +theorem gcd_zero_right (x : nat) : gcd x 0 = x := rfl theorem gcd_succ (x y : nat) : gcd x (succ y) = gcd (succ y) (x mod succ y) := well_founded.fix_eq gcd.F (x, succ y) theorem gcd_one_right (n : ℕ) : gcd n 1 = 1 := -calc gcd n 1 = gcd 1 (n mod 1) : gcd_succ n zero +calc gcd n 1 = gcd 1 (n mod 1) : gcd_succ ... = gcd 1 0 : mod_one - ... = 1 : gcd_zero_right -theorem gcd_def (x y : ℕ) : gcd x y = if y = 0 then x else gcd y (x mod y) := -nat.cases_on y - (calc gcd x 0 = x : gcd_zero_right x - ... = if 0 = 0 then x else gcd zero (x mod zero) : (if_pos rfl)⁻¹) - (λy₁, calc - gcd x (succ y₁) = gcd (succ y₁) (x mod succ y₁) : gcd_succ x y₁ - ... = if succ y₁ = 0 then x else gcd (succ y₁) (x mod succ y₁) : (if_neg (succ_ne_zero y₁))⁻¹) +theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (x mod y) +| 0 := !gcd_zero_right +| (succ y) := !gcd_succ ⬝ (if_neg !succ_ne_zero)⁻¹ -theorem gcd_self (n : ℕ) : gcd n n = n := -nat.cases_on n - rfl - (λn₁, calc - gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ mod succ n₁) : gcd_succ (succ n₁) n₁ - ... = gcd (succ n₁) 0 : mod_self (succ n₁) - ... = succ n₁ : gcd_zero_right) -theorem gcd_zero_left (n : nat) : gcd 0 n = n := -nat.cases_on n - rfl - (λ n₁, calc +theorem gcd_self : Π (n : ℕ), gcd n n = n +| 0 := rfl +| (succ n₁) := calc + gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ mod succ n₁) : gcd_succ + ... = gcd (succ n₁) 0 : mod_self + +theorem gcd_zero_left : Π (n : ℕ), gcd 0 n = n +| 0 := rfl +| (succ n₁) := calc gcd 0 (succ n₁) = gcd (succ n₁) (0 mod succ n₁) : gcd_succ ... = gcd (succ n₁) 0 : zero_mod - ... = (succ n₁) : gcd_zero_right) theorem gcd_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) := gcd_def m n ⬝ if_neg (ne_zero_of_pos H) @@ -70,8 +60,7 @@ gcd_def m n ⬝ if_neg (ne_zero_of_pos H) theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m mod n) := by_cases_zero_pos n (calc - gcd m 0 = m : gcd_zero_right - ... = gcd 0 m : gcd_zero_left + m = gcd 0 m : gcd_zero_left ... = gcd 0 (m mod 0) : mod_zero) (take n, assume H : 0 < n, gcd_of_pos m H) @@ -80,49 +69,32 @@ theorem gcd.induction {P : ℕ → ℕ → Prop} (H0 : ∀m, P m 0) (H1 : ∀m n, 0 < n → P n (m mod n) → P m n) : P m n := -let Q : nat × nat → Prop := λ p : nat × nat, P (pr₁ p) (pr₂ p) in -have aux : Q (m, n), from - well_founded.induction (m, n) (λp, prod.cases_on p - (λm n, nat.cases_on n - (λ ih, show P (pr₁ (m, 0)) (pr₂ (m, 0)), from H0 m) - (λ n₁ (ih : ∀p₂, p₂ ≺ (m, succ n₁) → P (pr₁ p₂) (pr₂ p₂)), - have hlt₁ : 0 < succ n₁, from succ_pos n₁, - have hlt₂ : (succ n₁, m mod succ n₁) ≺ (m, succ n₁), from gcd.lt.dec _ _, - have hp : P (succ n₁) (m mod succ n₁), from ih _ hlt₂, - show P m (succ n₁), from - H1 m (succ n₁) hlt₁ hp))), -aux +induction (m, n) (prod.rec (λm, nat.rec (λ IH, H0 m) + (λ n₁ v (IH : ∀p₂, p₂ ≺ (m, succ n₁) → P (pr₁ p₂) (pr₂ p₂)), + H1 m (succ n₁) !succ_pos (IH _ !gcd.lt.dec)))) theorem gcd_dvd (m n : ℕ) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := gcd.induction m n - (take m, - show (gcd m 0 ∣ m) ∧ (gcd m 0 ∣ 0), by rewrite [*gcd_zero_right]; split; apply dvd.refl; apply dvd_zero) - (take m n, - assume npos : 0 < n, - assume IH : (gcd n (m mod n) ∣ n) ∧ (gcd n (m mod n) ∣ (m mod n)), + (take m, and.intro (!one_mul ▸ !dvd_mul_left) !dvd_zero) + (take m n (npos : 0 < n), and.rec + (assume (IH₁ : gcd n (m mod n) ∣ n) (IH₂ : gcd n (m mod n) ∣ (m mod 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_left) (and.elim_right IH), + dvd_add (dvd.trans IH₁ !dvd_mul_left) IH₂, have H1 : (gcd n (m mod n) ∣ m), from !eq_div_mul_add_mod⁻¹ ▸ H, - have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹, - show (gcd m n ∣ m) ∧ (gcd m n ∣ n), from gcd_eq ▸ (and.intro H1 (and.elim_left IH))) + show (gcd m n ∣ m) ∧ (gcd m n ∣ n), from !gcd_rec⁻¹ ▸ (and.intro H1 IH₁))) -theorem gcd_dvd_left (m n : ℕ) : gcd m n ∣ m := and.elim_left !gcd_dvd +theorem gcd_dvd_left (m n : ℕ) : gcd m n ∣ m := and.left !gcd_dvd -theorem gcd_dvd_right (m n : ℕ) : gcd m n ∣ n := and.elim_right !gcd_dvd +theorem gcd_dvd_right (m n : ℕ) : gcd m n ∣ n := and.right !gcd_dvd theorem dvd_gcd {m n k : ℕ} : k ∣ m → k ∣ n → k ∣ gcd m n := -gcd.induction m n - (take m, assume (h₁ : k ∣ m) (h₂ : k ∣ 0), - show k ∣ gcd m 0, from !gcd_zero_right⁻¹ ▸ h₁) - (take m n, - assume npos : n > 0, - assume IH : k ∣ n → k ∣ m mod n → k ∣ gcd n (m mod n), - assume H1 : k ∣ m, - assume H2 : k ∣ n, - assert k ∣ m div n * n + m mod n, from !eq_div_mul_add_mod ▸ H1, - assert k ∣ m mod n, from nat.dvd_of_dvd_add_left this (dvd.trans H2 !dvd_mul_left), - have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹, - show k ∣ gcd m n, from gcd_eq ▸ IH H2 `k ∣ m mod n`) +gcd.induction m n (take m, imp.intro) + (take m n (npos : n > 0) + (IH : k ∣ n → k ∣ m mod n → k ∣ gcd n (m mod n)) + (H1 : k ∣ m) (H2 : k ∣ n), + have H3 : k ∣ m div n * n + m mod n, from !eq_div_mul_add_mod ▸ H1, + have H4 : k ∣ m mod n, from dvd_of_dvd_add_left H3 (dvd.trans H2 !dvd_mul_left), + !gcd_rec⁻¹ ▸ IH H2 H4) theorem gcd.comm (m n : ℕ) : gcd m n = gcd n m := dvd.antisymm @@ -143,11 +115,7 @@ theorem gcd_one_left (m : ℕ) : gcd 1 m = 1 := theorem gcd_mul_left (m n k : ℕ) : gcd (m * n) (m * k) = m * gcd n k := gcd.induction n k - (take n, - calc - gcd (m * n) (m * 0) = gcd (m * n) 0 : mul_zero - ... = m * n : gcd_zero_right - ... = m * gcd n 0 : gcd_zero_right) + (take n, calc gcd (m * n) (m * 0) = gcd (m * n) 0 : mul_zero) (take n k, assume H : 0 < k, assume IH : gcd (m * k) (m * (n mod k)) = m * gcd k (n mod k), @@ -181,18 +149,11 @@ eq_zero_of_gcd_eq_zero_left (!gcd.comm ▸ H) theorem gcd_div {m n k : ℕ} (H1 : k ∣ m) (H2 : k ∣ n) : gcd (m div k) (n div k) = gcd m n div k := or.elim (eq_zero_or_pos k) - (assume H3 : k = 0, - calc - gcd (m div k) (n div k) = gcd 0 0 : by subst k; rewrite *div_zero - ... = 0 : gcd_zero_left - ... = gcd m n div 0 : div_zero - ... = gcd m n div k : by subst k) - (assume H3 : k > 0, - eq.symm (div_eq_of_eq_mul_left H3 - (eq.symm (calc - gcd (m div k) (n div k) * k = gcd (m div k * k) (n div k * k) : gcd_mul_right - ... = gcd m (n div k * k) : div_mul_cancel H1 - ... = gcd m n : div_mul_cancel H2)))) + (assume H3 : k = 0, by subst k; rewrite *div_zero) + (assume H3 : k > 0, (div_eq_of_eq_mul_left H3 (calc + gcd m n = gcd m (n div k * k) : div_mul_cancel H2 + ... = gcd (m div k * k) (n div k * k) : div_mul_cancel H1 + ... = gcd (m div k) (n div k) * k : gcd_mul_right))⁻¹) theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : gcd m n ∣ gcd (k * m) n := dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index fc1b4ed81..a7db66e1b 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -13,69 +13,48 @@ namespace nat /- lt and le -/ theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n := -or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl) +le_of_eq_or_lt (or.swap H) theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n := -lt.by_cases - (suppose m < n, or.inl this) - (suppose m = n, or.inr this) - (suppose m > n, absurd (lt_of_le_of_lt H this) !lt.irrefl) +or.swap (eq_or_lt_of_le H) theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n := iff.intro lt_or_eq_of_le le_of_lt_or_eq -theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n := -or.elim (lt_or_eq_of_le H1) - (suppose m < n, this) - (suppose m = n, by contradiction) +theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) : m ≠ n → m < n := +or_resolve_right (eq_or_lt_of_le H1) theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n := iff.intro - (suppose m < n, and.intro (le_of_lt this) (take H1, lt.irrefl _ (H1 ▸ this))) - (suppose m ≤ n ∧ m ≠ n, lt_of_le_and_ne (and.elim_left this) (and.elim_right this)) + (take H, and.intro (le_of_lt H) (take H1, !lt.irrefl (H1 ▸ H))) + (and.rec lt_of_le_and_ne) theorem le_add_right (n k : ℕ) : n ≤ n + k := -nat.induction_on k - (calc n ≤ n : le.refl n - ... = n + zero : add_zero) - (λ k (ih : n ≤ n + k), calc - n ≤ succ (n + k) : le_succ_of_le ih - ... = n + succ k : add_succ) +nat.rec !le.refl (λ k, le_succ_of_le) k theorem le_add_left (n m : ℕ): n ≤ m + n := !add.comm ▸ !le_add_right theorem le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m := -h ▸ le_add_right n k +h ▸ !le_add_right -theorem le.elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m := -by induction h with m h ih;existsi 0; reflexivity; - cases ih with k H; existsi succ k; exact congr_arg succ H +theorem le.elim {n m : ℕ} : n ≤ m → ∃k, n + k = m := +le.rec (exists.intro 0 rfl) (λm h, Exists.rec + (λ k H, exists.intro (succ k) (H ▸ rfl))) theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m := -lt.by_cases - (suppose m < n, or.inl (le_of_lt this)) - (suppose m = n, or.inl (by subst m)) - (suppose m > n, or.inr (le_of_lt this)) +or.imp_left le_of_lt !lt_or_ge /- addition -/ theorem add_le_add_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m := -obtain (l : ℕ) (Hl : n + l = m), from le.elim H, -le.intro - (calc - k + n + l = k + (n + l) : add.assoc - ... = k + m : by subst m) +obtain l Hl, from le.elim H, le.intro (Hl ▸ !add.assoc) theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k := !add.comm ▸ !add.comm ▸ add_le_add_left H k theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m := -obtain (l : ℕ) (Hl : k + n + l = k + m), from (le.elim H), -le.intro (add.cancel_left - (calc - k + (n + l) = k + n + l : add.assoc - ... = k + m : Hl)) +obtain l Hl, from le.elim H, le.intro (add.cancel_left (!add.assoc⁻¹ ⬝ Hl)) theorem lt_of_add_lt_add_left {k n m : ℕ} (H : k + n < k + m) : n < m := let H' := le_of_lt H in @@ -121,27 +100,22 @@ theorem max_self [simp] (a : ℕ) : max a a = a := eq.rec_on !if_t_t rfl theorem max_le {n m k : ℕ} (H₁ : n ≤ k) (H₂ : m ≤ k) : max n m ≤ k := -decidable.by_cases - (suppose n < m, by rewrite [↑max, if_pos this]; apply H₂) - (suppose ¬ n < m, by rewrite [↑max, if_neg this]; apply H₁) +if H : n < m then by rewrite [↑max, if_pos H]; apply H₂ +else by rewrite [↑max, if_neg H]; apply H₁ theorem min_le_left (n m : ℕ) : min n m ≤ n := -decidable.by_cases - (suppose n < m, by rewrite [↑min, if_pos this]) - (suppose ¬ n < m, - assert m ≤ n, from or_resolve_right !lt_or_ge this, - by rewrite [↑min, if_neg `¬ n < m`]; apply this) +if H : n < m then by rewrite [↑min, if_pos H] +else assert H' : m ≤ n, from or_resolve_right !lt_or_ge H, + by rewrite [↑min, if_neg H]; apply H' theorem min_le_right (n m : ℕ) : min n m ≤ m := -decidable.by_cases - (suppose n < m, by rewrite [↑min, if_pos this]; apply le_of_lt this) - (suppose ¬ n < m, - by rewrite [↑min, if_neg `¬ n < m`]) +if H : n < m then by rewrite [↑min, if_pos H]; apply le_of_lt H +else assert H' : m ≤ n, from or_resolve_right !lt_or_ge H, + by rewrite [↑min, if_neg H] theorem le_min {n m k : ℕ} (H₁ : k ≤ n) (H₂ : k ≤ m) : k ≤ min n m := -decidable.by_cases - (suppose n < m, by rewrite [↑min, if_pos this]; apply H₁) - (suppose ¬ n < m, by rewrite [↑min, if_neg this]; apply H₂) +if H : n < m then by rewrite [↑min, if_pos H]; apply H₁ +else by rewrite [↑min, if_neg H]; apply H₂ theorem eq_max_right {a b : ℕ} (H : a < b) : b = max a b := (if_pos H)⁻¹ @@ -151,18 +125,14 @@ theorem eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b := open decidable theorem le_max_right (a b : ℕ) : b ≤ max a b := -by_cases - (suppose a < b, eq.rec_on (eq_max_right this) !le.refl) - (suppose ¬ a < b, or.rec_on (eq_or_lt_of_not_lt this) - (suppose a = b, eq.rec_on this (eq.rec_on (eq.symm (max_self a)) !le.refl)) - (suppose b < a, - have h : a = max a b, from eq_max_left (lt.asymm this), - eq.rec_on h (le_of_lt this))) +lt.by_cases + (suppose a < b, (eq_max_right this) ▸ !le.refl) + (suppose a = b, this ▸ !max_self⁻¹ ▸ !le.refl) + (suppose b < a, (eq_max_left (lt.asymm this)) ▸ (le_of_lt this)) theorem le_max_left (a b : ℕ) : a ≤ max a b := -by_cases - (suppose a < b, le_of_lt (eq.rec_on (eq_max_right this) this)) - (suppose ¬ a < b, eq.rec_on (eq_max_left this) !le.refl) +if h : a < b then le_of_lt (eq.rec_on (eq_max_right h) h) +else (eq_max_left h) ▸ !le.refl /- nat is an instance of a linearly ordered semiring and a lattice-/ @@ -221,30 +191,29 @@ section migrate_algebra attribute le.trans ge.trans lt.trans gt.trans [trans] attribute lt_of_lt_of_le lt_of_le_of_lt gt_of_gt_of_ge gt_of_ge_of_gt [trans] - theorem add_pos_left : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < a + b := - take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le - theorem add_pos_right : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < b + a := - take a H b, !add.comm ▸ add_pos_left H b - theorem add_eq_zero_iff_eq_zero_and_eq_zero : ∀{a b : ℕ}, + theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b := + @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le + theorem add_pos_right {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < b + a := + !add.comm ▸ add_pos_left H b + theorem add_eq_zero_iff_eq_zero_and_eq_zero {a b : ℕ} : a + b = 0 ↔ a = 0 ∧ b = 0 := - take a b : ℕ, - @algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le - theorem le_add_of_le_left : ∀{a b c : ℕ}, b ≤ c → b ≤ a + c := - take a b c H, @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H - theorem le_add_of_le_right : ∀{a b c : ℕ}, b ≤ c → b ≤ c + a := - take a b c H, @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le - theorem lt_add_of_lt_left : ∀{b c : ℕ}, b < c → ∀a, b < a + c := - take b c H a, @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H - theorem lt_add_of_lt_right : ∀{b c : ℕ}, b < c → ∀a, b < c + a := - take b c H a, @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le - theorem lt_of_mul_lt_mul_left : ∀{a b c : ℕ}, c * a < c * b → a < b := - take a b c H, @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le - theorem lt_of_mul_lt_mul_right : ∀{a b c : ℕ}, a * c < b * c → a < b := - take a b c H, @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le - theorem pos_of_mul_pos_left : ∀{a b : ℕ}, 0 < a * b → 0 < b := - take a b H, @algebra.pos_of_mul_pos_left _ _ a b H !zero_le - theorem pos_of_mul_pos_right : ∀{a b : ℕ}, 0 < a * b → 0 < a := - take a b H, @algebra.pos_of_mul_pos_right _ _ a b H !zero_le + @algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le + theorem le_add_of_le_left {a b c : ℕ} (H : b ≤ c) : b ≤ a + c := + @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H + theorem le_add_of_le_right {a b c : ℕ} (H : b ≤ c) : b ≤ c + a := + @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le + theorem lt_add_of_lt_left {b c : ℕ} (H : b < c) (a : ℕ) : b < a + c := + @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H + theorem lt_add_of_lt_right {b c : ℕ} (H : b < c) (a : ℕ) : b < c + a := + @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le + theorem lt_of_mul_lt_mul_left {a b c : ℕ} (H : c * a < c * b) : a < b := + @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le + theorem lt_of_mul_lt_mul_right {a b c : ℕ} (H : a * c < b * c) : a < b := + @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le + theorem pos_of_mul_pos_left {a b : ℕ} (H : 0 < a * b) : 0 < b := + @algebra.pos_of_mul_pos_left _ _ a b H !zero_le + theorem pos_of_mul_pos_right {a b : ℕ} (H : 0 < a * b) : 0 < a := + @algebra.pos_of_mul_pos_right _ _ a b H !zero_le end migrate_algebra theorem zero_le_one : 0 ≤ 1 := dec_trivial @@ -266,8 +235,8 @@ eq_zero_of_add_eq_zero_right Hk /- succ and pred -/ -theorem le_of_lt_succ {m n : nat} (H : m < succ n) : m ≤ n := -le_of_succ_le_succ H +theorem le_of_lt_succ {m n : nat} : m < succ n → m ≤ n := +le_of_succ_le_succ theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n := iff.rfl @@ -278,37 +247,20 @@ iff.intro le_of_lt_succ lt_succ_of_le theorem self_le_succ (n : ℕ) : n ≤ succ n := le.intro !add_one -theorem succ_le_or_eq_of_le {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m := -or.elim (lt_or_eq_of_le H) - (suppose n < m, or.inl (succ_le_of_lt this)) - (suppose n = m, or.inr this) +theorem succ_le_or_eq_of_le {n m : ℕ} : n ≤ m → succ n ≤ m ∨ n = m := +lt_or_eq_of_le theorem pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m := -nat.cases_on n - (assume H, !pred_zero⁻¹ ▸ zero_le m) - (take n', - suppose succ n' ≤ succ m, - have n' ≤ m, from le_of_succ_le_succ this, - !pred_succ⁻¹ ▸ this) +pred_le_pred theorem succ_le_of_le_pred {n m : ℕ} : succ n ≤ m → n ≤ pred m := -nat.cases_on m - (assume H, absurd H !not_succ_le_zero) - (take m', - suppose succ n ≤ succ m', - have n ≤ m', from le_of_succ_le_succ this, - !pred_succ⁻¹ ▸ this) +pred_le_pred theorem pred_le_pred_of_le {n m : ℕ} : n ≤ m → pred n ≤ pred m := -nat.cases_on n - (assume H, pred_zero⁻¹ ▸ zero_le (pred m)) - (take n', - suppose succ n' ≤ m, - !pred_succ⁻¹ ▸ succ_le_of_le_pred this) +pred_le_pred -theorem pre_lt_of_lt : ∀ {n m : ℕ}, n < m → pred n < m -| 0 m h := h -| (succ n) m h := lt_of_succ_lt h +theorem pre_lt_of_lt {n m : ℕ} : n < m → pred n < m := +lt_of_le_of_lt !pred_le theorem lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m := lt_of_not_ge @@ -316,13 +268,10 @@ lt_of_not_ge not_lt_of_ge (pred_le_pred_of_le this) H) theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m := -or_of_or_of_imp_left (succ_le_or_eq_of_le H) - (suppose succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ this) +or.imp_left le_of_succ_le_succ (succ_le_or_eq_of_le H) theorem le_pred_self (n : ℕ) : pred n ≤ n := -nat.cases_on n - (pred_zero⁻¹ ▸ !le.refl) - (take k : ℕ, (!pred_succ)⁻¹ ▸ !self_le_succ) +!pred_le theorem succ_pos (n : ℕ) : 0 < succ n := !zero_lt_succ @@ -330,11 +279,9 @@ theorem succ_pos (n : ℕ) : 0 < 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)))⁻¹ -theorem exists_eq_succ_of_lt {n m : ℕ} (H : n < m) : exists k, m = succ k := -discriminate - (suppose m = 0, absurd (this ▸ H) !not_lt_zero) - (take l, suppose m = succ l, - exists.intro l this) +theorem exists_eq_succ_of_lt {n : ℕ} : Π {m : ℕ}, n < m → ∃k, m = succ k +| 0 H := absurd H !not_lt_zero +| (succ k) H := exists.intro k rfl theorem lt_succ_self (n : ℕ) : n < succ n := lt.base n @@ -345,20 +292,10 @@ assume Plt, lt.trans Plt (self_lt_succ j) /- other forms of induction -/ protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n := -have ∀ {n m : nat}, m < n → P m, from - take n, - nat.rec_on n - (show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero) - (take n', - assume IH : ∀ {m : nat}, m < n' → P m, - assert P n', from H n' @IH, - show ∀m, m < succ n' → P m, from - take m, - suppose m < succ n', - or.by_cases (lt_or_eq_of_le (le_of_lt_succ this)) - (suppose m < n', IH this) - (suppose m = n', by subst m; assumption)), -this !lt_succ_self +nat.rec (λm, not.elim !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 protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n := diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index c54793069..0e4c9e5db 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -427,13 +427,8 @@ theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) : (dist_sub_eq_dist_add_left H n ▸ !dist.comm) ▸ !dist.comm theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k := -assert (m - k) + ((k - m) + (m - n)) = (m - n) + ((m - k) + (k - m)), - begin - generalize m - k, generalize k - m, generalize m - n, intro x y z, - rewrite [add.comm y x, add.left_comm] - end, have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)), - by rewrite [add.assoc, this, -add.assoc], +from (!add.comm ▸ !add.left_comm ▸ !add.assoc) ⬝ !add.assoc⁻¹, this ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub theorem dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l := @@ -446,7 +441,7 @@ assert ∀ n m, dist n m = n - m + (m - n), from take n m, rfl, by rewrite [this, this n m, mul.right_distrib, *mul_sub_right_distrib] theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m := -by rewrite [mul.comm k n, mul.comm k m, dist_mul_right, mul.comm] +!mul.comm ▸ !mul.comm ▸ !dist_mul_right ⬝ !mul.comm theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) := have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from diff --git a/library/data/pnat.lean b/library/data/pnat.lean index c06c5ef04..70f4b3a47 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -11,105 +11,89 @@ are those needed for that construction. -/ import data.rat.order data.nat -open nat rat +open nat rat subtype eq.ops namespace pnat -inductive pnat : Type := - pos : Π n : nat, n > 0 → pnat +definition pnat := { n : ℕ | n > 0 } notation `ℕ+` := pnat -definition nat_of_pnat (p : pnat) : ℕ := - pnat.rec_on p (λ n H, n) +theorem pos (n : ℕ) (H : n > 0) : ℕ+ := tag n H + +definition nat_of_pnat (p : ℕ+) : ℕ := elt_of p reserve postfix `~`:std.prec.max_plus local postfix ~ := nat_of_pnat -theorem nat_of_pnat_pos (p : pnat) : p~ > 0 := - pnat.rec_on p (λ n H, H) +theorem pnat_pos (p : ℕ+) : p~ > 0 := has_property p -definition add (p q : pnat) : pnat := - pnat.pos (p~ + q~) (nat.add_pos (nat_of_pnat_pos p) (nat_of_pnat_pos q)) +definition add (p q : ℕ+) : ℕ+ := + tag (p~ + q~) (nat.add_pos (pnat_pos p) (pnat_pos q)) infix `+` := add -definition mul (p q : pnat) : pnat := - pnat.pos (p~ * q~) (nat.mul_pos (nat_of_pnat_pos p) (nat_of_pnat_pos q)) +definition mul (p q : ℕ+) : ℕ+ := + tag (p~ * q~) (nat.mul_pos (pnat_pos p) (pnat_pos q)) infix `*` := mul -definition le (p q : pnat) := p~ ≤ q~ +definition le (p q : ℕ+) := p~ ≤ q~ infix `≤` := le notation p `≥` q := q ≤ p -definition lt (p q : pnat) := p~ < q~ +definition lt (p q : ℕ+) := p~ < q~ infix `<` := lt protected theorem pnat.eq {p q : ℕ+} : p~ = q~ → p = q := - pnat.cases_on p (λ p' Hp, pnat.cases_on q (λ q' Hq, - begin - rewrite ↑nat_of_pnat, - intro H, - generalize Hp, - generalize Hq, - rewrite H, - intro Hp Hq, - apply rfl - end)) + subtype.eq -definition pnat_le_decidable [instance] (p q : pnat) : decidable (p ≤ q) := - pnat.rec_on p (λ n H, pnat.rec_on q - (λ m H2, if Hl : n ≤ m then decidable.inl Hl else decidable.inr Hl)) +definition pnat_le_decidable [instance] (p q : ℕ+) : decidable (p ≤ q) := + nat.decidable_le p~ q~ -definition pnat_lt_decidable [instance] {p q : pnat} : decidable (p < q) := - pnat.rec_on p (λ n H, pnat.rec_on q - (λ m H2, if Hl : n < m then decidable.inl Hl else decidable.inr Hl)) +definition pnat_lt_decidable [instance] {p q : ℕ+} : decidable (p < q) := + nat.decidable_lt p~ q~ -theorem le.trans {p q r : pnat} (H1 : p ≤ q) (H2 : q ≤ r) : p ≤ r := nat.le.trans H1 H2 +theorem le.trans {p q r : ℕ+} (H1 : p ≤ q) (H2 : q ≤ r) : p ≤ r := nat.le.trans H1 H2 -definition max (p q : pnat) := - pnat.pos (nat.max (p~) (q~)) (nat.lt_of_lt_of_le (!nat_of_pnat_pos) (!le_max_right)) +definition max (p q : ℕ+) := + tag (nat.max p~ q~) (nat.lt_of_lt_of_le (!pnat_pos) (!le_max_right)) theorem max_right (a b : ℕ+) : max a b ≥ b := !le_max_right theorem max_left (a b : ℕ+) : max a b ≥ a := !le_max_left theorem max_eq_right {a b : ℕ+} (H : a < b) : max a b = b := - have Hnat : nat.max a~ b~ = b~, from nat.max_eq_right' H, - pnat.eq Hnat + pnat.eq (nat.max_eq_right' H) theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a := - have Hnat : nat.max a~ b~ = a~, from nat.max_eq_left' H, - pnat.eq Hnat + pnat.eq (nat.max_eq_left' H) -theorem le_of_lt {a b : ℕ+} (H : a < b) : a ≤ b := nat.le_of_lt H +theorem le_of_lt {a b : ℕ+} : a < b → a ≤ b := nat.le_of_lt -theorem not_lt_of_ge {a b : ℕ+} (H : a ≤ b) : ¬ (b < a) := nat.not_lt_of_ge H +theorem not_lt_of_ge {a b : ℕ+} : a ≤ b → ¬ (b < a) := nat.not_lt_of_ge -theorem le_of_not_gt {a b : ℕ+} (H : ¬ a < b) : b ≤ a := nat.le_of_not_gt H +theorem le_of_not_gt {a b : ℕ+} : ¬ a < b → b ≤ a := nat.le_of_not_gt theorem eq_of_le_of_ge {a b : ℕ+} (H1 : a ≤ b) (H2 : b ≤ a) : a = b := pnat.eq (nat.eq_of_le_of_ge H1 H2) theorem le.refl (a : ℕ+) : a ≤ a := !nat.le.refl -notation 2 := pnat.pos 2 dec_trivial -notation 3 := pnat.pos 3 dec_trivial -definition pone : pnat := pnat.pos 1 dec_trivial +notation 2 := (tag 2 dec_trivial : ℕ+) +notation 3 := (tag 3 dec_trivial : ℕ+) +definition pone : ℕ+ := tag 1 dec_trivial -definition rat_of_pnat [reducible] (n : ℕ+) : ℚ := - pnat.rec_on n (λ n H, of_nat n) +definition rat_of_pnat [reducible] (n : ℕ+) : ℚ := n~ -theorem pnat.to_rat_of_nat (n : ℕ+) : rat_of_pnat n = of_nat n~ := - pnat.rec_on n (λ n H, rfl) +theorem pnat.to_rat_of_nat (n : ℕ+) : rat_of_pnat n = of_nat n~ := rfl -- these will come in rat theorem rat_of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial theorem rat_of_pnat_ge_one (n : ℕ+) : rat_of_pnat n ≥ 1 := - pnat.rec_on n (λ m h, (iff.mpr !of_nat_le_of_nat) (succ_le_of_lt h)) + (iff.mpr !of_nat_le_of_nat) (pnat_pos n) theorem rat_of_pnat_is_pos (n : ℕ+) : rat_of_pnat n > 0 := - pnat.rec_on n (λ m h, (iff.mpr !of_nat_pos) h) + (iff.mpr !of_nat_pos) (pnat_pos n) theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : m ≤ n) : of_nat m ≤ of_nat n := (iff.mpr !of_nat_le_of_nat) H @@ -118,22 +102,13 @@ theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : m < n) : of_nat m < of_nat n := (iff.mpr !of_nat_lt_of_nat) H theorem rat_of_pnat_le_of_pnat_le {m n : ℕ+} (H : m ≤ n) : rat_of_pnat m ≤ rat_of_pnat n := - begin - rewrite *pnat.to_rat_of_nat, - apply of_nat_le_of_nat_of_le H - end + of_nat_le_of_nat_of_le H theorem rat_of_pnat_lt_of_pnat_lt {m n : ℕ+} (H : m < n) : rat_of_pnat m < rat_of_pnat n := - begin - rewrite *pnat.to_rat_of_nat, - apply of_nat_lt_of_nat_of_lt H - end + of_nat_lt_of_nat_of_lt H theorem pnat_le_of_rat_of_pnat_le {m n : ℕ+} (H : rat_of_pnat m ≤ rat_of_pnat n) : m ≤ n := - begin - rewrite *pnat.to_rat_of_nat at H, - apply (iff.mp !of_nat_le_of_nat) H - end + (iff.mp !of_nat_le_of_nat) H definition inv (n : ℕ+) : ℚ := (1 : ℚ) / rat_of_pnat n postfix `⁻¹` := inv @@ -173,13 +148,14 @@ theorem one_mul (n : ℕ+) : pone * n = n := end theorem pone_le (n : ℕ+) : pone ≤ n := - succ_le_of_lt (nat_of_pnat_pos n) + succ_le_of_lt (pnat_pos n) -theorem pnat_to_rat_mul (a b : ℕ+) : rat_of_pnat (a * b) = rat_of_pnat a * rat_of_pnat b := - by rewrite *pnat.to_rat_of_nat +theorem pnat_to_rat_mul (a b : ℕ+) : rat_of_pnat (a * b) = rat_of_pnat a * rat_of_pnat b := rfl theorem mul_lt_mul_left (a b c : ℕ+) (H : a < b) : a * c < b * c := - nat.mul_lt_mul_of_pos_right H !nat_of_pnat_pos + nat.mul_lt_mul_of_pos_right H !pnat_pos + +theorem one_lt_two : pone < 2 := !nat.le.refl theorem inv_two_mul_lt_inv (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ := begin @@ -189,9 +165,8 @@ theorem inv_two_mul_lt_inv (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ := have H : n~ < (2 * n)~, begin rewrite -one_mul at {1}, apply mul_lt_mul_left, - apply dec_trivial + apply one_lt_two end, - rewrite *pnat.to_rat_of_nat, apply of_nat_lt_of_nat_of_lt, apply H end @@ -238,7 +213,7 @@ theorem inv_mul_le_inv (p q : ℕ+) : (p * q)⁻¹ ≤ q⁻¹ := end theorem pnat_mul_le_mul_left' (a b c : ℕ+) (H : a ≤ b) : c * a ≤ c * b := - nat.mul_le_mul_of_nonneg_left H (nat.le_of_lt !nat_of_pnat_pos) + nat.mul_le_mul_of_nonneg_left H (nat.le_of_lt !pnat_pos) theorem mul.assoc (a b c : ℕ+) : a * b * c = a * (b * c) := pnat.eq !nat.mul.assoc @@ -259,8 +234,6 @@ theorem mul_le_mul_left (p q : ℕ+) : q ≤ p * q := theorem mul_le_mul_right (p q : ℕ+) : p ≤ p * q := by rewrite mul.comm; apply mul_le_mul_left -theorem one_lt_two : pone < 2 := dec_trivial - theorem pnat.lt_of_not_le {p q : ℕ+} (H : ¬ p ≤ q) : q < p := nat.lt_of_not_ge H @@ -275,7 +248,7 @@ theorem lt_add_left (p q : ℕ+) : p < p + q := have H : p~ < p~ + q~, begin rewrite -nat.add_zero at {1}, apply nat.add_lt_add_left, - apply nat_of_pnat_pos + apply pnat_pos end, apply H end @@ -296,30 +269,19 @@ theorem div_le_pnat (q : ℚ) (n : ℕ+) (H : q ≥ n⁻¹) : 1 / q ≤ rat_of_p end theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_pnat n) = m⁻¹ := - begin - have hsimp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c, from sorry, -- simp - rewrite [rat.mul.comm, *inv_mul_eq_mul_inv, hsimp, *inv_cancel_left, *rat.one_mul] - end + assert hsimp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c, from + λa b c, by rewrite[-*rat.mul.assoc]; exact (!rat.mul.right_comm ▸ rfl), + by rewrite [rat.mul.comm, *inv_mul_eq_mul_inv, hsimp, *inv_cancel_left, *rat.one_mul] -definition pceil (a : ℚ) : ℕ+ := pnat.pos (ubound a) !ubound_pos +definition pceil (a : ℚ) : ℕ+ := tag (ubound a) !ubound_pos theorem pceil_helper {a : ℚ} {n : ℕ+} (H : pceil a ≤ n) (Ha : a > 0) : n⁻¹ ≤ 1 / a := - begin - apply rat.le.trans, - apply inv_ge_of_le H, - apply div_le_div_of_le, - apply Ha, - apply ubound_ge - end + rat.le.trans (inv_ge_of_le H) (div_le_div_of_le Ha (ubound_ge a)) theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a := - begin - rewrite -(@div_div' (b / a)), - apply div_le_div_of_le, - apply div_pos_of_pos, - apply pos_div_of_pos_of_pos Hb Ha, - rewrite [(div_div_eq_mul_div (ne_of_gt Hb) (ne_of_gt Ha)), rat.one_mul], - apply ubound_ge - end + div_div' ▸ div_le_div_of_le + (div_pos_of_pos (pos_div_of_pos_of_pos Hb Ha)) + ((div_div_eq_mul_div (ne_of_gt Hb) (ne_of_gt Ha))⁻¹ ▸ + !rat.one_mul⁻¹ ▸ !ubound_ge) end pnat diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean index 2672b5c53..4122e004f 100644 --- a/library/data/quotient/util.lean +++ b/library/data/quotient/util.lean @@ -20,8 +20,8 @@ namespace quotient theorem flip_pair (a : A) (b : B) : flip (pair a b) = pair b a := rfl theorem flip_pr1 (a : A × B) : pr1 (flip a) = pr2 a := rfl theorem flip_pr2 (a : A × B) : pr2 (flip a) = pr1 a := rfl - theorem flip_flip (a : A × B) : flip (flip a) = a := - destruct a (take x y, rfl) + theorem flip_flip : Π a : A × B, flip (flip a) = a + | (pair x y) := rfl theorem P_flip {P : A → B → Prop} (a : A × B) (H : P (pr1 a) (pr2 a)) : P (pr2 (flip a)) (pr1 (flip a)) := @@ -59,14 +59,7 @@ namespace quotient map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B) : - map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') := - calc - map_pair2 f (pair a a') (pair b b') - = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b'))) - : {pr1.mk b b'} - ... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2.mk b b'} - ... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2.mk a a'} - ... = pair (f a b) (f a' b') : {pr1.mk a a'} + map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') := by esimp theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := by esimp @@ -74,91 +67,34 @@ namespace quotient theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := by esimp - theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : - flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) := - have Hx : pr1 (flip (map_pair2 f a b)) = pr1 (map_pair2 f (flip a) (flip b)), from - 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) : {(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) : {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 + theorem map_pair2_flip {A B C : Type} (f : A → B → C) : Π (a : A × A) (b : B × B), + flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) + | (pair a₁ a₂) (pair b₁ b₂) := rfl -- add_rewrite flip_pr1 flip_pr2 flip_pair -- add_rewrite map_pair_pr1 map_pair_pr2 map_pair_pair -- add_rewrite map_pair2_pr1 map_pair2_pr2 map_pair2_pair theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a) - (v w : A × A) : map_pair2 f v w = map_pair2 f w v := -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) : (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) : (map_pair2_pr2 f w v)⁻¹, -pair_eq Hx Hy + : Π (v w : A × A), map_pair2 f v w = map_pair2 f w v +| (pair v₁ v₂) (pair w₁ w₂) := + !map_pair2_pair ⬝ by rewrite [Hcomm v₁ w₁, Hcomm v₂ w₂] ⬝ !map_pair2_pair⁻¹ theorem map_pair2_assoc {A : Type} {f : A → A → A} (Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) : map_pair2 f (map_pair2 f u v) w = map_pair2 f u (map_pair2 f v w) := -have Hx : pr1 (map_pair2 f (map_pair2 f u v) w) = - pr1 (map_pair2 f u (map_pair2 f v w)), from - calc - 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)) : by rewrite [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 - 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)) : {map_pair2_pr2 f _ _} - ... = pr2 (map_pair2 f u (map_pair2 f v w)) : (map_pair2_pr2 f _ _)⁻¹, -pair_eq Hx Hy +show pair (f (f (pr1 u) (pr1 v)) (pr1 w)) (f (f (pr2 u) (pr2 v)) (pr2 w)) = + pair (f (pr1 u) (f (pr1 v) (pr1 w))) (f (pr2 u) (f (pr2 v) (pr2 w))), +by rewrite [Hassoc (pr1 u) (pr1 v) (pr1 w), Hassoc (pr2 u) (pr2 v) (pr2 w)] theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a : A, f a e = a) - (v : A × A) : map_pair2 f v (pair e e) = v := -have Hx : pr1 (map_pair2 f v (pair e e)) = pr1 v, from - (calc - pr1 (map_pair2 f v (pair e e)) = f (pr1 v) (pr1 (pair e e)) : by esimp - ... = f (pr1 v) e : by esimp - ... = pr1 v : Hid (pr1 v)), -have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from - (calc - pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by esimp - ... = f (pr2 v) e : by esimp - ... = pr2 v : Hid (pr2 v)), -prod.eq Hx Hy + : Π (v : A × A), map_pair2 f v (pair e e) = v +| (pair v₁ v₂) := + !map_pair2_pair ⬝ by rewrite [Hid v₁, Hid v₂] theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a) - (v : A × A) : map_pair2 f (pair e e) v = v := -have Hx : pr1 (map_pair2 f (pair e e) v) = pr1 v, from - calc - pr1 (map_pair2 f (pair e e) v) = f (pr1 (pair e e)) (pr1 v) : by esimp - ... = f e (pr1 v) : by esimp - ... = pr1 v : Hid (pr1 v), -have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from - calc - pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by esimp - ... = f e (pr2 v) : by esimp - ... = pr2 v : Hid (pr2 v), -prod.eq Hx Hy + : Π (v : A × A), map_pair2 f (pair e e) v = v +| (pair v₁ v₂) := + !map_pair2_pair ⬝ by rewrite [Hid v₁, Hid v₂] end quotient diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index bb1e584d5..14a2684b9 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -92,6 +92,9 @@ prerat.mk (num a * num b) (denom a * denom b) (mul_denom_pos a b) definition neg (a : prerat) : prerat := prerat.mk (- num a) (denom a) (denom_pos a) +definition smul (a : ℤ) (b : prerat) (H : a > 0) : prerat := +prerat.mk (a * num b) (a * denom b) (mul_pos H (denom_pos b)) + theorem of_int_add (a b : ℤ) : of_int (#int a + b) ≡ add (of_int a) (of_int b) := by esimp [equiv, num, denom, one, add, of_int]; rewrite [*int.mul_one] @@ -199,6 +202,9 @@ theorem inv_equiv_inv : ∀{a b : prerat}, a ≡ b → inv a ≡ inv b by rewrite [↑equiv at *, ▸*, mul.comm ad, mul.comm bd, H] ... ≡ inv (mk bn bd bdp) : (inv_of_pos bn_pos bdp)⁻¹) +theorem smul_equiv {a : ℤ} {b : prerat} (H : a > 0) : smul a b H ≡ b := +by esimp[equiv, smul]; rewrite[mul.assoc, mul.left_comm] + /- properties -/ theorem add.comm (a b : prerat) : add a b ≡ add b a := @@ -223,12 +229,18 @@ by rewrite [↑mul, ↑equiv, *mul.assoc] theorem mul_one (a : prerat) : mul a one ≡ a := by rewrite [↑mul, ↑one, ↑of_int, ↑equiv, ▸*, *mul_one] --- with the simplifier this will be easy theorem mul.left_distrib (a b c : prerat) : mul a (add b c) ≡ add (mul a b) (mul a c) := -begin - rewrite [↑mul, ↑add, ↑equiv, ▸*, *mul.left_distrib, *mul.right_distrib, -*int.mul.assoc], - apply sorry -end +have H : smul (denom a) (mul a (add b c)) (denom_pos a) = + add (mul a b) (mul a c), from begin + rewrite[↑smul, ↑mul, ↑add], + congruence, + rewrite[*mul.left_distrib, *mul.right_distrib, -*int.mul.assoc], + have T : ∀ {x y z w : ℤ}, x*y*z*w=y*z*x*w, from + λx y z w, (!int.mul.assoc ⬝ !int.mul.comm) ▸ rfl, + exact !congr_arg2 T T, + exact !mul.left_comm ▸ !int.mul.assoc⁻¹ +end, +equiv.symm (H ▸ smul_equiv (denom_pos a)) theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ one | (mk an ad adp) := diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 41e5e1ad9..93407fb30 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -27,13 +27,18 @@ theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c ∧ c > 0 (and.intro (have H2 [visible] : a + a > (b + b) + (a - b), from calc a + a > b + a : rat.add_lt_add_right H ... = b + a + b - b : rat.add_sub_cancel - ... = (b + b) + (a - b) : sorry, -- simp + ... = b + b + a - b : rat.add.right_comm + ... = (b + b) + (a - b) : add_sub, have H3 [visible] : (a + a) / (1 + 1) > ((b + b) + (a - b)) / (1 + 1), from div_lt_div_of_lt_of_pos H2 dec_trivial, by rewrite [div_two at H3, -div_add_div_same at H3, div_two at H3]; exact H3) (pos_div_of_pos_of_pos (iff.mpr !sub_pos_iff_lt H) dec_trivial)) -theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := sorry +theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := + calc + a + b - (c + d) = a + b - c - d : sub_add_eq_sub_sub + ... = a - c + b - d : sub_add_eq_add_sub + ... = a - c + (b - d) : add_sub theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) : q * n⁻¹ ≤ ε := @@ -52,7 +57,19 @@ theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) : p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ := by rewrite [rat.mul.assoc, rat.right_distrib, *inv_mul_eq_mul_inv] -theorem find_thirds (a b : ℚ) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b := sorry +theorem find_thirds (a b : ℚ) (H : b > 0) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b := + let n := pceil (of_nat 4 / b) in + have of_nat 3 * n⁻¹ < b, from calc + of_nat 3 * n⁻¹ < of_nat 4 * n⁻¹ + : rat.mul_lt_mul_of_pos_right dec_trivial !inv_pos + ... ≤ of_nat 4 * (b / of_nat 4) + : rat.mul_le_mul_of_nonneg_left (!inv_pceil_div dec_trivial H) !of_nat_nonneg + ... = b / of_nat 4 * of_nat 4 : rat.mul.comm + ... = b : rat.div_mul_cancel dec_trivial, + exists.intro n (calc + a + n⁻¹ + n⁻¹ + n⁻¹ = a + (1 + 1 + 1) * n⁻¹ : by rewrite[*rat.right_distrib,*rat.one_mul,-*rat.add.assoc] + ... = a + of_nat 3 * n⁻¹ : {show 1+1+1=of_nat 3, from dec_trivial} + ... < a + b : rat.add_lt_add_left this a) theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻¹) : a ≤ b := begin @@ -60,7 +77,7 @@ theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻ intro Hb, apply (exists.elim (find_midpoint Hb)), intro c Hc, - apply (exists.elim (find_thirds b c)), + apply (exists.elim (find_thirds b c (and.right Hc))), intro j Hbj, have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj (and.left Hc), exact absurd !H (not_le_of_gt Ha) @@ -77,26 +94,52 @@ theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a end theorem rewrite_helper (a b c d : ℚ) : a * b - c * d = a * (b - d) + (a - c) * d := - sorry + by rewrite[rat.mul_sub_left_distrib, rat.mul_sub_right_distrib, add_sub, rat.sub_add_cancel] theorem rewrite_helper3 (a b c d e f g: ℚ) : a * (b + c) - (d * e + f * g) = - (a * b - d * e) + (a * c - f * g) := sorry + (a * b - d * e) + (a * c - f * g) := + by rewrite[rat.mul.left_distrib, add_sub_comm] -theorem rewrite_helper4 (a b c d : ℚ) : a * b - c * d = (a * b - a * d) + (a * d - c * d) := sorry +theorem rewrite_helper4 (a b c d : ℚ) : a * b - c * d = (a * b - a * d) + (a * d - c * d) := + by rewrite[add_sub, rat.sub_add_cancel] -theorem rewrite_helper5 (a b x y : ℚ) : a - b = (a - x) + (x - y) + (y - b) := sorry +theorem rewrite_helper5 (a b x y : ℚ) : a - b = (a - x) + (x - y) + (y - b) := + by rewrite[*add_sub, *rat.sub_add_cancel] theorem rewrite_helper7 (a b c d x : ℚ) : - a * b * c - d = (b * c) * (a - x) + (x * b * c - d) := sorry + a * b * c - d = (b * c) * (a - x) + (x * b * c - d) := + by rewrite[rat.mul_sub_left_distrib, add_sub]; exact (calc + a * b * c - d = a * b * c - x * b * c + x * b * c - d : rat.sub_add_cancel + ... = b * c * a - b * c * x + x * b * c - d : + have ∀ {a b c : ℚ}, a * b * c = b * c * a, from + λa b c, !rat.mul.comm ▸ !rat.mul.right_comm, + this ▸ this ▸ rfl) theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) (H2 : b ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) : - (rat_of_pnat k) * a + b * (rat_of_pnat k) ≤ m⁻¹ + n⁻¹ := sorry + (rat_of_pnat k) * a + b * (rat_of_pnat k) ≤ m⁻¹ + n⁻¹ := + have (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹ = (2 * k)⁻¹ * (m⁻¹ + n⁻¹), + by rewrite[rat.mul.left_distrib,*inv_mul_eq_mul_inv]; exact !rat.mul.comm ▸ rfl, + have a + b ≤ k⁻¹ * (m⁻¹ + n⁻¹), from calc + a + b ≤ (2 * k)⁻¹ * (m⁻¹ + n⁻¹) + (2 * k)⁻¹ * (m⁻¹ + n⁻¹) : rat.add_le_add (this ▸ H) (this ▸ H2) + ... = ((2 * k)⁻¹ + (2 * k)⁻¹) * (m⁻¹ + n⁻¹) : rat.mul.right_distrib + ... = k⁻¹ * (m⁻¹ + n⁻¹) : (pnat.add_halves k) ▸ rfl, + calc (rat_of_pnat k) * a + b * (rat_of_pnat k) + = (rat_of_pnat k) * a + (rat_of_pnat k) * b : rat.mul.comm + ... = (rat_of_pnat k) * (a + b) : rat.left_distrib + ... ≤ (rat_of_pnat k) * (k⁻¹ * (m⁻¹ + n⁻¹)) : + iff.mp (!rat.le_iff_mul_le_mul_left !rat_of_pnat_is_pos) this + ... = m⁻¹ + n⁻¹ : by rewrite[-rat.mul.assoc, inv_cancel_left, rat.one_mul] theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ((a - d) + (c - e)) := - sorry + !congr_arg (calc + a + b + c - (d + (b + e)) = a + b + c - (d + b + e) : rat.add.assoc + ... = a + b - (d + b) + (c - e) : add_sub_comm + ... = a + b - b - d + (c - e) : sub_add_eq_sub_sub_swap + ... = a - d + (c - e) : rat.add_sub_cancel) -theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) := sorry +theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) := + !rat.add.comm ▸ (binary.comm4 rat.add.comm rat.add.assoc a b c d) ------------------------------------- -- The only sorry's after this point are for the simplifier. @@ -164,8 +207,12 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t) apply rat.add_le_add, apply HNj (max j Nj) (max_right j Nj), apply Ht, - have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = (n⁻¹ + n⁻¹ + j⁻¹) + (m⁻¹ + m⁻¹), - from sorry, -- simplifier + have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹), + from λm, calc + n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) + m⁻¹ : rat.add.right_comm + ... = n⁻¹ + (j⁻¹ + m⁻¹ + n⁻¹) + m⁻¹ : rat.add.assoc + ... = n⁻¹ + (n⁻¹ + (j⁻¹ + m⁻¹)) + m⁻¹ : rat.add.comm + ... = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹) : by rewrite[-*rat.add.assoc], rewrite hsimp, have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin apply rat.add_le_add, @@ -247,8 +294,8 @@ theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of ... = abs (s pone) + (1 + 1) : by rewrite [add.comm 1 (abs (s pone)), rat.add.comm 1, rat.add.assoc] ... ≤ of_nat (ubound (abs (s pone))) + (1 + 1) : rat.add_le_add_right (!ubound_ge) - ... = of_nat (ubound (abs (s pone)) + (1 + 1)) : by rewrite of_nat_add - ... = of_nat (ubound (abs (s pone)) + 1 + 1) : by rewrite nat.add.assoc + ... = of_nat (ubound (abs (s pone)) + (1 + 1)) : of_nat_add + ... = of_nat (ubound (abs (s pone)) + 1 + 1) : nat.add.assoc definition K₂ (s t : seq) := max (K s) (K t) @@ -546,13 +593,13 @@ theorem s_add_zero (s : seq) (H : regular s) : sadd s zero ≡ s := apply rat.le.refl end - theorem s_neg_cancel (s : seq) (H : regular s) : sadd (sneg s) s ≡ zero := - begin - rewrite [↑sadd, ↑sneg, ↑regular at H, ↑zero, ↑equiv], - intros, - rewrite [neg_add_eq_sub, rat.sub_self, rat.sub_zero, abs_zero], - apply add_invs_nonneg - end +theorem s_neg_cancel (s : seq) (H : regular s) : sadd (sneg s) s ≡ zero := + begin + rewrite [↑sadd, ↑sneg, ↑regular at H, ↑zero, ↑equiv], + intros, + rewrite [neg_add_eq_sub, rat.sub_self, rat.sub_zero, abs_zero], + apply add_invs_nonneg + end theorem neg_s_cancel (s : seq) (H : regular s) : sadd s (sneg s) ≡ zero := begin @@ -583,6 +630,7 @@ theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : apply Etv end +set_option tactic.goal_names false theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ := begin @@ -600,7 +648,8 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : apply rat.le.trans, apply rat.mul_le_mul_of_nonneg_right, apply pceil_helper Hn, - repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos), + repeat (apply rat.mul_pos | apply rat.add_pos | apply rat_of_pnat_is_pos | apply inv_pos), + --repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos), apply rat.le_of_lt, apply rat.add_pos, apply rat.mul_pos, @@ -609,15 +658,15 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : repeat apply inv_pos, apply rat.mul_pos, apply rat.add_pos, - repeat apply inv_pos, + apply inv_pos,apply inv_pos, -- repeat apply inv_pos, apply rat_of_pnat_is_pos, have H : (rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≠ 0, begin apply rat.ne_of_gt, - repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos) + repeat (apply rat.mul_pos | apply rat.add_pos | apply rat_of_pnat_is_pos | apply inv_pos), end, rewrite (rat.div_helper H), apply rat.le.refl - end, + end, apply rat.add_le_add, rewrite [-rat.mul_sub_left_distrib, abs_mul], apply rat.le.trans, @@ -648,7 +697,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : apply rat.le_of_lt, apply rat.mul_pos, apply rat.add_pos, - repeat apply inv_pos, + apply inv_pos,apply inv_pos, -- repeat apply inv_pos, apply rat_of_pnat_is_pos, apply rat.le_of_lt, apply inv_pos @@ -733,7 +782,11 @@ theorem mul_neg_equiv_neg_mul {s t : seq} : smul s (sneg t) ≡ sneg (smul s t) theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (H : sadd s (sneg t) ≡ zero) : s ≡ t := begin - have hsimp : ∀ a b c d e : ℚ, a + b + c + (d + e) = (b + d) + a + e + c, from sorry, + have hsimp : ∀ a b c d e : ℚ, a + b + c + (d + e) = b + d + a + e + c, from + λ a b c d e, calc + a + b + c + (d + e) = a + b + (d + e) + c : rat.add.right_comm + ... = a + (b + d) + e + c : by rewrite[-*rat.add.assoc] + ... = b + d + a + e + c : rat.add.comm, apply eq_of_bdd Hs Ht, intros, let He := bdd_of_eq H, diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index caf1b661d..4df79a9ea 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -22,8 +22,8 @@ open eq.ops open pnat -local notation 2 := pnat.pos (nat.of_num 2) dec_trivial -local notation 3 := pnat.pos (nat.of_num 3) dec_trivial +local notation 2 := subtype.tag (nat.of_num 2) dec_trivial +local notation 3 := subtype.tag (nat.of_num 3) dec_trivial namespace s @@ -206,11 +206,15 @@ theorem sub_consts (a b : ℚ) : const a + -const b = const (a - b) := !add_cons theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := by rewrite [add_consts, pnat.add_halves]-/ -theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ := sorry +theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ := + assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial, + by rewrite[*inv_mul_eq_mul_inv,-*rat.right_distrib,T,rat.one_mul] -theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) := sorry +theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) := + by rewrite[-sub_add_eq_sub_sub_swap,sub_add_cancel] -theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) := sorry +theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) := + by rewrite[*add_sub,*sub_add_cancel] definition rep (x : ℝ) : s.reg_seq := some (quot.exists_rep x) diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 08ade03ee..f8afcdb4f 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -16,14 +16,15 @@ open eq.ops pnat local notation 0 := rat.of_num 0 local notation 1 := rat.of_num 1 -local notation 2 := pnat.pos (nat.of_num 2) dec_trivial +local notation 2 := subtype.tag (nat.of_num 2) dec_trivial namespace s ----------------------------- -- helper lemmas -theorem neg_add_rewrite {a b : ℚ} : a + -b = -(b + -a) := sorry +theorem neg_add_rewrite {a b : ℚ} : a + -b = -(b + -a) := + by rewrite[neg_add_rev,neg_neg] theorem abs_abs_sub_abs_le_abs_sub (a b : ℚ) : abs (abs a - abs b) ≤ abs (a - b) := begin @@ -38,10 +39,6 @@ theorem abs_abs_sub_abs_le_abs_sub (a b : ℚ) : abs (abs a - abs b) ≤ abs (a apply trivial end --- does this not exist already?? -theorem forall_of_not_exists {A : Type} {P : A → Prop} (H : ¬ ∃ a : A, P a) : ∀ a : A, ¬ P a := - take a, assume Ha, H (exists.intro a Ha) - theorem and_of_not_or {a b : Prop} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b := and.intro (assume H', H (or.inl H')) (assume H', H (or.inr H')) @@ -517,7 +514,7 @@ theorem s_le_total {s t : seq} (Hs : regular s) (Ht : regular t) : s_le s t ∨ theorem s_le_of_not_lt {s t : seq} (Hle : ¬ s_lt s t) : s_le t s := begin rewrite [↑s_le, ↑nonneg, ↑s_lt at Hle, ↑pos at Hle], - let Hle' := forall_of_not_exists Hle, + let Hle' := iff.mp forall_iff_not_exists Hle, intro n, let Hn := neg_le_neg (rat.le_of_not_gt (Hle' n)), rewrite [↑sadd, ↑sneg, neg_add_rewrite], diff --git a/library/data/real/order.lean b/library/data/real/order.lean index b8ef6bc9a..6a37bc582 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -17,7 +17,7 @@ open -[coercions] nat open eq eq.ops pnat local notation 0 := rat.of_num 0 local notation 1 := rat.of_num 1 -notation 2 := pnat.pos (of_num 2) dec_trivial +notation 2 := subtype.tag (of_num 2) dec_trivial ---------------------------------------------------------------------------------------------------- @@ -43,11 +43,21 @@ theorem sep_by_inv {a b : ℚ} (H : a > b) : ∃ N : ℕ+, a > (b + N⁻¹ + N apply and.right Hc) end -theorem helper_1 {a : ℚ} (H : a > 0) : -a + -a ≤ -a := sorry +theorem helper_1 {a : ℚ} (H : a > 0) : -a + -a ≤ -a := + !neg_add ▸ neg_le_neg (le_add_of_nonneg_left (le_of_lt H)) -theorem rewrite_helper8 (a b c : ℚ) : a - b = c - b + (a - c) := sorry -- simp +theorem rewrite_helper8 (a b c : ℚ) : a - b = c - b + (a - c) := + by rewrite[add_sub,rat.sub_add_cancel] ⬝ !rat.add.comm -theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a := sorry +theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a := + rat.le_of_not_gt (suppose a < 0, + have H2 : 0 < -a, from neg_pos_of_neg this, + (rat.not_lt_of_ge !H) (iff.mp !lt_neg_iff_lt_neg (calc + (pceil (of_num 2 / -a))⁻¹ ≤ -a / of_num 2 + : !inv_pceil_div dec_trivial H2 + ... < -a / 1 + : div_lt_div_of_pos_of_lt_of_pos dec_trivial dec_trivial H2 + ... = -a : div_one))) --------- namespace s diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 72cdc4d2d..e2f4221f8 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -22,18 +22,16 @@ namespace subtype rfl theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 := - eq.subst H3 (take H2, tag_irrelevant H1 H2) H2 + eq.subst H3 (tag_irrelevant H1) H2 - protected theorem 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)) + protected theorem eq : ∀ {a1 a2 : {x | P x}} (H : elt_of a1 = elt_of a2), a1 = a2 + | (tag x1 H1) (tag x2 H2) := tag_eq protected definition is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} := inhabited.mk (tag a H) protected definition has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂) | (tag v₁ p₁) (tag v₂ p₂) := - match H v₁ v₂ with - | inl veq := begin left, substvars end - | inr vne := begin right, intro h, injection h, contradiction end - end + decidable_of_decidable_of_iff (H v₁ v₂) + (iff.intro tag_eq (λh, subtype.no_confusion h (λa b, a))) end subtype diff --git a/library/init/logic.lean b/library/init/logic.lean index 3a9851636..9cef322f9 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -57,8 +57,11 @@ namespace eq theorem trans (H₁ : a = b) (H₂ : b = c) : a = c := subst H₂ H₁ - theorem symm (H : a = b) : b = a := - eq.rec (refl a) H + theorem symm : a = b → b = a := + eq.rec (refl a) + + theorem substr {P : A → Prop} (H₁ : b = a) : P a → P b := + subst (symm H₁) namespace ops notation H `⁻¹` := symm H --input with \sy or \-1 or \inv @@ -74,8 +77,8 @@ eq.subst H₁ (eq.subst H₂ rfl) theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a := eq.subst H (eq.refl (f a)) -theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) (H : a₁ = a₂) : f a₁ = f a₂ := -congr rfl H +theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂ := +congr rfl section variables {A : Type} {a b c: A} @@ -114,25 +117,17 @@ namespace ne variable {A : Type} variables {a b : A} - theorem intro : (a = b → false) → a ≠ b := - assume H, H + theorem intro (H : a = b → false) : a ≠ b := H - theorem elim : a ≠ b → a = b → false := - assume H₁ H₂, H₁ H₂ + theorem elim (H : a ≠ b) : a = b → false := H - theorem irrefl : a ≠ a → false := - assume H, H rfl + theorem irrefl (H : a ≠ a) : false := H rfl - theorem symm : a ≠ b → b ≠ a := - assume (H : a ≠ b) (H₁ : b = a), H (H₁⁻¹) + theorem symm (H : a ≠ b) : b ≠ a := + assume (H₁ : b = a), H (H₁⁻¹) end ne -section - variables {A : Type} {a : A} - - theorem false.of_ne : a ≠ a → false := - assume H, H rfl -end +theorem false.of_ne {A : Type} {a : A} : a ≠ a → false := ne.irrefl infixl `==`:50 := heq @@ -141,15 +136,15 @@ namespace heq variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C} theorem to_eq (H : a == a') : a = a' := - have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from - λ Ht, eq.refl (eq.rec_on Ht a), - heq.rec_on H H₁ (eq.refl A) + have H₁ : ∀ (Ht : A = A), eq.rec a Ht = a, from + λ Ht, eq.refl a, + heq.rec H₁ H (eq.refl A) - theorem elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b := - eq.rec_on (to_eq H₁) H₂ + theorem elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) + : P a → P b := eq.rec_on (to_eq H₁) - theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b := - heq.rec_on H₁ H₂ + theorem subst {P : ∀T : Type, T → Prop} : a == b → P A a → P B b := + heq.rec_on theorem symm (H : a == b) : b == a := heq.rec_on H (refl a) @@ -235,19 +230,15 @@ notation a <-> b := iff a b notation a ↔ b := iff a b namespace iff - theorem intro (H₁ : a → b) (H₂ : b → a) : a ↔ b := - and.intro H₁ H₂ + theorem intro : (a → b) → (b → a) → (a ↔ b) := and.intro - theorem elim (H₁ : (a → b) → (b → a) → c) (H₂ : a ↔ b) : c := - and.rec H₁ H₂ + theorem elim : ((a → b) → (b → a) → c) → (a ↔ b) → c := and.rec - theorem elim_left (H : a ↔ b) : a → b := - elim (assume H₁ H₂, H₁) H + theorem elim_left : (a ↔ b) → a → b := and.left definition mp := @elim_left - theorem elim_right (H : a ↔ b) : b → a := - elim (assume H₁ H₂, H₂) H + theorem elim_right : (a ↔ b) → b → a := and.right definition mpr := @elim_right @@ -259,29 +250,29 @@ namespace iff theorem trans (H₁ : a ↔ b) (H₂ : b ↔ c) : a ↔ c := intro - (assume Ha, elim_left H₂ (elim_left H₁ Ha)) - (assume Hc, elim_right H₁ (elim_right H₂ Hc)) + (assume Ha, mp H₂ (mp H₁ Ha)) + (assume Hc, mpr H₁ (mpr H₂ Hc)) theorem symm (H : a ↔ b) : b ↔ a := - intro - (assume Hb, elim_right H Hb) - (assume Ha, elim_left H Ha) + intro (elim_right H) (elim_left H) + + theorem comm : (a ↔ b) ↔ (b ↔ a) := + intro symm symm open eq.ops theorem of_eq {a b : Prop} (H : a = b) : a ↔ b := - iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) + H ▸ rfl end iff theorem not_iff_not_of_iff (H₁ : a ↔ b) : ¬a ↔ ¬b := iff.intro - (assume (Hna : ¬ a) (Hb : b), absurd (iff.elim_right H₁ Hb) Hna) - (assume (Hnb : ¬ b) (Ha : a), absurd (iff.elim_left H₁ Ha) Hnb) + (assume (Hna : ¬ a) (Hb : b), Hna (iff.elim_right H₁ Hb)) + (assume (Hnb : ¬ b) (Ha : a), Hnb (iff.elim_left H₁ Ha)) theorem of_iff_true (H : a ↔ true) : a := iff.mp (iff.symm H) trivial -theorem not_of_iff_false (H : a ↔ false) : ¬a := -assume Ha : a, iff.mp H Ha +theorem not_of_iff_false : (a ↔ false) → ¬a := iff.mp theorem iff_true_intro (H : a) : a ↔ true := iff.intro @@ -289,16 +280,12 @@ iff.intro (λ Hr, H) theorem iff_false_intro (H : ¬a) : a ↔ false := -iff.intro - (λ Hl, absurd Hl H) - (λ Hr, false.rec _ Hr) +iff.intro H !false.rec theorem not_non_contradictory_iff_absurd (a : Prop) : ¬¬¬a ↔ ¬a := iff.intro - (assume Hl : ¬¬¬a, - assume Ha : a, absurd (non_contradictory_intro Ha) Hl) - (assume Hr : ¬a, - assume Hnna : ¬¬a, absurd Hr Hnna) + (λ (Hl : ¬¬¬a) (Ha : a), Hl (non_contradictory_intro Ha)) + absurd attribute iff.refl [refl] attribute iff.symm [symm] @@ -312,7 +299,8 @@ definition exists.intro := @Exists.intro notation `exists` binders `,` r:(scoped P, Exists P) := r notation `∃` binders `,` r:(scoped P, Exists P) := r -theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B := +theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} + (H1 : ∃x, p x) (H2 : ∀ (a : A), p a → B) : B := Exists.rec H2 H1 /- decidable -/ @@ -327,6 +315,16 @@ decidable.inl trivial definition decidable_false [instance] : decidable false := decidable.inr not_false +-- We use "dependent" if-then-else to be able to communicate the if-then-else condition +-- to the branches +definition dite (c : Prop) [H : decidable c] {A : Type} : (c → A) → (¬ c → A) → A := +decidable.rec_on H + +/- if-then-else -/ + +definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A := +decidable.rec_on H (λ Hc, t) (λ Hnc, e) + namespace decidable variables {p q : Prop} @@ -338,37 +336,29 @@ namespace decidable : decidable.rec_on H H1 H2 := decidable.rec_on H (λh, false.rec _ (H3 h)) (λh, H4) - definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q := - decidable.rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp) + definition by_cases {q : Type} [C : decidable p] : (p → q) → (¬p → q) → q := !dite - theorem em (p : Prop) [H : decidable p] : p ∨ ¬p := - by_cases (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp) + theorem em (p : Prop) [H : decidable p] : p ∨ ¬p := by_cases or.inl or.inr theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p := - by_cases - (assume H1 : p, H1) - (assume H1 : ¬p, false.rec _ (H H1)) + if H1 : p then H1 else false.rec _ (H H1) end decidable section variables {p q : Prop} open decidable definition decidable_of_decidable_of_iff (Hp : decidable p) (H : p ↔ q) : decidable q := - decidable.rec_on Hp - (assume Hp : p, inl (iff.elim_left H Hp)) - (assume Hnp : ¬p, inr (iff.elim_left (not_iff_not_of_iff H) Hnp)) + if Hp : p then inl (iff.mp H Hp) + else inr (iff.mp (not_iff_not_of_iff H) Hp) definition decidable_of_decidable_of_eq (Hp : decidable p) (H : p = q) : decidable q := decidable_of_decidable_of_iff Hp (iff.of_eq H) protected definition or.by_cases [Hp : decidable p] [Hq : decidable q] {A : Type} - : p ∨ q → (p → A) → (q → A) → A := - assume h h₁ h₂, by_cases - (λ hp : p, h₁ hp) - (λ hnp : ¬p, - by_cases - (λ hq : q, h₂ hq) - (λ hnq : ¬q, absurd h (λ n, or.elim h hnp hnq))) + (h : p ∨ q) (h₁ : p → A) (h₂ : q → A) : A := + if hp : p then h₁ hp else + if hq : q then h₂ hq else + false.rec _ (or.elim h hp hq) end section @@ -376,41 +366,35 @@ section open decidable (rec_on inl inr) definition decidable_and [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∧ q) := - rec_on Hp - (assume Hp : p, rec_on Hq - (assume Hq : q, inl (and.intro Hp Hq)) - (assume Hnq : ¬q, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hq Hnq)))) - (assume Hnp : ¬p, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hp Hnp))) + if hp : p then + if hq : q then inl (and.intro hp hq) + else inr (assume H : p ∧ q, hq (and.right H)) + else inr (assume H : p ∧ q, hp (and.left H)) definition decidable_or [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∨ q) := - rec_on Hp - (assume Hp : p, inl (or.inl Hp)) - (assume Hnp : ¬p, rec_on Hq - (assume Hq : q, inl (or.inr Hq)) - (assume Hnq : ¬q, inr (assume H : p ∨ q, or.elim H (assume Hp, absurd Hp Hnp) (assume Hq, absurd Hq Hnq)))) + if hp : p then inl (or.inl hp) else + if hq : q then inl (or.inr hq) else + inr (or.rec hp hq) definition decidable_not [instance] [Hp : decidable p] : decidable (¬p) := - rec_on Hp - (assume Hp, inr (λ Hnp, absurd Hp Hnp)) - (assume Hnp, inl Hnp) + if hp : p then inr (absurd hp) else inl hp definition decidable_implies [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p → q) := - rec_on Hp - (assume Hp : p, rec_on Hq - (assume Hq : q, inl (assume H, Hq)) - (assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq))) - (assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp)) + if hp : p then + if hq : q then inl (assume H, hq) + else inr (assume H : p → q, absurd (H hp) hq) + else inl (assume Hp, absurd Hp hp) definition decidable_iff [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ↔ q) := - show decidable ((p → q) ∧ (q → p)), from _ + decidable_and end definition decidable_pred [reducible] {A : Type} (R : A → Prop) := Π (a : A), decidable (R a) definition decidable_rel [reducible] {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b) definition decidable_eq [reducible] (A : Type) := decidable_rel (@eq A) -definition decidable_ne [instance] {A : Type} [H : decidable_eq A] : Π (a b : A), decidable (a ≠ b) := -show Π x y : A, decidable (x = y → false), from _ +definition decidable_ne [instance] {A : Type} [H : decidable_eq A] (a b : A) : decidable (a ≠ b) := +decidable_implies namespace bool theorem ff_ne_tt : ff = tt → false @@ -429,9 +413,8 @@ protected definition bool.has_decidable_eq [instance] : ∀a b : bool, decidable | tt tt := inl rfl definition decidable_eq_of_bool_pred {A : Type} {p : A → A → bool} (H₁ : is_dec_eq p) (H₂ : is_dec_refl p) : decidable_eq A := -take x y : A, by_cases - (assume Hp : p x y = tt, inl (H₁ Hp)) - (assume Hn : ¬ p x y = tt, inr (assume Hxy : x = y, absurd (H₂ y) (eq.rec_on Hxy Hn))) +take x y : A, if Hp : p x y = tt then inl (H₁ Hp) + else inr (assume Hxy : x = y, (eq.subst Hxy Hp) (H₂ y)) theorem decidable_eq_inl_refl {A : Type} [H : decidable_eq A] (a : A) : H a a = inl (eq.refl a) := match H a a with @@ -452,17 +435,17 @@ end inductive inhabited [class] (A : Type) : Type := mk : A → inhabited A -protected definition inhabited.value {A : Type} (h : inhabited A) : A := -inhabited.rec (λa, a) h +protected definition inhabited.value {A : Type} : inhabited A → A := +inhabited.rec (λa, a) protected definition inhabited.destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B := inhabited.rec H2 H1 definition default (A : Type) [H : inhabited A] : A := -inhabited.rec (λa, a) H +inhabited.value H definition arbitrary [irreducible] (A : Type) [H : inhabited A] : A := -inhabited.rec (λa, a) H +inhabited.value H definition Prop.is_inhabited [instance] : inhabited Prop := inhabited.mk true @@ -472,7 +455,7 @@ inhabited.rec_on H (λb, inhabited.mk (λa, b)) definition inhabited_Pi [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] : inhabited (Πx, B x) := -inhabited.mk (λa, inhabited.rec_on (H a) (λb, b)) +inhabited.mk (λa, !default) protected definition bool.is_inhabited [instance] : inhabited bool := inhabited.mk ff @@ -484,7 +467,7 @@ protected definition nonempty.elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : nonempty.rec H2 H1 theorem nonempty_of_inhabited [instance] {A : Type} [H : inhabited A] : nonempty A := -nonempty.intro (default A) +nonempty.intro !default /- subsingleton -/ @@ -492,7 +475,7 @@ inductive subsingleton [class] (A : Type) : Prop := intro : (∀ a b : A, a = b) → subsingleton A protected definition subsingleton.elim {A : Type} [H : subsingleton A] : ∀(a b : A), a = b := -subsingleton.rec (fun p, p) H +subsingleton.rec (λp, p) H definition subsingleton_prop [instance] (p : Prop) : subsingleton p := subsingleton.intro (λa b, !proof_irrel) @@ -518,104 +501,90 @@ protected theorem rec_subsingleton {p : Prop} [H : decidable p] : subsingleton (decidable.rec_on H H1 H2) := decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases" -/- if-then-else -/ - -definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A := -decidable.rec_on H (λ Hc, t) (λ Hnc, e) - -theorem if_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t := +theorem if_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (ite c t e) = t := decidable.rec (λ Hc : c, eq.refl (@ite c (decidable.inl Hc) A t e)) (λ Hnc : ¬c, absurd Hc Hnc) H -theorem if_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e := +theorem if_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t e : A} : (ite c t e) = e := decidable.rec (λ Hc : c, absurd Hc Hnc) (λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t e)) H -theorem if_t_t [simp] (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t := +theorem if_t_t [simp] (c : Prop) [H : decidable c] {A : Type} (t : A) : (ite c t t) = t := decidable.rec (λ Hc : c, eq.refl (@ite c (decidable.inl Hc) A t t)) (λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t t)) H -theorem implies_of_if_pos {c t e : Prop} [H : decidable c] (h : if c then t else e) : c → t := +theorem implies_of_if_pos {c t e : Prop} [H : decidable c] (h : ite c t e) : c → t := assume Hc, eq.rec_on (if_pos Hc) h -theorem implies_of_if_neg {c t e : Prop} [H : decidable c] (h : if c then t else e) : ¬c → e := +theorem implies_of_if_neg {c t e : Prop} [H : decidable c] (h : ite c t e) : ¬c → e := assume Hnc, eq.rec_on (if_neg Hnc) h theorem if_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : A} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) : - (if b then x else y) = (if c then u else v) := + ite b x y = ite c u v := decidable.rec_on dec_b (λ hp : b, calc - (if b then x else y) - = x : if_pos hp - ... = u : h_t (iff.mp h_c hp) - ... = (if c then u else v) : if_pos (iff.mp h_c hp)) + ite b x y = x : if_pos hp + ... = u : h_t (iff.mp h_c hp) + ... = ite c u v : if_pos (iff.mp h_c hp)) (λ hn : ¬b, calc - (if b then x else y) - = y : if_neg hn - ... = v : h_e (iff.mp (not_iff_not_of_iff h_c) hn) - ... = (if c then u else v) : if_neg (iff.mp (not_iff_not_of_iff h_c) hn)) + ite b x y = y : if_neg hn + ... = v : h_e (iff.mp (not_iff_not_of_iff h_c) hn) + ... = ite c u v : if_neg (iff.mp (not_iff_not_of_iff h_c) hn)) theorem if_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) : - (if b then x else y) = (if c then u else v) := + ite b x y = ite c u v := @if_ctx_congr A b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e) theorem if_ctx_simp_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) : - (if b then x else y) = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) := + ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) := @if_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e theorem if_simp_congr [congr] {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) : - (if b then x else y) = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) := + ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) := @if_ctx_simp_congr A b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e) theorem if_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c] (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) : - if b then x else y ↔ if c then u else v := + ite b x y ↔ ite c u v := decidable.rec_on dec_b (λ hp : b, calc - (if b then x else y) - ↔ x : iff.of_eq (if_pos hp) - ... ↔ u : h_t (iff.mp h_c hp) - ... ↔ (if c then u else v) : iff.of_eq (if_pos (iff.mp h_c hp))) + ite b x y ↔ x : iff.of_eq (if_pos hp) + ... ↔ u : h_t (iff.mp h_c hp) + ... ↔ ite c u v : iff.of_eq (if_pos (iff.mp h_c hp))) (λ hn : ¬b, calc - (if b then x else y) - ↔ y : iff.of_eq (if_neg hn) - ... ↔ v : h_e (iff.mp (not_iff_not_of_iff h_c) hn) - ... ↔ (if c then u else v) : iff.of_eq (if_neg (iff.mp (not_iff_not_of_iff h_c) hn))) + ite b x y ↔ y : iff.of_eq (if_neg hn) + ... ↔ v : h_e (iff.mp (not_iff_not_of_iff h_c) hn) + ... ↔ ite c u v : iff.of_eq (if_neg (iff.mp (not_iff_not_of_iff h_c) hn))) theorem if_ctx_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b] (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) : - if b then x else y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) := + ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) := @if_congr_prop b c x y u v dec_b (decidable_of_decidable_of_iff dec_b h_c) h_c h_t h_e theorem if_simp_congr_prop [congr] {b c x y u v : Prop} [dec_b : decidable b] (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) : - if b then x else y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) := + ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) := @if_ctx_simp_congr_prop b c x y u v dec_b h_c (λ h, h_t) (λ h, h_e) --- We use "dependent" if-then-else to be able to communicate the if-then-else condition --- to the branches -definition dite (c : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A := -decidable.rec_on H (λ Hc, t Hc) (λ Hnc, e Hnc) - -theorem dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = t Hc := +theorem dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : dite c t e = t Hc := decidable.rec (λ Hc : c, eq.refl (@dite c (decidable.inl Hc) A t e)) (λ Hnc : ¬c, absurd Hc Hnc) H -theorem dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = e Hnc := +theorem dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : dite c t e = e Hnc := decidable.rec (λ Hc : c, absurd Hc Hnc) (λ Hnc : ¬c, eq.refl (@dite c (decidable.inr Hnc) A t e)) @@ -629,19 +598,15 @@ theorem dif_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : dec (@dite b dec_b A x y) = (@dite c dec_c A u v) := decidable.rec_on dec_b (λ hp : b, calc - (if h : b then x h else y h) - = x hp : dif_pos hp - ... = x (iff.mpr h_c (iff.mp h_c hp)) : proof_irrel - ... = u (iff.mp h_c hp) : h_t - ... = (if h : c then u h else v h) : dif_pos (iff.mp h_c hp)) - (λ hn : ¬b, - let h_nc : ¬b ↔ ¬c := not_iff_not_of_iff h_c in - calc - (if h : b then x h else y h) - = y hn : dif_neg hn - ... = y (iff.mpr h_nc (iff.mp h_nc hn)) : proof_irrel - ... = v (iff.mp h_nc hn) : h_e - ... = (if h : c then u h else v h) : dif_neg (iff.mp h_nc hn)) + dite b x y = x hp : dif_pos hp + ... = x (iff.mpr h_c (iff.mp h_c hp)) : proof_irrel + ... = u (iff.mp h_c hp) : h_t + ... = dite c u v : dif_pos (iff.mp h_c hp)) + (λ hn : ¬b, let h_nc : ¬b ↔ ¬c := not_iff_not_of_iff h_c in calc + dite b x y = y hn : dif_neg hn + ... = y (iff.mpr h_nc (iff.mp h_nc hn)) : proof_irrel + ... = v (iff.mp h_nc hn) : h_e + ... = dite c u v : dif_neg (iff.mp h_nc hn)) theorem dif_ctx_simp_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A} @@ -667,13 +632,13 @@ decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, !false.rec (if_neg Hnc ▸ H₂)) notation `dec_trivial` := of_is_true trivial theorem not_of_not_is_true {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_true c) : ¬ c := -decidable.rec_on H₁ (λ Hc, absurd true.intro (if_pos Hc ▸ H₂)) (λ Hnc, Hnc) +if Hc : c then absurd trivial (if_pos Hc ▸ H₂) else Hc theorem not_of_is_false {c : Prop} [H₁ : decidable c] (H₂ : is_false c) : ¬ c := -decidable.rec_on H₁ (λ Hc, !false.rec (if_pos Hc ▸ H₂)) (λ Hnc, Hnc) +if Hc : c then !false.rec (if_pos Hc ▸ H₂) else Hc theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c := -decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, absurd true.intro (if_neg Hnc ▸ H₂)) +if Hc : c then Hc else absurd trivial (if_neg Hc ▸ H₂) -- namespace used to collect congruence rules for "contextual simplification" namespace contextual diff --git a/library/init/measurable.lean b/library/init/measurable.lean index 97dab5094..017f2ad36 100644 --- a/library/init/measurable.lean +++ b/library/init/measurable.lean @@ -12,14 +12,14 @@ open nat inductive measurable [class] (A : Type) := mk : (A → nat) → measurable A -definition size_of {A : Type} [s : measurable A] (a : A) : nat := -measurable.rec_on s (λ f, f) a +definition size_of {A : Type} [s : measurable A] : A → nat := +measurable.rec_on s (λ f, f) definition nat.measurable [instance] : measurable nat := measurable.mk (λ a, a) definition option.measurable [instance] (A : Type) [s : measurable A] : measurable (option A) := -measurable.mk (λ a, option.cases_on a zero (λ a, size_of a)) +measurable.mk (λ a, option.cases_on a zero size_of) definition prod.measurable [instance] (A B : Type) [sa : measurable A] [sb : measurable B] : measurable (prod A B) := measurable.mk (λ p, prod.cases_on p (λ a b, size_of a + size_of b)) diff --git a/library/init/nat.lean b/library/init/nat.lean index 851ceea0b..33d02f251 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -31,7 +31,7 @@ namespace nat -- add is defined in init.num definition sub (a b : nat) : nat := - nat.rec_on b a (λ b₁ r, pred r) + nat.rec_on b a (λ b₁, pred) definition mul (a b : nat) : nat := nat.rec_on b zero (λ b₁ r, r + a) @@ -56,11 +56,11 @@ namespace nat /- properties of inequality -/ - theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n + theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !le.refl - theorem le_succ (n : ℕ) : n ≤ succ n := by repeat constructor + theorem le_succ (n : ℕ) : n ≤ succ n := le.step !le.refl - theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor) + theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;repeat constructor theorem le_succ_iff_true [simp] (n : ℕ) : n ≤ succ n ↔ true := iff_true_intro (le_succ n) @@ -68,8 +68,8 @@ namespace nat theorem pred_le_iff_true [simp] (n : ℕ) : pred n ≤ n ↔ true := iff_true_intro (pred_le n) - theorem le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := - by induction H2 with n H2 IH;exact H1;exact le.step IH + theorem le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k := + le.rec H1 (λp H2, le.step) theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ @@ -77,62 +77,51 @@ namespace nat theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H - theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := - by induction H;reflexivity;exact le.step v_0 + theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m := + le.rec !le.refl (λa b, le.step) - theorem pred_le_pred {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := - by induction H;reflexivity;cases b;exact v_0;exact le.step v_0 + theorem pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m := + le.rec !le.refl (nat.rec (λa b, b) (λa b c, le.step)) - theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := - pred_le_pred H + theorem le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m := + pred_le_pred - theorem le_succ_of_pred_le {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m := - by cases n;exact le.step H;exact succ_le_succ H - - theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n := - by induction n with n IH;all_goals intros;cases a;apply IH;exact le_of_succ_le_succ a - - theorem succ_le_self_iff_false [simp] (n : ℕ) : succ n ≤ n ↔ false := - iff_false_intro not_succ_le_self - - theorem zero_le (n : ℕ) : 0 ≤ n := - by induction n with n IH;apply le.refl;exact le.step IH - - theorem zero_le_iff_true [simp] (n : ℕ) : 0 ≤ n ↔ true := - iff_true_intro (zero_le n) - - theorem lt.step {n m : ℕ} (H : n < m) : n < succ m := - le.step H - - theorem zero_lt_succ (n : ℕ) : 0 < succ n := - by induction n with n IH;apply le.refl;exact le.step IH - - theorem zero_lt_succ_iff_true [simp] (n : ℕ) : 0 < succ n ↔ true := - iff_true_intro (zero_lt_succ n) - - theorem lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k := - le.trans (le.step H1) H2 - - theorem lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k := - le.trans (succ_le_succ H1) H2 - - theorem lt_of_lt_of_le [trans] {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k := - le.trans H1 H2 - - theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m := - begin - cases H1 with m' H1', - { reflexivity}, - { cases H2 with n' H2', - { reflexivity}, - { exfalso, apply not_succ_le_self, exact lt.trans H1' H2'}}, - end + theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m := + nat.cases_on n le.step (λa, succ_le_succ) theorem not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero := by intro H; cases H theorem succ_le_zero_iff_false (n : ℕ) : succ n ≤ zero ↔ false := - iff_false_intro (not_succ_le_zero n) + iff_false_intro !not_succ_le_zero + + theorem not_succ_le_self : Π {n : ℕ}, ¬succ n ≤ n := + nat.rec !not_succ_le_zero (λa b c, b (le_of_succ_le_succ c)) + + theorem succ_le_self_iff_false [simp] (n : ℕ) : succ n ≤ n ↔ false := + iff_false_intro not_succ_le_self + + theorem zero_le : ∀ (n : ℕ), 0 ≤ n := + nat.rec !le.refl (λa, le.step) + + theorem zero_le_iff_true [simp] (n : ℕ) : 0 ≤ n ↔ true := + iff_true_intro !zero_le + + theorem lt.step {n m : ℕ} : n < m → n < succ m := le.step + + theorem zero_lt_succ (n : ℕ) : 0 < succ n := + succ_le_succ !zero_le + + theorem zero_lt_succ_iff_true [simp] (n : ℕ) : 0 < succ n ↔ true := + iff_true_intro (zero_lt_succ n) + + theorem lt.trans [trans] {n m k : ℕ} (H1 : n < m) : m < k → n < k := + le.trans (le.step H1) + + theorem lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k := + le.trans (succ_le_succ H1) + + theorem lt_of_lt_of_le [trans] {n m k : ℕ} : n < m → m ≤ k → n < k := le.trans theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self @@ -149,143 +138,112 @@ namespace nat theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : false := !lt.irrefl (lt_of_le_of_lt H1 H2) + theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) : m ≤ n → n = m := + le.cases_on H1 (λa, rfl) (λa b c, absurd (lt_of_le_of_lt b c) !lt.irrefl) + theorem lt_le_antisymm {n m : ℕ} (H1 : n < m) (H2 : m ≤ n) : false := le_lt_antisymm H2 H1 - theorem lt.asymm {n m : ℕ} (H1 : n < m) (H2 : m < n) : false := - le_lt_antisymm (le_of_lt H1) H2 + theorem lt.asymm {n m : ℕ} (H1 : n < m) : ¬ m < n := + le_lt_antisymm (le_of_lt H1) - definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := - begin - revert b H1 H2 H3, induction a with a IH, - { intros, cases b, - exact H2 rfl, - exact H1 !zero_lt_succ}, - { intros, cases b with b, - exact H3 !zero_lt_succ, - { apply IH, - intro H, exact H1 (succ_le_succ H), - intro H, exact H2 (congr rfl H), - intro H, exact H3 (succ_le_succ H)}} - end - - theorem lt.trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a := - lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H)) - - theorem lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := - lt.by_cases H1 (λH, H2 (le_of_eq H⁻¹)) (λH, H2 (le_of_lt H)) - - theorem lt_or_ge (a b : ℕ) : (a < b) ∨ (a ≥ b) := - lt_ge_by_cases inl inr - - theorem not_lt_zero (a : ℕ) : ¬ a < zero := - by intro H; cases H + theorem not_lt_zero (a : ℕ) : ¬ a < zero := !not_succ_le_zero theorem lt_zero_iff_false [simp] (a : ℕ) : a < zero ↔ false := iff_false_intro (not_lt_zero a) + theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b := + le.cases_on H (inl rfl) (λn h, inr (succ_le_succ h)) + + theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b := + or.elim H !le_of_eq !le_of_lt + -- less-than is well-founded definition lt.wf [instance] : well_founded lt := - begin - constructor, intro n, induction n with n IH, - { constructor, intros n H, exfalso, exact !not_lt_zero H}, - { constructor, intros m H, - assert aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, - { intros n₁ hlt, induction hlt, - { intro p, injection p with q, exact q ▸ IH}, - { intro p, injection p with q, exact (acc.inv (q ▸ IH) a)}}, - apply aux H rfl}, - end + well_founded.intro (nat.rec + (!acc.intro (λn H, absurd H (not_lt_zero n))) + (λn IH, !acc.intro (λm H, + elim (eq_or_lt_of_le (le_of_succ_le_succ H)) + (λe, eq.substr e IH) (acc.inv IH)))) - definition measure {A : Type} (f : A → ℕ) : A → A → Prop := - inv_image lt f + definition measure {A : Type} : (A → ℕ) → A → A → Prop := + inv_image lt definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) := inv_image.wf f lt.wf - theorem succ_lt_succ {a b : ℕ} (H : a < b) : succ a < succ b := - succ_le_succ H + theorem succ_lt_succ {a b : ℕ} : a < b → succ a < succ b := + succ_le_succ - theorem lt_of_succ_lt {a b : ℕ} (H : succ a < b) : a < b := - le_of_succ_le H + theorem lt_of_succ_lt {a b : ℕ} : succ a < b → a < b := + le_of_succ_le - theorem lt_of_succ_lt_succ {a b : ℕ} (H : succ a < succ b) : a < b := - le_of_succ_le_succ H + theorem lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b := + le_of_succ_le_succ definition decidable_le [instance] : decidable_rel le := - begin - intros n, induction n with n IH, - { intro m, left, apply zero_le}, - { intro m, cases m with m, - { right, apply not_succ_le_zero}, - { let H := IH m, clear IH, - cases H with H H, - left, exact succ_le_succ H, - right, intro H2, exact H (le_of_succ_le_succ H2)}} - end + nat.rec (λm, (decidable.inl !zero_le)) + (λn IH m, !nat.cases_on (decidable.inr (not_succ_le_zero n)) + (λm, decidable.rec (λH, inl (succ_le_succ H)) + (λH, inr (λa, H (le_of_succ_le_succ a))) (IH m))) definition decidable_lt [instance] : decidable_rel lt := _ definition decidable_gt [instance] : decidable_rel gt := _ definition decidable_ge [instance] : decidable_rel ge := _ - theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b := - by cases H with b' H; exact inl rfl; exact inr (succ_le_succ H) + theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b := + nat.rec (inr !zero_le) (λn, or.rec + (λh, inl (le_succ_of_le h)) + (λh, elim (eq_or_lt_of_le h) (λe, inl (eq.subst e !le.refl)) inr)) b - theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b := - by cases H with H H; exact le_of_eq H; exact le_of_lt H + theorem lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := + by_cases H1 (λh, H2 (elim !lt_or_ge (λa, absurd a h) (λa, a))) + + definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := + lt_ge_by_cases H1 (λh₁, + lt_ge_by_cases H3 (λh₂, H2 (le.antisymm h₂ h₁))) + + theorem lt.trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a := + lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H)) theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a := or.rec_on (lt.trichotomy a b) (λ hlt, absurd hlt hnlt) (λ h, h) - theorem lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b := - succ_le_succ h + theorem lt_succ_of_le {a b : ℕ} : a ≤ b → a < succ b := + succ_le_succ theorem lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h theorem succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h theorem succ_sub_succ_eq_sub [simp] (a b : ℕ) : succ a - succ b = a - b := - by induction b with b IH;reflexivity; apply congr (eq.refl pred) IH + nat.rec rfl (λ b, congr_arg pred) b theorem sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b := - eq.rec_on (succ_sub_succ_eq_sub a b) rfl + eq.symm !succ_sub_succ_eq_sub theorem zero_sub_eq_zero [simp] (a : ℕ) : zero - a = zero := - nat.rec_on a - rfl - (λ a₁ (ih : zero - a₁ = zero), congr (eq.refl pred) ih) + nat.rec rfl (λ a, congr_arg pred) a theorem zero_eq_zero_sub (a : ℕ) : zero = zero - a := - eq.rec_on (zero_sub_eq_zero a) rfl - - theorem sub_lt {a b : ℕ} : zero < a → zero < b → a - b < a := - have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from - λa h₁, le.rec_on h₁ - (λb h₂, le.cases_on h₂ - (lt.base zero) - (λ b₁ bpos, - eq.rec_on (sub_eq_succ_sub_succ zero b₁) - (eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero)))) - (λa₁ apos ih b h₂, le.cases_on h₂ - (lt.base a₁) - (λ b₁ bpos, - eq.rec_on (sub_eq_succ_sub_succ a₁ b₁) - (lt.trans (@ih b₁ bpos) (lt.base a₁)))), - λ h₁ h₂, aux h₁ h₂ + eq.symm !zero_sub_eq_zero theorem sub_le (a b : ℕ) : a - b ≤ a := - nat.rec_on b - (le.refl a) - (λ b₁ ih, le.trans !pred_le ih) + nat.rec_on b !le.refl (λ b₁, le.trans !pred_le) theorem sub_le_iff_true [simp] (a b : ℕ) : a - b ≤ a ↔ true := iff_true_intro (sub_le a b) + theorem sub_lt {a b : ℕ} (H1 : zero < a) (H2 : zero < b) : a - b < a := + !nat.cases_on (λh, absurd h !lt.irrefl) + (λa h, succ_le_succ (!nat.cases_on (λh, absurd h !lt.irrefl) + (λb c, eq.substr !succ_sub_succ_eq_sub !sub_le) H2)) H1 + theorem sub_lt_succ (a b : ℕ) : a - b < succ a := - lt_succ_of_le (sub_le a b) + lt_succ_of_le !sub_le theorem sub_lt_succ_iff_true [simp] (a b : ℕ) : a - b < succ a ↔ true := - iff_true_intro (sub_lt_succ a b) + iff_true_intro !sub_lt_succ end nat diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 7bf7fceb0..2b9599aaf 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -21,80 +21,99 @@ definition imp (a b : Prop) : Prop := a → b theorem mt (H1 : a → b) (H2 : ¬b) : ¬a := assume Ha : a, absurd (H1 Ha) H2 +theorem imp.id (H : a) : a := H + +theorem imp.intro (H : a) (H₂ : b) : a := H + +theorem imp.mp (H : a) (H₂ : a → b) : b := +H₂ H + +theorem imp.syl (H : a → b) (H₂ : c → a) (Hc : c) : b := +H (H₂ Hc) + +theorem imp.left (H : a → b) (H₂ : b → c) (Ha : a) : c := +H₂ (H Ha) + theorem imp_true (a : Prop) : (a → true) ↔ true := -iff.intro (assume H, trivial) (assume H H1, trivial) +iff_true_intro (imp.intro trivial) theorem true_imp (a : Prop) : (true → a) ↔ a := -iff.intro (assume H, H trivial) (assume H H1, H) +iff.intro (assume H, H trivial) imp.intro theorem imp_false (a : Prop) : (a → false) ↔ ¬ a := iff.rfl theorem false_imp (a : Prop) : (false → a) ↔ true := -iff.intro (assume H, trivial) (assume H H1, false.elim H1) +iff_true_intro false.elim theorem imp_iff_imp (H1 : a ↔ c) (H2 : b ↔ d) : (a → b) ↔ (c → d) := iff.intro - (λHab Hc, iff.elim_left H2 (Hab (iff.elim_right H1 Hc))) - (λHcd Ha, iff.elim_right H2 (Hcd (iff.elim_left H1 Ha))) + (λHab Hc, iff.mp H2 (Hab (iff.mpr H1 Hc))) + (λHcd Ha, iff.mpr H2 (Hcd (iff.mp H1 Ha))) /- not -/ -theorem not.elim (H1 : ¬a) (H2 : a) : false := H1 H2 +theorem not.elim {A : Type} (H1 : ¬a) (H2 : a) : A := absurd H2 H1 theorem not.intro (H : a → false) : ¬a := H theorem not_not_intro (Ha : a) : ¬¬a := -assume Hna : ¬a, absurd Ha Hna +assume Hna : ¬a, Hna Ha -theorem not_imp_not_of_imp {a b : Prop} : (a → b) → ¬b → ¬a := -assume Pimp Pnb Pa, absurd (Pimp Pa) Pnb +theorem not.mto {a b : Prop} : (a → b) → ¬b → ¬a := imp.left -theorem not_not_of_not_implies (H : ¬(a → b)) : ¬¬a := -assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H +theorem not_imp_not_of_imp {a b : Prop} : (a → b) → ¬b → ¬a := not.mto -theorem not_of_not_implies (H : ¬(a → b)) : ¬b := -assume Hb : b, absurd (assume Ha : a, Hb) H +theorem not_not_of_not_implies : ¬(a → b) → ¬¬a := +not.mto not.elim + +theorem not_of_not_implies : ¬(a → b) → ¬b := +not.mto imp.intro theorem not_not_em : ¬¬(a ∨ ¬a) := assume not_em : ¬(a ∨ ¬a), -have Hnp : ¬a, from - assume Hp : a, absurd (or.inl Hp) not_em, -absurd (or.inr Hnp) not_em +not_em (or.inr (not.mto or.inl not_em)) theorem not_true [simp] : ¬ true ↔ false := -iff.intro (assume H, H trivial) (assume H, false.elim H) +iff_false_intro (not_not_intro trivial) theorem not_false_iff [simp] : ¬ false ↔ true := -iff.intro (assume H, trivial) (assume H H1, H1) +iff_true_intro not_false theorem not_iff_not (H : a ↔ b) : ¬a ↔ ¬b := -iff.intro - (λHna Hb, Hna (iff.elim_right H Hb)) - (λHnb Ha, Hnb (iff.elim_left H Ha)) +iff.intro (not.mto (iff.mpr H)) (not.mto (iff.mp H)) /- and -/ -definition not_and_of_not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := -assume H : a ∧ b, absurd (and.elim_left H) Hna +definition not_and_of_not_left (b : Prop) : ¬a → ¬(a ∧ b) := +not.mto and.left -definition not_and_of_not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) := -assume H : a ∧ b, absurd (and.elim_right H) Hnb +definition not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b) := +not.mto and.right -theorem and.swap (H : a ∧ b) : b ∧ a := -and.intro (and.elim_right H) (and.elim_left H) +theorem and.swap : a ∧ b → b ∧ a := +and.rec (λHa Hb, and.intro Hb Ha) + +theorem and.imp (H₂ : a → c) (H₃ : b → d) : a ∧ b → c ∧ d := +and.rec (λHa Hb, and.intro (H₂ Ha) (H₃ Hb)) + +theorem and.imp_left (H : a → b) : a ∧ c → b ∧ c := +and.imp H imp.id + +theorem and.imp_right (H : a → b) : c ∧ a → c ∧ b := +and.imp imp.id H theorem and_of_and_of_imp_of_imp (H₁ : a ∧ b) (H₂ : a → c) (H₃ : b → d) : c ∧ d := -and.elim H₁ (assume Ha : a, assume Hb : b, and.intro (H₂ Ha) (H₃ Hb)) +and.imp H₂ H₃ H₁ theorem and_of_and_of_imp_left (H₁ : a ∧ c) (H : a → b) : b ∧ c := -and.elim H₁ (assume Ha : a, assume Hc : c, and.intro (H Ha) Hc) +and.imp_left H H₁ theorem and_of_and_of_imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b := -and.elim H₁ (assume Hc : c, assume Ha : a, and.intro Hc (H Ha)) +and.imp_right H H₁ theorem and.comm [simp] : a ∧ b ↔ b ∧ a := -iff.intro (λH, and.swap H) (λH, and.swap H) +iff.intro and.swap and.swap theorem and.assoc [simp] : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := iff.intro @@ -105,181 +124,158 @@ iff.intro obtain Ha Hb Hc, from H, and.intro (and.intro Ha Hb) Hc) -theorem and_true [simp] (a : Prop) : a ∧ true ↔ a := -iff.intro (assume H, and.left H) (assume H, and.intro H trivial) - -theorem true_and [simp] (a : Prop) : true ∧ a ↔ a := -iff.intro (assume H, and.right H) (assume H, and.intro trivial H) - -theorem and_false [simp] (a : Prop) : a ∧ false ↔ false := -iff.intro (assume H, and.right H) (assume H, false.elim H) - -theorem false_and [simp] (a : Prop) : false ∧ a ↔ false := -iff.intro (assume H, and.left H) (assume H, false.elim H) - -theorem and_self [simp] (a : Prop) : a ∧ a ↔ a := -iff.intro (assume H, and.left H) (assume H, and.intro H H) - -theorem and_imp_eq (a b c : Prop) : (a ∧ b → c) = (a → b → c) := -propext - (iff.intro (λ Pl a b, Pl (and.intro a b)) - (λ Pr Pand, Pr (and.left Pand) (and.right Pand))) - theorem and_iff_right {a b : Prop} (Ha : a) : (a ∧ b) ↔ b := -iff.intro - (assume Hab, and.elim_right Hab) - (assume Hb, and.intro Ha Hb) +iff.intro and.right (and.intro Ha) theorem and_iff_left {a b : Prop} (Hb : b) : (a ∧ b) ↔ a := -iff.intro - (assume Hab, and.elim_left Hab) - (assume Ha, and.intro Ha Hb) +iff.intro and.left (λHa, and.intro Ha Hb) + +theorem and_true [simp] (a : Prop) : a ∧ true ↔ a := +and_iff_left trivial + +theorem true_and [simp] (a : Prop) : true ∧ a ↔ a := +and_iff_right trivial + +theorem and_false [simp] (a : Prop) : a ∧ false ↔ false := +iff_false_intro and.right + +theorem false_and [simp] (a : Prop) : false ∧ a ↔ false := +iff_false_intro and.left + +theorem and_self [simp] (a : Prop) : a ∧ a ↔ a := +iff.intro and.left (assume H, and.intro H H) + +theorem and_imp_iff (a b c : Prop) : (a ∧ b → c) ↔ (a → b → c) := +iff.intro (λH a b, H (and.intro a b)) and.rec + +theorem and_imp_eq (a b c : Prop) : (a ∧ b → c) = (a → b → c) := +propext !and_imp_iff theorem and_iff_and (H1 : a ↔ c) (H2 : b ↔ d) : (a ∧ b) ↔ (c ∧ d) := -iff.intro - (assume Hab, and.intro (iff.elim_left H1 (and.left Hab)) (iff.elim_left H2 (and.right Hab))) - (assume Hcd, and.intro (iff.elim_right H1 (and.left Hcd)) (iff.elim_right H2 (and.right Hcd))) +iff.intro (and.imp (iff.mp H1) (iff.mp H2)) (and.imp (iff.mpr H1) (iff.mpr H2)) /- or -/ -definition not_or (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := -assume H : a ∨ b, or.rec_on H - (assume Ha, absurd Ha Hna) - (assume Hb, absurd Hb Hnb) +definition not_or : ¬a → ¬b → ¬(a ∨ b) := or.rec + +theorem or.imp (H₂ : a → c) (H₃ : b → d) : a ∨ b → c ∨ d := +or.rec (imp.syl or.inl H₂) (imp.syl or.inr H₃) + +theorem or.imp_left (H : a → b) : a ∨ c → b ∨ c := +or.imp H imp.id + +theorem or.imp_right (H : a → b) : c ∨ a → c ∨ b := +or.imp imp.id H theorem or_of_or_of_imp_of_imp (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d := -or.elim H₁ - (assume Ha : a, or.inl (H₂ Ha)) - (assume Hb : b, or.inr (H₃ Hb)) +or.imp H₂ H₃ H₁ theorem or_of_or_of_imp_left (H₁ : a ∨ c) (H : a → b) : b ∨ c := -or.elim H₁ - (assume H₂ : a, or.inl (H H₂)) - (assume H₂ : c, or.inr H₂) +or.imp_left H H₁ theorem or_of_or_of_imp_right (H₁ : c ∨ a) (H : a → b) : c ∨ b := -or.elim H₁ - (assume H₂ : c, or.inl H₂) - (assume H₂ : a, or.inr (H H₂)) +or.imp_right H H₁ theorem or.elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d := or.elim H Ha (assume H₂, or.elim H₂ Hb Hc) +theorem or.swap : a ∨ b → b ∨ a := or.rec or.inr or.inl + theorem or_resolve_right (H₁ : a ∨ b) (H₂ : ¬a) : b := -or.elim H₁ (assume Ha, absurd Ha H₂) (assume Hb, Hb) +or.elim H₁ (not.elim H₂) imp.id -theorem or_resolve_left (H₁ : a ∨ b) (H₂ : ¬b) : a := -or.elim H₁ (assume Ha, Ha) (assume Hb, absurd Hb H₂) +theorem or_resolve_left (H₁ : a ∨ b) : ¬b → a := +or_resolve_right (or.swap H₁) -theorem or.swap (H : a ∨ b) : b ∨ a := -or.elim H (assume Ha, or.inr Ha) (assume Hb, or.inl Hb) - -theorem or.comm [simp] : a ∨ b ↔ b ∨ a := -iff.intro (λH, or.swap H) (λH, or.swap H) +theorem or.comm [simp] : a ∨ b ↔ b ∨ a := iff.intro or.swap or.swap theorem or.assoc [simp] : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := iff.intro - (assume H, or.elim H - (assume H₁, or.elim H₁ - (assume Ha, or.inl Ha) - (assume Hb, or.inr (or.inl Hb))) - (assume Hc, or.inr (or.inr Hc))) - (assume H, or.elim H - (assume Ha, (or.inl (or.inl Ha))) - (assume H₁, or.elim H₁ - (assume Hb, or.inl (or.inr Hb)) - (assume Hc, or.inr Hc))) + (or.rec (or.imp_right or.inl) (imp.syl or.inr or.inr)) + (or.rec (imp.syl or.inl or.inl) (or.imp_left or.inr)) + +theorem or.imp_distrib : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := +iff.intro + (λH, and.intro (imp.syl H or.inl) (imp.syl H or.inr)) + (and.rec or.rec) + +theorem or_iff_right_of_imp {a b : Prop} (Ha : a → b) : (a ∨ b) ↔ b := +iff.intro (or.rec Ha imp.id) or.inr + +theorem or_iff_left_of_imp {a b : Prop} (Hb : b → a) : (a ∨ b) ↔ a := +iff.intro (or.rec imp.id Hb) or.inl theorem or_true [simp] (a : Prop) : a ∨ true ↔ true := -iff.intro (assume H, trivial) (assume H, or.inr H) +iff_true_intro (or.inr trivial) theorem true_or [simp] (a : Prop) : true ∨ a ↔ true := -iff.intro (assume H, trivial) (assume H, or.inl H) +iff_true_intro (or.inl trivial) theorem or_false [simp] (a : Prop) : a ∨ false ↔ a := -iff.intro - (assume H, or.elim H (assume H1 : a, H1) (assume H1 : false, false.elim H1)) - (assume H, or.inl H) +iff.intro (or.rec imp.id false.elim) or.inl theorem false_or [simp] (a : Prop) : false ∨ a ↔ a := -iff.intro - (assume H, or.elim H (assume H1 : false, false.elim H1) (assume H1 : a, H1)) - (assume H, or.inr H) +iff.trans or.comm !or_false theorem or_self (a : Prop) : a ∨ a ↔ a := -iff.intro - (assume H, or.elim H (assume H1, H1) (assume H1, H1)) - (assume H, or.inl H) +iff.intro (or.rec imp.id imp.id) or.inl theorem or_iff_or (H1 : a ↔ c) (H2 : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := -iff.intro - (λHab, or.elim Hab (λHa, or.inl (iff.elim_left H1 Ha)) (λHb, or.inr (iff.elim_left H2 Hb))) - (λHcd, or.elim Hcd (λHc, or.inl (iff.elim_right H1 Hc)) (λHd, or.inr (iff.elim_right H2 Hd))) +iff.intro (or.imp (iff.mp H1) (iff.mp H2)) (or.imp (iff.mpr H1) (iff.mpr H2)) /- distributivity -/ theorem and.distrib_left (a b c : Prop) : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) := iff.intro - (assume H, or.elim (and.right H) - (assume Hb : b, or.inl (and.intro (and.left H) Hb)) - (assume Hc : c, or.inr (and.intro (and.left H) Hc))) - (assume H, or.elim H - (assume Hab, and.intro (and.left Hab) (or.inl (and.right Hab))) - (assume Hac, and.intro (and.left Hac) (or.inr (and.right Hac)))) + (and.rec (λH, or.imp (and.intro H) (and.intro H))) + (or.rec (and.imp_right or.inl) (and.imp_right or.inr)) theorem and.distrib_right (a b c : Prop) : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) := -propext (!and.comm) ▸ propext (!and.comm) ▸ propext (!and.comm) ▸ !and.distrib_left +iff.trans (iff.trans !and.comm !and.distrib_left) (or_iff_or !and.comm !and.comm) theorem or.distrib_left (a b c : Prop) : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) := iff.intro - (assume H, or.elim H - (assume Ha, and.intro (or.inl Ha) (or.inl Ha)) - (assume Hbc, and.intro (or.inr (and.left Hbc)) (or.inr (and.right Hbc)))) - (assume H, or.elim (and.left H) - (assume Ha, or.inl Ha) - (assume Hb, or.elim (and.right H) - (assume Ha, or.inl Ha) - (assume Hc, or.inr (and.intro Hb Hc)))) + (or.rec (λH, and.intro (or.inl H) (or.inl H)) (and.imp or.inr or.inr)) + (and.rec (or.rec (imp.syl imp.intro or.inl) (imp.syl or.imp_right and.intro))) theorem or.distrib_right (a b c : Prop) : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := -propext (!or.comm) ▸ propext (!or.comm) ▸ propext (!or.comm) ▸ !or.distrib_left +iff.trans (iff.trans !or.comm !or.distrib_left) (and_iff_and !or.comm !or.comm) /- iff -/ -definition iff.def : (a ↔ b) = ((a → b) ∧ (b → a)) := -!eq.refl +definition iff.def : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl theorem iff_true [simp] (a : Prop) : (a ↔ true) ↔ a := -iff.intro - (assume H, iff.mpr H trivial) - (assume H, iff.intro (assume H1, trivial) (assume H1, H)) +iff.intro (assume H, iff.mpr H trivial) iff_true_intro theorem true_iff [simp] (a : Prop) : (true ↔ a) ↔ a := -iff.intro - (assume H, iff.mp H trivial) - (assume H, iff.intro (assume H1, H) (assume H1, trivial)) +iff.trans iff.comm !iff_true theorem iff_false [simp] (a : Prop) : (a ↔ false) ↔ ¬ a := -iff.intro - (assume H, and.left H) - (assume H, and.intro H (assume H1, false.elim H1)) +iff.intro and.left iff_false_intro theorem false_iff [simp] (a : Prop) : (false ↔ a) ↔ ¬ a := -iff.intro - (assume H, and.right H) - (assume H, and.intro (assume H1, false.elim H1) H) - -theorem iff_true_of_self (Ha : a) : a ↔ true := -iff.intro (assume H, trivial) (assume H, Ha) +iff.trans iff.comm !iff_false theorem iff_self [simp] (a : Prop) : (a ↔ a) ↔ true := -iff_true_of_self !iff.refl +iff_true_intro iff.rfl + +theorem forall_imp_forall {A : Type} {P Q : A → Prop} (H : ∀a, (P a → Q a)) (p : ∀a, P a) (a : A) : Q a := +(H a) (p a) theorem forall_iff_forall {A : Type} {P Q : A → Prop} (H : ∀a, (P a ↔ Q a)) : (∀a, P a) ↔ ∀a, Q a := -iff.intro (λp a, iff.elim_left (H a) (p a)) (λq a, iff.elim_right (H a) (q a)) +iff.intro (λp a, iff.mp (H a) (p a)) (λq a, iff.mpr (H a) (q a)) + +theorem exists_imp_exists {A : Type} {P Q : A → Prop} (H : ∀a, (P a → Q a)) (p : ∃a, P a) : ∃a, Q a := +exists.elim p (λa Hp, exists.intro a (H a Hp)) + +theorem exists_iff_exists {A : Type} {P Q : A → Prop} (H : ∀a, (P a ↔ Q a)) : (∃a, P a) ↔ ∃a, Q a := +iff.intro + (exists_imp_exists (λa, iff.mp (H a))) + (exists_imp_exists (λa, iff.mpr (H a))) theorem imp_iff {P : Prop} (Q : Prop) (p : P) : (P → Q) ↔ Q := -iff.intro (λf, f p) (λq p, q) +iff.intro (λf, f p) imp.intro theorem iff_iff_iff (H1 : a ↔ c) (H2 : b ↔ d) : (a ↔ b) ↔ (c ↔ d) := and_iff_and (imp_iff_imp H1 H2) (imp_iff_imp H2 H1) @@ -300,10 +296,8 @@ end /- congruences -/ -theorem congr_not {a b : Prop} (H : a ↔ b) : ¬a ↔ ¬b := -iff.intro - (assume H₁ : ¬a, assume H₂ : b, H₁ (iff.elim_right H H₂)) - (assume H₁ : ¬b, assume H₂ : a, H₁ (iff.elim_left H H₂)) +theorem congr_not [congr] {a b : Prop} (H : a ↔ b) : ¬a ↔ ¬b := +not_iff_not H section variables {a₁ b₁ a₂ b₂ : Prop} diff --git a/library/logic/eq.lean b/library/logic/eq.lean index d42f7f5d4..155858bc1 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -110,9 +110,8 @@ section assume (Hp : p) (Heq : p = false), Heq ▸ Hp theorem p_ne_true : ¬p → p ≠ true := - assume (Hnp : ¬p) (Heq : p = true), absurd trivial (Heq ▸ Hnp) + assume (Hnp : ¬p) (Heq : p = true), (Heq ▸ Hnp) trivial end theorem true_ne_false : ¬true = false := -assume H : true = false, - H ▸ trivial +p_ne_false trivial diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 1696516ea..093b70f3a 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -34,55 +34,26 @@ calc ... ↔ b ∧ (a ∧ c) : and.assoc theorem not_not_iff {a : Prop} [D : decidable a] : (¬¬a) ↔ a := -iff.intro - (assume H : ¬¬a, - by_cases (assume H' : a, H') (assume H' : ¬a, absurd H' H)) - (assume H : a, assume H', H' H) +iff.intro by_contradiction not_not_intro -theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a := -iff.mp not_not_iff H +theorem not_not_elim {a : Prop} [D : decidable a] : ¬¬a → a := +by_contradiction -theorem not_true_iff_false [simp] : ¬true ↔ false := -iff.intro (assume H, H trivial) false.elim +theorem not_or_iff_not_and_not {a b : Prop} : ¬(a ∨ b) ↔ ¬a ∧ ¬b := +or.imp_distrib -theorem not_false_iff_true [simp] : ¬false ↔ true := -iff.intro (assume H, trivial) (assume H H', H') - -theorem not_or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] : - ¬(a ∨ b) ↔ ¬a ∧ ¬b := -iff.intro - (assume H, or.elim (em a) - (assume Ha, absurd (or.inl Ha) H) - (assume Hna, or.elim (em b) - (assume Hb, absurd (or.inr Hb) H) - (assume Hnb, and.intro Hna Hnb))) - (assume (H : ¬a ∧ ¬b) (N : a ∨ b), - or.elim N - (assume Ha, absurd Ha (and.elim_left H)) - (assume Hb, absurd Hb (and.elim_right H))) - -theorem not_and_iff_not_or_not {a b : Prop} [Da : decidable a] [Db : decidable b] : +theorem not_and_iff_not_or_not {a b : Prop} [Da : decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b := iff.intro - (assume H, or.elim (em a) - (assume Ha, or.elim (em b) - (assume Hb, absurd (and.intro Ha Hb) H) - (assume Hnb, or.inr Hnb)) - (assume Hna, or.inl Hna)) - (assume (H : ¬a ∨ ¬b) (N : a ∧ b), - or.elim H - (assume Hna, absurd (and.elim_left N) Hna) - (assume Hnb, absurd (and.elim_right N) Hnb)) + (λH, by_cases (λa, or.inr (not.mto (and.intro a) H)) or.inl) + (or.rec (not.mto and.left) (not.mto and.right)) theorem imp_iff_not_or {a b : Prop} [Da : decidable a] : (a → b) ↔ ¬a ∨ b := iff.intro - (assume H : a → b, (or.elim (em a) - (assume Ha : a, or.inr (H Ha)) - (assume Hna : ¬a, or.inl Hna))) - (assume (H : ¬a ∨ b) (Ha : a), - or_resolve_right H (not_not_iff⁻¹ ▸ Ha)) + (by_cases (λHa H, or.inr (H Ha)) (λHa H, or.inl Ha)) + (or.rec not.elim imp.intro) -theorem not_implies_iff_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] : +theorem not_implies_iff_and_not {a b : Prop} [Da : decidable a] : ¬(a → b) ↔ a ∧ ¬b := calc ¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or} @@ -90,39 +61,30 @@ calc ... ↔ a ∧ ¬b : {not_not_iff} theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a := -assume H, by_contradiction (assume Hna : ¬a, - have Hnna : ¬¬a, from not_not_of_not_implies (mt H Hna), - absurd (not_not_elim Hnna) Hna) +by_cases imp.intro (imp.syl imp.mp not.elim) theorem forall_not_of_not_exists {A : Type} {p : A → Prop} [D : ∀x, decidable (p x)] (H : ¬∃x, p x) : ∀x, ¬p x := -take x, or.elim (em (p x)) - (assume Hp : p x, absurd (exists.intro x Hp) H) - (assume Hnp : ¬p x, Hnp) +take x, by_cases + (assume Hp : p x, absurd (exists.intro x Hp) H) + imp.id theorem forall_of_not_exists_not {A : Type} {p : A → Prop} [D : decidable_pred p] : ¬(∃ x, ¬p x) → ∀ x, p x := -assume Hne, take x, by_contradiction (assume Hnp : ¬ p x, Hne (exists.intro x Hnp)) +imp.syl (forall_imp_forall (λa, not_not_elim)) forall_not_of_not_exists theorem exists_not_of_not_forall {A : Type} {p : A → Prop} [D : ∀x, decidable (p x)] [D' : decidable (∃x, ¬p x)] (H : ¬∀x, p x) : ∃x, ¬p x := -by_contradiction - (assume H1 : ¬∃x, ¬p x, - have H2 : ∀x, ¬¬p x, from forall_not_of_not_exists H1, - have H3 : ∀x, p x, from take x, not_not_elim (H2 x), - absurd H3 H) +by_contradiction (λH1, absurd (λx, not_not_elim (forall_not_of_not_exists H1 x)) H) theorem exists_of_not_forall_not {A : Type} {p : A → Prop} [D : ∀x, decidable (p x)] - [D' : decidable (∃x, ¬¬p x)] (H : ¬∀x, ¬ p x) : + [D' : decidable (∃x, p x)] (H : ¬∀x, ¬ p x) : ∃x, p x := -obtain x (H : ¬¬ p x), from exists_not_of_not_forall H, -exists.intro x (not_not_elim H) +by_contradiction (imp.syl H forall_not_of_not_exists) theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false := -iff.intro - (assume H, false.of_ne H) - (assume H, false.elim H) +iff.intro false.of_ne false.elim theorem eq_self_iff_true [simp] {A : Type} (a : A) : (a = a) ↔ true := iff_true_intro rfl @@ -131,20 +93,12 @@ theorem heq_self_iff_true [simp] {A : Type} (a : A) : (a == a) ↔ true := iff_true_intro (heq.refl a) theorem iff_not_self [simp] (a : Prop) : (a ↔ ¬a) ↔ false := -iff.intro - (assume H, - have H' : ¬a, from assume Ha, (H ▸ Ha) Ha, - H' (H⁻¹ ▸ H')) - (assume H, false.elim H) +iff_false_intro (λH, + have H' : ¬a, from (λHa, (mp H Ha) Ha), + H' (iff.mpr H H')) theorem true_iff_false [simp] : (true ↔ false) ↔ false := -not_true_iff_false ▸ (iff_not_self true) +not_true ▸ (iff_not_self true) theorem false_iff_true [simp] : (false ↔ true) ↔ false := -not_false_iff_true ▸ (iff_not_self false) - -theorem iff_true_iff [simp] (a : Prop) : (a ↔ true) ↔ a := -iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H) - -theorem iff_false_iff_not [simp] (a : Prop) : (a ↔ false) ↔ ¬a := -iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H) +not_false_iff ▸ (iff_not_self false) diff --git a/library/logic/instances.lean b/library/logic/instances.lean index e9ac41a61..b8e89740c 100644 --- a/library/logic/instances.lean +++ b/library/logic/instances.lean @@ -21,43 +21,19 @@ relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans /- congruences for logic operations -/ theorem is_congruence_not : is_congruence iff iff not := -is_congruence.mk - (take a b, - assume H : a ↔ b, iff.intro - (assume H1 : ¬a, assume H2 : b, H1 (iff.elim_right H H2)) - (assume H1 : ¬b, assume H2 : a, H1 (iff.elim_left H H2))) +is_congruence.mk @congr_not theorem is_congruence_and : is_congruence2 iff iff iff and := -is_congruence2.mk - (take a1 b1 a2 b2, - assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, - iff.intro - (assume H3 : a1 ∧ a2, and_of_and_of_imp_of_imp H3 (iff.elim_left H1) (iff.elim_left H2)) - (assume H3 : b1 ∧ b2, and_of_and_of_imp_of_imp H3 (iff.elim_right H1) (iff.elim_right H2))) +is_congruence2.mk @congr_and theorem is_congruence_or : is_congruence2 iff iff iff or := -is_congruence2.mk - (take a1 b1 a2 b2, - assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, - iff.intro - (assume H3 : a1 ∨ a2, or_of_or_of_imp_of_imp H3 (iff.elim_left H1) (iff.elim_left H2)) - (assume H3 : b1 ∨ b2, or_of_or_of_imp_of_imp H3 (iff.elim_right H1) (iff.elim_right H2))) +is_congruence2.mk @congr_or theorem is_congruence_imp : is_congruence2 iff iff iff imp := -is_congruence2.mk - (take a1 b1 a2 b2, - assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, - iff.intro - (assume H3 : a1 → a2, assume Hb1 : b1, iff.elim_left H2 (H3 ((iff.elim_right H1) Hb1))) - (assume H3 : b1 → b2, assume Ha1 : a1, iff.elim_right H2 (H3 ((iff.elim_left H1) Ha1)))) +is_congruence2.mk @congr_imp theorem is_congruence_iff : is_congruence2 iff iff iff iff := -is_congruence2.mk - (take a1 b1 a2 b2, - assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, - iff.intro - (assume H3 : a1 ↔ a2, iff.trans (iff.symm H1) (iff.trans H3 H2)) - (assume H3 : b1 ↔ b2, iff.trans H1 (iff.trans H3 (iff.symm H2)))) +is_congruence2.mk @congr_iff definition is_congruence_not_compose [instance] := is_congruence.compose is_congruence_not definition is_congruence_and_compose [instance] := is_congruence.compose21 is_congruence_and @@ -75,7 +51,7 @@ end general_subst /- iff can be coerced to implication -/ definition mp_like_iff [instance] : relation.mp_like iff := -relation.mp_like.mk (λa b (H : a ↔ b), iff.elim_left H) +relation.mp_like.mk @iff.mp /- support for calculations with iff -/ diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index f2e119c91..3b68d8b1f 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -8,6 +8,12 @@ Universal and existential quantifiers. See also init.logic. import .connectives open inhabited nonempty +theorem exists_imp_distrib {A : Type} {B : Prop} {P : A → Prop} : ((∃ a : A, P a) → B) ↔ (∀ a : A, P a → B) := +iff.intro (λ e x H, e (exists.intro x H)) Exists.rec + +theorem forall_iff_not_exists {A : Type} {P : A → Prop} : (¬ ∃ a : A, P a) ↔ ∀ a : A, ¬ P a := +exists_imp_distrib + theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x := assume H1 : ∀x, ¬p x, obtain (w : A) (Hw : p w), from H, @@ -18,50 +24,36 @@ assume H1 : ∃x, ¬p x, obtain (w : A) (Hw : ¬p w), from H1, absurd (H2 w) Hw -theorem forall_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∀x, φ x) ↔ (∀x, ψ x) := -iff.intro - (assume Hl, take x, iff.elim_left (H x) (Hl x)) - (assume Hr, take x, iff.elim_right (H x) (Hr x)) +theorem forall_congr {A : Type} {φ ψ : A → Prop} : (∀x, φ x ↔ ψ x) → ((∀x, φ x) ↔ (∀x, ψ x)) := +forall_iff_forall -theorem exists_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∃x, φ x) ↔ (∃x, ψ x) := -iff.intro - (assume Hex, obtain w Pw, from Hex, - exists.intro w (iff.elim_left (H w) Pw)) - (assume Hex, obtain w Qw, from Hex, - exists.intro w (iff.elim_right (H w) Qw)) +theorem exists_congr {A : Type} {φ ψ : A → Prop} : (∀x, φ x ↔ ψ x) → ((∃x, φ x) ↔ (∃x, ψ x)) := +exists_iff_exists theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true := -iff.intro (assume H, trivial) (assume H, take x, trivial) +iff_true_intro (λH, trivial) theorem forall_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∀x : A, p) ↔ p := -iff.intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, Hr) +iff.intro (inhabited.destruct H) (λHr x, Hr) theorem exists_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∃x : A, p) ↔ p := -iff.intro - (assume Hl, obtain a Hp, from Hl, Hp) - (assume Hr, inhabited.destruct H (take a, exists.intro a Hr)) +iff.intro (Exists.rec (λx Hp, Hp)) (inhabited.destruct H exists.intro) theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) := iff.intro - (assume H, and.intro (take x, and.elim_left (H x)) (take x, and.elim_right (H x))) - (assume H, take x, and.intro (and.elim_left H x) (and.elim_right H x)) + (assume H, and.intro (take x, and.left (H x)) (take x, and.right (H x))) + (assume H x, and.intro (and.left H x) (and.right H x)) theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) := iff.intro - (assume H, obtain (w : A) (Hw : φ w ∨ ψ w), from H, - or.elim Hw - (assume Hw1 : φ w, or.inl (exists.intro w Hw1)) - (assume Hw2 : ψ w, or.inr (exists.intro w Hw2))) - (assume H, or.elim H - (assume H1, obtain (w : A) (Hw : φ w), from H1, - exists.intro w (or.inl Hw)) - (assume H2, obtain (w : A) (Hw : ψ w), from H2, - exists.intro w (or.inr Hw))) + (Exists.rec (λx, or.imp !exists.intro !exists.intro)) + (or.rec (exists_imp_exists (λx, or.inl)) + (exists_imp_exists (λx, or.inr))) -theorem nonempty_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A := -obtain w Hw, from H, nonempty.intro w +theorem nonempty_of_exists {A : Type} {P : A → Prop} : (∃x, P x) → nonempty A := +Exists.rec (λw H, intro w) section open decidable eq.ops @@ -70,16 +62,12 @@ section include H definition decidable_forall_eq [instance] : decidable (∀ x, x = a → P x) := - decidable.rec_on H - (λ pa, inl (λ x heq, eq.rec_on (eq.rec_on heq rfl) pa)) - (λ npa, inr (λ h, absurd (h a rfl) npa)) + if pa : P a then inl (λ x heq, eq.substr heq pa) + else inr (not.mto (λH, H a rfl) pa) definition decidable_exists_eq [instance] : decidable (∃ x, x = a ∧ P x) := - decidable.rec_on H - (λ pa, inl (exists.intro a (and.intro rfl pa))) - (λ npa, inr (λ h, - obtain (w : A) (Hw : w = a ∧ P w), from h, - absurd (and.rec_on Hw (λ h₁ h₂, h₁ ▸ h₂)) npa)) + if pa : P a then inl (exists.intro a (and.intro rfl pa)) + else inr (Exists.rec (λh, and.rec (λheq, eq.substr heq pa))) end /- exists_unique -/ @@ -96,7 +84,7 @@ exists.intro w (and.intro H1 H2) theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop} (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b := obtain w Hw, from H2, -H1 w (and.elim_left Hw) (and.elim_right Hw) +H1 w (and.left Hw) (and.right Hw) /- congruences -/ @@ -104,23 +92,13 @@ section variables {A : Type} {p₁ p₂ : A → Prop} (H : ∀x, p₁ x ↔ p₂ x) theorem congr_forall : (∀x, p₁ x) ↔ (∀x, p₂ x) := - iff.intro - (assume H', take x, iff.mp (H x) (H' x)) - (assume H', take x, iff.mpr (H x) (H' x)) + forall_congr H theorem congr_exists : (∃x, p₁ x) ↔ (∃x, p₂ x) := - iff.intro - (assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mp (H x) H₁))) - (assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mpr (H x) H₁))) + exists_congr H include H theorem congr_exists_unique : (∃!x, p₁ x) ↔ (∃!x, p₂ x) := - begin - apply congr_exists, - intro x, - apply congr_and (H x), - apply congr_forall, - intro y, - apply congr_imp (H y) !iff.rfl - end + congr_exists (λx, congr_and (H x) (congr_forall + (λy, congr_imp (H y) iff.rfl))) end