chore(hott): more cleanup.
Make zero and one reducible (see algebra/port.md) Change some theorems which need to compute into definitions
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
c968f920ba
commit
4ef58f1ba5
9 changed files with 71 additions and 115 deletions
|
|
@ -24,13 +24,13 @@ structure semigroup [class] (A : Type) extends has_mul A :=
|
|||
|
||||
attribute semigroup.is_hset_carrier [instance]
|
||||
|
||||
theorem mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
|
||||
definition mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
|
||||
!semigroup.mul_assoc
|
||||
|
||||
structure comm_semigroup [class] (A : Type) extends semigroup A :=
|
||||
(mul_comm : Πa b, mul a b = mul b a)
|
||||
|
||||
theorem mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
|
||||
definition mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
|
||||
!comm_semigroup.mul_comm
|
||||
|
||||
theorem mul.left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
|
||||
|
|
@ -51,7 +51,7 @@ abbreviation eq_of_mul_eq_mul_left' := @mul.left_cancel
|
|||
structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
|
||||
(mul_right_cancel : Πa b c, mul a b = mul c b → a = c)
|
||||
|
||||
theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
|
||||
definition mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
|
||||
a * b = c * b → a = c :=
|
||||
!right_cancel_semigroup.mul_right_cancel
|
||||
|
||||
|
|
@ -65,13 +65,13 @@ structure add_semigroup [class] (A : Type) extends has_add A :=
|
|||
|
||||
attribute add_semigroup.is_hset_carrier [instance]
|
||||
|
||||
theorem add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
|
||||
definition add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
|
||||
!add_semigroup.add_assoc
|
||||
|
||||
structure add_comm_semigroup [class] (A : Type) extends add_semigroup A :=
|
||||
(add_comm : Πa b, add a b = add b a)
|
||||
|
||||
theorem add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
|
||||
definition add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
|
||||
!add_comm_semigroup.add_comm
|
||||
|
||||
theorem add.left_comm [s : add_comm_semigroup A] (a b c : A) :
|
||||
|
|
@ -84,7 +84,7 @@ binary.right_comm (@add.comm A _) (@add.assoc A _) a b c
|
|||
structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
|
||||
(add_left_cancel : Πa b c, add a b = add a c → b = c)
|
||||
|
||||
theorem add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
|
||||
definition add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
|
||||
a + b = a + c → b = c :=
|
||||
!add_left_cancel_semigroup.add_left_cancel
|
||||
|
||||
|
|
@ -93,7 +93,7 @@ abbreviation eq_of_add_eq_add_left := @add.left_cancel
|
|||
structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
|
||||
(add_right_cancel : Πa b c, add a b = add c b → a = c)
|
||||
|
||||
theorem add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
|
||||
definition add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
|
||||
a + b = c + b → a = c :=
|
||||
!add_right_cancel_semigroup.add_right_cancel
|
||||
|
||||
|
|
@ -104,9 +104,9 @@ abbreviation eq_of_add_eq_add_right := @add.right_cancel
|
|||
structure monoid [class] (A : Type) extends semigroup A, has_one A :=
|
||||
(one_mul : Πa, mul one a = a) (mul_one : Πa, mul a one = a)
|
||||
|
||||
theorem one_mul [s : monoid A] (a : A) : 1 * a = a := !monoid.one_mul
|
||||
definition one_mul [s : monoid A] (a : A) : 1 * a = a := !monoid.one_mul
|
||||
|
||||
theorem mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one
|
||||
definition mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one
|
||||
|
||||
structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
|
||||
|
||||
|
|
@ -115,9 +115,9 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
|
|||
structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
|
||||
(zero_add : Πa, add zero a = a) (add_zero : Πa, add a zero = a)
|
||||
|
||||
theorem zero_add [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
|
||||
definition zero_add [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
|
||||
|
||||
theorem add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
|
||||
definition add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
|
||||
|
||||
structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
|
||||
|
||||
|
|
@ -160,7 +160,7 @@ section group
|
|||
variable [s : group A]
|
||||
include s
|
||||
|
||||
theorem mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
|
||||
definition mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
|
||||
|
||||
theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
|
||||
by rewrite [-mul.assoc, mul.left_inv, one_mul]
|
||||
|
|
|
|||
|
|
@ -3,9 +3,18 @@ We port a lot of algebra files from the standard library to the HoTT library.
|
|||
Port instructions:
|
||||
- use the script port.pl in scripts/ to port the file. e.g. execute the following in the `scripts` folder: `./port.pl ../library/algebra/lattice.lean ../hott/algebra/lattice.hlean`
|
||||
- remove imports starting with `data.` or `logic.` (sometimes you need to replace a `data.` import by the corresponding `types.` import)
|
||||
- All of the algebraic hierarchy is in the algebra namespace in the HoTT library.
|
||||
- Open namespaces `eq` and `algebra` if needed
|
||||
- (optional) add option `set_option class.force_new true`
|
||||
- fix all remaining errors. Typical errors include
|
||||
- Replacing "and" by "prod" in comments
|
||||
- and.intro is replaced by prod.intro, which should be prod.mk.
|
||||
|
||||
Currently, the following differences exist between the two libraries, relevant to porting:
|
||||
- All of the algebraic hierarchy is in the algebra namespace in the HoTT library (on top-level in the standard library).
|
||||
- The projections "zero" and "one" are reducible in HoTT. This was needed to allow type class inferences to infer
|
||||
```
|
||||
H : is_trunc 0 A |- is_trunc (succ (-1)) A
|
||||
H : is_trunc 1 A |- is_trunc (succ 0) A
|
||||
```
|
||||
- Projections of most algebraic structures are definitions instead of theorems in HoTT
|
||||
- Basic properties of `nat.add` have a simpler proof in HoTT (so that it computes better)
|
||||
|
|
@ -328,7 +328,7 @@ end
|
|||
structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A :=
|
||||
(eq_zero_sum_eq_zero_of_mul_eq_zero : Πa b, mul a b = zero → a = zero ⊎ b = zero)
|
||||
|
||||
theorem eq_zero_sum_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a b : A}
|
||||
definition eq_zero_sum_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a b : A}
|
||||
(H : a * b = 0) :
|
||||
a = 0 ⊎ b = 0 := !no_zero_divisors.eq_zero_sum_eq_zero_of_mul_eq_zero H
|
||||
|
||||
|
|
|
|||
|
|
@ -37,19 +37,6 @@ structure is_conditionally_constant [class] (f : A → B) :=
|
|||
(g : ∥A∥ → B)
|
||||
(eq : Π(a : A), f a = g (tr a))
|
||||
|
||||
-- structure is_retract (g : A → B) :=
|
||||
-- (X Y : Type)
|
||||
-- (f : X → Y)
|
||||
-- (s : A → X)
|
||||
-- (r : X → A)
|
||||
-- (s' : B → Y)
|
||||
-- (r' : Y → B)
|
||||
-- (R : Πa, r (s a) = a)
|
||||
-- (R' : Πb, r' (s' b) = b)
|
||||
-- (L : Πa, f (s a) = s' (g a))
|
||||
-- (K : Πx, g (r x) = r' (f x))
|
||||
-- (H : Πa, square (K (s a)) (R' (g a))⁻¹ (ap g (R a)) (ap r' (L a)))
|
||||
|
||||
namespace function
|
||||
|
||||
abbreviation sect [unfold 4] := @is_retraction.sect
|
||||
|
|
@ -198,40 +185,7 @@ namespace function
|
|||
is_constant.mk b (λv, by induction v with a p;exact p)
|
||||
|
||||
definition is_embedding_of_is_hprop_fiber [H : Π(b : B), is_hprop (fiber f b)] : is_embedding f :=
|
||||
begin
|
||||
intro a a',
|
||||
fapply adjointify,
|
||||
{ intro p, exact ap point (is_hprop.elim (fiber.mk a p) (fiber.mk a' idp))},
|
||||
{ exact abstract begin
|
||||
intro p, rewrite [-ap_compose],
|
||||
apply @is_constant.eq _ _ _ (is_constant_ap (f ∘ point) (fiber.mk a p) (fiber.mk a' idp))
|
||||
end end },
|
||||
{ intro p, induction p, rewrite [▸*,is_hprop_elim_self]},
|
||||
end
|
||||
|
||||
-- definition is_embedding_of_is_section_inv' [H : is_section f] {a : A} {b : B} (p : f a = b) :
|
||||
-- a = retr f b :=
|
||||
-- (left_inverse f a)⁻¹ ⬝ ap (retr f) p
|
||||
|
||||
-- definition is_embedding_of_is_section_inv [H : is_section f] {a a' : A} (p : f a = f a') :
|
||||
-- a = a' :=
|
||||
-- is_embedding_of_is_section_inv' f p ⬝ left_inverse f a'
|
||||
|
||||
-- definition is_embedding_of_is_section [constructor] [instance] [H : is_section f]
|
||||
-- : is_embedding f :=
|
||||
-- begin
|
||||
-- intro a a',
|
||||
-- fapply adjointify,
|
||||
-- { exact is_embedding_of_is_section_inv f},
|
||||
-- { exact abstract begin
|
||||
-- assert H2 : Π {b : B} (p : f a = b), ap f (is_embedding_of_is_section_inv' f p) = p ⬝ _,
|
||||
-- { }
|
||||
-- -- intro p, rewrite [+ap_con,-ap_compose],
|
||||
-- -- check_expr natural_square (left_inverse f),
|
||||
-- -- induction H with g q, esimp,
|
||||
-- end end },
|
||||
-- { intro p, induction p, esimp, apply con.left_inv},
|
||||
-- end
|
||||
is_embedding_of_is_hprop_fun _
|
||||
|
||||
definition is_retraction_of_is_equiv [instance] [H : is_equiv f] : is_retraction f :=
|
||||
is_retraction.mk f⁻¹ (right_inv f)
|
||||
|
|
@ -303,6 +257,8 @@ namespace function
|
|||
is_surjective_of_is_equiv
|
||||
is_equiv_equiv_is_embedding_times_is_surjective
|
||||
are in types.trunc
|
||||
|
||||
See types.arrow_2 for retractions
|
||||
-/
|
||||
|
||||
end function
|
||||
|
|
|
|||
|
|
@ -42,6 +42,11 @@ empty.rec _ H
|
|||
infix = := eq
|
||||
definition rfl {A : Type} {a : A} := eq.refl a
|
||||
|
||||
/-
|
||||
These notions are here only to make porting from the standard library easier.
|
||||
They are defined again in init/path.hlean, and those definitions will be used
|
||||
throughout the HoTT-library. That's why the notation for eq below is only local.
|
||||
-/
|
||||
namespace eq
|
||||
variables {A : Type} {a b c : A}
|
||||
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@ structure has_dvd.{l} [class] (A : Type.{l}) : Type.{l+1} := (dvd : A → A →
|
|||
structure has_le.{l} [class] (A : Type.{l}) : Type.{l+1} := (le : A → A → Type.{l})
|
||||
structure has_lt.{l} [class] (A : Type.{l}) : Type.{l+1} := (lt : A → A → Type.{l})
|
||||
|
||||
definition zero [reducible] {A : Type} [s : has_zero A] : A:= has_zero.zero A
|
||||
definition one {A : Type} [s : has_one A] : A := has_one.one A
|
||||
definition zero [reducible] {A : Type} [s : has_zero A] : A := has_zero.zero A
|
||||
definition one [reducible] {A : Type} [s : has_one A] : A := has_one.one A
|
||||
definition add {A : Type} [s : has_add A] : A → A → A := has_add.add
|
||||
definition mul {A : Type} [s : has_mul A] : A → A → A := has_mul.mul
|
||||
definition sub {A : Type} [s : has_sub A] : A → A → A := has_sub.sub
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ Ported from Coq HoTT.
|
|||
prelude
|
||||
import .nat .logic .equiv .pathover
|
||||
open eq nat sigma unit
|
||||
set_option class.force_new true
|
||||
--set_option class.force_new true
|
||||
|
||||
namespace is_trunc
|
||||
|
||||
|
|
@ -42,10 +42,10 @@ namespace is_trunc
|
|||
notation `ℕ₋₂` := trunc_index
|
||||
|
||||
namespace trunc_index
|
||||
definition add (n m : trunc_index) : trunc_index :=
|
||||
definition add [reducible] (n m : trunc_index) : trunc_index :=
|
||||
trunc_index.rec_on m n (λ k l, l .+1)
|
||||
|
||||
definition leq (n m : trunc_index) : Type₀ :=
|
||||
definition leq [reducible] (n m : trunc_index) : Type₀ :=
|
||||
trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
|
||||
|
||||
definition has_le_trunc_index [instance] [reducible] : has_le trunc_index :=
|
||||
|
|
@ -106,10 +106,6 @@ namespace is_trunc
|
|||
(n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) :=
|
||||
is_trunc.mk (is_trunc.to_internal (n.+1) A x y)
|
||||
|
||||
definition is_trunc_eq_zero [instance] [priority 1250] [H : is_trunc 1 A] (x y : A)
|
||||
: is_hset (x = y) :=
|
||||
@is_trunc_eq A 0 H x y
|
||||
|
||||
/- contractibility -/
|
||||
|
||||
definition is_contr.mk (center : A) (center_eq : Π(a : A), center = a) : is_contr A :=
|
||||
|
|
@ -143,9 +139,6 @@ namespace is_trunc
|
|||
A H
|
||||
--in the proof the type of H is given explicitly to make it available for class inference
|
||||
|
||||
theorem is_trunc_succ_zero [instance] [priority 950] (A : Type) [H : is_hset A] : is_trunc 1 A :=
|
||||
!is_trunc_succ
|
||||
|
||||
theorem is_trunc_of_leq.{l} (A : Type.{l}) {n m : trunc_index} (Hnm : n ≤ m)
|
||||
[Hn : is_trunc n A] : is_trunc m A :=
|
||||
have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from
|
||||
|
|
|
|||
|
|
@ -70,7 +70,6 @@ end sum
|
|||
-- Product type
|
||||
-- ------------
|
||||
|
||||
|
||||
namespace prod
|
||||
|
||||
-- notation for n-ary tuples
|
||||
|
|
@ -154,10 +153,3 @@ namespace prod
|
|||
end
|
||||
|
||||
end prod
|
||||
|
||||
/- logic (ported from standard library as second half of logic file) -/
|
||||
|
||||
/- iff -/
|
||||
|
||||
variables {a b c d : Type}
|
||||
open prod sum unit
|
||||
|
|
|
|||
|
|
@ -103,48 +103,49 @@ general m
|
|||
|
||||
/- addition -/
|
||||
|
||||
protected theorem add_zero [simp] (n : ℕ) : n + 0 = n :=
|
||||
protected definition add_zero [simp] (n : ℕ) : n + 0 = n :=
|
||||
rfl
|
||||
|
||||
theorem add_succ [simp] (n m : ℕ) : n + succ m = succ (n + m) :=
|
||||
definition add_succ [simp] (n m : ℕ) : n + succ m = succ (n + m) :=
|
||||
rfl
|
||||
|
||||
protected theorem zero_add [simp] (n : ℕ) : 0 + n = n :=
|
||||
nat.rec_on n
|
||||
!nat.add_zero
|
||||
(take m IH, show 0 + succ m = succ m, from
|
||||
calc
|
||||
0 + succ m = succ (0 + m) : add_succ
|
||||
... = succ m : IH)
|
||||
protected definition zero_add [simp] (n : ℕ) : 0 + n = n :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
reflexivity,
|
||||
exact ap succ IH
|
||||
end
|
||||
|
||||
theorem succ_add [simp] (n m : ℕ) : (succ n) + m = succ (n + m) :=
|
||||
nat.rec_on m
|
||||
(!nat.add_zero ▸ !nat.add_zero)
|
||||
(take k IH, calc
|
||||
succ n + succ k = succ (succ n + k) : add_succ
|
||||
... = succ (succ (n + k)) : IH
|
||||
... = succ (n + succ k) : add_succ)
|
||||
definition succ_add [simp] (n m : ℕ) : (succ n) + m = succ (n + m) :=
|
||||
begin
|
||||
induction m with m IH,
|
||||
reflexivity,
|
||||
exact ap succ IH
|
||||
end
|
||||
|
||||
protected theorem add_comm [simp] (n m : ℕ) : n + m = m + n :=
|
||||
nat.rec_on m
|
||||
(by rewrite [nat.add_zero, nat.zero_add])
|
||||
(take k IH, calc
|
||||
n + succ k = succ (n+k) : add_succ
|
||||
... = succ (k + n) : IH
|
||||
... = succ k + n : succ_add)
|
||||
protected definition add_comm [simp] (n m : ℕ) : n + m = m + n :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ apply nat.zero_add},
|
||||
{ exact !succ_add ⬝ ap succ IH}
|
||||
end
|
||||
|
||||
theorem succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m :=
|
||||
!succ_add ⬝ !add_succ⁻¹
|
||||
protected definition add_add (n l k : ℕ) : n + l + k = n + (k + l) :=
|
||||
begin
|
||||
induction l with l IH,
|
||||
reflexivity,
|
||||
exact succ_add (n + l) k ⬝ ap succ IH
|
||||
end
|
||||
|
||||
protected theorem add_assoc [simp] (n m k : ℕ) : (n + m) + k = n + (m + k) :=
|
||||
nat.rec_on k
|
||||
(by rewrite +nat.add_zero)
|
||||
(take l IH,
|
||||
calc
|
||||
(n + m) + succ l = succ ((n + m) + l) : add_succ
|
||||
... = succ (n + (m + l)) : IH
|
||||
... = n + succ (m + l) : add_succ
|
||||
... = n + (m + succ l) : add_succ)
|
||||
definition succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m :=
|
||||
!succ_add
|
||||
|
||||
protected definition add_assoc [simp] (n m k : ℕ) : (n + m) + k = n + (m + k) :=
|
||||
begin
|
||||
induction k with k IH,
|
||||
reflexivity,
|
||||
exact ap succ IH
|
||||
end
|
||||
|
||||
protected theorem add_left_comm : Π (n m k : ℕ), n + (m + k) = m + (n + k) :=
|
||||
left_comm nat.add_comm nat.add_assoc
|
||||
|
|
|
|||
Loading…
Reference in a new issue