Stream: Coq users

Topic: [noob] isSorted not working as expected

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?

Kenji Maillard (Jul 10 2021 at 10:35):

Is the error Cannot guess decreasing argument of fix ?

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.

leafGecko (Jul 10 2021 at 10:38):

That indeed solved the problem. Thanks!

Last updated: Apr 19 2024 at 04:02 UTC