How can I handle this `false = true` case?

Question

I am trying to prove the following lemma.

Inductive bool : Type :=
  | true
  | false.

Lemma andb_true_iff : forall b1 b2 : bool,
  b1 && b2 = true <-> b1 = true /\ b2 = true.
Proof.
  intros.
  split.
  - intros. split.
    + destruct b1.
      * reflexivity.
      * discriminate.
    + destruct b2.
      * reflexivity.
      * simpl. 

And now I get

1 goal
b1 : bool
H : b1 && false = true
______________________________________(1/1)
false = true

This is very absurd, since false = true is never True. However, I can't discriminate this goal.

OK, maybe we should prove H to be False, which is exact false = true. We can't reject to prove a goal which we believe to be False. However, why can't I even rewrite this goal to False? Is it because we have not proved it yet? So I prove the following

Lemma false_true: (false = true) -> False.
Proof.
  intros.
  simpl in H.
  discriminate H.
Qed.

And seems the Lemma false_true can't be applied to this goal. Instead, I know I can write the following lemma to perform a rewrite

Lemma false_true2: (false = true) = False.
Proof. Admitted.

However, I think false_true and false_true2 are somehow very similar. Is there any way that instead of rewrite by false_true2, we can just apply false_true?

Or must I write the following to apply?

Lemma false_true3: False -> (false = true).
Proof.
  intros.
  destruct H.
Qed.

== NOTE ==

I have solved this problem by destructing b1 either. However, I want to know is there any way to resolve false = true, since it looks weird to me.

Answer 1

If you have something that you cannot prove in the goal, but contradictions in the assumptions, such as False, then you can just ignore the goal, and use the contradictions, because "ex falso quodlibet", from False follows anything.

In Coq's logic, falsehood is usually represented as assuming that you have a value from an empty set, a value that cannot possibly be created, or that two values with different constructors are the same (the latter is false because constructors are defined to be injective).

The proof is usually done by considering the cases that could have caused those (impossible) values end up as assumptions, and since there are zero ways for that, you dont have any cases to consider, and the goal is proved.

For example, if you have a term H : False in your assumptions you can just do destruct H. If you have false = true (which are two different constructors of values of type bool) then you can use inversion.

Also check out How to prove False from obviously contradictory assumptions and How do I prove false from a false hypothesis?

By the way, note that false (a value) is not the same as False (a type or proposition),

and it is not possible to prove (false = true) = False. However you can prove false = true <-> False.

Answer 2

In the current case, it appends that the _ && _ returns the value false when the second argument is false. This is given by a theorem available in the Bool library. You can find this theorem using the Search command.

Require Import Bool.

Search (_ && false).

The result shows.

andb_false_r : forall b : bool, b && false = false

rewriting with this theorem in your hypothesis H returns and hypothesis of the form.

`false = true`

In general, when such a hypothesis appears, you can finish by using the tactics like easy or discriminate, but here, the goal's conclusion has exactly the same statement, so you can even use assumption.

Of course, in this case, I am not using a new definition of the type bool, rather I rely on existing knowledge, but you initial posting is ambiguous on this matter, because you show a definition of bool (which would be different from the one used in the standard library), but you do not show a definition of andb, so we have to assume you are using the standard version.

Answer 3

First of all, bool is a special type in Coq which is encoded in the as you suggested:

Inductive bool : Type :=
  | true
  | false.

However, the notation _&&_ is something special if you try to Locate "&&":

Notation
"x && y" := andb x y : bool_scope (default interpretation)

where andb: bool -> bool -> bool is something that you cannot simply discriminate on as this tactic only works on explicit type constructors. In your case (I am assuming that you are importing Bool from Coq's stdlib), a && b is a type returned by a function and Coq has no idea if a = false then this term would be false.

Quoting

OK, maybe we should prove H to be False, which is exact false = true. We can't reject to prove a goal that we believe to be False. However, why can't I even rewrite this goal to False?

No. Coq does not know H: False implies false = true. You need to prove it. Or more generally, you have to convince Coq that a && b = true implies a = true /\ b = true. Fortunately, this theorem is provided by Bool.andb_true_iff with which you can eliminate H into b1 = true and false = true. Then you can destruct H and use discriminate since false = true never holds by looking at the constructors of bool type.

A warm tip: you should be aware of False and false and corresponding && and /\ because they are totally different: False is defined at the Prop level whereas false is just a type constructor for bool, which is just a vanilla type.