How to try a tactic in Ltac, but continue if it fails

user_12288637 0
Viewed 53

I have a proof which concludes in two cases which look like this:

+ rewrite H. apply lemma1.
+ apply lemma1.

While this is relatively simple I would like to combine this into a single tactic. What I want to do in English is, "try to rewrite and if that fails, do nothing and try to apply lemma1.

So a related question is "What is the tactic that does nothing?"

Here is one of my attempts:

try (rewrite H || nil); apply lemma1.

I don't know know how to figure out what the "empty tactic" in Ltac is, nor how to find out its name.

Here is another, where I "distributed out" lemma1.

do 2 try (rewrite H; apply lemma1 || apply lemma1).

which also didn't prove the second case.

coq-tactic coq
1 Answers

I think you do not need a "do nothing" tactic in this case because when tactic given to the try fails try does nothing. If I see you right you want just try rewrite H; apply lemma1. and that is. So, it will try to rewrite H and in success case it will apply lemma1. Otherwise, when rewrite fails, it will just apply lemma1. So, it applies lemma1 in any case.

user_20666150
Related