From 3951b5028281427cdf8f64ea7d7fdada77f8c210 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Apr 2015 17:30:37 -0700 Subject: [PATCH] feat(library/data/prod): define swap --- library/data/prod.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/library/data/prod.lean b/library/data/prod.lean index f43ff7e62b..c82a0018bc 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -27,4 +27,15 @@ namespace prod (assume H, H ▸ and.intro rfl rfl) (assume H, and.elim H (assume H₄ H₅, equal H₄ H₅)), decidable_of_decidable_of_iff _ (iff.symm H₃) + + definition swap {A : Type} : A × A → A × A + | (a, b) := (b, a) + + theorem swap_swap {A : Type} : ∀ p : A × A, swap (swap p) = p + | (a, b) := rfl + + theorem eq_of_swap_eq {A : Type} : ∀ p₁ p₂ : A × A, swap p₁ = swap p₂ → p₁ = p₂ := + take p₁ p₂, assume seqs, + assert h₁ : swap (swap p₁) = swap (swap p₂), from congr_arg swap seqs, + by rewrite *swap_swap at h₁; exact h₁ end prod