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.
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).
Herbelin, thank you so much.
You made my day.
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?
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?)
I have to say, all these different way of writing things, and sub tactics of sub tactics makes it a bit hard to follow everything.
Often, it feels like the proof is long just because you picked the wrong tactic at after the first intro.
For the equality/identity, it was really just a thought.
On the very moment I didn’t think about the fact that the very same element could occur several time in the list. It’s because I use lists for sets (for some historical reasons) and because since I create everything from scratch, things that could in principle happen do not because the previous function prevents them from happening, though when you want to prove the second function on its own, you have to care about these spurious cases.