I’m working on a lifter from a low-level imperative language to Coq and have been using anonymous fixpoints with loop limits to represent standard loops. The loops pass around a store to maintain state. This works out fairly well for computation, but it’s fairly difficult to deal with in a proof. Here’s an example, where the fixpoint code is significantly simpler than what I’m actually dealing with :
Inductive value : Type :=
| VNull
| VInteger (n : Z)
| VBool (b : bool).
Definition store : Type := id_type -> value.
Definition fresh_store : store := fun _ => VNull.
Definition get_int (s : store) (id : id_type) :=
match s id with
| VInteger n => n
| _ => 0
end.
Definition update (s : store) (id : id_type) (v : value) : store :=
fun x => if String.eqb x id then v else s x.
Theorem mwe :
forall loop_limit max_i,
0 < max_i ->
max_i < (Z.of_nat loop_limit) ->
(fix loop loop_limit store :=
match loop_limit with
| O => None
| S n' => (
(* Loop condition *)
if (get_int store "I" >=? max_i) then
(* Loop terminates *)
Some store
else (
(* Loop body *)
let store' :=
update store "I" (VInteger (get_int store "I" + 1))
in loop n' store'
)
)
end
) loop_limit (update fresh_store "I" (VInteger 0)) <> None.
The issue I’m having is that most of the terms inside of the fixpoint loop seem to be untouchable in the proof context due to their inclusion of loop variables (here, loop_limit and store). I’d like to rewrite and simplify terms inside of the loop because it doesn’t seem like destructing the variables passed into the loop will be sufficient to resolve the expression enough to prove basic properties.
To my knowledge, I can’t extract the loop body with remember (loop body expression) as body because input variables won’t be caught and extracted (and even if they were, body would just become another function).
Is there a way that I can access, manipulate, and/or simplify the contents of an anonymous fixpoint that rely on the fixpoint arguments, within a proof environment, in a manner that is sufficiently robust to prove complex properties of lifted imperative code?