## Stream: Coq users

### Topic: Evaluate suitably a `fix` to explicit an internal fixpoint

#### Pierre Vial (Nov 06 2022 at 16:06):

Hi,
[EDIT:] I have to deal with a function `f` which has an internal fixpoint `g_int `
`f` is automatically generated and I'm not allowed to modify it's code.
The problem is: `g_int` is specified to perform an induction on a parameter `x`, whereas the induction is actually on another parameter `l2`, which is a list.

The thing is: it blocks the evaluation of `g_int` when it is fed with an empty list.
Is there a way to force `g_int` to evaluate with respect to `l2` even when the inductive argument is ill-specified?

[OLD POST]
I puzzled by the following problem:
I want to prove an equality.

The setting is the following:

``````Definition f
(x :  A1) (b1 : B1) (b2 : B2)  (l2 : list A2) :=
let fix g_int (x :  A1) (l3 : list A3) (l2 : list A2) {struct x} :=
match l2 with
| [] => (Cons1 x, rev l3)
|  (p2 :: l2) => (* some very complex expression involving `g_int`,
the parameters of `g_int` and also the "external" parameters `b1` and `b2`)
end
in g_int x [] l2
``````

Now:

• I want to define the internal function `g` of `f`separately in another file
(I can't change the definition of `f`).

• I want to prove the relation between `f` and `g`

So, first I do:

``````Fixpoint g  (x :  A1) (b1 : B1) (b2 : B2)  (l3 : list A3) (l2 : list A2) {struct x} :=
match l2 with
| [] => (Cons x, rev l2) (* `Cons` is the constructor of a certain type *)
|  (p2 :: l2) => (* the same expression, except now, `b1` and `b2` are not "external" parameters
end.
``````

Then I state, as expected:

``````Lemma foo x b1 b2  l2:  f x b1 b2 l2 = g x b1 b2 nil l2
Proof.
unfold f , g.
induction l2.
-  (* first case of the induction: both members have the form `(fix ... ) x [] []`and should evaluate to `(Cons1 x, [])`
Fail reflexivity.
Abort.
``````

Note that, in the first case, `reflexivity` fails. But `cbn` does nothing and `cbv` loops (well, does not output anything after more than 4 minutes).
My questions are:
1) a) why does `reflexivity` fail in the first case in the induction?
b) `cbn` does nothing, why? I should first evaluate the 3 outermost applications, right?

2) is there a way to do this without induction? Basically, I did only some cut-and-paste. That could even help me avoid defining explicitly `g` and having to prove the lemma...

#### Pierre Vial (Nov 06 2022 at 16:16):

Note that the internal fixpoint is specified as doing an induction on `x` (which is a record), but the inductve calls are clearly done on `l2` (guard checking has been deactivated).
When I modify the definition of `g` to specify that the induction of `g` is on `l2`, the evaluation of `g` works fine

#### Paolo Giarrusso (Nov 06 2022 at 23:27):

The thing is: it blocks the evaluation of g_int when it is fed with an empty list.
Is there a way to force g_int to evaluate with respect to l2 even when the inductive argument is ill-specified?

You _might_ be able to prove a _propositional_ equality giving the right equation, but since `g_int` is declared as recursive on `x`, you might need to pattern-match on `x` — to enable iota-reduction as specified in https://coq.inria.fr/refman/language/core/inductive.html#reduction-rule. (Other conversion rules are in https://coq.inria.fr/refman/language/core/conversion.html).

Last updated: Feb 04 2023 at 20:02 UTC