Stream: Coq users

Topic: Generalized Rewriting & Backtracking

view this post on Zulip Janno (Jun 02 2020 at 17:24):

Is there a way to get generalized rewriting with stratagies to interact with ltac backtracking? Asked differently: is there any way to get the following to succeed?

From Coq Require Import Setoid.
Axiom lem1 : False -> 1+1=2.
Axiom lem2 : True -> 1+1=2.
Goal 1+1=2. (rewrite_strat subterms (choice lem1 lem2)); exact I. Qed.

view this post on Zulip Matthieu Sozeau (Jun 03 2020 at 23:04):

I don't think rewrite_strat is a multi success tactic yes, but can certainly be turned into one (it's based on continuations already)

view this post on Zulip Janno (Jun 04 2020 at 12:38):

I suppose now I understand what a multi-success tactic is. Thanks! :)
Could you give an estimate of what would be involved in making this change (or providing a separate version of rewrite_strat)?

Last updated: Jun 18 2024 at 00:02 UTC