... gibt es eine Motivation, einen über den anderen zu verwenden?
Ja es gibt, aber (wie üblich) "es kommt darauf an". Lassen Sie uns zuerst ein wenig den Unterschied zwischen ihnen diskutieren.
Maximally-implizierten implizite (MII) Argumente fügen der Sprache die nächste Stufe der "Implizitheit" hinzu. Gewöhnliche (Nicht-MII) Argumente werden nur eingefügt, wenn eine Funktion auf mindestens ein Argument angewendet wird. Darüber hinaus fügt Coq diese Argumente nur vor einige zur Verfügung gestellt explizite Argument.
MII Argumente sind "gespannt": Coq sie eingefügt hält nach einige explizite Argument geliefert. Ein Eckfall: Wenn die Signatur einer Funktion mit einem MII-Argument beginnt, genügt es, den Funktionsnamen (auch ohne Anwendung) für Coq zu erwähnen, um ihn in eine partiell angewendete Funktion umzuwandeln (nicht bei Nicht-MII-Argumenten). Manchmal hilft dieses eifrige Verhalten, prägnanten Code zu schreiben, und manchmal ist es ein bisschen lästig, weil es uns zwingt, ansonsten überflüssige @ Symbole einzufügen, um das Einfügen von impliziten Argumenten zu unterdrücken.
Lassen Sie mich einige einfache Beispiele zeigen, die größtenteils aus dem Referenzhandbuch oder der Standardbibliothek stammen.
Präambel:
Require Import Coq.Lists.List. Import ListNotations.
Section Length.
Variable A:Type.
Die length Funktion hat nicht-MII erstes Argument:
Print Implicit length.
(*
Output:
length : forall A : Type, list A -> nat
Argument A is implicit
*)
Deshalb ist der folgende einfache Code fehlschlägt (es fehlschlägt, weil length nicht teilweise angewandt wird, so A ist nicht eingefügt):
Fail Check (fun l:list (list A) => map length l).
Man muss so etwas schreiben, damit es funktioniert:
Check (fun l:list (list A) => map (@length _) l).
(* or *)
Check (fun l:list (list A) => map (length (A := _)) l).
(* or *)
Check (fun l:list (list A) => map (fun xs => length xs) l).
Eine weitere Möglichkeit, MII Argumente zu verwenden wäre. Intuitiv, in diesem Fall Coq ersetzt length mit (@length _):
Arguments length {A} _.
Check (fun l:list (list A) => map length l).
End Length.
Aber manchmal maximal eingefügt Argumente werden immer in der Art und Weise, wenn man will, eine Funktion oder einen Konstruktor in seiner allgemeinsten Form verwenden (nicht teilweise angewendet).Ein Arbeitsbeispiel mit nicht-MII Argumenten aus dem Coq.Lists.List Modul:
Set Implicit Arguments. (* non-MII arguments is the default behavior *)
Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop :=
| Forall2_nil : Forall2 R [] []
| Forall2_cons : forall x y l l',
R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l').
Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] [].
Proof. exact Forall2_nil. Qed.
Aber exact Forall2_nil wird im Fall von MII Argumenten nicht. Die constructor wird uns helfen, aber:
Arguments Forall2_nil {A B} _.
Theorem Forall2_refl' : forall A B (R:A->B->Prop), Forall2 R [] [].
Proof. Fail (exact Forall2_nil). constructor. Qed.
Eine weitere Instanz der vorzeitigen implizite Argument Insertion (von Coq.Init.Logic). Dies funktioniert mit nicht-MII Argumente:
Declare Left Step eq_stepl.
Aber hier müssen wir hinzufügen '@':
Arguments eq_stepl {A} _ _ _ _ _.
Fail Declare Left Step eq_stepl.
Declare Left Step @eq_stepl.
Manchmal Taktik der Form <tactic-name> ... with (_ := _). wird in Gegenwart von MII Argumente versagen . Hier ist eine andere (in Betrieb) Beispiel aus Coq.Init.Logic:
Definition eq_ind_r :
forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
Defined.
Aber MII Argumente behindern unsere Fortschritte:
Arguments eq_sym {A x y} _.
Definition eq_ind_r' :
forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
intros A x P H y H0.
Fail elim eq_sym with (1 := H0); assumption.
(* this works *)
elim @eq_sym with (1 := H0); assumption.
(* or this: *)
elim (eq_sym H0); assumption.
Defined.
Ist ein aktueller als die anderen?
Ich weiß nicht, ich hoffe, jemand könnte etwas Licht darauf werfen.
Maximal implizite Argumente müssen einfach {} geschaffen werden, während ein oder ArgumentsImplicit Arguments angeben nichtmaximale diejenigen verwenden hat. Bedeutet es, dass maximale implizite Argumente bevorzugt werden sollten?
Standardmäßig deklariert die Direktive Set Implicit Arguments. nicht implizit eingefügte implizite Argumente. Also ist Coq konservativ (aber nicht zu viel) über das Niveau der Selbstverständlichkeit. Ich würde standardmäßig bei Nicht-MII-Argumenten bleiben und {} einfügen, wo es angebracht ist.