coq - 取元组列表中的第一个类型

Question

我有一个列表l有类型：l: list (list (A * B * C * D))我希望它为我返回一个类型list (list A)

我正在尝试split带有参数的函数代码list (A * B * C * D)以查看结果。

Require Import List.
Variables A B C D : Type.
Definition split_list (l: list (A * B * C * D)) : list (A * B * C) * list D 
           := split l.

我该如何编写函数？

Answer 1

我会这样做：

π1 : A × B → A
π1 ∘ π1 : A × B × C → A
π1 ∘ π1 ∘ π1 : A × B × C × D → A
map (π1 ∘ π1 ∘ π1) : (A × B × C × D) * → A *
map (map (π1 ∘ π1 ∘ π1)) : ((A × B × C × D) *) * → (A *) *

你可能需要这个：

Definition comp {s1 s2 s3 : Set} (f2 : s2 -> s3) (f1 : s1 -> s2) (o1 : s1) : s3 :=
  f2 (f1 o1).

Notation "f2 ∘ f1" := (comp f2 f1) (at level 30, right associativity).

Inductive Prod (s1 s2 : Set) : Set :=
  | Pair : s1 -> s2 -> Prod s1 s2.

Arguments Pair {_ _} _ _.

Notation "s1 × s2" := (Prod s1 s2) (at level 40, left associativity).

Notation "( o1 , o2 , .. , o3 )" := (Pair .. (Pair o1 o2) .. o3) (at level 0).

Definition proj_1 {s1 s2 : Set} (p1 : s1 × s2) : s1 :=
  match p1 with
  | (o1, _) => o1
  end.

Notation "'π1'" := proj_1 (at level 0).

Inductive List (s1 : Set) : Set :=
  | Nil : List s1
  | Cons : s1 -> List s1 -> List s1.

Arguments Nil {_}.

Arguments Cons {_} _ _.

Notation "s1 *" := (List s1) (at level 30, no associativity).

Notation "'ε'" := Nil (at level 0).

Notation "o1 ◁ l1" := (Cons o1 l1) (at level 60, right associativity).

Fixpoint map {s1 s2 : Set} (f1 : s1 -> s2) (l1 : s1 *) : s2 * :=
  match l1 with
  | ε => ε
  | o1 ◁ l2 => (f1 o1) ◁ (map f1 l2)
  end.