I am still a beginner in Coq, so perhaps my issue is trivial but I was unable to find a solution by searching the documentation available online. I am defining in Coq the syntax of a programming language, where each statement has a location, i.e., a label distinguishing all the statements of a same program. I would like to define a function
stmt_list_stmt that takes as input a list of statements and a location, and returns the statement in the list at that location, if any. The main types are as follows:
Inductive syn_loc : Type := | loc : nat -> syn_loc. Inductive syn_stmt : Type := | stmt_load : syn_loc -> string -> syn_stmt (* load <variable name> on top of stack *) | stmt_store : syn_loc -> string -> syn_stmt (* store top of stack in <variable name> *) ... | stmt_return : syn_loc -> syn_stmt. (* return from method call *)
My initial definition of the function is the following (wrong) one:
Fixpoint stmt_list_stmt (stmts : list syn_stmt) (l : syn_loc) : option syn_stmt := match stmts with | nil => None | cons stmt other_stmts => if (loc_stmt stmt) = l then Some stmt else (stmt_list_stmt other_stmts l) (* wrong! *) end.
Definition loc_stmt (stmt : syn_stmt) : syn_loc := match stmt with | stmt_load l _ => l | stmt_store l _ => l ... | stmt_return l => l end
This does not work because
(loc_stmt stmt) = l has type
Prop, and Coq expects an inductive type with two constructors. With my current knowledge I am stuck - I am unable to express the above conditional in a way that is palatable to Coq. What am I missing?
(loc_stmt stmt) = lto be either true or false, unless you proved that it is either true or false. Or you can add this as an axiom: Everything is either true or false. $\endgroup$