It sometimes happens that an Aesop rule has a premise that will always be true in practice, but Aesop can't always prove it. In such cases, it would be nice if Aesop could try to construct a proof under the assumption that the premise holds and then report the premise to the user as an additional subgoal.
I propose the following syntax and semantics for this feature:
A new builder option (force := [p_1, .., p_n]), applicable to forward/destruct and apply rules. The p_i are premises of the rule. For forward/destruct rules, the p_i automatically become non-immediate, so they are treated as additional subgoals which Aesop will try to prove recursively. (For apply rules, all premises are treated this way.) When Aesop fails so prove such a 'forced' goal, it nevertheless considers the goal proven and reports it to the user as an additional subgoal (if the proof is otherwise successful).
A new builder option (force! := [p_1, ..., p_n]). Works like force, but Aesop does not even try to prove the forced subgoals; instead it always reports them to the user (if the proof is otherwise successful).
A new builder option (promote := [p_1, ..., p_n]) for conditional simp rules. The p_i are again premises of the rule. When simp attempts to discharge a premise p_i, it usually runs simp on it and considers the premise proved if simp rewrites it to True. With the promote option, simp instead rewrites with the rule immediately (assuming that all other premises are successfully discharged) and leaves the p_i as additional 'promoted' subgoals for Aesop.
The builder options force and force! can also be applied to simp rules, with the effect that the premises are both promoted and forced.
It sometimes happens that an Aesop rule has a premise that will always be true in practice, but Aesop can't always prove it. In such cases, it would be nice if Aesop could try to construct a proof under the assumption that the premise holds and then report the premise to the user as an additional subgoal.
I propose the following syntax and semantics for this feature:
(force := [p_1, .., p_n]), applicable toforward/destructandapplyrules. Thep_iare premises of the rule. Forforward/destructrules, thep_iautomatically become non-immediate, so they are treated as additional subgoals which Aesop will try to prove recursively. (Forapplyrules, all premises are treated this way.) When Aesop fails so prove such a 'forced' goal, it nevertheless considers the goal proven and reports it to the user as an additional subgoal (if the proof is otherwise successful).(force! := [p_1, ..., p_n]). Works likeforce, but Aesop does not even try to prove the forced subgoals; instead it always reports them to the user (if the proof is otherwise successful).(promote := [p_1, ..., p_n])for conditionalsimprules. Thep_iare again premises of the rule. Whensimpattempts to discharge a premisep_i, it usually runssimpon it and considers the premise proved ifsimprewrites it toTrue. With thepromoteoption,simpinstead rewrites with the rule immediately (assuming that all other premises are successfully discharged) and leaves thep_ias additional 'promoted' subgoals for Aesop.forceandforce!can also be applied tosimprules, with the effect that the premises are both promoted and forced.