CODEWITHSUNDEEP
listtypescoq
hivert
hivert

Reputation: 10657

How to build a list of heterogeneous dependant pairs in Coq

I'd like to be able to have an heterogeneous sequence of dependent pairs (T, f) where T is in Set and f if a function T -> bool such as

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

Note: I'm using SSReflect syntax for lists. Clearly the type written above is not the right one.

Is it possible ?

Upvotes: 1

Views: 89

Answers (2)

ErikMD
ErikMD

Reputation: 14723

@ThéoWinterhalter's answer is the way to go here. Just add a precision w.r.t. his answer [I initially posted it as a comment but that hindered the readability of the code…]:

the type you are looking for here is {T : Set & T -> bool}, it is a Σ-type and relies on the following inductive:

Print sigT.

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

And to ease your definition of classif, you could also define a shortcut:

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)].

Upvotes: 1

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

You're looking for dependent pairs and are writing dependent functions instead. The type of pointed types is

{ A : Set & A }

Then you can build for instance the pair of nat and 1:

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

It is nicer with some notations but there you have it.

Upvotes: 1

Related Questions