The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

To reason with setoids, you may need to re-think your maths a bit. 
Setoids are close to set-theory, but they work in a very different 
mindset. However, they provide in practice a very good interaction 
between more-or-less-common mathematics and programming. In usual 
mathematics, you tend to consider that things are equal a priori, in 
programming on the other hand, you consider that things have a 
representation, and consider a notion of equality a posteriori.
Setoids can be seen as the mathematical way of speaking of the latter.

Now for your case, the answer is reasonably simple. To be able to handle 
a setoid situation, your predicate typeof needs itself to be morphism 
from the environments/terms/types to the setoid often called Omega, that 
is Prop, together with the equivalence ( (<->) or iff in Coq). Your 
proposal for typeof, seems not to be, so you'll have to rewrite it so 
that things fit (you will probably need to introduce more equivalences 
inside your definitional cases, a possibility is adding a case that 
specifically handles converting a type to another if they are equivalent).

In any case, once you know that typeof is a morphism, then you should be 
able to manipulate type derivations in a rather natural way.



Arnaud Spiwack

Edsko de Vries a écrit :
> Hi Adam,
>
> First, thanks for your detailed answer. Before I try and study it, can I
> ask you to clarify something for me? Suppose I take the approach using
> setoids. The boolean algebra stuff is only a minor part of a larger
> formalization of my type system. In my type system, types consist of a
> base type (such as Int) and a uniqueness attribute (which is just a term
> in a boolean algebra). Now suppose I have 
>
>   x :: Int:Or True True
>
> (that is, a variable x in my term language whose type consists of the
> base type 'Int' and the attribute 'Or True True', a boolean term), and
>
>   f :: Int:True -> Int:True
>
> My typing rule looks something like
>
>   G |- f :: a -> b     G |- x :: a
>   -------------------------------- App
>            G |- f x :: b
>
> (I'm simplifying quite a bit here and glossing over lots of detail); or
> in Coq something like
>
>   Inductive typeof : env -> trm -> typ -> Prop :=
>     ..
>     | forall (G : env) (f x : trm) (a b : typ),
>         typeof G f (fn a b) ->
>         typeof G x a ->
>         typeof G (trm_app f x) b.
>
> What I might want to prove (as a simple test) is that the type of 'f x'
> is 'Int:True'. However, (so far at least), this proof will fail, because
> the type in the domain of f (Int:True) does not match the type of x
> (Int:Or True True). 
>
> This is why I wanted to deal with equivalence classes of boolean terms
> instead; because then the type Int:{True} (where {True} is the
> equivalence class for {True}) and the type Int:{Or True True} are in
> fact identical (because the equivalence class {True} and the equivalence
> class {Or True True} are the same class of terms) (but I'm not sure how
> to do that). One other possibility that I was considering was to
> introduce a "smart" constructor for types that applies some function to
> the attribute in the type to get some sort of canonical form -- but that
> would involve writing that function first and proving it correct :) It
> may also make other proofs more complicated, I'm not sure. 
>
> Would the setoid stuff help me here?  
>
> Thanks!
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>