The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

(* 

Thanks for your suggestion, Adam. I agree that what I was trying to do
is really not inversion and, as such, my problem was not specific to
Coq.

What I really need to do is induct on the length of the
derivation. So, my solution below instruments the definition of relate
with a natural number index that counts the length of a
sub-derivation. With this facility, and a couple of auxiliary lemmas
(including one you provided) I can push my proof through.

However, I wonder if there is some more standard idiomatic way of
handling a situation like this. Ideally something that doesn't require
me having to pollute my definitions with this counter instrumentation.

Also, you will notice that my proof script is not very readable at all
:( I end up doing a lot of things manually, e.g, at various points
when I use eauto I'm left with uninstantiated existential variables,
so I often have to provide explicit parameters to eapply. Any tips for
how to avoid this and/or to make my proof more readable would be
great!

*)

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 -> nat -> alt -> typ -> typ -> Prop :=
| Rel_id : forall P a t, 
  relate P 0 a t t

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

| Rel_fun: forall P a a' t1 t2 t1' t2' t n n1 n2, 
  (relate P n1 a t1' t1) -> 
  (relate P n2 a' t2 t2') -> 
  (relate P n NoFun (typ_fun t1' t2') t) -> 
  (relate P (S n) Fun (typ_fun t1 t2) t).

Hint Constructors relate.

Lemma Rel_prim : forall P a t1 t2,
  In (t1, t2) P
  -> relate P 1 a t1 t2.
  intros; apply Rel_trans with NoFun t2; auto.
Qed.

Hint Immediate Rel_prim.

Lemma relate_append : forall P n a t0 t1 t2,
  relate P n a t0 t1
  -> In (t1, t2) P
  -> relate P (S n) a t0 t2.
  induction 1; eauto.
(* Thanks Adam! *) 
Qed.

Hint Immediate relate_append.

Lemma split_tail : forall P a n t t', 
  (relate P n a t t') ->
  (n <> 0) -> 
  (exists t_pen, exists a', 
    (relate P 1 a' t_pen t') /\
    (forall t_ext m, relate P m a' t_pen t_ext -> exists m', relate P m' a t 
t_ext)).
Proof.
intros.
rename H into T. rename H0 into n_neq_0.
induction T.
(* Case "id". *)
destruct n_neq_0; eauto.

(* Case "trans". *)
induction n.
(*   SCase "1-step derivation". *)
  inversion T. subst.
  exists t1. exists a'.
  split. eauto.
  intros. eauto.

(*   SCase "n-step derivation". *)
  clear IHn.
  assert ((S n) <> 0) as sn. eauto.
  destruct (IHT sn) as [t_pen [a'' [rel_pen ext]]].
  clear IHT sn n_neq_0.
  exists t_pen.  exists a''. split. eauto.
  intros.
  destruct (ext _ _ H0) as [m' r_m'_ext].
  exists (S m').
  eauto.

(* Case "fun". *)
induction n.

(*   SCase "1-step derivation". *)
  inversion T3. subst.
  clear IHT1 IHT2 IHT3.
  exists (typ_fun t1 t2). exists Fun.
  split. eauto.
  intros. eauto.

(*   SCase "n-step derivation". *)
  clear IHn.
  assert ((S n) <> 0) as sn. eauto.
  destruct (IHT3 sn) as [t_pen [a'' [rel_pen ext]]].
  clear IHT3 sn n_neq_0.
  exists t_pen.  exists a''. split. eauto.
  intros.
  destruct (ext _ _ H) as [m' r_m'_ext].
  exists (S m').
  eauto.
Qed.

Lemma relate_trans: forall P a1 a2 a3 t0 t1 t2 t3 n1 n2 n3, 
  (relate P n1 a1 t1 t2) -> 
  (relate P n2 a2 t2 t3) -> 
  (relate P n3 a3 t0 t1) -> 
  (exists a, exists n1', relate P n1' a t1 t3) /\ 
  (exists a, exists n3', relate P n3' a t0 t2).
Proof.
intros P a1 a2 a3 t0 t1 t2 t3 n1 n2 n3 P12 Pright Pleft.
generalize dependent t3.
generalize dependent a2.
generalize dependent t0.
generalize dependent a3.
generalize dependent n2.
generalize dependent n3.

induction P12.
(*   Case "id". *)
  intros. split; eauto.
  
(*   Case "Rel_trans". *)
  intros.

  pose proof (relate_append _ _ _ _ _ _ Pleft H) as left_append.

  assert ((exists a : alt, exists n1', relate P n1' a t2 t4) /\
          (exists a : alt, exists n3', relate P n3' a t0 t3)) as [[a1' [n1' 
D_fwd]] left_extended].
     eapply IHP12; eauto.
  split. 
(*      SCase "extending to the right". *)
     exists Fun. exists (S n1'). eauto.
     eauto.

(*      SCase "Rel_fun". *)
     intros.

      split.
(*       SSCase "right extension". *)
       assert ((exists a : alt,   exists n1' : nat, relate P n1' a (typ_fun 
t1' t2') t3) /\
               (exists a : alt, exists n3' : nat, relate P n3' a (typ_fun t1' 
t2') t)) as 
          [[aright [n1_right right_ext]] ignore].
         eapply (IHP12_3 0 n0 Fun); eauto. (* explicit params to inst. 
existentials *)
       clear IHP12_3 ignore.
         inversion right_ext.
(*            SSSCase "right ext is id". *)
            subst. exists Fun. exists 1. eauto.
(*            SSSCase "right ext is trans". *)
            subst. exists Fun. exists (S (S n4)). eauto.
(*            SSSCase "right ext is fun". *)
            subst. exists Fun. exists (S n4).
            assert ((exists a : alt, exists n1' : nat, relate P n1' a t1' t1) 
/\
                    (exists a : alt, exists n3' : nat, relate P n3' a t1'0 
t1)) as [useless [aarg [n3arg rel_args]]].
              eapply (IHP12_1 n5 0 a0 _ H1 Fun); eauto. (* explicit params to 
inst. existentials *)
            clear useless IHP12_1.
            assert ((exists a : alt, exists n1' : nat, relate P n1' a t2 
t2'0) /\
                    (exists a : alt, exists n3' : nat, relate P n3' a t2 
t2')) as [[aret [n3ret rel_rets]] useless].
              eapply (IHP12_2 0 n6 Fun); eauto. (* explicit params to inst. 
existentials *)
            clear useless IHP12_2.
            eauto.
(*       SSCase "left extension". *)

      induction n3.
(*         SSSCase "pleft is id". *)
         inversion Pleft. subst.
           eauto.
(*         SSSCase "pleft is not id". *)
        assert ((S n3) <> 0) as neq. eauto.
        clear IHn3.
        destruct (split_tail _ _ _ _ _ Pleft neq) as [t_left_pen [a'_left_pen 
[rel_pen_t' ext]]].
        inversion rel_pen_t'.
(*         SSSSCase "last step of pleft is a trans". *)
        subst.
        inversion H2. subst.
        assert (relate P (S (S n)) a'_left_pen t_left_pen t) as pen_ext.
           eapply Rel_trans. eapply H0. eauto.
        exists a3. eauto.
(*         SSSSCase "last step of pleft is a fun". *)
        subst.
        inversion H3. subst. clear H3.
        assert   ((exists a : alt, exists n1' : nat, relate P n1' a t1' t4) /\
                  (exists a : alt, exists n3' : nat, relate P n3' a t1' t1)) 
as [[aarg [n1'_arg rel_arg]] useless].
           eapply (IHP12_1 0 n5 Fun); eauto. (* explicit params to inst. 
existentials *)
        clear IHP12_1 useless.
        assert ((exists a : alt, exists n1' : nat, relate P n1' a t2 t2') /\
                (exists a : alt, exists n3' : nat, relate P n3' a t5 t2')) as 
[useless [aret [n1'_ret rel_ret]]].
           eapply (IHP12_2 n6 0 a'0 _ H1 Fun);  eauto. (* eauto leaves 
uninstantiated existentials *)
        assert (relate P (S n) Fun (typ_fun t4 t5) t) as pen_ext.
          eauto.
        exists a3. eauto.
Qed.

> -----Original Message-----
> From: Adam Chlipala 
> [mailto:adamc AT hcoop.net]
> Sent: Sunday, June 14, 2009 8:20 AM
> To: Nikhil Swamy
> Cc: 
> coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] Transitivity for a non-standard subtyping
> relation
> 
> (* Here's a lemma that makes it easy to solve the first of the "stuck"
> cases from your original post. *)
> 
> Lemma Rel_prim : forall P a t1 t2,
>   In (t1, t2) P
>   -> relate P a t1 t2.
>   intros; apply Rel_trans with NoFun t2; auto.
> Qed.
> 
> Hint Immediate Rel_prim.
> 
> Lemma relate_append : forall P a t0 t1 t2,
>   relate P a t0 t1
>   -> In (t1, t2) P
>   -> relate P a t0 t2.
>   induction 1; eauto.
> Qed.
> 
> (* I don't think this kind of manipulation could be passed off as
> "inversion" even in a pencil-and-paper proof, so I don't think this
> problem has much to do with Coq.  You would really need to prove this
> lemma inductively in any case, right? *)
> 
> Nikhil Swamy wrote:
> > 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.
> >      *)
>