Has anyone else tried using MetaCoq to write automation-style tactics?
It looks like other threads in this channel suggest that people have been writing tactics.
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.
Wouldn't that mean having MetaCoq as part of the trusted code base?
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?
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.
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.
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.
is that different from abstract
?
it lets you check things once _inside the tactic_ and not at Qed time, which I don't think abstract
does?
It would be a less hacky abstract
and that'd also let you ask coqchk
to recheck the output or not, I guess
@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)
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.
ditto for the other noncompositional part of type-checking, recursion — tho I don't have an example in mind
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?
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.
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.
Ha, I see!
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?
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.
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.
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
If you use the monad then I expect you will have Ast.term -> TM Ast.term
.
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.
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: Oct 13 2024 at 01:02 UTC