CODEWITHSUNDEEP
coqcoq-tactic
rausted
rausted

Reputation: 959

Coq true = false discriminate fails, no primitive equality

I'm trying to prove the following, and I think I have the right approach to solving by enumerating all the cases for b and all the single argument boolean functions f (should be 4 functions over 2 boolean values), proving the point by exhaustively destructing everything.

Theorem example :
  forall (f : bool -> bool) (b : bool),
  f (f b) = b.
Proof.
  intros.
  destruct (f (f b)).
  - destruct b. 
    + reflexivity. 
    + Fail discriminate. admit. 
  - destruct b eqn:Hqebb.
    + Fail discriminate. admit. 
    + reflexivity.  
Qed.

However, when I try to discriminate on the 2nd and 3rd steps, on false = true I get the following error:

Ltac call to "discriminate" failed.
No primitive equality found.

I've used discriminate before with inductive types and it worked as expected, so I was surprised it didn't work here with boolean types. Any ideas why?

Upvotes: 1

Views: 1996

Answers (2)

Vilhelm Sjöberg
Vilhelm Sjöberg

Reputation: 503

If you have an hypothesis true = false (which is impossible), you can use discriminate to finish the goal. In the goal you are stuck with, you are asked to prove true = false. No tactic can do that, it's an impossible task!

The particular example theorem you used is actually false:

Theorem not_example:
  ~ forall (f : bool -> bool) (b : bool), f (f b) = b.
Proof.  
  intros H.
  specialize (H (fun _ => true) false).
  simpl in H.
  discriminate.
Qed.

But in general, as Arthur said, the way to do this is is to use the eqn: option to destruct, to remember the relevant equations. E.g. here is a proof script that mostly proves your theorem, except for the cases where it is false:

Theorem example :
  forall (f : bool -> bool) (b : bool),
  f (f b) = b.
Proof.
  intros.
  destruct (f true) eqn:?; destruct (f false) eqn:?; destruct b; try congruence.

Upvotes: 3

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

The discriminate tactic only works if your context has a hypothesis that equates terms of inductive type that start with different constructors. When you perform the first call to discriminate, the context looks like this:

f : bool -> bool
============================
true = false

As you can see, the context does not contain any equality hypotheses, so discriminate cannot do anything. To solve this, you need to use the eqn: option to the destruct tactic, so that Coq records all the relevant facts in the context. For example, if you call

destruct b eqn:H.

and b is of type bool, then in addition to generating two subgoals as usual, Coq will add the hypotheses H : b = true and H : b = false.

(I appreciate that you changed your question, but I just wanted to note that the theorem you put there now is not provable. It shouldn't be too difficult to adapt this to your original question.)

Upvotes: 3

Related Questions