## Stream: Coq users

### Topic: list nat

#### zohaze (Feb 03 2023 at 16:40):

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

#### Michael Soegtrop (Feb 03 2023 at 18:23):

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

#### zohaze (Feb 04 2023 at 05:26):

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

#### Michael Soegtrop (Feb 04 2023 at 09:51):

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.

#### Pierre Castéran (Feb 04 2023 at 09:56):

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.

#### zohaze (Feb 25 2023 at 11:30):

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

#### Laurent Théry (Feb 25 2023 at 12:37):

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

#### zohaze (Feb 25 2023 at 14:10):

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

#### Pierre Castéran (Feb 25 2023 at 17:32):

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

#### zohaze (Feb 26 2023 at 17:22):

(deleted)

Last updated: Oct 04 2023 at 22:01 UTC