The Coq mailing list

[Stijn Timbermont <stijn.timbermont AT gmail.com>]

On Mon, Aug 15, 2011 at 4:04 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> Stijn Timbermont wrote:
>>
>> Concretely, I want to encode something that on paper would be written as
>> follows
>>
>> A ::=  0  |  A1 U A2  |  X  |  [A]  |  A \ X
>>
>> [...]
>>
>> Then I tried using Ensembles, and prove the laws.
>> A is then defined as Ensemble Aelt, so I have to define the element type.
>> The problem then is the form [A].
>>
>> Require Import Ensembles.
>>
>> Definition X := nat.
>>
>> Inductive Aelt : Type :=
>>  | e_single : X ->  Aelt
>>  | a_encap  : Ensemble Aelt ->  Aelt.
>>
>> This last definition is rejected with "Non-strictly positive
>> occurrence of "Aelt" in "Ensemble Aelt ->  Aelt".
>>
>
> Can you explain why you need an inductive type of sets and elements?  Why
> not assign different Coq types to X's, sets of X's, sets of sets of X's, and
> so on?
>

I understand your question as "why do I need the form [A], is it
really necessary to have elements of an A to (indirectly) contain
other A's". Correct?

A is in fact the encoding of an "effect" in a type and effect system.
The union is used for example in the typing rule of a let-expression.
In "let x = e1 in e2", if e1 has effect A1 and e2 has effect A2 then
the whole expression has effect A1 U A2.
Other expressions eliminate some X from the effect, using A \ X.
The form [A] is used to "protect" an effect from a eliminations or unions.
For example, if a and b are Xes, then a U b U a is equal to a U b,
but [a U b] U a is not equal to [a U b] or anything.
So this [A] really play an important role in the type system.

If I would use lists instead of ensembles there would be no problem,
and I would essentially have defined a custom tree datatype,
but without the non-syntactical equality properties.

Using ensembles would give me the properties I want,
but Coq does allow it, i presume in order to prevent things like "the
set of all sets" and the like?

I though about defining a custom equality relation over a tree-like datatype,
but that seems rather convoluted, amongst others because substitutions
in proofs would no longer work, correct?