Zulip Chat Archive

Stream: Program verification

Topic: SF kata


view this post on Zulip Reid Barton (Jun 13 2020 at 14:44):

Hi @Simon Hudon, I saw your solution to the "Evaluating the type safety of a toy language" kata using custom automation;
I found solve_by_elim was sufficient, once I realized it was running into its (very low) default depth limit in some cases

view this post on Zulip Reid Barton (Jun 13 2020 at 14:47):

Is it easy to explain what the tactics you wrote do? I didn't look at them closely.

view this post on Zulip Simon Hudon (Jun 13 2020 at 14:53):

Actually, what I did was porting my Coq solution to Lean. And Ltac's pattern matching has an interesting backtracking behavior that I did not try to adopt to a more idiomatic Lean approach. I built a monad transformer that does unbounded backtracking so that I can search
multiple assumptions that match each other precisely. I'm not sure that it's the best way to do it (it probably has a bunch of inefficiencies because of brute force searches) but I thought it conveyed the ideas well.

view this post on Zulip Simon Hudon (Jun 13 2020 at 14:59):

You could write:

do a <- mvar,
   b <- mvar,
   c <- mvar,
   goal ``(%%c -> %%a),
   h <- hyp ``(%%c -> %%b),
   h' <- hyp ``(%%b -> %%a),
   lift $ do x <- intro1, apply (h' (h x))

Then we iterate through the assumptions instantiating meta variables and, every time you try a solution, you can back track to the latest choice point to try something different, abandon meta variable assignments. I think it's a nice way of writing nested loops. Especially when consider that you could have a list of patterns that you iterate through using mmap. Then, each element of the list can make a choice point that you can jump back to.

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:01):

As an exemplar for the kata, maybe your solution would be better than mine though

view this post on Zulip Reid Barton (Jun 13 2020 at 15:08):

I see, interesting.

view this post on Zulip Reid Barton (Jun 13 2020 at 15:11):

Is this baked into Ltac's equivalent of the tactic monad? (note: I know nothing about Ltac)

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:15):

Yes, let me show you a comparison

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:17):

In Ltac, for this problem, I wrote the following tactic:

Ltac value_type :=
  match goal with
  | [ h : nvalue ?v |- (|- ?v \in Nat) ] => apply (nvalue_has_type _ h)
  | [ h : lvalue ?v |- (|- ?v \in List) ] => apply (lvalue_has_type _ h)
  end.

It tells you that if v is a term that is also natural number value nvalue, then, as a term, it has type Nat. ?v is a meta variable that can coordinate the various components of the goal that you're matching on

view this post on Zulip Reid Barton (Jun 13 2020 at 15:19):

Does value_type have a type?

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:20):

In Lean, I could have written (but did not):

meta def value_type : tactic unit := do
{ v <- var,
  `( %%v : Nat)  target,
  h <- hyp ``(nvalue %%v),
  lift $ mk_app ``nvalue_has_type [h] >>= apply } <|>
do { v <- var,
     `( %%v : List)  target,
     h <- hyp ``(nvalue %%v),
     lift $ mk_app ``nvalue_has_type [h] >>= apply }

view this post on Zulip Reid Barton (Jun 13 2020 at 15:20):

So in Lean, we have failure baked in to tactic but not backtracking

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:20):

Exactly

view this post on Zulip Reid Barton (Jun 13 2020 at 15:21):

Oh, I guess your value_type also exhibits backtracking because there could be multiple nvalue hypotheses in the context.

view this post on Zulip Reid Barton (Jun 13 2020 at 15:22):

I mean, in this example, there's no way that backtracking can help.

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:22):

Reid Barton said:

Does value_type have a type?

No, that's the alien thing for Lean user. In Lean, a tactic is a definition of type tactic. In Coq, a Definitionis something in the logic, Ltac defines something completely different and uses a different notation too -- whereas Lean has different notations for tactic, it's only syntactic sugar on top of Lean terms.

view this post on Zulip Reid Barton (Jun 13 2020 at 15:22):

But in principle, this | [ h : nvalue ?v |- (|- ?v \in Nat) ] would create a choice point that would try a second h' : nvalue ?v?

view this post on Zulip Reid Barton (Jun 13 2020 at 15:22):

Can Ltac things return values?

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:23):

Exactly

view this post on Zulip Reid Barton (Jun 13 2020 at 15:23):

Does Ltac give you some kind of cut to prevent this?

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:23):

No. They have tricks to do computations in Ltac but it is a hack

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:23):

It probably does, I can't think of what it is though

view this post on Zulip Reid Barton (Jun 13 2020 at 15:24):

OK, thanks for the explanations. I have seen some bits of Ltac before, but never tried to understand what exactly was going on.

view this post on Zulip Reid Barton (Jun 13 2020 at 15:24):

I assume the hacks are, like, stuff some state in the proof state somehow.

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:25):

I have recently spent more time with Software Foundations. It is truly a wonderful book. I'm currently in Programming Language Foundations. So much fun :)

view this post on Zulip Reid Barton (Jun 13 2020 at 15:25):

I mean all you really need is a stack of values, right? :upside_down:

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:25):

Yes and values are encoded as particular terms

view this post on Zulip Reid Barton (Jun 13 2020 at 15:26):

And then just implement Forth in Ltac

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:27):

That is one approach :upside_down:

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:29):

Maybe a continuation passing style would be a bit easier

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:29):

Not very pretty still

view this post on Zulip Simon Hudon (Jun 13 2020 at 15:32):

It's interesting to take a closer look at Coq and, for me, see that the pain points are not necessarily what I thought they would be but also, how nice it can be to write proofs and automation. The experience is more enjoyable than I expected

view this post on Zulip Simon Hudon (Jun 13 2020 at 18:07):

Update: I just read up on match in Ltac. It turns out, by default, the scope of back tracking is one match statement: if the pattern of one branch matches then the other branches are attempted. If anything after the match fails, the next pattern will not be attempted. If you use lazymatch instead of match, when the body of a branch fails, the whole match fails. New branches are not attempted. If you use multimatch, you get full back tracking.


Last updated: May 08 2021 at 22:13 UTC