diff --git a/library/init/core.lean b/library/init/core.lean index ac50b87763..87055a9e2e 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -77,7 +77,7 @@ reserve infixl ` ++ `:65 reserve infixr ` :: `:67 reserve infixl `; `:1 -universes u v +universes u v w /-- Gadget for optional parameter support. -/ @[reducible] def opt_param (α : Sort u) (default : α) : Sort u := @@ -143,6 +143,60 @@ and.rec (λ ha hb, hb) h def and.right := @and.elim_right +/- eq basic support -/ + +infix = := eq + +attribute [refl] eq.refl + +@[pattern] def rfl {α : Sort u} {a : α} : a = a := eq.refl a + +@[elab_as_eliminator, subst] +lemma eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b := +eq.rec h₂ h₁ + +notation h1 ▸ h2 := eq.subst h1 h2 + +@[trans] lemma eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c := +h₂ ▸ h₁ + +@[symm] lemma eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a := +h ▸ rfl + +infix == := heq + +lemma eq_of_heq {α : Sort u} {a a' : α} (h : a == a') : a = a' := +have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from + λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl), +show (eq.rec_on (eq.refl α) a : α) = a', from + this α a' h (eq.refl α) + +-- The following four lemmas could not be automatically generated when the +-- structures were declared, so we prove them manually here. +lemma prod.mk.inj {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} + : (x₁, y₁) = (x₂, y₂) → and (x₁ = x₂) (y₁ = y₂) := +assume (H_eq : (x₁, y₁) = (x₂, y₂)), +have H_nc : (x₁ = x₂ → y₁ = y₂ → and (x₁ = x₂) (y₁ = y₂)) → and (x₁ = x₂) (y₁ = y₂), from + @prod.no_confusion _ _ (and (x₁ = x₂) (y₁ = y₂)) _ _ H_eq, +H_nc (assume Hx Hy, and.intro Hx Hy) + +lemma prod.mk.inj_arrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} + : (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P := +assume H_eq P, +@prod.no_confusion _ _ P _ _ H_eq + +lemma pprod.mk.inj {α : Sort u} {β : Sort v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} + : pprod.mk x₁ y₁ = pprod.mk x₂ y₂ → and (x₁ = x₂) (y₁ = y₂) := +assume (H_eq : pprod.mk x₁ y₁ = pprod.mk x₂ y₂), +have H_nc : (x₁ = x₂ → y₁ = y₂ → and (x₁ = x₂) (y₁ = y₂)) → and (x₁ = x₂) (y₁ = y₂), from + @pprod.no_confusion _ _ (and (x₁ = x₂) (y₁ = y₂)) _ _ H_eq, +H_nc (assume Hx Hy, and.intro Hx Hy) + +lemma pprod.mk.inj_arrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} + : (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P := +assume H_eq P, +@prod.no_confusion _ _ P _ _ H_eq + inductive sum (α : Type u) (β : Type v) | inl {} : α → sum | inr {} : β → sum @@ -426,8 +480,6 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ ( reserve postfix `⁻¹`:std.prec.max_plus -- input with \sy or \-1 or \inv -infix = := eq -infix == := heq infix ∈ := mem notation a ∉ s := ¬ mem a s infix + := add @@ -458,24 +510,6 @@ infix \ := sdiff notation α × β := prod α β -- notation for n-ary tuples -/- eq basic support -/ - -attribute [refl] eq.refl - -@[pattern] def rfl {α : Sort u} {a : α} : a = a := eq.refl a - -@[elab_as_eliminator, subst] -lemma eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b := -eq.rec h₂ h₁ - -notation h1 ▸ h2 := eq.subst h1 h2 - -@[trans] lemma eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c := -h₂ ▸ h₁ - -@[symm] lemma eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a := -h ▸ rfl - /- sizeof -/ class has_sizeof (α : Sort u) := diff --git a/library/init/logic.lean b/library/init/logic.lean index ee1ced2520..a924f62ce9 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -137,12 +137,6 @@ attribute [refl] heq.refl section variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ} -lemma eq_of_heq (h : a == a') : a = a' := -have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from - λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl), -show (eq.rec_on (eq.refl α) a : α) = a', from - this α a' h (eq.refl α) - lemma heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a == b) : p a → p b := eq.rec_on (eq_of_heq h₁) diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index d31e74d7d4..61f5b03fb5 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -14,4 +14,4 @@ import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance import init.meta.simp_tactic init.meta.set_get_option_tactics import init.meta.interactive init.meta.converter init.meta.vm import init.meta.comp_value_tactics init.meta.smt -import init.meta.async_tactic +import init.meta.async_tactic init.meta.inductive_compiler diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index a371e57e48..1ea2a3ab15 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -229,6 +229,14 @@ meta def is_not : expr → option expr | ```(%%a → false) := some a | e := none +meta def is_and : expr → option (expr × expr) +| ```(and %%α %%β) := some (α, β) +| _ := none + +meta def is_or : expr → option (expr × expr) +| ```(or %%α %%β) := some (α, β) +| _ := none + meta def is_eq : expr → option (expr × expr) | ```((%%a : %%_) = %%b) := some (a, b) | _ := none diff --git a/library/init/meta/inductive_compiler.lean b/library/init/meta/inductive_compiler.lean new file mode 100644 index 0000000000..9cdab4a07b --- /dev/null +++ b/library/init/meta/inductive_compiler.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2017 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +-/ +prelude +import init.meta.tactic init.meta.simp_tactic init.meta.rewrite_tactic init.function + +namespace inductive_compiler +namespace tactic + +open tactic list + +private meta def fsimplify (S : simp_lemmas) (e : expr) (cfg : simp_config := {}) : tactic (expr × expr) := +do e_type ← infer_type e >>= whnf, + simplify_core cfg S `iff e + +private meta def fsimp_at (S : simp_lemmas := simp_lemmas.mk) (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic unit := +do when (expr.is_local_constant h = ff) (fail "tactic fsimp_at failed, the given expression is not a hypothesis"), + htype ← infer_type h, + S ← S^.append extra_lemmas, + (new_htype, heq) ← fsimplify S htype cfg, + assert (expr.local_pp_name h) new_htype, + mk_app `iff.mp [heq, h] >>= exact, + try $ clear h + +private meta def fsimp (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic unit := +do S ← return (simp_lemmas.mk), + S ← S^.append extra_lemmas, + simplify_goal S cfg >> try triv >> try (reflexivity reducible) + +private meta def at_end (e : expr) : ℕ → tactic (list (option expr)) +| 0 := fail "at_end expected arity > 0" +| 1 := return [some e] +| (n+1) := at_end n >>= (λ xs, return (none :: xs)) + +private meta def intros_simp_and_subst (inj_simps : simp_lemmas) : expr → tactic unit +| (expr.pi n bi b d) := do + H ← intro n, + Ht ← infer_type H, + try $ do { + (A, lhs, B, rhs) ← match_heq Ht, + unify A B, + heq ← mk_app `eq [lhs, rhs], + pr ← mk_app `eq_of_heq [H], + assertv n heq pr, + clear H }, + H ← get_local n, + try $ fsimp_at inj_simps H, + H ← get_local n, + -- TODO(dhs): this may be a performance problem in the future + -- We need it now because the simp rules (pack x1 y1 = pack x2 y2 <-> y1 == y2) have eq on the LHS. + -- To avoid subst here, we may need to subst in the proof of the pack injectivity lemmas. + subst H, + tgt ← target, + intros_simp_and_subst tgt + +| e := do skip + +private meta def prove_conjuncts_by_reflexivity : expr → tactic unit +| ```(and %%α %%β) := do + split, + reflexivity, + prove_conjuncts_by_reflexivity β +| _ := reflexivity + +meta def prove_nested_inj (inj_simps : simp_lemmas) (inner_ir_inj_arrow : name) : tactic unit := do + xs ← intros, + triv <|> solve1 (do + H_orig_eq ← return (ilast xs), + c ← mk_const inner_ir_inj_arrow, + inner_inj ← to_expr `(%%c %%H_orig_eq), + apply inner_inj, + target >>= intros_simp_and_subst inj_simps, + target >>= prove_conjuncts_by_reflexivity) + +meta def prove_pack_inj (unpack unpack_pack : name) : tactic unit := do + intros, split, + -- prove easy direction first + swap, + solve1 (do H ← intro1, fsimp [H]), + -- hard direction + H ← intro1, + Ht ← infer_type H, + (lhs, rhs) ← match_eq Ht, + arity ← return (expr.get_app_num_args lhs), + args1 ← at_end lhs arity, + args2 ← at_end rhs arity, + lhs' ← mk_mapp unpack args1, + rhs' ← mk_mapp unpack args2, + H_ty ← mk_app `eq [lhs', rhs'], + assert `H_up H_ty, + solve1 (fsimp [H]), + H_up ← get_local `H_up, + solve1 (do e_unpack_pack ← mk_const unpack_pack, + rewrite_at_core semireducible tt tt occurrences.all ff e_unpack_pack H_up, + H_up ← get_local `H_up, + rewrite_at_core semireducible tt tt occurrences.all ff e_unpack_pack H_up, + H_up ← get_local `H_up, + exact H_up) + +end tactic +end inductive_compiler diff --git a/library/init/meta/injection_tactic.lean b/library/init/meta/injection_tactic.lean index 2ba647ea9e..33e7be4f1a 100644 --- a/library/init/meta/injection_tactic.lean +++ b/library/init/meta/injection_tactic.lean @@ -9,6 +9,11 @@ import init.meta.tactic init.function namespace tactic open nat tactic environment expr list +private meta def at_end₂ (e₁ e₂ : expr) : ℕ → tactic (list (option expr)) +| 2 := return [some e₁, some e₂] +| (n+3) := at_end₂ (n+2) >>= (λ xs, return (none :: xs)) +| _ := fail "at_end expected arity > 1" + private meta def mk_intro_name : name → list name → name | n₁ (n₂ :: ns) := n₂ | n [] := if n = `a then `h else n @@ -19,23 +24,8 @@ private meta def injection_intro : expr → list name → tactic unit | (pi n bi b d) ns := do hname ← return $ mk_intro_name n ns, h ← intro hname, - ht ← infer_type h, - -- Clear new hypothesis if it is of the form (a = a) - try $ do { - (lhs, rhs) ← match_eq ht, - unify lhs rhs, - clear h }, - -- If new hypothesis is of the form (@heq A a B b) where - -- A and B can be unified then convert it into (a = b) using - -- the eq_of_heq lemma - try $ do { - (A, lhs, B, rhs) ← match_heq ht, - unify A B, - heq ← mk_app `eq [lhs, rhs], - pr ← mk_app `eq_of_heq [h], - assertv hname heq pr, - clear h }, injection_intro d (tail ns) + | e ns := skip meta def injection_with (h : expr) (ns : list name) : tactic unit := @@ -43,13 +33,15 @@ do ht ← infer_type h, (lhs, rhs) ← match_eq ht, env ← get_env, - if is_constructor_app env lhs ∧ - is_constructor_app env rhs ∧ - const_name (get_app_fn lhs) = const_name (get_app_fn rhs) + n_f ← return (const_name (get_app_fn lhs)), + n_inj ← return (n_f <.> "inj_arrow"), + if n_f = const_name (get_app_fn rhs) ∧ env~>contains n_inj then do - tgt ← target, - I_name ← return $ name.get_prefix (const_name (get_app_fn lhs)), - pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, h], + c_inj ← mk_const n_inj, + arity ← get_arity c_inj, + tgt ← target, + args ← at_end₂ h tgt (arity - 1), + pr ← mk_mapp n_inj args, pr_type ← infer_type pr, pr_type ← whnf pr_type, apply pr, diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index f051dd3066..f8a512b619 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -533,6 +533,18 @@ match (expr.is_not e) with | none := fail "expression is not a negation" end +meta def match_and (e : expr) : tactic (expr × expr) := +match (expr.is_and e) with +| (some (α, β)) := return (α, β) +| none := fail "expression is not a conjunction" +end + +meta def match_or (e : expr) : tactic (expr × expr) := +match (expr.is_or e) with +| (some (α, β)) := return (α, β) +| none := fail "expression is not a disjunction" +end + meta def match_eq (e : expr) : tactic (expr × expr) := match (expr.is_eq e) with | (some (lhs, rhs)) := return (lhs, rhs) diff --git a/library/init/native/ir.lean b/library/init/native/ir.lean index 269d8ac408..350dfbf3cd 100644 --- a/library/init/native/ir.lean +++ b/library/init/native/ir.lean @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jared Roesch -/ prelude - -import init.meta.name +import init.meta.name init.meta.inductive_compiler namespace ir diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 1a28a0f6ff..10ecab1340 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -27,6 +27,7 @@ Authors: Daniel Selsam, Leonardo de Moura #include "library/explicit.h" #include "library/reducible.h" #include "library/class.h" +#include "library/sorry.h" #include "library/trace.h" #include "library/app_builder.h" #include "library/type_context.h" @@ -42,6 +43,26 @@ Authors: Daniel Selsam, Leonardo de Moura #include "frontends/lean/inductive_cmds.h" namespace lean { + +static void check_for_sorry(buffer const & params, buffer const & inds, buffer > const & intro_rules) { + for (expr const & param : params) { + if (has_sorry(param)) + throw exception(sstream() << "type of parameter '" << mlocal_name(param) << "' contains 'sorry'"); + } + + for (expr const & ind : inds) { + if (has_sorry(ind)) + throw exception(sstream() << "inductive type '" << mlocal_name(ind) << "' contains 'sorry'"); + } + + for (buffer const & irs : intro_rules) { + for (expr const & ir : irs) { + if (has_sorry(ir)) + throw exception(sstream() << "constructor '" << mlocal_name(ir) << "' contains 'sorry'"); + } + } +} + static level mk_succn(level const & l, unsigned offset) { level result = l; for (unsigned i = 0; i < offset; ++i) @@ -663,6 +684,7 @@ public: } environment shared_inductive_cmd(buffer const & params, buffer const & inds, buffer > const & intro_rules) { + check_for_sorry(params, inds, intro_rules); buffer new_params; buffer new_inds; buffer > new_intro_rules; diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 1d8128fa66..fcc7f15f25 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -28,6 +28,7 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/annotation.h" #include "library/explicit.h" +#include "library/sorry.h" #include "library/unfold_macros.h" #include "library/protected.h" #include "library/private.h" @@ -46,6 +47,7 @@ Author: Leonardo de Moura #include "library/constructions/cases_on.h" #include "library/constructions/projection.h" #include "library/constructions/no_confusion.h" +#include "library/constructions/injective.h" #include "library/inductive_compiler/add_decl.h" #include "library/tactic/elaborator_exception.h" #include "frontends/lean/parser.h" @@ -57,7 +59,6 @@ Author: Leonardo de Moura #include "frontends/lean/decl_attributes.h" #include "frontends/lean/inductive_cmds.h" - #ifndef LEAN_DEFAULT_STRUCTURE_INTRO #define LEAN_DEFAULT_STRUCTURE_INTRO "mk" #endif @@ -165,6 +166,18 @@ struct structure_cmd_fn { throw parser_error("only attribute [class] accepted for structures", pos); } + void check_for_sorry() { + for (expr const & param : m_params) { + if (has_sorry(param)) + throw exception(sstream() << "type of parameter '" << mlocal_name(param) << "' contains 'sorry'"); + } + + for (field_decl const & fdecl : m_fields) { + if (has_sorry(fdecl.local)) + throw exception(sstream() << "field '" << mlocal_name(fdecl.local) << "' contains 'sorry'"); + } + } + /** \brief Parse structure name and (optional) universe parameters */ void parse_decl_name() { m_name_pos = m_p.pos(); @@ -1063,7 +1076,7 @@ struct structure_cmd_fn { } } - void declare_no_confustion() { + void declare_no_confusion() { if (!has_eq_decls(m_env)) return; if (!has_heq_decls(m_env)) @@ -1073,6 +1086,19 @@ struct structure_cmd_fn { add_alias(no_confusion_name); } + void declare_injective_lemmas() { + if (!has_eq_decls(m_env)) + return; + if (!has_heq_decls(m_env)) + return; + if (!has_and_decls(m_env)) + return; + + m_env = mk_injective_lemmas(m_env, m_name); + add_alias(mk_injective_name(m_name)); + add_alias(mk_injective_arrow_name(m_name)); + } + void add_doc_string() { if (m_doc_string) m_env = ::lean::add_doc_string(m_env, m_name, *m_doc_string); @@ -1103,6 +1129,7 @@ struct structure_cmd_fn { m_mk = m_name + m_mk_short; process_empty_new_fields(); } + check_for_sorry(); infer_resultant_universe(); set_ctx_locals(); include_ctx_levels(); @@ -1114,7 +1141,8 @@ struct structure_cmd_fn { declare_coercions(); add_doc_string(); if (!m_inductive_predicate) { - declare_no_confustion(); + declare_no_confusion(); + declare_injective_lemmas(); } return m_env; } diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 100c30512e..db545707b1 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -1179,7 +1179,7 @@ expr mk_eq_mp(type_context & ctx, expr const & h1, expr const & h2) { } expr mk_iff_mp(type_context & ctx, expr const & h1, expr const & h2) { - return mk_app(ctx, get_iff_mpr_name(), h1, h2); + return mk_app(ctx, get_iff_mp_name(), h1, h2); } void initialize_app_builder() { diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 0327060cc4..2238693a98 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -112,6 +112,7 @@ name const * g_if_pos = nullptr; name const * g_iff = nullptr; name const * g_iff_false_intro = nullptr; name const * g_iff_intro = nullptr; +name const * g_iff_mp = nullptr; name const * g_iff_mpr = nullptr; name const * g_iff_refl = nullptr; name const * g_iff_symm = nullptr; @@ -124,6 +125,8 @@ name const * g_imp_congr_ctx_eq = nullptr; name const * g_implies = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; +name const * g_inductive_compiler_tactic_prove_nested_inj = nullptr; +name const * g_inductive_compiler_tactic_prove_pack_inj = nullptr; name const * g_insert = nullptr; name const * g_int = nullptr; name const * g_int_has_add = nullptr; @@ -487,6 +490,7 @@ void initialize_constants() { g_iff = new name{"iff"}; g_iff_false_intro = new name{"iff_false_intro"}; g_iff_intro = new name{"iff", "intro"}; + g_iff_mp = new name{"iff", "mp"}; g_iff_mpr = new name{"iff", "mpr"}; g_iff_refl = new name{"iff", "refl"}; g_iff_symm = new name{"iff", "symm"}; @@ -499,6 +503,8 @@ void initialize_constants() { g_implies = new name{"implies"}; g_implies_of_if_neg = new name{"implies_of_if_neg"}; g_implies_of_if_pos = new name{"implies_of_if_pos"}; + g_inductive_compiler_tactic_prove_nested_inj = new name{"inductive_compiler", "tactic", "prove_nested_inj"}; + g_inductive_compiler_tactic_prove_pack_inj = new name{"inductive_compiler", "tactic", "prove_pack_inj"}; g_insert = new name{"insert"}; g_int = new name{"int"}; g_int_has_add = new name{"int", "has_add"}; @@ -863,6 +869,7 @@ void finalize_constants() { delete g_iff; delete g_iff_false_intro; delete g_iff_intro; + delete g_iff_mp; delete g_iff_mpr; delete g_iff_refl; delete g_iff_symm; @@ -875,6 +882,8 @@ void finalize_constants() { delete g_implies; delete g_implies_of_if_neg; delete g_implies_of_if_pos; + delete g_inductive_compiler_tactic_prove_nested_inj; + delete g_inductive_compiler_tactic_prove_pack_inj; delete g_insert; delete g_int; delete g_int_has_add; @@ -1238,6 +1247,7 @@ name const & get_if_pos_name() { return *g_if_pos; } name const & get_iff_name() { return *g_iff; } name const & get_iff_false_intro_name() { return *g_iff_false_intro; } name const & get_iff_intro_name() { return *g_iff_intro; } +name const & get_iff_mp_name() { return *g_iff_mp; } name const & get_iff_mpr_name() { return *g_iff_mpr; } name const & get_iff_refl_name() { return *g_iff_refl; } name const & get_iff_symm_name() { return *g_iff_symm; } @@ -1250,6 +1260,8 @@ name const & get_imp_congr_ctx_eq_name() { return *g_imp_congr_ctx_eq; } name const & get_implies_name() { return *g_implies; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } +name const & get_inductive_compiler_tactic_prove_nested_inj_name() { return *g_inductive_compiler_tactic_prove_nested_inj; } +name const & get_inductive_compiler_tactic_prove_pack_inj_name() { return *g_inductive_compiler_tactic_prove_pack_inj; } name const & get_insert_name() { return *g_insert; } name const & get_int_name() { return *g_int; } name const & get_int_has_add_name() { return *g_int_has_add; } diff --git a/src/library/constants.h b/src/library/constants.h index 331197b463..698d5b6526 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -114,6 +114,7 @@ name const & get_if_pos_name(); name const & get_iff_name(); name const & get_iff_false_intro_name(); name const & get_iff_intro_name(); +name const & get_iff_mp_name(); name const & get_iff_mpr_name(); name const & get_iff_refl_name(); name const & get_iff_symm_name(); @@ -126,6 +127,8 @@ name const & get_imp_congr_ctx_eq_name(); name const & get_implies_name(); name const & get_implies_of_if_neg_name(); name const & get_implies_of_if_pos_name(); +name const & get_inductive_compiler_tactic_prove_nested_inj_name(); +name const & get_inductive_compiler_tactic_prove_pack_inj_name(); name const & get_insert_name(); name const & get_int_name(); name const & get_int_has_add_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 4a85613d35..b2a4556eb7 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -107,6 +107,7 @@ if_pos iff iff_false_intro iff.intro +iff.mp iff.mpr iff.refl iff.symm @@ -119,6 +120,8 @@ imp_congr_ctx_eq implies implies_of_if_neg implies_of_if_pos +inductive_compiler.tactic.prove_nested_inj +inductive_compiler.tactic.prove_pack_inj insert int int.has_add diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt index d7f56a946d..a6aa07ecfb 100644 --- a/src/library/constructions/CMakeLists.txt +++ b/src/library/constructions/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(constructions OBJECT rec_on.cpp induction_on.cpp cases_on.cpp no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp has_sizeof.cpp - constructor.cpp drec.cpp) + constructor.cpp drec.cpp injective.cpp) diff --git a/src/library/constructions/init_module.cpp b/src/library/constructions/init_module.cpp index 45d704f1f3..37528c4868 100644 --- a/src/library/constructions/init_module.cpp +++ b/src/library/constructions/init_module.cpp @@ -6,14 +6,17 @@ Author: Leonardo de Moura */ #include "library/constructions/projection.h" #include "library/constructions/has_sizeof.h" +#include "library/constructions/injective.h" namespace lean{ void initialize_constructions_module() { initialize_def_projection(); initialize_has_sizeof(); + initialize_injective(); } void finalize_constructions_module() { + finalize_injective(); finalize_has_sizeof(); finalize_def_projection(); } diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp new file mode 100644 index 0000000000..76bd226b88 --- /dev/null +++ b/src/library/constructions/injective.cpp @@ -0,0 +1,283 @@ +/* +Copyright (c) 2017 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam, Leonardo de Moura +*/ +#include "kernel/find_fn.h" +#include "kernel/instantiate.h" +#include "kernel/declaration.h" +#include "kernel/type_checker.h" +#include "kernel/inductive/inductive.h" +#include "library/constructions/injective.h" +#include "library/type_context.h" +#include "library/app_builder.h" +#include "library/util.h" +#include "library/module.h" +#include "library/trace.h" +#include "library/vm/vm.h" +#include "library/tactic/tactic_state.h" +#include "library/tactic/intro_tactic.h" +#include "library/tactic/subst_tactic.h" + +namespace lean { + +static void collect_args(type_context & tctx, expr const & type, unsigned num_params, + buffer & params, buffer & args1, buffer & args2, buffer & new_args) { + expr ty = tctx.relaxed_whnf(type); + + for (unsigned param_idx = 0; param_idx < num_params; ++param_idx) { + expr param = tctx.push_local(binding_name(ty), binding_domain(ty), mk_implicit_binder_info()); + params.push_back(param); + ty = tctx.relaxed_whnf(instantiate(binding_body(ty), param)); + } + + expr type_post_params = ty; + + while (is_pi(ty)) { + expr arg = tctx.push_local(binding_name(ty), binding_domain(ty), mk_implicit_binder_info()); + args1.push_back(arg); + ty = tctx.relaxed_whnf(instantiate(binding_body(ty), arg)); + } + + expr result_type = ty; + ty = type_post_params; + + for (expr const & arg1 : args1) { + if (occurs(arg1, result_type)) { + args2.push_back(arg1); + } else { + expr arg2 = tctx.push_local(binding_name(ty), binding_domain(ty), mk_implicit_binder_info()); + args2.push_back(arg2); + new_args.push_back(arg2); + } + ty = tctx.relaxed_whnf(instantiate(binding_body(ty), args2.back())); + } + lean_assert(args1.size() == args2.size()); + lean_assert(!is_pi(ty)); +} + +expr mk_injective_type(environment const & env, name const & ir_name, expr const & ir_type, unsigned num_params, level_param_names const & lp_names) { + type_context tctx(env); + buffer params, args1, args2, new_args; + collect_args(tctx, ir_type, num_params, params, args1, args2, new_args); + expr c_ir_params = mk_app(mk_constant(ir_name, param_names_to_levels(lp_names)), params); + expr lhs = mk_app(c_ir_params, args1); + expr rhs = mk_app(c_ir_params, args2); + expr eq_type = mk_eq(tctx, lhs, rhs); + + buffer eqs; + for (unsigned arg_idx = 0; arg_idx < args1.size(); ++arg_idx) { + if (args1[arg_idx] != args2[arg_idx]) { + if (tctx.is_def_eq(tctx.infer(args1[arg_idx]), tctx.infer(args2[arg_idx]))) { + eqs.push_back(mk_eq(tctx, args1[arg_idx], args2[arg_idx])); + } else { + eqs.push_back(mk_heq(tctx, args1[arg_idx], args2[arg_idx])); + } + } + } + + expr and_type; + if (eqs.empty()) { + and_type = mk_true(); + } else { + and_type = eqs.back(); + unsigned i = eqs.size() - 1; + while (i > 0) { + --i; + and_type = mk_and(eqs[i], and_type); + } + } + + return tctx.mk_pi(params, tctx.mk_pi(args1, tctx.mk_pi(new_args, mk_arrow(eq_type, and_type)))); +} + +expr prove_by_assumption(type_context & tctx, expr const & ty, expr const & eq) { + if (is_eq(ty) && is_heq(tctx.infer(eq))) { + return mk_eq_of_heq(tctx, eq); + } else { + return eq; + } +} + +expr prove_conjuncts_core(type_context & tctx, expr const & ty, buffer const & eqs, unsigned idx) { + if (idx == eqs.size() - 1) { + lean_assert(!is_and(ty)); + return prove_by_assumption(tctx, ty, eqs[idx]); + } else { + expr A, B; + lean_verify(is_and(ty, A, B)); + expr a = prove_by_assumption(tctx, A, eqs[idx]); + expr b = prove_conjuncts_core(tctx, B, eqs, idx+1); + return mk_app(mk_constant(get_and_intro_name()), {A, B, a, b}); + } +} + +expr prove_conjuncts(type_context & tctx, expr const & ty, buffer const & eqs) { + return prove_conjuncts_core(tctx, ty, eqs, 0); +} + +expr prove_injective(environment const & env, expr const & inj_type, name const & ind_name) { + type_context tctx(env); + expr ty = inj_type; + + buffer args; + while (is_pi(ty)) { + expr arg = tctx.push_local_from_binding(ty); + args.push_back(arg); + ty = tctx.relaxed_whnf(instantiate(binding_body(ty), arg)); + } + + lean_assert(!args.empty()); + + expr tgt = ty; + + if (tgt == mk_true()) + return tctx.mk_lambda(args, mk_true_intro()); + + unsigned num_params = *inductive::get_num_params(env, ind_name); + unsigned num_indices = *inductive::get_num_indices(env, ind_name); + + buffer nc_args; + buffer mask; + for (unsigned i = 0; i < num_params; ++i) { + nc_args.push_back(args[i]); + mask.push_back(true); + } + for (unsigned i = 0; i < num_indices; ++i) { + mask.push_back(false); + } + nc_args.push_back(tgt); + mask.push_back(true); + + mask.push_back(false); + mask.push_back(false); + nc_args.push_back(args.back()); + mask.push_back(true); + + expr H_nc = mk_app(tctx, name(ind_name, "no_confusion"), num_params + num_indices + 4, &mask[0], &nc_args[0]); + + // (x1 = x2 -> xs1 == xs2 -> (x1 = x2 /\ xs1 = xs2) + ty = binding_domain(tctx.relaxed_whnf(tctx.infer(H_nc))); + + buffer eqs; + buffer eqs_to_keep; + while (is_pi(ty)) { + expr eq = tctx.push_local_from_binding(ty); + eqs.push_back(eq); + if (app_arg(tctx.infer(eq)) != app_arg(app_fn(tctx.infer(eq)))) + eqs_to_keep.push_back(eq); + ty = tctx.relaxed_whnf(instantiate(binding_body(ty), eq)); + } + + return tctx.mk_lambda(args, mk_app(H_nc, tctx.mk_lambda(eqs, prove_conjuncts(tctx, ty, eqs_to_keep)))); +} + +expr prove_injective_arrow(environment const & env, expr const & inj_arrow_type, name const & inj_name) { + type_context tctx(env); + expr ty = inj_arrow_type; + + buffer args; + while (is_pi(ty)) { + expr arg = tctx.push_local_from_binding(ty); + args.push_back(arg); + ty = tctx.relaxed_whnf(instantiate(binding_body(ty), arg)); + } + + lean_assert(args.size() >= 3); + expr H_eq = args[args.size() - 3]; + expr H_P = args[args.size() - 2]; + expr H_arrow = args[args.size() - 1]; + + expr conjuncts = mk_app(tctx, inj_name, H_eq); + expr pf = H_arrow; + while (is_and(tctx.infer(conjuncts))) { + pf = mk_app(pf, mk_and_elim_left(tctx, conjuncts)); + conjuncts = mk_and_elim_right(tctx, conjuncts); + } + pf = mk_app(pf, conjuncts); + return tctx.mk_lambda(args, pf); +} + +environment mk_injective_arrow(environment const & env, name const & ir_name) { + declaration d = env.get(mk_injective_name(ir_name)); + type_context tctx(env); + + name P_lp_name = mk_fresh_lp_name(d.get_univ_params()); + expr P = tctx.push_local(name("P"), mk_sort(mk_param_univ(P_lp_name)), mk_strict_implicit_binder_info()); + + expr ty = d.get_type(); + buffer args; + while (is_pi(ty)) { + expr arg = tctx.push_local_from_binding(ty); + args.push_back(arg); + ty = tctx.relaxed_whnf(instantiate(binding_body(ty), arg)); + } + + buffer eqs; + expr it = ty; + expr A, B; + while (is_and(it, A, B)) { + eqs.push_back(A); + it = B; + } + eqs.push_back(it); + + expr antecedent = P; + unsigned i = eqs.size(); + while (i > 0) { + --i; + antecedent = mk_arrow(eqs[i], antecedent); + } + + name inj_arrow_name = mk_injective_arrow_name(ir_name); + expr inj_arrow_type = tctx.mk_pi(args, tctx.mk_pi(P, mk_arrow(antecedent, P))); + expr inj_arrow_val = prove_injective_arrow(env, inj_arrow_type, mk_injective_name(ir_name)); + lean_trace(name({"constructions", "injective"}), tout() << inj_arrow_name << " : " << inj_arrow_type << "\n";); + environment new_env = module::add(env, check(env, mk_definition_inferring_trusted(env, inj_arrow_name, + cons(P_lp_name, d.get_univ_params()), inj_arrow_type, inj_arrow_val, true))); + return new_env; +} + +environment mk_injective_lemmas(environment const & _env, name const & ind_name) { + environment env = _env; + + auto idecls = inductive::is_inductive_decl(env, ind_name); + if (!idecls) + throw exception(sstream() << "'" << ind_name << "' not an inductive datatype\n"); + + if (is_inductive_predicate(env, ind_name) || !can_elim_to_type(env, ind_name)) + return _env; + + inductive::inductive_decl idecl = *idecls; + level_param_names lp_names = idecl.m_level_params; + unsigned num_params = idecl.m_num_params; + + buffer intro_rules; + to_buffer(idecl.m_intro_rules, intro_rules); + + for (inductive::intro_rule ir : intro_rules) { + name ir_name = inductive::intro_rule_name(ir); + expr ir_type = inductive::intro_rule_type(ir); + expr inj_type = mk_injective_type(env, ir_name, ir_type, num_params, lp_names); + expr inj_val = prove_injective(env, inj_type, ind_name); + lean_trace(name({"constructions", "injective"}), tout() << ir_name << " : " << inj_type << " :=\n " << inj_val;); + env = module::add(env, check(env, mk_definition_inferring_trusted(env, mk_injective_name(ir_name), lp_names, inj_type, inj_val, true))); + env = mk_injective_arrow(env, ir_name); + } + return env; +} + +name mk_injective_name(name const & ir_name) { + return name(ir_name, "inj"); +} + +name mk_injective_arrow_name(name const & ir_name) { + return name(ir_name, "inj_arrow"); +} + +void initialize_injective() { + register_trace_class(name({"constructions", "injective"})); +} + +void finalize_injective() {} +} diff --git a/src/library/constructions/injective.h b/src/library/constructions/injective.h new file mode 100644 index 0000000000..5b4b98c1fd --- /dev/null +++ b/src/library/constructions/injective.h @@ -0,0 +1,22 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam, Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { + +environment mk_injective_lemmas(environment const & env, name const & ind_name); + +environment mk_injective_arrow(environment const & env, name const & ir_name); + +expr mk_injective_type(environment const & env, name const & ir_name, expr const & ir_type, unsigned num_params, level_param_names const & lp_names); + +name mk_injective_name(name const & ir_name); +name mk_injective_arrow_name(name const & ir_name); + +void initialize_injective(); +void finalize_injective(); +} diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index 2dd2987982..72958ed72e 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -21,6 +21,7 @@ Author: Daniel Selsam #include "library/constructions/brec_on.h" #include "library/constructions/no_confusion.h" #include "library/constructions/has_sizeof.h" +#include "library/constructions/injective.h" #ifndef LEAN_DEFAULT_XINDUCTIVE_REC_ON #define LEAN_DEFAULT_XINDUCTIVE_REC_ON true @@ -99,6 +100,7 @@ class add_basic_inductive_decl_fn { if (gen_cases_on && gen_no_confusion && has_eq && has_heq) { m_env = mk_no_confusion(m_env, ind_name); + m_env = mk_injective_lemmas(m_env, ind_name); } if (gen_brec_on && has_prod) { diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp index 5487d3964b..734c42b4cd 100644 --- a/src/library/inductive_compiler/mutual.cpp +++ b/src/library/inductive_compiler/mutual.cpp @@ -22,6 +22,7 @@ Author: Daniel Selsam #include "library/attribute_manager.h" #include "library/pattern_attribute.h" #include "library/constructions/has_sizeof.h" +#include "library/constructions/injective.h" #include "library/inductive_compiler/compiler.h" #include "library/inductive_compiler/basic.h" #include "library/inductive_compiler/mutual.h" @@ -369,6 +370,25 @@ class add_mutual_inductive_decl_fn { } } + void define_injective() { + unsigned basic_ir_idx = 0; + for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { + buffer const & irs = m_mut_decl.get_intro_rules(ind_idx); + for (expr const & ir : irs) { + if (!static_cast(m_env.find(mk_injective_name(mlocal_name(m_basic_decl.get_intro_rule(0, basic_ir_idx)))))) { + return; + } + expr inj_and_type = mk_injective_type(m_env, mlocal_name(ir), Pi(m_mut_decl.get_params(), mlocal_type(ir)), m_mut_decl.get_num_params(), to_list(m_mut_decl.get_lp_names())); + expr inj_and_val = mk_constant(mk_injective_name(mlocal_name(m_basic_decl.get_intro_rule(0, basic_ir_idx))), m_mut_decl.get_levels()); + lean_trace(name({"inductive_compiler", "mutual", "injective"}), tout() << mk_injective_name(mlocal_name(ir)) << " : " << inj_and_type << " :=\n " << inj_and_val << "\n";); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, mk_injective_name(mlocal_name(ir)), to_list(m_mut_decl.get_lp_names()), inj_and_type, inj_and_val, true))); + m_env = mk_injective_arrow(m_env, mlocal_name(ir)); + m_tctx.set_env(m_env); + basic_ir_idx++; + } + } + } + void define_intro_rules() { unsigned basic_ir_idx = 0; for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { @@ -787,6 +807,7 @@ public: define_ind_types(); define_intro_rules(); define_sizeofs(); + define_injective(); define_recursors(); return m_env; @@ -812,6 +833,7 @@ void initialize_inductive_compiler_mutual() { register_trace_class(name({"inductive_compiler", "mutual", "rec"})); register_trace_class(name({"inductive_compiler", "mutual", "sizeof"})); register_trace_class(name({"inductive_compiler", "mutual", "range"})); + register_trace_class(name({"inductive_compiler", "mutual", "injective"})); g_mutual_suffix = new name("_mut_"); } diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 74fe55b1c7..5d1fe8bb9c 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -30,6 +30,7 @@ Author: Daniel Selsam #include "library/protected.h" #include "library/attribute_manager.h" #include "library/pattern_attribute.h" +#include "library/constructions/injective.h" #include "library/tactic/simp_lemmas.h" #include "library/constructions/has_sizeof.h" #include "library/inductive_compiler/ginductive.h" @@ -38,6 +39,7 @@ Author: Daniel Selsam #include "library/inductive_compiler/nested.h" #include "library/inductive_compiler/util.h" #include "library/tactic/induction_tactic.h" +#include "library/tactic/subst_tactic.h" #include "library/tactic/simp_result.h" #include "library/tactic/simplify.h" #include "library/tactic/eqn_lemmas.h" @@ -97,6 +99,7 @@ class add_nested_inductive_decl_fn { expr m_primitive_unpack; bool m_elim_to_type; + bool m_prove_inj; buffer > > > m_pack_arity; // [ind_idx][ir_idx][ir_arg_idx] @@ -104,6 +107,7 @@ class add_nested_inductive_decl_fn { bool m_in_define_nested_irs{false}; unsigned m_curr_nest_idx{0}; simp_lemmas m_lemmas; + simp_lemmas m_inj_lemmas; unsigned get_curr_ind_idx() { lean_assert(m_in_define_nested_irs); return m_pack_arity.size() - 1; } unsigned get_curr_ir_idx() { lean_assert(m_in_define_nested_irs); return m_pack_arity[get_curr_ind_idx()].size() - 1; } @@ -279,6 +283,49 @@ class add_nested_inductive_decl_fn { m_elim_to_type = nest_elim_to_type; } + void check_prove_inj() { + for (unsigned ind_idx = 0; ind_idx < m_nested_decl.get_num_inds(); ++ind_idx) { + for (unsigned ir_idx = 0; ir_idx < m_nested_decl.get_num_intro_rules(ind_idx); ++ir_idx) { + m_prove_inj = static_cast(m_env.find(mk_injective_arrow_name(mlocal_name(m_inner_decl.get_intro_rule(ind_idx, ir_idx))))); + return; + } + } + m_prove_inj = false; + } + + expr mk_pack_injective_type(name const & pack_name, optional pack_arity = optional()) { + type_context::tmp_locals locals(m_tctx); + buffer all_args; + expr full_ty = m_tctx.infer(mk_constant(pack_name, m_nested_decl.get_levels())); + expr ty = full_ty; + expr prev_ty; + + unsigned arg_idx = 0; + while (is_pi(ty)) { + expr arg = locals.push_local_from_binding(ty); + all_args.push_back(arg); + prev_ty = ty; + ty = m_tctx.relaxed_whnf(instantiate(binding_body(ty), arg)); + arg_idx++; + if (static_cast(pack_arity) && arg_idx == *pack_arity) { + break; + } + } + expr arg1 = all_args.back(); + all_args.pop_back(); + expr arg2 = locals.push_local_from_binding(prev_ty); + + expr eq_lhs = mk_app(mk_app(mk_constant(pack_name, m_nested_decl.get_levels()), all_args), arg1); + expr eq_rhs = mk_app(mk_app(mk_constant(pack_name, m_nested_decl.get_levels()), all_args), arg2); + + expr iff_lhs = mk_eq(m_tctx, eq_lhs, eq_rhs); + expr iff_rhs = mk_eq(m_tctx, arg1, arg2); + expr pack_inj_type = m_tctx.mk_pi(all_args, m_tctx.mk_pi(arg1, m_tctx.mk_pi(arg2, mk_iff(iff_lhs, iff_rhs)))); + lean_trace(name({"inductive_compiler", "nested", "injective"}), + tout() << "[pn_pack_injective_type]: " << full_ty << " ==> " << pack_inj_type << "\n";); + return pack_inj_type; + } + void define_theorem(name const & n, expr const & ty, expr const & val) { assert_no_locals(n, ty); assert_no_locals(n, val); @@ -806,7 +853,8 @@ class add_nested_inductive_decl_fn { prove_pi_pack_unpack(pi_pack, pi_unpack, ldeps, nested_pack_fn, nested_unpack_fn, arg_ty); prove_pi_unpack_pack(pi_pack, pi_unpack, ldeps, nested_pack_fn, nested_unpack_fn, arg_ty); - prove_pi_sizeof_pack(pi_pack, ldeps, nested_pack_fn, arg_ty); + prove_pi_pack_sizeof(pi_pack, ldeps, nested_pack_fn, arg_ty); + prove_pi_pack_injective(m_nested_decl.get_num_params() + ldeps.size() + 1); return optional >(pi_pack, m_nested_decl.get_num_params() + ldeps.size() + 1); } @@ -1033,6 +1081,7 @@ class add_nested_inductive_decl_fn { prove_nested_pack_unpack(start, end, c_nested_pack, c_nested_unpack, indices, nest_idx); prove_nested_unpack_pack(start, end, c_nested_pack, c_nested_unpack, indices, nest_idx); prove_nested_pack_sizeof(start, end, c_nested_pack, indices, nest_idx); + prove_nested_pack_injective(nest_idx); return optional(c_nested_pack, c_nested_unpack); } @@ -1214,6 +1263,7 @@ class add_nested_inductive_decl_fn { prove_primitive_pack_unpack(indices); prove_primitive_unpack_pack(indices); prove_primitive_pack_sizeof(indices); + prove_primitive_pack_injective(); } ///////////////////////////// @@ -1328,6 +1378,40 @@ class add_nested_inductive_decl_fn { simplify_fn(ctx, dcs, slss, cfg) {} }; + simp_config get_simp_config() { + simp_config cfg; + cfg.m_max_steps = 1000000; + cfg.m_contextual = false; + cfg.m_lift_eq = false; + cfg.m_canonize_instances = false; + cfg.m_canonize_proofs = false; + cfg.m_use_axioms = false; + cfg.m_zeta = false; + cfg.m_use_matcher = false; + return cfg; + } + + expr prove_by_tactic(name const & lemma_name, expr const & goal_type, name const & tactic, buffer const & rev_args) { + metavar_context mctx; + expr goal_mvar = mctx.mk_metavar_decl(local_context(), goal_type); + vm_obj tstate = to_obj(mk_tactic_state_for_metavar(m_env, m_opts, lemma_name, mctx, goal_mvar)); + buffer all_rev_args; + all_rev_args.push_back(tstate); + all_rev_args.append(rev_args); + + vm_state S(m_env, m_opts); + vm_obj result = S.invoke(tactic, all_rev_args.size(), all_rev_args.begin()); + + if (optional s_new = tactic::is_success(result)) { + lean_trace(name({"inductive_compiler", "nested", "prove"}), tout() << "[success]: " << lemma_name << "\n";); + mctx = s_new->mctx(); + return mctx.instantiate_mvars(goal_mvar); + } else { + lean_trace(name({"inductive_compiler", "nested", "prove"}), tout() << "[failed]: " << lemma_name << "\n";); + throw exception(sstream() << "Failed to prove: '" << lemma_name << "'"); + } + } + expr prove_by_simp(local_context const & lctx, expr const & thm, list Hs, bool use_sizeof) { environment env = set_reducible(m_env, get_sizeof_name(), reducible_status::Irreducible, false); env = set_reducible(env, get_add_name(), reducible_status::Irreducible, false); @@ -1340,15 +1424,7 @@ class add_nested_inductive_decl_fn { all_lemmas = add(tctx_whnf, all_lemmas, mlocal_name(H), H_type, H, LEAN_DEFAULT_PRIORITY); } lean_trace(name({"inductive_compiler", "nested", "simp", "start"}), tout() << thm << "\n";); - simp_config cfg; - cfg.m_max_steps = 1000000; - cfg.m_contextual = false; - cfg.m_lift_eq = false; - cfg.m_canonize_instances = false; - cfg.m_canonize_proofs = false; - cfg.m_use_axioms = false; - cfg.m_zeta = false; - cfg.m_use_matcher = false; + simp_config cfg = get_simp_config(); defeq_can_state dcs; sizeof_simplify_fn simplifier(tctx, dcs, all_lemmas, cfg); auto thm_pr = simplifier.prove_by_simp(get_eq_name(), thm); @@ -1436,6 +1512,20 @@ class add_nested_inductive_decl_fn { m_lemmas = add(tctx_synth, m_lemmas, n, LEAN_DEFAULT_PRIORITY); } + void prove_primitive_pack_injective() { + if (!m_prove_inj) return; + name pack_name = mk_primitive_name(fn_type::PACK); + expr goal = mk_pack_injective_type(pack_name); + name lemma_name = mk_injective_name(pack_name); + buffer args; + args.push_back(to_obj(mk_primitive_name(fn_type::UNPACK_PACK))); + args.push_back(to_obj(mk_primitive_name(fn_type::UNPACK))); + expr proof = prove_by_tactic(lemma_name, goal, get_inductive_compiler_tactic_prove_pack_inj_name(), args); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, lemma_name, to_list(m_nested_decl.get_lp_names()), goal, proof, true))); + m_tctx.set_env(m_env); + m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); + } + void prove_nested_pack_unpack(expr const & start, expr const & end, expr const & nested_pack, expr const & nested_unpack, buffer const & index_locals, unsigned nest_idx) { name n = mk_nested_name(fn_type::PACK_UNPACK, nest_idx); expr x_packed = mk_local_pp("x_packed", mk_app(end, index_locals)); @@ -1476,6 +1566,20 @@ class add_nested_inductive_decl_fn { m_lemmas = add(tctx_synth, m_lemmas, n, LEAN_DEFAULT_PRIORITY); } + void prove_nested_pack_injective(unsigned nest_idx) { + if (!m_prove_inj) return; + name pack_name = mk_nested_name(fn_type::PACK, nest_idx); + expr goal = mk_pack_injective_type(pack_name); + name lemma_name = mk_injective_name(pack_name); + buffer args; + args.push_back(to_obj(mk_nested_name(fn_type::UNPACK_PACK, nest_idx))); + args.push_back(to_obj(mk_nested_name(fn_type::UNPACK, nest_idx))); + expr proof = prove_by_tactic(lemma_name, goal, get_inductive_compiler_tactic_prove_pack_inj_name(), args); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, lemma_name, to_list(m_nested_decl.get_lp_names()), goal, proof, true))); + m_tctx.set_env(m_env); + m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); + } + expr prove_by_funext(expr const & goal, expr const & fn1, expr const & fn2) { buffer args; expr fn = get_app_args(goal, args); @@ -1530,7 +1634,7 @@ class add_nested_inductive_decl_fn { m_tctx.set_env(m_env); } - void prove_pi_sizeof_pack(expr const & pi_pack, buffer const & ldeps, expr const & nested_pack_fn, expr const & arg_ty) { + void prove_pi_pack_sizeof(expr const & pi_pack, buffer const & ldeps, expr const & nested_pack_fn, expr const & arg_ty) { name n = mk_pi_name(fn_type::SIZEOF_PACK); type_context tctx_synth(m_env, m_tctx.get_options(), m_synth_lctx, transparency_mode::Semireducible); @@ -1559,6 +1663,20 @@ class add_nested_inductive_decl_fn { m_tctx.set_env(m_env); } + void prove_pi_pack_injective(unsigned arity) { + if (!m_prove_inj) return; + name pack_name = mk_pi_name(fn_type::PACK); + expr goal = mk_pack_injective_type(pack_name, optional(arity)); + name lemma_name = mk_injective_name(pack_name); + buffer args; + args.push_back(to_obj(mk_pi_name(fn_type::UNPACK_PACK))); + args.push_back(to_obj(mk_pi_name(fn_type::UNPACK))); + expr proof = prove_by_tactic(lemma_name, goal, get_inductive_compiler_tactic_prove_pack_inj_name(), args); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, lemma_name, to_list(m_nested_decl.get_lp_names()), goal, proof, true))); + m_tctx.set_env(m_env); + m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); + } + //////////////////////////////////////////// ///// Stage 7: define nested recursors ///// //////////////////////////////////////////// @@ -1802,6 +1920,30 @@ class add_nested_inductive_decl_fn { return ty; } + + void define_nested_injectives() { + if (!m_prove_inj) return; + for (unsigned ind_idx = 0; ind_idx < m_nested_decl.get_num_inds(); ++ind_idx) { + for (unsigned ir_idx = 0; ir_idx < m_nested_decl.get_num_intro_rules(ind_idx); ++ir_idx) { + expr const & ir = m_nested_decl.get_intro_rule(ind_idx, ir_idx); + name inj_name = mk_injective_name(mlocal_name(ir)); + expr inj_type = mk_injective_type(m_env, mlocal_name(ir), Pi(m_nested_decl.get_params(), mlocal_type(ir)), + m_nested_decl.get_num_params(), to_list(m_nested_decl.get_lp_names())); + + buffer rev_args; + rev_args.push_back(to_obj(mk_injective_arrow_name(mlocal_name(m_inner_decl.get_intro_rule(ind_idx, ir_idx))))); + rev_args.push_back(to_obj(m_inj_lemmas)); + + expr inj_val = prove_by_tactic(inj_name, inj_type, get_inductive_compiler_tactic_prove_nested_inj_name(), rev_args); + m_env = module::add(m_env, + check(m_env, + mk_definition_inferring_trusted(m_env, inj_name, to_list(m_nested_decl.get_lp_names()), inj_type, inj_val, true))); + m_env = mk_injective_arrow(m_env, mlocal_name(ir)); + } + } + m_tctx.set_env(m_env); + } + public: add_nested_inductive_decl_fn(environment const & env, options const & opts, name_map const & implicit_infer_map, @@ -1826,6 +1968,7 @@ public: } check_elim_to_type(); + check_prove_inj(); define_nested_inds(); define_nested_has_sizeofs(); @@ -1833,6 +1976,8 @@ public: define_nested_irs(); define_nested_recursors(); define_nested_cases_on(); + define_nested_injectives(); + return optional(m_env); } @@ -1859,6 +2004,7 @@ void initialize_inductive_compiler_nested() { register_trace_class(name({"inductive_compiler", "nested", "sizeof"})); register_trace_class(name({"inductive_compiler", "nested", "prove"})); + register_trace_class(name({"inductive_compiler", "nested", "injective"})); register_trace_class(name({"inductive_compiler", "nested", "define"})); register_trace_class(name({"inductive_compiler", "nested", "define", "success"})); diff --git a/src/library/tactic/subst_tactic.h b/src/library/tactic/subst_tactic.h index 5afd4149b3..16f3312959 100644 --- a/src/library/tactic/subst_tactic.h +++ b/src/library/tactic/subst_tactic.h @@ -18,7 +18,7 @@ namespace lean { \pre mctx.get_metavar_decl(mvar) != none \pre typeof(H) is an equality \pre symm == false ==> is_local(lhs(typeof(H))) - \pre symm == false ==> is_local(rhs(typeof(H))) */ + \pre symm == true ==> is_local(rhs(typeof(H))) */ expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, expr const & mvar, expr const & H, bool symm, hsubstitution * substs); diff --git a/src/library/type_context.h b/src/library/type_context.h index b81f59c79b..77e4f06ca7 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -363,6 +363,11 @@ public: virtual optional is_stuck(expr const &) override; virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override; + virtual expr push_local_from_binding(expr const & e) { + lean_assert(is_binding(e)); + return push_local(binding_name(e), binding_domain(e), binding_info(e)); + } + virtual void pop_local() override; virtual expr abstract_locals(expr const & e, unsigned num_locals, expr const * locals) override; diff --git a/src/library/util.cpp b/src/library/util.cpp index fe216ea5b9..730de0c10f 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -51,6 +51,16 @@ level get_level(abstract_type_context & ctx, expr const & A) { return sort_level(S); } +name mk_fresh_lp_name(level_param_names const & lp_names) { + name l("l"); + int i = 1; + while (std::find(lp_names.begin(), lp_names.end(), l) != lp_names.end()) { + l = name("l").append_after(i); + i++; + } + return l; +} + bool occurs(expr const & n, expr const & m) { return static_cast(find(m, [&](expr const & e, unsigned) { return n == e; })); } @@ -155,6 +165,10 @@ bool has_pprod_decls(environment const & env) { return has_constructor(env, get_pprod_mk_name(), get_pprod_name(), 4); } +bool has_and_decls(environment const & env) { + return has_constructor(env, get_and_intro_name(), get_and_name(), 4); +} + /* n is considered to be recursive if it is an inductive datatype and 1) It has a constructor that takes n as an argument 2) It is part of a mutually recursive declaration, and some constructor diff --git a/src/library/util.h b/src/library/util.h index ad2cf29c8e..483f66acd0 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -19,6 +19,9 @@ bool is_internal_name(name const & n); of A is not a sort. */ level get_level(abstract_type_context & ctx, expr const & A); +/** brief Return a name that does not appear in `lp_names`. */ +name mk_fresh_lp_name(level_param_names const & lp_names); + /** \brief Return true iff \c n occurs in \c m */ bool occurs(expr const & n, expr const & m); /** \brief Return true iff there is a constant named \c n in \c m. */ @@ -48,6 +51,7 @@ bool has_punit_decls(environment const & env); bool has_pprod_decls(environment const & env); bool has_eq_decls(environment const & env); bool has_heq_decls(environment const & env); +bool has_and_decls(environment const & env); /** \brief Return true iff \c n is the name of a recursive datatype in \c env. That is, it must be an inductive datatype AND contain a recursive constructor. diff --git a/tests/lean/inductive_sorry.lean b/tests/lean/inductive_sorry.lean new file mode 100644 index 0000000000..1c6cdc314c --- /dev/null +++ b/tests/lean/inductive_sorry.lean @@ -0,0 +1,12 @@ +inductive foo (A : sorry → ℕ) +| mk : foo + +inductive foo : sorry → ℕ +| mk : foo 0 + +inductive foo +| mk : sorry → foo + +structure foo (A : sorry → ℕ) := (x : ℕ) + +structure foo : Type := (x : bool → sorry) diff --git a/tests/lean/inductive_sorry.lean.expected.out b/tests/lean/inductive_sorry.lean.expected.out new file mode 100644 index 0000000000..9e23205657 --- /dev/null +++ b/tests/lean/inductive_sorry.lean.expected.out @@ -0,0 +1,5 @@ +inductive_sorry.lean:1:0: error: type of parameter 'A' contains 'sorry' +inductive_sorry.lean:4:0: error: type of parameter 'foo' contains 'sorry' +inductive_sorry.lean:7:0: error: constructor 'foo.mk' contains 'sorry' +inductive_sorry.lean:10:0: error: type of parameter 'A' contains 'sorry' +inductive_sorry.lean:12:0: error: field 'x' contains 'sorry' diff --git a/tests/lean/interactive/complete_field.lean.expected.out b/tests/lean/interactive/complete_field.lean.expected.out index 6df64d0b20..e81445d627 100644 --- a/tests/lean/interactive/complete_field.lean.expected.out +++ b/tests/lean/interactive/complete_field.lean.expected.out @@ -3,7 +3,7 @@ {"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"} {"msg":{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"},"response":"additional_message"} {"message":"file invalidated","response":"ok","seq_num":0} -{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":411},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5} -{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":411},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9} +{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5} +{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9} {"completions":[{"source":,"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":144},"text":"right","type":"?a ∧ ?b → ?b"}],"prefix":"r","response":"ok","seq_num":13} -{"completions":[{"source":,"text":"assoc","type":"(?a ∧ ?b) ∧ ?c ↔ ?a ∧ ?b ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"cases_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":14,"file":"/library/init/logic.lean","line":399},"text":"comm","type":"?a ∧ ?b ↔ ?b ∧ ?a"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"dcases_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":11,"file":"/library/init/logic.lean","line":659},"text":"decidable","type":"decidable (?p ∧ ?q)"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec","type":"(Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → Π (n : ?a ∧ ?b), ?C n"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":6,"file":"/library/init/logic.lean","line":207},"text":"elim","type":"?a ∧ ?b → (?a → ?b → ?c) → ?c"},{"source":{"column":4,"file":"/library/init/core.lean","line":136},"text":"elim_left","type":"?a ∧ ?b → ?a"},{"source":{"column":4,"file":"/library/init/core.lean","line":141},"text":"elim_right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":386},"text":"imp","type":"(?a → ?c) → (?b → ?d) → ?a ∧ ?b → ?c ∧ ?d"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"induction_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"intro","type":"?a → ?b → ?a ∧ ?b"},{"source":{"column":4,"file":"/library/init/core.lean","line":139},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":411},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":144},"text":"right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":210},"text":"swap","type":"?a ∧ ?b → ?b ∧ ?a"},{"source":{"column":4,"file":"/library/init/logic.lean","line":213},"text":"symm","type":"?a ∧ ?b → ?b ∧ ?a"}],"prefix":"","response":"ok","seq_num":17} +{"completions":[{"source":,"text":"assoc","type":"(?a ∧ ?b) ∧ ?c ↔ ?a ∧ ?b ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"cases_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":14,"file":"/library/init/logic.lean","line":393},"text":"comm","type":"?a ∧ ?b ↔ ?b ∧ ?a"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"dcases_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":11,"file":"/library/init/logic.lean","line":653},"text":"decidable","type":"decidable (?p ∧ ?q)"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec","type":"(Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → Π (n : ?a ∧ ?b), ?C n"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":6,"file":"/library/init/logic.lean","line":201},"text":"elim","type":"?a ∧ ?b → (?a → ?b → ?c) → ?c"},{"source":{"column":4,"file":"/library/init/core.lean","line":136},"text":"elim_left","type":"?a ∧ ?b → ?a"},{"source":{"column":4,"file":"/library/init/core.lean","line":141},"text":"elim_right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":380},"text":"imp","type":"(?a → ?c) → (?b → ?d) → ?a ∧ ?b → ?c ∧ ?d"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"induction_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"intro","type":"?a → ?b → ?a ∧ ?b"},{"source":{"column":4,"file":"/library/init/core.lean","line":139},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":144},"text":"right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":204},"text":"swap","type":"?a ∧ ?b → ?b ∧ ?a"},{"source":{"column":4,"file":"/library/init/logic.lean","line":207},"text":"symm","type":"?a ∧ ?b → ?b ∧ ?a"}],"prefix":"","response":"ok","seq_num":17} diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 496705efc5..b61d7f2fab 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -112,6 +112,7 @@ run_cmd script_check_id `if_pos run_cmd script_check_id `iff run_cmd script_check_id `iff_false_intro run_cmd script_check_id `iff.intro +run_cmd script_check_id `iff.mp run_cmd script_check_id `iff.mpr run_cmd script_check_id `iff.refl run_cmd script_check_id `iff.symm @@ -124,6 +125,8 @@ run_cmd script_check_id `imp_congr_ctx_eq run_cmd script_check_id `implies run_cmd script_check_id `implies_of_if_neg run_cmd script_check_id `implies_of_if_pos +run_cmd script_check_id `inductive_compiler.tactic.prove_nested_inj +run_cmd script_check_id `inductive_compiler.tactic.prove_pack_inj run_cmd script_check_id `insert run_cmd script_check_id `int run_cmd script_check_id `int.has_add