search

harp-project / AML-Formalization

GNU Lesser General Public License v2.1
10 stars 5 forks source link

If a proof mode tactic can't solve a side condition, it shouldn't fail with an unhelpful message or hang forever #443

Open Engreyight opened 1 week ago

Engreyight commented 1 week ago

Certain tactics, such as mlDestructEx try solving side conditions, which sometimes fails. If this happens, they should at least produce an error with what failed, but it would be preferable to just let the user solve it.

Sometimes these tactics will also try solving forever, in which case they should instead time out and preferably do one of the above two things.

Example:

  Goal forall (f : Pattern -> Pattern) p,
    well_formed p ->
    (forall x, well_formed x -> well_formed (f x)) ->
    Γ ⊢ (ex, f p) ---> Top.
  Proof.
    intros * Hwfp Hwff.
    toMLGoal. specialize (Hwff p Hwfp); wf_auto2.
    mlIntro.
    (* This fails, but... *)
    Fail Timeout 5 mlDestructEx "0" as x.
    mlFreshEvar as x.
    opose proof (MLGoal_destructEx Γ [] [] Top x "0" (f p) AnyReasoning _ _ _ _ _).
    try_solve_pile.
    ltac2:(fm_solve ()).
    ltac2:(fm_solve ()).
    2: ltac2:(fm_solve ()).
    2: apply X; simpl.
    (* ...this is the proof state it should produce instead. *)
    (* The condition is unsolvable, so mlDestructEx hangs. *)
    (* The user should be asked to prove it instead. *)
  Abort.