Doing induction on hypothesis

[minitu]

I don't think I still fully grasp the idea of doing induction on hypothesis. For example, in the proof of step__eval of Smallstep.v,

Lemma step__eval : forall t t' n,
     t ==> t' ->
     t' || n ->
     t || n.
Proof.
  intros t t' n Hs. generalize dependent n.
  induction Hs; intros.
  ...

The hypothesis Hs is in the form of t ==> t', and doing induction on this makes it easy to prove the goal. But I still don't understand what induction Hs does exactly...

[jaewooklee93]

Inductive set step (==>) has three constructors.

One base case, ST_PlusConstConst : P (C n1) (C n2) ==> C (n1 + n2) and two inductive steps. ST_Plus1 : t1 ==> t1' → P t1 t2 ==> P t1' t2 ST_Plus2 : value v1 → t2 ==> t2' → P v1 t2 ==> P v1 t2'

The original goal is forall n : nat, t' || n -> t || n. Let's call this goal Q(t,t'). After induction on t ==> t', the goal is transformed into three questions,

(1) If t=P (C n1) (C n2) and t'=C (n1 + n2), does Q(t,t') hold?

(2) If t=P t1 t2 and t'=P t1' t2, where t1 ==> t1' so Q(t1,t1') from induction hypothesis, does Q(t,t') hold?

(3) If t=P v1 t2 and t'=P v1 t2', where value v1 and t2 ==> t2' so Q(t2,t2') from induction hypothesis, does Q(t,t') hold?

There is no way to construct the element t ==> t' other than those three ways. You may understand why answering these three questions is enough to show that original assertion holds.

[minitu]

@jaewooklee93 Thank you so much!