[Iris-Club] Well-Typedness of the Base Logic

[Ralf Jung]

Hello Craig,

indeed, Danny's answer is spot-in.  On paper we have a deep embedding with our
own notion of terms, variables and substitution (though we are lazy and never
define the latter).  In Coq, however, that would just be a huge pain and it is
much more convenient to re-use the binders and type system of the metalogic.
Iris' type system is essentially the simply-typed lambda calculus, so Coq is
easily powerful enough to do the type checking.

If you will, you could view this as working directly in some kind of
denotational semantics where the Iris types and terms are interpreted as Coq
types and terms.  This saves us all all the work of defining a term language and
substitution, of figuring out how to make the term language extensible with user
definitions (the "signature" on paper), and it is also vastly more efficient as
Coq doesn't have to work through this extra layer.

Every terminal in the grammar on §5.1 corresponds to a definition in Coq; you
found the file (primitive.v) with the ones involving iProp.  The
non-propositional ones are just the ones from Coq, e.g. we re-use Coq's pairs
and sums.  The rules in §5.2 then correspond to the rules of Coq's type system.

Does this answer your question?

Kind regards,
Ralf

On 26.04.2018 21:16, Danny Gratzer wrote:
> Hello,
> 
> I hope I am not misunderstanding your question but I believe the answer is that
> this step is never done
> explicitly.
> 
> The iris-coq formalization is a shallow embedding so there is no explicit Coq
> datatype for the syntax of base logic terms. 
> Functions are represented as normal Coq functions so there is no need to
> explicitly specify the typing rules governing
> them: they're built into Coq. Similarly with products, sums, etc. Once the type
> of propositions, iProp, is defined in Coq
> Iris propositions are just represented as  normal Coq terms belong to iProp.
> 
> I think that there should then really be no analog of 5.2 explicitly, it's
> encompassed in how the object terms
> are represented in Coq in the first place.
> 
> This is why, for instance, the definition of weakest preconditions we are able
> to take a guarded fixed point of
> a normal Coq function (see wp_def in theories/program_logic/weakestpre.v).
> 
> Danny
> 
>