From this example:
Example foo : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
y :: l = x :: j ->
x = y.
It can be solved just doing inversion on the second hypothesis:
Proof.
intros X x y z l j eq1 eq2. inversion eq2. reflexivity. Qed.
However, doing inversion also in the first hypothesis, yields apparently contradictory hypothesis:
Proof.
intros X x y z l j eq1 eq2. inversion eq2. inversion eq1. reflexivity. Qed.
Because, in this last proof, the generated hypothesis are:
H0 : y = x
H1 : l = j
H2 : x = z
H3 : y :: l = j
But, if I'm not missing something obvious, it is impossible for both H1 and H3 to be true at the same time.
Can someone explain me what is going on? Is it just that the example is "bad designed" (both hypothesis are contradictory) and that Coq inversion tactic just swallows them? Is it a principle of explosion based on two hypothesis considered together? If so, is it then possible to prove the example just by deriving anything from falsehood? How?
Your example is assuming contradictory hypotheses: they imply that length l + 2 is equal to length l + 1.
Require Import Coq.Lists.List.
Require Import Omega.
Example foo : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
y :: l = x :: j ->
x = y.
Proof.
intros X x y z l j eq1 eq2.
apply (f_equal (@length _)) in eq1.
apply (f_equal (@length _)) in eq2.
simpl in *.
omega.
Qed.
By the principle of explosion, it is not surprising that Coq is able to derive a contradictory context.
Besides this small oddity, there is nothing wrong with the fact that the generated hypotheses are contradictory: such contexts can arise even if the original hypotheses are consistent. Consider the following (admittedly contrived) proof:
Goal forall b c : bool, b = c -> c = b.
Proof.
intros b c e.
destruct b, c.
- reflexivity.
- discriminate.
- discriminate.
- reflexivity.
Qed.
The second and third branches have contradictory hypotheses (true = false and false = true), even if the original hypothesis, b = c, is innocuous. This example is a bit different from the original one, because the contradiction was not obtained by combining hypotheses. Instead, when we call destruct, we promise Coq to prove the conclusion by considering a few subgoals obtained by case analyses. If some of the subgoals happen to be contradictory, even better: there won't be any work to do there.