採取第一種類型的元組

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.