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?

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

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

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

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

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

@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.

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?

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

Last updated: Feb 01 2023 at 11:04 UTC