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