The Coq mailing list

[Jean-Marie Madiot <jean-marie.madiot AT inria.fr>]

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.