PCUIC vs Ast.term

[gmalecha]

I just recently started looking into PCUIC and it looks really great. Would it be possible to replace the Template.Ast.term definition with this one? Are there features that exist in one but not in the other?

[TheoWinterhalter]

PCUIC is an alternative syntax to the TemplateCoq one, replacing one by the other would rather mean only keeping one I think. If I'm correct, the point is that TemplateCoq follows rather closely the Coq implementation while PCUIC is supposed to be easier to reason on. Ultimately it should have utilities to easily go from one to the other.

[gmalecha]

Yes. The original motivation was exactly that, I was thinking that you could play tricks with partially applied functions, but that breaks Coq's internal invariants.

It isn't important to do now, but personally I would be in favor of moving to a single, cleaner representation.

[annenkov]

Hi guys, I think, n-ary application makes a big difference in convenience for reasoning. I believe that the mkApps smart constructor is used in various relations (and, IIRC, in substitution) to "normalize" various ways of nesting tApp with a list of arguments. I am currently working with the WcbvEval.eval relation and run into the mkApps issue.

I was hoping that something like this should hold:

l <> [ ] ->
WcbvEval.eval Σ Γ (mkApps t l) t ->
WcbvEval.eval Σ Γ (tApp t l) t

and I can replace derivations of mkApps with just tApp, but apparently this is not true (at least without imposing restrictions on what is t)

[gmalecha]

You probably want to phrase a viewApp : term -> term * list term that would guarantee that the resulting term does not have a head tApp constructor.

[annenkov]

Yes, good point. Actually, since I am translating to term from another type of expressions (with only binary applications), my translation guarantees that there are no empty or nested applications, I might be able to use that. Thanks!

[annenkov]

I still struggle with my proof involving mkApps. I think, if I targeted PCUIC instead, my development would be much easier. So, the question is which Ast makes more sense to target in a long run? Also, if we keep both, would it be reasonable to translate PCUIC to TemplateCoq and prove correctness? For me this direction makes a lot of sense, since I am developing an embedding of functional languages in Coq, so making a certified chain of translations MyAst -> PCUIC -> TemplateCoq is probably better (or at least, simpler, because PCUIC looks better as a target). What do you think @gmalecha @TheoWinterhalter @mattam82 ?

[mattam82]

It should be trivial to do the PCUIC -> Template translation, good to know we have a practical application for it too!

[gmalecha]

Personally, I think targeting PCUIC is the righy way to go, at least at the level that I understand things.

[TheoWinterhalter]

I think that is part of the goal of PCUIC, having something nicer to reason about.

[yforster]

I agree with Gregory and Théo.

Matthieu, would the translation require that stacked (binary) tApp in PCUIC get translated to one big Template Coq tApp (taking a term and a list)? That's not completely trivial anymore I think, but if you want going from TemplateCoq to PCUIC and back to be the identity on many terms it's necessary, no?

[annenkov]

would the translation require that stacked (binary) tApp in PCUIC get translated to one big Template Coq tApp (taking a term and a list)?

This is exactly the part which I am struggling with :) At least in the proof involving WcbvEval.eval relation and evaluation in my language a "stacked" (or nested) application is evaluated in different "direction" than the application to a list of terms.

[TheoWinterhalter]

All the more reason to do this once and for all then. :)

[annenkov]

Another thing that looks a bit strange to me: mkApps is also used in substitution (although, there might be a good reason for that). Because of this I didn't have much of a choice when I defined the translation from my language to TemplateCoq Ast. If I didn't collapse stacked applications, my substitution would not be compatible with the TemplateCoq substitution.

[mattam82]

Yep, that's the root of the issue, you need to preserve the mkApps invariant everywhere and this gets pretty messy (and ultimately, boring). Let's give it a try. @yforster I think the translation will be structurally recursive, if defined as follows:

Fix trans (t : PCUIC.term) {struct t} : Ast.term :=
  match t' with 
  | ... => trans u' 
  | tApp f u => mkApps (trans f) [trans u]

It shouldn't be too hard to prove pcuic_to_coq (coq_to_pcuic t) ~= t (where ~= is equality plus (c : t) ~= (fun x : t => x) c for the cast translation). Or do you see a problem with this?

[yforster]

I think there's a problem, yes.

If you start at Ast.tApp u [v1, v2] and you go to PCUIC you are PCUIC.tApp (PCUIC.tApp u' v1') v2' If you go back like this you are Ast.tApp (Ast.tApp u'' [v1'']) [v2'']. And I think in some cases, this is an issue. For instance the tCase rule in Ast.red1 expects a tConstruct b (mkApps ...), but that's not going to be true anymore.

So I guess you need something like

Fix trans (t : PCUIC.term) {struct t} : Ast.term :=
  match t' with 
  | ... => trans u' 
  | tApp f u => transApps f [trans u]
... end
with
transApp (t : PCUIC.term) (L : list Ast.term) : Ast.term :=
  match t with
  | tApp l r => transApp l (trans r :: L) 
  | t => mkApps (trans t) L

I.e. you have to make sure that when converting stacked PCUIC.tApp you put all of the right hand sides in the list, instead of producing stacked Ast.tApp with singleton lists.

Otherwise reducible terms might not be reducible anymore after the roundtrip, and I would guess there are problems with typing as well.

Edit: More severely, there might be problems unquoting stacked Ast.tApps, but that's just a guess.

[mattam82]

Hmm, but my mkApps (trans f) [trans u] will "unstack" the applications in f if there are any. You're right that we should be careful in the ML to ensure that we don't build ill-formed terms made of Ast.tApp though.

[yforster]

Oops, you're right. I had a wrong definition of mkApps in mind, this is indeed doing the unstacking properly, so everything is fine on this front.

[mattam82]

Out of curiosity, what kind of language are you translating @aa755 ? Clearly mkApps is giving trouble to everyone :) I believe we should however keep both representations for the time being. It seems I need a change of interpretation of fixpoints blocks also to ease reasoning in PCUIC, and it’ll be nice to mechanically check I’m proving things about an equivalent theory.

[annenkov]

@mattam82 were you asking me about the language I am translating? (I mean, Abhishek didn't comment on this issue). I am working of embedding of mini-ml style (plus inductives and pattern-matching) language in Coq. The idea is to use it as a source for lifting functional programs to Coq in a controlled way (as opposed to hs-to-coq source-to-source approach). I work with Bas Spitters on verifying smart contract languages and many of this languages have functional "core".

I agree, keeping both makes sense, since TemplateCoq syntax should follow the OCaml implementation closely. So having translation PCUIC <-> TemplateCoq would be nice to have (along with proofs of correctness).

[annenkov]

I've ported parts of my development to target PCUIC, but it turns out I just pushed the issue with mkApps to another corner. Now inverting anything involving PCUICWcbvEval.eval relation is painful because of the cases with mkApps in conclusion (e.g. cases like tConstruct). Specifically, when proving a case for application, I invert the hypothesis with eval, and one of the cases I have the following in my context: mkApps f agrs = tApp (T⟦ e1⟧) (T⟦ e2⟧), where T⟦ - ⟧ is a translation function. I want to learn something about f from that, but don't see any way of doing this.

I am thinking about defining a relation almost as PCUICWcbvEval.eval, but with values in a separate syntactic category. These values will include vConstr i c args, where args is a list of values. This is how I did it in the semantics to my language. But if I do this, I'll have to show that my relation is also a sub-relation of a small step relation of PCUIC (up to converting values to terms).

[TheoWinterhalter]

I had similar issues, so I added a function to count applications in order to deduce injectivity properties on mkApps, see here and the few lemmata that follow. I don't know if it can help you.

[annenkov]

Thanks @TheoWinterhalter, I'll look if I can use these.

[annenkov]

I decided to go back to my translation directly to TemplateCoq AST, since inversion of PCUICWcbvEval seems too problematic. Also, I think, way of evaluating applied constructors does not match with my evaluation of constructors.

With TemplateCoq WcbvEval I see two main issues:

• eval_beta evaluates nary application from left to right. This doesn't match the way I do it in my interpreter. Since I have binary application, I do recursion "on the left" traversing nested applications. I fixed this by "emulating" the nary application evaluation in the interpreter.

• usage of mkApps in eval_beta (and, I beleive, in eval_fix). This stuff I don't know how to fix really. I see that mkApps is used in subst as well, so, it looks like if I use the following function instead of mkApps:

Definition mkApps1 (t : term) (ts : list term):=
  match ts with
  | [] => t
  | _ => tApp t ts
  end.

If any nested application should be flattened by subst. Also, terms produces by my translation are guaranteed to have all the application flattened and have no empty applications. I played a bit with the WcbvEval relation with mkApps replaced with mkApps1; it seems to work for some cases of applications. And with this modified relation I can prove the lambda application case.

How wrong this modification can be, what do you think? Maybe it is possible to prove that this modified relation and the original one give the same results on terms with "well-formed" application.

[annenkov]

Ok, I think I understand that I still get nested tApps even though the substitution flattens nested applications. But why it's bad to have nested tApps? I understand that different ways of nesting will correspond to different derivations of WcbvEval.eval relation. But why this is important?

[annenkov]

I've modified the WcbvEval.eval relation to make the evaluation of applications more explicit. I've added a mutually defined eval_apps relation that takes care of evaluation of nary applications. Here is a gist link to an incomplete sketch of what I want: https://gist.github.com/annenkov/b89a075598ea84e0f3d3560004a12819

This relation follows the same way as the typing relation with typing_spine. However, I am not sure how to evaluate fixpoints (and also for tInd and tConstruct). I want all the applications to be evaluated in the same way as tLambda: one argument at a time. I would appreciate some feedback on this. @gmalecha @TheoWinterhalter @mattam82

[annenkov]

An alternative (an maybe a better one) would be to use the following cbv evaluation relation for PCUIC: https://gist.github.com/annenkov/5b2af547fb7ee018dc18161068071dc7

In this values are a separate type, distinct from term. The conversion function is used to convert values back to terms for substitution. I think, more controlled use of mkApps (only in the conversion function) makes this relation more well-behaved, and so, potentially easier to use. However, I the fixpoint case is indeed would be nice to simplify as @mattam82 mentioned. I my version, I assume that fixpoints are defined by recursion on the first arg.

[mattam82]

I'm not sure we can escape mkApps, even if the split of values and terms is somewhat nice in your latest WcbvEval. Can you show where the original problem is when you need to invert on PCUICWcbvEval, e.g. which lemma are you proving?

[annenkov]

Hi @mattam82 , sorry for the delay with my reply. The repo with my development is not (yet) public, but I gathered all relevant pieces here: https://gist.github.com/annenkov/10dedceffec2d02da9c094dd0dd62e2e.

Basically, I am proving that interpreter for our language gives the same result as PCUICWcbvEval.eval on the translated terms (with the translation given by expr_to_pcuic) for terminating programs. It seems that the case for the application of lambda works fine, but for the constructor application I have to invert hypothesis like mkApps f agrs = tApp (T⟦ e1⟧) (T⟦ e2⟧) hoping to say something about f. Basically all the rules with the conclusion of the form Σ;;; Γ |- mkApps f a ⇓mkApps something a' (⇓ is a notation for WcbvEval) are problematic. It seems, these rules "emulate" n-ary application by requiring a term being evaluated to be an iterated application and then evaluating all the terms in a list a in "one go". This is different from what's happening in my interpreter: there, the nested application would be evaluated recursively, essentially in the same way as I did in the alternative version of WcbvEval with separate type for values.