CODEWITHSUNDEEP
coqcoq-tactic
Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6589

Why does removing assumptions change the behaviour of the induction tactic?

I am trying to show that the various definitions of the reflexive-transitive closure are equivalent. Here is code that works:

Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Relations.Relation_Operators.

Hint Constructors clos_refl_trans.
Hint Constructors clos_refl_trans_1n.

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A), 
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z _ IH1 _ IH2]; eauto.
  induction IH1; eauto.
Qed.

Note the underscores denoting thrown away variables. If I give those variables names, the automation fails:

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A),
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z H1 IH1 H2 IH2]; eauto.
  induction IH1; eauto. (* three subgoals left *)
Fail Qed.

Upon examination, we find that the inner induction hypotheses are weaker in the second example. It looks like the induction tactic is detecting a behind-the-scenes dependency between the problematic assumptions and the object of the inner induction.

Is this documented anywhere? What's the rationale, and how can I predict that it will happen?

Upvotes: 0

Views: 68

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

I think that basically it will make your induction hypothesis depend on all the assumptions that are linked to the thing you induct on. If you do induction on x : P n m in a context where you have h : Q n and y : h = h' it will probably include them in the mix. In a lot of cases this does not correspond to what you want and doing some clean beforehand might make your induction suddenly go through.

There is also a very useful variant of induction, induction ... in which allows you to specify what part of the context you want to keep when doing the induction.

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A),
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z H1 IH1 H2 IH2]; eauto.
  induction IH1 in z, IH2 |- *. all: eauto.
Qed.

Here you get a warning that I don't really understand to be honest (Cannot remove x and Cannot remove y) but you get the expected result. This also has the advantage that it lets you specify what should be generalised.

Maybe someone has a better explanation though.

Upvotes: 2

Related Questions