The Coq mailing list

[Frederic Fort <frederic.fort AT inria.fr>]

Hello,

I am trying to prove the some facts about the type system of a simple Lambda calculus. However, I struggle to prove the transitivity of the subtype relation.

I have seen in papers that certain people simply "axiomatize" properties like transitivity and reflexivity by defining specific rules for these properties.

However, I find this inelegant as this makes proofs in other places more "cluttered" due to the additional constructors.

I have a few proofs that work fine. For transitivity however, I am stuck.

I have tried all kinds of (dependent) induction approaches, but I am generally stuck either because Coq requires me to prove that the unit type is a subtype of a function type or because the induction hypothesis doesn't take into account that subtyping of function input types is in the "opposite direction".

I suppose that there is some "Coq trick" that I am unfamiliar with (maybe I have to define a custom induction scheme ?).

Or maybe it is actually impossible to prove transitivity like that.

If somebody could show me what I am missing, I'd be grateful.

Yours sincerely,

Frédéric Fort

Here are my definitions:

Inductive expr :=
| Unt
| Var (n : nat)
| Lam (v : nat) (e : expr)
| App (f : expr) (arg : expr)
.

Inductive type :=
| TUnit
| TFun (tin tout : type)
.

Inductive typeSub : type -> type -> Prop :=
| SubTUnit : typeSub TUnit TUnit
| SubTFun : forall ti1 to1 ti2 to2, typeSub ti2 ti1 -> typeSub to1 to2 -> typeSub (TFun ti1 to1) (TFun ti2 to2)
.

Lemma refl:
forall t, typeSub t t.
Proof.
intros.
induction t; constructor; auto.
Qed.

Lemma sub_is_eq:
forall t1 t2, typeSub t1 t2 -> t1 = t2.
Proof.
intros.
induction H.
- reflexivity.
- rewrite IHtypeSub1. rewrite IHtypeSub2. reflexivity.
Qed.

Lemma trans:
forall t1 t2 t3,
typeSub t1 t2 -> typeSub t2 t3 -> typeSub t1 t3.
Proof.
intros t1 t2 t3 HSubL HSubR.
Admitted.