feaf(library): make sure basic standard library can be compiled with option "--to_axiom"
We use this option to erase proofs when generating the javascript version. The proofs are erased to minimize the size of the file that must be downloaded by users
This commit is contained in:
Leonardo de Moura
parent
82836fe9e0
commit
88c659c54e
10 changed files with 67 additions and 74 deletions
|
|
@ -318,8 +318,7 @@ section discrete_linear_ordered_field
|
|||
variables [s : discrete_linear_ordered_field A] {a b c : A}
|
||||
include s
|
||||
|
||||
|
||||
theorem dec_eq_of_dec_lt : ∀ x y : A, decidable (x = y) :=
|
||||
definition dec_eq_of_dec_lt : ∀ x y : A, decidable (x = y) :=
|
||||
take x y,
|
||||
decidable.by_cases
|
||||
(assume H : x < y, decidable.inr (ne_of_lt H))
|
||||
|
|
@ -329,8 +328,6 @@ section discrete_linear_ordered_field
|
|||
(assume H' : ¬ y < x,
|
||||
decidable.inl (le.antisymm (le_of_not_gt H') (le_of_not_gt H))))
|
||||
|
||||
reveal dec_eq_of_dec_lt
|
||||
|
||||
definition discrete_linear_ordered_field.to_discrete_field [trans-instance] [reducible] [coercion]
|
||||
: discrete_field A :=
|
||||
⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ namespace is_congruence
|
|||
|
||||
/- tools to build instances -/
|
||||
|
||||
theorem compose
|
||||
definition compose
|
||||
{T2 : Type} {R2 : T2 → T2 → Prop}
|
||||
{T3 : Type} {R3 : T3 → T3 → Prop}
|
||||
{g : T2 → T3} (C2 : is_congruence R2 R3 g)
|
||||
|
|
@ -80,7 +80,7 @@ namespace is_congruence
|
|||
is_congruence R1 R3 (λx, g (f x)) :=
|
||||
is_congruence.mk (λx1 x2 H, app C2 (app C1 H))
|
||||
|
||||
theorem compose21
|
||||
definition compose21
|
||||
{T2 : Type} {R2 : T2 → T2 → Prop}
|
||||
{T3 : Type} {R3 : T3 → T3 → Prop}
|
||||
{T4 : Type} {R4 : T4 → T4 → Prop}
|
||||
|
|
@ -91,19 +91,19 @@ namespace is_congruence
|
|||
is_congruence R1 R4 (λx, g (f1 x) (f2 x)) :=
|
||||
is_congruence.mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
|
||||
|
||||
theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
|
||||
definition const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
|
||||
⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
||||
is_congruence R1 R2 (λu : T1, c) :=
|
||||
is_congruence.mk (λx y H1, H c)
|
||||
|
||||
end is_congruence
|
||||
|
||||
theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
definition congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
[C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
||||
is_congruence R1 R2 (λu : T1, c) :=
|
||||
is_congruence.const R2 (is_reflexive.refl R2) R1 c
|
||||
|
||||
theorem congruence_trivial [instance] {T : Type} (R : T → T → Prop) :
|
||||
definition congruence_trivial [instance] {T : Type} (R : T → T → Prop) :
|
||||
is_congruence R R (λu, u) :=
|
||||
is_congruence.mk (λx y H, H)
|
||||
|
||||
|
|
|
|||
|
|
@ -6,15 +6,13 @@ Author: Jeremy Avigad, Floris van Doorn
|
|||
import logic.cast
|
||||
|
||||
namespace empty
|
||||
protected theorem elim (A : Type) : empty → A :=
|
||||
protected definition elim (A : Type) : empty → A :=
|
||||
empty.rec (λe, A)
|
||||
|
||||
protected theorem subsingleton [instance] : subsingleton empty :=
|
||||
protected definition subsingleton [instance] : subsingleton empty :=
|
||||
subsingleton.intro (λ a b, !empty.elim a)
|
||||
end empty
|
||||
|
||||
reveal empty.elim
|
||||
|
||||
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
|
||||
take (a b : empty), decidable.inl (!empty.elim a)
|
||||
|
||||
|
|
|
|||
|
|
@ -27,66 +27,66 @@ namespace ops
|
|||
postfix `⁻¹` := inverse
|
||||
end ops
|
||||
|
||||
protected theorem refl [refl] (A : Type) : A ≃ A :=
|
||||
protected definition refl [refl] (A : Type) : A ≃ A :=
|
||||
mk (@id A) (@id A) (λ x, rfl) (λ x, rfl)
|
||||
|
||||
protected theorem symm [symm] {A B : Type} : A ≃ B → B ≃ A
|
||||
protected definition symm [symm] {A B : Type} : A ≃ B → B ≃ A
|
||||
| (mk f g h₁ h₂) := mk g f h₂ h₁
|
||||
|
||||
protected theorem trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A ≃ C
|
||||
protected definition trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A ≃ C
|
||||
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
|
||||
mk (f₂ ∘ f₁) (g₁ ∘ g₂)
|
||||
(show ∀ x, g₁ (g₂ (f₂ (f₁ x))) = x, by intros; rewrite [l₂, l₁])
|
||||
(show ∀ x, f₂ (f₁ (g₁ (g₂ x))) = x, by intros; rewrite [r₁, r₂])
|
||||
(show ∀ x, g₁ (g₂ (f₂ (f₁ x))) = x, by intros; rewrite [l₂, l₁]; reflexivity)
|
||||
(show ∀ x, f₂ (f₁ (g₁ (g₂ x))) = x, by intros; rewrite [r₁, r₂]; reflexivity)
|
||||
|
||||
lemma false_equiv_empty : empty ≃ false :=
|
||||
definition false_equiv_empty : empty ≃ false :=
|
||||
mk (λ e, empty.rec _ e) (λ h, false.rec _ h) (λ e, empty.rec _ e) (λ h, false.rec _ h)
|
||||
|
||||
lemma arrow_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
|
||||
definition arrow_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
|
||||
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
|
||||
mk
|
||||
(λ (h : A₁ → B₁) (a : A₂), f₂ (h (g₁ a)))
|
||||
(λ (h : A₂ → B₂) (a : A₁), g₂ (h (f₁ a)))
|
||||
(λ h, funext (λ a, by rewrite [l₁, l₂]))
|
||||
(λ h, funext (λ a, by rewrite [r₁, r₂]))
|
||||
(λ h, funext (λ a, by rewrite [l₁, l₂]; reflexivity))
|
||||
(λ h, funext (λ a, by rewrite [r₁, r₂]; reflexivity))
|
||||
|
||||
section
|
||||
open unit
|
||||
lemma arrow_unit_equiv_unit [simp] (A : Type) : (A → unit) ≃ unit :=
|
||||
definition arrow_unit_equiv_unit [simp] (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 [simp] (A : Type) : (unit → A) ≃ A :=
|
||||
definition unit_arrow_equiv [simp] (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 [simp] (A : Type) : (empty → A) ≃ unit :=
|
||||
definition empty_arrow_equiv_unit [simp] (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 [simp] (A : Type) : (false → A) ≃ unit :=
|
||||
definition false_arrow_equiv_unit [simp] (A : Type) : (false → A) ≃ unit :=
|
||||
calc (false → A) ≃ (empty → A) : arrow_congr false_equiv_empty !equiv.refl
|
||||
... ≃ unit : empty_arrow_equiv_unit
|
||||
end
|
||||
|
||||
lemma prod_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ × B₁) ≃ (A₂ × B₂)
|
||||
definition prod_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ × B₁) ≃ (A₂ × B₂)
|
||||
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
|
||||
mk
|
||||
(λ p, match p with (a₁, b₁) := (f₁ a₁, f₂ b₁) end)
|
||||
(λ p, match p with (a₂, b₂) := (g₁ a₂, g₂ b₂) end)
|
||||
(λ p, begin cases p, esimp, rewrite [l₁, l₂] end)
|
||||
(λ p, begin cases p, esimp, rewrite [r₁, r₂] end)
|
||||
(λ p, begin cases p, esimp, rewrite [l₁, l₂], reflexivity end)
|
||||
(λ p, begin cases p, esimp, rewrite [r₁, r₂], reflexivity end)
|
||||
|
||||
lemma prod_comm [simp] (A B : Type) : (A × B) ≃ (B × A) :=
|
||||
definition prod_comm [simp] (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 [simp] (A B C : Type) : ((A × B) × C) ≃ (A × (B × C)) :=
|
||||
definition prod_assoc [simp] (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)
|
||||
|
|
@ -94,97 +94,97 @@ mk (λ t, match t with ((a, b), c) := (a, (b, c)) end)
|
|||
|
||||
section
|
||||
open unit prod.ops
|
||||
lemma prod_unit_right [simp] (A : Type) : (A × unit) ≃ A :=
|
||||
definition prod_unit_right [simp] (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 [simp] (A : Type) : (unit × A) ≃ A :=
|
||||
definition prod_unit_left [simp] (A : Type) : (unit × A) ≃ A :=
|
||||
calc (unit × A) ≃ (A × unit) : prod_comm
|
||||
... ≃ A : prod_unit_right
|
||||
|
||||
lemma prod_empty_right [simp] (A : Type) : (A × empty) ≃ empty :=
|
||||
definition prod_empty_right [simp] (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 [simp] (A : Type) : (empty × A) ≃ empty :=
|
||||
definition prod_empty_left [simp] (A : Type) : (empty × A) ≃ empty :=
|
||||
calc (empty × A) ≃ (A × empty) : prod_comm
|
||||
... ≃ empty : prod_empty_right
|
||||
end
|
||||
|
||||
section
|
||||
open sum
|
||||
lemma sum_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ + B₁) ≃ (A₂ + B₂)
|
||||
definition sum_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ + B₁) ≃ (A₂ + B₂)
|
||||
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
|
||||
mk
|
||||
(λ s, match s with inl a₁ := inl (f₁ a₁) | inr b₁ := inr (f₂ b₁) end)
|
||||
(λ s, match s with inl a₂ := inl (g₁ a₂) | inr b₂ := inr (g₂ b₂) end)
|
||||
(λ s, begin cases s, {esimp, rewrite l₁}, {esimp, rewrite l₂} end)
|
||||
(λ s, begin cases s, {esimp, rewrite r₁}, {esimp, rewrite r₂} end)
|
||||
(λ s, begin cases s, {esimp, rewrite l₁, reflexivity}, {esimp, rewrite l₂, reflexivity} end)
|
||||
(λ s, begin cases s, {esimp, rewrite r₁, reflexivity}, {esimp, rewrite r₂, reflexivity} end)
|
||||
|
||||
open bool unit
|
||||
lemma bool_equiv_unit_sum_unit : bool ≃ (unit + unit) :=
|
||||
definition bool_equiv_unit_sum_unit : bool ≃ (unit + unit) :=
|
||||
mk (λ b, match b with tt := inl star | ff := inr star end)
|
||||
(λ s, match s with inl star := tt | inr star := ff 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 [simp] (A B : Type) : (A + B) ≃ (B + A) :=
|
||||
definition sum_comm [simp] (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 [simp] (A B C : Type) : ((A + B) + C) ≃ (A + (B + C)) :=
|
||||
definition sum_assoc [simp] (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 [simp] (A : Type) : (A + empty) ≃ A :=
|
||||
definition sum_empty_right [simp] (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 [simp] (A : Type) : (empty + A) ≃ A :=
|
||||
definition sum_empty_left [simp] (A : Type) : (empty + A) ≃ A :=
|
||||
calc (empty + A) ≃ (A + empty) : sum_comm
|
||||
... ≃ A : sum_empty_right
|
||||
end
|
||||
|
||||
section
|
||||
open prod.ops
|
||||
lemma arrow_prod_equiv_prod_arrow (A B C : Type) : (C → A × B) ≃ ((C → A) × (C → B)) :=
|
||||
definition arrow_prod_equiv_prod_arrow (A B C : Type) : (C → A × B) ≃ ((C → A) × (C → B)) :=
|
||||
mk (λ f, (λ c, (f c).1, λ c, (f c).2))
|
||||
(λ p, λ c, (p.1 c, p.2 c))
|
||||
(λ f, funext (λ c, begin esimp, cases f c, esimp end))
|
||||
(λ p, begin cases p, esimp end)
|
||||
|
||||
lemma arrow_arrow_equiv_prod_arrow (A B C : Type) : (A → B → C) ≃ (A × B → C) :=
|
||||
definition arrow_arrow_equiv_prod_arrow (A B C : Type) : (A → B → C) ≃ (A × B → C) :=
|
||||
mk (λ f, λ p, f p.1 p.2)
|
||||
(λ f, λ a b, f (a, b))
|
||||
(λ f, rfl)
|
||||
(λ f, funext (λ p, begin cases p, esimp end))
|
||||
|
||||
open sum
|
||||
lemma sum_arrow_equiv_prod_arrow (A B C : Type) : ((A + B) → C) ≃ ((A → C) × (B → C)) :=
|
||||
definition sum_arrow_equiv_prod_arrow (A B C : Type) : ((A + B) → C) ≃ ((A → C) × (B → C)) :=
|
||||
mk (λ f, (λ a, f (inl a), λ b, f (inr b)))
|
||||
(λ p, (λ s, match s with inl a := p.1 a | inr b := p.2 b end))
|
||||
(λ f, funext (λ s, begin cases s, esimp, esimp end))
|
||||
(λ p, begin cases p, esimp end)
|
||||
|
||||
lemma sum_prod_distrib (A B C : Type) : ((A + B) × C) ≃ ((A × C) + (B × C)) :=
|
||||
definition sum_prod_distrib (A B C : Type) : ((A + B) × C) ≃ ((A × C) + (B × C)) :=
|
||||
mk (λ p, match p with (inl a, c) := inl (a, c) | (inr b, c) := inr (b, c) end)
|
||||
(λ s, match s with inl (a, c) := (inl a, c) | inr (b, c) := (inr b, c) end)
|
||||
(λ p, begin cases p with ab c, cases ab, repeat esimp end)
|
||||
(λ s, begin cases s with ac bc, cases ac, esimp, cases bc, esimp end)
|
||||
|
||||
lemma prod_sum_distrib (A B C : Type) : (A × (B + C)) ≃ ((A × B) + (A × C)) :=
|
||||
definition prod_sum_distrib (A B C : Type) : (A × (B + C)) ≃ ((A × B) + (A × C)) :=
|
||||
calc (A × (B + C)) ≃ ((B + C) × A) : prod_comm
|
||||
... ≃ ((B × A) + (C × A)) : sum_prod_distrib
|
||||
... ≃ ((A × B) + (A × C)) : sum_congr !prod_comm !prod_comm
|
||||
|
||||
lemma bool_prod_equiv_sum (A : Type) : (bool × A) ≃ (A + A) :=
|
||||
definition bool_prod_equiv_sum (A : Type) : (bool × A) ≃ (A + A) :=
|
||||
calc (bool × A) ≃ ((unit + unit) × A) : prod_congr bool_equiv_unit_sum_unit !equiv.refl
|
||||
... ≃ (A × (unit + unit)) : prod_comm
|
||||
... ≃ ((A × unit) + (A × unit)) : prod_sum_distrib
|
||||
|
|
@ -193,29 +193,29 @@ end
|
|||
|
||||
section
|
||||
open sum nat unit prod.ops
|
||||
lemma nat_equiv_nat_sum_unit : nat ≃ (nat + unit) :=
|
||||
definition nat_equiv_nat_sum_unit : nat ≃ (nat + unit) :=
|
||||
mk (λ n, match n with zero := inr star | succ a := inl a end)
|
||||
(λ s, match s with inl n := succ n | inr star := zero 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 [simp] : (nat + unit) ≃ nat :=
|
||||
definition nat_sum_unit_equiv_nat [simp] : (nat + unit) ≃ nat :=
|
||||
equiv.symm nat_equiv_nat_sum_unit
|
||||
|
||||
lemma nat_prod_nat_equiv_nat [simp] : (nat × nat) ≃ nat :=
|
||||
definition nat_prod_nat_equiv_nat [simp] : (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 [simp] : (nat + bool) ≃ nat :=
|
||||
definition nat_sum_bool_equiv_nat [simp] : (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 [simp] : (nat + nat) ≃ nat :=
|
||||
definition nat_sum_nat_equiv_nat [simp] : (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
|
||||
|
|
@ -235,7 +235,7 @@ mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end)
|
|||
mul_div_cancel' (dvd_of_even (even_of_odd_succ (odd_of_not_even h)))]}
|
||||
end))
|
||||
|
||||
lemma prod_equiv_of_equiv_nat {A : Type} : A ≃ nat → (A × A) ≃ A :=
|
||||
definition prod_equiv_of_equiv_nat {A : Type} : A ≃ nat → (A × A) ≃ A :=
|
||||
take e, calc
|
||||
(A × A) ≃ (nat × nat) : prod_congr e e
|
||||
... ≃ nat : nat_prod_nat_equiv_nat
|
||||
|
|
|
|||
|
|
@ -284,8 +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 !zero_mod
|
||||
(take n, !mul_zero ▸ !mul_one ▸ !mul_mod_mul_left)
|
||||
nat.cases_on n (by rewrite zero_mod)
|
||||
(take n, by rewrite [-zero_add (succ n) at {1}, add_mod_self])
|
||||
|
||||
theorem mul_mod_eq_mod_mul_mod (m n k : nat) : (m * n) mod k = ((m mod k) * n) mod k :=
|
||||
calc
|
||||
|
|
@ -301,7 +301,8 @@ 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 :=
|
||||
!mul_one ▸ (!mul_div_mul_left H)
|
||||
assert (n * 1) div (n * 1) = 1 div 1, from !mul_div_mul_left H,
|
||||
by rewrite [div_one at this, -this, *mul_one]
|
||||
|
||||
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]
|
||||
|
|
|
|||
|
|
@ -290,9 +290,8 @@ lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j :=
|
|||
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 :=
|
||||
nat.rec (λm, not.elim !not_lt_zero)
|
||||
nat.rec (λm h, absurd h !not_lt_zero)
|
||||
(λn' (IH : ∀ {m : ℕ}, m < n' → P m) m l,
|
||||
or.by_cases (lt_or_eq_of_le (le_of_lt_succ l))
|
||||
IH (λ e, eq.rec (H n' @IH) e⁻¹)) (succ n) n !lt_succ_self
|
||||
|
|
|
|||
|
|
@ -87,9 +87,9 @@ by_contradiction (suppose ¬ odd n,
|
|||
|
||||
lemma even_succ_of_odd {n} : odd n → even (succ n) :=
|
||||
suppose odd n,
|
||||
have n mod 2 = 1 mod 2, from mod_eq_of_odd this,
|
||||
have (n+1) mod 2 = 0, from add_mod_eq_add_mod_right 1 this,
|
||||
this
|
||||
assert n mod 2 = 1 mod 2, from mod_eq_of_odd this,
|
||||
assert (n+1) mod 2 = 2 mod 2, from add_mod_eq_add_mod_right 1 this,
|
||||
by rewrite mod_self at this; exact this
|
||||
|
||||
lemma odd_succ_succ_of_odd {n} : odd n → odd (succ (succ n)) :=
|
||||
suppose odd n,
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ definition pnat := { n : ℕ | n > 0 }
|
|||
|
||||
notation `ℕ+` := pnat
|
||||
|
||||
theorem pos (n : ℕ) (H : n > 0) : ℕ+ := tag n H
|
||||
definition pos (n : ℕ) (H : n > 0) : ℕ+ := tag n H
|
||||
|
||||
definition nat_of_pnat (p : ℕ+) : ℕ := elt_of p
|
||||
reserve postfix `~`:std.prec.max_plus
|
||||
|
|
|
|||
|
|
@ -628,7 +628,7 @@ if c then true else false
|
|||
definition is_false (c : Prop) [H : decidable c] : Prop :=
|
||||
if c then false else true
|
||||
|
||||
theorem of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c :=
|
||||
definition of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c :=
|
||||
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, !false.rec (if_neg Hnc ▸ H₂))
|
||||
|
||||
notation `dec_trivial` := of_is_true trivial
|
||||
|
|
|
|||
|
|
@ -12,31 +12,29 @@ namespace relation
|
|||
|
||||
/- logical equivalence relations -/
|
||||
|
||||
theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
|
||||
definition is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
|
||||
relation.is_equivalence.mk (@eq.refl T) (@eq.symm T) (@eq.trans T)
|
||||
|
||||
theorem is_equivalence_iff [instance] : relation.is_equivalence iff :=
|
||||
definition is_equivalence_iff [instance] : relation.is_equivalence iff :=
|
||||
relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans
|
||||
|
||||
/- congruences for logic operations -/
|
||||
|
||||
theorem is_congruence_not : is_congruence iff iff not :=
|
||||
definition is_congruence_not : is_congruence iff iff not :=
|
||||
is_congruence.mk @congr_not
|
||||
|
||||
theorem is_congruence_and : is_congruence2 iff iff iff and :=
|
||||
definition is_congruence_and : is_congruence2 iff iff iff and :=
|
||||
is_congruence2.mk @congr_and
|
||||
|
||||
theorem is_congruence_or : is_congruence2 iff iff iff or :=
|
||||
definition is_congruence_or : is_congruence2 iff iff iff or :=
|
||||
is_congruence2.mk @congr_or
|
||||
|
||||
theorem is_congruence_imp : is_congruence2 iff iff iff imp :=
|
||||
definition is_congruence_imp : is_congruence2 iff iff iff imp :=
|
||||
is_congruence2.mk @congr_imp
|
||||
|
||||
theorem is_congruence_iff : is_congruence2 iff iff iff iff :=
|
||||
definition is_congruence_iff : is_congruence2 iff iff iff iff :=
|
||||
is_congruence2.mk @congr_iff
|
||||
|
||||
reveal is_congruence_not is_congruence_and is_congruence_or is_congruence_imp is_congruence_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
|
||||
definition is_congruence_or_compose [instance] := is_congruence.compose21 is_congruence_or
|
||||
|
|
|
|||
Loading…
Reference in a new issue