6
In Coq, ist es irgendwie möglich, ein Lemma oder Hypothese auf einen Teilausdruck des aktuellen Ziels anzuwenden? Ich möchte zum Beispiel die Tatsache anwenden, dass Plus kommutativ ist, um in diesem Beispiel 3 und 4 zu tauschen.Wie Umschreiben auf einen Unterausdruck des aktuellen Ziels
Require Import Coq.Arith.Plus.
Inductive foobar : nat -> Prop :=
| foob : forall n:nat, foobar n.
Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)
gibt:
Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".
Wie kann ich coq, wo genau in diesem Ziel sagen plus_comm bewerben?
Es funktioniert, wenn ich das Folgende tue, was ich eigentlich an erster Stelle beweisen wollte. Ziel foobar (3 + 4) = foobar (4 + 3). Beweis. umschreiben plus_comm. Reflexivität. Qed. Ich denke, Rewrite funktioniert nicht auf Werte, nur auf Typen. –
"rewrite" funktioniert bei beiden (eigentlich sind Typen Begriffe in Coq ;-). Das Hauptproblem hier ist, dass 'foob (3 + 4)' den Typ 'foobar (3 + 4)' und 'foob (4 + 3)' den Typ 'foobar (4 + 3)' hat. Coq kann prüfen, ob beide gleich sind (daher ist die Gleichheit gut typisiert), aber "rewrite" verwendet eine Zwischenform, wo dies nicht der Fall ist, daher die kryptische Fehlermeldung, die Sie mit 'rewrite (plus_comm 3 4) 'erhalten. – Virgile
Normalerweise sollten Sie 'pattern' (http://coq.inria.fr/refman/Reference-Manual011.html#pattern) für lokale Aktionen innerhalb des Begriffs verwenden können. Dies scheitert jedoch aus dem gleichen Grund, den @ Virgile erwähnt hat. Wenn das möglich ist, können Sie auch vorübergehend zu einem "vollständigeren" Gleichheitstyp wechseln (z. B. "JMeq"), dort etwas tun und dann zurückgehen. (Ich stelle es mir gerne als die 'komplexe Zahl' vor - ein Analogon der Gleichheit.) – nobody