¿No se puede reescribir el objetivo con una afirmación?
No estoy seguro de entender por qué en algunos casos reescribir H funciona y en otros no.
Aquí, por ejemplo:
“`
Teorema add_assoc2 : forall n m: nat, n + m = m + n.
Proof. intros. rewrite add_comm. reflexivity. Qed.
Teorema plus_4: forall n m p q: nat,
n + (n * p) + m + (m * p) = n + m + (n * p) + (m * p).
Proof.
intros.
assert (H: n * p + m = m + n * p).
{ rewrite <- add_assoc2. reflexivity. }
rewrite H.
<code>
Obtenemos:
</code>
1 objetivo
n, m, p, q : nat
H : n * p + m = m + n * p
<strong><em>_</em><em>_</em><em>_</em><em>_</em><em>_</em><em>_</em><em>_</em><em>_</em><em>_</em><em>_</em><em>_</em>_</strong>(1/1)
n + n * p + m + m * p = n + m + n * p + m * p
“`
Pero Coq se queja: Found no subterm matching "n * p + m" in the current goal.
¿Por qué?
Claramente veo uno en el lado izquierdo. Al usar inducción, reescribir con IHn no plantea ningún problema, incluso si hay otros términos delante de la expresión reescribible.
davy.ai
En el ejemplo dado, el término
n*p + mse puede encontrar en el lado derecho de la ecuaciónm + n*pen la hipótesisH. Sin embargo, al intentar reescribir este término usandoH, Coq busca el subtérmino exacton*p + men la meta. Este subtérmino exacto no se puede encontrar en la meta, ya que se expresa comon + n*p + m + m*p.En los casos en los que la reescritura funciona, es porque el subtérmino específico que se está reescribiendo se encuentra exactamente como está en la meta, o porque las reglas de reescritura utilizadas pueden coincidir y simplificar el término en múltiples pasos hasta que coincida eventualmente con el subtérmino.
Cuando se utiliza la inducción, la reescritura con
IHnpuede no ser un problema porque la hipótesis de inducción es una ecuación explícita que coincide exactamente con un subtérmino, y se puede utilizar para reescribir la meta por sustitución. Además, la hipótesis de inducción ya es una afirmación comprobada, mientras que la hipótesisHen el ejemplo dado es simplemente una suposición que aún no ha sido probada.