## Stream: Program verification

### Topic: SF kata

#### 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

#### 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.

#### 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.

#### 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. #### Simon Hudon (Jun 13 2020 at 15:01): As an exemplar for the kata, maybe your solution would be better than mine though #### Reid Barton (Jun 13 2020 at 15:08): I see, interesting. #### 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) #### Simon Hudon (Jun 13 2020 at 15:15): Yes, let me show you a comparison #### 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 #### Reid Barton (Jun 13 2020 at 15:19): Does value_type have a type? #### 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 }


#### Reid Barton (Jun 13 2020 at 15:20):

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

Exactly

#### 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.

#### Reid Barton (Jun 13 2020 at 15:22):

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

#### 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.

#### 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?

#### Reid Barton (Jun 13 2020 at 15:22):

Can Ltac things return values?

Exactly

#### Reid Barton (Jun 13 2020 at 15:23):

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

#### Simon Hudon (Jun 13 2020 at 15:23):

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

#### Simon Hudon (Jun 13 2020 at 15:23):

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

#### 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.

#### Reid Barton (Jun 13 2020 at 15:24):

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

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

#### Reid Barton (Jun 13 2020 at 15:25):

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

#### Simon Hudon (Jun 13 2020 at 15:25):

Yes and values are encoded as particular terms

#### Reid Barton (Jun 13 2020 at 15:26):

And then just implement Forth in Ltac

#### Simon Hudon (Jun 13 2020 at 15:27):

That is one approach :upside_down:

#### Simon Hudon (Jun 13 2020 at 15:29):

Maybe a continuation passing style would be a bit easier

#### Simon Hudon (Jun 13 2020 at 15:29):

Not very pretty still

#### 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

#### 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