coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to prove two records equal

From: Suneel Sarswat <suneel.sarswat AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] How to prove two records equal
Date: Wed, 18 Aug 2021 17:15:55 +0530
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=suneel.sarswat AT gmail.com; spf=Pass smtp.mailfrom=suneel.sarswat AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f182.google.com
Ironport-hdrordr: A9a23:yGh/O65RyL7W6IMQbwPXwMXXdLJyesId70hD6qkRc20zTiX8raqTdZsgpHzJYVoqOE3I+urgBEDjewK/yXcd2+B4VotKNzOW3VdAQrsSibcKAAeNJ8Q9zINgPGtbHJSWweefMWRH
Ironport-phdr: A9a23:VhypKxa0JQMTx6ku2sfwqwn/LTHM0IqcDmcuAnoPtbtCf+yZ8oj4OwSHvLMx1gePDNyQtq0MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5YHfbx9MiTagbr9/LBe7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+TbxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8qVlRwLyiCofODE38G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5uhYYsSCeoOI/hXr43grFUTtxS+HxKsBe31xT9Um3T72rY60/knEQ7YwgMgG8gCsG/Oo9XvL6cTX/q6zLXTwDXMavNZwzb96IzSfh89pvGMWKt9fMzMwkYgCw3LlE+fqZD5PzyLzOQNtXCW4eRuW++rj2Mqtxx9ryWty8sxioTHiY0Yx1Ta+ClnwIg7KtK2RUplbdOqEpZduC+XOYt1T88/TG9mtiY3xqMCtJO9YSMEy4wnygbBZ/Cbd4WE+BHuWeaLLTtmmX5ofKiziwux/ES+zOD3S9O630xQriVfl9nBrnAN2ALX6siAUvZ9+12u2TeL1wzK6uBLOl04mbPVK5I8wbM8iIAfsUvEHi/xl0X2iLGZel849eiv7uTrerTmppmCOI9okgzyLLgil8ilDek7MgUCRXaX9fm42bH54EH0Q6tGguUzkqbDsZDaIcobprS+Aw9Qyosj8Au/DzG439sGmXkLNklFdwidj4jyNVDBOuz4AOywg1SpijhrxvTGMqf9DZXKK3jPiK3hcqpl605A1AozyshS6I5TCrEYOf78RkvxtMHDARIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvObrEWIhAszHkbvMh+vSm2XQ+gBoWebSj9ZoRcnGxWPp8dRa3e33p1+wcF2oHukIFRfbxl1SeGWpIenC/UqZ6/TghE52vEa/MQ4mshPqK2yLtTc4eXXxPFl3ZSSSgTI6DQfpZMEp6zedulzUFUf6qTIpzjHlGUSf1zrNmKqzf/ShK7foLNfBw7uzX0AA4rHl6VpTHlW6KSG5wkyUDQDpkhMhC

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