The Coq mailing list

[Jason Hu <fdhzs2010 AT hotmail.com>]

Hi Frederic,

I forgot that fixpoint structure is stricter in Coq. The conventional solution to this situation is to do induction on t2. The following proof has passed in my environment:

Hint Constructors typeSub.

Lemma trans':

  forall t2 t1 t3, typeSub t1 t2 -> typeSub t2 t3 -> typeSub t1 t3.

Proof.

  induction t2; intros;

    inversion H; inversion H0; eauto.

Qed.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Frederic Fort <frederic.fort AT inria.fr>
Sent: Monday, October 2, 2023 5:26 PM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proving transitiviy of simple type system

 

Thank you all for your kind input.

Indeed the simplest/most obvious solution was to simply use the previous lemmas, but as my goal was to progress from a "boring" lambda calculus to something more interesting, I was focussed on doing it the "right" way from the beginning.

But maybe that'll have to wait until I add universal quantifiers :)

As Jason suggested, I tried to generalize over t3 before performing the induction over HSubL. However, the proof gets stuck then too (or neither me, nor the automatic tactics I know find how to progress). I attached the file to this mail.

Thank you all again,

Frédéric

---

De: "Lasse Blaauwbroek" <lasse AT blaauwbroek.eu>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Lundi 2 Octobre 2023 21:06:13
Objet: Re: [Coq-Club] Proving transitiviy of simple type system

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.