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

refactor(library/data): rename prod_ext and dpair_ext to prod.eta and sigma.eta

Browse source 
Reason: they will be generated automatically by definitional package.
This commit is contained in:
Leonardo de Moura 2014-11-03 08:29:05 -08:00
parent a2e75159c8
commit ae9d11c9c4
3 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/int/basic.lean
View file

@ -201,7 +201,7 @@ exists_intro (pr1 (rep a))
(exists_intro (pr2 (rep a)) (exists_intro (pr2 (rep a))
(calc (calc
a = psub (rep a) : (psub_rep a)⁻¹ a = psub (rep a) : (psub_rep a)⁻¹
... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹})) ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod.eta (rep a))⁻¹}))
-- TODO it should not be opaque. -- TODO it should not be opaque.
protected opaque definition has_decidable_eq [instance] : decidable_eq ℤ := protected opaque definition has_decidable_eq [instance] : decidable_eq ℤ :=
@ -312,7 +312,7 @@ or.imp_or (or.swap (proj_zero_or (rep a)))
exists_intro (pr1 (rep a)) exists_intro (pr1 (rep a))
(calc (calc
a = psub (rep a) : (psub_rep a)⁻¹ a = psub (rep a) : (psub_rep a)⁻¹
... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹} ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod.eta (rep a))⁻¹}
... = psub (pair (pr1 (rep a)) 0) : {H2} ... = psub (pair (pr1 (rep a)) 0) : {H2}
... = of_nat (pr1 (rep a)) : rfl)) ... = of_nat (pr1 (rep a)) : rfl))
(assume H : pr1 (proj (rep a)) = 0, (assume H : pr1 (proj (rep a)) = 0,
@ -320,7 +320,7 @@ or.imp_or (or.swap (proj_zero_or (rep a)))
exists_intro (pr2 (rep a)) exists_intro (pr2 (rep a))
(calc (calc
a = psub (rep a) : (psub_rep a)⁻¹ a = psub (rep a) : (psub_rep a)⁻¹
... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹} ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod.eta (rep a))⁻¹}
... = psub (pair 0 (pr2 (rep a))) : {H2} ... = psub (pair 0 (pr2 (rep a))) : {H2}
... = -(psub (pair (pr2 (rep a)) 0)) : by simp ... = -(psub (pair (pr2 (rep a)) 0)) : by simp
... = -(of_nat (pr2 (rep a))) : rfl)) ... = -(of_nat (pr2 (rep a))) : rfl))

2
library/data/prod.lean
View file

@ -37,7 +37,7 @@ namespace prod
theorem pr2.pair : pr₂ (a, b) = b := theorem pr2.pair : pr₂ (a, b) = b :=
rfl rfl
theorem prod_ext (p : prod A B) : pair (pr₁ p) (pr₂ p) = p := protected theorem eta (p : prod A B) : pair (pr₁ p) (pr₂ p) = p :=
destruct p (λx y, eq.refl (x, y)) destruct p (λx y, eq.refl (x, y))
variables {a₁ a₂ : A} {b₁ b₂ : B} variables {a₁ a₂ : A} {b₁ b₂ : B}

2
library/data/sigma.lean
View file

@ -22,7 +22,7 @@ namespace sigma
protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p := protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
rec H p rec H p
theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p := protected theorem eta (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
destruct p (take a b, rfl) destruct p (take a b, rfl)
theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) : theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) :