Cases vs induction tactics goal refactoring

Stream: new members

[Andrea Delmastro]

Hello,
I'm having some trouble figuring out how to complete this demonstration by induction. I have the following code:

inductive small_step_star : com × pstate → com × pstate → Prop
| refl {c : com} {s : pstate} : small_step_star (c, s) (c, s)

| step {c c₁ c₂ : com} {s s₁ s₂ : pstate}:
  small_step (c, s) (c₁, s₁) →
  small_step_star (c₁, s₁) (c₂, s₂) →
  small_step_star (c, s) (c₂, s₂)


infix `↝*`:70 := small_step_star

lemma seq_star {c c₁ c₂ : com} {s₁ s₂ : pstate} :
  (c₁, s₁)↝*(c, s₂) → (c₁ ;; c₂, s₁)↝*(c ;; c₂, s₂) :=
begin
  intro,
  induction ‹(c₁, s₁)↝*(c, s₂)›,
      case refl : { sorry },
      case step: { sorry}
end

I cannot understand why in the refl case c₁ isn't replaced by c and s₂ by s₁, as stated by the definition of small_step_star.refl. I would like the goal to be (c ;; c₂, s₁)↝*(c ;; c₂, s₁) and not (c₁ ;; c₂, s₁)↝*(c ;; c₂, s₂) . If I use cases instead of induction it works well, but in the second case I need the inductive hypotesis to close the demonstration.

[Patrick Johnson]

You need import tactic.induction and then intro h, induction' h to get the goals you want. Next time please post a #mwe.

[Andrea Delmastro]

Thank you! Sorry for the mwe, I wasn't aware of it, next time I'll be more carefull.

[Eric Wieser]

Without a #mwe it's hard to tell, but you might just need the generalizing argument to induction (and not the primed version)

[Anne Baanen]

On the other hand, induction' automatically determines what to generalize, which is much nicer than having to figure it out by hand :)

[Andrea Delmastro]

Thank you, the induction' version worked just as expected, correctly generalizing what I needed