Coq how to target and transform hypotheses to show that they're false?

Question

I'm trying to prove that if two lists of booleans are equal (using a definition of equality that walks the lists structurally in the obvious way), then they have the same length.

In the course of doing so, however, I end up in a situation with a hypothesis that is false/uninhabited, but not literally False (and thus can't be targeted by the contradiction tactic).

Here's what I have so far.

Require Import Coq.Lists.List.
Require Export Coq.Bool.Bool.

Require Import Lists.List.
Import ListNotations.

Open Scope list_scope.
Open Scope nat_scope.



Fixpoint list_bool_eq (a : list bool) (b: list bool) : bool :=
  match (a, b) with
  | ([], []) => true
  | ([], _) => false
  | (_, []) => false
  | (true::a', true::b') => list_bool_eq a' b'
  | (false::a', false::b') => list_bool_eq a' b'
  | _ => false
  end.

Fixpoint length (a : list bool) : nat :=
  match a with
  | [] => O
  | _::a' => S (length a')
  end.

Theorem equal_implies_same_length : forall (a b : list bool) , (list_bool_eq a b) = true ->  (length a) = (length b).
intros.
induction a.
induction b.
simpl. reflexivity.

After this, the "goal state" (what's the right word?) of coq as shown by coqide looks like this.

2 subgoals
a : bool
b : list bool
H : list_bool_eq [] (a :: b) = true
IHb : list_bool_eq [] b = true -> length [] = length b
______________________________________(1/2)
length [] = length (a :: b)
______________________________________(2/2)
length (a :: a0) = length b

Clearing away some of the extraneous detail...

Focus 1.
clear IHb.

We get

1 subgoal
a : bool
b : list bool
H : list_bool_eq [] (a :: b) = true
______________________________________(1/1)
length [] = length (a :: b)

To us, as humans, length [] = length (a :: b) is clearly false/uninhabited, but that's okay because H : list_bool_eq [] (a :: b) = true is false too.

However, the hypothesis H is not literally False, so we can't just use contradiction.

How do I target/"focus my attention from the perspective of Coq" on the hypothesis H so I can show that it's uninhabited. Is there something roughly analogous to a proof bullet -, +, *, { ... } that creates a new context inside my proof specifically for showing that a given hypothesis is false?

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2017-07-11T22:27:44

If you simplify your hypothesis (simpl in H), you will see that it is equivalent to false = true. At that point, you can conclude the goal with the easy tactic, which is capable of discharging such "obvious" contradictions even when they are syntactically equal to False. As a matter of fact, you should not even need to perform the simplification beforehand; easy should be powerful enough to figure out what is contradictory by itself.

(It would have been better to prove the following stronger result: forall l1 l2, list_bool_eq l1 l2 = true <-> l1 = l2.)

Coq how to target and transform hypotheses to show that they're false?

1 Answers