feat(kernel): add experimental support for quotient types

library/init/default.lean

@@ -8,4 +8,4 @@ Authors: Leonardo de Moura
 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
+import init.bool init.num init.sigma init.measurable init.setoid init.quot

library/init/quot.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+Quotient types
+-/
+prelude
+import init.sigma init.setoid
+open sigma.ops setoid
+
+constant quot.{l}   : Π {A : Type.{l}}, setoid A → Type.{l}
+
+namespace quot
+  constant mk        : Π {A : Type}   [s : setoid A], A → quot s
+  notation `⟦`:max a `⟧`:0 := mk a
+
+  constant sound     : Π {A : Type}   [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
+  constant exact     : Π {A : Type}   [s : setoid A] {a b : A}, ⟦a⟧ = ⟦b⟧ → a ≈ b
+  constant lift      : Π {A B : Type} [s : setoid A] (f : A → B), (∀ a b, a ≈ b → f a = f b) → quot s → B
+  constant ind       : ∀ {A : Type}   [s : setoid A] {B : quot s → Prop}, (∀ a, B ⟦a⟧) → ∀ q, B q
+
+  init_quotient
+
+  protected theorem lift_beta {A B : Type} [s : setoid A] (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) (a : A) : lift f c ⟦a⟧ = f a :=
+  rfl
+
+  protected theorem ind_beta {A : Type} [s : setoid A] {B : quot s → Prop} (p : ∀ a, B ⟦a⟧) (a : A) : ind p ⟦a⟧ = p a :=
+  rfl
+
+  protected definition lift_on [reducible] {A B : Type} [s : setoid A] (q : quot s) (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) : B :=
+  lift f c q
+
+  protected theorem induction_on {A : Type} [s : setoid A] {B : quot s → Prop} (q : quot s) (H : ∀ a, B ⟦a⟧) : B q :=
+  ind H q
+
+  section
+  variable {A : Type}
+  variable [s : setoid A]
+  variable {B : quot s → Type}
+  include s
+
+  protected definition indep [reducible] (f : Π a, B ⟦a⟧) (a : A) : Σ q, B q :=
+  ⟨⟦a⟧, f a⟩
+
+  protected lemma indep_coherent (f : Π a, B ⟦a⟧)
+                       (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
+                       : ∀ a b, a ≈ b → indep f a = indep f b  :=
+  λa b e, sigma.equal (sound e) (H a b e)
+
+  protected lemma lift_indep_pr1
+    (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
+    (q : quot s) : (lift (indep f) (indep_coherent f H) q).1 = q  :=
+  ind (λ a, by esimp) q
+
+  protected definition rec [reducible]
+     (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
+     (q : quot s) : B q :=
+  let p := lift (indep f) (indep_coherent f H) q in
+  eq.rec_on (lift_indep_pr1 f H q) (p.2)
+
+  protected definition rec_on [reducible]
+     (q : quot s) (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b) : B q :=
+  rec f H q
+  end
+
+  section
+  variables {A B C : Type}
+  variables [s₁ : setoid A] [s₂ : setoid B]
+  include s₁ s₂
+
+  protected definition lift₂ [reducible]
+     (f : A → B → C)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
+     (q₁ : quot s₁) (q₂ : quot s₂) : C :=
+  lift
+    (λ a₁, lift (λ a₂, f a₁ a₂) (λ a b H, c a₁ a a₁ b (setoid.refl a₁) H) q₂)
+    (λ a b H, ind (λ a', proof c a a' b a' H (setoid.refl a') qed) q₂)
+    q₁
+
+  protected definition lift_on₂ [reducible]
+    (q₁ : quot s₁) (q₂ : quot s₂) (f : A → B → C) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : C :=
+  lift₂ f c q₁ q₂
+
+  protected theorem ind₂ {C : quot s₁ → quot s₂ → Prop} (H : ∀ a b, C ⟦a⟧ ⟦b⟧) (q₁ : quot s₁) (q₂ : quot s₂) : C q₁ q₂ :=
+  quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁
+
+  protected theorem induction_on₂ {C : quot s₁ → quot s₂ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (H : ∀ a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂ :=
+  quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁
+  end
+end quot

src/CMakeLists.txt

@@ -317,6 +317,8 @@ add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
 add_subdirectory(kernel/inductive)
 set(LEAN_LIBS ${LEAN_LIBS} inductive)
+add_subdirectory(kernel/quotient)
+set(LEAN_LIBS ${LEAN_LIBS} quotient)
 add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
 add_subdirectory(library/tactic)

src/frontends/lean/builtin_cmds.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
+#include "kernel/quotient/quotient.h"
 #include "kernel/default_converter.h"
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
@@ -68,6 +69,7 @@ static void print_axioms(parser & p) {
     env.for_each_declaration([&](declaration const & d) {
             name const & n = d.get_name();
             if (!d.is_definition() &&
+                !is_quotient_decl(env, n) &&
                 !inductive::is_inductive_decl(env, n) &&
                 !inductive::is_elim_rule(env, n) &&
                 !inductive::is_intro_rule(env, n)) {
@@ -678,6 +680,10 @@ static environment help_cmd(parser & p) {
     return p.env();
 }
 
+environment init_quotient_cmd(parser & p) {
+    return module::declare_quotient(p.env());
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",          "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -695,6 +701,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("find_decl",     "find definitions and/or theorems", find_cmd));
     add_cmd(r, cmd_info("local",         "define local attributes or notation", local_cmd));
     add_cmd(r, cmd_info("help",          "brief description of available commands and options", help_cmd));
+    add_cmd(r, cmd_info("init_quotient", "initialize quotient type computational rules", init_quotient_cmd));
     add_cmd(r, cmd_info("#erase_cache",  "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#projections",  "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
     add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd));

src/frontends/lean/token_table.cpp

@@ -99,7 +99,7 @@ void init_token_table(token_table & t) {
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent",
-         "include", "omit", "migrate", "#erase_cache", "#projections", "#telescope_eq", nullptr};
+         "include", "omit", "migrate", "init_quotient", "#erase_cache", "#projections", "#telescope_eq", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/init/init.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/init_module.h"
 #include "kernel/init_module.h"
 #include "kernel/inductive/inductive.h"
+#include "kernel/quotient/quotient.h"
 #include "library/init_module.h"
 #include "library/tactic/init_module.h"
 #include "library/definitional/init_module.h"
@@ -27,6 +28,7 @@ void initialize() {
     initialize_sexpr_module();
     initialize_kernel_module();
     initialize_inductive_module();
+    initialize_quotient_module();
     init_default_print_fn();
     initialize_library_module();
     initialize_tactic_module();
@@ -40,6 +42,7 @@ void finalize() {
     finalize_definitional_module();
     finalize_tactic_module();
     finalize_library_module();
+    finalize_quotient_module();
     finalize_inductive_module();
     finalize_kernel_module();
     finalize_sexpr_module();

src/kernel/quotient/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(quotient quotient.cpp)
+target_link_libraries(quotient ${LEAN_LIBS})

src/kernel/quotient/quotient.cpp

@@ -0,0 +1,168 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+Quotient types for kernels with proof irrelevance.
+*/
+#include "util/sstream.h"
+#include "kernel/kernel_exception.h"
+#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_quotient       = nullptr;
+static name * g_quotient_lift  = nullptr;
+static name * g_quotient_ind   = nullptr;
+static name * g_quotient_mk    = nullptr;
+static name * g_quotient_sound = nullptr;
+static name * g_quotient_exact = nullptr;
+
+struct quotient_env_ext : public environment_extension {
+    bool m_initialized;
+    quotient_env_ext():m_initialized(false){}
+};
+
+/** \brief Auxiliary object for registering the environment extension */
+struct quotient_env_ext_reg {
+    unsigned m_ext_id;
+    quotient_env_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<quotient_env_ext>()); }
+};
+
+static quotient_env_ext_reg * g_ext = nullptr;
+
+/** \brief Retrieve environment extension */
+static quotient_env_ext const & get_extension(environment const & env) {
+    return static_cast<quotient_env_ext const &>(env.get_extension(g_ext->m_ext_id));
+}
+
+/** \brief Update environment extension */
+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);
+}
+
+optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(expr const & e, extension_context & ctx) const {
+    environment const & env = ctx.env();
+    expr const & fn         = get_app_fn(e);
+    if (!is_constant(fn))
+        return none_ecs();
+    quotient_env_ext const & ext = get_extension(env);
+    if (!ext.m_initialized)
+        return none_ecs();
+    unsigned mk_pos;
+    if (const_name(fn) == *g_quotient_lift) {
+        mk_pos = 5;
+    } else if (const_name(fn) == *g_quotient_ind) {
+        mk_pos = 4;
+    } else {
+        return none_ecs();
+    }
+
+    buffer<expr> args;
+    get_app_args(e, args);
+    if (args.size() <= mk_pos)
+        return none_ecs();
+
+    auto mk_cs = ctx.whnf(args[mk_pos]);
+    expr const & mk = mk_cs.first;
+    expr const & mk_fn = get_app_fn(mk);
+    if (!is_constant(mk_fn))
+        return none_ecs();
+    if (const_name(mk_fn) != *g_quotient_mk)
+        return none_ecs();
+
+    expr const & f = args[mk_pos-2];
+    expr r = mk_app(f, app_arg(mk));
+    return some_ecs(r, mk_cs.second);
+}
+
+template<typename Ctx>
+optional<expr> is_quot_meta_app_core(Ctx & ctx, expr const & e) {
+    expr const & fn         = get_app_fn(e);
+    if (!is_constant(fn))
+        return none_expr();
+    unsigned mk_pos;
+    if (const_name(fn) == *g_quotient_lift) {
+        mk_pos = 5;
+    } else if (const_name(fn) == *g_quotient_ind) {
+        mk_pos = 4;
+    } else {
+        return none_expr();
+    }
+
+    buffer<expr> args;
+    get_app_args(e, args);
+    if (args.size() <= mk_pos)
+        return none_expr();
+
+    expr mk_app = ctx.whnf(args[mk_pos]).first;
+    return has_expr_metavar_strict(mk_app);
+}
+
+optional<expr> quotient_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
+    return is_quot_meta_app_core(ctx, e);
+}
+
+bool quotient_normalizer_extension::supports(name const & feature) const {
+    return feature == *g_quotient_extension;
+}
+
+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_quotient_sound || n == *g_quotient_exact;
+}
+
+void initialize_quotient_module() {
+    g_quotient_extension = new name("quotient_extension");
+    g_quotient           = new name{"quot"};
+    g_quotient_lift      = new name{"quot", "lift"};
+    g_quotient_ind       = new name{"quot", "ind"};
+    g_quotient_mk        = new name{"quot", "mk"};
+    g_quotient_sound     = new name{"quot", "sound"};
+    g_quotient_exact     = new name{"quot", "exact"};
+    g_ext                = new quotient_env_ext_reg();
+}
+
+void finalize_quotient_module() {
+    delete g_ext;
+    delete g_quotient_extension;
+    delete g_quotient;
+    delete g_quotient_lift;
+    delete g_quotient_ind;
+    delete g_quotient_mk;
+    delete g_quotient_sound;
+    delete g_quotient_exact;
+}
+}

src/kernel/quotient/quotient.h

@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+Quotient types for kernels with proof irrelevance.
+*/
+#pragma once
+
+namespace lean {
+/** \brief Normalizer extension for applying quotient computational rules. */
+class quotient_normalizer_extension : public normalizer_extension {
+public:
+    virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
+    virtual optional<expr> may_reduce_later(expr const & e, extension_context & ctx) const;
+    virtual bool supports(name const & feature) const;
+};
+
+/** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */
+environment declare_quotient(environment const & env);
+/** \brief Return true iff \c n is one of the quotient type builtin constants. */
+bool is_quotient_decl(environment const & env, name const & n);
+void initialize_quotient_module();
+void finalize_quotient_module();
+}

src/library/module.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "util/name_map.h"
 #include "kernel/type_checker.h"
+#include "kernel/quotient/quotient.h"
 #include "library/module.h"
 #include "library/sorry.h"
 #include "library/kernel_serializer.h"
@@ -162,6 +163,7 @@ void register_module_object_reader(std::string const & k, module_object_reader r
 static std::string * g_glvl_key  = nullptr;
 static std::string * g_decl_key  = nullptr;
 static std::string * g_inductive = nullptr;
+static std::string * g_quotient  = nullptr;
 
 namespace module {
 environment add(environment const & env, std::string const & k, std::function<void(serializer &)> const & wr) {
@@ -203,6 +205,19 @@ bool is_definition(environment const & env, name const & n) {
     return ext.m_module_defs.contains(n);
 }
 
+environment declare_quotient(environment const & env) {
+    environment new_env = ::lean::declare_quotient(env);
+    return add(new_env, *g_quotient, [=](serializer &) {});
+}
+
+static void quotient_reader(deserializer &, module_idx, shared_environment & senv,
+                            std::function<void(asynch_update_fn const &)>  &,
+                            std::function<void(delayed_update_fn const &)> &) {
+    senv.update([&](environment const & env) {
+            return ::lean::declare_quotient(env);
+        });
+}
+
 environment add_inductive(environment                  env,
                           level_param_names const &    level_params,
                           unsigned                     num_params,
@@ -560,11 +575,14 @@ void initialize_module() {
     g_glvl_key       = new std::string("glvl");
     g_decl_key       = new std::string("decl");
     g_inductive      = new std::string("ind");
+    g_quotient       = new std::string("quot");
     register_module_object_reader(*g_inductive, module::inductive_reader);
+    register_module_object_reader(*g_quotient, module::quotient_reader);
 }
 
 void finalize_module() {
     delete g_inductive;
+    delete g_quotient;
     delete g_decl_key;
     delete g_glvl_key;
     delete g_object_readers;

src/library/module.h

@@ -106,6 +106,9 @@ environment add_inductive(environment                  env,
                           unsigned                     num_params,
                           list<inductive::inductive_decl> const & decls);
 
+/** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */
+environment declare_quotient(environment const & env);
+
 /**
    \brief Declare a single inductive datatype. This is just a helper function implemented on top of
     the previous (more general) add_inductive.

src/library/standard_kernel.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/inductive/inductive.h"
+#include "kernel/quotient/quotient.h"
 #include "library/inductive_unifier_plugin.h"
 
 namespace lean {
@@ -17,7 +18,8 @@ environment mk_environment(unsigned trust_lvl) {
                                   true /* Eta */,
                                   true /* Type.{0} is impredicative */,
                                   /* builtin support for inductive */
-                                  std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()));
+                                  compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
+                                          std::unique_ptr<normalizer_extension>(new quotient_normalizer_extension())));
     return set_unifier_plugin(env, mk_inductive_unifier_plugin());
 }
 }

tests/lean/run/finset.lean

@@ -0,0 +1,86 @@
+import logic.axioms.extensional data.list
+open list setoid quot
+
+namespace finset
+
+  definition eqv {A : Type} (l₁ l₂ : list A) :=
+  ∀ a, a ∈ l₁ ↔ a ∈ l₂
+
+  infix `∼` := eqv
+
+  theorem eqv.refl {A : Type} (l : list A) : l ∼ l :=
+  λ a, !iff.refl
+
+  theorem eqv.symm {A : Type} {l₁ l₂ : list A} : l₁ ∼ l₂ → l₂ ∼ l₁ :=
+  λ H a, iff.symm (H a)
+
+  theorem eqv.trans {A : Type} {l₁ l₂ l₃ : list A} : l₁ ∼ l₂ → l₂ ∼ l₃ → l₁ ∼ l₃ :=
+  λ H₁ H₂ a, iff.trans (H₁ a) (H₂ a)
+
+  theorem eqv.is_equivalence (A : Type) : equivalence (@eqv A) :=
+  and.intro (@eqv.refl A) (and.intro (@eqv.symm A) (@eqv.trans A))
+
+  definition finset_setoid [instance] (A : Type) : setoid (list A) :=
+  setoid.mk (@eqv A) (eqv.is_equivalence A)
+
+  definition finset (A : Type) : Type :=
+  quot (finset_setoid A)
+
+  definition to_finset {A : Type} (l : list A) : finset A :=
+  ⟦l⟧
+
+  definition mem {A : Type} (a : A) (s : finset A) : Prop :=
+  quot.lift_on s
+    (λ l : list A, a ∈ l)
+    (λ l₁ l₂ r, propext (r a))
+
+  infix ∈ := mem
+
+  theorem mem_list {A : Type} {a : A} {l : list A} : a ∈ l → a ∈ ⟦l⟧ :=
+  λ H, H
+
+  definition empty {A : Type} : finset A :=
+  ⟦nil⟧
+
+  notation `∅` := empty
+
+  definition union {A : Type} (s₁ s₂ : finset A) : finset A :=
+  quot.lift_on₂ s₁ s₂
+    (λ l₁ l₂ : list A, ⟦l₁ ++ l₂⟧)
+    (λ l₁ l₂ l₃ l₄ r₁ r₂,
+      begin
+        apply quot.sound,
+        intro a,
+        apply iff.intro,
+        begin
+          intro inl₁l₂,
+          apply (or.elim (mem_or_mem_of_mem_append inl₁l₂)),
+          intro inl₁, exact (mem_append_of_mem_or_mem (or.inl (iff.mp (r₁ a) inl₁))),
+          intro inl₂, exact (mem_append_of_mem_or_mem (or.inr (iff.mp (r₂ a) inl₂)))
+        end,
+        begin
+          intro inl₃l₄,
+          apply (or.elim (mem_or_mem_of_mem_append inl₃l₄)),
+          intro inl₃, exact (mem_append_of_mem_or_mem (or.inl (iff.mp' (r₁ a) inl₃))),
+          intro inl₄, exact (mem_append_of_mem_or_mem (or.inr (iff.mp' (r₂ a) inl₄)))
+        end,
+      end)
+
+  infix `∪` := union
+
+  theorem mem_union_left {A : Type} (s₁ s₂ : finset A) (a : A) : a ∈ s₁ → a ∈ s₁ ∪ s₂ :=
+  quot.ind₂ (λ l₁ l₂ ainl₁, mem_append_left l₂ ainl₁) s₁ s₂
+
+  theorem mem_union_right {A : Type} (s₁ s₂ : finset A) (a : A) : a ∈ s₂ → a ∈ s₁ ∪ s₂ :=
+  quot.ind₂ (λ l₁ l₂ ainl₂, mem_append_right l₁ ainl₂) s₁ s₂
+
+  theorem union_empty {A : Type} (s : finset A) : s ∪ ∅ = s :=
+  quot.induction_on s (λ l, quot.sound (λ a, by rewrite append_nil_right))
+
+  theorem empty_union {A : Type} (s : finset A) : ∅ ∪ s = s :=
+  quot.induction_on s (λ l, quot.sound (λ a, by rewrite append_nil_left))
+
+  example : to_finset (1::2::nil) ∪ to_finset (2::3::nil) = ⟦1 :: 2 :: 2 :: 3 :: nil⟧ :=
+  rfl
+
+end finset

tests/lean/run/pquot.lean

@@ -86,7 +86,7 @@ mk :: (refl  : ∀x, R x x)
       (trans : ∀{x y z}, R x y → R y z → R x z)
 
 -- Definiable quotients are exact if R is an equivalence relation
-theorem quot.exact {A : Type} {R : A → A → Prop} (eqv : is_equiv R) (q : dquot R) : pquot.exact R :=
+theorem quot_exact {A : Type} {R : A → A → Prop} (eqv : is_equiv R) (q : dquot R) : pquot.exact R :=
 λ (a b : A) (H : pquot.abs R a = pquot.abs R b),
   have H₁ : pquot.abs R a = pquot.abs R a → R (dquot.rep q (pquot.abs R a)) (dquot.rep q (pquot.abs R a)),
     from λH, is_equiv.refl eqv _,