refactor(library/logic/axioms): rename files, import logic.axioms.classical now imports all classical axioms
This commit is contained in:
parent
e5c25ff7a3
commit
003a2c1e2c
8 changed files with 73 additions and 77 deletions
|
@ -7,5 +7,4 @@ Author: Jeremy Avigad
|
||||||
|
|
||||||
The standard library together with the classical axioms.
|
The standard library together with the classical axioms.
|
||||||
-/
|
-/
|
||||||
|
import standard logic.axioms.classical
|
||||||
import standard logic.axioms
|
|
||||||
|
|
|
@ -4,7 +4,8 @@ logic.axioms
|
||||||
Axioms that extend the Calculus of Constructions.
|
Axioms that extend the Calculus of Constructions.
|
||||||
|
|
||||||
* [funext](funext.lean) : function extensionality
|
* [funext](funext.lean) : function extensionality
|
||||||
* [classical](classical.lean) : the law of the excluded middle
|
* [prop_complete](classical.lean) : the law of the excluded middle
|
||||||
* [hilbert](hilbert.lean) : choice functions
|
* [hilbert](hilbert.lean) : choice functions
|
||||||
* [prop_decidable](prop_decidable.lean) : the decidable class is trivial with excluded middle
|
* [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)
|
* [examples](examples/examples.md)
|
|
@ -3,57 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
Module: logic.axioms.classical
|
Module: logic.axioms.classical
|
||||||
Author: Leonardo de Moura
|
Author: Jeremy Avigad
|
||||||
-/
|
-/
|
||||||
|
import logic.axioms.prop_complete logic.axioms.funext logic.axioms.hilbert
|
||||||
import logic.connectives logic.quantifiers logic.cast algebra.relation
|
import logic.axioms.prop_decidable
|
||||||
|
|
||||||
open eq.ops
|
|
||||||
|
|
||||||
axiom prop_complete (a : Prop) : a = true ∨ a = false
|
|
||||||
|
|
||||||
definition eq_true_or_eq_false := prop_complete
|
|
||||||
|
|
||||||
theorem cases (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 P H1 H2 a
|
|
||||||
|
|
||||||
-- this supercedes the em in decidable
|
|
||||||
theorem em (a : Prop) : a ∨ ¬a :=
|
|
||||||
or.elim (prop_complete a)
|
|
||||||
(assume Ht : a = true, or.inl (of_eq_true Ht))
|
|
||||||
(assume Hf : a = false, or.inr (not_of_eq_false Hf))
|
|
||||||
|
|
||||||
theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
|
|
||||||
cases (λ x, x = false ∨ x = true)
|
|
||||||
(or.inr rfl)
|
|
||||||
(or.inl rfl)
|
|
||||||
a
|
|
||||||
|
|
||||||
theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b :=
|
|
||||||
or.elim (prop_complete a)
|
|
||||||
(assume Hat, or.elim (prop_complete b)
|
|
||||||
(assume Hbt, Hat ⬝ Hbt⁻¹)
|
|
||||||
(assume Hbf, false.elim (Hbf ▸ (Hab (of_eq_true Hat)))))
|
|
||||||
(assume Haf, or.elim (prop_complete b)
|
|
||||||
(assume Hbt, false.elim (Haf ▸ (Hba (of_eq_true Hbt))))
|
|
||||||
(assume Hbf, Haf ⬝ Hbf⁻¹))
|
|
||||||
|
|
||||||
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
|
|
||||||
iff.elim (assume H1 H2, propext H1 H2) H
|
|
||||||
|
|
||||||
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
|
|
||||||
propext
|
|
||||||
(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)))
|
|
||||||
|
|
|
@ -1,10 +0,0 @@
|
||||||
/-
|
|
||||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Module: logic.axioms.default
|
|
||||||
Author: Jeremy Avigad
|
|
||||||
-/
|
|
||||||
|
|
||||||
import logic.axioms.classical logic.axioms.funext logic.axioms.hilbert
|
|
||||||
import logic.axioms.prop_decidable
|
|
|
@ -1,14 +1,15 @@
|
||||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
/-
|
||||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||||
-- Author: Leonardo de Moura
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
-- logic.axioms.funext
|
Module: logic.axioms.funext
|
||||||
-- ===================
|
Author: Leonardo de Moura
|
||||||
|
|
||||||
|
Function extensionality.
|
||||||
|
-/
|
||||||
import logic.cast algebra.function data.sigma
|
import logic.cast algebra.function data.sigma
|
||||||
open function eq.ops
|
open function eq.ops
|
||||||
|
|
||||||
-- Function extensionality
|
|
||||||
axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π a, B a} (H : ∀ a, f a = g a), f = g
|
axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π a, B a} (H : ∀ a, f a = g a), f = g
|
||||||
|
|
||||||
namespace function
|
namespace function
|
||||||
|
@ -30,5 +31,4 @@ namespace function
|
||||||
(H : ∀ a, f a == g a) : f == g :=
|
(H : ∀ a, f a == g a) : f == g :=
|
||||||
let HH : B = B' := (funext (λ x, heq.type_eq (H x))) in
|
let HH : B = B' := (funext (λ x, heq.type_eq (H x))) in
|
||||||
cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app HH f a) (H a))))
|
cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app HH f a) (H a))))
|
||||||
|
|
||||||
end function
|
end function
|
||||||
|
|
|
@ -7,10 +7,8 @@ Authors: Leonardo de Moura, Jeremy Avigad
|
||||||
|
|
||||||
Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the constructive one).
|
Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the constructive one).
|
||||||
-/
|
-/
|
||||||
|
|
||||||
import logic.quantifiers
|
import logic.quantifiers
|
||||||
import data.subtype data.sum
|
import data.subtype data.sum
|
||||||
|
|
||||||
open subtype inhabited nonempty
|
open subtype inhabited nonempty
|
||||||
|
|
||||||
/- the axiom -/
|
/- the axiom -/
|
||||||
|
|
59
library/logic/axioms/prop_complete.lean
Normal file
59
library/logic/axioms/prop_complete.lean
Normal file
|
@ -0,0 +1,59 @@
|
||||||
|
/-
|
||||||
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
|
Module: logic.axioms.classical
|
||||||
|
Author: Leonardo de Moura
|
||||||
|
-/
|
||||||
|
|
||||||
|
import logic.connectives logic.quantifiers logic.cast algebra.relation
|
||||||
|
|
||||||
|
open eq.ops
|
||||||
|
|
||||||
|
axiom prop_complete (a : Prop) : a = true ∨ a = false
|
||||||
|
|
||||||
|
definition eq_true_or_eq_false := prop_complete
|
||||||
|
|
||||||
|
theorem cases (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 P H1 H2 a
|
||||||
|
|
||||||
|
-- this supercedes the em in decidable
|
||||||
|
theorem em (a : Prop) : a ∨ ¬a :=
|
||||||
|
or.elim (prop_complete a)
|
||||||
|
(assume Ht : a = true, or.inl (of_eq_true Ht))
|
||||||
|
(assume Hf : a = false, or.inr (not_of_eq_false Hf))
|
||||||
|
|
||||||
|
theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
|
||||||
|
cases (λ x, x = false ∨ x = true)
|
||||||
|
(or.inr rfl)
|
||||||
|
(or.inl rfl)
|
||||||
|
a
|
||||||
|
|
||||||
|
theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b :=
|
||||||
|
or.elim (prop_complete a)
|
||||||
|
(assume Hat, or.elim (prop_complete b)
|
||||||
|
(assume Hbt, Hat ⬝ Hbt⁻¹)
|
||||||
|
(assume Hbf, false.elim (Hbf ▸ (Hab (of_eq_true Hat)))))
|
||||||
|
(assume Haf, or.elim (prop_complete b)
|
||||||
|
(assume Hbt, false.elim (Haf ▸ (Hba (of_eq_true Hbt))))
|
||||||
|
(assume Hbf, Haf ⬝ Hbf⁻¹))
|
||||||
|
|
||||||
|
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
|
||||||
|
iff.elim (assume H1 H2, propext H1 H2) H
|
||||||
|
|
||||||
|
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
|
||||||
|
propext
|
||||||
|
(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)))
|
|
@ -5,8 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Module: logic.axioms.prop_decidable
|
Module: logic.axioms.prop_decidable
|
||||||
Author: Leonardo de Moura
|
Author: Leonardo de Moura
|
||||||
-/
|
-/
|
||||||
|
import logic.axioms.prop_complete logic.axioms.hilbert
|
||||||
import logic.axioms.classical logic.axioms.hilbert
|
|
||||||
open decidable inhabited nonempty
|
open decidable inhabited nonempty
|
||||||
|
|
||||||
-- Excluded middle + Hilbert implies every proposition is decidable
|
-- Excluded middle + Hilbert implies every proposition is decidable
|
||||||
|
|
Loading…
Add table
Reference in a new issue