The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

(* Thanks Adam and Matthew (and everyone else) for taking a look at 
   this. I hope the following sketch and example convey better the 
   essence of my problem.
     
   Here's an informal statement and (incomplete) proof sketch of my
   lemma:

 Lemma 1: forall a a' t1 t2 t3,
   (D1) relate a t1 t2
   (D2) relate a' t2 t3
   =>  relate Fun t1 t3
   
   By induction on the structure of (D1), the interesting case is when
   (D1) is an application of (Rel_fun), as shown below:

 (D1.1)  relate a s1 t1           
 (D1.2)  relate a' t1' s1'
 (D1.3)  relate NoFun (typ_fun s1 s1') t2
 -------------------------------------------------------- [D1]
   relate Fun (typ_fun t1 t1') t2

   From the induction hypothesis applied to D1.3 and D2 we get 
   
 (D2')  relate Fun (typ_fun s1 s1') t3. 

   Now, by inversion on (D2'), we get the following interesting case:

 (D2'.1)  relate b r1 s1           
 (D2'.2)  relate b' s1' r1'
 (D2'.3)  relate NoFun (typ_fun r1 r1') t3
 ----------------------------------------------------- [D2']
   relate Fun (typ_fun s1 s1')  t3

   Now, the goal is to construct (relate Fun (typ_fun t1 t1') t3).  We
   can do this by using Rel_fun, to first take a "step" to 
   (typ_fun r1 r1') and then to use (D2'.3) to complete the derivation.

   I can use the induction hypothesis on (D1.2) and (D2'.2) to construct 
   
   (G.2)  (relate Fun t1' r1')

   Similarly, I'd like to use the induction hypothesis on (D1.1) and
   (D2'.1) to construct:

   (G.1)  (relate Fun r1 t1)

   So, now I can construct:

 (G.1)   (relate Fun r1 t1)
 (G.2)   (relate Fun t1' r1')
 (D2'.3) (relate NoFun (typ_fun r1 r1') t3)
 ----------------------------------------------------------- [Goal]
   relate Fun (typ_fun t1 t1') t3

   
   However, this doesn't quite work in Coq because the induction
   hypothesis on (D1.1) only applies to derivations that "extend D1.1
   to the right", i.e., derivations that are of the form (relate a t1
   x) and not (relate a x s1), which is what we have in (D2'.1).

   My thought at this point was to attempt to prove a version of this
   transitivity lemma in which extending a derivation both "to the
   right" and "from the left" is explicitly included in the induction
   hypothesis. I.e, something like:

 Lemma 2: forall a a' a'' t0 t1 t2 t3,
   (D1) relate a t1 t2
   (D2) relate a' t2 t3
   (D3) relate a'' t0 t1
   =>  relate Fun t1 t3  /\ relate Fun t0 t2

   But, from my previous posting, you will see that I get stuck in
   carrying out this proof because I reach a point where I have


 (D1.1)  relate a s1 t1           
 (D1.2)  relate a' t1' s1'
 (D1.3)  relate NoFun (typ_fun s1 s1') t2
 -------------------------------------------------------- [D1]
   relate Fun (typ_fun t1 t1') t2

and 

  (D3)   (relate a t0 (typ_fun t1 t1'))

   and need to show (relate Fun t0 t).

   In order to do this, what I really want to do is inspect the "last
   step" of (D3) and in the case where it is of the following form,

       (relate Fun (typ_fun r1 r1') (typ_fun t1 t1'))

   I want to construct a 
   
       (relate Fun (typ_fun r1 r1') (typ_fun s1 s1')) 

   using the premises of D1 and D3, and the induction hypotheses.

   However, I don't have a way of inverting/inducting on (D3) so that
   I can inspect the tail of the derivation.

   In case this handwaving is too confusing, I'm including a variation
   of my system below in which I have replaced the contravariance of
   relate in the argument of a function with covariance. I state and
   prove the transitivity lemma (a version of Lemma 1 above) for this
   altered system. I hope this also helps provide some intuitions for
   this system. 

   Again, many thanks for taking the time to look at this. I really
   appreciate your help!

--Nik

*)

Require Import List.

Inductive typ : Type :=
| typ_atom : nat -> typ
| typ_fun : typ -> typ -> typ.

Inductive alt : Type :=
| Fun
| NoFun.

Notation prims := (list (typ * typ)).

Inductive relate : prims -> alt -> typ -> typ -> Prop :=
| Rel_id : forall P a t,
  relate P a t t

| Rel_trans: forall P a a' t1 t2 t3, 
  (In (t1, t2) P) -> 
  (relate P a t2 t3) -> 
  (relate P a' t1 t3)

| Rel_fun: forall P a a' t1 t2 t1' t2' t, 
  (relate P a t1 t1') ->  (* Note the change from the previous version---no 
longer contravariant *)
  (relate P a' t2 t2') -> 
  (relate P NoFun (typ_fun t1' t2') t) -> 
  (relate P Fun (typ_fun t1 t2) t).

Hint Constructors relate.

Lemma relate_trans: forall P a1 a2 t1 t2 t3, 
  (relate P a1 t1 t2) -> 
  (relate P a2 t2 t3) -> 
  (exists a, relate P a t1 t3).
intros P a1 a2 t1 t2 t3 P12 P23.
generalize dependent a2.
generalize dependent t3.
induction P12.
  (* Case id *)
  intros; eauto.

  (* Case trans *)
  intros.
    destruct (IHP12 _ _ P23) as [aa tail].
    exists Fun. eauto.

  (* Case fun *)
  intros.
    destruct (IHP12_3 _ _ P23) as [aa tail].
    clear IHP12_3.

    inversion tail.

    (* Case tail is id *)
    subst. exists Fun. eauto.
    
    (* Case tail is trans *)
    subst. exists Fun. eauto.
    
    (* Case tail is fun -- the interesting case *)
    subst.
      rename H6 into tail_of_tail.
      rename H1 into tail_arg.
      rename H4 into tail_ret.
    (* The two adjacent applications of Rel_fun, 
        first from (typ_fun t1 t2) to (typ_fun t1' t2') in P12
        and then from (typ_fun t1' t2') to (typ_fun t1'0 t2'0) in tail
        can be collapsed into a single application of Rel_fun by
        composing P12_1 and tail_arg, and P12_2 with tail_ret *)
     destruct (IHP12_1 _ _ tail_arg) as [a_arg arg].
     destruct (IHP12_2 _ _ tail_ret) as [a_ret ret].
     exists Fun.
       eauto.
Qed.

> -----Original Message-----
> From: Matthew Brecknell 
> [mailto:matthew AT brecknell.net]
> Sent: Saturday, June 13, 2009 11:23 PM
> To: Nikhil Swamy
> Cc: 
> coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] Transitivity for a non-standard subtyping
> relation
> 
> 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...
> 
> 
>