From 64327eb804ac593c1ec689c5a914581c1b34dd22 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 20 Jul 2017 15:13:43 +0100 Subject: [PATCH] fix precedence of ->* and some other small changes --- hott/algebra/inf_group.hlean | 23 ++++++++++------------- hott/init/pointed.hlean | 2 +- hott/types/nat/hott.hlean | 5 ++++- hott/types/pointed2.hlean | 4 ++-- library/data/int/order.lean | 4 ++-- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/hott/algebra/inf_group.hlean b/hott/algebra/inf_group.hlean index 5a8009b43..6823d23b6 100644 --- a/hott/algebra/inf_group.hlean +++ b/hott/algebra/inf_group.hlean @@ -141,17 +141,6 @@ definition add_comm_inf_semigroup_of_add_comm_inf_monoid [reducible] [trans_inst [H : add_comm_inf_monoid A] : add_comm_inf_semigroup A := @comm_inf_monoid.to_comm_inf_semigroup A H -section add_comm_inf_monoid - variables [s : add_comm_inf_monoid A] - include s - - theorem add_comm_three (a b c : A) : a + b + c = c + b + a := - by rewrite [{a + _}add.comm, {_ + c}add.comm, -*add.assoc] - - theorem add.comm4 : Π (n m k l : A), n + m + (k + l) = n + k + (m + l) := - comm4 add.comm add.assoc -end add_comm_inf_monoid - /- group -/ structure inf_group [class] (A : Type) extends inf_monoid A, has_inv A := @@ -609,8 +598,16 @@ namespace norm_num definition add1 [s : has_add A] [s' : has_one A] (a : A) : A := add a one -theorem add_comm_four [s : add_comm_inf_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) := - by rewrite [-add.assoc at {1}, add.comm, {a + b}add.comm at {1}, *add.assoc] +theorem add_comm_three [s : add_comm_inf_semigroup A] (a b c : A) : a + b + c = c + b + a := + by rewrite [{a + _}add.comm, {_ + c}add.comm, -*add.assoc] + +theorem add.comm4 [s : add_comm_inf_semigroup A] : + Π (n m k l : A), n + m + (k + l) = n + k + (m + l) := +comm4 add.comm add.assoc + +theorem add_comm_four [s : add_comm_inf_semigroup A] (a b : A) : + a + a + (b + b) = (a + b) + (a + b) := +!add.comm4 theorem add_comm_middle [s : add_comm_inf_semigroup A] (a b c : A) : a + b + c = a + c + b := by rewrite [add.assoc, add.comm b, -add.assoc] diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean index bde775b40..caa01ab1c 100644 --- a/hott/init/pointed.hlean +++ b/hott/init/pointed.hlean @@ -112,7 +112,7 @@ namespace pointed abbreviation respect_pt [unfold 3] := @pmap.resp_pt notation `map₊` := pmap - infix ` →* `:30 := pmap + infix ` →* `:28 := pmap attribute pmap.to_fun ppi_gen.to_fun [coercion] -- notation `Π*` binders `, ` r:(scoped P, ppi _ P) := r -- definition pmap.mk [constructor] {A B : Type*} (f : A → B) (p : f pt = pt) : A →* B := diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index 874883dbc..4cc9ac044 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -161,10 +161,13 @@ namespace nat attribute is_succ.mk [instance] + definition is_succ_1 [instance] : is_succ 1 := is_succ.mk 0 + definition is_succ_add_right [instance] [constructor] (n m : ℕ) [H : is_succ m] : is_succ (n+m) := by induction H with m; constructor - definition is_succ_add_left [instance] [constructor] (n m : ℕ) [H : is_succ n] : is_succ (n+m) := + definition is_succ_add_left [instance] [priority 900] [constructor] (n m : ℕ) [H : is_succ n] : + is_succ (n+m) := by induction H with n; cases m with m: constructor definition is_succ_bit0 [constructor] (n : ℕ) [H : is_succ n] : is_succ (bit0 n) := diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index c38b65ad7..faaf5c4aa 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -554,7 +554,7 @@ namespace pointed phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C := - phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ + phomotopy.mk (λa, rfl) !ap_constant⁻¹ definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C := pmap.mk (pcompose g) (eq_of_phomotopy (pcompose_pconst g)) @@ -562,7 +562,7 @@ namespace pointed definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C := pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f)) - /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof) -/ + /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof), rename to ppmap_pequiv_ppmap_right -/ definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := pequiv.MK' (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*) begin intro f, apply eq_of_phomotopy, apply pinv_pcompose_cancel_left end diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 81052110d..1ba1910da 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -313,10 +313,10 @@ theorem le_of_lt_add_one {a b : ℤ} (H : a < b + 1) : a ≤ b := have H1 : a + 1 ≤ b + 1, from add_one_le_of_lt H, le_of_add_le_add_right H1 -theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b := +theorem sub_one_lt_of_le {a b : ℤ} (H : a ≤ b) : a - 1 < b := lt_of_add_one_le (begin rewrite sub_add_cancel, exact H end) -theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b := +theorem le_of_sub_one_lt {a b : ℤ} (H : a - 1 < b) : a ≤ b := !sub_add_cancel ▸ add_one_le_of_lt H theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 :=