Why isn't plus_assoc rewriting correctly?
-
29-09-2020 - |
Pergunta
First I have plus_assoc
ready.
Theorem plus_assoc : forall n m p : nat,
n + (m + p) = (n + m) + p.
for simplicity we omit the proof of plus_assoc
.
now I want to prove plus_swap
:
Theorem plus_swap : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof. intros n m p. rewrite -> plus_assoc. ...
the equation was rewritten into n + m + p = m + ( n + p )
, rather than the expected (n + m) + p = m + (n + p)
. why?
Solução
It is rewriting correctly. Coq doesn't print redundant parentheses. The +
operator is left-associative, so n + m + p
is a valid way of writing the term (n + m) + p
, and Coq prints it without the parentheses.
Coq < Check (n + m) + p.
n + m + p
: nat
Just to be clear, n + m +p
and (n + m) + p
are exactly the same term, not just terms that are equal. They're different ways to use notations to write Nat.add (Nat.add n m)
.
Theorem plus_swap : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof.
intros n m p.
Unset Printing Notations.
Show. (* Now the goal is shown as: eq (Nat.add n (Nat.add m p)) (Nat.add m (Nat.add n p)) *)
rewrite -> plus_assoc. (* Now the goal is: eq (Nat.add (Nat.add n m) p) (Nat.add m (Nat.add n p)) *)
Licenciado em: CC-BY-SA com atribuição
Não afiliado a cs.stackexchange