coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] : Lexicographic order well foundedness

From: Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] : Lexicographic order well foundedness
Date: Thu, 26 Aug 2021 02:22:32 +0200
Authentication-results: mail2-smtp-roc.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-pl1-f169.google.com
Ironport-hdrordr: A9a23:E/EioKCJEbF1WGjlHemd55DYdb4zR+YMi2TDtnoedfUxSKalfq+V8MjzuSWVtN9pYgBEpTnYAtjlfZq+z/NICOsqUotKNTOO0ACVxedZnOjfKlXbakrDH4VmtJuIHZIOauHYPBxfgdzh6Ae1V+sx2dXvytHPudvj
Ironport-phdr: A9a23:rc0BARJ1PLvE6F4POdmcuLxmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvbM81RSUAs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipy+y+4ZnebxhHiDe9Y755MQm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lTbNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDwQLspWzqt8r1rRQfnhykHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTyxODZ26b4QSC+oOJ/1Yr4jgqFQUsBCwHBSsC/3yxT9SnHD22qI60+M8GgzB2wwgAswBv2nOrNrvM6cSXue1wLPUzTrddfNWxTb96JXTch06rvGMWKh/ccvVyUU1CwzFiVCQpJXjMjiI2esDr3KV4PB8VeKzlWEnsQdxryCry8kjhIfHiY0bx1PY+ShkwYs4O9+1RFNmbNK6EZZdtyOXOpdrTs0sQmxkpDo3xL0atZO1ciYHx5UqywLBZ/GHdYWD/xztVOGUIThihXJlfqqyiAyo8Uih1u38VtO40VhEridDj9LCtWgN2gTN5sSbTvZx5ESs1DaV2wzN9+1JLlo4mbfaJpMlxLM7i4Advl7ZHiDsnUX7lK+WeVsg+uiv8+nnZ6/ppp6YN4NtkgH+NrkiltWxAeglMwUDW3KX+eu71L3k8k35RKtFgucqnanetZDWPcUbpqinDA9Jyosv9QqzAjO83NkbnXQLNkxJdA+IgoTzJl3DIfT1Ae+6g1u2kTdrw/7GPqfmApXINnXDl6rhcqhg5E5G0gUzyt9f55VOBrEdPv3zQFPxtN3FDh8iKAG0zOPnB8981oMaQ26AHqiZMKbKvV+S+u0vO/WMZJMSuDvlN/cl4OfugWYlll8ZYKmmxoAaaGu4H/RjO0WWe2DggtYHEWcQvwoxVvbmiFOYUW0bW3HnVKUlozo/FYiODIHZR4nrjqbS8j28G8hpa2ZKDlmXEHvhP6KZVvsWYSWdJYc1lSEJWaKoTIAmkw2jrhP71qFPIe/d+ylevpXmgosmr9bPnA0/oGQnR/+W1HuAGjkcdoIgQjY32OVnpRU4xA7dgO53hPtXEdEV7PRMAF9S3Xv0wOlzCtS0UQXELI/hoLmOTdCvADV3RdU0kYZmXg==

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

[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