The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On Mon, Oct 2, 2023 at 8:02 PM Frederic Fort <frederic.fort AT inria.fr> 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 ?).

If you try to do the proof on paper (like you should when you're getting stuck), you'll see that it is already non-trivial.  So, there's no "Coq trick" specifically, just finding the correct proof.

The solution is to do a structural induction on the middle type t2, followed by inversion on the t1 <: t2 and t2 <: t3 hypotheses.

Lemma trans:
  forall t1 t2 t3,
  typeSub t1 t2 -> typeSub t2 t3 -> typeSub t1 t3.
Proof.
  intros t1 t2; revert t2 t1.
  induction t2; intros t1 t3 HSubL HSubR; inversion HSubL; inversion HSubR; econstructor; eauto.
Qed.

Why the middle type t2?  Because it's the only form that gives you an induction hypothesis usable with contravariance, which swaps the roles of t1 and t3.

There's a lot more details in the POPLmark challenge, but since it uses a much more complicated subtyping relation, the proof is much more complex.  First, transitivity and weakening must be proved simultaneously.  Second, in some encodings of bound variables, recursion is not always on a subterm of t2 but on a freshened-up subterm of t2, so the proof is no longer by induction on the structure of t2, but can still be done by induction on the size of t2.

Hope this helps,

- Xavier Leroy

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.