Keeping information when using induction?

Question

I am using the Coq Proof Assistant to implement a model of a (small) programming language (extending an implementation of Featherweight Java by Bruno De Fraine, Erik Ernst, Mario Südholt). One thing that keeps coming up when using the induction tactic is how to preserve the information wrapped in type constructors.

I have a sub typing Prop implemented as

Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3
| st_extends : forall C D,
    extends C D ->
    sub_type (c_typ C) (c_typ D).

Hint Constructors sub_type.

where extends is the class extension mechanism as seen in Java, and typ represents the two different kinds of types available,

Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ : rname -> typ.

An example of where I would like type information to be preserved is when using the induction tactic on a hypothesis like

H: sub_type (c_typ u) (c_typ v)

E.g. in

u : cname
v : cname
fsv : flds
H : sub_type (c_typ u) (c_typ v)
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

using induction H. discards all information about u and v. The st_refl case becomes

u : cname
v : cname
fsv : flds
t : typ
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

As you can see the information that u and v are related to the typ constructors in H, and thus to t, is lost. What is worse is that due to this Coq is unable to see that u and v must in fact be the same in this case.

When using the inversion tactic on H Coq succeeds in seeing that u and v are the same. That tactic is not applicable here however, as I need the induction hypotheses that induction generates to prove the st_trans and st_extends cases.

Is there a tactic that combines the best of inversion and induction to both generate induction hypotheses and derive equalities without destroying information about what is wrapped in the constructors? Alternatively, is there a way to manually derive the information I need? info inversion H and info induction H both show that a lot of transformations are applied automatically (especially with inversion). These have led me to experiment with the change tactic along with let ... in construction, but without any progress.

Lab

Answer 1

This is a general problem when you need to induct over a hypothesis with a dependent type (sub_type (c_typ u) (c_typ v)) whose parameters have a particular structure (c_typ u). There is a general trick, which is to selectively rewrite the structured parameter to a variable, keeping the equality in the environment.

set (t1 := c_typ u) in H; assert (Eq1 : t1 = c_typ u) by reflexivity; clearbody t1.
set (t2 := c_typ u) in H; assert (Eq2 : t2 = c_typ u) by reflexivity; clearbody t2.
induction H. (*often "; try subst" or "; try rewrite Eq1; try rewrite Eq2" *).

Since Coq 8.2, this common set-assert-clearbody pattern is performed by the built-in tactic remember term as ident in *goal_occurences*.

Here's a silly lemma proved using this tactic.

Lemma subtype_r_left_equal :
  forall r1 t2, sub_type (r_typ r1) t2 -> r_typ r1 = t2.
Proof.
  intros.
  remember (r_typ r1) as t1 in H.
  induction H.
  congruence.
  solve [firstorder].
  discriminate.
Qed.

---

Bonus tip (from experience, but it's been a while so I don't remember the details): when you're doing fairly syntactic reasoning on type systems (which tends to be the case when you do these kinds of mechanical proofs), it can be convenient to keep typing judgements in Set. Think of typing derivations as objects you're reasoning about. I remember cases where it was convenient to introduce equalities on typing derivation, which doesn't always work with typing derivations in Prop.

---

With your Problem.v, here's a proof of the reflexivity case. For transitivity, I suspect your induction hypothesis isn't strong enough. This may be a byproduct of the way you simplified the problem, though transitivity often does require surprisingly involved induction hypotheses or lemmas.

Fact sub_type_fields: forall u v fsv,
  sub_type (c_typ u) (c_typ v) -> fields v fsv ->
  exists fs, fields u (fsv ++ fs).
Proof.
  intros.
  remember (c_typ u) as t1 in H.
  remember (c_typ v) as t2 in H.
  induction H.
  (* case st_refl *)
  assert (v = u). congruence. subst v t.
  exists nil. rewrite <- app_nil_end. assumption.
  (* case st_trans *)
  subst t1 t3.
  (* case st_extends *)
Admitted.

Hortenciahortensa

@Matthias: Does generalize dependent H0. induction H. help? It's all I can offer without having something I could feed to Coq myself (your question is missing more definitions than I care to fill out, I'm not familiar enough with Java's type system). – Enfold

That did not persuade Coq to do the right thing. I have created a zip file containing just the definitions necessary to play with the Fact I am having trouble proving: Problem.v contains the definitions and Fact, the rest are auxiliaries. I appreciate your help. – Lab

@Matthias: For reflexivity, you just need to rewrite the goal using the available equalities. For a one-shot, I find it simplest to assert the equality, then use it. If this comes up in a lot of proofs, you might start defining tactics that look for common patterns. – Enfold

the tactics remember and revert are maybe even simplier to use. – Seraphine

Answer 2

I ran into a similar problem and Coq 8.3's "dependent induction" tactic took care of business.

Realgar

In my case it was actually because the proof was impossible due to a problem in the semantic rules I had defined. With the problem fixed the proof was relatively straight-forward. :-) And in general I have found that it is a good idea to take a step back and check the definitions I am using if something is too hard to prove. – Lab

does it ever "mean" something if you need both? like if your induction fails it's often because your induction hypothesis is too weak. – Coz

Answer 3

I was sure CPDT had some commentary on this issue, but it's not entirely obvious where it is. Here are some links:

1. http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.html Section "Predicates with Implicit Equality" shows perhaps the very simplest case where Coq "loses information" (on a destruct, rather than an induction.) It also explains WHY this information is lost: when you destruct a type applied to an argument which is not a free variable, those types are replaced with free variables first (which is why Coq loses the information.)

2. http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html Section "Methods for Avoiding Axioms" shows some tricks for avoiding axiom K, including the "equality trick" described by Gilles. Search for "using a common equality-based trick for supporting induction on non-variable arguments to type families"

I think that this phenomenon is closely related to dependent pattern matching.

Mainspring