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: Oct 13 2024 at 01:02 UTC