## Stream: Coq users

### Topic: Fixpoint to test if a list is ordered

#### Roberto Cebulski (Dec 14 2022 at 00:05):

Hello, i'm trying to define a fixpoint to get a proposition if a list of real numbers is ordered but im getting an error saying that the recursive definition is ill-formed. Could someone shed some light? Thanks.

Fixpoint isordered (lr: list R) :Prop:=
match lr with
|nil => False
|h :: (h' :: t) => (h < h') /\ (isordered (h' :: t))
|h :: nil => True
end.

Error:
Recursive definition of isordered is ill-formed.
In environment
isordered : list R -> Prop
lr : list R
h : R
l : list R
h' : R
t : list R
Recursive call to isordered has principal argument equal to
"h' :: t" instead of one of the following variables:
"l" "t".
Recursive definition is:
"fun lr : list R =>
match lr with
| nil => False
| h :: nil => True
| h :: h' :: t => h < h' /\ isordered (h' :: t)
end".

Edit: XD Forget it. I got it.
Fixpoint isordered (lr: list R) :Prop:=
match lr with
|nil => False
|h :: t => match t with
|h' :: t' => (h < h') /\ isordered t
|nil => True
end
end.

#### Dominique Larchey-Wendling (Dec 14 2022 at 06:42):

Notice that `h'::t` is not as subterm of `_::h'::t` ... destructing then reconstructing does not pass the guard checker.
Here is a possible work arround.

Alternatively, you could also define `isordered` as an inductive predicate.

Best,

D.

``````Require Import List.

Parameters (X : Type) (R : X -> X -> Prop).

Fixpoint isordered (lr: list X) :Prop:=
match lr with
|nil => False
|h :: ((h' :: t) as l) => (R h h') /\ (isordered l)
|h :: nil => True
end.
``````

#### Pierre Castéran (Dec 14 2022 at 07:14):

Just a remark. You may say that the empty list is ordered (consistent with Stdlib, allowing to prove that the tail of an ordered list is ordered).

``````Fixpoint isordered (lr: list X) :Prop:=
match lr with
|nil | h :: nil => True
|h :: ((h' :: t) as l) => (R h h') /\ (isordered l)
end.
``````

#### Guillaume Melquiond (Dec 14 2022 at 07:51):

Also, it usually makes for much simpler proofs to use an auxiliary definition:

``````Fixpoint isordered' (h: X) (lr: list X) :=
match lr with
| nil => True
| h' :: l => R h h' /\ isordered' h' l
end.

Definition isordered (lr: list X)  :=
match lr with
| nil => True (* or False, depending on what you want *)
| h :: l => isordered' h l
end.
``````

#### Roberto Cebulski (Dec 14 2022 at 14:41):

Thanks for the tips guys.

Last updated: Jun 16 2024 at 02:41 UTC