I am new to Coq, and was hoping that someone with more experience could help me with a problem I am facing.
I have defined a relation to represent the evaluation of a program in an imaginary programming language. The goal of the language is unify function calls and a constrained subset of macro invocations under a single semantics. Here is the definition of the relation, with its first constructor (I am omitting the rest to save space and avoid unnecessary details).
Inductive EvalExpr:
store -> (* Store, mapping L-values to R-values *)
environment -> (* Local environment, mapping function-local variables names to L-values *)
environment -> (* Global environment, mapping global variables names to L-values *)
function_table ->(* Mapping function names to function definitions *)
macro_table -> (* Mapping macro names to macro definitions *)
expr -> (* The expression to evaluate *)
Z -> (* The value the expression terminates to *)
store -> (* The final state of the program store after evaluation *)
Prop :=
(* Numerals evaluate to their integer representation and do not
change the store *)
| E_Num : forall S E G F M z,
EvalExpr S E G F M (Num z) z S
...
The mappings are defined as follows:
Module Import NatMap := FMapList.Make(OrderedTypeEx.Nat_as_OT).
Module Import StringMap := FMapList.Make(OrderedTypeEx.String_as_OT).
Definition store : Type := NatMap.t Z.
Definition environment : Type := StringMap.t nat.
Definition function_table : Type := StringMap.t function_definition.
Definition macro_table : Type := StringMap.t macro_definition.
I do not think the definitions of the other types are relevant to this question, but I can add them if needed.
Now when trying to prove the following lemma, which seems intuitively obvious, I get stuck:
Lemma S_Equal_EvalExpr_EvalExpr : forall S1 S2,
NatMap.Equal S1 S2 ->
forall E G F M e v S',
EvalExpr S1 E G F M e v S' <-> EvalExpr S2 E G F M e v S'.
Proof.
intros. split.
(* -> *)
- intros. induction H0.
+ (* Num *)
Fail constructor.
Abort.
If I were able to rewrite S2 for S1 in the goal, the proof would be trivial; however, if I try to do this, I get the following error:
H : NatMap.Equal S S2
(* Other premises *)
---------------------
EvalExpr S2 E G F M (Num z) z S
rewrite <- H.
Found no subterm matching "NatMap.find (elt:=Z) ?M2433 S2" in the current goal.
I think this has to do with finite mappings being abstract types, and thus not being rewritable like concrete types are. However, I noticed that I can rewrite mappings within other equations/relations found in Coq.FSets.FMapFacts. How would I tell Coq to let me rewrite mapping types inside my EvalExpr relation?
Update: Here is a gist containing a minimal working example of my problem. The definitions of some of the mapping types have been altered for brevity, but the problem is the same.
Arthur's answer explains the problem very well.
One other (?) way to do it could be to modify your Inductive definition of EvalExpr to explicitly use the equality that you care about (NatMap.Equal instead of Eq). You will have to say in each rule that it is enough for two maps to be Equal.
For example:
| E_Num : forall S E G F M z,
EvalExpr S E G F M (Num z) z S
becomes
| E_Num : forall S1 S2 E G F M z,
NatMap.Equal S1 S2 ->
EvalExpr S1 E G F M (Num z) z S2
Then when you want to prove your Lemma and apply the constructor, you will have to provide a proof that S1 and S2 are equal. (you'll have to reason a little using that NatMap.Equal is an equivalence relation).