## Stream: new members

### Topic: Cases vs induction tactics goal refactoring

#### Andrea Delmastro (Mar 31 2022 at 13:26):

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 (Mar 31 2022 at 13:37):

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 (Mar 31 2022 at 14:03):

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

#### Eric Wieser (Mar 31 2022 at 22:40):

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 (Apr 01 2022 at 08:35):

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

#### Andrea Delmastro (Apr 01 2022 at 08:54):

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

Last updated: Dec 20 2023 at 11:08 UTC