## Stream: Coq users

### Topic: elements mismatch

#### pianke (Feb 28 2023 at 16:21):

``````Fixpoint f  (l: list nat) :list nat :=
match l  with
| nil => nil
| [x] => [x]
| h1::((h2::t) as tl) => if eqb h1 h2  then h1 :: f  tl
else nil
end.
``````

example =[5;5;5;5;5;5] -> [5;5;5;5;5;5]
[5;5;5;5;6;5] it gives [5;5;5;5]. i want to modify it so that it gives [] in case of single mismatch found in the list e.g
[5;5;5;5;6;5]-> [] but i get [5;5;5;5]
May i exclude the last element of the list from comparison by | [x] => nil ?

#### Pierre Castéran (Feb 28 2023 at 17:48):

A possible solution (with an accumulator):

``````Fixpoint f_aux  (P: nat -> nat -> bool) (l acc: list nat) : list nat :=
match l with
nil => rev acc
| [x] => rev (x::acc)
| h1::((h2::t) as tl) => if P h1 h2  then f_aux P tl (h1::acc) else nil
end.

Definition f P l := f_aux P l [].

Compute f Nat.eqb  [5;5;5;5;5;5].
Compute f Nat.eqb  [5;5;5;6;5;5;5].

Compute f Nat.ltb [5;6;8;9;15;25] .
Compute f Nat.ltb [5;6;8;8;9;15;25].
``````

Indeed, if you replace `Nat.eqb`with Nat.ltb, you can implement a function which returns `l`if it is strictly sorted, otherwise `[]`.

#### Laurent Théry (Feb 28 2023 at 17:57):

you mean that?

``````Require Import List.
Import ListNotations.

Fixpoint all_same (l: list nat) : bool :=
match l  with
| nil => true
| [x] => true
| h1::((h2::t) as tl) => ((Nat.eqb h1 h2) && all_same tl)
end.

Definition f (l : list nat) : list nat := if all_same l then l else [].
``````

#### zohaze (Mar 12 2023 at 09:05):

When i apply it i get message "not truely recursive function" . Although results are ok but code get underlines and code color get change.

#### Pierre Castéran (Mar 12 2023 at 10:42):

You may have changed the `Definition` command into `Fixpoint`in the definition of `f`.

#### zohaze (Mar 12 2023 at 15:12):

Now i am getting both messages.
1)Not a truly recursive fixpoint.(Yellow color & underline)
2) Function where i use it recursively defined (guarded on 1st argument).but still underline .
3)when i unfold function where it is being used then fix before function name appears. Due to which i am unable to simplify it.

Last updated: Oct 04 2023 at 20:01 UTC