Как построить список гетерогенных зависимых пар в Coq - PullRequest
Новая
       8

Как построить список гетерогенных зависимых пар в Coq

0 голосов
/ 12 января 2020

Я хотел бы иметь возможность иметь гетерогенную последовательность зависимых пар (T, f), где T находится в Set и f, если функция T -> bool такая как 

Definition classif :
  seq (forall T : Set, T -> bool) :=
  [:: (fun b : bool => b); (fun n : nat => false)].

Примечание: я использую синтаксис SSReflect для списков. Очевидно, что написанный выше тип не является правильным.

Возможно ли это?

Ответы [ 2 ]

1 голос
/ 12 января 2020

@ Ответ Тео Винтерхальтера - путь к go здесь. Просто добавьте точность к его ответу [Я изначально разместил его как комментарий, но это затрудняло читабельность кода…]:

тип, который вы ищете здесь - {T : Set & T -> bool}, это Σ-type и использует следующую индуктивность: 

Print sigT.

Inductive sigT (A : Type) (P : A -> Type) : Type :=
    existT : forall x : A, P x -> {x : A & P x}

. Чтобы упростить определение classif, вы также можете определить ярлык: 

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Definition sigma (T' : Set) f := (existT (fun A : Set => A -> bool) T' f).

Definition classif :
  seq {T : Set & T -> bool} :=
[:: sigma (fun b : bool => b); sigma (fun n : nat => false)].
1 голос
/ 12 января 2020

Вы ищете зависимые пары и вместо этого пишете зависимые функции. Тип указанных типов: 

{ A : Set & A }

Затем вы можете построить, например, пару nat и 1: 

Check (existT (fun A : Set => A) nat 1) : { A : Set & A }.

Это лучше с некоторыми обозначениями, но вы иметь его.

...