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...
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
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