Menu
I'm in Coq trying to prove that
Theorem evenb_n__oddb_Sn : ∀n : nat,
evenb n = negb (evenb (S n)).
I'm using induction on n. The base case is trivial, so I'm at the inductive case and my goal looks like:
k : nat
IHk : evenb k = negb (evenb (S k))
============================
evenb (S k) = negb (evenb (S (S k)))
Now of course there's a fundamental axiom of functions that asserts
a = b -> f a = f b
For all functions f : A -> B. So I could apply negb to both sides, which would give me
k : nat
IHk : evenb k = negb (evenb (S k))
============================
negb (evenb (S k)) = negb (negb (evenb (S (S k))))
Which would let me use my inductive hypothesis from right to left, the negations on the right would cancel each other out, and the defintion of evenb would complete the proof.
Now, there might be a better way to prove this particular theorem (edit: there is, I did it another way), but as this in general seems like a useful thing to do, what's the way to modify an equality goal in Coq by applying a function to both sides?
Note: I realize that this wouldn't work for any arbitrary function: for example, you could use it to prove that -1 = 1 by applying abs to both sides. However, it holds for any injective function (one for which f a = f b -> a = b), which negb is. Perhaps a better question to ask, then, is given a function which operates on a proposition (for example, negb x = negb y -> x = y), how can I use that function to modify the current goal?
223
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. inversion: Deduces equalities that must be true given an equality between two constructors.
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.
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.
It seems that you just want the apply tactic. If you have a lemma negb_inj : forall b c, negb b = negb c -> b = c, doing apply negb_inj on your goal would give you exactly that.
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
