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.

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.
```

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.
```

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.
```

Thanks for the tips guys.

Last updated: Oct 04 2023 at 23:01 UTC