Stream: Coq users

Topic: ✔ Understanding a rewrite with `app_assoc_reverse`

Julin S (Dec 29 2021 at 16:57):

I found an example in CPDT book where a goal changed from

progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)

to

progDenote (compile e1 ++ (compile e2 ++ [iBinop b]) ++ p) s =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)

when rewriting was done with

rewrite app_assoc_reverse.

But I couldn't understand how app_assoc_reverse which looks like

app_assoc_reverse : forall (A : Type) (l m n : list A),
  (l ++ m) ++ n = l ++ m ++ n

was applicable here.

Rewriting from left to right with app_assoc_reverse was able to change progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) to progDenote (compile e1 ++ (compile e2 ++ [iBinop b]) ++ p).

But which parts of progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s correspond to the l, m and n in the (l ++ m) ++ n part of app_assoc_reverse?

Kenji Maillard (Dec 29 2021 at 17:00):

Isn't the instantiation l := compile e1, m := compile e2 ++ [iBinop b] and n := p ?

Paolo Giarrusso (Dec 29 2021 at 17:08):

makes sense, assuming ++ is right-associative (which this code implies); so compile e1 ++ compile e2 ++ [iBinop b] really parses as compile e1 ++ (compile e2 ++ [iBinop b]).

Julin S (Dec 29 2021 at 17:08):

But if l, m, n were like

((compile e1 ++ compile e2 ++ [iBinop b]) ++ p)
  |        |    |                      |     |
  +--------+    +----------------------+     +
      l                    m                 n

then it should've become just

(compile e1 ++ compile e2 ++ [iBinop b] ++ p)
 |        |    |                      |    |
 +--------+    +----------------------+    +
     l                    m                n

right?

Why did it become

(compile e1 ++ (compile e2 ++ [iBinop b]) ++ p)

with the extra set of parenthesis.

Julin S (Dec 29 2021 at 17:09):

Oh.. ++ being right associative makes sense.

Julin S (Dec 29 2021 at 17:11):

Wait, if it was right associative, it should've become

(compile e1 ++ (compile e2 ++ ([iBinop b] ++ p)))

right?

Kenji Maillard (Dec 29 2021 at 17:15):

(compile e1 ++ (compile e2 ++ ([iBinop b] ++ p))) is the same as (compile e1 ++ compile e2 ++ [iBinop b] ++ p), but both of these are different from what you actually obtain (compile e1 ++ (compile e2 ++ [iBinop b]) ++ p)

Julin S (Dec 29 2021 at 17:19):

But how is the (compile e1 ++ (compile e2 ++ [iBinop b]) ++ p) derived though? Is it not a straightforward replacement of the l, m, n into l ++ m ++ n?

Kenji Maillard (Dec 29 2021 at 17:19):

it is, keeping in mind that x is the same as (x) so l ++ m ++ n is the same thing as l ++ (m) ++ n

Paolo Giarrusso (Dec 29 2021 at 17:21):

Kenji's right, but you can also confirm that interactively by passing arguments to app_assoc_reverse

Paolo Giarrusso (Dec 29 2021 at 17:22):

e.g. rewrite (app_assoc_reverse (compile e1) (compile e2 ++ [iBinop b]) p)

Paolo Giarrusso (Dec 29 2021 at 17:25):

_or_ rewrite app_assoc_reverse with (l := compile e1) (m := compile e2 ++ [iBinop b]) (n := p)

Paolo Giarrusso (Dec 29 2021 at 17:25):

Set Printing Parentheses might also be useful during the exercise. Quoting https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:flag.Printing-Parentheses:

When this flag is on, parentheses are printed even if implied by associativity and precedence. Default is off.

Julin S (Dec 29 2021 at 17:36):

Oh, okay. The extra pair of parenthesis came as the m itself is a concatenation (compile e2 ++ [iBinop b]).

Also, hadn't used that with syntax before.

Thanks!

Notification Bot (Dec 29 2021 at 17:36):

Ju-sh has marked this topic as resolved.

Last updated: Oct 01 2023 at 18:01 UTC