The evaluation relation used in erasure is nondeterministic because `eval_fix`

uses `is_constructor_or_box`

while `eval_fix_value`

uses just `~is_constructor`

:

```
Definition f := tFix [{| dname := nAnon; dbody := tLambda nAnon (tRel 0); rarg := 0 |}] 0.
Lemma eval1 Σ :
Σ ⊢ tApp f tBox ▷ tApp f tBox.
Proof. change (tApp f tBox) with (mkApps f [tBox]). repeat constructor. Qed.
Lemma eval2 Σ :
Σ ⊢ tApp f tBox ▷ tBox.
Proof.
change (tApp f tBox) with (mkApps f [tBox]).
eapply eval_fix; repeat constructor; try easy.
eapply eval_beta; repeat constructor.
Qed.
```

I suppose `eval_fix_value`

case should be using `is_constructor_or_box`

like `eval_fix`

, right?

Hmm, I think you're right, can you please report an issue about this?

We certainly should also uncomment the proof below that eval is deterministic :)

Sure. I can also see if I can fix it and submit a PR.

I don't think that proof is finished (PCUIC does not seem to have a proof of it either). I have a proof of it, but first using a slightly restated intermediate evaluation relation that I then show is equivalent (except for this particular part I was asking about), so it is a bit of code.

It used to be proven until we changed something in fixpoint unfolding , maybe we were precisely hitting this problem (we would have anyway)

I changed the constructor of `eval`

, but now the correctness proof of erasure broke because, in the case where a PCUIC fix is stuck with enough arguments, we only know that the structural argument is not a constructor, and we need to show that its erasure is not a constructor and not a box.

Ideally I guess we should show the case is impossible because the environment is axiom free, so the structural argument has to be a constructor (by canonicity). Is this true?

If the PCUIC fix is stuck indeed we would have a closed value in an inductive type that is not a constructor and that is impossible.

Your reasoning is correct

Are there existing results about this in MetaCoq?

There does not seem to be anything yet. It might be in one of Yannick Forster's branches. In principle it follows from SN, SR etc...

@Yannick Forster (Gitter import) ?

Matthieu Sozeau said:

Yannick Forster (Gitter import) ?

This account has not been claimed and was therefore archived.

Cyril Cohen said:

Matthieu Sozeau said:

Yannick Forster (Gitter import) ?

This account has not been claimed and was therefore archived.

Ok, thanks!

I have another related issue which I think is also an issue in PCUIC big-step evaluation. As far as I can tell, there is no possible derivation for the execution of the following program:

```
Fixpoint f (a b : nat) {struct b} := b.
Definition prog := (fun x => f x) 0 0.
```

The problem is that the evaluation relations do not allow adding arguments to things that evaluate to stuck fixpoint, they only allow saying that the fully applied syntactic fixpoint will evaluate to something.

Hmm, this looks like a completely legitimate program to me, you mean that the eval_fix rule is wrong then?

Indeed, it does not allow this program to compute to anything.

I think it would make sense to replace `eval_fix`

and `eval_fix_value`

by

```
| eval_fix_value f mfix idx args narg fn a av :
Σ ⊢ f ▷ mkApps (tFix mfix idx) args ->
Σ ⊢ a ▷ av ->
cunfold_fix mfix idx = Some (narg, fn) ->
(#|args| <> narg \/
(#|args| = narg /\ ~is_ctor_or_box av)) ->
Σ ⊢ tApp f a ▷ mkApps (tFix mfix idx) (args ++ [av])
| eval_fix f mfix idx args narg fn a av v :
Σ ⊢ f ▷ mkApps (tFix mfix idx) args ->
Σ ⊢ a ▷ av ->
cunfold_fix mfix idx = Some (narg, fn) ->
#|args| = narg ->
is_ctor_or_box av ->
Σ ⊢ mkApps fn (args ++ [av]) ▷ v ->
Σ ⊢ tApp f a ▷ v
```

(And potentially make it `#|args| < narg`

in `eval_fix`

). As an added bonus, with this replacement it is _way_ easier to invert and proving it deterministic is easy.

Actually, scratch that part about `#|args| < narg`

, I can see now that more arguments might be needed

That looks right. I'm surprised we didn't see the problem before, but that might be explained because we only exercise the evaluation relations after erasure in CertiCoq, where we additionally assume there are no longer stuck fixpoints.

I'm working on doing this as we need it as well. I'm curious, is there a reason `unfold_fix`

is used in some places in the evaluation relation? So far I have replaced all of them with `cunfold_fix`

which seems more in line with how the other rules work (with `csubst`

)

Ok, cool. [unfold_fix] and [cunfold_fix] are interchangeable on closed terms, so yes that's more uniform this way.

Ok, thanks!

I'll look into the lemma we need for erasure correctness.

Awesome!

I'm not totally sure what the new rules should look like for template Coq's relation due to the n-ary applications there. I guess it still needs to have `mkApps`

at the conclusion there

It seems like WcbvEval for template-coq (kernel) terms is gone now.

There is still this one: https://github.com/MetaCoq/metacoq/blob/coq-8.11/checker/theories/WcbvEval.v

Yes, true. I've seen that one but wasn't sure if it uses the kernel AST, but it seems it does. BTW, `mkApps`

there is a bit different, it flattens the application instead of building the nested applications: https://github.com/MetaCoq/metacoq/blob/6d1ab4c5ab77bed63259133e747be83a7e643d87/template-coq/theories/Ast.v#L57

Yeah, because of this I'm not totally sure what the rule needs to look like. Also I'm not sure if there should be a rule that allows non-canonical terms to compute to the same thing as their canonical counterparts

Everything is proven assuming well-formed terms in checker/template-coq, so you can assume every `tApp t u`

is well-formed (`t`

cannot be an application)

Ok, that helps. Then it should have `mkApps`

at the conclusion as well, I think.

I guess it should ressemble the new relation, where you have `eval_fix ... : eval f (mkApps (mkFix mfix idx) args') -> ... eval (mkApps f args) res`

.

Yes, you're kind of forced to see the whole spine of arguments in this representation.

Hmm right, but the rules have to be generalized to n-ary args instead of just adding a single argument to the stuck fixpoint, right?

```
| eval_fix f mfix idx fixargsv args argsv narg fn res :
eval f (mkApps (tFix mfix idx) fixargsv) ->
All2 eval args argsv ->
unfold_fix mfix idx = Some (narg, fn) ->
is_constructor narg (fixargsv ++ argsv) ->
eval (mkApps fn (fixargsv ++ argsv)) res ->
eval (mkApps f args) res
| eval_fix_value f mfix idx fixargsv args argsv narg fn :
eval f (mkApps (tFix mfix idx) fixargsv) ->
All2 eval args argsv ->
unfold_fix mfix idx = Some (narg, fn) ->
~~is_constructor narg (fixargsv ++ argsv) ->
eval (mkApps f args) (mkApps (tFix mfix idx) (fixargsv ++ argsv))
```

Like this, I suppose. I think I will give up on proving this one deterministic :)

I understand, dealing with mkApps is no fun ;) But yes this looks right.

I updated it and proved the old results about it in the PR. The only thing missing is the fix/fix_value cases for `erases_correct`

. I looked at it for a bit but it didn't seem totally straightforward to adapt the old proof.

Ok, I will look at those with Yannick Forster. It was on our agenda already to show that we can even weaken the requirement a bit more: no need to test if the recursive argument is a constructor or a box in erasure, as it should be statically known to be.

I'll be on vacation next week though. Do you want this merged while incomplete or can it wait?

It can wait, we can use a fork, no problem.

I took another look and managed to prove the new cases, except for the impossible case where a fixpoint is stuck on a non-constructor.

@Matthieu Sozeau should I leave it as a draft until we have the remaining case?

I think we can merge it with this left as a todo, so you can turn it into a PR. I’ll be doing POPL PC work for the coming weeks so I don’t know if I’ll get around to it soon, but Yannick might.

Last updated: Jun 18 2024 at 23:01 UTC