coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] weird rewriting results

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] weird rewriting results
Date: Tue, 15 Jan 2019 06:07:45 +0000
Accept-language: en-US
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-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:vf7LAhTJGu02mB5K+E47ZDxplNpsv+yvbD5Q0YIujvd0So/mwa6yYxaN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpx1jzIDbb46YL+Z+cbjHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5coYbjvVsBsx6+BAmxD+3h0DBJiGT23ao80+88FgzI2BIvH8gQv3TRrNT5LqkcXvq7zanTyjXDaehb1i376IjVaBwuv+yDXa9qfcXL1EkiDgXIhUiTp4z9Jz6Y2fgBv3KG4+Z8V++jkXMrpg9wrzS128sglonEipoIxl3E6Sl12pg5KcG2RUJhf9KoDYdcuzuHO4Z4Rs4uW29otzg5x7EavJO2eSkHxIglyhPfbvGKd4aI7xbtWeuUJTp0mW9qdK66ihms6kev1uP8W8+p21hQtCVFiMPDtnUV2hzT9MeHTvx981+91DmByg7f9vxILVkzm6TUNpIt27kwmYENvkjZGS/2hVn2g7SRdkU5/Oin9v7rYq38pp+bK497lB3xMrgvmsy4B+Q0KA8OX3WH+eS4073j+k75TK9Wgf0xl6nVqJHaJcIFqa6lGwJY3Zov5wyiAzu60tkUh2QLIVxEdR6dkoTlJ1HDLOj9DfilglSslDlrx+rBPr3kGpjDKmbMkK3/crZ4609Q0gQ9wspR5pJPDbEBJun+VVX3tNzFFBM2LRG7w/v9BNpny4MSQXiPDbOBMKPOrV+I4foiLPWLZI8MoTryN/wl5+P1gnIigl8cfayp3YMNZ3yiH/RmJV+ZYXv2jdsbH2cKpFl2cOu/wlaFSHtYY2u4d6M6/DAyToy8R8+XTYe0xbeFwS2TH5tMZ2kABEraQlnycIDRefoWZSeDauNojScDU/D1aYI72BS/8iPz1KFgKMLd/DBeuJ7+ktFosb6A3Sou/CB5WpzOm1qGSHt5yztRFm0GmZtnqEk48W+tlK1xgvhWD9tWvqkbWwEnc5PQ0qpzFoKrA16TTpKyUF+jB+6eL3QpVNtomY0HZVs7Ftm/yBnejXLzXu0l0oeTDZlxyZrymnj8I8EhlCTv6ZJ51hwDb5IKMmerwKli6wLUGojF1V2DkLqnfrgd2yiL83qfyW2JvwdTVwsiCKg=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi,

with a goal

(?Γ1 ++ ?Γ2) ++ ?Q :: ?Γ3 = Γ1 ++ Γ2 ++ (Q :: sel3) ++ l1 ++ Φ2

applying the tactic

rewrite app_assoc_cons.

gives the new goal

(?Γ1 ++ ?Γ2) ++ ?Q :: ?Γ3 =
(Γ1 ++ Γ2) ++
Q
:: (fix app (l3 m : list (PropF V)) {struct l3} :
list (PropF V) :=
match l3 with
| [] => m
| a :: l4 => a :: app l4 m
end) sel3 (l1 ++ Φ2)

This is where app_assoc_cons is

Check app_assoc_cons.
app_assoc_cons
: forall (A : Type) (l m : list A) (x : A) (xs : list A),
l ++ m ++ x :: xs = (l ++ m) ++ x :: xs

and is using the version of rewrite obtained from

Require Import ssreflect.

What is happening here?

Thanks

Jeremy

[Coq-Club] weird rewriting results, Jeremy Dawson, 01/15/2019
- Re: [Coq-Club] weird rewriting results, Laurent Thery, 01/15/2019
  - Re: [Coq-Club] weird rewriting results, Jeremy Dawson, 01/22/2019
    - Re: [Coq-Club] weird rewriting results, Laurent Thery, 01/22/2019