feat(inductive_compiler): generate injectivity lemmas
This commit is contained in:
Daniel Selsam
Leonardo de Moura
parent
98e93b73b2
commit
538ac8d187
29 changed files with 803 additions and 72 deletions
|
|
@ -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) :=
|
||||
|
|
|
|||
|
|
@ -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₁)
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
103
library/init/meta/inductive_compiler.lean
Normal file
103
library/init/meta/inductive_compiler.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > 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<expr> 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<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules) {
|
||||
check_for_sorry(params, inds, intro_rules);
|
||||
buffer<expr> new_params;
|
||||
buffer<expr> new_inds;
|
||||
buffer<buffer<expr> > new_intro_rules;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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() {
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
|
|
|||
283
src/library/constructions/injective.cpp
Normal file
283
src/library/constructions/injective.cpp
Normal file
|
|
@ -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<expr> & params, buffer<expr> & args1, buffer<expr> & args2, buffer<expr> & 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> nc_args;
|
||||
buffer<bool> 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<expr> eqs;
|
||||
buffer<expr> 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<expr> 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<expr> 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<expr> 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<inductive::intro_rule> 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() {}
|
||||
}
|
||||
22
src/library/constructions/injective.h
Normal file
22
src/library/constructions/injective.h
Normal file
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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<expr> const & irs = m_mut_decl.get_intro_rules(ind_idx);
|
||||
for (expr const & ir : irs) {
|
||||
if (!static_cast<bool>(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_");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<buffer<buffer<optional<unsigned> > > > 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<bool>(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<unsigned> pack_arity = optional<unsigned>()) {
|
||||
type_context::tmp_locals locals(m_tctx);
|
||||
buffer<expr> 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<bool>(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<pair<expr, unsigned> >(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<expr_pair>(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<vm_obj> 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<vm_obj> 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<tactic_state> 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<expr> 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<vm_obj> 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<expr> 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<vm_obj> 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<expr> 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<expr> const & ldeps, expr const & nested_pack_fn, expr const & arg_ty) {
|
||||
void prove_pi_pack_sizeof(expr const & pi_pack, buffer<expr> 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<unsigned>(arity));
|
||||
name lemma_name = mk_injective_name(pack_name);
|
||||
buffer<vm_obj> 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<vm_obj> 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<implicit_infer_kind> 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<environment>(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"}));
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
|
|
@ -363,6 +363,11 @@ public:
|
|||
virtual optional<expr> 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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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<bool>(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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
12
tests/lean/inductive_sorry.lean
Normal file
12
tests/lean/inductive_sorry.lean
Normal file
|
|
@ -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)
|
||||
5
tests/lean/inductive_sorry.lean.expected.out
Normal file
5
tests/lean/inductive_sorry.lean.expected.out
Normal file
|
|
@ -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'
|
||||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue