The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Wed, 30 Jul 2003, Lukasz Stafiniak wrote:

> Hi List,
>
> Can the following equality be decided?
>
> Inductive typterm : Set->Set :=
>    tybool : (typterm bool)
>  | tynat : (typterm nat)
>  | tyfun : (a, b : Set)(typterm a)->(typterm b)->(typterm (a->b)).
>
> Definition deceq : (a,b:Set)(typterm a)->(typterm b)->
> {a==b}+{~a==b}.
>
> Is it anyway true, that ~nat==bool? Do you know any other means to decide
> type equality (computationally)?
>
> Thank You, Best Regards,
> Lukasz
>
>

Hello again.

After some discussion with Gilles Dowek, we have identified at least one
unprovable equality needed to establish your deceq result, that is

        nat = (bool -> nat)

Those two are isomorphic, at least when viewed as sets (since bool -> nat
is isomorphic to nat*nat). So you won't be able to establish
~nat=(bool->nat). And proving nat = (bool -> nat) is not provable
either in the system. So that makes your deceq unprovable.


Btw, concerning the status of ~nat=(nat->bool) (mentionned by JF Monin),
Gilles and I have also the feeling that it's unprovable as such. But
it might be provable with enough axioms (excluded middle, plus maybe a
form of axiom of choice). We can at least prove that there isn't any
surjective function from nat to nat->bool (Cantor argument), but that does
not gives us the falsity of nat = (nat->bool).


If your goal is to formalize the semantics of a language with bool & nat
as base types and the arrow construct, you might rather want to define

Inductive typterm : Set :=
  Nat : typterm
| Bool : typterm
| Fun : typterm -> typterm -> typterm.

Then the equality over typterm is trivially decidable. And you can later
on project these abstract types to concrete types when needed, by
something like:

Fixpoint domain [t:typterm] : Set := Cases t of
  Nat => nat
| Bool => bool
| (Fun t1 t2) => (domain t1) -> (domain t2)
end.

I hope this tip can fit your needs...

Pierre Letouzey