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 `match`

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

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

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

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

(Does this proposal make sense?)

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?

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?

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.

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

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.

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

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?

Right

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

Ah, sorry, the thread topic was about `x : Ast.term`

being open (having evars, context variables, axioms, etc) in Gallina / the metalanguage, not about `x : Ast.term`

having `tEvar`

or w/e as a subterm

Indeed, my bad.

Last updated: Jul 23 2024 at 20:01 UTC