# Prooving the length of a list under constraint

Dear all,

I am going a bit further in my Coq journey and I am confronted with a new problem.
I don’t exactly know if it’s the property that I have illdefined or if it is the proof process that I miss, si here it is:

I want essentially to prove that a list of booleans where each element is different (unique) has at most a size of 2.

My lemma looks like that :

``````Lemma there_are_two_bools :
forall l:list bool, (forall b, In b l -> exists! b2, In b2 l /\ b = b2) -> length l <= 2.

Proof.
intros.
case l.
unfold length.
intuition.

intros.
case l0.
unfold length.
intuition.

intros.
case l1.
unfold length.
intuition.

intros.
``````

At which point I essentially have a 3 elements list (longer than too) but the structure if l has vanished and so I don’t know how to use the unicity condition to show that this case is ill formed.

Your hypothesis does not state that every element of the list is unique, it is actually a tautology because the existential can be satisfied with the element given as hypothesis:

``````From Coq Require Import List.

Lemma valid A (l : list A) : forall b, In b l -> exists! b2, In b2 l /\ b = b2.
Proof. intros b b_in_l; exists b; red; intuition. Qed.
``````

In order to state that the list has no duplicate elements you could use the `NoDup` predicate from the standard library.

Thank you for that very quick anwser.

Could I ask for a bit more?
In particular, what does my hypothesis says?

I mean, if “there exists a unique b2 such that b2 in L and b2 = b” does not provide unicity I am not sure what it means then.

I’ll check NoDup, I guess it’s defined recursively.

Thank you.

b2 is always unique since you ask it to be equal to b, the problem is that this isn’t the unicity you want to talk about. You mean something like “there exists a unique i such that the ith element of L is b”.

So, silly question (only partially related) does ‘=’ mean equality or identity in Coq?

And, I think I see what you mean, b could be uniquely set but occur several time in the list on its own (like a pointer thing).

Then my question partly remains, since even with something like NoDup, when I do things like ‘case l’ then I lose grip on ‘NoDup l’ since I have in my hypothesis ‘b0 : bool’ and ‘l0 : list bool’ but nowhere do I have ‘l = b :: l0’ (which is weird to my understanding).

Thank you.

but nowhere do I have `l = b :: l0`

Then you probably mean using `case_eq l` (or `destruct l eqn:Hl`).

does ‘=’ mean equality or identity in Coq?

Yes, by default.

Herbelin, thank you so much.
My proof is still a bit longish I assume compared to what should be possible, but, indeed I managed to prove that my list only has 2 elements.

case_eq is really great.

Though, I have one more question if I may.
When I type `case x` it just apply case analysis on x in the goal, but when I do `case x, x0` it applies it also in the hypothesis.
Is there a reason for that?

Thank you

When I type `case x` it just apply case analysis on x in the goal, but when I do `case x, x0` it applies it also in the hypothesis.
Is there a reason for that?

Huh, probably not a good reason. The tactic `case` was supposed to evolve towards the semantics of `destruct` at some time but this was not pursued. As a trace of this `case x, x0` is like `destruct x, x0`. Do `case x; case x0` or `case x, x0 in |- *` if you want to work only on the goal (in the latter case, it will also remove the now useless hypotheses).

Also, I realize that I may have misunderstood your question about “equality or identity”. I thought you were talking about so-called Martin-Löf’s identity type and that you were using identity synonymously to equality. If this was a equation calling to choose between equality(in the sense of a syntactic proposition) or identity (in the sense of “true equality”), then the equal sign is an “equality” predicate, that is, it does not presume that the equality necessarily holds. In particular, we can have “equality” assumptions, which by construction are just assumed and thus have no proof. As for “equality” statements, only those which have a proof are worth be called identity. (But maybe, this was not your question either?)