Stream: Coq users

Topic: [noob] isSorted not working as expected


view this post on Zulip leafGecko (Jul 10 2021 at 10:32):

Fixpoint isSorted (l: list nat): bool :=
  match l with
  | nil => true
  | x :: nil => true
  | x1 :: x2 :: xs => if x1 <=? x2 then isSorted (x2 :: xs) else false
end.

the code throws error around isSorted (x2 :: xs). Why?

view this post on Zulip Kenji Maillard (Jul 10 2021 at 10:35):

Is the error Cannot guess decreasing argument of fix ?

view this post on Zulip Ana de Almeida Borges (Jul 10 2021 at 10:35):

Even though it is clear for us that x2 :: xs is a subterm of x1 :: x2 :: xs, this is not clear for Coq. Here is how you can make it clear:

Fixpoint isSorted (l: list nat): bool :=
  match l with
  | nil => true
  | x :: nil => true
  | x1 :: (x2 :: xs) as x2xs => if x1 <=? x2 then isSorted x2xs else false
end.

view this post on Zulip leafGecko (Jul 10 2021 at 10:38):

That indeed solved the problem. Thanks!


Last updated: Feb 01 2023 at 13:03 UTC