coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] effects of revert

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] effects of revert
Date: Tue, 1 Dec 2020 10:06:07 +0100
Authentication-results: mail3-smtp-sop.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 relay6-d.mail.gandi.net
Ironport-phdr: 9a23:3JrKix2qtqWtO7vPsmDT+DRfVm0co7zxezQtwd8ZseIeKPad9pjvdHbS+e9qxAeQG9mCtLQd1bOd4/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalvIBi3sAnducobjZd/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+kbxVoByhqRJ8zYDbbo6aO/hica3SZt4aWWlMU9xNWyBdDI6xbY0CBPcBM+ZCqIn9okMDoxqkCg6wGOPg0DlIiWf306071+QuCh/J3BY8H9kTt3nUo8/6O7kOUe+vyqnE1zrDb/JS2Tjm9ofIaAwhrOqXXbJzccvR0kovFwLAjlWVt4PlJSmZ1uITvGiH9udtU/+khGE7pQ9ruDev2tsshZfThoIT0l3K9SF0zZsrKdClR0B2Yt2pHIZRui2GM4Z7Td8vTm5stSs51LAItp22cTYExpkm2hPSZP6KfYeM7x7+SuucIjh2iXR4c7y8nxa/6VasxvD+W8Wu0ltGsjBJnsTPu30DzRDf98yKR/hl8ku81zuC2Brf5vxALEwuiKbWKZoszqQtmpcSv0nOGDL9ll/sg6+MbEok//Cl6+T5bbXioZ+RL5V0hR/6Mqs0ms2yAP00PRUUU2ie4+u81bnj8Vf2QLpQiP05j6jZvIrcJcsFuq61Gw5V0oA95BajFzqqzskUkHsdIF9HZB6LlZXlNlLALfziEPuyh1ehnC9ux//cP73hBpvNLmLEkLfkZbt95FRTxxQvzd9F4ZJYEL4BIPP3WkDqqtPYFAM5Phevw+bkCNR9zYAeWWOKAq+cLqzSq0WE5uQxLOmQfIMVoiryK+A55/7yin80gUMSfa6w3ZcOdH+4GulmLF6CbHr3gtYBFH8KsRAkQOzrjl2CSz9TaGyoU6Iy/DFoQL6hWIzEX8WmhKGL9Ca9BJxfIG5cWX6WFnK9WIwHR/4KXw2TJsVsiCBMAbeoRpMo01ehtQvwxqB7BvHX6zYbtJfm2cIz4eDPw0JhvQdoBtiQhjneB1p/mXkFEmdvgPJP5Hdlw1LG6pBWxuRCHIUNtehKQxw5NJvZwvY8Dd3uCFqYI4W5DW2+S9DjOgkfC9I8x9hUPhRnFtGrn06G02yvCr4R0bOCApA1tKTRwyqpfpcv+zP9zKAkymIebI5KPGyiiLR48lGNVZXKgl6alqOveL5a2iPRpj6O

clearbody m; revert m
should produce what you want

Information is not thrown away, "pose (m := ms_ordI f (Γ1 ++ G1) (G2 ++ Γ2) c
X)" will put you back at your starting point

Gaëtan Gilbert

On 01/12/2020 07:40, Jeremy Dawson wrote:

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