Zulip Chat Archive

Stream: new members

Topic: Cases vs induction tactics goal refactoring

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

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₂) :=
  induction ‹(c₁, s₁)↝*(c, s₂)›,
      case refl : { sorry },
      case step: { sorry}

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