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 fseparately 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: Sep 25 2023 at 12:01 UTC