Formal verification of simple imperative language

Stream: Program verification

[Leo Ericson]

Hello!

I have done a translation of the correctness proof in Concrete Semantics with Isabelle/HOL to Lean (well, only the forward direction). I saw before that there was interest in having a similar proof in Mathlib's archive so I'm asking if there is interest in my formalization too. If so I'm willing to put up a PR (it still depends on LoVelib from Hitchhiker's Guide). The language has addition, boolean expressions, if-statements and while-loops. I haven't put it up on Github yet though.

Edit: I've "removed" the dependency on LoVe Library by copying over the definitions that are necessary. I'm not sure if this is the approach.

[Huỳnh Trần Khanh]

how about... uploading your code on github first? :grinning:

[Leo Ericson]

Fair enough, here ya go: https://github.com/Zetagon/mathlib/blob/master/archive/whilecc.lean
I haven't made efforts to make it conform to Mathlib's conventions yet

[Mario Carneiro]

star is relation.trans_gen. The lemmas about bool, le, and list should either exist or be placed where they should go in mathlib. For the rest, it looks good for the mathlib archive once it is adjusted to mathlib style, although I think you should think about how to turn this into something more reusable so that it can go into mathlib proper

[Leo Ericson]

hmm I have mostly thought about this as an example others could study as it is quite specific to a particular compiler. I'm not quite sure in what way it would be reusable by others. What did you have in mind?

[Huỳnh Trần Khanh]

Maybe you should just modify your code to follow mathlib conventions and make a pull request. Because this code can't really be made reusable. But it is a very educational example. Be sure to add a docstring mentioning the Logical Verification course!

[Huỳnh Trần Khanh]

Oh, and Concrete Semantics too!

[Eric Wieser]

I wonder if @Jasmin Blanchette is interested in pull requests to https://github.com/blanchette/logical_verification_2020 to update it to the latest mathlib, or whether it's better frozen in time

[Jasmin Blanchette]

It's frozen in time. I ported it already to 2021. See https://github.com/blanchette/logical_verification_2021 . We don't use much of mathlib; it's easy to port.

[Kevin Buzzard]

When will you port to Lean 4?

[Jasmin Blanchette]

Once mathlib has been ported. I'm a late adopter anyway. ;)

[Jasmin Blanchette]

@Eric Wieser the repository you see is just a dump. It's not meant to be a development repository, and I don't expect pull requests there. The sources, including the master files that generate problem/solution pairs, are in a separate (private) repository. If you want to suggest a change, I'll be happy to discuss it.

(Incidentally, if you know how to disable PRs on GitHub, I'm all ears.)

[Eric Wieser]

Ah, my apologies - I think the best you can do is put a comment in the readme to that effect.

[Jannis Limperg]

Jasmin Blanchette said:

(Incidentally, if you know how to disable PRs on GitHub, I'm all ears.)

You could maybe archive the Github repo.

[Eric Wieser]

That doesn't let you push to the repo though

[Huỳnh Trần Khanh]

You can set interaction limits. Settings > Temporary interaction limits.