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

refactor(hott): fix "sorry"s at int/basic.hlean, and comment the remaining "sorry"s

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-27 08:34:11 -07:00
parent 8c06803f54
commit b3cd3efbb4
9 changed files with 79 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
hott/algebra/binary.hlean
View file

@ -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

5
hott/algebra/category/adjoint.hlean
View file

@ -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

9
hott/algebra/category/constructions/comma.hlean
View file

@ -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

3
hott/hit/torus.hlean
View file

@ -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

2
hott/hit/two_quotient.hlean
View file

@ -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

6
hott/init/logic.hlean
View file

@ -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

3
hott/types/cubical/squareover.hlean
View file

@ -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

72
hott/types/int/basic.hlean
View file

@ -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
nat.add.cancel_right (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
= 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 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
: 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)

3
hott/types/nat/basic.hlean
View file

@ -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,