coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove two records equal

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to prove two records equal
Date: Wed, 18 Aug 2021 13:55:30 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay11.mail.gandi.net
Ironport-hdrordr: A9a23:Kkhrva7H1UDRrsmn8wPXwMXXdLJyesId70hD6qkDc20wTiX+rbHIoB17726QtN9/YhAdcLy7V5VoBEmsl6KdgrNhXotKPjOJhILAFugLhrcKgQeNJ8SUzIRgPMlbHpSWROeRMWRH
Ironport-phdr: A9a23:FXWYFBPeJJOK+6je7ZIl6nb4DRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv60r3QaCANqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yfy+94fXbglVizawYbF/JwiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjULxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4LpxSBLwlSkJKTA5/mHUhMJ+gq1UrxCuqABwzYPPfIGYN+Bzcr/Bcd4UR2dMWNtaWSxbAoO7aosCF+sPMvxEqInhvVQOqwOxCwitBOPr0TBHmGX23bEn2OkmHgHJxhIvH84Uv3TSttn1O6YSUeSuw6bW1zXDc+hb2Sz+6InIaRAhovCMXbd1ccXP00kjDQXFgUuMqYH8OT6ey+sCvXSB4eV6SeKvl3Aoqxt3ojW3xskhjpTEipwIx17L9ih0w5s5KNykREN/btOpDJRduiWZOoZoTc0vQH9ltig7x7AbtpO2ficExZA6yxPBaPGJfI6F6Q/gWuaJOTp0mm9pdbClixuw7USs0PDwW8u33VpQsCZInMTAu3YQ3BLJ8MeHUOFy/kK51DaPyQ/T7uZELFgulaXFL54u2L4xmocOvUjZGy/5gkT2jKuMekUr4Oeo7fnoYrT8qp+aKYB0lhnyMqUomsOhHeQ1KhYCU3WZ9Oim1rDv4Vf1TKhIg/A1iKXVrp7XKdkDqq68GQBV04Ij6xilDzeh1dQVhXYHI0hbdxKblYfpPUvCIP/5Dfe7mFujji1rx+zdM736AZXMLmPDkLTgfbZ47k5T1hAzwcpZ551KFrENOOjzVVPptNzEEh85NBS5zPrgCNVkz48RRWaPArKCP67Jql+J5ucvI/GWa4MPuTb9LeIl5//0gnMjl18dZ/rh4ZxCY3ehW/9iPk+xYHz2g95HH31ZkBA5SbnFgd6eWDhkSHe2Va8m+nlvB4urEY7FAI+shLaMxjuTBZ5HfWNHD1WBCzHuepnSCKREUz6bPsI0ym9MbrOmUYJ0jXlGWyfhyKt8LevR/yAC85TuyIosjwU2vQox5Cd3DsGY3nvLSWxozDtgr94exq17qF0kkxGG2Kl8xfNRE9BSofVETlViXaM=

You can prove

Require Import Eqdep_dec.

Lemma mkr_eq a b e e' (H:a = b) : mkr a e = mkr b e'.
Proof.
destruct H.
f_equal. apply eq_proofs_unicity.
decide equality.
Qed.

then just apply the lemma

Gaëtan Gilbert

On 18/08/2021 13:45, Suneel Sarswat wrote:

Dear all,
I have the following record type.
*Record r:Type:= mkr {t:nat; cond: Nat.ltb t 1= false}.
*

Now I have the following goal:

*{|
t := x;
cond := Morphisms.iff_flip_impl_subrelation ((x <? 1) = false) (~ x < 1)
(Nat.ltb_nlt (x) 1) n |} *
*=
{|
t := x;
cond := cond0 |}*

In hypothesis I have :
*n : ~ x < 1
cond0 : (x <? 1) = false*

How do I prove such a goal? Thanks in advance.
Regards,
Suneel.

[Coq-Club] How to prove two records equal, Suneel Sarswat, 08/18/2021
- Re: [Coq-Club] How to prove two records equal, Gaëtan Gilbert, 08/18/2021