From b3cd3efbb4e200ba18964eb8115362db7156c570 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jul 2015 08:34:11 -0700 Subject: [PATCH] refactor(hott): fix "sorry"s at int/basic.hlean, and comment the remaining "sorry"s --- hott/algebra/binary.hlean | 6 ++ hott/algebra/category/adjoint.hlean | 5 +- .../category/constructions/comma.hlean | 9 ++- hott/hit/torus.hlean | 3 + hott/hit/two_quotient.hlean | 2 + hott/init/logic.hlean | 6 ++ hott/types/cubical/squareover.hlean | 3 +- hott/types/int/basic.hlean | 76 ++++++++++++------- hott/types/nat/basic.hlean | 3 + 9 files changed, 79 insertions(+), 34 deletions(-) diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean index 05471610cd..a58114540a 100644 --- a/hott/algebra/binary.hlean +++ b/hott/algebra/binary.hlean @@ -59,6 +59,12 @@ namespace binary (a*b)*c = a*(b*c) : H_assoc ... = a*(c*b) : H_comm ... = (a*c)*b : H_assoc + + theorem comm4 (a b c d : A) : a*b*(c*d) = a*c*(b*d) := + calc + a*b*(c*d) = a*b*c*d : H_assoc + ... = a*c*b*d : right_comm H_comm H_assoc + ... = a*c*(b*d) : H_assoc end section diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index c02c04885a..5e44dbe514 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -73,6 +73,7 @@ namespace category infix `⋍`:25 := equivalence -- \backsimeq or \equiv infix `≌`:25 := isomorphism -- \backcong or \iso +/- definition is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D) : is_hprop (is_left_adjoint F) := begin @@ -86,7 +87,7 @@ namespace category { apply sorry /-rewrite [assoc, -{((G (ε' d)) ∘ (η (G' d))) ∘ (G' (ε d))}(assoc)],-/ -- apply concat, apply (ap (λc, c ∘ η' _)), rewrite -assoc, apply idp }, ---/-rewrite [-nat_trans.assoc]-/apply sorry +-- rewrite [-nat_trans.assoc] apply sorry ---assoc (G (ε' d)) (η (G' d)) (G' (ε d)) { apply sorry}}, { apply sorry}, @@ -157,5 +158,5 @@ namespace category definition is_equiv_equivalence_of_eq (C D : Category) : is_equiv (@equivalence_of_eq C D) := sorry - +-/ end category diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean index 2d3dd637c0..a10aad4a21 100644 --- a/hott/algebra/category/constructions/comma.hlean +++ b/hott/algebra/category/constructions/comma.hlean @@ -46,9 +46,9 @@ namespace category end --TODO: remove. This is a different version where Hq is not in square brackets - definition eq_comp_inverse_of_comp_eq' {ob : Type} {C : precategory ob} {d c b : ob} {r : hom c d} - {q : hom b c} {x : hom b d} {Hq : is_iso q} (p : r ∘ q = x) : r = x ∘ q⁻¹ʰ := - sorry --eq_inverse_comp_of_comp_eq p + axiom eq_comp_inverse_of_comp_eq' {ob : Type} {C : precategory ob} {d c b : ob} {r : hom c d} + {q : hom b c} {x : hom b d} {Hq : is_iso q} (p : r ∘ q = x) : r = x ∘ q⁻¹ʰ + -- := sorry --eq_inverse_comp_of_comp_eq p definition comma_object_eq {x y : comma_object S T} (p : ob1 x = ob1 y) (q : ob2 x = ob2 y) (r : T (hom_of_eq q) ∘ mor x ∘ S (inv_of_eq p) = mor y) : x = y := @@ -158,6 +158,7 @@ namespace category strict_precategory (comma_object S T) := strict_precategory.mk (comma_category S T) !is_trunc_comma_object +/- --set_option pp.notation false definition is_univalent_comma (HA : is_univalent A) (HB : is_univalent B) : is_univalent (comma_category S T) := @@ -172,6 +173,6 @@ namespace category { apply sorry}, { apply sorry}, end - +-/ end category diff --git a/hott/hit/torus.hlean b/hott/hit/torus.hlean index 889ef24daf..b7ffb43a33 100644 --- a/hott/hit/torus.hlean +++ b/hott/hit/torus.hlean @@ -76,6 +76,8 @@ namespace torus (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 := !elim_incl1 +/- + TODO(Leo): uncomment after we finish elim_incl2 definition elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf) @@ -83,6 +85,7 @@ namespace torus (!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2)) (!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) := !elim_incl2 +-/ end torus diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index b44a5ee944..bd20aa8ed3 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -296,6 +296,7 @@ namespace two_quotient ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t := !elim_inclt --ap_e_closure_elim_h incl1 (elim_incl1 P2) t +/- --print elim theorem elim_incl2 {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') @@ -309,6 +310,7 @@ namespace two_quotient xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q)),▸*], exact sorry end +-/ end end two_quotient diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index af1ea7d8a9..8016656817 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -61,6 +61,12 @@ end eq definition congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ := eq.subst H₁ (eq.subst H₂ rfl) +theorem congr_arg {A B : Type} (a a' : A) (f : A → B) (Ha : a = a') : f a = f a' := +eq.subst Ha rfl + +theorem congr_arg2 {A B C : Type} (a a' : A) (b b' : B) (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := +eq.subst Ha (eq.subst Hb rfl) + section variables {A : Type} {a b c: A} open eq.ops diff --git a/hott/types/cubical/squareover.hlean b/hott/types/cubical/squareover.hlean index 21a7f841d1..4e6b79308a 100644 --- a/hott/types/cubical/squareover.hlean +++ b/hott/types/cubical/squareover.hlean @@ -81,6 +81,7 @@ namespace eq : squareover B (square_of_eq_top s) q₁₀ q₁₂ q₀₁ q₂₁ := by induction q₂₁; induction q₁₂; esimp at r;induction r;induction q₁₀;constructor +/- definition squareover_equiv_pathover (q₁₀ : b₀₀ =[p₁₀] b₂₀) (q₁₂ : b₀₂ =[p₁₂] b₂₂) (q₀₁ : b₀₀ =[p₀₁] b₀₂) (q₂₁ : b₂₀ =[p₂₁] b₂₂) : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁ ≃ q₁₀ ⬝o q₂₁ =[eq_of_square s₁₁] q₀₁ ⬝o q₁₂ := @@ -119,5 +120,5 @@ namespace eq (pathover_ap B f (apdo b p)) (change_path !ap_constant⁻¹ idpo)) : r =[p] r₂ := by induction p; esimp at s; apply pathover_idp_of_eq; apply eq_of_vdeg_squareover; exact s - +-/ end eq diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index 2e7f123c8f..e09199e26e 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -160,14 +160,13 @@ calc ... = pr2 q + pr1 p : !add.comm protected theorem int_equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r := -have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from - calc - pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by exact sorry +add.cancel_right (calc + pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : add.right_comm ... = pr2 p + pr1 q + pr2 r : {H1} - ... = pr2 p + (pr1 q + pr2 r) : by exact sorry + ... = pr2 p + (pr1 q + pr2 r) : add.assoc ... = pr2 p + (pr2 q + pr1 r) : {H2} - ... = pr2 p + pr1 r + pr2 q : by exact sorry, -show pr1 p + pr2 r = pr2 p + pr1 r, from add.cancel_right H3 + ... = pr2 p + pr2 q + pr1 r : add.assoc + ... = pr2 p + pr1 r + pr2 q : add.right_comm) definition int_equiv_int_equiv : is_equivalence int_equiv := is_equivalence.mk @int_equiv.refl @int_equiv.symm @int_equiv.trans @@ -339,11 +338,11 @@ int.cases_on a (take n',!repr_sub_nat_nat)) definition padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' := -calc - pr1 (padd p q) + pr2 (padd p' q') = pr1 p + pr2 p' + (pr1 q + pr2 q') : by exact sorry +calc pr1 p + pr1 q + (pr2 p' + pr2 q') + = pr1 p + pr2 p' + (pr1 q + pr2 q') : add.comm4 ... = pr2 p + pr1 p' + (pr1 q + pr2 q') : {Ha} ... = pr2 p + pr1 p' + (pr2 q + pr1 q') : {Hb} - ... = pr2 (padd p q) + pr1 (padd p' q') : by exact sorry + ... = pr2 p + pr2 q + (pr1 p' + pr1 q') : add.comm4 definition padd_comm (p q : ℕ × ℕ) : padd p q = padd q p := calc @@ -415,13 +414,19 @@ definition padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) := show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add.comm ▸ rfl definition padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p := -show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p, from by exact sorry +calc pr1 p + pr1 q + pr2 q + pr2 p + = pr1 p + (pr1 q + pr2 q) + pr2 p : nat.add.assoc + ... = pr1 p + (pr1 q + pr2 q + pr2 p) : nat.add.assoc + ... = pr1 p + (pr2 q + pr1 q + pr2 p) : nat.add.comm + ... = pr1 p + (pr2 q + pr2 p + pr1 q) : add.right_comm + ... = pr1 p + (pr2 p + pr2 q + pr1 q) : nat.add.comm + ... = pr2 p + pr2 q + pr1 q + pr1 p : nat.add.comm definition add.left_inv (a : ℤ) : -a + a = 0 := have H : repr (-a + a) ≡ repr 0, from calc repr (-a + a) ≡ padd (repr (neg a)) (repr a) : repr_add - ... ≡ padd (pneg (repr a)) (repr a) : sorry + ... = padd (pneg (repr a)) (repr a) : repr_neg ... ≡ repr 0 : padd_pneg, eq_of_repr_int_equiv_repr H @@ -508,19 +513,18 @@ int.cases_on a definition int_equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ} (H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm) : xa * xn + ya * yn + (xb * ym + yb * xm) = xa * yn + ya * xn + (xb * xm + yb * ym) := -have H3 : xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn)) - = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)), from - calc - xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn)) - = xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm)) - : by exact sorry - ... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : by exact sorry - ... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : by exact sorry - ... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym)) - : by exact sorry - ... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)) - : by exact sorry, -nat.add.cancel_right H3 +nat.add.cancel_right (calc + xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn)) + = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : add.comm4 + ... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : nat.add.comm + ... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : !congr_arg2 add.comm4 add.comm4 + ... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) + : by rewrite[-+mul.left_distrib,-+mul.right_distrib]; exact H1 ▸ H2 ▸ rfl + ... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : !congr_arg2 add.comm4 add.comm4 + ... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : !nat.add.comm ▸ !nat.add.comm ▸ rfl + ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*xm+yb*ym)) : add.comm4 + ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xm+yb*ym + (xb*xn+yb*yn)) : nat.add.comm + ... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : add.comm4) definition pmul_congr {p p' q q' : ℕ × ℕ} (H1 : p ≡ p') (H2 : q ≡ q') : pmul p q ≡ pmul p' q' := int_equiv_mul_prep H1 H2 @@ -541,8 +545,19 @@ eq_of_repr_int_equiv_repr ... = pmul (repr b) (repr a) : pmul_comm ... = repr (b * a) : repr_mul) ▸ !int_equiv.refl) +private theorem pmul_assoc_prep {p1 p2 q1 q2 r1 r2 : ℕ} : + ((p1*q1+p2*q2)*r1+(p1*q2+p2*q1)*r2, (p1*q1+p2*q2)*r2+(p1*q2+p2*q1)*r1) = + (p1*(q1*r1+q2*r2)+p2*(q1*r2+q2*r1), p1*(q1*r2+q2*r1)+p2*(q1*r1+q2*r2)) := +begin + rewrite[+mul.left_distrib,+mul.right_distrib,*mul.assoc], + rewrite (@add.comm4 (p1 * (q1 * r1)) (p2 * (q2 * r1)) (p1 * (q2 * r2)) (p2 * (q1 * r2))), + rewrite (nat.add.comm (p2 * (q2 * r1)) (p2 * (q1 * r2))), + rewrite (@add.comm4 (p1 * (q1 * r2)) (p2 * (q2 * r2)) (p1 * (q2 * r1)) (p2 * (q1 * r1))), + rewrite (nat.add.comm (p2 * (q2 * r2)) (p2 * (q1 * r1))) +end + definition pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) := -by exact sorry +pmul_assoc_prep definition mul.assoc (a b c : ℤ) : (a * b) * c = a * (b * c) := eq_of_repr_int_equiv_repr @@ -553,22 +568,29 @@ eq_of_repr_int_equiv_repr ... = pmul (repr a) (repr (b * c)) : repr_mul ... = repr (a * (b * c)) : repr_mul) ▸ !int_equiv.refl) +set_option pp.coercions true + definition mul_one (a : ℤ) : a * 1 = a := eq_of_repr_int_equiv_repr (int_equiv_of_eq ((calc repr (a * 1) = pmul (repr a) (repr 1) : repr_mul - ... = (pr1 (repr a), pr2 (repr a)) : by exact sorry + ... = (pr1 (repr a), pr2 (repr a)) : by unfold [pmul, repr]; krewrite [*mul_zero, *mul_one, *nat.add_zero, *nat.zero_add] ... = repr a : prod.eta))) definition one_mul (a : ℤ) : 1 * a = a := mul.comm a 1 ▸ mul_one a +private theorem mul_distrib_prep {a1 a2 b1 b2 c1 c2 : ℕ} : + ((a1+b1)*c1+(a2+b2)*c2, (a1+b1)*c2+(a2+b2)*c1) = + (a1*c1+a2*c2+(b1*c1+b2*c2), a1*c2+a2*c1+(b1*c2+b2*c1)) := +by rewrite[+mul.right_distrib] ⬝ (!congr_arg2 !add.comm4 !add.comm4) + definition mul.right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c := eq_of_repr_int_equiv_repr (calc repr ((a + b) * c) = pmul (repr (a + b)) (repr c) : repr_mul ... ≡ pmul (padd (repr a) (repr b)) (repr c) : pmul_congr !repr_add int_equiv.refl - ... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : by exact sorry + ... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : mul_distrib_prep ... = padd (repr (a * c)) (pmul (repr b) (repr c)) : {(repr_mul a c)⁻¹} ... = padd (repr (a * c)) (repr (b * c)) : repr_mul ... ≡ repr (a * c + b * c) : int_equiv.symm !repr_add) diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean index ac14b70842..df664b300c 100644 --- a/hott/types/nat/basic.hlean +++ b/hott/types/nat/basic.hlean @@ -151,6 +151,9 @@ left_comm add.comm add.assoc n m k definition add.right_comm (n m k : ℕ) : n + m + k = n + k + m := right_comm add.comm add.assoc n m k +theorem add.comm4 : Π {n m k l : ℕ}, n + m + (k + l) = n + k + (m + l) := +comm4 add.comm add.assoc + definition add.cancel_left {n m k : ℕ} : n + m = n + k → m = k := nat.rec_on n (take H : 0 + m = 0 + k,