The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

(* Dear Coq-club,

First off, I apologize for what may be an overly detailed example---I
can't seem to make it any simpler while still revealing the problem I
am facing. Any suggestions you have for how I might prove the lemma
described below are much appreciated! 

Thanks in advance,
--Nik

I'm working with a system that uses a subtyping relation defined in
the manner shown below. Informally, in the definition of relate, the
list P:prims defines a set of primitive subtyping relationships. The
purpose of relate is to compose these primitive relationships 
transitively and by inspecting the structure of function types. The
unusual thing is that transitivity is formulated in a way that is 
always right-associative and where successive applications of 
the Rel_fun rule are disallowed.  *)

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) -> 
  (relate P a' t2 t2') -> 
  (relate P NoFun (typ_fun t1' t2') t) -> 
  (relate P Fun (typ_fun t1 t2) t).

(* My goal is to prove the following transitivity property for relate, as
   shown below: *)

Lemma relate_trans_v1: forall P a1 a2 t1 t2 t3, 
  (relate P a1 t1 t2) -> 
  (relate P a2 t2 t3) -> 
  (exists a, relate P a t1 t3).
Admitted.

(* However, because of the contravariance in the argument of the
functions in the Rel_fun, I suspect I require the stronger lemma shown
below. But, I am unable to prove this lemma, because I can't come up
with the appropriate induction principle. BTW, if I get rid of the
contravariance in Rel_fun, then relate_trans_v1 above is very easily
proved. *)

Hint Constructors relate.

Lemma relate_trans: forall P a1 a2 a3 t0 t1 t2 t3, 
  (relate P a1 t1 t2) -> 
  (relate P a2 t2 t3) -> 
  (relate P a3 t0 t1) -> 
  (exists a, relate P a t1 t3) /\ (exists a, relate P a t0 t2).
Proof.
intros P a1 a2 a3 t0 t1 t2 t3 P12 P23 P01.
generalize dependent t3.
generalize dependent a2.
generalize dependent t0.
generalize dependent a3.

induction P12.
  (* Case id *)
  intros. eauto.
  
  (* Case Rel_trans *)
  intros.


  assert ((exists a : alt, relate P a t2 t4) /\
          (exists a : alt, relate P a t2 t3)) as [[m_fwd D_fwd] [m_useless 
D_useless]].
     eapply IHP12; eauto.
  split. 
     (* Sub-case: extending to the right *)
     exists Fun. eauto.

     (* Sub-case: extending from the left *)
     (* Stuck:
              How can I construct (relate P a3 t0 t2) from
              H and P01 to use IHP12?

              Inverting on P01 only allows me to inspect the "head"
              of the derivation, not the "tail", which is what I need
              to tack on the (t1, t2) primitive relation at the end of
              P01.
     *)
     
     Focus 2.

  (* Case Rel_fun *)
     intros.
     
     (* Stuck again: 

        Similar to the previous sub case, how can I invert P01 and
        "fix up" the tail of the derivation so that I can
        construct (relate P a3 t0 (typ_fun t1' t2'))? 
     *) 
Admitted.