refactor(library/logic): rename theorems

2014-12-15 16:13:04 -05:00 · 2014-12-15 16:13:04 -05:00 · da719e6ee4
commit da719e6ee4
parent 3e9a484851
10 changed files with 99 additions and 82 deletions
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@ -48,8 +48,8 @@ let u : {x | (∃y, P y) → P x} :=
 has_property u Hex

 theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
-    P (@epsilon A (exists_imp_nonempty Hex) P) :=
-epsilon_spec_aux (exists_imp_nonempty Hex) P Hex
+    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))
@ -60,7 +60,7 @@ epsilon_spec (exists_intro a (eq.refl a))

 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) :=
-let f := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y),
+let f := λx, @epsilon _ (nonempty_of_exists (H x)) (λy, R x y),
    H := take x, epsilon_spec (H x)
 in exists_intro f H

--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@ -1,12 +1,16 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: cast.lean
+Author: Leonardo de Moura
+
+Casts and heterogeneous equality. See also init.datatypes and init.logic.
+-/
+
 import logic.eq logic.quantifiers
 open eq.ops

-- cast.lean
-- =========
-
 section
  universe variable u
  variables {A B : Type.{u}}
@ -30,20 +34,24 @@ namespace heq
  definition type_eq (H : a == b) : A = B :=
  heq.rec_on H (eq.refl A)

-  theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
+  theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) :
+    C b H₁ :=
  rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁

  theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b :=
  drec_on H !cast_eq
 end heq

-theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p :=
+theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) :
+  eq.rec_on H p == p :=
 eq.drec_on H !heq.refl

 section
  universe variables u v
  variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}
-  theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') : f a == f' a :=
+
+  theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') :
+    f a == f' a :=
  have aux : ∀ (f : Π x, P x) (f' : Π x, P x), f == f' → f a == f' a, from
    take f f' H, heq.to_eq H ▸ heq.refl (f a),
  (H₂ ▸ aux) f f' H₁
@ -105,7 +113,8 @@ section
    take H : P = P, heq.refl (eq.rec_on H f a),
  (H ▸ aux) H

-  theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
+  theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) :
+    eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
  heq.to_eq (calc
    eq.rec_on H f a == f a                   : rec_on_app H f a
      ... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
@ -116,7 +125,6 @@ section
  have H₂ : ∀ (H : (Π x, P x) = (Π x, P' x)), cast H f a == f a, from
    H ▸ H₁,
  H₂ (pi_eq H)
-
 end

 section
@ -144,7 +152,8 @@ section
      (Hd : cast (dcongr_arg3 D Ha Hb Hc) d = d') : f a b c d = f a' b' c' d' :=
  heq.to_eq (hcongr_arg4 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))

-  --mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition. Then proving eq is easier than proving heq)
+  -- mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition.
+  -- Then proving eq is easier than proving heq)
  theorem hdcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : b == b')
      (Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c')
        : f a b c = f a' b' c' :=
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: logic.connectives
 Authors: Jeremy Avigad, Leonardo de Moura

-The propositional connectives. See also init.datatypes.
+The propositional connectives. See also init.datatypes and init.logic.
 -/

 variables {a b c d : Prop}
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@ -1,6 +1,10 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: logic.default
+Author: Jeremy Avigad
+-/

 import logic.eq logic.connectives logic.cast logic.subsingleton
 import logic.quantifiers logic.instances logic.identities
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@ -1,16 +1,13 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: logic.eq
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn

-Additional declarations/theorems about equality
+Additional declarations/theorems about equality. See also init.datatypes and init.logic.
 -/

-- logic.eq
-- ========
-
-- Equality.
-
 open eq.ops

 namespace eq
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@ -1,36 +1,37 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Jeremy Avigad, Leonardo de Moura
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.

-- logic.identities
-- ============================
+Module: logic.identities
+Authors: Jeremy Avigad, Leonardo de Moura

-- Useful logical identities. In the absence of propositional extensionality, some of the
-- calculations use the type class support provided by logic.instances
+Useful logical identities. Since we are not using propositional extensionality, some of the
+calculations use the type class support provided by logic.instances.
+-/

 import logic.connectives logic.instances logic.quantifiers logic.cast

 open relation decidable relation.iff_ops

-theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
+theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
 calc
  (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or.assoc
    ... ↔ a ∨ (c ∨ b)       : {or.comm}
     ... ↔ (a ∨ c) ∨ b      : iff.symm or.assoc

-theorem or_left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) :=
+theorem or.left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) :=
 calc
  a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc
    ... ↔ (b ∨ a) ∨ c       : {or.comm}
     ... ↔ b ∨ (a ∨ c)      : or.assoc

-theorem and_right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
+theorem and.right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
 calc
  (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc
    ... ↔ a ∧ (c ∧ b)       : {and.comm}
     ... ↔ (a ∧ c) ∧ b      : iff.symm and.assoc

-theorem and_left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) :=
+theorem and.left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) :=
 calc
  a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc
    ... ↔ (b ∧ a) ∧ c       : {and.comm}
@ -46,14 +47,14 @@ iff.intro
 theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a :=
 iff.mp not_not_iff H

-theorem not_true_iff_false : (¬true) ↔ false :=
+theorem not_true_iff_false : ¬true ↔ false :=
 iff.intro (assume H, H trivial) false.elim

-theorem not_false_iff_true : (¬false) ↔ true :=
+theorem not_false_iff_true : ¬false ↔ true :=
 iff.intro (assume H, trivial) (assume H H', H')

 theorem not_or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
-  (¬(a ∨ b)) ↔ (¬a ∧ ¬b) :=
+  ¬(a ∨ b) ↔ ¬a ∧ ¬b :=
 iff.intro
  (assume H, or.elim (em a)
    (assume Ha, absurd (or.inl Ha) H)
@ -65,7 +66,8 @@ iff.intro
      (assume Ha, absurd Ha (and.elim_left H))
      (assume Hb, absurd Hb (and.elim_right H)))

-theorem not_and {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) :=
+theorem not_and_iff_not_or_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
+  ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
 iff.intro
  (assume H, or.elim (em a)
    (assume Ha, or.elim (em b)
@ -77,7 +79,7 @@ iff.intro
      (assume Hna, absurd (and.elim_left N) Hna)
      (assume Hnb, absurd (and.elim_right N) Hnb))

-theorem imp_or {a b : Prop} [Da : decidable a] : (a → b) ↔ (¬a ∨ b) :=
+theorem imp_iff_not_or {a b : Prop} [Da : decidable a] : (a → b) ↔ ¬a ∨ b :=
 iff.intro
  (assume H : a → b, (or.elim (em a)
    (assume Ha  : a,   or.inr (H Ha))
@ -85,27 +87,29 @@ iff.intro
  (assume (H : ¬a ∨ b) (Ha : a),
    or_resolve_right H (not_not_iff⁻¹ ▸ Ha))

-theorem not_implies {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a → b)) ↔ (a ∧ ¬b) :=
-calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or}
-            ... ↔ (¬¬a ∧ ¬b)  : not_or_iff_not_and_not
-            ... ↔ (a ∧ ¬b)    : {not_not_iff}
+theorem not_implies_iff_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
+  ¬(a → b) ↔ a ∧ ¬b :=
+calc
+  ¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or}
+       ... ↔ ¬¬a ∧ ¬b  : not_or_iff_not_and_not
+       ... ↔ a ∧ ¬b    : {not_not_iff}

 theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a :=
 assume H, by_contradiction (assume Hna : ¬a,
  have Hnna : ¬¬a, from not_not_of_not_implies (mt H Hna),
  absurd (not_not_elim Hnna) Hna)

-theorem not_exists_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
+theorem forall_not_of_not_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
    (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 Hn : ¬P x, Hn)

-theorem not_forall_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
+theorem exists_not_of_not_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
    [D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) :
  ∃x, ¬P x :=
@by_contradiction _ D' (assume H1 : ¬∃x, ¬P x,
-  have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not.decidable (D x)) H1,
+  have H2 : ∀x, ¬¬P x, from @forall_not_of_not_exists _ _ (take x, not.decidable (D x)) H1,
  have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x),
  absurd H3 H)

@ -119,32 +123,32 @@ iff.intro
  (assume H1 : a,     absurd H1 H)
  (assume H2 : false, false.elim H2)

-theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false :=
+theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false :=
 iff.intro
  (assume H, false.of_ne H)
  (assume H, false.elim H)

-theorem eq_id {A : Type} (a : A) : (a = a) ↔ true :=
+theorem eq_self_iff_true {A : Type} (a : A) : (a = a) ↔ true :=
 iff_true_intro rfl

-theorem heq_id {A : Type} (a : A) : (a == a) ↔ true :=
+theorem heq_self_iff_true {A : Type} (a : A) : (a == a) ↔ true :=
 iff_true_intro (heq.refl a)

-theorem a_iff_not_a (a : Prop) : (a ↔ ¬a) ↔ false :=
+theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
 iff.intro
  (assume H,
    have H' : ¬a, from assume Ha, (H ▸ Ha) Ha,
    H' (H⁻¹ ▸ H'))
  (assume H, false.elim H)

-theorem true_eq_false : (true ↔ false) ↔ false :=
-not_true_iff_false ▸ (a_iff_not_a true)
+theorem true_iff_false : (true ↔ false) ↔ false :=
+not_true_iff_false ▸ (iff_not_self true)

-theorem false_eq_true : (false ↔ true) ↔ false :=
-not_false_iff_true ▸ (a_iff_not_a false)
+theorem false_iff_true : (false ↔ true) ↔ false :=
+not_false_iff_true ▸ (iff_not_self false)

-theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a :=
+theorem iff_true_iff (a : Prop) : (a ↔ true) ↔ a :=
 iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H)

-theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a :=
+theorem iff_false_iff_not (a : Prop) : (a ↔ false) ↔ ¬a :=
 iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H)
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@ -20,7 +20,6 @@ relation.is_equivalence.mk (@eq.refl T) (@eq.symm T) (@eq.trans T)
 theorem is_equivalence_iff [instance] : relation.is_equivalence iff :=
 relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans

-
 /- congruences for logic operations -/

 theorem is_congruence_not : is_congruence iff iff not :=
@ -62,14 +61,12 @@ is_congruence2.mk
      (assume H3 : a1 ↔ a2, iff.trans (iff.symm H1) (iff.trans H3 H2))
      (assume H3 : b1 ↔ b2, iff.trans H1 (iff.trans H3 (iff.symm H2))))

-- theorem is_congruence_const_iff [instance] := is_congruence.const iff iff.refl
 definition is_congruence_not_compose [instance] := is_congruence.compose is_congruence_not
 definition is_congruence_and_compose [instance] := is_congruence.compose21 is_congruence_and
 definition is_congruence_or_compose [instance] := is_congruence.compose21 is_congruence_or
 definition is_congruence_implies_compose [instance] := is_congruence.compose21 is_congruence_imp
 definition is_congruence_iff_compose [instance] := is_congruence.compose21 is_congruence_iff

-
 /- a general substitution operation with respect to an arbitrary congruence -/

 namespace general_subst
@ -77,13 +74,11 @@ namespace general_subst
    {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (is_congruence.app C H) H1
 end general_subst

-
 /- iff can be coerced to implication -/

 definition mp_like_iff [instance] : relation.mp_like iff :=
 relation.mp_like.mk (λa b (H : a ↔ b), iff.elim_left H)

-
 /- support for calculations with iff -/

 namespace iff
--- a/library/logic/logic.md
+++ b/library/logic/logic.md
@ -1,22 +1,22 @@
 logic
 =====

-Additional constructions and axioms. By default, `import logic` does not
-import any axioms.
+Logical constructions and theorems, beyond what has already been
+declared in init.datatypes and init.logic. 

-Logical operations and connectives.
+The subfolder logic.axioms declares additional axioms. 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
 * [cast](cast.lean) : casts and heterogeneous equality
 * [quantifiers](quantifiers.lean) : existential and universal quantifiers
 * [identities](identities.lean) : some useful identities
+* [instances](instances.lean) : class instances for eq and iff
+* [subsingleton](subsingleton.lean)
+* [default](default.lean)

-Constructively, inhabited types have a witness, while nonempty types
-are "proof irrelevant". Classically (assuming the axioms in
-logic.axioms.hilbert) the two are equivalent. Type class inferences
-are set up to use "inhabited" however, so users should use that to
-declare that types have an element. Use "nonempty" in the hypothesis
-of a theorem when the theorem does not depend on the witness chosen.
+Subfolders:

 * [axioms](axioms/axioms.md) : additional axioms
 * [examples](examples/examples.md)
--- a/library/logic/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@ -4,16 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.

 Module: logic.quantifiers
 Authors: Leonardo de Moura, Jeremy Avigad
+
+Universal and existential quantifiers. See also init.logic.
 -/

 open inhabited nonempty

-theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
+theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
 assume H1 : ∀x, ¬p x,
  obtain (w : A) (Hw : p w), from H,
  absurd Hw (H1 w)

-theorem forall_not_exists {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
+theorem not_exists_not_of_forall {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
 assume H1 : ∃x, ¬p x,
  obtain (w : A) (Hw : ¬p w), from H1,
  absurd (H2 w) Hw
@ -41,12 +43,14 @@ iff.intro
  (assume Hl, obtain a Hp, from Hl, Hp)
  (assume Hr, inhabited.destruct H (take a, exists_intro a Hr))

-theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
+theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) :
+  (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
 iff.intro
  (assume H, and.intro (take x, and.elim_left (H x)) (take x, and.elim_right (H x)))
  (assume H, take x, and.intro (and.elim_left H x) (and.elim_right H x))

-theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) :=
+theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) :
+  (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) :=
 iff.intro
  (assume H, obtain (w : A) (Hw : φ w ∨ ψ w), from H,
    or.elim Hw
@ -58,7 +62,7 @@ iff.intro
    (assume H2, obtain (w : A) (Hw : ψ w), from H2,
      exists_intro w (or.inr Hw)))

-theorem exists_imp_nonempty {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A :=
+theorem nonempty_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A :=
 obtain w Hw, from H, nonempty.intro w

 section
--- a/library/logic/subsingleton.lean
+++ b/library/logic/subsingleton.lean
@ -1,8 +1,11 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
+
+Module: logic.subsingleton
+Author: Floris van Doorn
 -/
+
 import logic.eq

 inductive subsingleton [class] (A : Type) : Prop :=
@ -28,7 +31,8 @@ subsingleton.intro (fun d1 d2,
      d2)
   d1)

-protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
+protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p]
+    {H1 : p → Type} {H2 : ¬p → Type}
    (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
  : subsingleton (decidable.rec_on H H1 H2) :=
 decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"