Stream: MetaCoq

Topic: Tactics in MetaCoq

Gregory Malecha (Aug 31 2022 at 02:31):

Has anyone else tried using MetaCoq to write automation-style tactics?

Gregory Malecha (Aug 31 2022 at 17:22):

It looks like other threads in this channel suggest that people have been writing tactics.

Bas Spitters (Sep 25 2022 at 09:08):

Such verified tactics may perhaps also be used to speed up coq, as one could choose not to run the type checker at each Qed.

Théo Winterhalter (Sep 25 2022 at 09:45):

Wouldn't that mean having MetaCoq as part of the trusted code base?

Meven Lennon-Bertrand (Sep 26 2022 at 09:04):

Yes, but it does not seem unreasonable to me to incorporate proven-correct tactics (in particular heavy decision tactics) to a TCB. As a middle ground, you could also try and store whatever kind of certificate these tactics would give you to speed up re-checking. Although you probably need to use SProp to do this properly, otherwise the type-checking of your whole proof might depend on the computational behaviour of those sub-proofs you never created/stored/re-checked?

Théo Winterhalter (Sep 26 2022 at 09:07):

Yeah, but this means trusting the plugin. And also, if it's only a handful of tactics, then there's no way your proof script is going to only use those, and storing which ones are certified or not has a cost I guess.

Meven Lennon-Bertrand (Sep 26 2022 at 09:20):

What I have in mind is having some decision tactic which, in case it succeeds, returns you some i_succeeded(witness) : P : SProp, where witness can be basically anything. If you trust the tactic, you can just avoid rechecking the witness, if you don’t you can have a smaller witness-rechecking as part of the kernel. The main point is that you do not have to encode the witness as a Gallina term and the (re)checking as some fancy conversion problem. But yeah, in any case this will increase the TCB.

Matthieu Sozeau (Sep 26 2022 at 09:31):

I think MetaCoq does not really change anything here. To avoid rechecking proof terms we should rather have a special kind of signed cast that allows the kernel to see it has already checked some term. We could then "trust" this way the outputs of verified tactics.

Gaëtan Gilbert (Sep 26 2022 at 09:32):

is that different from abstract?

Paolo Giarrusso (Sep 26 2022 at 09:33):

it lets you check things once _inside the tactic_ and not at Qed time, which I don't think abstract does?

Matthieu Sozeau (Sep 26 2022 at 09:33):

It would be a less hacky abstract

Paolo Giarrusso (Sep 26 2022 at 09:33):

and that'd also let you ask coqchk to recheck the output or not, I guess

Paolo Giarrusso (Sep 26 2022 at 09:34):

@Meven Lennon-Bertrand Also, in general you'd also want i_succeeded to keep any universe constraints (which would be automatic with Matthieu's proposal)

Matthieu Sozeau (Sep 26 2022 at 09:35):

One thing that would be fun IMHO is to plug in the verified erasure + CertiCoq/ConCert in the kernel as an alternative to vm_compute/native_compute. Then you could run erased versions of your tactics during type-checking.

Paolo Giarrusso (Sep 26 2022 at 09:35):

ditto for the other noncompositional part of type-checking, recursion — tho I don't have an example in mind

Meven Lennon-Bertrand (Sep 26 2022 at 10:02):

Paolo Giarrusso said:

ditto for the other noncompositional part of type-checking, recursion — tho I don't have an example in mind

What do you mean by this?

Paolo Giarrusso (Sep 26 2022 at 10:18):

I mean, "the tactic has typechecked its result hence the kernel needn't check it again" relies implicitly on compositionality of typechecking, so it fails on the exceptions — universe constraints and termination checking.

Concretely, if you had Fixpoint foo : statement. Proof. ... verified_tactic. ... Qed., _and_ verified_tactic calls foo recursively, skipping Qed checking isn't sound even when the tactic is correct. Of course, as I said, I don't have in mind an example where this would actually happen.

Paolo Giarrusso (Sep 26 2022 at 10:19):

and again, Matthieu's approach handles this too just fine, as long as the kernel doesn't skip entirely checking the content of the signed cast.

Meven Lennon-Bertrand (Sep 26 2022 at 10:19):

Ha, I see!

Paolo Giarrusso (Sep 26 2022 at 10:21):

actually, how easy is this "halfway checking" for the kernel? It's not obviously easy even on paper, and ignoring the constraints of the implementation. Say you just reject recursion, what about universes?

Matthieu Sozeau (Sep 26 2022 at 11:01):

You might skip rechecking the typing of the "verified" subterm while still having to do the guard-checking. I guess Conor and Forsberg's work on typechecking "actors" might be a good model to think about these issues.

Matthieu Sozeau (Sep 26 2022 at 11:02):

The cast should definitely record a set of universes and constraints needed, then you would do a kind of subsumption check to see that the subterm fits in its context.

Jason Gross (Oct 13 2022 at 08:43):

Is there a good introduction to programming in the template monad? (I'm trying to prove Löb's theorem in Coq on top of MetaCoq, and the first step is that I need to write a Gallina function quote : Ast.term -> Ast.term (and then a function that says something like forall (t T : Ast.term) (pf : t is well-typed of type T), quote t and quote T are well-typed of type Ast.term and quote pf is a well-typed quoted proof that quote t has type quote T), and I'm wondering if I can use the template monad to skip writing quote by hand

Théo Winterhalter (Oct 13 2022 at 08:50):

If you use the monad then I expect you will have Ast.term -> TM Ast.term.

Yannick Forster (Oct 13 2022 at 08:52):

I think the quickest way to go is manually following this pattern:

From MetaCoq Require Import Template.Loader bytestring.
Require Import List.
Import ListNotations.

Open Scope bs.

Fixpoint quote_nat (n : nat) : Ast.term :=
  match n with
  | 0 => <% 0 %>
  | S n => Ast.tApp <% S %> [ quote_nat n ]
  end.

Fixpoint quote (t : Ast.term) : Ast.term :=
  match t with
  | Ast.tRel n => Ast.tApp <% Ast.tRel %> [ quote_nat n ]
  | _ => Ast.tVar "todo"
  end.

Yannick Forster (Oct 13 2022 at 08:55):

You could imagine writing a function generate_quote : forall A : Type, TemplateMonad (A -> Ast.term), but for this to be applicable to Ast.term itself it would need to support nested inductives, and I guess that's way harder to get right

Last updated: Apr 20 2024 at 09:01 UTC