Question about IMP language and proof automation

Stream: new members

[Ilmārs Cīrulis]

I started to learn by working on the simple training language IMP from Concrete Semantics book.

Experimenting with this concept, we see that Isabelle manages to prove many simple equivalences automatically. One example is the unfolding of while loops: Lemma 7.3. WHILE b DO c ∼ IF b THEN c;; WHILE b DO c ELSE SKIP

I have put my current work in Lean here on Github. As one can see, the proof of the lemma 7.3 is simple, but not automatic.

Is there anything I can do to make the proof as easy as in Isabelle, where it is, I suppose, something like an one-liner?

[Henrik Böving]

You can do this one fully automatically by configuring aesop to work with your inductive type I'd say. If you're not willing to do that this is pretty much as good as it gets with core means for now.

[Ilmārs Cīrulis]

Thank you!

[Ilmārs Cīrulis]

Ok, now another question...
I can't prove lemma 7.4 or lemma 7.5. (see at the same place)

I want to use induction H (in the proof of lemma 7.4, for example), but it is not working.

This is the error message:

index in target's type is not a variable (consider using the `cases` tactic instead)
  Com.While b c1

[Ilmārs Cīrulis]

I've tried anything I could imagine but without success.
Send help... :sob:

[Henrik Böving]

lemma L_7_5 (b: BExp) (c1 c2: Com) (Hc: equivalent_commands c1 c2):
    equivalent_commands (Com.While b c1) (Com.While b c2) := by
  intros s t; constructor <;> intro H
  . generalize hfoo : (Com.While b c1) = foo at H
    induction H <;> simp at hfoo
    · sorry
    · sorry
  . sorry

Can be used to get aroudn that limitation of induction, alternatively you can recursively refer to your theorem without induction if you want

[Ilmārs Cīrulis]

Thank you, it really helps! :)

[Ilmārs Cīrulis]

Maybe someone can help with the proof of L_7_9 here?

The last step with both WhileTrue is causing me problems, it seems. I tried to look at Isabella theory at https://isabelle.in.tum.de/dist/library/HOL/HOL-IMP/Big_Step.html , but it didn't help yet.

[Ilmārs Cīrulis]

Wohoo, I did it :)