The Coq mailing list

[Olivier Desmettre <desmettr AT pauillac.inria.fr>]

----- Forwarded message from 
owner-coq-club AT pauillac.inria.fr
 -----

From: Jean Goubault-Larrecq 
<goubault AT lsv.ens-cachan.fr>
Organization: LSV, ENS Cachan
To: Nadeem Abdul Hamid 
<nadeem AT acm.org>
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Injection

Nadeem Abdul Hamid wrote:
> Parameters A,B:Set.
> Inductive SomeDef : Set
>   := sbase : A -> SomeDef
>   |  scons : (k:Set)(k -> SomeDef) -> SomeDef.

        No, you're doomed.  Note that (scons SomeDef)
has type (SomeDef -> SomeDef) -> SomeDef.  Call i=(scons SomeDef).
If Inversion worked on this case, i.e. if
        Cases x of
          scons f => ...
        | sbase a => ...
was allowed with x : SomeDef, f : (SomeDef -> SomeDef), a : A,
then notice that
        Cases (scons SomeDef f') of
          scons f => do-something-with f
        | sbase a => do-some-dummy-thing
would reduce to do-something-with f'.
        
        You would then get, as in my last mail,
an implementation of the untyped lambda-calculus
in Coq, making it non-terminating.
        Oh, by the way I just now realize that I
failed to send my previous answer to coq-club, too.
I have included it at the end.

> I don't mind changing the definition of SomeRel, but for certain reasons I
> really would like to use the given definition of SomeDef.

        I don't think you can escape changing it!
See above.  Maybe I could help if you tell me more
about what you would like to do?
        All the best,

        -- Jean.

--------------------------------------
--------------------------------------

Sender: 
goubault AT lsv.ens-cachan.fr
Date: Thu, 03 Jan 2002 11:15:35 +0100
From: Jean Goubault-Larrecq 
<goubault AT lsv.ens-cachan.fr>
Organization: LSV, ENS Cachan
To: Nadeem Abdul Hamid 
<nadeem AT acm.org>
Subject: Re: [Coq-Club] Injection

Nadeem Abdul Hamid wrote:
> Inductive jdef : Set
> := jconst : (k:Set)k -> jdef.
> 
> Lemma eq_jdef : (x,y:nat)
>                           (jconst ? x)=(jconst ? y)
>                           -> x=y.
> 
> Normally, the Injection tactic could be used, but apparently
> jdef is impredicative so it doesn't work.

        The first problem here is more with dependent types.
You have to use some form of dependent inversion.
However, I'll tell you why you cannot prove what
you intend to as you intend to.

        The real question is: is jdef really the inductive
type you had in mind?  You have to be aware that inhabitants
of jdef as you defined it can be rather complex.

        For example, (jconst nat) embeds all natural numbers
in jdef; (jconst (list nat)) embeds all lists of
natural numbers...; (well "embeds" provided you
can show that they are all injective, which you
are trying to do); in fact it is not hard to see
that every set (every type t:Set) embeds in jset
this way... including jset itself of course, or
even types that are larger than jset, like jset->jset.
Try this:
        Definition i := (jconst (jdef -> jdef)).
Then i has type (jdef -> jdef) -> jdef.
If it were provably injective, then you would already
run into some cardinality problems if you take
the set-theoretic semantics of data types---so
jdef is arguably a strange datatype already.

        In fact, the way you are trying to show
that (jconst nat) is injective would also
work to show that i above is injective, and
this would amount to building (by a dependent
Cases ... of ... end) a function r : jdef -> (jdef -> jdef)
such that
        (r (i f)) reduces to f.

        It is well-known that you get models
of the untyped lambda-calculus this way, in
particular the looping term Omega:
        Definition delta : jdef := (i [x:jdef] (r x x)).
        Definition Omega : jdef := (r delta delta).

Then    Omega = (r delta delta)
                = (r (i [x:jdef] (r x x)) delta)
                -> [x:jdef] (r x x) delta
                -> (r delta delta)
                = Omega.

        So you definitely do not want Inversion
to work on jdef if you want the reduction calculus
of Coq to terminate---and in passing, to be consistent.

        Again, the real question is: is jdef the
real type you want?  Have you considered:

Inductive jdef [k:Set] : Set := jconst : k -> (jdef k).
Lemma eq_jdef : (x,y:nat) (jconst ? x)=(jconst ? y) -> x=y.
Proof. Intros. Inversion H. Trivial. Qed.

        -- Jean.


----- End of forwarded message from 
owner-coq-club AT pauillac.inria.fr
 -----