From ebe6ec0017e4cf1d525e0e0dcaece80a37054809 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jul 2015 16:39:53 -0400 Subject: [PATCH] feat(library): add '[rewrite]' annotation some some theorems --- library/data/equiv.lean | 36 +++++++++---------- library/data/finset/basic.lean | 6 ++-- library/data/list/basic.lean | 66 +++++++++++++++++----------------- library/data/nat/basic.lean | 37 +++++++++---------- library/init/logic.lean | 2 +- library/init/nat.lean | 53 +++++++++++++++++++++++---- library/logic/connectives.lean | 36 +++++++++---------- 7 files changed, 139 insertions(+), 97 deletions(-) diff --git a/library/data/equiv.lean b/library/data/equiv.lean index 841906a02..e8b78af8f 100644 --- a/library/data/equiv.lean +++ b/library/data/equiv.lean @@ -50,22 +50,22 @@ lemma arrow_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ section open unit -lemma arrow_unit_equiv_unit (A : Type) : (A → unit) ≃ unit := +lemma arrow_unit_equiv_unit [rewrite] (A : Type) : (A → unit) ≃ unit := mk (λ f, star) (λ u, (λ f, star)) (λ f, funext (λ x, by cases (f x); reflexivity)) (λ u, by cases u; reflexivity) -lemma unit_arrow_equiv (A : Type) : (unit → A) ≃ A := +lemma unit_arrow_equiv [rewrite] (A : Type) : (unit → A) ≃ A := mk (λ f, f star) (λ a, (λ u, a)) (λ f, funext (λ x, by cases x; reflexivity)) (λ u, rfl) -lemma empty_arrow_equiv_unit (A : Type) : (empty → A) ≃ unit := +lemma empty_arrow_equiv_unit [rewrite] (A : Type) : (empty → A) ≃ unit := mk (λ f, star) (λ u, λ e, empty.rec _ e) (λ f, funext (λ x, empty.rec _ x)) (λ u, by cases u; reflexivity) -lemma false_arrow_equiv_unit (A : Type) : (false → A) ≃ unit := +lemma false_arrow_equiv_unit [rewrite] (A : Type) : (false → A) ≃ unit := calc (false → A) ≃ (empty → A) : arrow_congr false_equiv_empty !equiv.refl ... ≃ unit : empty_arrow_equiv_unit end @@ -78,13 +78,13 @@ lemma prod_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ (λ p, begin cases p, esimp, rewrite [l₁, l₂] end) (λ p, begin cases p, esimp, rewrite [r₁, r₂] end) -lemma prod_comm (A B : Type) : (A × B) ≃ (B × A) := +lemma prod_comm [rewrite] (A B : Type) : (A × B) ≃ (B × A) := mk (λ p, match p with (a, b) := (b, a) end) (λ p, match p with (b, a) := (a, b) end) (λ p, begin cases p, esimp end) (λ p, begin cases p, esimp end) -lemma prod_assoc (A B C : Type) : ((A × B) × C) ≃ (A × (B × C)) := +lemma prod_assoc [rewrite] (A B C : Type) : ((A × B) × C) ≃ (A × (B × C)) := mk (λ t, match t with ((a, b), c) := (a, (b, c)) end) (λ t, match t with (a, (b, c)) := ((a, b), c) end) (λ t, begin cases t with ab c, cases ab, esimp end) @@ -92,20 +92,20 @@ mk (λ t, match t with ((a, b), c) := (a, (b, c)) end) section open unit prod.ops -lemma prod_unit_right (A : Type) : (A × unit) ≃ A := +lemma prod_unit_right [rewrite] (A : Type) : (A × unit) ≃ A := mk (λ p, p.1) (λ a, (a, star)) (λ p, begin cases p with a u, cases u, esimp end) (λ a, rfl) -lemma prod_unit_left (A : Type) : (unit × A) ≃ A := +lemma prod_unit_left [rewrite] (A : Type) : (unit × A) ≃ A := calc (unit × A) ≃ (A × unit) : prod_comm ... ≃ A : prod_unit_right -lemma prod_empty_right (A : Type) : (A × empty) ≃ empty := +lemma prod_empty_right [rewrite] (A : Type) : (A × empty) ≃ empty := mk (λ p, empty.rec _ p.2) (λ e, empty.rec _ e) (λ p, empty.rec _ p.2) (λ e, empty.rec _ e) -lemma prod_empty_left (A : Type) : (empty × A) ≃ empty := +lemma prod_empty_left [rewrite] (A : Type) : (empty × A) ≃ empty := calc (empty × A) ≃ (A × empty) : prod_comm ... ≃ empty : prod_empty_right end @@ -127,25 +127,25 @@ mk (λ b, match b with tt := inl star | ff := inr star end) (λ b, begin cases b, esimp, esimp end) (λ s, begin cases s with u u, {cases u, esimp}, {cases u, esimp} end) -lemma sum_comm (A B : Type) : (A + B) ≃ (B + A) := +lemma sum_comm [rewrite] (A B : Type) : (A + B) ≃ (B + A) := mk (λ s, match s with inl a := inr a | inr b := inl b end) (λ s, match s with inl b := inr b | inr a := inl a end) (λ s, begin cases s, esimp, esimp end) (λ s, begin cases s, esimp, esimp end) -lemma sum_assoc (A B C : Type) : ((A + B) + C) ≃ (A + (B + C)) := +lemma sum_assoc [rewrite] (A B C : Type) : ((A + B) + C) ≃ (A + (B + C)) := mk (λ s, match s with inl (inl a) := inl a | inl (inr b) := inr (inl b) | inr c := inr (inr c) end) (λ s, match s with inl a := inl (inl a) | inr (inl b) := inl (inr b) | inr (inr c) := inr c end) (λ s, begin cases s with ab c, cases ab, repeat esimp end) (λ s, begin cases s with a bc, esimp, cases bc, repeat esimp end) -lemma sum_empty_right (A : Type) : (A + empty) ≃ A := +lemma sum_empty_right [rewrite] (A : Type) : (A + empty) ≃ A := mk (λ s, match s with inl a := a | inr e := empty.rec _ e end) (λ a, inl a) (λ s, begin cases s with a e, esimp, exact empty.rec _ e end) (λ a, rfl) -lemma sum_empty_left (A : Type) : (empty + A) ≃ A := +lemma sum_empty_left [rewrite] (A : Type) : (empty + A) ≃ A := calc (empty + A) ≃ (A + empty) : sum_comm ... ≃ A : sum_empty_right end @@ -191,23 +191,23 @@ mk (λ n, match n with 0 := inr star | succ a := inl a end) (λ n, begin cases n, repeat esimp end) (λ s, begin cases s with a u, esimp, {cases u, esimp} end) -lemma nat_sum_unit_equiv_nat : (nat + unit) ≃ nat := +lemma nat_sum_unit_equiv_nat [rewrite] : (nat + unit) ≃ nat := equiv.symm nat_equiv_nat_sum_unit -lemma nat_prod_nat_equiv_nat : (nat × nat) ≃ nat := +lemma nat_prod_nat_equiv_nat [rewrite] : (nat × nat) ≃ nat := mk (λ p, mkpair p.1 p.2) (λ n, unpair n) (λ p, begin cases p, apply unpair_mkpair end) (λ n, mkpair_unpair n) -lemma nat_sum_bool_equiv_nat : (nat + bool) ≃ nat := +lemma nat_sum_bool_equiv_nat [rewrite] : (nat + bool) ≃ nat := calc (nat + bool) ≃ (nat + (unit + unit)) : sum_congr !equiv.refl bool_equiv_unit_sum_unit ... ≃ ((nat + unit) + unit) : sum_assoc ... ≃ (nat + unit) : sum_congr nat_sum_unit_equiv_nat !equiv.refl ... ≃ nat : nat_sum_unit_equiv_nat open decidable -lemma nat_sum_nat_equiv_nat : (nat + nat) ≃ nat := +lemma nat_sum_nat_equiv_nat [rewrite] : (nat + nat) ≃ nat := mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end) (λ n, if even n then inl (n div 2) else inr ((n - 1) div 2)) (λ s, begin diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index 5733d9a6a..f31519379 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -84,7 +84,7 @@ theorem mem_list_of_mem {a : A} {l : nodup_list A} : a ∈ ⟦l⟧ → a ∈ elt definition singleton (a : A) : finset A := to_finset_of_nodup [a] !nodup_singleton -theorem mem_singleton (a : A) : a ∈ singleton a := +theorem mem_singleton [rewrite] (a : A) : a ∈ singleton a := mem_of_mem_list !mem_cons theorem eq_of_mem_singleton {x a : A} : x ∈ singleton a → x = a := @@ -116,10 +116,10 @@ to_finset_of_nodup [] nodup_nil notation `∅` := !empty -theorem not_mem_empty (a : A) : a ∉ ∅ := +theorem not_mem_empty [rewrite] (a : A) : a ∉ ∅ := λ aine : a ∈ ∅, aine -theorem mem_empty_iff (x : A) : x ∈ ∅ ↔ false := +theorem mem_empty_iff [rewrite] (x : A) : x ∈ ∅ ↔ false := iff.mp' !iff_false_iff_not !not_mem_empty theorem mem_empty_eq (x : A) : x ∈ ∅ = false := diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index bff7ae1f5..f3e69f8db 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -18,7 +18,7 @@ notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l variable {T : Type} -lemma cons_ne_nil (a : T) (l : list T) : a::l ≠ [] := +lemma cons_ne_nil [rewrite] (a : T) (l : list T) : a::l ≠ [] := by contradiction lemma head_eq_of_cons_eq {A : Type} {h₁ h₂ : A} {t₁ t₂ : list A} : @@ -40,17 +40,17 @@ definition append : list T → list T → list T notation l₁ ++ l₂ := append l₁ l₂ -theorem append_nil_left (t : list T) : [] ++ t = t +theorem append_nil_left [rewrite] (t : list T) : [] ++ t = t -theorem append_cons (x : T) (s t : list T) : (x::s) ++ t = x::(s ++ t) +theorem append_cons [rewrite] (x : T) (s t : list T) : (x::s) ++ t = x::(s ++ t) -theorem append_nil_right : ∀ (t : list T), t ++ [] = t +theorem append_nil_right [rewrite] : ∀ (t : list T), t ++ [] = t | [] := rfl | (a :: l) := calc (a :: l) ++ [] = a :: (l ++ []) : rfl ... = a :: l : append_nil_right l -theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u) +theorem append.assoc [rewrite] : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u) | [] t u := rfl | (a :: l) t u := show a :: (l ++ t ++ u) = (a :: l) ++ (t ++ u), @@ -61,11 +61,11 @@ definition length : list T → nat | [] := 0 | (a :: l) := length l + 1 -theorem length_nil : length (@nil T) = 0 +theorem length_nil [rewrite] : length (@nil T) = 0 -theorem length_cons (x : T) (t : list T) : length (x::t) = length t + 1 +theorem length_cons [rewrite] (x : T) (t : list T) : length (x::t) = length t + 1 -theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length t +theorem length_append [rewrite] : ∀ (s t : list T), length (s ++ t) = length s + length t | [] t := calc length ([] ++ t) = length t : rfl ... = length [] + length t : zero_add @@ -91,9 +91,9 @@ definition concat : Π (x : T), list T → list T | a [] := [a] | a (b :: l) := b :: concat a l -theorem concat_nil (x : T) : concat x [] = [x] +theorem concat_nil [rewrite] (x : T) : concat x [] = [x] -theorem concat_cons (x y : T) (l : list T) : concat x (y::l) = y::(concat x l) +theorem concat_cons [rewrite] (x y : T) (l : list T) : concat x (y::l) = y::(concat x l) theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a] | [] := rfl @@ -101,7 +101,7 @@ theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a] show b :: (concat a l) = (b :: l) ++ (a :: []), by rewrite concat_eq_append -theorem concat_ne_nil (a : T) : ∀ (l : list T), concat a l ≠ [] := +theorem concat_ne_nil [rewrite] (a : T) : ∀ (l : list T), concat a l ≠ [] := by intro l; induction l; repeat contradiction /- last -/ @@ -111,16 +111,16 @@ definition last : Π l : list T, l ≠ [] → T | [a] h := a | (a₁::a₂::l) h := last (a₂::l) !cons_ne_nil -lemma last_singleton (a : T) (h : [a] ≠ []) : last [a] h = a := +lemma last_singleton [rewrite] (a : T) (h : [a] ≠ []) : last [a] h = a := rfl -lemma last_cons_cons (a₁ a₂ : T) (l : list T) (h : a₁::a₂::l ≠ []) : last (a₁::a₂::l) h = last (a₂::l) !cons_ne_nil := +lemma last_cons_cons [rewrite] (a₁ a₂ : T) (l : list T) (h : a₁::a₂::l ≠ []) : last (a₁::a₂::l) h = last (a₂::l) !cons_ne_nil := rfl theorem last_congr {l₁ l₂ : list T} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) : last l₁ h₁ = last l₂ h₂ := by subst l₁ -theorem last_concat {x : T} : ∀ {l : list T} (h : concat x l ≠ []), last (concat x l) h = x +theorem last_concat [rewrite] {x : T} : ∀ {l : list T} (h : concat x l ≠ []), last (concat x l) h = x | [] h := rfl | [a] h := rfl | (a₁::a₂::l) h := @@ -139,13 +139,13 @@ definition reverse : list T → list T | [] := [] | (a :: l) := concat a (reverse l) -theorem reverse_nil : reverse (@nil T) = [] +theorem reverse_nil [rewrite] : reverse (@nil T) = [] -theorem reverse_cons (x : T) (l : list T) : reverse (x::l) = concat x (reverse l) +theorem reverse_cons [rewrite] (x : T) (l : list T) : reverse (x::l) = concat x (reverse l) -theorem reverse_singleton (x : T) : reverse [x] = [x] +theorem reverse_singleton [rewrite] (x : T) : reverse [x] = [x] -theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s) +theorem reverse_append [rewrite] : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s) | [] t2 := calc reverse ([] ++ t2) = reverse t2 : rfl ... = (reverse t2) ++ [] : append_nil_right @@ -158,7 +158,7 @@ theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ ( ... = reverse t2 ++ concat a2 (reverse s2) : concat_eq_append ... = reverse t2 ++ reverse (a2 :: s2) : rfl -theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l +theorem reverse_reverse [rewrite] : ∀ (l : list T), reverse (reverse l) = l | [] := rfl | (a :: l) := calc reverse (reverse (a :: l)) = reverse (concat a (reverse l)) : rfl @@ -178,9 +178,9 @@ definition head [h : inhabited T] : list T → T | [] := arbitrary T | (a :: l) := a -theorem head_cons [h : inhabited T] (a : T) (l : list T) : head (a::l) = a +theorem head_cons [rewrite] [h : inhabited T] (a : T) (l : list T) : head (a::l) = a -theorem head_append [h : inhabited T] (t : list T) : ∀ {s : list T}, s ≠ [] → head (s ++ t) = head s +theorem head_append [rewrite] [h : inhabited T] (t : list T) : ∀ {s : list T}, s ≠ [] → head (s ++ t) = head s | [] H := absurd rfl H | (a :: s) H := show head (a :: (s ++ t)) = head (a :: s), @@ -190,9 +190,9 @@ definition tail : list T → list T | [] := [] | (a :: l) := l -theorem tail_nil : tail (@nil T) = [] +theorem tail_nil [rewrite] : tail (@nil T) = [] -theorem tail_cons (a : T) (l : list T) : tail (a::l) = l +theorem tail_cons [rewrite] (a : T) (l : list T) : tail (a::l) = l theorem cons_head_tail [h : inhabited T] {l : list T} : l ≠ [] → (head l)::(tail l) = l := list.cases_on l @@ -208,13 +208,13 @@ definition mem : T → list T → Prop notation e ∈ s := mem e s notation e ∉ s := ¬ e ∈ s -theorem mem_nil_iff (x : T) : x ∈ [] ↔ false := +theorem mem_nil_iff [rewrite] (x : T) : x ∈ [] ↔ false := iff.rfl theorem not_mem_nil (x : T) : x ∉ [] := iff.mp !mem_nil_iff -theorem mem_cons (x : T) (l : list T) : x ∈ x :: l := +theorem mem_cons [rewrite] (x : T) (l : list T) : x ∈ x :: l := or.inl rfl theorem mem_cons_of_mem (y : T) {x : T} {l : list T} : x ∈ l → x ∈ y :: l := @@ -340,16 +340,16 @@ definition sublist (l₁ l₂ : list T) := ∀ ⦃a : T⦄, a ∈ l₁ → a ∈ infix `⊆` := sublist -theorem nil_sub (l : list T) : [] ⊆ l := +theorem nil_sub [rewrite] (l : list T) : [] ⊆ l := λ b i, false.elim (iff.mp (mem_nil_iff b) i) -theorem sub.refl (l : list T) : l ⊆ l := +theorem sub.refl [rewrite] (l : list T) : l ⊆ l := λ b i, i theorem sub.trans {l₁ l₂ l₃ : list T} (H₁ : l₁ ⊆ l₂) (H₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ := λ b i, H₂ (H₁ i) -theorem sub_cons (a : T) (l : list T) : l ⊆ a::l := +theorem sub_cons [rewrite] (a : T) (l : list T) : l ⊆ a::l := λ b i, or.inr i theorem sub_of_cons_sub {a : T} {l₁ l₂ : list T} : a::l₁ ⊆ l₂ → l₁ ⊆ l₂ := @@ -360,10 +360,10 @@ theorem cons_sub_cons {l₁ l₂ : list T} (a : T) (s : l₁ ⊆ l₂) : (a::l (λ e : b = a, or.inl e) (λ i : b ∈ l₁, or.inr (s i)) -theorem sub_append_left (l₁ l₂ : list T) : l₁ ⊆ l₁++l₂ := +theorem sub_append_left [rewrite] (l₁ l₂ : list T) : l₁ ⊆ l₁++l₂ := λ b i, iff.mp' (mem_append_iff b l₁ l₂) (or.inl i) -theorem sub_append_right (l₁ l₂ : list T) : l₂ ⊆ l₁++l₂ := +theorem sub_append_right [rewrite] (l₁ l₂ : list T) : l₂ ⊆ l₁++l₂ := λ b i, iff.mp' (mem_append_iff b l₁ l₂) (or.inr i) theorem sub_cons_of_sub (a : T) {l₁ l₂ : list T} : l₁ ⊆ l₂ → l₁ ⊆ (a::l₂) := @@ -399,7 +399,7 @@ definition find : T → list T → nat | a [] := 0 | a (b :: l) := if a = b then 0 else succ (find a l) -theorem find_nil (x : T) : find x [] = 0 +theorem find_nil [rewrite] (x : T) : find x [] = 0 theorem find_cons (x y : T) (l : list T) : find x (y::l) = if x = y then 0 else succ (find x l) @@ -461,9 +461,9 @@ definition nth : list T → nat → option T | (a :: l) 0 := some a | (a :: l) (n+1) := nth l n -theorem nth_zero (a : T) (l : list T) : nth (a :: l) 0 = some a +theorem nth_zero [rewrite] (a : T) (l : list T) : nth (a :: l) 0 = some a -theorem nth_succ (a : T) (l : list T) (n : nat) : nth (a::l) (succ n) = nth l n +theorem nth_succ [rewrite] (a : T) (l : list T) (n : nat) : nth (a::l) (succ n) = nth l n theorem nth_eq_some : ∀ {l : list T} {n : nat}, n < length l → Σ a : T, nth l n = some a | [] n h := absurd h !not_lt_zero diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 8d63ae93f..c3ef4904a 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -49,10 +49,10 @@ by contradiction -- add_rewrite succ_ne_zero -theorem pred_zero : pred 0 = 0 := +theorem pred_zero [rewrite] : pred 0 = 0 := rfl -theorem pred_succ (n : ℕ) : pred (succ n) = n := +theorem pred_succ [rewrite] (n : ℕ) : pred (succ n) = n := rfl theorem eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) := @@ -103,13 +103,13 @@ general m /- addition -/ -theorem add_zero (n : ℕ) : n + 0 = n := +theorem add_zero [rewrite] (n : ℕ) : n + 0 = n := rfl -theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) := +theorem add_succ [rewrite] (n m : ℕ) : n + succ m = succ (n + m) := rfl -theorem zero_add (n : ℕ) : 0 + n = n := +theorem zero_add [rewrite] (n : ℕ) : 0 + n = n := nat.induction_on n !add_zero (take m IH, show 0 + succ m = succ m, from @@ -117,7 +117,7 @@ nat.induction_on n 0 + succ m = succ (0 + m) : add_succ ... = succ m : IH) -theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) := +theorem succ_add [rewrite] (n m : ℕ) : (succ n) + m = succ (n + m) := nat.induction_on m (!add_zero ▸ !add_zero) (take k IH, calc @@ -125,7 +125,7 @@ nat.induction_on m ... = succ (succ (n + k)) : IH ... = succ (n + succ k) : add_succ) -theorem add.comm (n m : ℕ) : n + m = m + n := +theorem add.comm [rewrite] (n m : ℕ) : n + m = m + n := nat.induction_on m (!add_zero ⬝ !zero_add⁻¹) (take k IH, calc @@ -136,7 +136,7 @@ nat.induction_on m theorem succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m := !succ_add ⬝ !add_succ⁻¹ -theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) := +theorem add.assoc [rewrite] (n m k : ℕ) : (n + m) + k = n + (m + k) := nat.induction_on k (!add_zero ▸ !add_zero) (take l IH, @@ -146,7 +146,7 @@ nat.induction_on k ... = n + succ (m + l) : add_succ ... = n + (m + succ l) : add_succ) -theorem add.left_comm (n m k : ℕ) : n + (m + k) = m + (n + k) := +theorem add.left_comm [rewrite] (n m k : ℕ) : n + (m + k) = m + (n + k) := left_comm add.comm add.assoc n m k theorem add.right_comm (n m k : ℕ) : n + m + k = n + k + m := @@ -186,7 +186,7 @@ eq_zero_of_add_eq_zero_right (!add.comm ⬝ H) theorem eq_zero_and_eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 := and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H) -theorem add_one (n : ℕ) : n + 1 = succ n := +theorem add_one [rewrite] (n : ℕ) : n + 1 = succ n := !add_zero ▸ !add_succ theorem one_add (n : ℕ) : 1 + n = succ n := @@ -194,20 +194,20 @@ theorem one_add (n : ℕ) : 1 + n = succ n := /- multiplication -/ -theorem mul_zero (n : ℕ) : n * 0 = 0 := +theorem mul_zero [rewrite] (n : ℕ) : n * 0 = 0 := rfl -theorem mul_succ (n m : ℕ) : n * succ m = n * m + n := +theorem mul_succ [rewrite] (n m : ℕ) : n * succ m = n * m + n := rfl -- commutativity, distributivity, associativity, identity -theorem zero_mul (n : ℕ) : 0 * n = 0 := +theorem zero_mul [rewrite] (n : ℕ) : 0 * n = 0 := nat.induction_on n !mul_zero (take m IH, !mul_succ ⬝ !add_zero ⬝ IH) -theorem succ_mul (n m : ℕ) : (succ n) * m = (n * m) + m := +theorem succ_mul [rewrite] (n m : ℕ) : (succ n) * m = (n * m) + m := nat.induction_on m (!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add_zero⁻¹) (take k IH, calc @@ -219,7 +219,7 @@ nat.induction_on m ... = n * k + n + succ k : add.assoc ... = n * succ k + succ k : mul_succ) -theorem mul.comm (n m : ℕ) : n * m = m * n := +theorem mul.comm [rewrite] (n m : ℕ) : n * m = m * n := nat.induction_on m (!mul_zero ⬝ !zero_mul⁻¹) (take k IH, calc @@ -250,7 +250,7 @@ calc ... = n * m + k * n : mul.comm ... = n * m + n * k : mul.comm -theorem mul.assoc (n m k : ℕ) : (n * m) * k = n * (m * k) := +theorem mul.assoc [rewrite] (n m k : ℕ) : (n * m) * k = n * (m * k) := nat.induction_on k (calc (n * m) * 0 = n * (m * 0) : mul_zero) @@ -261,13 +261,13 @@ nat.induction_on k ... = n * (m * l + m) : mul.left_distrib ... = n * (m * succ l) : mul_succ) -theorem mul_one (n : ℕ) : n * 1 = n := +theorem mul_one [rewrite] (n : ℕ) : n * 1 = n := calc n * 1 = n * 0 + n : mul_succ ... = 0 + n : mul_zero ... = n : zero_add -theorem one_mul (n : ℕ) : 1 * n = n := +theorem one_mul [rewrite] (n : ℕ) : 1 * n = n := calc 1 * n = n * 1 : mul.comm ... = n : mul_one @@ -314,5 +314,6 @@ section migrate_algebra notation a ∣ b := dvd a b migrate from algebra with nat replacing dvd → dvd + end migrate_algebra end nat diff --git a/library/init/logic.lean b/library/init/logic.lean index cbca787c4..3827619e8 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -504,7 +504,7 @@ decidable.rec (λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t e)) H -theorem if_t_t (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t := +theorem if_t_t [rewrite] (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else 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)) diff --git a/library/init/nat.lean b/library/init/nat.lean index c44290f8e..fe10da573 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -62,6 +62,12 @@ namespace nat theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor) + theorem le_succ_iff_true [rewrite] (n : ℕ) : n ≤ succ n ↔ true := + iff_true_intro (le_succ n) + + theorem pred_le_iff_true [rewrite] (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 @@ -86,15 +92,24 @@ namespace nat 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 [rewrite] (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 [rewrite] (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 [rewrite] (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 @@ -116,9 +131,19 @@ namespace nat 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) + theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self + theorem lt_self_iff_false [rewrite] (n : ℕ) : n < n ↔ false := + iff_false_intro (lt.irrefl n) + theorem self_lt_succ (n : ℕ) : n < succ n := !le.refl + + theorem self_lt_succ_iff_true [rewrite] (n : ℕ) : n < succ n ↔ true := + iff_true_intro (self_lt_succ n) + theorem lt.base (n : ℕ) : n < succ n := !le.refl theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : false := @@ -147,15 +172,18 @@ namespace nat 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)) - definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := + 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 - definition not_lt_zero (a : ℕ) : ¬ a < zero := + theorem not_lt_zero (a : ℕ) : ¬ a < zero := by intro H; cases H + theorem lt_zero_iff_false [rewrite] (a : ℕ) : a < zero ↔ false := + iff_false_intro (not_lt_zero a) + -- less-than is well-founded definition lt.wf [instance] : well_founded lt := begin @@ -221,7 +249,7 @@ namespace nat definition max (a b : ℕ) : ℕ := if a < b then b else a definition min (a b : ℕ) : ℕ := if a < b then a else b - theorem max_self (a : ℕ) : max a a = a := + theorem max_self [rewrite] (a : ℕ) : max a a = a := eq.rec_on !if_t_t rfl theorem max_eq_right' {a b : ℕ} (H : a < b) : max a b = b := @@ -242,6 +270,9 @@ namespace nat (λ h : a < b, le_of_lt (eq.rec_on (eq_max_right h) h)) (λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl) + theorem le_max_left_iff_true [rewrite] (a b : ℕ) : a ≤ max a b ↔ true := + iff_true_intro (le_max_left a b) + theorem le_max_right (a b : ℕ) : b ≤ max a b := by_cases (λ h : a < b, eq.rec_on (eq_max_right h) !le.refl) @@ -251,13 +282,16 @@ namespace nat have aux : a = max a b, from eq_max_left (lt.asymm h), eq.rec_on aux (le_of_lt h))) - theorem succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b := + theorem le_max_right_iff_true [rewrite] (a b : ℕ) : b ≤ max a b ↔ true := + iff_true_intro (le_max_right a b) + + theorem succ_sub_succ_eq_sub [rewrite] (a b : ℕ) : succ a - succ b = a - b := by induction b with b IH;reflexivity; apply congr (eq.refl pred) IH 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 - theorem zero_sub_eq_zero (a : ℕ) : zero - a = zero := + theorem zero_sub_eq_zero [rewrite] (a : ℕ) : zero - a = zero := nat.rec_on a rfl (λ a₁ (ih : zero - a₁ = zero), congr (eq.refl pred) ih) @@ -285,5 +319,12 @@ namespace nat (le.refl a) (λ b₁ ih, le.trans !pred_le ih) - lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b) + theorem sub_le_iff_true [rewrite] (a b : ℕ) : a - b ≤ a ↔ true := + iff_true_intro (sub_le a b) + + theorem sub_lt_succ (a b : ℕ) : a - b < succ a := + lt_succ_of_le (sub_le a b) + + theorem sub_lt_succ_iff_true [rewrite] (a b : ℕ) : a - b < succ a ↔ true := + iff_true_intro (sub_lt_succ a b) end nat diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 2aeea79fe..7c893134d 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -61,10 +61,10 @@ have Hnp : ¬a, from assume Hp : a, absurd (or.inl Hp) not_em, absurd (or.inr Hnp) not_em -theorem not_true : ¬ true ↔ false := +theorem not_true [rewrite] : ¬ true ↔ false := iff.intro (assume H, H trivial) (assume H, false.elim H) -theorem not_false_iff : ¬ false ↔ true := +theorem not_false_iff [rewrite] : ¬ false ↔ true := iff.intro (assume H, trivial) (assume H H1, H1) theorem not_iff_not (H : a ↔ b) : ¬a ↔ ¬b := @@ -105,19 +105,19 @@ iff.intro obtain Ha Hb Hc, from H, and.intro (and.intro Ha Hb) Hc) -theorem and_true (a : Prop) : a ∧ true ↔ a := +theorem and_true [rewrite] (a : Prop) : a ∧ true ↔ a := iff.intro (assume H, and.left H) (assume H, and.intro H trivial) -theorem true_and (a : Prop) : true ∧ a ↔ a := +theorem true_and [rewrite] (a : Prop) : true ∧ a ↔ a := iff.intro (assume H, and.right H) (assume H, and.intro trivial H) -theorem and_false (a : Prop) : a ∧ false ↔ false := +theorem and_false [rewrite] (a : Prop) : a ∧ false ↔ false := iff.intro (assume H, and.right H) (assume H, false.elim H) -theorem false_and (a : Prop) : false ∧ a ↔ false := +theorem false_and [rewrite] (a : Prop) : false ∧ a ↔ false := iff.intro (assume H, and.left H) (assume H, false.elim H) -theorem and_self (a : Prop) : a ∧ a ↔ a := +theorem and_self [rewrite] (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) := @@ -190,18 +190,18 @@ iff.intro (assume Hb, or.inl (or.inr Hb)) (assume Hc, or.inr Hc))) -theorem or_true (a : Prop) : a ∨ true ↔ true := +theorem or_true [rewrite] (a : Prop) : a ∨ true ↔ true := iff.intro (assume H, trivial) (assume H, or.inr H) -theorem true_or (a : Prop) : true ∨ a ↔ true := +theorem true_or [rewrite] (a : Prop) : true ∨ a ↔ true := iff.intro (assume H, trivial) (assume H, or.inl H) -theorem or_false (a : Prop) : a ∨ false ↔ a := +theorem or_false [rewrite] (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) -theorem false_or (a : Prop) : false ∨ a ↔ a := +theorem false_or [rewrite] (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) @@ -249,22 +249,22 @@ propext (!or.comm) ▸ propext (!or.comm) ▸ propext (!or.comm) ▸ !or.distrib definition iff.def : (a ↔ b) = ((a → b) ∧ (b → a)) := !eq.refl -theorem iff_true (a : Prop) : (a ↔ true) ↔ a := +theorem iff_true [rewrite] (a : Prop) : (a ↔ true) ↔ a := iff.intro (assume H, iff.mp' H trivial) (assume H, iff.intro (assume H1, trivial) (assume H1, H)) -theorem true_iff (a : Prop) : (true ↔ a) ↔ a := +theorem true_iff [rewrite] (a : Prop) : (true ↔ a) ↔ a := iff.intro (assume H, iff.mp H trivial) (assume H, iff.intro (assume H1, H) (assume H1, trivial)) -theorem iff_false (a : Prop) : (a ↔ false) ↔ ¬ a := +theorem iff_false [rewrite] (a : Prop) : (a ↔ false) ↔ ¬ a := iff.intro (assume H, and.left H) (assume H, and.intro H (assume H1, false.elim H1)) -theorem false_iff (a : Prop) : (false ↔ a) ↔ ¬ a := +theorem false_iff [rewrite] (a : Prop) : (false ↔ a) ↔ ¬ a := iff.intro (assume H, and.right H) (assume H, and.intro (assume H1, false.elim H1) H) @@ -272,7 +272,7 @@ iff.intro theorem iff_true_of_self (Ha : a) : a ↔ true := iff.intro (assume H, trivial) (assume H, Ha) -theorem iff_self (a : Prop) : (a ↔ a) ↔ true := +theorem iff_self [rewrite] (a : Prop) : (a ↔ a) ↔ true := iff_true_of_self !iff.refl theorem forall_iff_forall {A : Type} {P Q : A → Prop} (H : ∀a, (P a ↔ Q a)) : (∀a, P a) ↔ ∀a, Q a := @@ -291,10 +291,10 @@ section variables {A : Type} {c₁ c₂ : Prop} - definition if_true (t e : A) : (if true then t else e) = t := + definition if_true [rewrite] (t e : A) : (if true then t else e) = t := if_pos trivial - definition if_false (t e : A) : (if false then t else e) = e := + definition if_false [rewrite] (t e : A) : (if false then t else e) = e := if_neg not_false end