2

Coqで定義された次の Inductive 型があります。

Inductive natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.

Notation "x :: l" := (cons x l) (at level 60, right associativity). 
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y  nil) ..).

natlist は基本的に自然数のリストです (Python のリストに似ています)。以下の定義を使用して、2 つの natlist の結合を見つけようとしています。

Definition union_of_lists : natlist -> natlist -> natlist

つまり Eval simpl in (union_of_lists [1,2,3] [1,4,1]) 、[1,2,3,1,4,1] を返す必要があります。

以下の疑問があります。

  • この定義には引数がないため、実際に入力を取得して処理するにはどうすればよいでしょうか?
  • 定義 union_of_lists は正確に何を返しますか? それはただのnatlistですか？

ヘルプやヒントは大歓迎です。

4

1 に答える 1

1

私は自分で答えを見つけました:)私がしたことは、別のFixpoint関数appendを作成し、それをの定義に割り当てましたunion_of_lists。

Fixpoint append(l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | (h :: t) => h :: app t l2
  end.`

その後

Definition union_of_lists : natlist -> natlist -> natlist := append.

Eval simpl in (append [1,2,3] [1,2,3]) (* returns [1,2,3,1,2,3] *)

定義union_of_listsは、引数を取りnatlist、型の別の関数を返す関数を返しますnatlist -> natlist（つまり、natlist引数を取り、を返す関数natlist）。

この定義は、関数または値のいずれかを返すことができる関数型プログラミングunion_of_listsの関数に似ています。

于 2010-09-06T20:30:42.503 に答える