1
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ You can't expect (loc_stmt stmt) = l to 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$
    – Trebor
    Jan 7 at 19:01
  • $\begingroup$ Alternatively, you can define a boolean equality instead. $\endgroup$
    – Trebor
    Jan 7 at 19:01

2 Answers 2

2
$\begingroup$

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.
$\endgroup$
0
$\begingroup$

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.
$\endgroup$
6
  • $\begingroup$ I want to give operational semantics via a step transition relation, then define a symbolic operational semantics, and prove the latter to be equivalent to the former. The actual language is an OO language with multiple classes and methods, so there are many more structural invariants than just having distinct locations for distinct statements. That's why I do not specify programs as maps from locations to statements - every method would have its map and I would still have to specify all these maps do not overlap. So I express all the invariants via a predicate. $\endgroup$ Jan 8 at 17:03
  • $\begingroup$ It's usually better not to provide "fake motivation". If you stated from the beginning that you were doing semantics of an object-oriented language, you could have gotten a much more useful answer. A simple programming language (of whatever kind) can be dealt with quite easily in Coq. $\endgroup$ Jan 8 at 17:30
  • 1
    $\begingroup$ Are you familiar with Software foundations? It might be a useful source of knowledge for your purposes. $\endgroup$ Jan 8 at 17:32
  • $\begingroup$ Not really familar, but I am perusing Software Foundations as reference, it helps me a lot, and I shall read it more systematically in the future. To explain better whst I am doing, I am modeling a trimmed down version of the JVM specification, so the Coq model must be not too abstract to stay faithful to the original document. Explaining the motivation is always a tradeoff game between giving a meaningful context and not burdening the explanation or asking other people to do your work, sorry if I was not effective in that regard. $\endgroup$ Jan 9 at 10:47
  • 1
    $\begingroup$ Related work in this case should not be ignored. A shallow search reveals CoqJVM: An Executable Specification of the Java Virtual Machine using Dependent Types and A Formal Executable Semantics of the JavaCard Platform, at least. $\endgroup$ Jan 9 at 18:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.