The Coq mailing list

[Jasper Hugunin <jasper AT hugunin.net>]

The simple answer is that you want lexprod (Lexicographic order) rather than symprod (Symmetric product), defined in Relations.Relation_Operators.

lexprod has the definition you expect.

Best,

- Jasper Hugunin

On Wed, Aug 25, 2021 at 5:22 PM Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com> wrote:

Dear List, I am trying to write some functions in coq whose termination proofs use lexicographic order. My minimized problem is :

-------------------------

Require Import FunInd.
Require Import Recdef Coq.Arith.Wf_nat ZArith Coq.ZArith.Zwf Omega.
Require Import Relations.Relation_Operators.

Function test (x: string * nat) {wf (symprod string nat (ltof string length) (ltof nat (fun id => id)) ) x} :=
match x with
| (EmptyString, 0) => 0
| (EmptyString, S n) => test (EmptyString, n)
| ((String a s), n) => test (s, n + 1)
end.

---------------

I cannot prove that the function terminates. It seems that the problem is due to the fact that in Relations.Relation_Operators.v, symprod is defined like following:

Inductive symprod : A * B -> A * B -> Prop :=
| left_sym :
  forall x x':A, leA x x' -> forall y:B, symprod (x, y) (x', y)
| right_sym :
  forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y').

instead of :

Inductive symprod : A * B -> A * B -> Prop :=
| left_sym :
  forall x x':A, leA x x' -> forall y y':B, symprod (x, y) (x', y')
| right_sym :
  forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y').

-------------------

Any ideas ? 

--

Regards,

M. Wendlasida OUEDRAOGO