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.eqbwith Nat.ltb, you can implement a function which returns lif 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 Fixpointin 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