The Coq mailing list

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

Dear all,

This is my first mail to coq-club.
I am a PhD student from Belgium and I am using Coq to try formalize a
type soundness proof,
but I am having difficulties encoding in Coq something what I believe
to be a set algebra.
(I am fairly new to the formal treatment of programming languages.)

Concretely, I want to encode something that on paper would be written as 
follows

A ::=  0  |  A1 U A2  |  X  |  [A]  |  A \ X

So 0 means empty, U is a union operator, X are singleton elements (for
example numbers or identifiers),
[A] encapsulates an A as a singleton element and A \ X is a sort of
set minus that removes X from A.
The following laws govern equality on A.
The first four are the commutativity, associactivity, idempotence and
unitarity laws.
The last five specify the minus operation. The singleton [A] is not
affected by a minus.

A1 U A2  =  A2 U A1
(A1 U A2) U A3 = A1 U (A2 U A3)
A U A = A
A U 0 = A
0 \ X = 0
(A1 U A2) \X = A1 \ X U A2 \ X
X \ X = 0
X1 \ X2 = X1  if X1 /= X2
[A] \ X = [A]

My first attempt was to encode A as an inductive type,
and define the laws as axioms, until i realized that this is unsound.

Definition X := nat.

Inductive A : Set :=
 | a_empty : A
 | a_union : A -> A -> A
 | a_singl : X -> A
 | a_encap : A -> A
 | e_minus : A -> X -> A.

Axiom A_commutativity : forall A1 A2, a_union A1 A2 = a_union A2 A1.

Theorem inconsistency : False.
Proof.
 assert (a_union a_empty (a_singl 1) = a_union (a_singl 1) a_empty)
   by apply A_commutativity.
 inversion H.
Qed.


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".

I understand the positivity condition is there to prevent inconsistency,
but that leaves me stuck on how to encode A in Coq.

Any tips?

Many thanks,
Stijn Timbermont



On Mon, Aug 15, 2011 at 1:13 PM, 
�<coq-club-request AT inria.fr>
 wrote:
> Welcome to list 
>Â coq-club AT inria.fr
> Your subscription email is 
>Â stijn.timbermont AT gmail.com
>
>
> The Coq mailing list
>
> ________________________________
> Everything about this list: https://sympa-roc.inria.fr/wws/info/coq-club