The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

(* 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.
>      *)