This project contains a Coq proof of an equivalence relation on the Imp language that is not congruent. This answers a question from the Program Equivalence (Equiv) chapter of Programming Language Foundations, which is the second book of Software Foundations. This proof is suggested in this answer on the Computer Science StackExchange.
- Author(s):
- Dennis Gosnell (initial)
- License: BSD 3-Clause "New" or "Revised" License
- Compatible Coq versions: 8.12 or later
- Additional dependencies: none
- Related publication(s): none
The easiest way to install the latest released version of Equivalence Not Congruence for Imp is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-coq-equivalence-not-congruence
To instead build and install manually, do:
git clone https://github.com/cdepillabout/coq-equivalence-not-congruence.git
cd coq-equivalence-not-congruence
make # or make -j <number-of-cores-on-your-machine>
make install
If you're using Nix, you can get into a shell with Coq available by running
nix develop
:
$ nix develop
You can build all the Coq files in this repo with make
:
$ make
After building, you can open up any of the files in
theories/
in coqide
in order to work through the proofs.
You can regenerate the files in this repo (like README.md
) from the
meta.yml
file by cloning
coq-community/templates
and
running generate.sh
:
$ /some/path/to/coq-community/templates/generate.sh
You can also generate HTML documentation with coqdoc
:
$ make html
The Program Equivalence (Equiv) chapter of Programming Language Foundations has a question like the following:
We've shown that the
cequiv
relation is both an equivalence and a congruence on commands. Can you think of a relation on commands that is an equivalence but not a congruence?
There is an answer to this question on the Computer Science StackExchange:
Let
x
,y
be two fixed distinct variable names.Call
P
andQ
equivalent iffQ
is obtained fromP
by optionally swapping the variable namesx
andy
. That is, eitherQ = P
orQ = P{x/y,y/x}
where the latter uses simultaneous substitution.It is an equivalence. Reflexivity follows by construction. For symmetry,
P == Q
swaps ifQ == P
swaps (where==
is the equivalence relation). For transitivity, we consider the four cases: in the swap-swap case we get the same program back.It is not a congruence since
(x := x + 1) == (y := y + 1)
and(x := 0) == (x := 0)
, but(x := 0; x := x + 1) =/= (x := 0; y := y + 1)
The theories/RenameVars.v
file has a
formalization of this equivalence relation on the Imp language, as well as a
proof that there is no congruence in this case.
This repo contains other examples of equivalence relations that are not congruences:
-
This file contains an example of an equivalence relation where two Imp programs are considered equivalent if they have the same number of unique assignments for a set of variables. For instance,
(X := X + 1; X := 200)
is equivalent to(Y := 3)
(since they both assign to one unique variable).This file proves this is an equivalence relation, and shows that it is not a congruence.