From b960e123b15adc5d9b27e0e41566f25149a466f1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 31 Mar 2015 21:45:11 -0700 Subject: [PATCH] feat(kernel): add experimental support for quotient types --- library/init/default.lean | 2 +- library/init/quot.lean | 91 +++++++++++++++ src/CMakeLists.txt | 2 + src/frontends/lean/builtin_cmds.cpp | 7 ++ src/frontends/lean/token_table.cpp | 2 +- src/init/init.cpp | 3 + src/kernel/quotient/CMakeLists.txt | 2 + src/kernel/quotient/quotient.cpp | 168 ++++++++++++++++++++++++++++ src/kernel/quotient/quotient.h | 26 +++++ src/library/module.cpp | 22 +++- src/library/module.h | 3 + src/library/standard_kernel.cpp | 4 +- tests/lean/run/finset.lean | 86 ++++++++++++++ tests/lean/run/pquot.lean | 2 +- 14 files changed, 414 insertions(+), 6 deletions(-) create mode 100644 library/init/quot.lean create mode 100644 src/kernel/quotient/CMakeLists.txt create mode 100644 src/kernel/quotient/quotient.cpp create mode 100644 src/kernel/quotient/quotient.h create mode 100644 tests/lean/run/finset.lean diff --git a/library/init/default.lean b/library/init/default.lean index 77bd3d61b..538a19c64 100644 --- a/library/init/default.lean +++ b/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 diff --git a/library/init/quot.lean b/library/init/quot.lean new file mode 100644 index 000000000..49b7c3725 --- /dev/null +++ b/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 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 39689d82b..7ae601f63 100644 --- a/src/CMakeLists.txt +++ b/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) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index f85b07eab..b5fc8270d 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index e52591d8e..ff2559e8b 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/init/init.cpp b/src/init/init.cpp index 255b438b4..1cb6aedf5 100644 --- a/src/init/init.cpp +++ b/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(); diff --git a/src/kernel/quotient/CMakeLists.txt b/src/kernel/quotient/CMakeLists.txt new file mode 100644 index 000000000..831b8a6ce --- /dev/null +++ b/src/kernel/quotient/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(quotient quotient.cpp) +target_link_libraries(quotient ${LEAN_LIBS}) diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp new file mode 100644 index 000000000..30e8ace85 --- /dev/null +++ b/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()); } +}; + +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(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(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> 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 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 +optional 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 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 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; +} +} diff --git a/src/kernel/quotient/quotient.h b/src/kernel/quotient/quotient.h new file mode 100644 index 000000000..138d4d211 --- /dev/null +++ b/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> operator()(expr const & e, extension_context & ctx) const; + virtual optional 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(); +} diff --git a/src/library/module.cpp b/src/library/module.cpp index 94638728a..478dce600 100644 --- a/src/library/module.cpp +++ b/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" @@ -159,9 +160,10 @@ void register_module_object_reader(std::string const & k, module_object_reader r readers[k] = r; } -static std::string * g_glvl_key = nullptr; -static std::string * g_decl_key = nullptr; +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 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 &, + std::function &) { + 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; diff --git a/src/library/module.h b/src/library/module.h index 79c774468..a6a627484 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -106,6 +106,9 @@ environment add_inductive(environment env, unsigned num_params, list 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. diff --git a/src/library/standard_kernel.cpp b/src/library/standard_kernel.cpp index ad80b25fb..947999af2 100644 --- a/src/library/standard_kernel.cpp +++ b/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(new inductive_normalizer_extension())); + compose(std::unique_ptr(new inductive_normalizer_extension()), + std::unique_ptr(new quotient_normalizer_extension()))); return set_unifier_plugin(env, mk_inductive_unifier_plugin()); } } diff --git a/tests/lean/run/finset.lean b/tests/lean/run/finset.lean new file mode 100644 index 000000000..bef56dfef --- /dev/null +++ b/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 diff --git a/tests/lean/run/pquot.lean b/tests/lean/run/pquot.lean index 8d9587e7b..708327380 100644 --- a/tests/lean/run/pquot.lean +++ b/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 _,