The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Nada,

Le 19 févr. 2012 à 19:51, Nada Amin a écrit :

> Hello,
> 
> I am trying to prove transitivity of a subtyping relation. On paper, I
> would prove it by induction on the middle term, then inner inductions
> on the size of the left and right derivations. In Coq, I generalize
> (an equality on) the middle term to not loose information, induct on
> it, and then use dependent inductions on the left and right
> derivations. This works for most cases, but I get stuck in one case
> because some of the induction hypotheses have extra equality terms,
> which render them useless as they are impossible to apply.

Maybe that's why on paper you'd use induction on the size of the derivations
and not structural induction on them. I already encountered this in a proof 
about transitivity of a subtyping relation. When you launch the nested 
inductions
on HSubL and HSubR, you will only get induction hypotheses that are restricted
to whatever instance of HMid you are considering (in this case tp_sel t l).
Maybe you'd need hypotheses of the form instead: 
forall deriv, size deriv < size (sub_tp_tsel_r ...) -> ...

It's not completely trivial to define size of derivations in Prop though,
as you can't eliminate from Prop to nat. Neither can you prove wellfoundedness
of a subterm relation on derivations in Prop (that would contradict 
proof-irrelevance!).
One option is to index the derivation by its size, another is to move it to
Set/Type (and optionally show equivalence to the original Prop version).
After all it makes sense because you treat derivations as computational
structures when you can distinguish their sizes.

Hope this helps,
-- Matthieu

> Is there a
> way to get the benefit of dependent inductions (i.e. impossible cases
> are automatically ruled out by inversion), but not have those too
> constraining equalities in the induction hypotheses?
> 
> I'd appreciate any hints or insights about dependent induction.
> 
> For more context:
> 
> This is the subtyping relation:
> https://github.com/namin/dot/blob/master/src/coq/Dot_Rules.v#L149
> 
> I am trying to prove:
> Theorem sub_tp_transitive : forall TMid, transitivity_on TMid.
> where
> Definition transitivity_on TMid := forall E T T',
>  E |= T ~<: TMid -> E |= TMid ~<: T' -> E |= T ~<: T'.
> 
> I start the proof like this:
> 
> introv HSubL HSubR. gen E T T'. gen_eq TMid as TMid' eq. gen TMid' eq.
>  induction TMid; intros;
>    dependent induction HSubL; intros;
>      dependent induction HSubR; simplify_dep_elim; subst; auto; try
> solve [ ... ].
> 
> The case that's causing trouble is when
> HSubL is E |= S' ~<: tp_sel t l derived by sub_tp_tsel_r
> HSubR is E |= tp_sel t l ~<: U' derived by sub_tp_tsel_l
> 
> The problem is that the induction hypotheses have equalities such as U
> = tp_sel t l or S = tp_sel t l. If these equalities weren't there, I
> could make the proof go through.
> 
> Thanks.
> ~n