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

fix(hott): change some theorems to definitions

Browse source 
This ensures that the HoTT library compiles with the option --to_axiom
This commit is contained in:
Floris van Doorn 2015-12-17 14:42:30 -05:00 committed by Leonardo de Moura
parent c852f7bc71
commit 74366aa061
2 changed files with 31 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
hott/algebra/order.hlean
View file

@ -23,24 +23,24 @@ section
variable [s : weak_order A]
include s
theorem le.refl (a : A) : a ≤ a := !weak_order.le_refl
definition le.refl (a : A) : a ≤ a := !weak_order.le_refl
theorem le_of_eq {a b : A} (H : a = b) : a ≤ b := H ▸ le.refl a
definition le_of_eq {a b : A} (H : a = b) : a ≤ b := H ▸ le.refl a
theorem le.trans [trans] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
definition le.trans [trans] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
theorem ge.trans [trans] {a b c : A} (H1 : a ≥ b) (H2: b ≥ c) : a ≥ c := le.trans H2 H1
definition ge.trans [trans] {a b c : A} (H1 : a ≥ b) (H2: b ≥ c) : a ≥ c := le.trans H2 H1
theorem le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
definition le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
-- Alternate syntax. (Abbreviations do not migrate well.)
theorem eq_of_le_of_ge {a b : A} : a ≤ b → b ≤ a → a = b := !le.antisymm
definition eq_of_le_of_ge {a b : A} : a ≤ b → b ≤ a → a = b := !le.antisymm
end
structure linear_weak_order [class] (A : Type) extends weak_order A :=
(le_total : Πa b, le a b ⊎ le b a)
theorem le.total [s : linear_weak_order A] (a b : A) : a ≤ b ⊎ b ≤ a :=
definition le.total [s : linear_weak_order A] (a b : A) : a ≤ b ⊎ b ≤ a :=
!linear_weak_order.le_total
/- strict orders -/
@ -53,15 +53,15 @@ section
variable [s : strict_order A]
include s
theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
theorem not_lt_self (a : A) : ¬ a < a := !lt.irrefl -- alternate syntax
definition lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
definition not_lt_self (a : A) : ¬ a < a := !lt.irrefl -- alternate syntax
theorem lt_self_iff_empty (a : A) : a < a ↔ empty :=
iff_empty_intro (lt.irrefl a)
theorem lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
definition lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
theorem gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
definition gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
theorem ne_of_lt {a b : A} (lt_ab : a < b) : a ≠ b :=
assume eq_ab : a = b,
@ -98,13 +98,13 @@ section
variables {a b c : A}
include s
theorem le_of_lt : a < b → a ≤ b := !order_pair.le_of_lt
definition le_of_lt : a < b → a ≤ b := !order_pair.le_of_lt
theorem lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c := !order_pair.lt_of_lt_of_le
definition lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c := !order_pair.lt_of_lt_of_le
theorem lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c := !order_pair.lt_of_le_of_lt
definition lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c := !order_pair.lt_of_le_of_lt
private theorem lt_irrefl (s' : order_pair A) (a : A) : ¬ a < a := !order_pair.lt_irrefl
private definition lt_irrefl (s' : order_pair A) (a : A) : ¬ a < a := !order_pair.lt_irrefl
private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
lt_of_lt_of_le lt_ab (le_of_lt lt_bc)
@ -112,9 +112,9 @@ section
definition order_pair.to_strict_order [trans_instance] [reducible] : strict_order A :=
⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
definition gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
theorem gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
definition gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
theorem not_le_of_gt (H : a > b) : ¬ a ≤ b :=
assume H1 : a ≤ b,
@ -129,7 +129,7 @@ structure strong_order_pair [class] (A : Type) extends weak_order A, has_lt A :=
(le_iff_lt_sum_eq : Πa b, le a b ↔ lt a b ⊎ a = b)
(lt_irrefl : Π a, ¬ lt a a)
theorem le_iff_lt_sum_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ⊎ a = b :=
definition le_iff_lt_sum_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ⊎ a = b :=
!strong_order_pair.le_iff_lt_sum_eq
theorem lt_sum_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ⊎ a = b :=
@ -138,7 +138,7 @@ iff.mp le_iff_lt_sum_eq le_ab
theorem le_of_lt_sum_eq [s : strong_order_pair A] {a b : A} (lt_sum_eq : a < b ⊎ a = b) : a ≤ b :=
iff.mpr le_iff_lt_sum_eq lt_sum_eq
private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a :=
private definition lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a :=
!strong_order_pair.lt_irrefl
private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b :=

24
hott/init/nat.hlean
View file

@ -43,7 +43,7 @@ namespace nat
definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
protected lemma le_refl [refl] : Π a : nat, a ≤ a :=
protected definition le_refl [refl] : Π a : nat, a ≤ a :=
le.nat_refl
protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
@ -83,28 +83,28 @@ namespace nat
/- properties of inequality -/
protected theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !nat.le_refl
protected definition le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !nat.le_refl
theorem le_succ (n : ℕ) : n ≤ succ n := le.step !nat.le_refl
definition le_succ (n : ℕ) : n ≤ succ n := le.step !nat.le_refl
theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;repeat constructor
definition pred_le (n : ℕ) : pred n ≤ n := by cases n;repeat constructor
theorem le_succ_iff_unit [simp] (n : ℕ) : n ≤ succ n ↔ unit :=
definition le_succ_iff_unit [simp] (n : ℕ) : n ≤ succ n ↔ unit :=
iff_unit_intro (le_succ n)
theorem pred_le_iff_unit [simp] (n : ℕ) : pred n ≤ n ↔ unit :=
definition pred_le_iff_unit [simp] (n : ℕ) : pred n ≤ n ↔ unit :=
iff_unit_intro (pred_le n)
protected theorem le_trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
protected definition le_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 := nat.le_trans H !le_succ
definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := nat.le_trans H !le_succ
theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := nat.le_trans !le_succ H
definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := nat.le_trans !le_succ H
protected theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
protected definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
definition succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
le.rec !nat.le_refl (λa b, le.step)
theorem pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
@ -128,7 +128,7 @@ namespace nat
theorem succ_le_self_iff_empty [simp] (n : ℕ) : succ n ≤ n ↔ empty :=
iff_empty_intro not_succ_le_self
theorem zero_le : Π (n : ℕ), 0 ≤ n :=
definition zero_le : Π (n : ℕ), 0 ≤ n :=
nat.rec !nat.le_refl (λa, le.step)
theorem zero_le_iff_unit [simp] (n : ℕ) : 0 ≤ n ↔ unit :=