The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Hi,

  You will probably have to require also Relations.Operators_Properties (where well-roundedness of the lexicographic product of two wfs is proved).

  AFAIK, Relation_Operators defines the lexicographic product as a relation on dependent pairs. If you are not familiar with this kind of data, it may be useful to work with a simpler definition (i.e. of type relation (A * B).  If you are interested, I may send you such definitions.

Pierre

Le 26 août 2021 à 02:49, Jasper Hugunin <jasper AT hugunin.net> a écrit :

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