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
>

A first&quick answer:

Here comes a proof of nat==bool. It might be possible to do shorter, but
the idea is here: we inject naturals into booleans and show this can't be
a injection.

_________________________________________________________________________
Section nat_neq_bool.

Variable A : nat == bool.

Definition nat_to_bool : nat -> bool.
Rewrite <- A.
Exact [x]x.
Defined.

Lemma injective :
(a,b:nat)(nat_to_bool a)=(nat_to_bool b) -> a=b.
Intros a b.
Unfold nat_to_bool.
Unfold eq_rec eq_rect.
Case A; Simpl.
Auto.
Qed.

Lemma bool_cardinal :
 (b,b',b'':bool)~b=b' -> ~b'=b'' -> ~b''=b -> False.
Intros b b' b''; Case b; Case b'; Case b''; Auto.
Qed.

Lemma nat_neq_bool : False.
Apply (bool_cardinal
         (nat_to_bool O)
         (nat_to_bool (S O))
         (nat_to_bool (S (S O))));
Intro; Assert H0 := (injective ? ? H); Inversion H0.
Qed.

End nat_neq_bool.

Check nat_neq_bool.
________________________________________________________________________

For your initial question of decidability, you will need the following
facts:

bool <> A -> B
nat <> A -> B

and a bunch of things looking like A?B -> C?D -> ((A->C)?(B->C))
with all variety of ? being = or <>.

bool <> A -> B (resp nat) should be doable by same technics as nat<>bool.
But I'm unsure of the doability of the last ones. Sounds a bit like
extensionality, which is not provable (but can be a valid axiom). I give
you a definitive answer later on.

Pierre Letouzey