## Stream: Coq users

### Topic: Beginner: SF question

#### Callan McGill (Oct 25 2021 at 13:14):

I am trying to work solve the question on `combine_even_orr` from SF and running into some issues. I define the function as follows:

``````Definition combine_odd_even (Podd Peven : nat -> Prop) : nat -> Prop :=
fun n => match evenb n with
| true  => Peven n
| false => Podd n
end.
``````

When I work with this I run into issues. For example, when trying to prove the following:

``````Theorem combine_odd_even_intro :
forall (Podd Peven : nat -> Prop) (n : nat),
(oddb n = true -> Podd n) ->
(oddb n = false -> Peven n) ->
combine_odd_even Podd Peven n.
Proof.

intros Podd Peven n odd_pf even_pf. unfold combine_odd_even. destruct (evenb n).
- apply even_pf.
``````

The destruct does not give me access to the equality `evenb n = true` in the first branch and that makes it very awkward to work with. I was wondering if there is a tactic that remembers the evidence for the equality and also if there is a better way to be doing this sort of thing?

#### Gaëtan Gilbert (Oct 25 2021 at 13:24):

`destruct (evenb n) eqn:H`

#### Callan McGill (Oct 25 2021 at 13:28):

Thank you very much! :)

#### drew (Oct 25 2021 at 14:28):

It's exercise 3 here https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html

#### drew (Oct 25 2021 at 14:28):

ah, whoops, i see!

good clue :)

#### drew (Oct 25 2021 at 16:03):

why can i not `discriminate` on `x :: l = [ ]`?

#### drew (Oct 25 2021 at 16:04):

i get `No primitive equality found. `

#### Gaëtan Gilbert (Oct 25 2021 at 16:04):

is that your goal or an hypothesis?

that is my goal

#### drew (Oct 25 2021 at 16:06):

ah shoot, this is the wrong thread, apologies.

#### Gaëtan Gilbert (Oct 25 2021 at 16:06):

discriminate is for when you have an absurd hypothesis not an impossible goal

#### drew (Oct 25 2021 at 16:06):

ha, makes sense

Last updated: Jan 29 2023 at 01:02 UTC