Coq - Rewriting a FMap Within a Relation

Link:: https://stackoverflow.com/q/70998788

Display all goals and responses

Question

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'.forall S1 S2 : NatMap.t Z,
NatMap.Equal (elt:=Z) S1 S2 ->
forall (E G : environment) (F : function_table)
  (M : macro_table) (e : expr) (v : Z) (S' : store),
EvalExpr S1 E G F M e v S' <->
EvalExpr S2 E G F M e v S'
Proof.forall S1 S2 : NatMap.t Z,
NatMap.Equal (elt:=Z) S1 S2 ->
forall (E G : environment) (F : function_table)
  (M : macro_table) (e : expr) (v : Z) (S' : store),
EvalExpr S1 E G F M e v S' <->
EvalExpr S2 E G F M e v S'
  intros.S1, S2: NatMap.t Z
H: NatMap.Equal (elt:=Z) S1 S2
E, G: environment
F: function_table
M: macro_table
e: expr
v: Z
S': store
EvalExpr S1 E G F M e v S' <->
EvalExpr S2 E G F M e v S' split.S1, S2: NatMap.t Z
H: NatMap.Equal (elt:=Z) S1 S2
E, G: environment
F: function_table
M: macro_table
e: expr
v: Z
S': store
EvalExpr S1 E G F M e v S' ->
EvalExpr S2 E G F M e v S'
S1, S2: NatMap.t Z
H: NatMap.Equal (elt:=Z) S1 S2
E, G: environment
F: function_table
M: macro_table
e: expr
v: Z
S': store
EvalExpr S2 E G F M e v S' ->
EvalExpr S1 E G F M e v S'
  (* -> *)
  -S1, S2: NatMap.t Z
H: NatMap.Equal (elt:=Z) S1 S2
E, G: environment
F: function_table
M: macro_table
e: expr
v: Z
S': store
EvalExpr S1 E G F M e v S' ->
EvalExpr S2 E G F M e v S' intros.S1, S2: NatMap.t Z
H: NatMap.Equal (elt:=Z) S1 S2
E, G: environment
F: function_table
M: macro_table
e: expr
v: Z
S': store
H0: EvalExpr S1 E G F M e v S'
EvalExpr S2 E G F M e v S' induction H0.S2: NatMap.t Z
S: store
H: NatMap.Equal (elt:=Z) S S2
E, G: environment
F: function_table
M: macro_table
z: Z
EvalExpr S2 E G F M (Num z) z S
    + (* Num *)S2: NatMap.t Z
S: store
H: NatMap.Equal (elt:=Z) S S2
E, G: environment
F: function_table
M: macro_table
z: Z
EvalExpr S2 E G F M (Num z) z S
      Fail constructor.The command has indeed failed with message:
In environment
S2 : NatMap.t Z
S : store
H : NatMap.Equal (elt:=Z) S S2
E, G : environment
F : function_table
M : macro_table
z : Z
Unable to unify "S" with "S2".
S2: NatMap.t Z
S: store
H: NatMap.Equal (elt:=Z) S S2
E, G: environment
F: function_table
M: macro_table
z: Z
EvalExpr S2 E G F M (Num z) z S

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:

1 subgoal

  S2 : NatMap.t Z
  S : store
  H : NatMap.Equal (elt:=Z) S S2
  E, G : environment
  F : function_table
  M : macro_table
  z : Z
  ============================
  EvalExpr S2 E G F M (Num z) z S      Fail rewrite <- H.The command has indeed failed with message:
Found no subterm matching "NatMap.find (elt:=Z) ?M2110
                             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.

Answer (Arthur Azevedo De Amorim)

The issue here is that the relation NatMap.Equal, which says that two maps have the same bindings, is not the same as the notion of equality in Coq's logic, =. While it is always possible to rewrite with =, rewriting with some other relation R is only possible if you can prove that the property you are trying to show is compatible with it. This is already done for the relations in FMap, which is why rewriting there works.

You have two options:

Replace FMap with an implementation for which the intended map equality coincides with =, a property usually known as extensionality. There are many libraries that provide such data structures, including my own extructures, but also finmap and std++. Then, you never need to worry about a custom equality relation; all the important properties of maps work with =.
Keep FMap, but use the generalized rewriting mechanism to allow rewriting with FMap.Equal. To do this, you probably need to modify the definition of your execution relation so that it is compatible with FMap.Equal. Unfortunately, I believe the only way to do this is by explicitly adding equality hypotheses everywhere, e.g.
```
Definition EvalExpr' S E G F M e v S' :=
  exists S0 S0', NatMap.Equal S S0 /\
                   NatMap.Equal S' S0' /\
                   EvalExpr S0 E G F M e v S0'.
```
Since this will pollute your definitions, I would not recommend this approach.

Answer (larsr)

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