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?

`destruct (evenb n) eqn:H`

Thank you very much! :)

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

ah, whoops, i see!

re: the destruct heading

good clue :)

why can i not `discriminate`

on `x :: l = [ ]`

?

i get `No primitive equality found. `

is that your goal or an hypothesis?

that is my goal

ah shoot, this is the wrong thread, apologies.

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

ha, makes sense

Last updated: Jul 24 2024 at 12:02 UTC