Hi!
I’m trying to prove the following theorem from ‘Logic’ which equates the two definitions of reversing a list.
I would want to proceed by induction on l. But I am not able to execute the “intros l” command. How do I do that?
Also, I would really appreciate any tips on syntax. I am facing trouble with telling Coq what I want to do, and unable to give the proper commands to execute and write efficient and compact proofs of theorems.
Thank you :))
Note that Software Foundation uses Function Extensionality in many places. Function Extensionality is the axiom saying that two functions are equal when they agree on all inputs, in other words:
Lemma functional_extensionality {A B} (f g : A -> B) :
(forall x, f x = g x) -> f = g.
To make progress here, you need to apply this lemma/axiom. By itself, Coq does not “intuit” this reasoning rule, so if you just intros l there, there is nothing to introduce, since the equality of functions is “just an equality” and not something defined using a quantifier.
Ah, I see. Thank you so much! I had read up on functional extensionality but didn’t realize it would be used here.