The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

Hi Frédéric,

In this particular case, you don't really need an additional inductive proof for your transitivity lemma. The other lemmas you've already proven are sufficient. This is because your subtyping relation is somewhat trivial, as you prove yourself through your sub_is_eq lemma. You can prove transitivity as follows:

Lemma trans:
forall t1 t2 t3,
typeSub t1 t2 -> typeSub t2 t3 -> typeSub t1 t3.
Proof.
intros. apply sub_is_eq in H. apply sub_is_eq in H0. subst. apply refl.
Qed.

This is obviously no longer possible once you define a more "interesting" subtype relation.

Lasse

On 02-10-2023 19:53, Frederic Fort wrote:

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.