From 9cb759e0a975d930bdb47101ce388de1823e8373 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Apr 2015 22:39:51 -0700 Subject: [PATCH] feat(library/logic/axioms/examples/leftinv_of_inj): add classical example --- .../logic/axioms/examples/leftinv_of_inj.lean | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 library/logic/axioms/examples/leftinv_of_inj.lean diff --git a/library/logic/axioms/examples/leftinv_of_inj.lean b/library/logic/axioms/examples/leftinv_of_inj.lean new file mode 100644 index 000000000..228c05c7d --- /dev/null +++ b/library/logic/axioms/examples/leftinv_of_inj.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Leonardo de Moura + +Classical proof that if f is injective, then f has a left inverse (if domain is not empty). +The proof uses the classical axioms: choice and excluded middle. +The excluded middle is being used "behind the scenes" to allow us to write the if-then-else expression +with (∃ a : A, f a = b). +-/ +import algebra.function logic.axioms.classical +open function + +definition mk_left_inv {A B : Type} [h : nonempty A] (f : A → B) : B → A := +λ b : B, if ex : (∃ a : A, f a = b) then some ex else inhabited.value (inhabited_of_nonempty h) + +theorem has_left_inverse_of_injective {A B : Type} {f : A → B} : nonempty A → injective f → has_left_inverse f := +assume h : nonempty A, +assume inj : ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂, +let finv : B → A := mk_left_inv f in +have linv : finv ∘ f = id, from + funext (λ a, + assert ex : ∃ a₁ : A, f a₁ = f a, from exists.intro a rfl, + assert h₁ : f (some ex) = f a, from !some_spec, + begin + esimp [mk_left_inv, compose, id], + rewrite [dif_pos ex], + exact (!inj h₁) + end), +exists.intro finv linv