Menu
I'm trying to destruct a pair equivalence hypothesis in proof when using Coq. But I didn't find the tactic for me.
The case is:
a, b, a', b' : nat
H0 : (a, b) = (a', b')
I want to destruct the pairs in H0 to generate
H1 : a = a'
H2 : b = b'
How can I achieve this? Which tactic should I use? Or should I define lemma for destructing such pair?
Thank you!
474
simpl: Simplifies the goal or hypotheses in the context. unfold: Unfolds the definitions of terms. apply: Uses implications to transform goals and hypotheses. rewrite: Replaces a term with an equivalent term if the equivalence of the terms has already been proven.
Tactics specify how to transform the proof state of an incomplete proof to eventually generate a complete proof. Proofs can be developed in two basic ways: In forward reasoning, the proof begins by proving simple statements that are then combined to prove the theorem statement as the last step of the proof.
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.
Use injection H0 followed by intros as a first approximation.
126
You can also do it in one step with inversion H0.
3
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
