The Coq mailing list

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

Hi,

Here is a file which defines a simple lexicographic product (on non-dependent pairs) with a proof of well foundedness.

Example of use:

Example Ex1 : lexico lt lt (3,5) (4,2).

left;auto.

Qed.

Example Ex2 : lexico lt lt (3,5) (3,6).

right;auto.

Qed.

Best regards,

Pierre

 https://github.com/coq-community/hydra-battles/blob/master/theories/ordinals/Prelude/Simple_LexProd.v

Le 26 août 2021 à 10:56, Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com> a écrit :

Hi,

l am not familiar with this kind of data. 

lexicographic product is defined as :

Section Lexicographic_Product.

  Variable A : Type.
  Variable B : A -> Type.
  Variable leA : A -> A -> Prop.
  Variable leB : forall x:A, B x -> B x -> Prop.

  Inductive lexprod : sigT B -> sigT B -> Prop :=

...

But what I need would be like:

Section Lexicographic_Product.

Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop.
  Variable leB : B -> B -> Prop.

  Inductive lexprod : A * B -> A * B -> Prop :=

...

like in symprod but with left_sym : forall x x':A, leA x x' -> forall y y':B, symprod (x, y) (x', y'). 

Can you send me an example with lexprod and/or is there a library with a simpler definition (relation (A * B)) with well foundedness proof?

Thank you for your answers.

Le jeu. 26 août 2021 à 08:50, Castéran Pierre <pierre.casteran AT gmail.com> a écrit :

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                                                        

--

Cordialement,

M. Wendlasida Tertius OUEDRAOGO

Mobile : 0751061208