Using Induction tactic on Props

[woong8556]

I was always curious about it, and it finally became a trouble in midterm exam.

When I try to use induction tactic, I often face the following problem: on which term am I using induction?

For example, let's assume we have to use induction on H : ev (3 * n). Here, ev is the inductively defined nat->prop thing, prop of nat being even number, as we learned in class.

If I use induction H, I think that this starts an induction with * (which is inductively defined), rather than ev (which is the thing I intended).

How can I deal with this trouble?

[jaewooklee93]

No, it properly performed induction on ev as you intended. If your context was H: ev (3*n), induction H transforms it along the inductive definition of ev. ev has only two constructors, ev_0: ev 0 and ev_SS: ev m -> ev (2+m). Therefore, your ev has two possibilities

By the way, even though * is inductively defined, actually you cannot use induction on * because induction only deal with Prop(our ev) or Set(nat, list X, ...) defined by Inductive. However * was not defined by Inductive but defined by fix(Fixpoint), which is a quite different thing from Inductive.

So, the answer for your question is, induction always acts on the whole H, not partially.

[woong8556]

Hmm. Thanks.

When I was doing the same in the exam, however, I couldn't see the terms like H1: 0=(n + (n + (n + 0)). When I tried this with inversion tactic rather than induction tactic, I saw the same H1: 0=(n + (n + (n + 0)) thing (and it almost brought me to the end of the proof, but I realized I must do this inductively. I needed IH.) but when I used induction tactic, I couldn't see any more assumptions. I'm quite sure the induction tactic was applied in some wrong way.

We might encounter this trouble in general cases. We may be interested in doing induction in other inductive terms, rather than the inductive term induction H automatically unfolds. I'm curious about this. Thanks.

[jaewooklee93]

Oh.. sorry. You're definitely right. I confused induction with inversion. I will try to think about it more. However, generally I prefer to use inversion for Prop, and that may be the reason of my confusion. Of course, induction is usually stronger than inversion, but sometimes it creates an over-complicated induction hypothesis. I'm curious about what the specific statement you faced is, so please share your Lemma if you don't mind.

In my case, I didn't use ev at all in solving Problem 7, I rather used inversion n using tactic, which is not in the textbook, but in the official documentation.

[jaewooklee93]

@woong8556 Well... I've tried it for a long time, however I must confess that I failed to use induction H properly. So I should agree with you that induction on ev (3*n) doesn't give a meaningful result. To the best of my knowledge, induction on Prop was only used for ev n in our homework like this.

Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  intros; induction H0; try assumption;
  apply IHev; inversion H; apply H2.
Qed.

I think this is a really special case, because H0: ev n has the simplest form of ev. I guess that we'd better to use induction only on nat or list except for such rare cases.

I just guessed your proof structure and solved the problem in that way. Also, I avoided induction on Prop except for the very first step of Theorem ex, and used only tactics in the textbook.

Please check this out.

Require Import Arith.

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

Theorem two_fold: forall P: nat -> Prop,
  P 0 -> P 1 ->
  (forall m, P m -> P (2+m)) ->
  forall n, P n.
Proof.
  intros.
  assert (forall k, P k /\ P (1+k)).
  intros; induction k; split; try destruct IHk;
  try assumption; apply H1; assumption.
  apply H2.
Qed.

Theorem div3: forall n,
  ev (3*n) -> ev n.
Proof.
  apply (two_fold (fun n => ev (3*n) -> ev n));
  intros; try constructor; try simpl in H0.
  - inversion H; inversion H1.
  - apply H; repeat rewrite <- plus_n_Sm in H0;
    inversion H0 ;inversion H2; inversion H4; apply H6.
Qed.

Theorem ex: forall n, ev n ->
  exists k, n=2*k.
Proof.
  intros; induction H.
  - exists 0; reflexivity.
  - inversion IHev as [x H0]; exists (1+x); rewrite H0;
    rewrite mult_plus_distr_l; reflexivity.
Qed.

Theorem main: forall m n,
  2*m=3*n ->
  exists k, n=2*k.
Proof.
  intros; apply ex; apply div3; rewrite <- H.
  assert (forall k,ev (2*k)).
  induction k; simpl; try rewrite <- plus_n_Sm;
  constructor; assumption.
  apply H0.
Qed.

If you want to take a look at small steps of the proof, just replace all the semicolons ; to periods .

[woong8556]

Wow! I owe you thanks, and I feel sorry not giving you my proofs earlier. The two_fold lemma allows us to smash the problem. Very impressive.

My intentions to proving the problem was following the steps below:

1. forall m t, (2*m)=t -> ev t
2. forall n, ev (3*n) -> ev n
3. forall n, ev n -> exists k, n=(2*k) So it is basically identical to your intention. I was stuck in 2.

I think we will learn this in further curriculum, as I can see MoreInd section in http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html , so I will close this. Thank you very much @jaewooklee93 !

[jaewooklee93]

@woong8556 It is my pleasure. I want to make small number of additional comment here.

1. I think MoreInd will not be covered in the course. Because if you examine chapter dependencies, MoreInd is indicated as an optional chapter, and our current position Imp and its following doesn't depends on MoreInd.
2. However, it seems that MoreInd is worth studying. There is induction n using as well. I used apply (two_fold (fun n => ev (3*n) -> ev n)); at the very first line of Theorem div3, which makes P:=(fun n => ev (3*n) -> ev n) explicitly, but it can be replaced by just induction n using two_fold, which is much simpler, since it automatically chooses P.
3. The important thing is not just knowing two_fold. Knowing why we must use two_fold here is much important. That's because the proof of ev (3*n) -> ev n is totally different for even numbers and odd numbers. For an even n, ev (3*n) is true and you have to prove ev n. However, for an odd n, ev (3*n) is false, so there is nothing to prove. This difference between two groups means that you have to prove the theorem separately. First prove it for even numbers and then prove it for odd numbers. For this work, we exploit two_fold.

4. Basic induction with P n->P (1+n) can be quite weak in some situations like this. You can easily find that there are other induction principles other than two_fold. There are several examples.

   Theorem strong: forall P: nat->Prop,
   (forall m, (forall k, k<m->P k)->P m) ->
   forall n, P n.

   It is known as strong induction (강한 수학적 귀납법).

   Theorem induction_on_length:
   forall (X:Type) (P: list X->Prop),
   P nil ->
   (forall n l, (forall l', length l'=n -> P l') ->
    length l=1+n -> P l) ->
   forall l, P l.

   There are some cases that you cannot prove P t -> P (h::t) directly, but you can prove P l'->P l, where 1+length l'=length l, then induction_on_length would be useful.

5. All these things are about how to bypass the defect of direct application of induction on ev (3*n). However, it seems that remember tactic explained in MoreInd can be useful as a more direct cure for that defect. There is a sentence said:

   The problem is that induction over a Prop only works properly over completely general instances of the Prop, i.e. one in which all the arguments are free (unconstrained) variables. In this respect it behaves more like destruct than like inversion.

   There are some exercises, we got a trouble when we use only destruct, since it destroyed some of our information, so we used destruct ~ eqn instead. I guess that remember does the similar thing for induction.

[jaewooklee93]

One more last comment here.

I think you don't need to close this issue now, because question you posted seems really precious and hits the nail on the head, and other students may have the same question about induction, while it may not be covered in the class later. So if you remain this issue open, more students can refer to our discussion.

[jeehoonkang]

@jaewooklee93 I agree.

[woong8556]

Really thank you @jaewooklee93 for being specific!

The strong induction and induction on length strategies also seem to be powerful tools.

I just reminded the point that induction on ev (3*n) -> ev n needs to be separated into two problems, for odds and for evens. It really is important!

I had not realized that this topic may not be studied on our course. I reopened it so other students can also think about this problem.

[woong8556]

And I also re-read the first comment @jaewooklee93 left. Thanks for clarifying the fact that fixpoint-defined functions can't be inversed by induction. I think I need to study harder.

[jaewooklee93]

I realized that if you want to induction on H: ev (3*n) directly, you have to use remember tactics as follows: remember (3*n) as m. Then H transforms into H: ev m and induction H will properly work. However, that induction doesn't help you at this situation. Because the case of 3*n=2*k doesn't give any evidence for the case of 3*n=2*k+2, so unfortunately induction hypothesis generated by H is useless here...