refactor(library/data/prod): cleanup
This commit is contained in:
Leonardo de Moura
parent
1306d08399
commit
86591c7272
4 changed files with 43 additions and 39 deletions
|
|
@ -7,7 +7,7 @@
|
|||
|
||||
-- The integers, with addition, multiplication, and subtraction.
|
||||
|
||||
import ..nat.basic ..nat.order ..nat.sub ..prod ..quotient ..quotient tools.tactic algebra.relation
|
||||
import data.nat.basic data.nat.order data.nat.sub data.prod data.quotient tools.tactic algebra.relation
|
||||
import algebra.binary
|
||||
import tools.fake_simplifier
|
||||
|
||||
|
|
@ -84,22 +84,22 @@ or.elim le_or_gt
|
|||
theorem proj_ge_pr1 {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : pr1 (proj a) = pr1 a - pr2 a :=
|
||||
calc
|
||||
pr1 (proj a) = pr1 (pair (pr1 a - pr2 a) 0) : {proj_ge H}
|
||||
... = pr1 a - pr2 a : pr1_pair (pr1 a - pr2 a) 0
|
||||
... = pr1 a - pr2 a : pr1.pair (pr1 a - pr2 a) 0
|
||||
|
||||
theorem proj_ge_pr2 {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : pr2 (proj a) = 0 :=
|
||||
calc
|
||||
pr2 (proj a) = pr2 (pair (pr1 a - pr2 a) 0) : {proj_ge H}
|
||||
... = 0 : pr2_pair (pr1 a - pr2 a) 0
|
||||
... = 0 : pr2.pair (pr1 a - pr2 a) 0
|
||||
|
||||
theorem proj_le_pr1 {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : pr1 (proj a) = 0 :=
|
||||
calc
|
||||
pr1 (proj a) = pr1 (pair 0 (pr2 a - pr1 a)) : {proj_le H}
|
||||
... = 0 : pr1_pair 0 (pr2 a - pr1 a)
|
||||
... = 0 : pr1.pair 0 (pr2 a - pr1 a)
|
||||
|
||||
theorem proj_le_pr2 {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : pr2 (proj a) = pr2 a - pr1 a :=
|
||||
calc
|
||||
pr2 (proj a) = pr2 (pair 0 (pr2 a - pr1 a)) : {proj_le H}
|
||||
... = pr2 a - pr1 a : pr2_pair 0 (pr2 a - pr1 a)
|
||||
... = pr2 a - pr1 a : pr2.pair 0 (pr2 a - pr1 a)
|
||||
|
||||
theorem proj_flip (a : ℕ × ℕ) : proj (flip a) = flip (proj a) :=
|
||||
have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from
|
||||
|
|
|
|||
|
|
@ -610,7 +610,7 @@ show lhs = rhs, from
|
|||
... = rhs : (if_pos H1)⁻¹)
|
||||
(assume H1 : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_imp_pos H1,
|
||||
have H2 : gcd_aux_measure p' = x mod y, from pr2_pair _ _,
|
||||
have H2 : gcd_aux_measure p' = x mod y, from pr2.pair _ _,
|
||||
have H3 : gcd_aux_measure p' < gcd_aux_measure p, from H2⁻¹ ▸ mod_lt ypos,
|
||||
calc
|
||||
lhs = g1 p' : if_neg H1
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ import logic.inhabited logic.eq logic.decidable
|
|||
-- data.prod
|
||||
-- =========
|
||||
|
||||
open inhabited decidable
|
||||
open inhabited decidable eq.ops
|
||||
|
||||
-- The cartesian product.
|
||||
inductive prod (A B : Type) : Type :=
|
||||
|
|
@ -21,39 +21,43 @@ notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
|
|||
namespace prod
|
||||
section
|
||||
parameters {A B : Type}
|
||||
|
||||
definition pr1 (p : prod A B) := rec (λ x y, x) p
|
||||
definition pr2 (p : prod A B) := rec (λ x y, y) p
|
||||
|
||||
theorem pr1_pair (a : A) (b : B) : pr1 (a, b) = a :=
|
||||
rfl
|
||||
|
||||
theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b :=
|
||||
rfl
|
||||
|
||||
protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
|
||||
rec H p
|
||||
|
||||
theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p :=
|
||||
definition pr1 (p : prod A B) := rec (λ x y, x) p
|
||||
definition pr2 (p : prod A B) := rec (λ x y, y) p
|
||||
notation `pr₁`:max := pr1
|
||||
notation `pr₂`:max := pr2
|
||||
|
||||
variables (a : A) (b : B)
|
||||
|
||||
theorem pr1.pair : pr₁ (a, b) = a :=
|
||||
rfl
|
||||
|
||||
theorem pr2.pair : pr₂ (a, b) = b :=
|
||||
rfl
|
||||
|
||||
theorem prod_ext (p : prod A B) : pair (pr₁ p) (pr₂ p) = p :=
|
||||
destruct p (λx y, eq.refl (x, y))
|
||||
|
||||
open eq.ops
|
||||
variables {a₁ a₂ : A} {b₁ b₂ : B}
|
||||
|
||||
theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
|
||||
H1 ▸ H2 ▸ rfl
|
||||
theorem pair_eq : a₁ = a₂ → b₁ = b₂ → (a₁, b₁) = (a₂, b₂) :=
|
||||
assume H1 H2, H1 ▸ H2 ▸ rfl
|
||||
|
||||
protected theorem equal {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
|
||||
destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
|
||||
protected theorem equal {p₁ p₂ : prod A B} : pr₁ p₁ = pr₁ p₂ → pr₂ p₁ = pr₂ p₂ → p₁ = p₂ :=
|
||||
destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, pair_eq H₁ H₂))
|
||||
|
||||
protected definition is_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
|
||||
inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b)))
|
||||
protected definition is_inhabited [instance] : inhabited A → inhabited B → inhabited (prod A B) :=
|
||||
take (H₁ : inhabited A) (H₂ : inhabited B),
|
||||
inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (pair a b)))
|
||||
|
||||
protected definition has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=
|
||||
take u v : A × B,
|
||||
have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
|
||||
protected definition has_decidable_eq [instance] : decidable_eq A → decidable_eq B → decidable_eq (A × B) :=
|
||||
take (H₁ : decidable_eq A) (H₂ : decidable_eq B) (u v : A × B),
|
||||
have H₃ : u = v ↔ (pr₁ u = pr₁ v) ∧ (pr₂ u = pr₂ v), from
|
||||
iff.intro
|
||||
(assume H, H ▸ and.intro rfl rfl)
|
||||
(assume H, and.elim H (assume H4 H5, equal H4 H5)),
|
||||
decidable_iff_equiv _ (iff.symm H3)
|
||||
(assume H, and.elim H (assume H₄ H₅, equal H₄ H₅)),
|
||||
decidable_iff_equiv _ (iff.symm H₃)
|
||||
end
|
||||
end prod
|
||||
|
|
|
|||
|
|
@ -47,13 +47,13 @@ rfl
|
|||
|
||||
theorem map_pair_pair {A B : Type} (f : A → B) (a a' : A)
|
||||
: map_pair f (pair a a') = pair (f a) (f a') :=
|
||||
(pr1_pair a a') ▸ (pr2_pair a a') ▸ (rfl)
|
||||
(pr1.pair a a') ▸ (pr2.pair a a') ▸ rfl
|
||||
|
||||
theorem map_pair_pr1 {A B : Type} (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) :=
|
||||
pr1_pair _ _
|
||||
!pr1.pair
|
||||
|
||||
theorem map_pair_pr2 {A B : Type} (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) :=
|
||||
pr2_pair _ _
|
||||
!pr2.pair
|
||||
|
||||
-- ### coordinatewise binary maps
|
||||
|
||||
|
|
@ -68,16 +68,16 @@ theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B)
|
|||
calc
|
||||
map_pair2 f (pair a a') (pair b b')
|
||||
= pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b')))
|
||||
: {pr1_pair b b'}
|
||||
... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2_pair b b'}
|
||||
... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2_pair a a'}
|
||||
... = pair (f a b) (f a' b') : {pr1_pair a a'}
|
||||
: {pr1.pair b b'}
|
||||
... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2.pair b b'}
|
||||
... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2.pair a a'}
|
||||
... = pair (f a b) (f a' b') : {pr1.pair a a'}
|
||||
|
||||
theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
|
||||
pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := pr1_pair _ _
|
||||
pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := !pr1.pair
|
||||
|
||||
theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
|
||||
pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := pr2_pair _ _
|
||||
pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := !pr2.pair
|
||||
|
||||
theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
|
||||
flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
|
||||
|
|
|
|||
Loading…
Reference in a new issue