Wie zu beiden Seiten einer Gleichheit in Coq

Question

hinzufügen Dies scheint wie eine wirklich einfache Frage, aber ich konnte nichts nützliches finden.

ich habe die Erklärung

n - x = n 

und möchte

(n - x) + x = n + x 

ich beweisen nicht in der Lage zu finden, was Theorem dies zulässt.

Answer 1

Sie sollten sich die Taktik rewrite ansehen (und dann vielleicht reflexivity).

EDIT: weitere Informationen über Rewrite:

• Sie können rewrite Hrewrite -> H zu nach rechts
• links umschreiben können Sie rewrite <- H von rechts neu zu schreiben

• Sie können nach links verwenden, um die pattern Taktik Wählen Sie nur bestimmte Instanzen des Ziels neu zu schreiben. Zum Beispiel, um die zweite n nur zu umschreiben, können Sie die folgenden Schritte

  Muster durchführen n bei 2. Rewrite < - H.

In Ihrem Fall ist die Lösung viel einfacher.

Answer 2

Es gibt eine leistungsstarke Suchmaschine in Coq mit Mustern. Sie können zum Beispiel versuchen:

Search (_=_ -> _+_=_+_). 

Answer 3

Aufbauend auf @gallais' Vorschlag auf f_equal verwenden. Wir beginnen in dem folgenden Zustand:

n : nat 
x : nat 
H : n - x = n 
============================ 
n - x + x = n + x 

(1) Erste Variante über "vorwärts" Argumentation mit dem f_equal Lemma (wo man Theoreme Hypothesen gelten).

Check f_equal. 
f_equal 
: forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y 

es die Funktion f benötigt, so

apply f_equal with (f := fun t => t + x) in H. 

Dies gibt Ihnen:

H : n - x + x = n + x 

Dies kann über apply H. oder exact H. oder assumption. oder auto. ... oder einige gelöst werden eine andere Art, die Ihnen am meisten zusagt.

(2) Oder Sie können "rückwärts" Argumentation verwenden (wo man Sätze auf das Ziel anwendet). Es gibt auch die f_equal2 Lemma:

Check f_equal2. 
f_equal2 
: forall (A1 A2 B : Type) (f : A1 -> A2 -> B) 
    (x1 y1 : A1) (x2 y2 : A2), 
    x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 

Wir haben es nur auf das Ziel anzuwenden, die in zwei trivialen subgoals führt.

apply f_equal2. assumption. reflexivity. 

oder nur

apply f_equal2; trivial. 

(3) Es besteht auch die speziellere Lemma f_equal2_plus:

Check f_equal2_plus. 
(* 
f_equal2_plus 
    : forall x1 y1 x2 y2 : nat, 
    x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 
*) 

Mit diesem Lemma können wir das Ziel, mit dem folgenden lösen Einstrich:

apply (f_equal2_plus _ _ _ _ H eq_refl).