The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

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