feat(library/standard): add sigma types and subtypes, make inhabited constructive

library/standard/data/data.md

@@ -1,7 +1,7 @@
 data
 ====
 
-Various datatypes.
+Various data types.
 
 Basic types:
 
@@ -15,7 +15,10 @@ Basic types:
 
 Constructors:
 
+* [prod](prod.lean) : cartesian product
+* [sum](sum.lean)
+* [sigma](sigma.lean) : the dependent product
 * [option](option.lean)
-* [pair](pair.lean)
+* [subtype](subtype.lean)
 * [list](list/list.md)
 * [set](set.lean)

library/standard/data/pair.lean

@@ -1,45 +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.classes.inhabited logic.connectives.eq
-
-namespace pair
-inductive pair (A B : Type) : Type :=
-| mk_pair : A → B → pair A B
-
-section thms
-  parameters {A B : Type}
-
-  definition fst [inline] (p : pair A B) := pair_rec (λ x y, x) p
-  definition snd [inline] (p : pair A B) := pair_rec (λ x y, y) p
-
-  theorem pair_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (pair A B) :=
-  inhabited_elim H1 (λ a, inhabited_elim H2 (λ b, inhabited_intro (mk_pair a b)))
-
-  theorem fst_mk_pair (a : A) (b : B) : fst (mk_pair a b) = a :=
-  refl a
-
-  theorem snd_mk_pair (a : A) (b : B) : snd (mk_pair a b) = b :=
-  refl b
-
-  theorem pair_ext (p : pair A B) : mk_pair (fst p) (snd p) = p :=
-  pair_rec (λ x y, refl (mk_pair x y)) p
-
-  theorem pair_ext_eq {p1 p2 : pair A B} (H1 : fst p1 = fst p2) (H2 : snd p1 = snd p2) : p1 = p2 :=
-  calc p1  = mk_pair (fst p1) (snd p1) : symm (pair_ext p1)
-       ... = mk_pair (fst p2) (snd p1) : {H1}
-       ... = mk_pair (fst p2) (snd p2) : {H2}
-       ... = p2                        : pair_ext p2
-end thms
-
-instance pair_inhabited
-
-precedence `×`:30
-infixr × := pair
-
--- notation for n-ary tuples
-notation `(` h `,` t:(foldl `,` (e r, mk_pair r e) h) `)` := t
-end pair

library/standard/data/prod.lean

@@ -0,0 +1,48 @@
+-- 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.classes.inhabited logic.connectives.eq
+
+inductive prod (A B : Type) : Type :=
+| pair : A → B → prod A B
+
+precedence `×`:30
+infixr × := prod
+
+-- notation for n-ary tuples
+notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t
+
+namespace prod
+
+section
+
+  parameters {A B : Type}
+
+  abbreviation pr1 (p : prod A B) := prod_rec (λ x y, x) p
+  abbreviation pr2 (p : prod A B) := prod_rec (λ x y, y) p
+
+  theorem pr1_pair (a : A) (b : B) : pr1 (a, b) = a := refl a
+  theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b := refl b
+
+  -- TODO: remove prefix when we can protect it
+  theorem pair_destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
+  prod_rec H p
+
+  theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p :=
+  pair_destruct p (λx y, refl (x, y))
+
+  theorem pair_eq {p1 p2 : prod A B} (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2) : p1 = p2 :=
+  calc p1  = pair (pr1 p1) (pr2 p1) : symm (prod_ext p1)
+       ... = pair (pr1 p2) (pr2 p1) : {H1}
+       ... = pair (pr1 p2) (pr2 p2) : {H2}
+       ... = p2                        : prod_ext p2
+
+  theorem prod_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
+  inhabited_elim H1 (λa, inhabited_elim H2 (λb, inhabited_intro (pair a b)))
+
+end
+
+instance prod_inhabited
+
+end prod

library/standard/data/sigma.lean

@@ -0,0 +1,57 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura, Jeremy Avigad
+
+import logic.classes.inhabited logic.connectives.eq
+
+inductive sigma {A : Type} (B : A → Type) : Type :=
+| dpair : Πx : A, B x → sigma B
+
+notation `Σ` binders `,` r:(scoped P, sigma P) := r
+
+namespace sigma
+
+section
+
+  parameters {A : Type} {B : A → Type}
+
+  abbreviation dpr1 (p : Σ x, B x) : A := sigma_rec (λ a b, a) p
+  abbreviation dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) := sigma_rec (λ a b, b) p
+
+  theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := refl a
+  theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := refl b
+
+  -- TODO: remove prefix when we can protect it
+  theorem sigma_destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
+  sigma_rec H p
+
+  theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
+  sigma_destruct p (take a b, refl _)
+
+  -- Note that we give the general statment explicitly, to help the unifier
+  theorem dpair_eq {a1 a2 : A} {b1 : B a1} {b2 : B a2} (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2) :
+    dpair a1 b1 = dpair a2 b2 :=
+  (show ∀(b2 : B a2) (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2), dpair a1 b1 = dpair a2 b2, from
+    eq_rec
+      (take (b2' : B a1),
+	assume (H1' : a1 = a1),
+	assume (H2' : eq_rec_on H1' b1 = b2'),
+	show dpair a1 b1 = dpair a1 b2', from
+	  calc
+	    dpair a1 b1 = dpair a1 (eq_rec_on H1' b1) : {symm (eq_rec_on_irrel H1' b1)}
+	      ... = dpair a1 b2' : {H2'}) H1)
+  b2 H1 H2
+
+  theorem sigma_eq {p1 p2 : Σx : A, B x} :
+    ∀(H1 : dpr1 p1 = dpr1 p2) (H2 : eq_rec_on H1 (dpr2 p1) = (dpr2 p2)), p1 = p2 :=
+  sigma_destruct p1 (take a1 b1, sigma_destruct p2 (take a2 b2 H1 H2, dpair_eq H1 H2))
+
+  theorem sigma_inhabited (H1 : inhabited A) (H2 : inhabited (B (default A))) :
+    inhabited (sigma B) :=
+   inhabited_elim H1 (λa, inhabited_elim H2 (λb, inhabited_intro (dpair (default A) b)))
+
+end
+
+instance sigma_inhabited
+
+end sigma

library/standard/data/subtype.lean

@@ -0,0 +1,45 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura, Jeremy Avigad
+
+import logic.classes.inhabited logic.connectives.eq
+
+inductive subtype {A : Type} (P : A → Prop) : Type :=
+| tag : Πx : A, P x → subtype P
+
+notation `{` binders `|` r:(scoped P, subtype P) `}` := r
+
+namespace subtype
+
+section
+  parameter {A : Type}
+  parameter {P : A → Prop}
+
+  -- TODO: make this a coercion?
+  definition  elt_of (a : {x | P x}) : A := subtype_rec (λ x y, x) a
+  theorem has_property (a : {x | P x}) : P (elt_of a) := subtype_rec (λ x y, y) a
+
+  theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := refl a
+
+  theorem subtype_destruct {Q : {x | P x} → Prop} (a : {x | P x})
+      (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a :=
+    subtype_rec H a
+
+  theorem tag_irrelevant {a : A} (H1 H2 : P a) : tag a H1 = tag a H2 := refl (tag a H1)
+
+  theorem tag_ext (a : subtype P) : Π(H : P (elt_of a)), tag (elt_of a) H = a :=
+    subtype_destruct a (take (x : A) (H1 : P x) (H2 : P x), refl _)
+
+  theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
+  (show ∀(H2 : P a2), tag a1 H1 = tag a2 H2, from subst H3 (take H2, tag_irrelevant H1 H2)) H2
+
+  theorem subtype_eq {a1 a2 : {x | P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
+  subtype_destruct a1 (take x1 H1, subtype_destruct a2 (take x2 H2 H, tag_eq H))
+
+  -- TODO: need inhabited
+
+end
+
+end subtype
+
+-- instance subtype_inhabited

library/standard/logic/axioms/examples/diaconescu.lean

@@ -1,8 +1,6 @@
-----------------------------------------------------------------------------------------------------
 -- 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.axioms.hilbert logic.axioms.funext
 using eq_proofs
@@ -15,15 +13,20 @@ hypothesis propext {a b : Prop} : (a → b) → (b → a) → a = b
 
 parameter p : Prop
 
-definition u [private] := epsilon (λ x, x = true ∨ p)
+definition u [private] := epsilon (λx, x = true ∨ p)
 
-definition v [private] := epsilon (λ x, x = false ∨ p)
+definition v [private] := epsilon (λx, x = false ∨ p)
 
 lemma u_def [private] : u = true ∨ p :=
-epsilon_ax (exists_intro true (or_inl (refl true)))
+sorry
+-- previous proof:
+-- epsilon_spec (exists_intro true (or_inl (refl true))
+-- fully elaborated: 
+-- @epsilon_spec Prop (λx : Prop, x = true ∨ p) (exists_intro true (or_inl (refl true)))
 
 lemma v_def [private] : v = false ∨ p :=
-epsilon_ax (exists_intro false (or_inl (refl false)))
+sorry
+-- epsilon_spec (exists_intro false (or_inl (refl false))
 
 lemma uv_implies_p [private] : ¬(u = v) ∨ p :=
 or_elim u_def

library/standard/logic/axioms/hilbert.lean

@@ -1,25 +1,67 @@
-----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-----------------------------------------------------------------------------------------------------
+-- Authors: Leonardo de Moura, Jeremy Avigad
 
 import logic.classes.inhabited logic.connectives.eq logic.connectives.quantifiers
+import data.subtype data.sum
 
-variable epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A
-axiom epsilon_ax {A : Type} {P : A → Prop} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P)
+using subtype
+
+-- logic.axioms.hilbert
+-- ====================
+
+-- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the
+-- constructive one).
+
+axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
+  {x : A | (∃x : A, P x) → P x}
+
+-- In the presence of classical logic, we could prove this from the weaker
+-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : { x : A | P x }
+
+theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
+let u : {x : A | nonempty A → true} := strong_indefinite_description (λa, true) H in
+inhabited_intro (elt_of u)
+
+theorem inhabited_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
+nonempty_imp_inhabited (obtain w Hw, from H, exists_intro w trivial)
+
+
+-- the Hilbert epsilon function
+-- ----------------------------
+
+definition epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A :=
+let u : {x : A | (∃y, P y) → P x} :=
+  strong_indefinite_description P (inhabited_imp_nonempty H) in
+elt_of u
+
+theorem epsilon_spec_aux {A : Type} (H : inhabited A) (P : A → Prop) (Hex : ∃y, P y) :
+    P (@epsilon A H P) :=
+let u : {x : A | (∃y, P y) → P x} :=
+  strong_indefinite_description P (inhabited_imp_nonempty H) in
+has_property u Hex
+
+theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
+    P (@epsilon A (inhabited_exists Hex) P) :=
+epsilon_spec_aux (inhabited_exists Hex) P Hex
 
 theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (inhabited_intro a) (λ x, x = a) = a :=
-epsilon_ax (exists_intro a (refl a))
+epsilon_spec (exists_intro a (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 [inline] := λ x, @epsilon _ (inhabited_exists (H x)) (λ y, R x y),
-    H [inline] := take x, epsilon_ax (H x)
+
+-- 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) :=
+let f [inline] := λx, @epsilon _ (inhabited_exists (H x)) (λy, R x y),
+    H [inline] := take x, epsilon_spec (H x)
 in exists_intro f H
 
-theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) :=
+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,
+  (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))

library/standard/logic/axioms/prop_decidable.lean

@@ -11,11 +11,12 @@ using decidable
 
 -- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle
 theorem inhabited_decidable [instance] (a : Prop) : inhabited (decidable a) :=
-or_elim (em a)
-  (assume Ha,  inhabited_intro (inl Ha))
-  (assume Hna, inhabited_intro (inr Hna))
+nonempty_imp_inhabited
+  (or_elim (em a)
+    (assume Ha, nonempty_intro (inl Ha))
+    (assume Hna, nonempty_intro (inr Hna)))
 
 -- Note that inhabited_decidable is marked as an instance, and it is silently used
 -- for synthesizing the implicit argument in the following 'epsilon'
 theorem prop_decidable [instance] (a : Prop) : decidable a :=
-epsilon (λ d, true)
+epsilon (λd, true)

library/standard/logic/classes/inhabited.lean

@@ -1,19 +1,19 @@
-----------------------------------------------------------------------------------------------------
 -- 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
-----------------------------------------------------------------------------------------------------
 
 import logic.connectives.basic
 
-inductive inhabited (A : Type) : Prop :=
+inductive inhabited (A : Type) : Type :=
 | inhabited_intro : A → inhabited A
 
-theorem inhabited_elim {A : Type} {B : Prop} (H1 : inhabited A) (H2 : A → B) : B :=
+definition inhabited_elim {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
 inhabited_rec H2 H1
 
-theorem inhabited_Prop [instance] : inhabited Prop :=
+definition inhabited_Prop [instance] : inhabited Prop :=
 inhabited_intro true
 
-theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
+definition inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
 inhabited_elim H (take b, inhabited_intro (λa, b))
+
+definition default (A : Type) {H : inhabited A} : A := inhabited_elim H (take a, a)

library/standard/logic/connectives/eq.lean

@@ -14,6 +14,8 @@ inductive eq {A : Type} (a : A) : A → Prop :=
 
 infix `=`:50 := eq
 
+theorem eq_irrel {A : Type} {a : A} (H1 : a = a) : H1 = (refl a) := refl _
+
 theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
 eq_rec H2 H1
 
@@ -24,12 +26,22 @@ calc_subst subst
 calc_refl  refl
 calc_trans trans
 
+theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
+subst H (refl a)
+
 theorem true_ne_false : ¬true = false :=
 assume H : true = false,
   subst H trivial
 
-theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
-subst H (refl a)
+-- eq_rec with arguments swapped, for transporting an element of a dependent type
+definition eq_rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
+eq_rec H2 H1
+
+theorem eq_rec_on_irrel {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec_on H b = b :=
+@trans _ _ (eq_rec_on (refl a) b) _ (refl _) (refl _)
+
+theorem eq_rec_irrel {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec b H = b :=
+eq_rec_on_irrel H b
 
 namespace eq_proofs
   postfix `⁻¹`:100 := symm

library/standard/logic/connectives/quantifiers.lean

@@ -38,9 +38,6 @@ theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
 obtain w Hw, from H2,
 H1 w (and_elim_left Hw) (and_elim_right Hw)
 
-theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A :=
-obtain w Hw, from H, inhabited_intro w
-
 theorem forall_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∀x, φ x) ↔ (∀x, ψ x) :=
 iff_intro
   (assume Hl, take x, iff_elim_left (H x) (Hl x))
@@ -81,7 +78,9 @@ iff_intro
     (assume H2, obtain (w : A) (Hw : ψ w), from H2,
       exists_intro w (or_inr Hw)))
 
-theorem forall_not_inhabited {A : Type} {B : A → Prop} (H : ¬ inhabited A) : ∀x, B x :=
-take x,
-  have Hi : inhabited A, from inhabited_intro x,
-  absurd_elim (B x) Hi H
+abbreviation nonempty (A : Type) := ∃x : A, true
+
+theorem nonempty_intro {A : Type} (x : A) : nonempty A := exists_intro x trivial
+
+theorem inhabited_imp_nonempty {A : Type} (H : inhabited A) : nonempty A :=
+exists_intro (default A) trivial

library/standard/standard.lean

@@ -2,4 +2,4 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic tools.tactic data.num data.string data.pair logic.connectives.cast
+import logic tools.tactic data.num data.string data.prod logic.connectives.cast