The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Jeremy,

> Le 25 juil. 2019 à 04:10, Jeremy Dawson 
> <Jeremy.Dawson AT anu.edu.au>
>  a écrit :
> 
> Hi,
> 
> I'm implementing some netalogic in Coq, in which it is easy to say. (for 
> example)
> 
> is_derivable A -> is_derivable B -> is_derivable (A and B)
> 
> Unlike some other proof logics, we get an object which represents the 
> actual proof (whose type is is_derivable (A and B)), and potentially we 
> should be able to define the height or size (number of steps) of the 
> proof tree involved.
> 
> However, whereas the natural view of the type of is_derivable would be
> formula -> Prop, I find that to define the height of the proof object I 
> need to make the type of is_derivable formula -> Type
> 
> Then I find that whereas my initial version (that is, the Prop version) 
> of is_derivable involved standard stuff like Forall and In (of types ... 
> -> Prop), I need versions of these with types --- -> Type.  Examples 
> shown below.
> 
> My questions are:
>   - does this sort of thing already exist (maybe under a different 
> name), and
>   - is there an easier way than defining new versions of these standard
> library functions?

As already answered by Dominique, you can either index your derivations by a 
height 
(it’s slightly cumbersome though to see this indexing everywhere), or squash 
derivations
in Type. In the MetaCoq project we went with the second approach and had to 
indeed develop
extensively the theory of All/Alli/All2/Exists on predicates in Type which is 
absent from the 
stdlib. You might want to reuse some of this [1].

As you can see, most of the stdlib is geared towards a logic in Prop, but we 
know today
that we can equivalently do it in Type and squash/make things 
proof-irrelevant as a last step
thanks to a « bracket » type in most situations (in Prop/sProp or using 
truncation to hProp in HoTT).
Hopefully the upcoming stdlib will be more agnostic w.r.t. the logic but it’s 
not entirely 
trivial to be generic over that today.

[1] 
https://github.com/MetaCoq/metacoq/tree/coq-8.8/template-coq/theories/utils.v
— Matthieu