Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] : Lexicographic order well foundedness

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] : Lexicographic order well foundedness


Chronological Thread 
  • From: Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] : Lexicographic order well foundedness
  • Date: Thu, 26 Aug 2021 10:56:47 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ouedraogo.tertius AT gmail.com; spf=Pass smtp.mailfrom=ouedraogo.tertius AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg1-f172.google.com
  • Ironport-hdrordr: A9a23:sGAsQapQtCqM6v4UdIw76T0aV5ogeYIsimQD101hICG9vPb4qynIppQmPH7P4wr5N0tPpTntAsW9qDbnmqKdn7NhXotKLTONhILAFugL0WKh+UyDJ8SUzINgPMlbAs1D4aXLfDxHsfo=
  • Ironport-phdr: A9a23:45VcJRMcLqQR+Z5vzFkl6nbaDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv60r3QaCANqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yfy+94fXbglVizawYbF/JwiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjULxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4LpxSBLwhygHOTw2/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kb4QAEewBMvtcr4bnvFsOrAaxChOxD+321z9HmGL53bcg3OQmHgHG2xErEtUJsHTJstr6Kb0SXvqyzKnHyjXPde9W1inn6IjUcxAhvOqMUKl/ccrU00YvFgfFgk+MpoziOjOYz+IAuHWU4OR8T+ygkXInqx1vrTi1wMchkofHi4YXx1zZ+yt13oY7KMO2RkB1fNOqEJVduiGZOoZrXM4vTX9ktSQnx7AIp5O2czYHxZcmyhPed/GKb4aG7xzlWe2MLzl4g3dld6i+hxa06UWv0Pf8Vsio0FZKtCZEnNfMu3YQ3BLQ8siKUuVx8lul1DqV1A3e6vtILV4pmafbMZIt37w9moQVvE/eBCH5gl/2g7WTdkg8+uin9eDnYrL+q5+ZLYB0iwX+Pr02msywHOg0KwYOU3WZ9OiizrHj8kr5QLJFjv0yjKbVqozVJcMepqKhAg9V1Jgs6wqnAju4zNgVmWMLIVFFdR6dkYTlJlHDLOrlAfq9nVigiDJryOrHPr3lDJXNNH/DkLL5cLZ69k5T1hc8zcpF6JJTBbEBJ+j/WlPvu9zCEh85MhG0w/38BdVy04MRQ2OPAquDPKzOtl+I4/ojI/OQa48NpDb9N/8l6ubygn8+gF8RZLWm3Z8KaH+jBflmOEWYYX/0gtgbC2sKvww+TPbriFKYSzJTaWyyDOoA4WQwD5vjBoPeTKishqaA1WG1BM54fGdDX2+BF3vsfp6FV/5ETz+fLtVolTMDHeymVoItzxipuwi817d9MuvJ4QUXsJvi0J5+4OiFxkJ6ziB9E8nIizLFdGpzhG5dH1fePYh6qE15j0+MiO122qMCU9NU4PxNX0ExMpuOl4SS5Pj9XwvAepGCT1P0G71O5Bk+S9swx5kFZEMvQ72f

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                                                                  



Archive powered by MHonArc 2.6.19+.

Top of Page