Stream: Coq users

Topic: Beginner: SF question


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Oct 25 2021 at 13:24):

destruct (evenb n) eqn:H

view this post on Zulip Callan McGill (Oct 25 2021 at 13:28):

Thank you very much! :)

view this post on Zulip drew (Oct 25 2021 at 14:28):

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

view this post on Zulip drew (Oct 25 2021 at 14:28):

ah, whoops, i see!

view this post on Zulip drew (Oct 25 2021 at 14:28):

re: the destruct heading

view this post on Zulip drew (Oct 25 2021 at 14:28):

good clue :)

view this post on Zulip drew (Oct 25 2021 at 16:03):

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

view this post on Zulip drew (Oct 25 2021 at 16:04):

i get No primitive equality found.

view this post on Zulip Gaëtan Gilbert (Oct 25 2021 at 16:04):

is that your goal or an hypothesis?

view this post on Zulip drew (Oct 25 2021 at 16:04):

that is my goal

view this post on Zulip drew (Oct 25 2021 at 16:06):

ah shoot, this is the wrong thread, apologies.

view this post on Zulip Gaëtan Gilbert (Oct 25 2021 at 16:06):

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

view this post on Zulip drew (Oct 25 2021 at 16:06):

ha, makes sense


Last updated: Jan 29 2023 at 01:02 UTC