CODEWITHSUNDEEP
coq
Isabelle Newbie
Isabelle Newbie

Reputation: 9378

Coq's mathematical proof language: Rewriting in if condition

I'm trying to learn Coq's mathematical proof language, but I ran into some trouble trying to prove something that I reduced to the following silly statement:

Lemma foo: forall b: bool, b = true -> (if b then 0 else 1) = 0.

Here's my attempt:

proof.
  let b: bool.
  let H: (b = true).

At this point the proof state is:

  b : bool
  H : b = true
  ============================
  thesis := 
   (if b then 0 else 1) = 0

Now I want to rewrite the if condition b to true in order to be able to prove the thesis. However, both a "small step" of

  have ((if b then 0 else 1) = (if true then 0 else 1)) by H.

and a "bigger step" of

  have ((if b then 0 else 1) = 0) by H.

fail with Warning: Insufficient justification. I don't think there's anything wrong with rewriting in the condition, as the normal rewrite -> H tactic will do the same.

I can also get this to work without problems by wrapping the if in a function:

Definition ite (cond: bool) (a b: nat) := if cond then a else b.
Lemma bar: forall b: bool, b = true -> (ite b 0 1) = 0.
proof.
  let b: bool. let H: (b = true).
  have (ite b 0 1 = ite true 0 1) by H. thus ~= 0.
end proof.

This is not very nice, of course. Am I doing anything wrong? Is there a way to rescue my original proof? Is this just a shortcoming of the implementation of the mathematical proof language?

I note that there is a possibly related example in Section 11.3.3 of the manual (at https://coq.inria.fr/doc/Reference-Manual013.html):

  a := false : bool
  b := true : bool
  H : False
  ============================
  thesis :=
  if b then True else False

Coq <  reconsider thesis as True.

But I don't know how to get the b := true part into the context.

Upvotes: 6

Views: 506

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15404

One possible solution is to use per cases on b (see sect. 11.3.12):

Lemma foo:
  forall b: bool, b = true -> (if b then 0 else 1) = 0.
proof.
  let b : bool.
  per cases on b.
    suppose it is true. thus thesis.
    suppose it is false. thus thesis.
  end cases.
end proof.
Qed.

I also tried to recreated the proof state of your reference manual example, you could use define for that:

Lemma manual_11_3_3 :
  if false then True else False ->
  if true then True else False.
proof.
  define a as false.
  define b as true.
  assume H : (if a then True else False).
  reconsider H as False.
  reconsider thesis as True.
Abort.

Upvotes: 3

Mitchell Buckley
Mitchell Buckley

Reputation: 118

It seems that the keyword proof enters into a proof mode that is declarative. By constrast, the keyword Proof enters into a proof mode that is imperative. In this second case we can prove it easily as follows.

Lemma foo: forall b: bool, b = true -> (if b then 0 else 1) = 0.                                     
Proof.                                                                                              
  intros b H.                                                                                       
  rewrite H.                                                                                        
  reflexivity.                                                                                      
Qed.

In the first case I do not have an answer. I tried a number of approaches that were similar to yours but found the same problem again and again. Perhaps someone who is more familiar with declarative proofs can give a full answer. Please let us know if you find the solution!

Upvotes: -1

Related Questions