diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean index 9f76abf45a..106c540d9b 100644 --- a/library/init/meta/coinductive_predicates.lean +++ b/library/init/meta/coinductive_predicates.lean @@ -69,9 +69,6 @@ meta def add_theorem_by (n : name) (ls : list name) (type : expr) (tac : tactic add_decl $ mk_theorem n ls type body, return $ const n $ ls.map param -meta def is_assigned (m : expr): tactic bool := -((get_assignment m >> return ff) <|> return tt) - meta def mk_exists_lst (args : list expr) (inner : expr) : tactic expr := args.mfoldr (λarg i:expr, do t ← infer_type arg, @@ -405,7 +402,7 @@ meta def add_coinductive_predicate func_intros.mmap' (λ⟨n, pp_n, t⟩, solve1 $ do bs ← intros, ms ← apply_core ((const n u_params).app_of_list $ ps ++ fs.map prod.fst) {new_goals := new_goals.all}, - params ← (ms.zip bs).enum.mfilter (λ⟨n, m, d⟩, is_assigned m), + params ← (ms.zip bs).enum.mfilter (λ⟨n, m, d⟩, bnot <$> is_assigned m), params.mmap' (λ⟨n, m, d⟩, mono d (fs.map prod.snd) <|> fail format! "failed to prove montonoicity of {n+1}. parameter of intro-rule {pp_n}")))), diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index dd05657918..906f1d5ebc 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -385,6 +385,9 @@ meta constant get_univ_assignment : level → tactic level /-- Return the value assigned to the given meta-variable. Fail if argument is not a meta-variable or if it is not assigned. -/ meta constant get_assignment : expr → tactic expr +/-- Return the value assigned to the given meta-variable. + Fail if argument is not a meta-variable. -/ +meta constant is_assigned : expr → tactic bool meta constant mk_fresh_name : tactic name /-- Return a hash code for expr that ignores inst_implicit arguments, and proofs. -/ @@ -728,16 +731,16 @@ do gs ← get_goals, meta def solve (ts : list (tactic unit)) : tactic unit := first $ map solve1 ts - private meta def focus_aux : list (tactic unit) → list expr → list expr → tactic unit +private meta def focus_aux : list (tactic unit) → list expr → list expr → tactic unit | [] [] rs := set_goals rs | (t::ts) [] rs := fail "focus tactic failed, insufficient number of goals" | tts (g::gs) rs := -do set_goals [g], - _::_ ← get_goals | focus_aux tts gs rs, - t::ts ← pure tts | fail "focus tactic failed, insufficient number of tactics", - t, - rs' ← get_goals, - focus_aux ts gs (rs ++ rs') + mcond (is_assigned g) (focus_aux tts gs rs) $ + do set_goals [g], + t::ts ← pure tts | fail "focus tactic failed, insufficient number of tactics", + t, + rs' ← get_goals, + focus_aux ts gs (rs ++ rs') /-- `focus [t_1, ..., t_n]` applies t_i to the i-th goal. Fails if the number of goals is not n. -/ meta def focus (ts : list (tactic unit)) : tactic unit := @@ -758,11 +761,11 @@ do g::gs ← get_goals, private meta def all_goals_core (tac : tactic unit) : list expr → list expr → tactic unit | [] ac := set_goals ac | (g :: gs) ac := - do set_goals [g], - _::_ ← get_goals | all_goals_core gs ac, - tac, - new_gs ← get_goals, - all_goals_core gs (ac ++ new_gs) + mcond (is_assigned g) (all_goals_core gs ac) $ + do set_goals [g], + tac, + new_gs ← get_goals, + all_goals_core gs (ac ++ new_gs) /-- Apply the given tactic to all goals. -/ meta def all_goals (tac : tactic unit) : tactic unit := @@ -772,11 +775,11 @@ do gs ← get_goals, private meta def any_goals_core (tac : tactic unit) : list expr → list expr → bool → tactic unit | [] ac progress := guard progress >> set_goals ac | (g :: gs) ac progress := - do set_goals [g], - _::_ ← get_goals | any_goals_core gs ac progress, - succeeded ← try_core tac, - new_gs ← get_goals, - any_goals_core gs (ac ++ new_gs) (succeeded.is_some || progress) + mcond (is_assigned g) (any_goals_core gs ac progress) $ + do set_goals [g], + succeeded ← try_core tac, + new_gs ← get_goals, + any_goals_core gs (ac ++ new_gs) (succeeded.is_some || progress) /-- Apply the given tactic to any goal where it succeeds. The tactic succeeds only if tac succeeds for at least one goal. -/ diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 0dc73f460e..05526486eb 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -601,7 +601,7 @@ vm_obj tactic_get_assignment(vm_obj const & e, vm_obj const & s0) { tactic_state const & s = tactic::to_state(s0); metavar_context mctx = s.mctx(); if (!is_metavar(to_expr(e))) { - return tactic::mk_exception("get_assignment tactic failed, argument is not an universe metavariable", s); + return tactic::mk_exception("get_assignment tactic failed, argument is not a metavariable", s); } else if (auto r = mctx.get_assignment(to_expr(e))) { return tactic::mk_success(to_obj(*r), s); } else { @@ -609,6 +609,15 @@ vm_obj tactic_get_assignment(vm_obj const & e, vm_obj const & s0) { } } +vm_obj tactic_is_assigned(vm_obj const & g, vm_obj const & s0) { + tactic_state const & s = tactic::to_state(s0); + if (!is_metavar(to_expr(g))) { + return tactic::mk_exception("is_assigned tactic failed, argument is not a metavariable", s); + } else { + return tactic::mk_success(mk_vm_bool(s.mctx().is_assigned(to_expr(g))), s); + } +} + vm_obj tactic_state_get_options(vm_obj const & s) { return to_obj(tactic::to_state(s).get_options()); } @@ -881,6 +890,7 @@ void initialize_tactic_state() { DECLARE_VM_BUILTIN(name({"tactic_state", "set_options"}), tactic_state_set_options); DECLARE_VM_BUILTIN(name({"tactic", "target"}), tactic_target); DECLARE_VM_BUILTIN(name({"tactic", "result"}), tactic_result); + DECLARE_VM_BUILTIN(name({"tactic", "is_assigned"}), tactic_is_assigned); DECLARE_VM_BUILTIN(name({"tactic", "format_result"}), tactic_format_result); DECLARE_VM_BUILTIN(name({"tactic", "infer_type"}), tactic_infer_type); DECLARE_VM_BUILTIN(name({"tactic", "whnf"}), tactic_whnf);