SF kata

Stream: Program verification

[Reid Barton]

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

[Reid Barton]

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

[Simon Hudon]

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.

[Simon Hudon]

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.

[Simon Hudon]

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

[Reid Barton]

I see, interesting.

[Reid Barton]

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

[Simon Hudon]

Yes, let me show you a comparison

[Simon Hudon]

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

[Reid Barton]

Does value_type have a type?

[Simon Hudon]

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 }

[Reid Barton]

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

[Simon Hudon]

Exactly

[Reid Barton]

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

[Reid Barton]

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

[Simon Hudon]

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.

[Reid Barton]

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

[Reid Barton]

Can Ltac things return values?

[Simon Hudon]

Exactly

[Reid Barton]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

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

[Simon Hudon]

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 :)

[Reid Barton]

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

[Simon Hudon]

Yes and values are encoded as particular terms

[Reid Barton]

And then just implement Forth in Ltac

[Simon Hudon]

That is one approach :upside_down:

[Simon Hudon]

Maybe a continuation passing style would be a bit easier

[Simon Hudon]

Not very pretty still

[Simon Hudon]

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

[Simon Hudon]

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.