Versorgung Abschnitt Argumente für Beispiele

Question

Betrachten Sie diesen Abschnitt:

Section MyMap. 

Variables D R : Type. 

Fixpoint mymap (f : D -> R) (l : list D) : list R := 
    match l with 
    | nil => nil 
    | d :: t => f d :: mymap f t 
    end. 

End MyMap. 

Hier habe ich Variables verwendet, um meine Domain und Bereichstypen zu deklarieren. Als Plausibilitätsprüfung auf die Definition meiner Funktion, würde Ich mag ein Example enthalten:

Example example_map_S : mymap S [0; 1; 2] = [1; 2; 3]. 
Proof. 
    simpl; trivial. 
Qed. 

aber es ich in meinem Abschnitt so tun können, nicht scheint. Stattdessen erhalte ich:

Error: The term "S" has type "nat -> nat" while it is expected to have type "D -> R". 

Das ist nicht allzu überraschend, so machen wir es eine andere Art und Weise versuchen:

Example example_map_S : @mymap nat nat S [0; 1; 2] = [1; 2; 3]. 
Proof. 
    simpl; trivial. 
Qed. 

Welche produziert:

Error: The term "nat" has type "Set" while it is expected to have type "D -> R". 

Ich nehme an, das ist fair, Abschnitt-ized Variables aren Das gleiche gilt für implizite Argumente. Aber es bleibt immer noch die Frage!

Wie kann ich Beton Variables zu einem Begriff vor dem Schließen des Abschnitts liefern, um nützliche Examples zu erstellen?

Answer 1

Section MyMap. 
... 

Wenn wir die Art der mymapinnerhalb den Abschnitt überprüfen, erhalten wir

Check mymap. 
(* mymap : (D -> R) -> list D -> list R *) 

Natürlich haben wir D und R mit nat nicht vereinigen können, da D und R sind einige lokal postulierte Typen.

können wir jedoch eine Art Ihr Beispiel in dieser verallgemeinerten Einstellung simulieren, die erwartete Eigenschaft der mymap Funktion zeigt:

Example example_nil (f : D -> R) : 
    mymap f [] = [] := eq_refl. 

Example example_3elems (f : D -> R) (d0 d1 d2 : D) : 
    mymap f [d0; d1; d2] = [f d0; f d1; f d2] := eq_refl. 

End MyMap.