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
x :: l = [ ]?
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: Jan 29 2023 at 01:02 UTC