Menu
Is it possible to switch the current goal or subgoal to prove in Coq?
For example, I have a goal like this (from an eexists):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
What I want to do is to split and prove the right conjunct first. This I think will give the value of the existential variable ?s, and the left conjunct should be just a simplification away.
But split by default set the left conjunct ?s > 0 as the current goal.
______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
I know I can prefix tactics with 2: to operate on the second subgoal, but it's awkward because
1) I can't see the hypotheses for goal#2 and
2) if it's in a different context, goal#2 might be the third or the k_th goal. The proof won't be portable.
That's why I want to set the second goal as the current.
BTW, I am using CoqIDE (8.5).
708
rewrite: Replaces a term with an equivalent term if the equivalence of the terms has already been proven. inversion: Deduces equalities that must be true given an equality between two constructors. left / right: Replaces a goal consisting of a disjunction P \/ Q with just P or Q .
All that you need is to provide the witness first: Inductive A := X | Y . Definition P (a: A) : bool := match a with X => true | Y => false end. Theorem test : exists a: A, P a = true.
assert (HA := l1 H). assert (HB := l2 H). You can also do something like assert (H' := H). to explicitly copy H into H' , although you can usually resort to a more direct way for getting what you want. Save this answer.
reflexivity. Use reflexivity when your goal is to prove that something equals itself. In this example we will prove that any term x of type Set is equal to itself.
You can use Focus 2 to focus on the second goal.
105
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
