Unter welchen Bedingungen erweitert "Eval cbv delta in" eine Definition in Coq?

Question

In Proof General (mit Coq 8,5), ausgeführt ich folgendes:

Require Import Arith. 
Eval cbv delta in Nat.add_comm 3 7. 

Der Ausgang ist

Nat.add_comm 3 7 : 3 + 7 = 7 + 3 

Allerdings gibt Print Nat.add_comm. eine lange und komplizierte Funktion nimmt zwei NATs als Eingang. Ich erwartete, dass mein Code die Definition von Nat.add_comm erweitert, was Eval cbv delta in _. in ähnlichen Situationen tut. Als Anfänger weiß ich, dass da ein naives Missverständnis lauert. Was vermisse ich?

Answer 1

ein bisschen auf Daniels Kommentar Erweiterung wird cbv delta eine Kennung entfalten, wenn

1. er einen Körper hat (dh kein Kontextvariable, Axiom, Feld in einem Modul Argumente zum aktuellen Modul Funktors, gebunden Variable, etc.), und
2. es Körper transparent gegeben, dh entweder der Beweis Skript wurde mit Defined geschlossen anstatt Qed oder der Körper wurde über := oder die automatische Verpflichtung Taktik gegeben (für Program Definition) oder typeclass Auflösung (für Instance s ohne Körper) und
3. es wurde über Opaque id oder Strategy opaque [id] nicht markiert opak und
4. es nicht durch „-Modul-locking“ eine weitere Konstante, dh definiert innerhalb eines Moduls (oder Modul Funktors) mit einem Modul-Typ ascription über : geschaffen statt <: (Ausnahme: wenn der Modultyp selbst den Körper für die konstante liefert) derzeit

Beachten Sie, dass, kann vm_compute um 3 zu erhalten (und die Vereinigung Motor kann auch, aber compute, lazy, cbv, hnf, cbn (normalerweise), simpl (normalerweise), und red kann nicht), aber nichts wird um die anderen herumkommen.