coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 :=
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 :=
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.PierreLe 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 HuguninOn 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
- [Coq-Club] : Lexicographic order well foundedness, Wendlasida Ouedraogo, 08/26/2021
- Re: [Coq-Club] : Lexicographic order well foundedness, Jasper Hugunin, 08/26/2021
- Re: [Coq-Club] : Lexicographic order well foundedness, Castéran Pierre, 08/26/2021
- Re: [Coq-Club] : Lexicographic order well foundedness, Wendlasida Ouedraogo, 08/26/2021
- Re: [Coq-Club] : Lexicographic order well foundedness, Castéran Pierre, 08/26/2021
- Re: [Coq-Club] : Lexicographic order well foundedness, Wendlasida Ouedraogo, 08/26/2021
- Re: [Coq-Club] : Lexicographic order well foundedness, Castéran Pierre, 08/26/2021
- Re: [Coq-Club] : Lexicographic order well foundedness, Jasper Hugunin, 08/26/2021
Archive powered by MHonArc 2.6.19+.