From 86591c7272a3d989eaa04b34296c2e5419f1fa8b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Oct 2014 13:38:08 -0700 Subject: [PATCH] refactor(library/data/prod): cleanup --- library/data/int/basic.lean | 10 +++---- library/data/nat/div.lean | 2 +- library/data/prod.lean | 52 ++++++++++++++++++--------------- library/data/quotient/util.lean | 18 ++++++------ 4 files changed, 43 insertions(+), 39 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 01c51be12..8d6e89710 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -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 diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 423c92767..a633584e5 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -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 diff --git a/library/data/prod.lean b/library/data/prod.lean index 4e4931a04..3b78f571b 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -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 diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean index ca109f903..8c7b5c96c 100644 --- a/library/data/quotient/util.lean +++ b/library/data/quotient/util.lean @@ -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) :=