CODEWITHSUNDEEP
listmathcoq
Tweak
Tweak

Reputation: 187

Proof with list in Coq

I'm trying to proof something in CoqIDE (for school). I'm blocking on a step, here is the 

`Print length. (* la longueur de listes *)


Lemma mystere A:  forall l : list A, length l = 0 <-> l = nil.
intros.
destruct l.
* split.
- intros.
reflexivity.
- intros. 
simpl.
reflexivity.
* split.
- intros.
???? <- I have tried many things, but without success..
Admitted.
`

Thanks guys for your consideration !

Upvotes: 2

Views: 444

Answers (2)

shafiq ahmad
shafiq ahmad

Reputation: 11

Try this: I think change your Lemma like so,

Definition length_nil_list (l: nat): bool :=
match l with
| O => true
| S _ => false
end.

Compute length_nil_list (S O).
Compute length_nil_list (O).
Compute length_nil_list (S (S O)).

Definition list_nil {X : Type} (l: list X): bool:=
match l with
| nil => true
| cons h t => false
end.

Compute list_nil [].
Compute list_nil [0].
Compute list_nil nil.

Lemma mystere A:  forall l : list A, 
length_nil_list (length l) = true <-> list_nil l = true.
Proof.
intros.
destruct l.
* split.
- intros.
reflexivity.
- intros. 
simpl.
reflexivity.
* split. 
- simpl. auto.
- simpl in *. auto.
Qed.

Upvotes: 0

Jason Gross
Jason Gross

Reputation: 6138

Your context has a hypothesis

H : length (a :: l) = 0

This is absurd, because length (a :: l) is a successor. You can see this by running simpl in * or simpl in H, which results in

H : S (length l) = 0

If you now run

Search (S _) 0.

the second entry (after H) is

O_S: forall n : nat, 0 <> S n

So we can run symmetry in H to get a hypothesis that matches better with O_S.

H : 0 = S (length l)

Since a <> b is just a = b -> False, we can now run apply O_S in H to get

H : False

And now we are effectively done. We can finish the proof with exfalso; assumption, or with exfalso; exact H, or with easy, or with now trivial (or now idtac), or with case H, or with destruct H, or with elim H, or with refine match H with end, or with induction H, or with refine (False_rect _ H), or tauto. All of these basically amount to the same thing (although some of them, like easy and tauto, can also solve other goals).

Upvotes: 6

Related Questions