的例子

提供部分參數考慮本節：的例子

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.

在這裏，我用Variables聲明我的定義域和值域類型。由於我的函數的定義完整性檢查，我想包括Example：

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

但是似乎我無法將部分內這樣做。相反，我得到：

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

這不是太奇怪，所以讓我們嘗試另一種方式：

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

主要生產：

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

我想這是公平的，部分-美化版Variables AREN與隱含的論證不同。但它仍然留下了問題！

如何在結束本節之前提供混凝土Variables以創建有用的Examples？

來源

2017-02-02 phs

AFAIK你不能。您必須先關閉該部分才能使參數被拉姆達提升。 – gallais

Boooooo。這顯然不是一個大問題，但將我的例子遠離他們的定義會傷害他們的實用性。 – phs

順便說一句，我認爲你想'變量'而不是'參數'，因爲'參數'是'Axiom'的另一個名字。在關閉該部分併發出'Check mymap.'命令後，可以看到差異。 –

Section MyMap. 
...

如果我們檢查的mymap類型裏面的部分，我們得到

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

當然，我們也不能統一D和R與nat，因爲D和R一些本地假定的類型。

但是，我們可以排序的模擬你的例子在這個廣義的設置，顯示了mymap功能的預期性能：

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.

來源

2017-02-02 08:32:55

回答

相關問題