The Coq mailing list

[Matthew Brecknell <coq-club AT brecknell.org>]

On Fri, 2009-06-12 at 16:18 -0700, Nikhil Swamy wrote:
> 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).

(* Hi Nikhil,

Sometimes it helps to work through some simple examples. Given this
simple primitive subtype relation: *)

Definition a : typ := typ_atom 0.
Definition b : typ := typ_atom 1.

Definition P : prims := (a,b) :: nil.

(* Then it's easy to show subtype-relatedness between some simple
function types: *)

Lemma rel_a_b: relate P NoFun a b.
  apply Rel_trans with NoFun b; simpl; auto; constructor.
Qed.

Hint Resolve rel_a_b.

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

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

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

Lemma rel_fun_ba_ab: relate P Fun (typ_fun b a) (typ_fun a b).
  (* ??? *)
Admitted.

(* Perhaps you could show how to do that before attempting the general
case?

Also, you may be making life unnecessarily difficult for yourself by
putting all of the parameters to relate after the colon. (I'm not sure
of the correct terminology to use here). You could move at least prims
and the second typ to be parameters before the colon, and that might
save you some of the headaches associated with dependent elimination.

Regards,
Matthew
*)