The Coq mailing list

[Jason Hu <fdhzs2010 AT hotmail.com>]

What you claim is not true. There is a standard exercise of transitivity elimination (akin to cut elimination in proof theory) for many common systems with subtyping. This process is not necessarily obvious, nor known how to do for all systems, but many important
 systems do have it, e.g. F-sub. For your example, alpha <: alpha is indeed required, however, not T <: T for all T. That is, reflexivity is probable. Similarly, F-sub's transitivity is also probable. You can find many proofs by looking up POPLMark.

Thanks,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Lasse Blaauwbroek <lasse AT blaauwbroek.eu>
Sent: Monday, October 2, 2023 6:15:40 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proving transitiviy of simple type system

 

Although Jean-Marie's and Jason's generalizations both work here, I
believe that the crucial point is still that this subtyping relation is
trivial. As far as I know, for most sufficiently "interesting" subtyping
relations, transitivity and reflexivity are not provable without
axiomatizing them. That is, you have to add reflexivity and transitivity
constructors (unless you modify all other constructors such that
transitivity is "built-in", but that amounts to the same thing). For
example, as soon as you have type variables you will not be able to
prove "\alpha < \alpha" without the axiom.

I'd be curious to know what kind of type-system you have in mind where
this is not needed?

On 02-10-2023 23:43, Jean-Marie Madiot wrote:
> Hello Frédéric,
>
> One standard "Coq trick" that you may already know is to generalize
> the statement before performing the induction, typically by doing
> something like "revert t3 HSubR; induction HSubL"  or "revert t1
> HSubL; induction HSubR" in your example.
>
> However typeSub is contravariant in one of its argument, which makes
> things more interesting: only generalizing for all "HSubL" or for all
> "HSubR" won't be enough, you need to be able to switch sides.
>
> Suppose that you have a coarser (hence non trivial) subtyping relation
> such as
>
> Inductive typeSub : type -> type -> Prop :=
> | SubTUnit : typeSub TUnit TUnit
> | SubTFunUnit : forall ti to, typeSub (TFun ti to) TUnit
> | SubTFun : forall ti1 to1 ti2 to2, typeSub ti2 ti1 -> typeSub to1 to2
> -> typeSub (TFun ti1 to1) (TFun ti2 to2).
>
> Infix "<" := typeSub.
>
> Then you can generalize on both sides in this way:
>
> Lemma trans_aux t1 t2 : t1 < t2 -> (forall x, x < t1 -> x < t2) /\
> (forall x, t2 < x -> t1 < x).
> Proof.
>   intros HSub; induction HSub; split; intros x Hx; inversion Hx;
> subst; constructor; firstorder.
> Qed.
>
> Lemma trans: forall t1 t2 t3, t1 < t2 -> t2 < t3 -> t1 < t3.
> Proof.
>   intros t1 t2 t3 HSubL.
>   apply trans_aux, HSubL.
> Qed.
>
> Regards,
> Jean-Marie
>
> Le 02/10/2023 à 19:53, Frederic Fort a écrit :
>> 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.