Coq mathematical proof language: rewriting if condition

Question

I am trying to learn Coq mathematical proof language, but I ran into some problems trying to prove something that I led to the following stupid statement:

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

Here is my attempt:

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

At this point, the proof:

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

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

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

and the "bigger step"

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

fail with Warning: Insufficient justification. I don’t think that something is wrong with rewriting in the state, since the normal tactics of rewrite -> H will do the same.

I can also make this work without problems by wrapping an if in a function:

 Definition ite (cond: bool) (ab: 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 something wrong? Is there a way to save my original evidence? Is it just a flaw in the implementation of the language of mathematical evidence?

I note that in section 11.3.3 of the manual there is a possible related example ( 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 do not know how to get the b := true part in context.

Answer 1

One possible solution is to use per cases on b (see section 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 recreate the proof of your example reference manual, you can use define to do this:

 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. 

Answer 2

The proof keyword seems to proof into evidence mode, which is declarative. In contrast, the proof keyword goes into proof mode, which is mandatory. In this second case, we can easily prove this.

 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 have no answer. I tried several approaches that were similar to yours, but found the same problem again and again. Perhaps someone who is more familiar with declarative evidence may give a complete answer. Let us know if you find a solution!