CODEWITHSUNDEEP
coqproof
Musher Soccoli
Musher Soccoli

Reputation: 149

Proving existance by providing an example

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

Answers (1)

Pierre Jouvelot
Pierre Jouvelot

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

Related Questions