feat(library/init): move propext to init/quot, add Jeremy's funext theorem

library/algebra/category/basic.lean

@@ -5,9 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: algebra.category.basic
 Author: Floris van Doorn
 -/
-
-import logic.axioms.funext
-
 open eq eq.ops
 
 structure category [class] (ob : Type) : Type :=

library/algebra/category/constructions.lean

@@ -60,7 +60,7 @@ namespace category
   variables {A : Type} [H : decidable_eq A]
   include H
   definition set_hom [reducible] (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
-  theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
+  theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := rec_subsingleton
   definition set_compose [reducible] {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
   decidable.rec_on
     (H b c)

library/algebra/category/functor.lean

@@ -5,9 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: algebra.category.functor
 Author: Floris van Doorn
 -/
-
 import .basic
-import logic.cast
+import logic.cast logic.funext
 open function
 open category eq eq.ops heq
 

library/data/quotient/classical.lean

@@ -1,8 +1,7 @@
 -- Copyright (c) 2014 Floris van Doorn. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
-
-import algebra.relation data.subtype logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
+import algebra.relation data.subtype logic.axioms.classical logic.axioms.hilbert
 import .basic
 
 namespace quotient

library/init/default.lean

@@ -9,3 +9,4 @@ prelude
 import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod init.priority
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
+import init.funext

library/init/funext.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Jeremy Avigad
+
+function extensionality from quotients
+-/
+prelude
+import init.quot
+
+section
+  open quot
+  variables {A : Type} {B : A → Type}
+
+  private definition fun_eqv (f₁ f₂ : Πx : A, B x) : Prop := ∀x, f₁ x = f₂ x
+
+  infix `~` := fun_eqv    -- this is "~"
+
+  private theorem fun_eqv.refl (f : Πx : A, B x) : f ~ f := take x, rfl
+
+  private theorem fun_eqv.symm {f₁ f₂ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₁ :=
+  λH x, eq.symm (H x)
+
+  private theorem fun_eqv.trans {f₁ f₂ f₃ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
+  λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)
+
+  private theorem fun_eqv.is_equivalence (A : Type) (B : A → Type) : equivalence (@fun_eqv A B) :=
+  and.intro (@fun_eqv.refl A B) (and.intro (@fun_eqv.symm A B) (@fun_eqv.trans A B))
+
+  definition fun_setoid [instance] (A : Type) (B : A → Type) : setoid (Πx : A, B x) :=
+  setoid.mk (@fun_eqv A B) (fun_eqv.is_equivalence A B)
+
+  definition extfun (A : Type) (B : A → Type) : Type :=
+  quot (fun_setoid A B)
+
+  definition fun_to_extfun (f : Πx : A, B x) : extfun A B :=
+  ⟦f⟧
+
+  definition extfun_app (f : extfun A B) : Πx : A, B x :=
+  take x,
+  quot.lift_on f
+    (λf : Πx : A, B x, f x)
+    (λf₁ f₂ H, H x)
+
+  theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
+  assume H, calc
+     f₁ = extfun_app ⟦f₁⟧      : rfl
+    ... = extfun_app ⟦f₂⟧      : {sound H}
+    ... = f₂                   : rfl
+end

library/init/quot.lean

@@ -11,6 +11,8 @@ import init.sigma init.setoid
 open sigma.ops setoid
 
 constant quot.{l}   : Π {A : Type.{l}}, setoid A → Type.{l}
+-- Remark: if we do not use propext here, then we would need a quot.lift for propositions.
+constant propext {a b : Prop} : a ↔ b → a = b
 
 namespace quot
   constant mk        : Π {A : Type}   [s : setoid A], A → quot s

library/logic/axioms/classical.lean

@@ -5,5 +5,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: logic.axioms.classical
 Author: Jeremy Avigad
 -/
-import logic.axioms.prop_complete logic.axioms.funext logic.axioms.hilbert
+import logic.axioms.prop_complete logic.axioms.hilbert
 import logic.axioms.prop_decidable

library/logic/axioms/examples/diaconescu.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.axioms.hilbert logic.axioms.funext
+import logic.axioms.hilbert logic.eq
 open eq.ops nonempty inhabited
 
 -- Diaconescu’s theorem

library/logic/axioms/extensional.lean

@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.axioms.extensional
-Author: Leonardo de Moura
-
-Import extensionality axioms: funext and propext
--/
-import logic.axioms.propext logic.axioms.funext

library/logic/axioms/prop_complete.lean

@@ -6,7 +6,7 @@ Module: logic.axioms.classical
 Author: Leonardo de Moura
 -/
 import logic.connectives logic.quantifiers logic.cast algebra.relation
-import logic.axioms.propext logic.axioms.em
+import logic.axioms.em
 open eq.ops
 
 theorem prop_complete (a : Prop) : a = true ∨ a = false :=

library/logic/axioms/propext.lean

@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.axioms.funext
-Author: Leonardo de Moura
-
-Propositional extensionality.
--/
-axiom propext {a b : Prop} : a ↔ b → a = b

library/logic/funext.lean

@@ -1,17 +1,14 @@
 /-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: logic.axioms.funext
 Author: Leonardo de Moura
 
-Function extensionality.
+Basic theorems for functions
 -/
 import logic.cast algebra.function data.sigma
 open function eq.ops
 
-axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π a, B a} (H : ∀ a, f a = g a), f = g
-
 namespace function
   variables {A B C D: Type}
 
@@ -28,7 +25,7 @@ namespace function
   funext (take x, rfl)
 
   theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x}
-      (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
-  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

src/kernel/quotient/quotient.cpp

@@ -11,15 +11,9 @@ Quotient types for kernels with proof irrelevance.
 #include "kernel/environment.h"
 #include "kernel/quotient/quotient.h"
 
-// Hash code used to identify expected declarations
-#define QUOT_MK_HASH    1806675635
-#define QUOT_SOUND_HASH 392276735
-#define QUOT_EXACT_HASH 843388255
-#define QUOT_LIFT_HASH  3998074667
-#define QUOT_IND_HASH   2559759863
-
 namespace lean {
 static name * g_quotient_extension = nullptr;
+static name * g_propext        = nullptr;
 static name * g_quotient       = nullptr;
 static name * g_quotient_lift  = nullptr;
 static name * g_quotient_ind   = nullptr;
@@ -50,21 +44,7 @@ static environment update(environment const & env, quotient_env_ext const & ext)
     return env.update(g_ext->m_ext_id, std::make_shared<quotient_env_ext>(ext));
 }
 
-static void check_type_hash(environment const & env, name const & d, unsigned hash) {
-    auto decl = env.find(d);
-    if (!decl)
-        throw kernel_exception(env, sstream() << "failed to initialize quotient type, declaration '" << d << "' is missing");
-    if (decl->get_type().hash() != hash)
-        throw kernel_exception(env, sstream() << "invalid quotient builtin declaration '" << d << "', hash code does not match"
-                               << ", expected: " << hash << ", got: " << decl->get_type().hash());
-}
-
 environment declare_quotient(environment const & env) {
-    check_type_hash(env, name{"quot", "mk"},    QUOT_MK_HASH);
-    check_type_hash(env, name{"quot", "sound"}, QUOT_SOUND_HASH);
-    check_type_hash(env, name{"quot", "exact"}, QUOT_EXACT_HASH);
-    check_type_hash(env, name{"quot", "lift"},  QUOT_LIFT_HASH);
-    check_type_hash(env, name{"quot", "ind"},   QUOT_IND_HASH);
     quotient_env_ext ext = get_extension(env);
     ext.m_initialized = true;
     return update(env, ext);
@@ -140,12 +120,13 @@ bool is_quotient_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;
     return
-        n == *g_quotient || n == *g_quotient_lift || n == *g_quotient_ind || n == *g_quotient_mk ||
+        n == *g_propext || n == *g_quotient || n == *g_quotient_lift || n == *g_quotient_ind || n == *g_quotient_mk ||
         n == *g_quotient_sound || n == *g_quotient_exact;
 }
 
 void initialize_quotient_module() {
     g_quotient_extension = new name("quotient_extension");
+    g_propext            = new name{"propext"};
     g_quotient           = new name{"quot"};
     g_quotient_lift      = new name{"quot", "lift"};
     g_quotient_ind       = new name{"quot", "ind"};
@@ -157,6 +138,7 @@ void initialize_quotient_module() {
 
 void finalize_quotient_module() {
     delete g_ext;
+    delete g_propext;
     delete g_quotient_extension;
     delete g_quotient;
     delete g_quotient_lift;