How to apply in many hypothesis at once?

user_8809295 0
Viewed 45

I have these things as truth:

a, x, y : nat
l : list nat
H : x <= y
S : sorted (y :: l)
IHS : sorted (insert a (y :: l))
H0 : a > x
H1 : a > y

How may I apply Nat.lt_le_incl in both H0 and H1 without copy-paste? apply in * does not work, even if i try it. I get the following error: Syntax error: [id_or_meta] expected after 'in' (in [in_hyp_as])

coq
1 Answers

You can use a match tactic:

repeat match goal with
| H : ?a > ?b |- _ => apply Nat.lt_le_incl in H
end

The repeat tactic simply runs its argument for as many times as possible. The match tactic checks if the goal and context have a certain form and, if so, runs the tactic supplied in the corresponding branch. (The wildcard after the |- means that we don't care what the goal is; we are just interested in finding hypotheses of the form ?a > ?b.)

user_16337700
Related