coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Transitivity for a non-standard subtyping relation

From: Matthew Brecknell <matthew AT brecknell.net>
To: Nikhil Swamy <nswamy AT microsoft.com>
Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Transitivity for a non-standard subtyping relation
Date: Sun, 14 Jun 2009 16:22:32 +1000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I wrote:
> (* However, if subtype-relatedness (according to the way you've defined
> it) really is transitive, it should be possible to show the following,
> but I don't see how to do it: *)

Silly me, I see it now:

Lemma rel_fun_ba_ab: relate P Fun (typ_fun b a) (typ_fun a b).
apply Rel_fun with NoFun NoFun a b; auto; constructor.
Qed.

So I guess that brings me no closer to understanding your problem.
Sigh...

[Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
- Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
- Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Matthew Brecknell
  - Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Matthew Brecknell
    - RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
      - Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
        
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
        
        Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
        
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
        Message not available
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
    - [Coq-Club] Module Types, Cedric Auger
      - Re: [Coq-Club] Module Types, Elie Soubiran
        
        Re: [Coq-Club] Module Types, Cedric Auger