From 01ba0b474713ed85cb696efc0d830e9c0efd5554 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jul 2015 11:13:24 -0700 Subject: [PATCH] feat(library/logic/equiv): add equivalence between types This is a good test for the simplifier --- library/data/equiv.lean | 224 +++++++++++++++++++++++++++++++++++ library/data/nat/parity.lean | 16 +++ 2 files changed, 240 insertions(+) create mode 100644 library/data/equiv.lean diff --git a/library/data/equiv.lean b/library/data/equiv.lean new file mode 100644 index 000000000..a46fd23ef --- /dev/null +++ b/library/data/equiv.lean @@ -0,0 +1,224 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura + +In the standard library we cannot assume the univalence axiom. +We say two types are equivalent if they are isomorphic. +-/ +import data.sum data.nat +open function + +structure equiv (A B : Type) := + (to_fun : A → B) + (inv : B → A) + (left_inv : left_inverse inv to_fun) + (right_inv : right_inverse inv to_fun) + +namespace equiv + +infix `≃`:50 := equiv + +protected theorem refl [refl] (A : Type) : A ≃ A := +mk (@id A) (@id A) (λ x, rfl) (λ x, rfl) + +protected theorem symm [symm] {A B : Type} : A ≃ B → B ≃ A +| (mk f g h₁ h₂) := mk g f h₂ h₁ + +protected theorem trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A ≃ C +| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) := + mk (f₂ ∘ f₁) (g₁ ∘ g₂) + (show ∀ x, g₁ (g₂ (f₂ (f₁ x))) = x, by intros; rewrite [l₂, l₁]) + (show ∀ x, f₂ (f₁ (g₁ (g₂ x))) = x, by intros; rewrite [r₁, r₂]) + +lemma false_equiv_empty : empty ≃ false := +mk (λ e, empty.rec _ e) (λ h, false.rec _ h) (λ e, empty.rec _ e) (λ h, false.rec _ h) + +lemma arrow_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂) +| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) := + mk + (λ (h : A₁ → B₁) (a : A₂), f₂ (h (g₁ a))) + (λ (h : A₂ → B₂) (a : A₁), g₂ (h (f₁ a))) + (λ h, funext (λ a, by rewrite [l₁, l₂])) + (λ h, funext (λ a, by rewrite [r₁, r₂])) + +section +open unit +lemma arrow_unit_equiv_unit (A : Type) : (A → unit) ≃ unit := +mk (λ f, star) (λ u, (λ f, star)) + (λ f, funext (λ x, by cases (f x); reflexivity)) + (λ u, by cases u; reflexivity) + +lemma unit_arrow_equiv (A : Type) : (unit → A) ≃ A := +mk (λ f, f star) (λ a, (λ u, a)) + (λ f, funext (λ x, by cases x; reflexivity)) + (λ u, rfl) + +lemma empty_arrow_equiv_unit (A : Type) : (empty → A) ≃ unit := +mk (λ f, star) (λ u, λ e, empty.rec _ e) + (λ f, funext (λ x, empty.rec _ x)) + (λ u, by cases u; reflexivity) + +lemma false_arrow_equiv_unit (A : Type) : (false → A) ≃ unit := +calc (false → A) ≃ (empty → A) : arrow_congr false_equiv_empty !equiv.refl + ... ≃ unit : empty_arrow_equiv_unit +end + +lemma prod_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ × B₁) ≃ (A₂ × B₂) +| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) := + mk + (λ p, match p with (a₁, b₁) := (f₁ a₁, f₂ b₁) end) + (λ p, match p with (a₂, b₂) := (g₁ a₂, g₂ b₂) end) + (λ p, begin cases p, esimp, rewrite [l₁, l₂] end) + (λ p, begin cases p, esimp, rewrite [r₁, r₂] end) + +lemma prod_comm (A B : Type) : (A × B) ≃ (B × A) := +mk (λ p, match p with (a, b) := (b, a) end) + (λ p, match p with (b, a) := (a, b) end) + (λ p, begin cases p, esimp end) + (λ p, begin cases p, esimp end) + +lemma prod_assoc (A B C : Type) : ((A × B) × C) ≃ (A × (B × C)) := +mk (λ t, match t with ((a, b), c) := (a, (b, c)) end) + (λ t, match t with (a, (b, c)) := ((a, b), c) end) + (λ t, begin cases t with ab c, cases ab, esimp end) + (λ t, begin cases t with a bc, cases bc, esimp end) + +section +open unit prod.ops +lemma prod_unit_right (A : Type) : (A × unit) ≃ A := +mk (λ p, p.1) + (λ a, (a, star)) + (λ p, begin cases p with a u, cases u, esimp end) + (λ a, rfl) + +lemma prod_unit_left (A : Type) : (unit × A) ≃ A := +calc (unit × A) ≃ (A × unit) : prod_comm + ... ≃ A : prod_unit_right + +lemma prod_empty_right (A : Type) : (A × empty) ≃ empty := +mk (λ p, empty.rec _ p.2) (λ e, empty.rec _ e) (λ p, empty.rec _ p.2) (λ e, empty.rec _ e) + +lemma prod_empty_left (A : Type) : (empty × A) ≃ empty := +calc (empty × A) ≃ (A × empty) : prod_comm + ... ≃ empty : prod_empty_right +end + +section +open sum +lemma sum_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ + B₁) ≃ (A₂ + B₂) +| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) := + mk + (λ s, match s with inl a₁ := inl (f₁ a₁) | inr b₁ := inr (f₂ b₁) end) + (λ s, match s with inl a₂ := inl (g₁ a₂) | inr b₂ := inr (g₂ b₂) end) + (λ s, begin cases s, {esimp, rewrite l₁}, {esimp, rewrite l₂} end) + (λ s, begin cases s, {esimp, rewrite r₁}, {esimp, rewrite r₂} end) + +open bool unit +lemma bool_equiv_unit_sum_unit : bool ≃ (unit + unit) := +mk (λ b, match b with tt := inl star | ff := inr star end) + (λ s, match s with inl star := tt | inr star := ff end) + (λ b, begin cases b, esimp, esimp end) + (λ s, begin cases s with u u, {cases u, esimp}, {cases u, esimp} end) + +lemma sum_comm (A B : Type) : (A + B) ≃ (B + A) := +mk (λ s, match s with inl a := inr a | inr b := inl b end) + (λ s, match s with inl b := inr b | inr a := inl a end) + (λ s, begin cases s, esimp, esimp end) + (λ s, begin cases s, esimp, esimp end) + +lemma sum_assoc (A B C : Type) : ((A + B) + C) ≃ (A + (B + C)) := +mk (λ s, match s with inl (inl a) := inl a | inl (inr b) := inr (inl b) | inr c := inr (inr c) end) + (λ s, match s with inl a := inl (inl a) | inr (inl b) := inl (inr b) | inr (inr c) := inr c end) + (λ s, begin cases s with ab c, cases ab, repeat esimp end) + (λ s, begin cases s with a bc, esimp, cases bc, repeat esimp end) + +lemma sum_empty_right (A : Type) : (A + empty) ≃ A := +mk (λ s, match s with inl a := a | inr e := empty.rec _ e end) + (λ a, inl a) + (λ s, begin cases s with a e, esimp, exact empty.rec _ e end) + (λ a, rfl) + +lemma sum_empty_left (A : Type) : (empty + A) ≃ A := +calc (empty + A) ≃ (A + empty) : sum_comm + ... ≃ A : sum_empty_right +end + +section +open prod.ops +lemma arrow_prod_equiv_prod_arrow (A B C : Type) : (C → A × B) ≃ ((C → A) × (C → B)) := +mk (λ f, (λ c, (f c).1, λ c, (f c).2)) + (λ p, λ c, (p.1 c, p.2 c)) + (λ f, funext (λ c, begin esimp, cases f c, esimp end)) + (λ p, begin cases p, esimp end) + +lemma arrow_arrow_equiv_prod_arrow (A B C : Type) : (A → B → C) ≃ (A × B → C) := +mk (λ f, λ p, f p.1 p.2) + (λ f, λ a b, f (a, b)) + (λ f, rfl) + (λ f, funext (λ p, begin cases p, esimp end)) + +open sum +lemma sum_arrow_equiv_prod_arrow (A B C : Type) : ((A + B) → C) ≃ ((A → C) × (B → C)) := +mk (λ f, (λ a, f (inl a), λ b, f (inr b))) + (λ p, (λ s, match s with inl a := p.1 a | inr b := p.2 b end)) + (λ f, funext (λ s, begin cases s, esimp, esimp end)) + (λ p, begin cases p, esimp end) + +lemma sum_prod_distrib (A B C : Type) : ((A + B) × C) ≃ ((A × C) + (B × C)) := +mk (λ p, match p with (inl a, c) := inl (a, c) | (inr b, c) := inr (b, c) end) + (λ s, match s with inl (a, c) := (inl a, c) | inr (b, c) := (inr b, c) end) + (λ p, begin cases p with ab c, cases ab, repeat esimp end) + (λ s, begin cases s with ac bc, cases ac, esimp, cases bc, esimp end) + +lemma prod_sum_distrib (A B C : Type) : (A × (B + C)) ≃ ((A × B) + (A × C)) := +calc (A × (B + C)) ≃ ((B + C) × A) : prod_comm + ... ≃ ((B × A) + (C × A)) : sum_prod_distrib + ... ≃ ((A × B) + (A × C)) : sum_congr !prod_comm !prod_comm +end + +section +open sum nat unit prod.ops +lemma nat_equiv_nat_sum_unit : nat ≃ (nat + unit) := +mk (λ n, match n with 0 := inr star | succ a := inl a end) + (λ s, match s with inl n := succ n | inr star := zero end) + (λ n, begin cases n, repeat esimp end) + (λ s, begin cases s with a u, esimp, {cases u, esimp} end) + +lemma nat_sum_unit_equiv_nat : (nat + unit) ≃ nat := +equiv.symm nat_equiv_nat_sum_unit + +lemma nat_prod_nat_equiv_nat : (nat × nat) ≃ nat := +mk (λ p, mkpair p.1 p.2) + (λ n, unpair n) + (λ p, begin cases p, apply unpair_mkpair end) + (λ n, mkpair_unpair n) + +lemma nat_sum_bool_equiv_nat : (nat + bool) ≃ nat := +calc (nat + bool) ≃ (nat + (unit + unit)) : sum_congr !equiv.refl bool_equiv_unit_sum_unit + ... ≃ ((nat + unit) + unit) : sum_assoc + ... ≃ (nat + unit) : sum_congr nat_sum_unit_equiv_nat !equiv.refl + ... ≃ nat : nat_sum_unit_equiv_nat + +open decidable +lemma nat_sum_nat_equiv_nat : (nat + nat) ≃ nat := +mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end) + (λ n, if even n then inl (n div 2) else inr ((n - 1) div 2)) + (λ s, begin + have two_gt_0 : 2 > 0, from dec_trivial, + cases s, + {esimp, rewrite [if_pos (even_two_mul _), mul_div_cancel_left _ two_gt_0]}, + {esimp, rewrite [if_neg (not_even_two_mul_plus_one _), add_sub_cancel, mul_div_cancel_left _ two_gt_0]} + end) + (λ n, by_cases + (λ h : even n, begin rewrite [if_pos h], esimp, rewrite [mul_div_cancel' (dvd_of_even h)] end) + (λ h : ¬ even n, + begin + rewrite [if_neg h], esimp, + cases n, + {exact absurd even_zero h}, + {rewrite [-add_one, add_sub_cancel, + mul_div_cancel' (dvd_of_even (even_of_odd_succ (odd_of_not_even h)))]} + end)) +end +end equiv diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean index 124ef351c..d5803f3c9 100644 --- a/library/data/nat/parity.lean +++ b/library/data/nat/parity.lean @@ -116,6 +116,22 @@ lemma dvd_of_odd {n} : odd n → 2 ∣ n+1 := lemma odd_of_dvd {n} : 2 ∣ n+1 → odd n := λ h, odd_of_even_succ (even_of_dvd h) +lemma even_two_mul : ∀ n, even (2 * n) := +λ n, even_of_dvd (dvd_mul_right 2 n) + +lemma odd_two_mul_plus_one : ∀ n, odd (2 * n + 1) := +λ n, odd_succ_of_even (even_two_mul n) + +lemma not_even_two_mul_plus_one : ∀ n, ¬ even (2 * n + 1) := +λ n, not_even_of_odd (odd_two_mul_plus_one n) + +lemma not_odd_two_mul : ∀ n, ¬ odd (2 * n) := +λ n, not_odd_of_even (even_two_mul n) + +lemma even_pred_of_odd : ∀ {n}, odd n → even (pred n) +| 0 h := absurd h not_odd_zero +| (n+1) h := even_of_odd_succ h + lemma even_or_odd : ∀ n, even n ∨ odd n := λ n, by_cases (λ h : even n, or.inl h)