```
Fixpoint myfunction ( l: list nat) : list nat :=
match l with
| nil => nil
|h::t => match (here code requires h and next of h) with
|false => []
|true => h1:: myfunction t
end
end.
```

Want to keep list of h1 in true (case). e.g l=[2,33,41,5,66,7] require list [33,41,5,66,7] .

If i write h::h1::t then i have to add third constructor h::nil . This case gives wrong results when there are

odd elements in input list.

You need to define what happens in the case the list has exactly 1 element, because if the list length is odd, you will end up in this case. So you need a match structure like:

```
match l with
| nil => nil
| h::nil => what do we do here?
| h1::h2::t => the usual case
end
```

```
Fixpoint myfunction ( l l2: list nat) : list nat :=
match l with
| nil => nil
||h::nil => [h]
|h1::h2::t => match (leb h2 ( count h1 l2) ) with
|false => []
|true => h2:: myfunction t l2
end
end.
```

I need first &next element of complete list for comaparison (list may contain even or odd elements).

1) h1::h2::t ->during recursive call there is jump/skip of two elements.

e.g l=[2,33,41,5,66,7,8] output list = [33 ] t=[41,5,66,7,8].

During next recursion h1=41 & h2= 5 output list = [33,5 ]

But i need [33,41, 5 ]

2) How i should append element of constructor 2 with list of constructor 3, or correct the above?

You can pass (h2::t) as argument to the recursive call (or (h1::t) since you prepend h2 in the recursive call). You need to give a measure then (as explained before). Coq won't be able to figure out automatically that the list is decreasing, but the proof will be trivial.

You may use the `as`

keyword like in

```
Fixpoint f (l: list nat) :list nat :=
match l with
| nil => nil
| [x] => [x]
| h1::((h2::t) as tl) => if p h1 h2
then h1 :: f tl (* skips 1 element *)
else h2 :: h1 :: f t (* skips 2 elements *)
end.
```

Lot of thanks.

I want to adjust function (fun a b l) in above . Output

of this function is list which gives nil in case of one element in the list and in empty case). I am replacing l with (fun a b l) then second constructor [x]=> [x] gives problem. May i address it? error msg: cannot find decreasing value.

```
Fixpoint f (a b:nat) (l: list nat) :list nat :=
match (fun a b l) with
| nil => nil
| [x] => [x] (* according to modification it should be nil in case of one element *)
| h1::((h2::t) as tl) => if p h1 h2
then h1 :: f a b tl (* skips 1 element *)
else h2 :: h1 :: f a b t (* skips 2 elements *)
end.
```

This looks ok :

```
Require Import List.
Import ListNotations.
Parameter p : nat -> nat -> bool.
Fixpoint f (a b:nat) (l: list nat) : list nat :=
match l with
| nil => nil
| [x] => [x] (* according to modification it should be nil in case of one element *)
| h1::((h2::t) as tl) => if p h1 h2
then h1 :: f a b tl (* skips 1 element *)
else h2 :: h1 :: f a b t (* skips 2 elements *)
end.
```

```
```

output list of (fun a b l) is different list than input argument list l.Secondly, output of (fun a b l) is empty when it contains one element and or when it is empty. But input argument list l is empty only when this list is empty.Third,in recursive call tl should be assign to input argument list l which causes conflict with output of (fun a b l). Introduction of two lists , one for fun ab l and second for recursive call . (could be solution?0

Fixpoint f (a b:nat) (l l2: list nat) :list nat :=

match (F a b l) with

| nil => nil

| [x] => [x] (* problem here, according to modification it should be nil in case of one element in new definition *)

| h1::((h2::t) as tl) => if eq h1 h2

then h1 :: f a b l tl (* skips 1 element *)

else h2 :: h1 :: f a b l t

May be you should assume (or prove with your example) that `length (F a b l) <= length l`

. (I renamed `fun`

into `F`

because `fun`

is a Coq keyword). Here's a simple example (you may have to change the definitions of `F`

and `p`

).

Note that your definitions present some problems (in addition to the recursion):

The arguments `a`

, `b`

and `l`

keep the same value during all the computation, and `l2`

is unused.

So, it's extremely difficult to understand and comment what you wanted to compute.

```
Require Import Arith Lia List Recdef .
Import ListNotations.
Definition F a b l := map (fun x => x + a + b) l.
Remark Fdecr : forall a b l, length (F a b l) <= length l.
Proof.
intros; unfold F; now rewrite map_length.
Qed.
Definition p : nat -> nat -> bool := Nat.ltb.
Function f (a b: nat) (l: list nat) {measure length l} : list nat :=
match (F a b l) with
nil | [_] => nil
| x:: ( (y:: t) as tl) => if p x y then x :: f a b tl
else y :: x :: f a b t
end.
Proof.
intros.
generalize (Fdecr a b l) ;rewrite teq; simpl; lia.
intros.
generalize (Fdecr a b l); rewrite teq; simpl; lia.
Defined.
(* Example *)
Compute f 10 20 [4;6;3;7].
```

(deleted)

Last updated: Oct 04 2023 at 22:01 UTC