Menu
In Coq, when attempting to prove equality of records, is there a tactic that will decompose that into equality of all of its fields? For example,
Record R := {x:nat;y:nat}.
Variables a b c d : nat.
Lemma eqr : {|x:=a;y:=b|} = {|x:=c;y:=d|}.
Is there a tactic that will reduce this to a = c /\ b = d? Note that in general, any of a b c d might be big complicated proof terms (which I can then discharge with a proof irrelevance axiom).
306
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.
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.
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.
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.
You can use the f_equal tactic, which will work not only for records, but also for arbitrary goals of the form f x1 .. xn = f y1 .. yn, where f is any function symbol, of which constructors are a particular case.
134
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
