```
Fixpoint count (v:nat) (l:list nat) : nat :=
match l with
| [] => 0
| h :: t => (if beq_nat h v then 1 else 0) + (count v t)
end.
Lemma lenth_1: forall (j: nat) (l: list nat),
length (0::l)=1->
count 0 (0::l)=1->
count( S j)(0::l)=0.
```

I think it would be good to add a description so people here can get a better idea.

Length of list is 1. It means one element is present in the list. At head position zero is present. Now presence of zero is confirm.Any other element which is not zero is not present in the list. We can say count_occ of (S j) in the list is zero. I can write this lemma as.

```
Lemma lenth_1: forall (j: nat) (l: list nat),
length (0::l)=1->
count 0 (0::l)=1->
(count( S j)(0::l)>0)->False.
```

(deleted)

Want to write lemma which shows that when one element exist in the list then list length is 1( Its means single element is present at the head and tail of the list is empty). Any element which is not part of list ,its occurrence in the same list is zero.

Any one like to tell me the problem in above lemma's statement. I do not know the error/problem in above.

zohaze said:

Any one like to tell me the problem in above lemma's statement. I do not know the error/problem in above.

There is no problem with your lemma. You can prove it by a case analysis on l.

```
Lemma length_1: forall (j: nat) (l: list nat),
length (0::l) =1 -> count 0 (0::l) = 1-> count(S j) (0::l)=0.
Proof.
destruct l.
- reflexivity.
- discriminate.
Qed.
```

Thank you.

@Pierre Castéran. Above lemma is valid when length is 1. May I write a lemma that list length is 1 for the following list & function

```
c :: myfunction n' a b c (d+1) l &
Fixpoint myfunction (n a b c d: nat) (l : list nat) : list nat :=
match n with
| O => [c]
| S n' =>
if a <? nth b l 0 then
c :: myfunction n' a b c (d+1) l
else
myfunction n' a b c d l
end.
```

Initial d=0.

Any one likes to help me in solving the above problem?

Hi Sara,

It is difficult to answer whithout knowing what your function should compute in function of its arguments.

For instance how the result of a computation depends on `d`

?

I noticed also also `a`

, `b`

and `l`

keep the same value along the computation,

and thus the test `a <? nth b l 0`

is always true, or always false.

My intuition is that, if `a < nth b l 0`

, your function will return a list with `n+1`

occurrences of `c`

, otherwise the list `[c]`

.

```
Compute myfunction 6 1 2 42 0 (1::2::3::4::5::nil).
= 42 :: 42 :: 42 :: 42 :: 42 :: 42 :: 42 :: nil
: list nat
Compute myfunction 6 4 2 42 0 (1::2::3::4::5::nil).
= 42 :: nil
: list nat
```

Pierre

First thanks.Initial value of a,b d=0. Value of d is incremented by the addition of element in the list.(1 element then d=1 ,2 elements then d=2). I am asking if have this list " c :: myfunction n' a b c (d+1) l" at output ,then I can prove list length is 1?

Hi, Sara,

If `a=b=d=0`

, and `a <? nth b l 0`

is true, then `myfunction n a b c d l`

returns a list of length `n+1`

,

if `a <? nth b l 0`

is false, it returns a list of lenght 1.

Thus the whole expression you give `c :: myfunction n' a b c (d+1) l`

has a length greater or equal than 2.

Note that the value of `d`

does not matter.

Here are some examples you may execute, and try new ones of your own.

```
(** a is less than the first element of the list *)
Compute 5::myfunction 5 0 0 5 0 (7::8::9::nil).
(** a is greater or equal than the first element of the list *)
Compute 5::myfunction 5 0 0 5 0 (0::7::8::9::nil).
(** l is empty *)
Compute 5::myfunction 8 0 0 5 0 nil.
```

If you remove the useless `d`

argument and rewrite the function in order to avoid repeated evaluations of the same test, you can obtain an equivalent and simpler definition.

```
Definition my_function (n a b c (* d removed *) :nat) l :=
if (a <? nth b l 0)
then repeat c (1+n)
else c::nil.
Compute 5::my_function 5 0 0 5 (7::8::9::nil).
Compute 5::my_function 5 0 0 5 (0::7::8::9::nil).
Compute 5::my_function 8 0 0 5 nil.
```

Best regards,

Pierre

Last updated: Sep 26 2023 at 12:02 UTC