coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] effects of revert

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] effects of revert
Date: Tue, 1 Dec 2020 17:40:25 +1100
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=VoHv8ghWo8RI7gab5lU9totif8LOuFLvlq6pSJjnMMw=; b=S/NFgf4OKypWu7OUFj3D/YwKD9GdfhxcZylTUB3aaItOAuCZDbcvjVJlXnl0PDRC4FiO4X+lLgebnVmGB3pYq8Jbm8z/Wyu+Ip47SHUPK9UiQ1Xb2mhA+Z282aExQ1MjsDvLBe3Ci3GM06QH9nTHPgIDqKqjrAv+JpW9dcQK5N0LhZhMbQFeHT1dWB2kpwsOLG6czvBu3YtJzOBsuYApc2HZ3dUT5Wedo4Yz2cQQ4cmWOqNjsmUO43pR31KiWQApDdY+8k0+jF89uKbLHkzcqNwOm/5z4ntAXoVpVux8Mq45OuBgMOWL8Li3X2k8O4Rgq6t6sGxkK6bZ/ArwOQ/0/Q==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=PAiGMozDNZvciGnsKvLEmgCXf4hAoHuldyd0nflFsKz1xJTb5zE7B8Qhymrw4Fe4SDEsHBMAD8N2ElfHjhan427CNDQdJBd19EOXfAOhq+rE812Y9ELADUf0SIbSmDXTngXtiV8vO0V13RWCbtQPXR4CtgK/Eu79IhVw7m6T8AR72+xMm6+dZ0wZ0MRBe2ikpSJe6L2WdZp2H408WJxU1FEcdt/UroseYsyQg3bny/0wKLsV8ldKmMqqju2lT/AmIFrkrMSiqpzc209az8elALyyKLRsyFZd4cya/k3xdTlEZOwALXRwBJIqQbdJXu4dBIkp6IzFplIQwNKXnffl5Q==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:NlM+5ha5Dm9yV5+dLa8yJhH/LSx+4OfEezUN459isYplN5qZrs24bnLW6fgltlLVR4KTs6sC17OJ9fm+ACdQud6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6txjdu8gLjYdtKas91gbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRy/pxJx3o3abo+bO/Vica3dfNwVSHFdXstSTSFNHp+wYoUNAucHIO1Wr5P9p1wLrRamAQejGvnvxSFNhn72wKY03f4uEA/d3AwnGdIFrXPZotHrO6cIT++1yanJwS/NYfxM1zb984/IchY6rP6WW7JwbNDdxlcyGAPYlFmfs5HlMiqT2+8QvGeV8/BuWvizi247tQ5xuD6vy98oh4fJmo8YxV7K+Cp2zYs6K9C0VVB2bMK6HJZStyyXM4p7TMwjTmxnuCg3yKMLtJ25cSYFypkqxBDRZvyafoaH5B/oSeWfIS9giX9qZL6znQu+/VSix+HmS8W4zFVHojBBn9XRrnwA2Bje5tKaRvZ+4kutwzaC2g/J5u1aPUw4i6zWIIM7zLEqjJocq0HDEzf2mEroiK+WcV0p9/Sm5Or6frnqu4aQOYh7hAzwK6gundewDvoiPggJQmib5f+z1Lr+/U3/XbpGlOU2krPesJDGO8sUurK5Aw5S0oYl8Rq/CCqm0MgcnXkAK1JFewiLgJTuO1HLOPz4DPG/jEqwkDpzyP3KIqftDojRInXBirvtYKpx5k1GxAc30NxT/5dUBasAIPL3VE/xrtvYDhohPgKw3ennEsty1oYeWG6VDKGWKq3TsUSP5uIpOOSDfokVuCvnJ/c7+vHukGU1lkUAfaWxx5sYdGi4Huh6I0WeeXfjntABEX4TsgUiSOzqlUaNXCVIZ3eyWqI8/is0BJinDYfFXICtgaaO0D21Hp1MNSh6DQXGGnDxMo6ARv0kaSSII8YnnCZOHeyqTJZk3hWzvif7zaBmJ6za4HtLm4jk0Y1X6vfekAB62TVrFMObmzWvQnt5m3JOazYpx6d5iUV71xGO3bU+iuEORo8b3O9ATgpvbc2U9Od9Ed2nAludLOfMc06vR5CdOR90Vsg4moVcakBgXdiuk1bKwnjyWuJHp/mwHJUxt5nk8T3xKsJ6lymU/ZQa1wBjZ+YUcGqsi+h46hTZAJPPnwOBjaG2eK8A3SnLsmCe0W6Ju0IeWwl1A/ycDCIvI3DOpNG83XvsCrqnCLApKAxEkJTQI61XLNDlkBNPWaW6NQ==

Hi,

Doing a proof, from here

H : G1 ++ c :: G2 = c1 :: c0
m := ms_ordI f (Γ1 ++ G1) (G2 ++ Γ2) c X
: ms_ord f ((Γ1 ++ G1) ++ ps ++ G2 ++ Γ2) ((Γ1 ++ G1) ++ c :: G2 ++ Γ2)
============================
ms_ord f (Γ1 ++ (G1 ++ ps ++ G2) ++ Γ2) (Γ1 ++ (G1 ++ c :: G2) ++ Γ2)

when I do
revert H.

it gives as the goal
G1 ++ c :: G2 = c1 :: c0 ->
ms_ord f (Γ1 ++ (G1 ++ ps ++ G2) ++ Γ2) (Γ1 ++ (G1 ++ c :: G2) ++ Γ2)

but when I do
revert m.

it gives
let m := ms_ordI f (Γ1 ++ G1) (G2 ++ Γ2) c X in
ms_ord f (Γ1 ++ (G1 ++ ps ++ G2) ++ Γ2) (Γ1 ++ (G1 ++ c :: G2) ++ Γ2)

What I want is
ms_ord f ((Γ1 ++ G1) ++ ps ++ G2 ++ Γ2) ((Γ1 ++ G1) ++ c :: G2 ++ Γ2) ->
ms_ord f (Γ1 ++ (G1 ++ ps ++ G2) ++ Γ2) (Γ1 ++ (G1 ++ c :: G2) ++ Γ2)

How do I get that, and why does revert do something different.

Further if after
revert m.
I do
simpl.
it just deletes m so the information that
ms_ord f ((Γ1 ++ G1) ++ ps ++ G2 ++ Γ2) ((Γ1 ++ G1) ++ c :: G2 ++ Γ2)

It seems odd that a tactic called "simpl" should throw away information, so as to make the goal unprovable.

Cheers,

Jeremy

[Coq-Club] effects of revert, Jeremy Dawson, 12/01/2020
- Re: [Coq-Club] effects of revert, Gaëtan Gilbert, 12/01/2020