refactor(library): remove unifier_plugin
This commit is contained in:
Leonardo de Moura
parent
c98f1bfd24
commit
384e8bf7bf
33 changed files with 65 additions and 1612 deletions
|
|
@ -712,10 +712,13 @@ lemma count_gt_zero_of_mem : ∀ {a : A} {l : list A}, a ∈ l → count a l > 0
|
|||
... > 0 : count_gt_zero_of_mem this)
|
||||
|
||||
lemma count_eq_zero_of_not_mem {a : A} {l : list A} (h : a ∉ l) : count a l = 0 :=
|
||||
match count a l with
|
||||
| zero := suppose count a l = zero, this
|
||||
| (succ n) := suppose count a l = succ n, absurd (mem_of_count_gt_zero (begin rewrite this, exact dec_trivial end)) h
|
||||
end rfl
|
||||
have ∀ n, count a l = n → count a l = 0,
|
||||
begin
|
||||
intro n, cases n,
|
||||
{ intro this, exact this },
|
||||
{ intro this, exact absurd (mem_of_count_gt_zero (begin rewrite this, exact dec_trivial end)) h }
|
||||
end,
|
||||
this (count a l) rfl
|
||||
|
||||
end count
|
||||
end list
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ namespace sigma
|
|||
variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}}
|
||||
|
||||
definition unpack {C : (Σa, B a) → Type} {u : Σa, B a} (H : C ⟨u.1 , u.2⟩) : C u :=
|
||||
destruct u (λx y H, H) H
|
||||
begin cases u, exact H end
|
||||
|
||||
theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
|
||||
(HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ :=
|
||||
|
|
@ -42,21 +42,4 @@ namespace sigma
|
|||
definition pr3 [reducible] (x : Σ a b, C a b) := x.2.2
|
||||
definition pr3' [reducible] (x : Σ a b c, D a b c) := x.2.2.1
|
||||
definition pr4 [reducible] (x : Σ a b c, D a b c) := x.2.2.2
|
||||
|
||||
theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
|
||||
(H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : cast (dcongr_arg2 C H₁ H₂) c₁ = c₂) :
|
||||
⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
|
||||
dcongr_arg3 dtrip H₁ H₂ H₃
|
||||
|
||||
theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
|
||||
{c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
|
||||
(H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
|
||||
hdcongr_arg3 dtrip H₁ (heq_of_eq H₂) H₃
|
||||
|
||||
theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
|
||||
∀(H₁ : pr1 p₁ = pr1 p₂) (H₂ : pr2' p₁ = pr2' p₂)
|
||||
(H₃ : eq.rec_on (congr_arg2 C H₁ H₂) (pr3 p₁) = pr3 p₂), p₁ = p₂ :=
|
||||
destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
|
||||
(take b₂ c₂ H₁ H₂ H₃, ndtrip_eq H₁ H₂ H₃))))
|
||||
|
||||
end sigma
|
||||
|
|
|
|||
|
|
@ -187,7 +187,9 @@ variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
|
|||
theorem eq_of_heq (H : a == a') : a = a' :=
|
||||
have H₁ : ∀ (Ht : A = A), eq.rec a Ht = a, from
|
||||
λ Ht, eq.refl a,
|
||||
heq.rec H₁ H (eq.refl A)
|
||||
have H₂ : ∀ (Ht : A = A), eq.rec a Ht = a', from
|
||||
heq.rec H₁ H,
|
||||
H₂ (eq.refl A)
|
||||
|
||||
theorem heq.elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b)
|
||||
: P a → P b := eq.rec_on (eq_of_heq H₁)
|
||||
|
|
|
|||
|
|
@ -32,7 +32,11 @@ namespace nat
|
|||
|
||||
protected definition no_confusion [reducible] [unfold 4]
|
||||
{P : Type} {v₁ v₂ : ℕ} (H : v₁ = v₂) : nat.no_confusion_type P v₁ v₂ :=
|
||||
eq.rec (λ H₁ : v₁ = v₁, nat.rec (λ h, h) (λ a ih h, h (eq.refl a)) v₁) H H
|
||||
have v₁ = v₁ → nat.no_confusion_type P v₁ v₁, from
|
||||
λ H₁ : v₁ = v₁, nat.rec (λ h, h) (λ a ih h, h (eq.refl a)) v₁,
|
||||
have v₁ = v₂ → nat.no_confusion_type P v₁ v₂, from
|
||||
eq.rec this H,
|
||||
this H
|
||||
|
||||
/- basic definitions on natural numbers -/
|
||||
inductive le (a : ℕ) : ℕ → Prop :=
|
||||
|
|
|
|||
|
|
@ -124,17 +124,4 @@ section
|
|||
(Hc : cast (eq_of_heq (hcongr_arg2 C Ha Hb)) c = c')
|
||||
: f a b c = f a' b' c' :=
|
||||
eq_of_heq (hcongr_arg3 f Ha Hb (eq_rec_to_heq Hc))
|
||||
|
||||
theorem hhdcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
|
||||
(Hc : c == c')
|
||||
(Hd : cast (dcongr_arg3 D Ha (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hb)
|
||||
(!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hc)) d = d')
|
||||
: f a b c d = f a' b' c' d' :=
|
||||
eq_of_heq (hcongr_arg4 f Ha Hb Hc (eq_rec_to_heq Hd))
|
||||
|
||||
theorem hddcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
|
||||
(Hc : cast (eq_of_heq (hcongr_arg2 C Ha Hb)) c = c')
|
||||
(Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d')
|
||||
: f a b c d = f a' b' c' d' :=
|
||||
eq_of_heq (hcongr_arg4 f Ha Hb (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
|
||||
end
|
||||
|
|
|
|||
|
|
@ -26,10 +26,6 @@ namespace eq
|
|||
theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : eq.rec_on H₁ b = eq.rec_on H₂ b :=
|
||||
rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹
|
||||
|
||||
theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
|
||||
eq.rec_on H b = eq.rec_on H' b :=
|
||||
eq.drec_on H (λ(H' : f a = f a), !rec_on_id⁻¹) H'
|
||||
|
||||
theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) :
|
||||
eq.drec_on H b = eq.drec_on H' b :=
|
||||
proof_irrel H H' ▸ rfl
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
|
|||
coercion.cpp private.cpp placeholder.cpp aliases.cpp level_names.cpp
|
||||
update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
|
||||
standard_kernel.cpp sorry.cpp replace_visitor.cpp unifier.cpp
|
||||
unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp
|
||||
explicit.cpp num.cpp
|
||||
string.cpp head_map.cpp match.cpp definition_cache.cpp
|
||||
declaration_index.cpp class.cpp util.cpp print.cpp annotation.cpp
|
||||
typed_expr.cpp let.cpp protected.cpp
|
||||
|
|
|
|||
|
|
@ -6,19 +6,17 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "kernel/hits/hits.h"
|
||||
#include "library/inductive_unifier_plugin.h"
|
||||
|
||||
namespace lean {
|
||||
using inductive::inductive_normalizer_extension;
|
||||
/** \brief Create Lean environment for Homotopy Type Theory */
|
||||
environment mk_hott_environment(unsigned trust_lvl) {
|
||||
environment env = environment(trust_lvl,
|
||||
false /* Type.{0} is not proof irrelevant */,
|
||||
true /* Eta */,
|
||||
false /* Type.{0} is not impredicative */,
|
||||
/* builtin support for inductive and hits */
|
||||
compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
|
||||
std::unique_ptr<normalizer_extension>(new hits_normalizer_extension())));
|
||||
return set_unifier_plugin(env, mk_inductive_unifier_plugin());
|
||||
return environment(trust_lvl,
|
||||
false /* Type.{0} is not proof irrelevant */,
|
||||
true /* Eta */,
|
||||
false /* Type.{0} is not impredicative */,
|
||||
/* builtin support for inductive and hits */
|
||||
compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
|
||||
std::unique_ptr<normalizer_extension>(new hits_normalizer_extension())));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,158 +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
|
||||
*/
|
||||
#include "util/lazy_list_fn.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "library/unifier_plugin.h"
|
||||
#include "library/unifier.h"
|
||||
#include "library/util.h"
|
||||
|
||||
namespace lean {
|
||||
static optional<expr> is_elim_meta_app(old_type_checker & ctx, expr const & e) {
|
||||
expr const & elim_fn = get_app_fn(e);
|
||||
if (!is_constant(elim_fn))
|
||||
return none_expr();
|
||||
unsigned major_idx = 0;
|
||||
if (auto idx = inductive::get_elim_major_idx(ctx.env(), const_name(elim_fn)))
|
||||
major_idx = *idx;
|
||||
else
|
||||
return none_expr();
|
||||
buffer<expr> elim_args;
|
||||
get_app_args(e, elim_args);
|
||||
if (elim_args.size() < major_idx + 1)
|
||||
return none_expr();
|
||||
expr intro_app = ctx.whnf(elim_args[major_idx]).first;
|
||||
return ctx.is_stuck(intro_app);
|
||||
}
|
||||
|
||||
class inductive_unifier_plugin_cell : public unifier_plugin_cell {
|
||||
/** \brief Return true iff the lhs or rhs of the constraint c is of the form (elim ... (?m ...) ...) */
|
||||
bool is_elim_meta_cnstr(old_type_checker & tc, constraint const & c) const {
|
||||
return false;
|
||||
return is_eq_cnstr(c) && (is_elim_meta_app(tc, cnstr_lhs_expr(c)) ||
|
||||
is_elim_meta_app(tc, cnstr_rhs_expr(c)));
|
||||
}
|
||||
|
||||
/** \brief Return true iff \c e is of the form (?m ... (intro ...) ...) */
|
||||
bool is_meta_intro_app(old_type_checker & tc, expr const & e) const {
|
||||
if (!is_app(e) || !is_meta(e))
|
||||
return false;
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
for (expr const & a : args) {
|
||||
expr arg = get_app_fn(a);
|
||||
if (!is_constant(arg))
|
||||
continue;
|
||||
if (inductive::is_intro_rule(tc.env(), const_name(arg)))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/** \brief Return true iff the lhs or rhs of the constraint c is of the form (?m ... (intro ...)) */
|
||||
bool is_meta_intro_cnstr(old_type_checker & tc, constraint const & c) const {
|
||||
return is_eq_cnstr(c) && (is_meta_intro_app(tc, cnstr_lhs_expr(c)) || is_meta_intro_app(tc, cnstr_rhs_expr(c)));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Given (elim args) =?= t, where elim is the eliminator/recursor for the inductive declaration \c decl,
|
||||
and the major premise is of the form (?m ...), we create a case split where we try to assign (?m ...)
|
||||
to the different constructors of decl.
|
||||
*/
|
||||
lazy_list<constraints> add_elim_meta_cnstrs(old_type_checker & tc, inductive::inductive_decl const & decl,
|
||||
expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
|
||||
constraint_seq cs) const {
|
||||
lean_assert(is_constant(elim));
|
||||
environment const & env = tc.env();
|
||||
levels elim_lvls = const_levels(elim);
|
||||
unsigned elim_num_lvls = length(elim_lvls);
|
||||
unsigned major_idx = *inductive::get_elim_major_idx(env, const_name(elim));
|
||||
expr meta = args[major_idx]; // save this argument, we will update it
|
||||
lean_assert(has_expr_metavar_strict(meta));
|
||||
buffer<expr> margs;
|
||||
expr const & m = get_app_args(meta, margs);
|
||||
expr mtype = tc.infer(m, cs);
|
||||
buffer<constraints> alts;
|
||||
for (auto const & intro : inductive::inductive_decl_intros(decl)) {
|
||||
constraint_seq cs_intro = cs;
|
||||
name const & intro_name = inductive::intro_rule_name(intro);
|
||||
declaration intro_decl = env.get(intro_name);
|
||||
levels intro_lvls;
|
||||
if (intro_decl.get_num_univ_params() == elim_num_lvls) {
|
||||
intro_lvls = elim_lvls;
|
||||
} else {
|
||||
lean_assert(intro_decl.get_num_univ_params() == elim_num_lvls - 1);
|
||||
intro_lvls = tail(elim_lvls);
|
||||
}
|
||||
expr intro_fn = mk_constant(inductive::intro_rule_name(intro), intro_lvls);
|
||||
expr hint = intro_fn;
|
||||
expr intro_type = tc.whnf(inductive::intro_rule_type(intro), cs_intro);
|
||||
while (is_pi(intro_type)) {
|
||||
expr new_arg = mk_app(mk_aux_metavar_for(mtype), margs);
|
||||
hint = mk_app(hint, new_arg);
|
||||
intro_type = tc.whnf(instantiate(binding_body(intro_type), new_arg), cs_intro);
|
||||
}
|
||||
constraint c1 = mk_eq_cnstr(meta, hint, j);
|
||||
args[major_idx] = hint;
|
||||
expr reduce_elim = tc.whnf(mk_app(elim, args), cs_intro);
|
||||
constraint c2 = mk_eq_cnstr(reduce_elim, t, j);
|
||||
cs_intro = constraint_seq(c1) + constraint_seq(c2) + cs_intro;
|
||||
buffer<constraint> cs_buffer;
|
||||
cs_intro.linearize(cs_buffer);
|
||||
alts.push_back(to_list(cs_buffer.begin(), cs_buffer.end()));
|
||||
}
|
||||
return to_lazy(to_list(alts.begin(), alts.end()));
|
||||
}
|
||||
|
||||
lazy_list<constraints> process_elim_meta_core(old_type_checker & tc, expr const & lhs, expr const & rhs, justification const & j) const {
|
||||
lean_assert(is_elim_meta_app(tc, lhs));
|
||||
auto dcs = tc.is_def_eq_types(lhs, rhs, j);
|
||||
if (!dcs.first)
|
||||
return lazy_list<constraints>();
|
||||
constraint_seq cs = dcs.second;
|
||||
buffer<expr> args;
|
||||
expr const & elim = get_app_args(lhs, args);
|
||||
environment const & env = tc.env();
|
||||
auto it_name = *inductive::is_elim_rule(env, const_name(elim));
|
||||
if (is_recursive_datatype(env, it_name))
|
||||
return lazy_list<constraints>();
|
||||
auto decls = *inductive::is_inductive_decl(env, it_name);
|
||||
for (auto const & d : std::get<2>(decls)) {
|
||||
if (inductive::inductive_decl_name(d) == it_name)
|
||||
return add_elim_meta_cnstrs(tc, d, elim, args, rhs, j, cs);
|
||||
}
|
||||
lean_unreachable(); // LCOV_EXCL_LINE
|
||||
}
|
||||
|
||||
public:
|
||||
/**
|
||||
\brief Try to solve constraint of the form (elim ... (?m ...)) =?= t, by assigning (?m ...) to the introduction rules
|
||||
associated with the eliminator \c elim.
|
||||
*/
|
||||
virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
|
||||
if (!is_eq_cnstr(c))
|
||||
return lazy_list<constraints>();
|
||||
expr const & lhs = cnstr_lhs_expr(c);
|
||||
expr const & rhs = cnstr_rhs_expr(c);
|
||||
justification const & j = c.get_justification();
|
||||
if (is_elim_meta_app(tc, lhs))
|
||||
return process_elim_meta_core(tc, lhs, rhs, j);
|
||||
else if (is_elim_meta_app(tc, rhs))
|
||||
return process_elim_meta_core(tc, rhs, lhs, j);
|
||||
else
|
||||
return lazy_list<constraints>();
|
||||
}
|
||||
|
||||
virtual bool delay_constraint(old_type_checker & tc, constraint const & c) const {
|
||||
return is_elim_meta_cnstr(tc, c) || is_meta_intro_cnstr(tc, c);
|
||||
}
|
||||
};
|
||||
|
||||
unifier_plugin mk_inductive_unifier_plugin() {
|
||||
return std::make_shared<inductive_unifier_plugin_cell>();
|
||||
}
|
||||
}
|
||||
|
|
@ -1,12 +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
|
||||
*/
|
||||
#pragma once
|
||||
#include "library/unifier_plugin.h"
|
||||
namespace lean {
|
||||
/** \brief Return a unifier plugin that handles constraints containing eliminators and introductions */
|
||||
unifier_plugin mk_inductive_unifier_plugin();
|
||||
}
|
||||
|
|
@ -23,7 +23,6 @@ Author: Leonardo de Moura
|
|||
#include "library/reducible.h"
|
||||
#include "library/aliases.h"
|
||||
#include "library/coercion.h"
|
||||
#include "library/unifier_plugin.h"
|
||||
#include "library/io_state.h"
|
||||
#include "library/idx_metavar.h"
|
||||
#include "library/sorry.h"
|
||||
|
|
@ -94,7 +93,6 @@ void initialize_library_module() {
|
|||
initialize_reducible();
|
||||
initialize_aliases();
|
||||
initialize_coercion();
|
||||
initialize_unifier_plugin();
|
||||
initialize_sorry();
|
||||
initialize_class();
|
||||
initialize_library_util();
|
||||
|
|
@ -142,7 +140,6 @@ void finalize_library_module() {
|
|||
finalize_library_util();
|
||||
finalize_class();
|
||||
finalize_sorry();
|
||||
finalize_unifier_plugin();
|
||||
finalize_coercion();
|
||||
finalize_aliases();
|
||||
finalize_reducible();
|
||||
|
|
|
|||
|
|
@ -6,20 +6,18 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "kernel/quotient/quotient.h"
|
||||
#include "library/inductive_unifier_plugin.h"
|
||||
|
||||
namespace lean {
|
||||
using inductive::inductive_normalizer_extension;
|
||||
|
||||
/** \brief Create standard Lean environment */
|
||||
environment mk_environment(unsigned trust_lvl) {
|
||||
environment env = environment(trust_lvl,
|
||||
true /* Type.{0} is proof irrelevant */,
|
||||
true /* Eta */,
|
||||
true /* Type.{0} is impredicative */,
|
||||
/* builtin support for inductive */
|
||||
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());
|
||||
return environment(trust_lvl,
|
||||
true /* Type.{0} is proof irrelevant */,
|
||||
true /* Eta */,
|
||||
true /* Type.{0} is impredicative */,
|
||||
/* builtin support for inductive */
|
||||
compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
|
||||
std::unique_ptr<normalizer_extension>(new quotient_normalizer_extension())));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -28,7 +28,6 @@ Author: Leonardo de Moura
|
|||
#include "library/module.h"
|
||||
#include "library/unifier.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/unifier_plugin.h"
|
||||
#include "library/print.h"
|
||||
#include "library/expr_lt.h"
|
||||
#include "library/projection.h"
|
||||
|
|
@ -344,7 +343,6 @@ struct unifier_fn {
|
|||
constraints m_postponed; // constraints that will not be solved
|
||||
owned_map m_owned_map; // mapping from metavariable name m to constraint idx
|
||||
expr_map m_type_map; // auxiliary map for storing the type of the expr in choice constraints
|
||||
unifier_plugin m_plugin;
|
||||
type_checker_ptr m_tc;
|
||||
type_checker_ptr m_flex_rigid_tc; // type checker used when solving flex rigid constraints. By default,
|
||||
// only the definitions from the main module are treated as transparent.
|
||||
|
|
@ -450,7 +448,7 @@ struct unifier_fn {
|
|||
unifier_fn(environment const & env, unsigned num_cs, constraint const * cs,
|
||||
substitution const & s,
|
||||
unifier_config const & cfg):
|
||||
m_env(env), m_subst(s), m_plugin(get_unifier_plugin(env)),
|
||||
m_env(env), m_subst(s),
|
||||
m_config(cfg), m_num_steps(0) {
|
||||
switch (m_config.m_kind) {
|
||||
case unifier_kind::Cheap:
|
||||
|
|
@ -1074,8 +1072,7 @@ struct unifier_fn {
|
|||
add_meta_occ(rhs, cidx);
|
||||
return true;
|
||||
} else if (m_tc->may_reduce_later(lhs) ||
|
||||
m_tc->may_reduce_later(rhs) ||
|
||||
m_plugin->delay_constraint(*m_tc, c)) {
|
||||
m_tc->may_reduce_later(rhs)) {
|
||||
unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
|
||||
add_meta_occs(lhs, cidx);
|
||||
add_meta_occs(rhs, cidx);
|
||||
|
|
@ -1575,7 +1572,7 @@ struct unifier_fn {
|
|||
|
||||
bool process_plugin_constraint(constraint const & c) {
|
||||
lean_assert(!is_choice_cnstr(c));
|
||||
lazy_list<constraints> alts = m_plugin->solve(*m_tc, c);
|
||||
lazy_list<constraints> alts;
|
||||
alts = append(alts, process_const_const_cnstr(c));
|
||||
return process_lazy_constraints(alts, c.get_justification());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,94 +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
|
||||
*/
|
||||
#include "util/lazy_list_fn.h"
|
||||
#include "library/unifier_plugin.h"
|
||||
|
||||
namespace lean {
|
||||
class binary_unifier_plugin_cell : public unifier_plugin_cell {
|
||||
protected:
|
||||
unifier_plugin m_p1;
|
||||
unifier_plugin m_p2;
|
||||
public:
|
||||
binary_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):m_p1(p1), m_p2(p2) {}
|
||||
virtual bool delay_constraint(old_type_checker & tc, constraint const & c) const {
|
||||
return m_p1->delay_constraint(tc, c) || m_p2->delay_constraint(tc, c);
|
||||
}
|
||||
};
|
||||
|
||||
class append_unifier_plugin_cell : public binary_unifier_plugin_cell {
|
||||
public:
|
||||
append_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
|
||||
virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
|
||||
return append(m_p1->solve(tc, c), m_p2->solve(tc, c));
|
||||
}
|
||||
};
|
||||
|
||||
class orelse_unifier_plugin_cell : public binary_unifier_plugin_cell {
|
||||
public:
|
||||
orelse_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
|
||||
virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
|
||||
return orelse(m_p1->solve(tc, c), m_p2->solve(tc, c));
|
||||
}
|
||||
};
|
||||
|
||||
unifier_plugin append(unifier_plugin const & p1, unifier_plugin const & p2) {
|
||||
return std::make_shared<append_unifier_plugin_cell>(p1, p2);
|
||||
}
|
||||
|
||||
unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2) {
|
||||
return std::make_shared<orelse_unifier_plugin_cell>(p1, p2);
|
||||
}
|
||||
|
||||
static unifier_plugin noop_unifier_plugin() {
|
||||
class noop_unifier_plugin_cell : public unifier_plugin_cell {
|
||||
public:
|
||||
virtual lazy_list<constraints> solve(old_type_checker &, constraint const &) const {
|
||||
return lazy_list<constraints>();
|
||||
}
|
||||
virtual bool delay_constraint(old_type_checker &, constraint const &) const { return false; }
|
||||
};
|
||||
return std::make_shared<noop_unifier_plugin_cell>();
|
||||
}
|
||||
|
||||
struct unifier_plugin_ext : public environment_extension {
|
||||
unifier_plugin m_plugin;
|
||||
unifier_plugin_ext() {
|
||||
m_plugin = noop_unifier_plugin();
|
||||
}
|
||||
};
|
||||
|
||||
struct unifier_plugin_ext_reg {
|
||||
unsigned m_ext_id;
|
||||
unifier_plugin_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<unifier_plugin_ext>()); }
|
||||
};
|
||||
|
||||
static unifier_plugin_ext_reg * g_ext = nullptr;
|
||||
static unifier_plugin_ext const & get_extension(environment const & env) {
|
||||
return static_cast<unifier_plugin_ext const &>(env.get_extension(g_ext->m_ext_id));
|
||||
}
|
||||
static environment update(environment const & env, unifier_plugin_ext const & ext) {
|
||||
return env.update(g_ext->m_ext_id, std::make_shared<unifier_plugin_ext>(ext));
|
||||
}
|
||||
|
||||
void initialize_unifier_plugin() {
|
||||
g_ext = new unifier_plugin_ext_reg();
|
||||
}
|
||||
|
||||
void finalize_unifier_plugin() {
|
||||
delete g_ext;
|
||||
}
|
||||
|
||||
environment set_unifier_plugin(environment const & env, unifier_plugin const & p) {
|
||||
unifier_plugin_ext ext = get_extension(env);
|
||||
ext.m_plugin = p;
|
||||
return update(env, ext);
|
||||
}
|
||||
|
||||
unifier_plugin const & get_unifier_plugin(environment const & env) {
|
||||
return get_extension(env).m_plugin;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,40 +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
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lazy_list.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "library/constraint.h"
|
||||
#include "library/old_type_checker.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief A unifier_plugin provides a simple way to extend the \c unify procedures.
|
||||
Whenever, the default implementation does not know how to solve a constraint, it invokes the plugin.
|
||||
The plugin return a lazy_list (stream) of possible solutions. Each "solution" is represented as
|
||||
a new list of constraints.
|
||||
|
||||
The method \c delay_constraint is invoked to decide whether the particular constraint should
|
||||
be delayed. This is useful when implementing unification plugins
|
||||
*/
|
||||
class unifier_plugin_cell {
|
||||
public:
|
||||
virtual ~unifier_plugin_cell() {}
|
||||
virtual lazy_list<constraints> solve(old_type_checker &, constraint const &) const = 0;
|
||||
virtual bool delay_constraint(old_type_checker &, constraint const &) const = 0;
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<unifier_plugin_cell> unifier_plugin;
|
||||
/** \brief Combine two plugins by appending their solutions. */
|
||||
unifier_plugin append(unifier_plugin const & p1, unifier_plugin const & p2);
|
||||
/** \brief Combine two plugins by taking the solutions of p1, if it is empty, then return solutions of p2 */
|
||||
unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2);
|
||||
|
||||
environment set_unifier_plugin(environment const & env, unifier_plugin const & p);
|
||||
unifier_plugin const & get_unifier_plugin(environment const & env);
|
||||
void initialize_unifier_plugin();
|
||||
void finalize_unifier_plugin();
|
||||
}
|
||||
|
|
@ -1,14 +1,13 @@
|
|||
inductive fibrant [class] (T : Type) : Type :=
|
||||
mk : fibrant T
|
||||
|
||||
inductive Fib : Type :=
|
||||
mk : ΠA : Type, fibrant A → Fib
|
||||
structure Fib : Type :=
|
||||
(type : Type) (is_fibrant : fibrant type)
|
||||
|
||||
namespace Fib
|
||||
|
||||
definition type [coercion] (F : Fib) : Type := Fib.rec_on F (λA f, A)
|
||||
|
||||
definition is_fibrant [instance] (F : Fib) : fibrant (type F) := Fib.rec_on F (λA f, f)
|
||||
attribute type [coercion]
|
||||
attribute is_fibrant [instance]
|
||||
|
||||
end Fib
|
||||
-- open Fib
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
error_pos_bug2.lean:17:37: error: type expected at
|
||||
error_pos_bug2.lean:16:37: error: type expected at
|
||||
A
|
||||
|
|
|
|||
|
|
@ -1,9 +0,0 @@
|
|||
VISIT eq2.lean
|
||||
WAIT
|
||||
REPLACE 134
|
||||
(λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : (eq.rec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂),
|
||||
WAIT
|
||||
REPLACE 134
|
||||
(λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : _ = c₂),
|
||||
WAIT
|
||||
INFO 134
|
||||
|
|
@ -1,95 +0,0 @@
|
|||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGININFO
|
||||
-- SYMBOL|134|2
|
||||
(
|
||||
-- ACK
|
||||
-- SYMBOL|134|3
|
||||
λ
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|6
|
||||
b₂
|
||||
-- ACK
|
||||
-- TYPE|134|11
|
||||
A → Type
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|11
|
||||
B
|
||||
-- ACK
|
||||
-- TYPE|134|13
|
||||
A
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|13
|
||||
a₁
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|18
|
||||
H₂
|
||||
-- ACK
|
||||
-- TYPE|134|23
|
||||
B a₁
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|23
|
||||
b₁
|
||||
-- ACK
|
||||
-- TYPE|134|26
|
||||
B a₁ → B a₁ → Prop
|
||||
-- ACK
|
||||
-- SYMBOL|134|26
|
||||
=
|
||||
-- ACK
|
||||
-- TYPE|134|28
|
||||
B a₁
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|28
|
||||
b₂
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|33
|
||||
c₂
|
||||
-- ACK
|
||||
-- TYPE|134|38
|
||||
Π (a : A), B a → Type
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|38
|
||||
C
|
||||
-- ACK
|
||||
-- TYPE|134|40
|
||||
A
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|40
|
||||
a₁
|
||||
-- ACK
|
||||
-- TYPE|134|43
|
||||
B a₁
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|43
|
||||
b₂
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|48
|
||||
H₃
|
||||
-- ACK
|
||||
-- TYPE|134|53
|
||||
C a₁ b₂
|
||||
-- ACK
|
||||
-- SYNTH|134|53
|
||||
drec_on (congr_arg2_dep C (refl a₁) H₂) c₁
|
||||
-- ACK
|
||||
-- SYMBOL|134|53
|
||||
_
|
||||
-- ACK
|
||||
-- TYPE|134|55
|
||||
C a₁ b₂ → C a₁ b₂ → Prop
|
||||
-- ACK
|
||||
-- SYMBOL|134|55
|
||||
=
|
||||
-- ACK
|
||||
-- TYPE|134|57
|
||||
C a₁ b₂
|
||||
-- ACK
|
||||
-- IDENTIFIER|134|57
|
||||
c₂
|
||||
-- ACK
|
||||
-- ENDINFO
|
||||
|
|
@ -1,161 +0,0 @@
|
|||
-- 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, Floris van Doorn
|
||||
|
||||
-- logic.connectives.eq
|
||||
-- ====================
|
||||
|
||||
-- Equality.
|
||||
prelude
|
||||
definition Prop := Type.{0}
|
||||
-- eq
|
||||
-- --
|
||||
|
||||
inductive eq {A : Type} (a : A) : A → Prop :=
|
||||
refl : eq a a
|
||||
|
||||
infix `=`:50 := eq
|
||||
definition rfl {A : Type} {a : A} := eq.refl a
|
||||
|
||||
-- proof irrelevance is built in
|
||||
theorem proof_irrel {a : Prop} {H1 H2 : a} : H1 = H2 := rfl
|
||||
|
||||
namespace eq
|
||||
theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) :=
|
||||
proof_irrel
|
||||
|
||||
theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 :=
|
||||
proof_irrel
|
||||
|
||||
theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
|
||||
eq.rec H2 H1
|
||||
|
||||
theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
|
||||
subst H2 H1
|
||||
|
||||
theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
|
||||
subst H (refl a)
|
||||
end eq
|
||||
|
||||
attribute eq.subst [subst]
|
||||
attribute eq.refl [refl]
|
||||
attribute eq.trans [trans]
|
||||
|
||||
namespace eq_ops
|
||||
postfix `⁻¹`:1024 := eq.symm
|
||||
infixr `⬝`:75 := eq.trans
|
||||
infixr `▸`:75 := eq.subst
|
||||
end eq_ops
|
||||
open eq_ops
|
||||
|
||||
namespace eq
|
||||
-- eq_rec with arguments swapped, for transporting an element of a dependent type
|
||||
|
||||
-- definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
|
||||
-- eq.rec H2 H1
|
||||
|
||||
definition drec_on {A : Type} {a a' : A} {B : Πa' : A, a = a' → Type} (H1 : a = a') (H2 : B a (refl a)) : B a' H1 :=
|
||||
eq.rec (λH1 : a = a, show B a H1, from H2) H1 H1
|
||||
|
||||
theorem drec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : drec_on H b = b :=
|
||||
refl (drec_on rfl b)
|
||||
|
||||
theorem drec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : drec_on H b = b :=
|
||||
drec_on H (λ(H' : a = a), drec_on_id H' b) H
|
||||
|
||||
theorem drec_on_constant2 {A : Type} {a₁ a₂ a₃ a₄ : A} {B : Type} (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : drec_on H₁ b = drec_on H₂ b :=
|
||||
drec_on_constant H₁ b ⬝ drec_on_constant H₂ b ⁻¹
|
||||
|
||||
theorem drec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : drec_on H b = drec_on H' b :=
|
||||
drec_on H (λ(H : a = a) (H' : f a = f a), drec_on_id H b ⬝ drec_on_id H' b⁻¹) H H'
|
||||
|
||||
theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq.rec b H = b :=
|
||||
id_refl H⁻¹ ▸ refl (eq.rec b (refl a))
|
||||
|
||||
theorem drec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
|
||||
(u : P a) :
|
||||
drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u :=
|
||||
(show ∀(H2 : b = c), drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u,
|
||||
from drec_on H2 (fun (H2 : b = b), drec_on_id H2 _))
|
||||
H2
|
||||
end eq
|
||||
|
||||
open eq
|
||||
|
||||
theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
|
||||
H ▸ rfl
|
||||
|
||||
theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
|
||||
H ▸ rfl
|
||||
|
||||
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
|
||||
f a = g b :=
|
||||
H1 ▸ H2 ▸ rfl
|
||||
|
||||
theorem congr_arg2 {A B C : Type} {a a' : A} {b b' : B} (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
|
||||
congr (congr_arg f Ha) Hb
|
||||
|
||||
theorem congr_arg3 {A B C D : Type} {a a' : A} {b b' : B} {c c' : C} (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f a' b' c' :=
|
||||
congr (congr_arg2 f Ha Hb) Hc
|
||||
|
||||
theorem congr_arg4 {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f a' b' c' d' :=
|
||||
congr (congr_arg3 f Ha Hb Hc) Hd
|
||||
|
||||
theorem congr_arg5 {A B C D E F : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} (f : A → B → C → D → E → F) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f a' b' c' d' e' :=
|
||||
congr (congr_arg4 f Ha Hb Hc Hd) He
|
||||
|
||||
theorem congr2 {A B C : Type} {a a' : A} {b b' : B} (f f' : A → B → C) (Hf : f = f') (Ha : a = a') (Hb : b = b') : f a b = f' a' b' :=
|
||||
Hf ▸ congr_arg2 f Ha Hb
|
||||
|
||||
theorem congr3 {A B C D : Type} {a a' : A} {b b' : B} {c c' : C} (f f' : A → B → C → D) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f' a' b' c' :=
|
||||
Hf ▸ congr_arg3 f Ha Hb Hc
|
||||
|
||||
theorem congr4 {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} (f f' : A → B → C → D → E) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f' a' b' c' d' :=
|
||||
Hf ▸ congr_arg4 f Ha Hb Hc Hd
|
||||
|
||||
theorem congr5 {A B C D E F : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} (f f' : A → B → C → D → E → F) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f' a' b' c' d' e' :=
|
||||
Hf ▸ congr_arg5 f Ha Hb Hc Hd He
|
||||
|
||||
theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
|
||||
{b₁ : B a₁} {b₂ : B a₂} (f : Πa, B a → C) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) :
|
||||
f a₁ b₁ = f a₂ b₂ :=
|
||||
eq.drec_on H₁
|
||||
(λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.drec_on H₁ b₁ = b₂),
|
||||
calc
|
||||
f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : sorry -- {(eq.drec_on_id H₁ b₁)⁻¹}
|
||||
... = f a₁ b₂ : sorry)
|
||||
b₂ H₁ H₂
|
||||
|
||||
|
||||
theorem congr_arg3_dep {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
|
||||
(H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
|
||||
f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
|
||||
eq.drec_on H₁
|
||||
(λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : _ = c₂),
|
||||
have H₃' : eq.drec_on H₂ c₁ = c₂,
|
||||
from (drec_on_irrel H₂ (congr_arg2_dep C (refl a₁) H₂) c₁⁻¹) ▸ H₃,
|
||||
congr_arg2_dep (f a₁) H₂ H₃')
|
||||
b₂ H₂ c₂ H₃
|
||||
|
||||
theorem congr_arg3_ndep_dep {A B : Type} {C : A → B → Type} {D : Type} {a₁ a₂ : A} {b₁ b₂ : B} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
|
||||
(H₁ : a₁ = a₂) (H₂ : b₁ = b₂) (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
|
||||
f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
|
||||
congr_arg3_dep f H₁ (drec_on_constant H₁ b₁ ⬝ H₂) H₃
|
||||
|
||||
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
|
||||
fun x, congr_fun H x
|
||||
|
||||
theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
|
||||
H1 ▸ H2
|
||||
|
||||
theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
|
||||
H1⁻¹ ▸ H2
|
||||
|
||||
theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
|
||||
fun Ha, H2 (H1 Ha)
|
||||
|
||||
theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c :=
|
||||
fun Ha, H2 ▸ (H1 Ha)
|
||||
|
||||
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
|
||||
fun Ha, H2 (H1 ▸ Ha)
|
||||
|
|
@ -74,8 +74,6 @@ namespace semigroup
|
|||
definition carrier [coercion] (g : semigroup)
|
||||
:= semigroup.rec (fun c s, c) g
|
||||
|
||||
definition is_semigroup [instance] [g : semigroup] : semigroup_struct (carrier g)
|
||||
:= semigroup.rec (fun c s, s) g
|
||||
end semigroup
|
||||
|
||||
namespace monoid
|
||||
|
|
@ -101,7 +99,7 @@ namespace monoid
|
|||
:= monoid.rec (fun c s, c) m
|
||||
|
||||
definition is_monoid [instance] (m : monoid) : monoid_struct (carrier m)
|
||||
:= monoid.rec (fun c s, s) m
|
||||
:= sorry
|
||||
end monoid
|
||||
end algebra
|
||||
|
||||
|
|
|
|||
|
|
@ -1,58 +0,0 @@
|
|||
import logic
|
||||
|
||||
variables {A : Type} {a a' : A}
|
||||
|
||||
definition to_eq₁ (H : a == a') : a = a' :=
|
||||
begin
|
||||
assert H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
|
||||
intro Ht,
|
||||
exact (eq.refl (eq.rec_on Ht a)),
|
||||
show a = a', from
|
||||
heq.rec_on H H₁ (eq.refl A)
|
||||
end
|
||||
|
||||
definition to_eq₂ (H : a == a') : a = a' :=
|
||||
begin
|
||||
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
|
||||
begin
|
||||
intro Ht,
|
||||
exact (eq.refl (eq.rec_on Ht a))
|
||||
end,
|
||||
show a = a', from
|
||||
heq.rec_on H H₁ (eq.refl A)
|
||||
end
|
||||
|
||||
definition to_eq₃ (H : a == a') : a = a' :=
|
||||
begin
|
||||
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
|
||||
by intro Ht; exact (eq.refl (eq.rec_on Ht a)),
|
||||
show a = a', from
|
||||
heq.rec_on H H₁ (eq.refl A)
|
||||
end
|
||||
|
||||
definition to_eq₄ (H : a == a') : a = a' :=
|
||||
begin
|
||||
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
|
||||
from assume Ht, eq.refl (eq.rec_on Ht a),
|
||||
show a = a', from
|
||||
heq.rec_on H H₁ (eq.refl A)
|
||||
end
|
||||
|
||||
definition to_eq₅ (H : a == a') : a = a' :=
|
||||
begin
|
||||
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
|
||||
proof
|
||||
λ Ht, eq.refl (eq.rec_on Ht a)
|
||||
qed,
|
||||
show a = a', from
|
||||
heq.rec_on H H₁ (eq.refl A)
|
||||
end
|
||||
|
||||
definition to_eq₆ (H : a == a') : a = a' :=
|
||||
begin
|
||||
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
|
||||
assume Ht,
|
||||
eq.refl (eq.rec_on Ht a),
|
||||
show a = a', from
|
||||
heq.rec_on H H₁ (eq.refl A)
|
||||
end
|
||||
|
|
@ -1,18 +1,12 @@
|
|||
import logic
|
||||
|
||||
namespace setoid
|
||||
inductive setoid : Type :=
|
||||
mk_setoid: Π (A : Type), (A → A → Prop) → setoid
|
||||
structure setoid : Type :=
|
||||
(carrier : Type) (eqv : carrier → carrier → Prop)
|
||||
|
||||
definition carrier (s : setoid)
|
||||
:= setoid.rec (λ a eq, a) s
|
||||
infix `≈` := setoid.eqv _
|
||||
|
||||
definition eqv {s : setoid} : carrier s → carrier s → Prop
|
||||
:= setoid.rec (λ a eqv, eqv) s
|
||||
|
||||
infix `≈` := eqv
|
||||
|
||||
attribute carrier [coercion]
|
||||
attribute setoid.carrier [coercion]
|
||||
|
||||
inductive morphism (s1 s2 : setoid) : Type :=
|
||||
mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
|
||||
|
|
|
|||
|
|
@ -1,18 +1,12 @@
|
|||
import logic
|
||||
|
||||
namespace setoid
|
||||
inductive setoid : Type :=
|
||||
mk_setoid: Π (A : Type), (A → A → Prop) → setoid
|
||||
structure setoid : Type :=
|
||||
(carrier : Type) (eqv : carrier → carrier → Prop)
|
||||
|
||||
definition carrier (s : setoid)
|
||||
:= setoid.rec (λ a eq, a) s
|
||||
infix `≈` := setoid.eqv _
|
||||
|
||||
definition eqv {s : setoid} : carrier s → carrier s → Prop
|
||||
:= setoid.rec (λ a eqv, eqv) s
|
||||
|
||||
infix `≈` := eqv
|
||||
|
||||
attribute carrier [coercion]
|
||||
attribute setoid.carrier [coercion]
|
||||
|
||||
inductive morphism (s1 s2 : setoid) : Type :=
|
||||
mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
|
||||
|
|
|
|||
|
|
@ -1,23 +1,15 @@
|
|||
import logic
|
||||
|
||||
namespace setoid
|
||||
inductive setoid : Type :=
|
||||
mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
|
||||
structure setoid : Type :=
|
||||
(carrier : Type) (eqv : carrier → carrier → Prop)
|
||||
|
||||
set_option pp.universes true
|
||||
infix `≈` := setoid.eqv _
|
||||
|
||||
attribute setoid.carrier [coercion]
|
||||
|
||||
check setoid
|
||||
definition test : Type.{2} := setoid.{0}
|
||||
|
||||
definition carrier (s : setoid)
|
||||
:= setoid.rec (λ a eq, a) s
|
||||
|
||||
definition eqv {s : setoid} : carrier s → carrier s → Prop
|
||||
:= setoid.rec (λ a eqv, eqv) s
|
||||
|
||||
infix `≈` := eqv
|
||||
|
||||
attribute carrier [coercion]
|
||||
definition test : Type.{1} := setoid.{0}
|
||||
|
||||
inductive morphism (s1 s2 : setoid) : Type :=
|
||||
mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
|
||||
|
|
|
|||
|
|
@ -1,23 +1,12 @@
|
|||
import logic
|
||||
|
||||
namespace setoid
|
||||
inductive setoid : Type :=
|
||||
mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
|
||||
structure setoid : Type :=
|
||||
(carrier : Type) (eqv : carrier → carrier → Prop)
|
||||
|
||||
set_option pp.universes true
|
||||
infix `≈` := setoid.eqv _
|
||||
|
||||
check setoid
|
||||
definition test : Type.{2} := setoid.{0}
|
||||
|
||||
definition carrier (s : setoid)
|
||||
:= setoid.rec (λ a eq, a) s
|
||||
|
||||
definition eqv {s : setoid} : carrier s → carrier s → Prop
|
||||
:= setoid.rec (λ a eqv, eqv) s
|
||||
|
||||
infix `≈` := eqv
|
||||
|
||||
attribute carrier [coercion]
|
||||
attribute setoid.carrier [coercion]
|
||||
|
||||
inductive morphism (s1 s2 : setoid) : Type :=
|
||||
mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
|
||||
|
|
@ -32,9 +21,9 @@ namespace setoid
|
|||
check morphism2
|
||||
check morphism2.mk
|
||||
|
||||
inductive my_struct : Type :=
|
||||
mk_foo : Π (s1 s2 : setoid) (s3 s4 : setoid), morphism2 s1 s2 → morphism2 s3 s4 → my_struct
|
||||
structure my_struct : Type :=
|
||||
(s1 s2 : setoid) (s3 s4 : setoid) (f₁ : morphism2 s1 s2) (f₂ : morphism2 s3 s4)
|
||||
|
||||
check my_struct
|
||||
definition tst2 : Type.{4} := my_struct.{1 2 1 2}
|
||||
definition tst2 : Type.{3} := my_struct.{1 2 1 2}
|
||||
end setoid
|
||||
|
|
|
|||
|
|
@ -1,2 +1 @@
|
|||
check @dec_trivial
|
||||
print dec_trivial
|
||||
|
|
|
|||
|
|
@ -60,6 +60,7 @@ set_option find_decl.expensive true
|
|||
|
||||
find_decl bool.ff ≠ bool.tt
|
||||
|
||||
/-
|
||||
-- map using well-founded recursion. We could have used the default recursor.
|
||||
-- this is just a test for the definitional package
|
||||
definition map.F {A B : Type₁} (f : A → B) (tf₁ : tree_forest A) : (Π tf₂ : tree_forest A, tf₂ ≺ tf₁ → map.res B tf₂) → map.res B tf₁ :=
|
||||
|
|
@ -95,5 +96,6 @@ definition map {A B : Type₁} (f : A → B) (tf : tree_forest A) : map.res B tf
|
|||
well_founded.fix (@map.F A B f) tf
|
||||
|
||||
eval map succ (sum.inl (tree.node 2 (forest.cons (tree.node 1 (forest.nil nat)) (forest.nil nat))))
|
||||
-/
|
||||
|
||||
end manual
|
||||
|
|
|
|||
|
|
@ -45,8 +45,6 @@ section
|
|||
definition mul := semigroup.rec (λmul assoc, mul) s a b
|
||||
section
|
||||
infixl `*` := mul
|
||||
definition assoc : (a * b) * c = a * (b * c) :=
|
||||
semigroup.rec (λmul assoc, assoc) s a b c
|
||||
end
|
||||
end
|
||||
end semigroup
|
||||
|
|
@ -56,8 +54,6 @@ section
|
|||
include s
|
||||
definition semigroup_has_mul [instance] : has_mul A := has_mul.mk semigroup.mul
|
||||
|
||||
theorem mul_assoc (a b c : A) : a * b * c = a * (b * c) :=
|
||||
!semigroup.assoc
|
||||
end
|
||||
|
||||
-- comm_semigroup
|
||||
|
|
@ -75,25 +71,9 @@ section
|
|||
variables {A : Type} [s : comm_semigroup A]
|
||||
variables a b c : A
|
||||
definition mul (a b : A) : A := comm_semigroup.rec (λmul assoc comm, mul) s a b
|
||||
definition assoc : mul (mul a b) c = mul a (mul b c) :=
|
||||
comm_semigroup.rec (λmul assoc comm, assoc) s a b c
|
||||
definition comm : mul a b = mul b a :=
|
||||
comm_semigroup.rec (λmul assoc comm, comm) s a b
|
||||
end
|
||||
end comm_semigroup
|
||||
|
||||
section
|
||||
variables {A : Type} [s : comm_semigroup A]
|
||||
variables a b c : A
|
||||
include s
|
||||
definition comm_semigroup_semigroup [instance] : semigroup A :=
|
||||
semigroup.mk comm_semigroup.mul comm_semigroup.assoc
|
||||
|
||||
theorem mul_comm : a * b = b * a := !comm_semigroup.comm
|
||||
|
||||
theorem mul_left_comm : a * (b * c) = b * (a * c) :=
|
||||
binary.left_comm mul_comm mul_assoc a b c
|
||||
end
|
||||
|
||||
-- monoid
|
||||
-- ------
|
||||
|
|
@ -106,151 +86,4 @@ mk : Π (mul: A → A → A) (one : A)
|
|||
(∀a, 1 * a = a) →
|
||||
monoid A
|
||||
|
||||
namespace monoid
|
||||
section
|
||||
variables {A : Type} [s : monoid A]
|
||||
variables a b c : A
|
||||
include s
|
||||
section
|
||||
definition mul := monoid.rec (λmul one assoc right_id left_id, mul) s a b
|
||||
definition one := monoid.rec (λmul one assoc right_id left_id, one) s
|
||||
infixl `*` := mul
|
||||
notation 1 := one
|
||||
definition assoc : (a * b) * c = a * (b * c) :=
|
||||
monoid.rec (λmul one assoc right_id left_id, assoc) s a b c
|
||||
definition right_id : a * 1 = a :=
|
||||
monoid.rec (λmul one assoc right_id left_id, right_id) s a
|
||||
definition left_id : 1 * a = a :=
|
||||
monoid.rec (λmul one assoc right_id left_id, left_id) s a
|
||||
end
|
||||
end
|
||||
end monoid
|
||||
|
||||
section
|
||||
variables {A : Type} [s : monoid A]
|
||||
variable a : A
|
||||
include s
|
||||
definition monoid_has_one [instance] : has_one A := has_one.mk (monoid.one)
|
||||
definition monoid_semigroup [instance] : semigroup A :=
|
||||
semigroup.mk monoid.mul monoid.assoc
|
||||
|
||||
theorem mul_right_id : a * 1 = a := !monoid.right_id
|
||||
theorem mul_left_id : 1 * a = a := !monoid.left_id
|
||||
end
|
||||
|
||||
|
||||
-- comm_monoid
|
||||
-- -----------
|
||||
|
||||
inductive comm_monoid [class] (A : Type) : Type :=
|
||||
mk : Π (mul: A → A → A) (one : A)
|
||||
(infixl `*` := mul) (notation 1 := one),
|
||||
(∀a b c, (a * b) * c = a * (b * c)) →
|
||||
(∀a, a * 1 = a) →
|
||||
(∀a, 1 * a = a) →
|
||||
(∀a b, a * b = b * a) →
|
||||
comm_monoid A
|
||||
|
||||
namespace comm_monoid
|
||||
section
|
||||
variables {A : Type} [s : comm_monoid A]
|
||||
variables a b c : A
|
||||
definition mul := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b
|
||||
definition one := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s
|
||||
definition assoc : mul (mul a b) c = mul a (mul b c) :=
|
||||
comm_monoid.rec (λmul one assoc right_id left_id comm, assoc) s a b c
|
||||
definition right_id : mul a one = a :=
|
||||
comm_monoid.rec (λmul one assoc right_id left_id comm, right_id) s a
|
||||
definition left_id : mul one a = a :=
|
||||
comm_monoid.rec (λmul one assoc right_id left_id comm, left_id) s a
|
||||
definition comm : mul a b = mul b a :=
|
||||
comm_monoid.rec (λmul one assoc right_id left_id comm, comm) s a b
|
||||
end
|
||||
end comm_monoid
|
||||
|
||||
section
|
||||
variables {A : Type} [s : comm_monoid A]
|
||||
include s
|
||||
definition comm_monoid_monoid [instance] : monoid A :=
|
||||
monoid.mk comm_monoid.mul comm_monoid.one comm_monoid.assoc
|
||||
comm_monoid.right_id comm_monoid.left_id
|
||||
definition comm_monoid_comm_semigroup [instance] : comm_semigroup A :=
|
||||
comm_semigroup.mk comm_monoid.mul comm_monoid.assoc comm_monoid.comm
|
||||
end
|
||||
|
||||
-- bundled structures
|
||||
-- ------------------
|
||||
|
||||
inductive Semigroup [class] : Type := mk : Π carrier : Type, semigroup carrier → Semigroup
|
||||
section
|
||||
variable S : Semigroup
|
||||
definition Semigroup.carrier [coercion] : Type := Semigroup.rec (λc s, c) S
|
||||
definition Semigroup.struc [instance] : semigroup S := Semigroup.rec (λc s, s) S
|
||||
end
|
||||
|
||||
inductive CommSemigroup [class] : Type :=
|
||||
mk : Π carrier : Type, comm_semigroup carrier → CommSemigroup
|
||||
section
|
||||
variable S : CommSemigroup
|
||||
definition CommSemigroup.carrier [coercion] : Type := CommSemigroup.rec (λc s, c) S
|
||||
definition CommSemigroup.struc [instance] : comm_semigroup S := CommSemigroup.rec (λc s, s) S
|
||||
end
|
||||
|
||||
inductive Monoid [class] : Type := mk : Π carrier : Type, monoid carrier → Monoid
|
||||
section
|
||||
variable S : Monoid
|
||||
definition Monoid.carrier [coercion] : Type := Monoid.rec (λc s, c) S
|
||||
definition Monoid.struc [instance] : monoid S := Monoid.rec (λc s, s) S
|
||||
end
|
||||
|
||||
inductive CommMonoid : Type := mk : Π carrier : Type, comm_monoid carrier → CommMonoid
|
||||
section
|
||||
variable S : CommMonoid
|
||||
definition CommMonoid.carrier [coercion] : Type := CommMonoid.rec (λc s, c) S
|
||||
definition CommMonoid.struc [instance] : comm_monoid S := CommMonoid.rec (λc s, s) S
|
||||
end
|
||||
end algebra
|
||||
|
||||
open algebra
|
||||
|
||||
section examples
|
||||
|
||||
theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
|
||||
calc
|
||||
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
|
||||
... = a * b * (c * d) : !mul_assoc
|
||||
|
||||
theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
|
||||
|
||||
theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
|
||||
calc
|
||||
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
|
||||
... = a * b * (c * d) : !mul_assoc
|
||||
|
||||
-- for test4b to work, we need instances at the level of the bundled structures as well
|
||||
definition Monoid_Semigroup [instance] (M : Monoid) : Semigroup :=
|
||||
Semigroup.mk (Monoid.carrier M) _
|
||||
|
||||
theorem test4 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
|
||||
test1 a b c d
|
||||
|
||||
theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
|
||||
calc
|
||||
a * 1 * b * c = a * b * c : by rewrite mul_right_id
|
||||
... = a * (b * c) : !mul_assoc
|
||||
|
||||
theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
|
||||
calc
|
||||
a * 1 * b * c = a * b * c : by rewrite mul_right_id
|
||||
... = a * (b * c) : !mul_assoc
|
||||
|
||||
theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
|
||||
calc
|
||||
a * 1 * b * c = a * b * c : by rewrite mul_right_id
|
||||
... = a * (b * c) : !mul_assoc
|
||||
|
||||
theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
|
||||
calc
|
||||
a * 1 * b * c = a * b * c : by rewrite mul_right_id
|
||||
... = a * (b * c) : !mul_assoc
|
||||
end examples
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ have aux : is_eq a a = tt, from
|
|||
(λ (a₁ : nat) (ih : is_eq a₁ a₁ = tt), ih),
|
||||
H ▸ aux
|
||||
|
||||
/-
|
||||
theorem is_eq.to_eq (a b : nat) : is_eq a b = tt → a = b :=
|
||||
nat.induction_on a
|
||||
(λb, nat.cases_on b (λh, rfl) (λb₁ H, absurd H !ff_ne_tt))
|
||||
|
|
@ -31,3 +32,4 @@ nat.induction_on a
|
|||
have aux : a₁ = b₁, from ih b₁ H,
|
||||
aux ▸ rfl))
|
||||
b
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -28,63 +28,4 @@ namespace vector
|
|||
end
|
||||
end play
|
||||
|
||||
print "====================="
|
||||
definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
|
||||
vector.brec_on w (λ (n : nat) (w : vector A n),
|
||||
vector.cases_on w
|
||||
(λ (B : vector.below vnil), v)
|
||||
(λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : vector.below (vcons a₁ v₁)),
|
||||
vcons a₁ (pr₁ B)))
|
||||
|
||||
exit
|
||||
check vector.brec_on
|
||||
definition bw := @vector.below
|
||||
|
||||
definition sum {n : nat} (v : vector nat n) : nat :=
|
||||
vector.brec_on v (λ (n : nat) (v : vector nat n),
|
||||
vector.cases_on v
|
||||
(λ (B : bw vnil), zero)
|
||||
(λ (n₁ : nat) (a : nat) (v₁ : vector nat n₁) (B : bw (vcons a v₁)),
|
||||
a + pr₁ B))
|
||||
|
||||
example : sum (10 :: 20 :: vnil) = 30 :=
|
||||
rfl
|
||||
|
||||
definition addk {n : nat} (v : vector nat n) (k : nat) : vector nat n :=
|
||||
vector.brec_on v (λ (n : nat) (v : vector nat n),
|
||||
vector.cases_on v
|
||||
(λ (B : bw vnil), vnil)
|
||||
(λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)),
|
||||
vcons (a₁+k) (pr₁ B)))
|
||||
|
||||
example : addk (1 :: 2 :: vnil) 3 = 4 :: 5 :: vnil :=
|
||||
rfl
|
||||
|
||||
example : append (1 :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil :=
|
||||
rfl
|
||||
|
||||
definition head {A : Type} {n : nat} (v : vector A (succ n)) : A :=
|
||||
nat.cases_on v
|
||||
(λ H : succ n = 0, nat.no_confusion H)
|
||||
(λn' h t (H : succ n = succ n'), h)
|
||||
rfl
|
||||
|
||||
definition tail {A : Type} {n : nat} (v : vector A (succ n)) : vector A n :=
|
||||
@nat.cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v
|
||||
(λ H : succ n = 0, nat.no_confusion H)
|
||||
(λ (n' : nat) (h : A) (t : vector A n') (H : succ n = succ n'),
|
||||
t)
|
||||
rfl
|
||||
|
||||
definition add {n : nat} (w v : vector nat n) : vector nat n :=
|
||||
@nat.brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w
|
||||
(λ (n : nat) (w : vector nat n),
|
||||
vector.cases_on w
|
||||
(λ (B : bw vnil) (w : vector nat zero), vnil)
|
||||
(λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)) (v : vector nat (succ n₁)),
|
||||
vcons (a₁ + head v) (pr₁ B (tail v)))) v
|
||||
|
||||
example : add (1 :: 2 :: vnil) (3 :: 5 :: vnil) = 4 :: 7 :: vnil :=
|
||||
rfl
|
||||
|
||||
end vector
|
||||
|
|
|
|||
|
|
@ -68,16 +68,6 @@ namespace vector
|
|||
example : addk (1 :: 2 :: vnil) 3 = 4 :: 5 :: vnil :=
|
||||
rfl
|
||||
|
||||
definition append.{l} {A : Type.{l+1}} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
|
||||
vector.brec_on w (λ (n : nat) (w : vector A n),
|
||||
vector.cases_on w
|
||||
(λ (B : bw vnil), v)
|
||||
(λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : bw (vcons a₁ v₁)),
|
||||
vcons a₁ (pr₁ B)))
|
||||
|
||||
example : append ((1:nat) :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil :=
|
||||
rfl
|
||||
|
||||
definition head {A : Type} {n : nat} (v : vector A (succ n)) : A :=
|
||||
vector.cases_on v
|
||||
(λ H : succ n = 0, nat.no_confusion H)
|
||||
|
|
|
|||
|
|
@ -1,618 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
-- Ported from Coq HoTT
|
||||
-- definition id {A : Type} (a : A) := a
|
||||
definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
|
||||
infixr ∘ := compose
|
||||
|
||||
-- Path
|
||||
-- ----
|
||||
set_option unifier.max_steps 100000
|
||||
|
||||
inductive path {A : Type} (a : A) : A → Type :=
|
||||
idpath : path a a
|
||||
definition idpath := @path.idpath
|
||||
infix `≈` := path
|
||||
-- TODO: is this right?
|
||||
notation x `≈`:50 y `:>`:0 A:0 := @path A x y
|
||||
notation `idp`:max := idpath _ -- TODO: can we / should we use `1`?
|
||||
|
||||
namespace path
|
||||
-- Concatenation and inverse
|
||||
-- -------------------------
|
||||
|
||||
definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
|
||||
path.rec (λu, u) q p
|
||||
|
||||
definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
|
||||
path.rec (idpath x) p
|
||||
|
||||
infixl `⬝` := concat
|
||||
postfix `**`:100 := inverse
|
||||
|
||||
-- In Coq, these are not needed, because concat and inv are kept transparent
|
||||
definition inv_1 {A : Type} (x : A) : (idpath x)** ≈ idpath x := idp
|
||||
|
||||
definition concat_11 {A : Type} (x : A) : idpath x ⬝ idpath x ≈ idpath x := idp
|
||||
|
||||
|
||||
-- The 1-dimensional groupoid structure
|
||||
-- ------------------------------------
|
||||
|
||||
-- The identity path is a right unit.
|
||||
definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p ⬝ idp ≈ p :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- The identity path is a right unit.
|
||||
definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp ⬝ p ≈ p :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- Concatenation is associative.
|
||||
definition concat_p_pp {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
|
||||
p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r :=
|
||||
path.rec_on r (path.rec_on q idp)
|
||||
|
||||
definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
|
||||
(p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) :=
|
||||
path.rec_on r (path.rec_on q idp)
|
||||
|
||||
-- The left inverse law.
|
||||
definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p** ≈ idp :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- The right inverse law.
|
||||
definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p** ⬝ p ≈ idp :=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
-- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
|
||||
-- redundant, following from earlier theorems.
|
||||
|
||||
definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p** ⬝ (p ⬝ q) ≈ q :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p** ⬝ q) ≈ q :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q** ≈ p :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q**) ⬝ q ≈ p :=
|
||||
path.rec_on q (take p, path.rec_on p idp) p
|
||||
|
||||
-- Inverse distributes over concatenation
|
||||
definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)** ≈ q** ⬝ p** :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p** ⬝ q)** ≈ q** ⬝ p :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
-- universe metavariables
|
||||
definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q**)** ≈ q ⬝ p** :=
|
||||
path.rec_on p (λq, path.rec_on q idp) q
|
||||
|
||||
definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p** ⬝ q**)** ≈ q ⬝ p :=
|
||||
path.rec_on p (path.rec_on q idp)
|
||||
|
||||
-- Inverse is an involution.
|
||||
definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p**** ≈ p :=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
-- Theorems for moving things around in equations
|
||||
-- ----------------------------------------------
|
||||
|
||||
definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q :=
|
||||
have gen : Πp q, p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q, from
|
||||
path.rec_on r
|
||||
(take p q,
|
||||
assume h : p ≈ idp** ⬝ q,
|
||||
show idp ⬝ p ≈ q, from concat_1p _ ⬝ h ⬝ concat_1p _),
|
||||
gen p q
|
||||
|
||||
definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q ⬝ p** → r ⬝ p ≈ q :=
|
||||
path.rec_on p (take q r h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q r
|
||||
|
||||
definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
p ≈ r ⬝ q → r** ⬝ p ≈ q :=
|
||||
path.rec_on r (take p q h, concat_1p _ ⬝ h ⬝ concat_1p _) p q
|
||||
|
||||
definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q ⬝ p → r ⬝ p** ≈ q :=
|
||||
path.rec_on p (take q r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) q r
|
||||
|
||||
definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r** ⬝ q ≈ p → q ≈ r ⬝ p :=
|
||||
path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
|
||||
|
||||
definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
q ⬝ p** ≈ r → q ≈ r ⬝ p :=
|
||||
path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
|
||||
|
||||
definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
r ⬝ q ≈ p → q ≈ r** ⬝ p :=
|
||||
path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
|
||||
|
||||
definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
q ⬝ p ≈ r → q ≈ r ⬝ p** :=
|
||||
path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
|
||||
|
||||
definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
p ⬝ q** ≈ idp → p ≈ q :=
|
||||
path.rec_on q (take p h, (concat_p1 _)** ⬝ h) p
|
||||
|
||||
definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
q** ⬝ p ≈ idp → p ≈ q :=
|
||||
path.rec_on q (take p h, (concat_1p _)** ⬝ h) p
|
||||
|
||||
definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
p ⬝ q ≈ idp → p ≈ q** :=
|
||||
path.rec_on q (take p h, (concat_p1 _)** ⬝ h) p
|
||||
|
||||
definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
q ⬝ p ≈ idp → p ≈ q** :=
|
||||
path.rec_on q (take p h, (concat_1p _)** ⬝ h) p
|
||||
|
||||
definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
idp ≈ p** ⬝ q → p ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
idp ≈ q ⬝ p** → p ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ q ⬝ p → p** ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ p ⬝ q → p** ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
|
||||
-- Transport
|
||||
-- ---------
|
||||
|
||||
-- keep transparent, so transport _ idp p is definitionally equal to p
|
||||
definition transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y :=
|
||||
path.rec_on p u
|
||||
|
||||
definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : transport _ idp u ≈ u :=
|
||||
idp
|
||||
|
||||
-- TODO: is the binding strength on x reasonable? (It is modeled on the notation for subst
|
||||
-- in the standard library.)
|
||||
-- This idiom makes the operation right associative.
|
||||
notation p `#`:65 x:64 := transport _ p x
|
||||
|
||||
definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- TODO: is this better than an alias? Note use of curly brackets
|
||||
definition ap01 := ap
|
||||
|
||||
definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
|
||||
Πx : A, f x ≈ g x
|
||||
|
||||
infix `~` := pointwise_paths
|
||||
|
||||
definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ~ g :=
|
||||
λx, path.rec_on H idp
|
||||
|
||||
definition ap10 {A B} {f g : A → B} (H : f ≈ g) : f ~ g := apD10 H
|
||||
|
||||
definition ap11 {A B} {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y :=
|
||||
path.rec_on H (path.rec_on p idp)
|
||||
|
||||
-- TODO: Note that the next line breaks the proof!
|
||||
-- opaque_hint (hiding path.rec_on)
|
||||
-- set_option pp.implicit true
|
||||
definition apD {A:Type} {B : A → Type} (f : Πa:A, B a) {x y : A} (p : x ≈ y) : p # (f x) ≈ f y :=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
-- More theorems for moving things around in equations
|
||||
-- ---------------------------------------------------
|
||||
|
||||
definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
|
||||
u ≈ p** # v → p # u ≈ v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
definition moveR_transport_V {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
|
||||
u ≈ p # v → p** # u ≈ v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
definition moveL_transport_V {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
|
||||
p # u ≈ v → u ≈ p** # v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
definition moveL_transport_p {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
|
||||
p** # u ≈ v → u ≈ p # v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
|
||||
-- Functoriality of functions
|
||||
-- --------------------------
|
||||
|
||||
-- Here we prove that functions behave like functors between groupoids, and that [ap] itself is
|
||||
-- functorial.
|
||||
|
||||
-- Functions take identity paths to identity paths
|
||||
definition ap_1 {A B : Type} (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp
|
||||
|
||||
definition apD_1 {A B} (x : A) (f : forall x : A, B x) : apD f idp ≈ idp :> (f x ≈ f x) := idp
|
||||
|
||||
-- Functions commute with concatenation.
|
||||
definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition ap_p_pp {A B : Type} (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) :
|
||||
r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) :=
|
||||
path.rec_on p (take r q, path.rec_on q (concat_p_pp r idp idp)) r q
|
||||
|
||||
definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) :
|
||||
(ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) :=
|
||||
path.rec_on p (take q, path.rec_on q (take r, concat_pp_p _ _ _)) q r
|
||||
|
||||
-- Functions commute with path inverses.
|
||||
definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)** ≈ ap f (p**) :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p**) ≈ (ap f p)** :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- TODO: rename id to idmap?
|
||||
definition ap_idmap {A : Type} {x y : A} (p : x ≈ y) : ap id p ≈ p :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition ap_compose {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
|
||||
ap (g ∘ f) p ≈ ap g (ap f p) :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- Sometimes we don't have the actual function [compose].
|
||||
definition ap_compose' {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
|
||||
ap (λa, g (f a)) p ≈ ap g (ap f p) :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- The action of constant maps.
|
||||
definition ap_const {A B : Type} {x y : A} (p : x ≈ y) (z : B) :
|
||||
ap (λu, z) p ≈ idp :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- Naturality of [ap].
|
||||
definition concat_Ap {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) :=
|
||||
path.rec_on q (concat_1p _ ⬝ (concat_p1 _)**)
|
||||
|
||||
-- Naturality of [ap] at identity.
|
||||
definition concat_A1p {A : Type} {f : A → A} (p : forall x, f x ≈ x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ q :=
|
||||
path.rec_on q (concat_1p _ ⬝ (concat_p1 _)**)
|
||||
|
||||
definition concat_pA1 {A : Type} {f : A → A} (p : forall x, x ≈ f x) {x y : A} (q : x ≈ y) :
|
||||
(p x) ⬝ (ap f q) ≈ q ⬝ (p y) :=
|
||||
path.rec_on q (concat_p1 _ ⬝ (concat_1p _)**)
|
||||
|
||||
--TODO: note that the Coq proof for the preceding is
|
||||
--
|
||||
-- match q as i in (_ ≈ y) return (p x ⬝ ap f i ≈ i ⬝ p y) with
|
||||
-- | idpath => concat_p1 _ ⬝ (concat_1p _)**
|
||||
-- end.
|
||||
--
|
||||
-- It is nice that we don't have to give the predicate.
|
||||
|
||||
-- Naturality with other paths hanging around.
|
||||
definition concat_pA_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x)
|
||||
{x y : A} (q : x ≈ y)
|
||||
{w z : B} (r : w ≈ f x) (s : g y ≈ z) :
|
||||
(r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) :=
|
||||
path.rec_on q (take s, path.rec_on s (take r, idp)) s r
|
||||
|
||||
-- Action of [apD10] and [ap10] on paths
|
||||
-- -------------------------------------
|
||||
|
||||
-- Application of paths between functions preserves the groupoid structure
|
||||
|
||||
definition apD10_1 {A} {B : A → Type} (f : Πx, B x) (x : A) : apD10 (idpath f) x ≈ idp := idp
|
||||
|
||||
definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
|
||||
apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x :=
|
||||
path.rec_on h (take h', path.rec_on h' idp) h'
|
||||
|
||||
definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) :
|
||||
apD10 (h**) x ≈ (apD10 h x)** :=
|
||||
path.rec_on h idp
|
||||
|
||||
definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
|
||||
|
||||
definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
|
||||
ap10 (h ⬝ h') x ≈ ap10 h x ⬝ ap10 h' x := apD10_pp h h' x
|
||||
|
||||
definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h**) x ≈ (ap10 h x)** := apD10_V h x
|
||||
|
||||
-- [ap10] also behaves nicely on paths produced by [ap]
|
||||
definition ap_ap10 {A B C} (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) :
|
||||
ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
-- Transport and the groupoid structure of paths
|
||||
-- ---------------------------------------------
|
||||
|
||||
-- TODO: move from above?
|
||||
-- definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x)
|
||||
-- : idp # u ≈ u := idp
|
||||
|
||||
definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) :
|
||||
p ⬝ q # u ≈ q # p # u :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
|
||||
p # p** # z ≈ z :=
|
||||
(transport_pp P (p**) p z)** ⬝ ap (λr, transport P r z) (concat_Vp p)
|
||||
|
||||
definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
|
||||
p** # p # z ≈ z :=
|
||||
(transport_pp P p (p**) z)** ⬝ ap (λr, transport P r z) (concat_pV p)
|
||||
|
||||
|
||||
-----------------------------------------------
|
||||
-- *** Examples of difficult induction problems
|
||||
-----------------------------------------------
|
||||
|
||||
theorem double_induction
|
||||
{A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z)
|
||||
{C : Π(x y z : A), Π(p : x ≈ y), Π(q : y ≈ z), Type}
|
||||
(H : C x x x (idpath x) (idpath x)) :
|
||||
C x y z p q :=
|
||||
path.rec_on p (take z q, path.rec_on q H) z q
|
||||
|
||||
theorem double_induction2
|
||||
{A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y)
|
||||
{C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type}
|
||||
(H : C z z z (idpath z) (idpath z)) :
|
||||
C x y z p q :=
|
||||
path.rec_on p (take y q, path.rec_on q H) y q
|
||||
|
||||
theorem double_induction2'
|
||||
{A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y)
|
||||
{C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type}
|
||||
(H : C z z z (idpath z) (idpath z)) : C x y z p q :=
|
||||
path.rec_on p (take y q, path.rec_on q H) y q
|
||||
|
||||
theorem triple_induction
|
||||
{A : Type} {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w)
|
||||
{C : Π(x y z w : A), Π(p : x ≈ y), Π(q : y ≈ z), Π(r: z ≈ w), Type}
|
||||
(H : C x x x x (idpath x) (idpath x) (idpath x)) :
|
||||
C x y z w p q r :=
|
||||
path.rec_on p (take z q, path.rec_on q (take w r, path.rec_on r H)) z q w r
|
||||
|
||||
reveal path.double_induction2
|
||||
-- try this again
|
||||
definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q**) ⬝ q ≈ p :=
|
||||
double_induction2 p q idp
|
||||
|
||||
reveal path.triple_induction
|
||||
definition transport_p_pp {A : Type} (P : A → Type)
|
||||
{x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) :
|
||||
ap (λe, e # u) (concat_p_pp p q r) ⬝ (transport_pp P (p ⬝ q) r u) ⬝
|
||||
ap (transport P r) (transport_pp P p q u)
|
||||
≈ (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p # u))
|
||||
:> ((p ⬝ (q ⬝ r)) # u ≈ r # q # p # u) :=
|
||||
triple_induction p q r (take u, idp) u
|
||||
|
||||
-- Here is another coherence lemma for transport.
|
||||
definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
|
||||
transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z)
|
||||
:= path.rec_on p idp
|
||||
|
||||
-- Dependent transport in a doubly dependent type.
|
||||
definition transportD {A : Type} (B : A → Type) (C : Π a : A, B a → Type)
|
||||
{x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1 y) :
|
||||
C x2 (p # y) :=
|
||||
path.rec_on p z
|
||||
|
||||
-- Transporting along higher-dimensional paths
|
||||
definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) :
|
||||
p # z ≈ q # z := ap (λp', p' # z) r
|
||||
|
||||
-- An alternative definition.
|
||||
definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q)
|
||||
(z : Q x) :
|
||||
transport2 Q r z ≈ ap10 (ap (transport Q) r) z :=
|
||||
path.rec_on r idp
|
||||
|
||||
definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y}
|
||||
(r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) :
|
||||
transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z :=
|
||||
path.rec_on r1 (path.rec_on r2 idp)
|
||||
|
||||
-- TODO: another interesting case
|
||||
definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) :
|
||||
transport2 Q (r**) z ≈ ((transport2 Q r z)**) :=
|
||||
-- path.rec_on r idp -- doesn't work
|
||||
path.rec_on r (idpath (inverse (transport2 Q (idpath p) z)))
|
||||
|
||||
definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q)
|
||||
(s : z ≈ w) :
|
||||
ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s :=
|
||||
path.rec_on r (concat_p1 _ ⬝ (concat_1p _)**)
|
||||
|
||||
-- TODO (from Coq library): What should this be called?
|
||||
definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) :
|
||||
f y (p # z) ≈ (p # (f x z)) :=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
-- Transporting in particular fibrations
|
||||
-- -------------------------------------
|
||||
|
||||
/-
|
||||
From the Coq HoTT library:
|
||||
|
||||
One frequently needs lemmas showing that transport in a certain dependent type is equal to some
|
||||
more explicitly defined operation, defined according to the structure of that dependent type.
|
||||
For most dependent types, we prove these lemmas in the appropriate file in the types/
|
||||
subdirectory. Here we consider only the most basic cases.
|
||||
-/
|
||||
|
||||
-- Transporting in a constant fibration.
|
||||
definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :
|
||||
transport (λx, B) p y ≈ y :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) :
|
||||
transport_const p y ≈ transport2 (λu, B) r y ⬝ transport_const q y :=
|
||||
path.rec_on r (concat_1p _)**
|
||||
|
||||
-- Transporting in a pulled back fibration.
|
||||
definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) :
|
||||
transport (λx, P (f x)) p z ≈ transport P (ap f p) z :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') :
|
||||
transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition apD10_ap_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) :
|
||||
apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition apD10_ap_postcompose {A B C} (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) :
|
||||
apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- TODO: another example where a term has to be given explicitly
|
||||
-- A special case of [transport_compose] which seems to come up a lot.
|
||||
definition transport_idmap_ap A (P : A → Type) x y (p : x ≈ y) (u : P x) :
|
||||
transport P p u ≈ transport (λz, z) (ap P p) u :=
|
||||
path.rec_on p (idpath (transport (λ (z : Type), z) (ap P (idpath x)) u))
|
||||
|
||||
|
||||
-- The behavior of [ap] and [apD]
|
||||
-- ------------------------------
|
||||
|
||||
-- In a constant fibration, [apD] reduces to [ap], modulo [transport_const].
|
||||
definition apD_const {A B} {x y : A} (f : A → B) (p: x ≈ y) :
|
||||
apD f p ≈ transport_const p (f x) ⬝ ap f p :=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
-- The 2-dimensional groupoid structure
|
||||
-- ------------------------------------
|
||||
|
||||
-- Horizontal composition of 2-dimensional paths.
|
||||
definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') :
|
||||
p ⬝ q ≈ p' ⬝ q' :=
|
||||
path.rec_on h (path.rec_on h' idp)
|
||||
|
||||
infixl `⬝⬝`:75 := concat2
|
||||
|
||||
-- 2-dimensional path inversion
|
||||
definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p** ≈ q** :=
|
||||
path.rec_on h idp
|
||||
|
||||
-- Whiskering
|
||||
-- ----------
|
||||
|
||||
definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r :=
|
||||
idp ⬝⬝ h
|
||||
|
||||
definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r :=
|
||||
h ⬝⬝ idp
|
||||
|
||||
|
||||
-- Unwhiskering, a.k.a. cancelling
|
||||
-- -------------------------------
|
||||
|
||||
definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) :=
|
||||
path.rec_on p (take r, path.rec_on r (take q a, (concat_1p q)** ⬝ a)) r q
|
||||
|
||||
definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) :=
|
||||
path.rec_on r (take p, path.rec_on p (take q a, a ⬝ concat_p1 q)) p q
|
||||
|
||||
-- Whiskering and identity paths.
|
||||
|
||||
definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_p1 p)** ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
|
||||
path.rec_on h (path.rec_on p idp)
|
||||
|
||||
definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
|
||||
path.rec_on q idp
|
||||
|
||||
definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
|
||||
path.rec_on q idp
|
||||
|
||||
definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_1p p) ** ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
|
||||
path.rec_on h (path.rec_on p idp)
|
||||
|
||||
definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
h ⬝⬝ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) :=
|
||||
path.rec_on h idp
|
||||
|
||||
definition concat2_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
idp ⬝⬝ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) :=
|
||||
path.rec_on h idp
|
||||
|
||||
-- TODO: note, 4 inductions
|
||||
-- The interchange law for concatenation.
|
||||
definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x ≈ y} {q q' q'' : y ≈ z}
|
||||
(a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') :
|
||||
(a ⬝⬝ c) ⬝ (b ⬝⬝ d) ≈ (a ⬝ b) ⬝⬝ (c ⬝ d) :=
|
||||
path.rec_on d (path.rec_on c (path.rec_on b (path.rec_on a idp)))
|
||||
|
||||
definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
|
||||
(whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
|
||||
path.rec_on b (path.rec_on a (concat_1p _)**)
|
||||
|
||||
-- Structure corresponding to the coherence equations of a bicategory.
|
||||
|
||||
-- The "pentagonator": the 3-cell witnessing the associativity pentagon.
|
||||
definition pentagon {A : Type₁} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
|
||||
whiskerL p (concat_p_pp q r s)
|
||||
⬝ concat_p_pp p (q ⬝ r) s
|
||||
⬝ whiskerR (concat_p_pp p q r) s
|
||||
≈ concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s :=
|
||||
path.rec_on p (take q, path.rec_on q (take r, path.rec_on r (take s, path.rec_on s idp))) q r s
|
||||
|
||||
-- The 3-cell witnessing the left unit triangle.
|
||||
definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) :=
|
||||
path.rec_on p (take q, path.rec_on q idp) q
|
||||
|
||||
definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p :=
|
||||
(whiskerR_p1 p ⬝⬝ whiskerL_1p q)**
|
||||
⬝ (concat_p1 _ ⬝⬝ concat_p1 _)
|
||||
⬝ (concat_1p _ ⬝⬝ concat_1p _)
|
||||
⬝ (concat_whisker _ _ _ _ p q)
|
||||
⬝ (concat_1p _ ⬝⬝ concat_1p _)**
|
||||
⬝ (concat_p1 _ ⬝⬝ concat_p1 _)**
|
||||
⬝ (whiskerL_1p q ⬝⬝ whiskerR_p1 p)
|
||||
|
||||
|
||||
-- The action of functions on 2-dimensional paths
|
||||
definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q :=
|
||||
path.rec_on r idp
|
||||
|
||||
definition ap02_pp {A B} (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') :
|
||||
ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' :=
|
||||
path.rec_on r (path.rec_on r' idp)
|
||||
|
||||
definition ap02_p2p {A B} (f : A→B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p')
|
||||
(s : q ≈ q') :
|
||||
ap02 f (r ⬝⬝ s) ≈ ap_pp f p q
|
||||
⬝ (ap02 f r ⬝⬝ ap02 f s)
|
||||
⬝ (ap_pp f p' q')** :=
|
||||
path.rec_on r (path.rec_on s (path.rec_on q (path.rec_on p idp)))
|
||||
|
||||
definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) :
|
||||
apD f p ≈ transport2 B r (f x) ⬝ apD f q :=
|
||||
path.rec_on r (concat_1p _)**
|
||||
end path
|
||||
Loading…
Add table
Reference in a new issue