The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

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.