## Stream: Coq users

### Topic: length finding

#### sara lee (Oct 16 2021 at 04:10):

Lemma length_l: forall (a b: nat) (l : list nat),
b>0->
length l > 0->
length l <= a + b->
length l > b.
is provable with current hypothesis?

#### Paolo Giarrusso (Oct 16 2021 at 04:20):

No: a = 0, b = length l is a counterexample.

#### Paolo Giarrusso (Oct 16 2021 at 04:23):

Better: any length l <= b (with both positive) is a counterexample for any a.

#### Paolo Giarrusso (Oct 16 2021 at 04:24):

And instead of quantifying over l and taking the length, you could quantify over (c : nat)

#### zohaze (Oct 16 2021 at 06:21):

Thank you. quantify over (c : nat) means linking with other question list formation. Please reply question related to list formation.

#### sara lee (Oct 16 2021 at 06:39):

I also do not know how to find length l . I think count will show number of elements. Lets see suggestion by @Paolo Giarrusso.

#### Paolo Giarrusso (Oct 16 2021 at 09:37):

@zohaze What I meant does not require computing `length l`. I just meant that the proposed `length_l` is equivalent to `foo` below:

``````Lemma foo : forall (a b c : nat),
b > 0 ->
c > 0 ->
c <= a + b ->
c > b.
Proof. Admitted. (* Not actually provable. *)

Lemma length_l: forall (a b: nat) (l : list nat),
b>0->
length l > 0->
length l <= a + b->
length l > b.
Proof. intros. apply foo. Qed. (* This would work. *)
``````

Anyway, I replied to the other question.

#### zohaze (Oct 17 2021 at 11:07):

length l >0 . Want to compare two values of the list . I should write nth a l d or nth a (x::l) d. Two elements should exist in the list .I should perform induction so that list become x::x0::l , nth a (x::x0::l) d?

#### zohaze (Oct 17 2021 at 11:13):

I want to prove that one value of the list is larger than other. What basic lemmas may be helpful?

Last updated: Sep 30 2023 at 05:01 UTC