Beginner: SF question · Coq users

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?