The Coq mailing list

[Jason Hu <fdhzs2010 AT hotmail.com>]

> 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".

This shouldn't occur. That means you did your case analysis incorrectly. If you do an induction on typeSub t1 t2, and then an inversion on typeSub t2 t3, you should have only two cases left. Then IH should just work. If you IH doesn't discharge the goal, it means it's not general enough. Based on how you write your lemma, I think that you should generalize t3 before doing induction on typeSub t1 t2​. Then IH should be general enough.

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 1:53 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] Proving transitiviy of simple type system

 

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.