Stream: MetaCoq

Topic: SafeChecker on open terms?


view this post on Zulip Jason Gross (Apr 15 2023 at 19:05):

How feasible would it be to write a version of the safechecker that works well with ASTs that refer to axioms and/or context variables? That is, I want a version of the safechecker that takes in some extra information about the ASTs (a Boolean for each subterm saying whether or not the term can be matched on, which will be provided by running some program in the template monad), performs Gallina matching only when the extra information says the subterm can be matched on, and otherwise emits a collection of side conditions (or consumes a collection of pre-computed side conditions), corresponding to the typing problems for the subterms that are not to be matched on.

view this post on Zulip Jason Gross (Apr 15 2023 at 19:06):

This could be specialized to the normal safechecker by saying "every subterm can be matched on", and then the side conditions are trivial.

view this post on Zulip Jason Gross (Apr 15 2023 at 19:07):

But it could also be used to safecheck all of the quotation theory in a systematic way.

view this post on Zulip Jason Gross (Apr 15 2023 at 19:10):

(Which, in conjunction with moving the safechecker to be a partial function that can be fueled without a SN axiom, and splitting off the proofs so that we can get unsquashed typing judgments, makes me optimistic about actually getting to Löb's theorem)

view this post on Zulip Jason Gross (Apr 18 2023 at 07:16):

(Does this proposal make sense?)

view this post on Zulip Théo Winterhalter (Apr 18 2023 at 07:40):

And do you think there would a way to do this without impacting the extracted checker? I guess we could also cheat and use the safe checker (almost) as is but by using evars or something similar to replace the subterms you don't want to analyse?

view this post on Zulip Jason Gross (Apr 18 2023 at 07:57):

There's the dumb solution of "duplicate all the code". There's a slightly more clever solution where, if we set things up right, we should be able to do something like Definition safechecker_component_to_extract := Eval cbv beta iota delta [general_safechecker_component] in general_safechecker_component all_subterms_can_be_discriminated., (though I think we can only do this with the non-recursive part of functions (and will need to duplicate the Fix_F invocation or whatever).

But the evar trick is clever, I could use that. Can the safechecker be generalized to emit a collection of constraints/equations that need to hold on the evars? (And then I'd need a lemma that says that this judgment is stable under evar instantiation ... does that exist?)

I guess I could even just abstract over the terms and safecheck the open term (using tRel or tVar instead of tEvar), and that would be even simpler? And then is there some lemma about parallel substitution into the empty context?

view this post on Zulip Théo Winterhalter (Apr 18 2023 at 09:27):

Ah indeed it could work, but if you abstract over subterms they might be in richer contexts, that's why I suggested evars.
But no, most of the evar stuff is not done. We might try to do it for rewrite rules though.

view this post on Zulip Jason Gross (Apr 18 2023 at 21:24):

What if I abstract into the context rather than with a lambda? Like, to check Sigma ;;; [] |- f a b c : T, can I safecheck Sigma ;;; [fT; aT; bT; cT] |- tApp (tVar 3) [tVar 2; tVar 1; tVar 0] : T or something, together with proving Sigma ;;; [] |- f : fT, Sigma ;;; [] |- a : aT, etc? (This is the parallel subst lemma I was asking about.)

view this post on Zulip Jason Gross (Apr 19 2023 at 05:55):

I guess the lemma is called substitution, and I can prove

Lemma closed_substitution {cf : config.checker_flags} {Σ}
  (s : list term)
  (Γ' : list term)
  (t T : term)
  (Hs : All2 (fun t T => Σ ;;; [] |- t : T) s Γ')
  (wfΣ : wf Σ)
  (Γ'' := List.map (fun ty => {| BasicAst.decl_name := {| binder_name := nAnon; binder_relevance := Relevant |} ; BasicAst.decl_body := None ; BasicAst.decl_type := ty |}) Γ')
  (Ht : Σ ;;; Γ'' |- t : T)
  : Σ ;;; [] |- subst0 s t : subst0 s T.
Proof.
  apply (@substitution cf Σ wfΣ [] Γ'' s [] t T);
    try (cbn; rewrite app_context_nil_l; assumption).
  clear Ht t T.
  subst Γ''; induction Hs; cbn [List.map]; constructor; trivial.
  { rewrite subst_closedn; [ assumption | ].
    change 0 with #|[]:context|.
    eapply @type_closed; eassumption. }
Qed.

and now I just need to make a tweak to subst0 so that there's no lift0 on the substitution. Then I can write a template monad program to generate all the arguments to this lemma from a goal, and the only thing that will remain is using the safechecker to derive Σ ;;; Γ'' |- t : T for the constructed arguments.

view this post on Zulip Théo Winterhalter (Apr 19 2023 at 06:37):

But what if the subterm is inside a λ\lambda?

view this post on Zulip Jason Gross (Apr 19 2023 at 08:58):

Why does it matter if the subterm is under a lambda? The subterms that I'm abstracting over will all be closed / well-typed in the empty context. Closed terms don't need to be lifted in de Bruijn, right?

view this post on Zulip Matthieu Sozeau (Apr 19 2023 at 09:13):

Right

view this post on Zulip Théo Winterhalter (Apr 19 2023 at 09:28):

Yes, I was asking whether you would have open terms basically, as the thread suggests. :smile:

view this post on Zulip Jason Gross (Apr 19 2023 at 19:22):

Ah, sorry, the thread topic was about x : Ast.termbeing open (having evars, context variables, axioms, etc) in Gallina / the metalanguage, not about x : Ast.term having tEvar or w/e as a subterm

view this post on Zulip Théo Winterhalter (Apr 19 2023 at 20:36):

Indeed, my bad.


Last updated: Jul 23 2024 at 20:01 UTC