michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/logic/axioms): we have only one extra axiom

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-29 13:30:18 -07:00
parent 6dbcf86fd4
commit bbd6946a15
20 changed files with 201 additions and 279 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/lean/tutorial.org
View file

@ -126,12 +126,12 @@ the type =false= must be empty, since we don't have a proof for =false=.
Most systems based on the _propositions as types_ paradigm are based on constructive logic.
In Lean, we support classical and constructive logic. We can load
_classical axiom_ by using =import classical=. When the classical
_classical choice axiom_ by using =import logic.choice= or =import classical=. When the classical
extensions are loaded, the _excluded middle_ is a theorem,
and =em p= is a proof for =p ∨ ¬ p=.
#+BEGIN_SRC lean
import logic.axioms.classical
import logic.choice
constant p : Prop
check em p
#+END_SRC

2
library/classical.lean
View file

@ -5,4 +5,4 @@ Author: Jeremy Avigad
The standard library together with the classical axioms.
-/
import standard logic.axioms.classical
import standard logic.choice

2
library/data/quotient/classical.lean
View file

@ -5,7 +5,7 @@ Author: Floris van Doorn
A classical treatment of quotients, using Hilbert choice.
-/
import algebra.relation data.subtype logic.axioms.classical logic.axioms.hilbert
import algebra.relation data.subtype logic.choice
import .basic
namespace quotient

2
library/data/real/complete.lean
View file

@ -12,7 +12,7 @@ Here, we show that ℝ is complete.
-/
import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat
import logic.axioms.classical
import logic.choice
open -[coercions] rat
local notation 0 := rat.of_num 0
local notation 1 := rat.of_num 1

2
library/data/real/division.lean
View file

@ -9,7 +9,7 @@ At this point, we no longer proceed constructively: this file makes heavy use of
and excluded middle.
-/
import data.real.basic data.real.order data.rat data.nat logic.axioms.classical
import data.real.basic data.real.order data.rat data.nat logic.choice
open -[coercions] rat
open -[coercions] nat
open eq.ops pnat

2
library/data/set/classical_inverse.lean
View file

@ -6,7 +6,7 @@ Author: Jeremy Avigad, Andrew Zipperer
Using classical logic, defines an inverse function.
-/
import .function .map
import logic.axioms.classical
import logic.choice
open eq.ops
namespace set

11
library/logic/axioms/axioms.md
View file

@ -1,11 +0,0 @@
logic.axioms
============
Axioms that extend the Calculus of Constructions.
* [funext](funext.lean) : function extensionality
* [prop_complete](classical.lean) : the law of the excluded middle
* [hilbert](hilbert.lean) : choice functions
* [prop_decidable](prop_decidable.lean) : the decidable class is trivial with excluded middle
* [classical](classical.lean) : imports all of the above
* [examples](examples/examples.md)

7
library/logic/axioms/classical.lean
View file

@ -1,7 +0,0 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
-/
import logic.axioms.prop_complete logic.axioms.hilbert
import logic.axioms.prop_decidable

55
library/logic/axioms/em.lean
View file

@ -1,55 +0,0 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Prove excluded middle using: excluded middle follows from Hilbert's choice operator, function extensionality,
and Prop extensionality
-/
import logic.axioms.hilbert logic.eq
open eq.ops
section
parameter p : Prop
private definition U (x : Prop) : Prop := x = true ∨ p
private definition V (x : Prop) : Prop := x = false ∨ p
private noncomputable definition u := epsilon U
private noncomputable definition v := epsilon V
private lemma u_def : U u :=
epsilon_spec (exists.intro true (or.inl rfl))
private lemma v_def : V v :=
epsilon_spec (exists.intro false (or.inl rfl))
private lemma not_uv_or_p : ¬(u = v) ∨ p :=
or.elim u_def
(assume Hut : u = true,
or.elim v_def
(assume Hvf : v = false,
have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
or.inl Hne)
(assume Hp : p, or.inr Hp))
(assume Hp : p, or.inr Hp)
private lemma p_implies_uv : p → u = v :=
assume Hp : p,
have Hpred : U = V, from
funext (take x : Prop,
have Hl : (x = true ∨ p) → (x = false ∨ p), from
assume A, or.inr Hp,
have Hr : (x = false ∨ p) → (x = true ∨ p), from
assume A, or.inr Hp,
show (x = true ∨ p) = (x = false ∨ p), from
propext (iff.intro Hl Hr)),
have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
show u = v, from H'
theorem em : p ∨ ¬p :=
have H : ¬(u = v) → ¬p, from mt p_implies_uv,
or.elim not_uv_or_p
(assume Hne : ¬(u = v), or.inr (H Hne))
(assume Hp : p, or.inl Hp)
end

4
library/logic/axioms/examples/examples.md
View file

@ -1,4 +0,0 @@
logic.axioms.examples
=====================
* [diaconescu](diaconescu.lean) : Diaconescu's theorem

40
library/logic/axioms/examples/leftinv_of_inj2.lean
View file

@ -1,40 +0,0 @@
/-
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).
This proof does not use Hilbert's choice, but the simpler axiom of choice which is just a proposition.
-/
import logic.axioms.classical
open function
-- The forall_not_of_not_exists at logic.axioms uses decidable.
theorem forall_not_of_not_exists {A : Type} {p : A → Prop}
(H : ¬∃x, p x) : ∀x, ¬p x :=
take x, or.elim (em (p x))
(assume Hp : p x, absurd (exists.intro x Hp) H)
(assume Hnp : ¬p x, Hnp)
theorem has_left_inverse_of_injective {A B : Type} {f : A → B} : nonempty A → injective f → ∃ g, ∀ x, g (f x) = x :=
suppose nonempty A,
assume inj : ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂,
have ∃ g : B → A, ∀ b, (∀ a, f a = b → g b = a) ∨ (∀ a, f a ≠ b), from
axiom_of_choice (λ b : B, or.elim (em (∃ a, f a = b))
(suppose (∃ a, f a = b),
obtain w `f w = b`, from this,
exists.intro w (or.inl (take a,
suppose f a = b,
have f w = f a, begin subst this, exact `f w = f a` end,
inj w a `f w = f a`)))
(suppose ¬(∃ a, f a = b),
obtain a, from `nonempty A`,
exists.intro a (or.inr (forall_not_of_not_exists this)))),
obtain g hg, from this,
exists.intro g (take a,
or.elim (hg (f a))
(suppose (∀ a₁, f a₁ = f a → g (f a) = a₁),
this a rfl)
(suppose (∀ a₁, f a₁ ≠ f a),
absurd rfl (this a)))

69
library/logic/axioms/hilbert.lean
View file

@ -1,69 +0,0 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad
Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the constructive one).
-/
import logic.quantifiers
import data.subtype data.sum
open subtype inhabited nonempty
/- the axiom -/
-- In the presence of classical logic, we could prove this from a weaker statement:
-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
{ x | (∃y : A, P y) → P x}
theorem exists_true_of_nonempty {A : Type} (H : nonempty A) : ∃x : A, true :=
nonempty.elim H (take x, exists.intro x trivial)
noncomputable definition inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A :=
let u : {x | (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
inhabited.mk (elt_of u)
noncomputable definition inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
inhabited_of_nonempty (obtain w Hw, from H, nonempty.intro w)
/- the Hilbert epsilon function -/
noncomputable definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
let u : {x | (∃y, P y) → P x} :=
strong_indefinite_description P H in
elt_of u
theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) :
P (@epsilon A H P) :=
let u : {x | (∃y, P y) → P x} :=
strong_indefinite_description P H in
have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property u,
aux Hex
theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
P (@epsilon A (nonempty_of_exists Hex) P) :=
epsilon_spec_aux (nonempty_of_exists Hex) P Hex
theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a :=
epsilon_spec (exists.intro a (eq.refl a))
noncomputable definition some {A : Type} {P : A → Prop} (H : ∃x, P x) : A :=
@epsilon A (nonempty_of_exists H) P
theorem some_spec {A : Type} {P : A → Prop} (H : ∃x, P x) : P (some H) :=
epsilon_spec H
/- the axiom of choice -/
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) :
∃f, ∀x, R x (f x) :=
have H : ∀x, R x (some (H x)), from take x, some_spec (H x),
exists.intro _ H
theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} :
(∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=
iff.intro
(assume H : (∀x, ∃y, P x y), axiom_of_choice H)
(assume H : (∃f, (∀x, P x (f x))),
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H,
exists.intro (fw x) (Hw x))

54
library/logic/axioms/prop_complete.lean
View file

@ -1,54 +0,0 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import logic.connectives logic.quantifiers logic.cast algebra.relation
import logic.axioms.em
open eq.ops
theorem prop_complete (a : Prop) : a = true ∨ a = false :=
or.elim (em a)
(λ t, or.inl (propext (iff.intro (λ h, trivial) (λ h, t))))
(λ f, or.inr (propext (iff.intro (λ h, absurd h f) (λ h, false.elim h))))
definition eq_true_or_eq_false := prop_complete
theorem cases_true_false (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
or.elim (prop_complete a)
(assume Ht : a = true, Ht⁻¹ ▸ H1)
(assume Hf : a = false, Hf⁻¹ ▸ H2)
theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
cases_true_false P H1 H2 a
-- this supercedes by_cases in decidable
definition by_cases {p q : Prop} (Hpq : p → q) (Hnpq : ¬p → q) : q :=
or.elim (em p) (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
-- this supercedes by_contradiction in decidable
theorem by_contradiction {p : Prop} (H : ¬p → false) : p :=
by_cases
(assume H1 : p, H1)
(assume H1 : ¬p, false.rec _ (H H1))
theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
cases_true_false (λ x, x = false ∨ x = true)
(or.inr rfl)
(or.inl rfl)
a
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
iff.elim (assume H1 H2, propext (iff.intro H1 H2)) H
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
propext (iff.intro
(assume H, eq.of_iff H)
(assume H, iff.of_eq H))
open relation
theorem iff_congruence [instance] (P : Prop → Prop) : is_congruence iff iff P :=
is_congruence.mk
(take (a b : Prop),
assume H : a ↔ b,
show P a ↔ P b, from iff.of_eq (eq.of_iff H ▸ eq.refl (P a)))

24
library/logic/axioms/prop_decidable.lean
View file

@ -1,24 +0,0 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Excluded middle + Hilbert implies every proposition is decidable.
-/
import logic.axioms.prop_complete logic.axioms.hilbert data.sum
open decidable inhabited nonempty sum
noncomputable definition decidable_inhabited [instance] [priority 0] (a : Prop) : inhabited (decidable a) :=
inhabited_of_nonempty
(or.elim (em a)
(assume Ha, nonempty.intro (inl Ha))
(assume Hna, nonempty.intro (inr Hna)))
noncomputable definition prop_decidable [instance] [priority 0] (a : Prop) : decidable a :=
arbitrary (decidable a)
noncomputable definition type_decidable (A : Type) : A + (A → false) :=
match prop_decidable (nonempty A) with
| inl Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
| inr Hn := sum.inr (λ a, absurd (nonempty.intro a) Hn)
end

181
library/logic/choice.lean Normal file
View file

@ -0,0 +1,181 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad
-/
import logic.quantifiers logic.eq
import data.subtype data.sum
open subtype inhabited nonempty
/- the axiom -/
-- In the presence of classical logic, we could prove this from a weaker statement:
-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
{ x | (∃y : A, P y) → P x}
theorem exists_true_of_nonempty {A : Type} (H : nonempty A) : ∃x : A, true :=
nonempty.elim H (take x, exists.intro x trivial)
noncomputable definition inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A :=
let u : {x | (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
inhabited.mk (elt_of u)
noncomputable definition inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
inhabited_of_nonempty (obtain w Hw, from H, nonempty.intro w)
/- the Hilbert epsilon function -/
noncomputable definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
let u : {x | (∃y, P y) → P x} :=
strong_indefinite_description P H in
elt_of u
theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) :
P (@epsilon A H P) :=
let u : {x | (∃y, P y) → P x} :=
strong_indefinite_description P H in
have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property u,
aux Hex
theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
P (@epsilon A (nonempty_of_exists Hex) P) :=
epsilon_spec_aux (nonempty_of_exists Hex) P Hex
theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a :=
epsilon_spec (exists.intro a (eq.refl a))
noncomputable definition some {A : Type} {P : A → Prop} (H : ∃x, P x) : A :=
@epsilon A (nonempty_of_exists H) P
theorem some_spec {A : Type} {P : A → Prop} (H : ∃x, P x) : P (some H) :=
epsilon_spec H
/- the axiom of choice -/
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) :
∃f, ∀x, R x (f x) :=
have H : ∀x, R x (some (H x)), from take x, some_spec (H x),
exists.intro _ H
theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} :
(∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=
iff.intro
(assume H : (∀x, ∃y, P x y), axiom_of_choice H)
(assume H : (∃f, (∀x, P x (f x))),
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H,
exists.intro (fw x) (Hw x))
/-
Prove excluded middle using Hilbert's choice
The proof follows Diaconescu proof that shows that the axiom of choice implies the excluded middle.
-/
section diaconescu
open eq.ops
parameter p : Prop
private definition U (x : Prop) : Prop := x = true ∨ p
private definition V (x : Prop) : Prop := x = false ∨ p
private noncomputable definition u := epsilon U
private noncomputable definition v := epsilon V
private lemma u_def : U u :=
epsilon_spec (exists.intro true (or.inl rfl))
private lemma v_def : V v :=
epsilon_spec (exists.intro false (or.inl rfl))
private lemma not_uv_or_p : ¬(u = v) ∨ p :=
or.elim u_def
(assume Hut : u = true,
or.elim v_def
(assume Hvf : v = false,
have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
or.inl Hne)
(assume Hp : p, or.inr Hp))
(assume Hp : p, or.inr Hp)
private lemma p_implies_uv : p → u = v :=
assume Hp : p,
have Hpred : U = V, from
funext (take x : Prop,
have Hl : (x = true ∨ p) → (x = false ∨ p), from
assume A, or.inr Hp,
have Hr : (x = false ∨ p) → (x = true ∨ p), from
assume A, or.inr Hp,
show (x = true ∨ p) = (x = false ∨ p), from
propext (iff.intro Hl Hr)),
have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
show u = v, from H'
theorem em : p ∨ ¬p :=
have H : ¬(u = v) → ¬p, from mt p_implies_uv,
or.elim not_uv_or_p
(assume Hne : ¬(u = v), or.inr (H Hne))
(assume Hp : p, or.inl Hp)
end diaconescu
theorem prop_complete (a : Prop) : a = true ∨ a = false :=
or.elim (em a)
(λ t, or.inl (propext (iff.intro (λ h, trivial) (λ h, t))))
(λ f, or.inr (propext (iff.intro (λ h, absurd h f) (λ h, false.elim h))))
definition eq_true_or_eq_false := prop_complete
section aux
open eq.ops
theorem cases_true_false (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
or.elim (prop_complete a)
(assume Ht : a = true, Ht⁻¹ ▸ H1)
(assume Hf : a = false, Hf⁻¹ ▸ H2)
theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
cases_true_false P H1 H2 a
-- this supercedes by_cases in decidable
definition by_cases {p q : Prop} (Hpq : p → q) (Hnpq : ¬p → q) : q :=
or.elim (em p) (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
-- this supercedes by_contradiction in decidable
theorem by_contradiction {p : Prop} (H : ¬p → false) : p :=
by_cases
(assume H1 : p, H1)
(assume H1 : ¬p, false.rec _ (H H1))
theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
cases_true_false (λ x, x = false ∨ x = true)
(or.inr rfl)
(or.inl rfl)
a
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
iff.elim (assume H1 H2, propext (iff.intro H1 H2)) H
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
propext (iff.intro
(assume H, eq.of_iff H)
(assume H, iff.of_eq H))
end aux
/- All propositions are decidable -/
section all_decidable
open decidable sum
noncomputable definition decidable_inhabited [instance] [priority 0] (a : Prop) : inhabited (decidable a) :=
inhabited_of_nonempty
(or.elim (em a)
(assume Ha, nonempty.intro (inl Ha))
(assume Hna, nonempty.intro (inr Hna)))
noncomputable definition prop_decidable [instance] [priority 0] (a : Prop) : decidable a :=
arbitrary (decidable a)
noncomputable definition type_decidable (A : Type) : A + (A → false) :=
match prop_decidable (nonempty A) with
| inl Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
| inr Hn := sum.inr (λ a, absurd (nonempty.intro a) Hn)
end
end all_decidable

2
library/logic/axioms/examples/leftinv_of_inj.lean → library/logic/examples/leftinv_of_inj.lean
View file

@ -9,7 +9,7 @@ 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 logic.axioms.classical
import logic.choice
open function
noncomputable definition mk_left_inv {A B : Type} [h : nonempty A] (f : A → B) : B → A :=

13
library/logic/logic.md
View file

@ -2,10 +2,9 @@ logic
=====
Logical constructions and theorems, beyond what has already been
declared in init.datatypes and init.logic.
declared in init.datatypes and init.logic.
The subfolder logic.axioms declares additional axioms. The command
`import logic` does not import any axioms by default.
The command `import logic` does not import any axioms by default.
* [connectives](connectives.lean) : the propositional connectives
* [eq](eq.lean) : additional theorems for equality and disequality
@ -16,7 +15,13 @@ The subfolder logic.axioms declares additional axioms. The command
* [subsingleton](subsingleton.lean)
* [default](default.lean)
The file `choice.lean` declares a choice axiom, and uses it to
prove the excluded middle, propositional completeness, axiom of
choice, and prove that the decidable class is trivial when the
choice axiom is assumed.
* [choice](choice.lean)
Subfolders:
* [axioms](axioms/axioms.md) : additional axioms
* [examples](examples/examples.md)

2
tests/lean/empty.lean
View file

@ -1,4 +1,4 @@
import logic logic.axioms.hilbert
import logic logic.choice
open inhabited nonempty
noncomputable definition v1 : Prop := epsilon (λ x, true)

2
tests/lean/interactive/class_bug.lean
View file

@ -1,4 +1,4 @@
import logic.axioms.hilbert data.nat.basic
import logic.choice data.nat.basic
open nonempty inhabited nat
theorem int_inhabited [instance] : inhabited nat := inhabited.mk zero

2
tests/lean/print_ax2.lean
View file

@ -1,3 +1,3 @@
import logic.axioms.hilbert logic.axioms.em
import logic.choice
print axioms