How do I define a function in Coq with if...then..else behavior?

Question

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.

where

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?

Answer 1

Thanks to Trebor's suggestion (define a boolean equality), I was able to find that it is possible to automatically generate a boolean equality definition as follows:

Scheme Equality for syn_loc. (* defines syn_loc_beq *)

Fixpoint stmt_list_stmt (stmts : list syn_stmt) (l : syn_loc) : option syn_stmt :=
  match stmts with 
  | nil => None
  | cons stmt other_stmts => if (syn_loc_beq (loc_stmt stmt) l) then Some stmt else (stmt_list_stmt other_stmts l)
  end.

Answer 2

You are making your life difficult by programming as if Coq were a low-level language. Coq is a powerful language which supports abstraction, so:

• Do not use specific types for variable names and locations, use type parameters instead – you can always instantiate them later.
• Do not use lists of statements, just say that a program is a mapping from locations to statements. (The type of locations can be finite.)

Note that your suggeted implementation allows multiple statements to share the same location, and there is no relationship between the order of statements in the list and their locations. Presumably these are not desirable features.

I include below some sample code. If you'd like better advice, you should tell us what you intend to do: implement a simulator, a compiler, prove correctness of programs?

Require Import Coq.Strings.String.

Section MyLanguage.

  (* The type of variable names. *)
  Variable Var : Type.

  (* The type of locations. *)
  Variable Loc : Type.

  (* Statements. *)
  Inductive Stmt : Type :=
  | stmt_load : Var -> Stmt   (* load <variable name> on top of stack *)
  | stmt_store : Var -> Stmt (* store top of stack in <variable name> *)
  | stmt_return : Loc -> Stmt. (* return from method call *)

  (* A program is a mapping from locations to statements. *)
  Definition Program := Loc -> Stmt.

  (* The statement at a given location becomes a triviality. *)
  Definition stmt_at (p : Program) (l : Loc) := p l.

End MyLanguage.

(* We instantiate the above definitions so that variable names are strings,
   and a program is a finite sequence of statements. *)

Section Example.

  Definition ExampleLoc (k : nat) := { n : nat | n < k }.

  (* Statements with strings for variable names and locations natural numbers up to k. *)
  Definition ExampleStmt (k : nat) := Stmt string (ExampleLoc k).

  (* A program of size k is a map {0, 1, ..., k - 1} to statements. *)
  Definition ExampleProgram (k : nat) := Program string (ExampleLoc k).

End Example.