![coq programming language coq programming language](https://miro.medium.com/max/1104/0*TXtUqak9j7f2om4C.png)
![coq programming language coq programming language](https://learnpracticeandshare.com/wp-content/uploads/2020/12/Awesome-Coq-Programming-Resources-List-780x470.jpg)
The definitions of some of the mapping types have been altered for brevity, but the problem is the same. Update: Here is a gist containing a minimal working example of my problem. How would I tell Coq to let me rewrite mapping types inside my EvalExpr relation? However, I noticed that I can rewrite mappings within other equations/relations found in. I think this has to do with finite mappings being abstract types, and thus not being rewritable like concrete types are. 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įound no subterm matching "NatMap.find (elt:=Z) ?M2433 S2" in the current goal. Now when trying to prove the following lemma, which seems intuitively obvious, I get stuck: Lemma S_Equal_EvalExpr_EvalExpr : forall S1 S2,ĮvalExpr S1 E G F M e v S' EvalExpr S2 E G F M e v S'. I do not think the definitions of the other types are relevant to this question, but I can add them if needed. Module Import StringMap := FMapList.Make(OrderedTypeEx.String_as_OT).ĭefinition environment : Type := StringMap.t nat.ĭefinition function_table : Type := StringMap.t function_definition.ĭefinition macro_table : Type := StringMap.t macro_definition. The mappings are defined as follows: Module Import NatMap := FMapList.Make(OrderedTypeEx.Nat_as_OT). (* Numerals evaluate to their integer representation and do not Store -> (* The final state of the program store after evaluation *) Z -> (* The value the expression terminates to *) Macro_table -> (* Mapping macro names to macro definitions *) Store -> (* Store, mapping L-values to R-values *)Įnvironment -> (* Local environment, mapping function-local variables names to L-values *)Įnvironment -> (* Global environment, mapping global variables names to L-values *)įunction_table ->(* Mapping function names to function definitions *) Here is the definition of the relation, with its first constructor (I am omitting the rest to save space and avoid unnecessary details). The goal of the language is unify function calls and a constrained subset of macro invocations under a single semantics. I have defined a relation to represent the evaluation of a program in an imaginary programming language. I am new to Coq, and was hoping that someone with more experience could help me with a problem I am facing.