## Stream: Coq users

### Topic: pattern matching with two parameters

#### zohaze (Oct 27 2021 at 23:26):

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

#### Paolo Giarrusso (Oct 27 2021 at 23:51):

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.

#### zohaze (Oct 28 2021 at 00:20):

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

#### zohaze (Oct 28 2021 at 00:31):

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

#### Paolo Giarrusso (Oct 28 2021 at 01:45):

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

#### Paolo Giarrusso (Oct 28 2021 at 01:47):

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

#### zohaze (Nov 01 2021 at 02:10):

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)

#### zohaze (Nov 03 2021 at 14:27):

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

#### zohaze (Dec 18 2021 at 15:58):

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.

#### zohaze (Dec 19 2021 at 12:57):

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

Last updated: Oct 03 2023 at 04:02 UTC