pattern matching with two parameters · Coq users

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):

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?

zohaze (Nov 03 2021 at 02:06):

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 ?

Stream: Coq users

Topic: pattern matching with two parameters

zohaze (Oct 27 2021 at 23:26):