coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nada Amin <namin AT alum.mit.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] dependent induction and useless induction hypotheses
- Date: Sun, 19 Feb 2012 19:51:22 +0100
- Authentication-results: mr.google.com; spf=pass (google.com: domain of nada.amin AT gmail.com designates 10.180.7.231 as permitted sender) smtp.mail=nada.amin AT gmail.com; dkim=pass header.i=nada.amin AT gmail.com
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. 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
- [Coq-Club] dependent induction and useless induction hypotheses, Nada Amin
- Re: [Coq-Club] dependent induction and useless induction hypotheses, Matthieu Sozeau
Archive powered by MhonArc 2.6.16.