Hi there,

I'm playing around with the really great Equations approach and got stuck.

I derive `Subterm`

but then I received a proof obligation that I do not know how to solve.

Here is my toy language with conditionals:

```
Inductive Term : Type :=
| boolT (b: bool)
| natT (n: nat)
| iteT (i t e: Term).
```

To derive a termination measure, I use `Subterm`

:

```
Derive NoConfusion NoConfusionHom for Term.
Derive Subterm for Term.
```

Then I define the Small-Step operational semantics (on purpose as a function) like so:

```
Equations eval1 (term : Term) : option Term by wf term Term_subterm :=
eval1 (iteT (boolT true) t2 _ ) := Some t2;
eval1 (iteT (boolT false) _ t3) := Some t3;
eval1 (iteT (iteT t11 t12 t13) t2 t3) with eval1 (iteT t11 t12 t13) => {
eval1 (iteT (iteT t11 t12 t13) t2 t3) (Some t1') := Some (iteT t1' t2 t3);
eval1 (iteT (iteT t11 t12 t13) t2 t3) None := None
};
eval1 _ := None.
```

Now I use `eval1`

to define the multi-step relation `eval__n`

:

```
Equations eval1' (term : Term) : option Term :=
eval1' (iteT t1 t2 t3) := eval1 (iteT t1 t2 t3);
eval1' term := Some term.
Equations eval__n (term : Term) : (option Term) by wf term Term_subterm :=
eval__n' (iteT t1 t2 t3) with eval1' (iteT t1 t2 t3) => {
eval__n' (iteT t1 t2 t3) (Some term') := eval__n' term';
eval__n' (iteT t1 t2 t3) None := None
};
eval__n' term := Some term.
Next Obligation.
```

Now the goal is:

```
t1, t2, t3, term' : Term
eval__n : forall x : Term, Term_subterm x (iteT t1 t2 t3) -> option Term
============================
Term_subterm term' (iteT t1 t2 t3)
```

How do I solve such a goal?

Also, the `by rec`

as explained in this stackoverflow post does not seem to work anymore.

What would be the proper way to establish a measure without `Derive`

?

Is it always via the `wellfounded`

relation now?

This seems provable for your toy language — not sure how, and counterexamples wouldn't surprise me — but would fail, for instance, if you add lambdas or loops.

It seems that Coq's looking at `eval__n' (iteT t1 t2 t3) (Some term') := eval__n' term';`

and asking "why do you think `term'`

is smaller than `iteT t1 t2 t3`

" — I think that's true for your current toy language (and I don't know a proof), but it wouldn't be for most interesting extension.

That's for good reason: this property implies the language is normalizing. What's worse, this property is false even for strongly normalizing languages: normalization can cause size blowup; even a single beta-reduction `(\x. t) u`

can produce output of quadratic size `|t| * |u|`

, since it will replicate `u`

once for each occurrence of `x`

in `t`

.

Is it always via the wellfounded relation now?

Indeed, one always uses relations `R`

that are well-founded (such that `WellFounded R`

is a typeclass instance). (But `wellfounded`

itself isn't a relation); `Subterm`

is one such relation.

oh sorry — while the above is mostly true, your goal isn't provable — you need to "remember" that `term'`

comes from `eval1' (iteT t1 t2 t3)`

. That requires using the "inspect pattern"

That's basically Equations' version of using `destruct e eqn:?`

instead of `destruct e`

: here it'd records in context the propositional equality `eval1' (iteT t1 t2 t3) = Some term'`

. See https://github.com/mattam82/Coq-Equations/blob/3c2342f9b15e20c91d36293126123ea617c7a532/examples/Basics.v#L506-L538 for more info.

I was too quick.

Following the above advice

```
Equations eval__n' (term : FCPterm) : (option FCPterm) by wf term FCPterm_subterm :=
eval__n' (iteT t1 t2 t3) with inspect (eval1' (iteT t1 t2 t3)) => {
eval__n' (iteT t1 t2 t3) (Some term' eqn: eq1) := eval__n' term';
eval__n' (iteT t1 t2 t3) (None eqn: eq2) := None
};
eval__n' term := Some term.
Next Obligation.
```

I get one proof obligation:

```
t1, t2, t3, term' : FCPterm
eq1 : eval1' (iteT t1 t2 t3) = Some term'
eval__n' : forall x : FCPterm, FCPterm_subterm x (iteT t1 t2 t3) -> option FCPterm
============================
FCPterm_subterm term' (iteT t1 t2 t3)
```

Here is how far I got:

```
clear eval__n'.
move: eq1.
funelim (eval1' (iteT t1 t2 t3)).
funelim (eval1 (iteT t1 t2 t3)) => //=;
move => eq_some; injection eq_some => eq_term; rewrite -eq_term.
- exact: (Relation_Operators.t_step _ _ _ _ (FCPterm_direct_subterm_2_2 _ _ _)).
- exact: (Relation_Operators.t_step _ _ _ _ (FCPterm_direct_subterm_2_1 _ _ _)).
- apply Hind in Heq.
by [apply cond_subterm].
Defined.
```

I'm not sure whether this is the proper way of writing such a proof. Is it?

In the last line of the proof, I use lemma `cond_subterm`

which I do not know how to prove:

```
Lemma cond_subterm: forall t1 t1' t2 t3,
FCPterm_subterm t1 t1' -> FCPterm_subterm (iteT t1 t2 t3) (iteT t1' t2 t3).
```

After all, `FCPterm_subterm`

is just a transitive closure `clos_trans`

with `step`

and `trans`

but the hypothesis `FCPterm_subterm t1 t1'`

hints more towards some form of induction. I found the induction principle `clos_trans_ind`

but when I try to use it, I get an error:

```
Error: Anomaly "File "plugins/ssr/ssrcommon.ml", line 792, characters 18-24: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
```

What is the proper way to write this proof?

Sebastian Ertel has marked this topic as unresolved.

I managed to write the function with my own metric `subTermCount`

like this:

```
Equations eval__n (term : FCPterm) : (option FCPterm) by wf (subTermCount term) lt :=
eval__n (iteT t1 t2 t3) with inspect (SmallStep.eval1' (iteT t1 t2 t3)) => {
eval__n (iteT t1 t2 t3) (Some term' eqn: eq1) := eval__n term';
eval__n (iteT t1 t2 t3) (None eqn: eq2) := None
};
eval__n term := Some term.
```

Proving the remaining obligation was now trivial.

Nevertheless, I would still like to understand whether there exists a solution to the `cond_subterm`

lemma above.

Does it have to do with the fact that the `Derive Subterm`

command does not handle nested recursive occurences like is hinted at in this paper?

Your Term datatype doesn't have nested recursive occurrences; I think your proof strategy was correct.

all anomalies are valid bug reports, so you should probably file a bug with some reproduction code

Since your anomaly seems to be in ssreflect code, I guess it's in elim, so I wonder what induction or apply do with that induction principle

Last updated: Oct 13 2024 at 01:02 UTC