The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Isn’t your subtyping relation just equality of types?

 

Thorsten

 

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Frederic Fort <frederic.fort AT inria.fr>
Date: Monday, 2 October 2023 at 19:03
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] Proving transitiviy of simple type system

You don't often get email from frederic.fort AT inria.fr. Learn why this is important

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.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.