Reputation: 149
If i have a Theorem of the form:
Theorem my_thm (n: nat -> nat): exists t: nat, n t = 0.
Admitted.
If I want to prove it for a function that is such that my_func 0 = 0
, how can I tell coq that indeed there exists such t because my_func 0 = 0 ?
This does not have a deep goal but understand how existential proof works in coq.
Upvotes: 1
Views: 141
Reputation: 923
You can add an argument, here P
, that would assert that this property holds, and use it later on in your theorem, using the exists
tactic. For instance (I'm using ssreflect, but I guess you'll get the idea):
Theorem my_thm (n: nat -> nat) (P : n 0 = 0) : exists u, n u = 0.
Proof.
exists 0.
exact: P.
Qed.
Of course, you can also change the theorem body to better suit your needs.
Upvotes: 1