Reference 16-oct. n1 > n2 & s < n2. It means recursive call is equal to n2 (lower value of pattern matching). We can prove mylen23=n2 ?

```
Require Import List PeanoNat.
Import ListNotations.
Fixpoint mylen2 (n1 n2 a b s c: nat) (l : list nat) : list nat :=
match n1 ,s <? n2 with
| O,true => [c]
| O, false=>nil
|_ ,false =>nil
|S n',true =>
if a <? nth b l 0 then
c:: mylen2 n' n2 a b (S s) c l
else
mylen2 n' n2 a b (S s) c l
end.
Fixpoint mylen23 (n1 n2 a b s c: nat) (l : list nat) : nat :=
match n1 ,s <? n2 with
| O,true => 1
| O, false=>0
|_ ,false =>0
|S n',true =>
if a <? nth b l 0 then
1+ mylen23 n' n2 a b (S s) c l
else
mylen23 n' n2 a b (S s) c l
end.
```

We can prove mylen23=n2 ?

No. Since `a`

, `b`

and `l`

are constant, ensure that `a >= nth b l 0`

, then `mylen23`

is either 0 or 1.

if a <? nth b l 0 then element will add in the list. Why we ensure a >= nth b l 0?

If a &b are not constant. On each recursive call their values are changing .Then possible?( I add two functions which change a &b )

I'm sorry, I'm unable to make sense of the question, of the context, or of what you're trying to do :frown:

However, at least https://coq.discourse.group has sections for some non-English languages, in case that is helpful.

I am asking that on each recursive call if new values are being assign to a & b (by introducing functions f1 f2 within function mylen23 ), then I can prove mylen23=n2 ? If I have non empty list then mylen23=0 could be avoided?

(deleted)

I am asking question again . Might be it is clear now. Both values(a & b) are changing on each iteration. After true condition add a value in the list. Just want to find the length of output list.

```
Require Import List PeanoNat.
Import ListNotations.
Fixpoint mylen2 (n1 n2 a b s c: nat) (l : list nat) : list nat :=
let a := (2+a) in
let b := (3+b) in
match n1 ,s <? n2 with
| O,true => [c]
| O, false=>nil
|_ ,false =>nil
|S n',true =>
if a <? nth b l 0 then
c:: mylen2 n' n2 a b (S s) c l
else
mylen2 n' n2 a b (S s) c l
end.
Fixpoint mylen23 (n1 n2 a b s c: nat) (l : list nat) : nat :=
let a := (2+a) in
let b := (3+b) in
match n1 ,s <? n2 with
| O,true => 1
| O, false=>0
|_ ,false =>0
|S n',true =>
if a <? nth b l 0 then
1+ mylen23 n' n2 a b (S s) c l
else
mylen23 n' n2 a b (S s) c l
end.
```

I want to write a lemma which shows that list length=2( by using above ). List =c::c:: mylen2 n' n2 a b (S(S s)) c l and its length is 2.

I am using above function to find length of list. Under what condition length of list is 2 ?

Last updated: Jan 29 2023 at 06:02 UTC