diff --git a/coq/.gitignore b/coq/.gitignore
new file mode 100644
index 0000000..a0a367a
--- /dev/null
+++ b/coq/.gitignore
@@ -0,0 +1,7 @@
+*.vo
+*.glob
+*.v.d
+.*.aux
+.coq-native
+_CoqProject
+*~
diff --git a/coq/DemoSyntaxReduction.v b/coq/DemoSyntaxReduction.v
new file mode 100644
index 0000000..549a787
--- /dev/null
+++ b/coq/DemoSyntaxReduction.v
@@ -0,0 +1,226 @@
+Require Import MyTactics.
+Require Import Autosubst.Autosubst.
+
+(* This file is intended as a mini-demonstration of:
+   1. defining the syntax of a calculus, in de Bruijn's representation;
+   2. equipping it with an operational semantics;
+   3. proving a basic lemma, e.g.,
+      stability of the semantics under substitution. *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* The syntax of the lambda-calculus. *)
+
+Inductive term :=
+| Var:          var -> term
+| Lam:  {bind term} -> term
+| App: term -> term -> term
+.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The following incantations let [AutoSubst] work its magic for us.
+   We obtain, for free, the operations of de Bruijn algebra: application
+   of a substitution to a term, composition of substitutions, etc. *)
+
+Instance Ids_term : Ids term. derive. Defined.
+Instance Rename_term : Rename term. derive. Defined.
+Instance Subst_term : Subst term. derive. Defined.
+Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A demo of the tactics [autosubst] and [asimpl]. *)
+
+Goal
+  forall sigma,
+  (Lam (App (Var 0) (Var 1))).[sigma] =
+   Lam (App (Var 0) (sigma 0).[ren (+1)]).
+Proof.
+  intros.
+  (* The tactic [autosubst] proves this equality. *)
+  autosubst.
+Restart.
+  intros.
+  (* If desired, we can first simplify this equality using [asimpl]. *)
+  asimpl.
+  (* [ids], the identity substitution, maps 0 to [Var 0], 1 to [Var 1],
+     and so on, so it is really equal to [Var] itself. As a result, the
+     built-in tactic [reflexivity] proves this simplified equation. *)
+  reflexivity.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* More demos: let us check that the laws of substitution are satisfied. *)
+
+Lemma subst_var:
+  forall x sigma,
+  (Var x).[sigma] = sigma x.
+Proof.
+  autosubst.
+Qed.
+
+Lemma subst_lam:
+  forall t sigma,
+  (Lam t).[sigma] = Lam (t.[up sigma]).
+Proof.
+  autosubst.
+Qed.
+
+Lemma subst_app:
+  forall t1 t2 sigma,
+  (App t1 t2).[sigma] = App t1.[sigma] t2.[sigma].
+Proof.
+  autosubst.
+Qed.
+
+(* A reminder of the meaning of [up sigma]. *)
+
+Lemma up_def:
+  forall sigma,
+  up sigma = Var 0 .: (sigma >> ren (+1)).
+Proof.
+  intros. autosubst.
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A small-step reduction semantics. *)
+
+(* This is a relation between terms: hence, its type is [term -> term -> Prop].
+   It is inductively defined by three inference rules, as follows: *)
+
+Inductive red : term -> term -> Prop :=
+
+(* Beta-reduction. The use of an explicit equality hypothesis is a technical
+   convenience. We could instead write [red (App (Lam t1) t2) t1.[t2/]] in
+   the conclusion, and remove the auxiliary variable [u], but that would make
+   it more difficult for Coq to apply the inference rule [RedBeta]. Using an
+   explicit equality premise makes the rule more widely applicable. Of course
+   the user still has to prove (after applying the rule) that the equality
+   holds. *)
+| RedBeta:
+    forall t1 t2 u,
+    t1.[t2/] = u ->
+    red (App (Lam t1) t2) u
+
+(* Reduction in the left-hand side of an application. *)
+| RedAppL:
+    forall t1 t2 u,
+    red t1 t2 ->
+    red (App t1 u) (App t2 u)
+
+(* Reduction in the right-hand side of an application. *)
+| RedAppR:
+    forall t u1 u2,
+    red u1 u2 ->
+    red (App t u1) (App t u2)
+.
+
+(* The following means that [eauto with red] is allowed to apply the above
+   three inference rules. *)
+
+Hint Constructors red : red.
+
+(* No strategy is built into this reduction relation: it is not restricted to
+   call-by-value or call-by-name. It is nondeterministic. Only weak reduction
+   is permitted here: we have not allowed reduction under a [Lam]. These choices
+   are arbitrary: this is just a demo anyway. *)
+
+(* -------------------------------------------------------------------------- *)
+
+(* This incantation means that [eauto with autosubst] can use the tactic
+   [autosubst] to prove an equality. It is used in the last "expert" proof
+   of the lemma [red_subst] below.  *)
+
+Hint Extern 1 (_ = _) => autosubst : autosubst.
+
+(* -------------------------------------------------------------------------- *)
+
+(* Let us now prove that the semantics is stable under arbitrary substitutions. *)
+
+Lemma red_subst:
+  forall t1 t2,
+  red t1 t2 ->
+  forall sigma,
+  red t1.[sigma] t2.[sigma].
+Proof.
+
+  (* We attack a proof by induction on the derivation of [red t1 t2]. *)
+  induction 1; intros.
+  (* Case: [RedBeta]. *)
+  { subst u.
+    eapply RedBeta.
+    (* Wow -- we have to prove a complicated-looking commutation property
+       of substitutions. Fortunately, [autosubst] is here for us! *)
+    autosubst. }
+  (* Case: [RedAppL]. The proof can be done slowly, in three steps:
+     1. push the substitution into [App];
+     2. apply the rule [RedAppL]; a simpler subgoal remains to be proved;
+     3. apply the induction hypothesis, which proves this subgoal. *)
+  { asimpl.
+    eapply RedAppL.
+    eapply IHred. }
+  (* Case: [RedAppR]. The proof could be done using the same three steps
+     as above, but one can also let the last two steps be automatically
+     found by [eauto]. *)
+  { asimpl. eauto using red. }
+  (* The proof is now finished. *)
+
+  (* For the fun of it, let us do the proof again in a more "expert" style. *)
+Restart.
+  (* The proof is still by induction. All three cases begin in the same way,
+     so this common pattern can be shared, as follows. We use the semicolon
+     which in Ltac has special meaning: when one writes [command1; command2],
+     [command1] can produce multiple subgoals, and [command2] is applied to
+     every subgoal (in parallel). Thus, here, in each of the three cases,
+     we perform the sequence of commands [intros; subst; asimpl; econstructor].
+     The effect of [econstructor] is to apply one of [RedBeta], [RedAppL] and
+     [RedAppR] -- whichever is applicable. *)
+  induction 1; intros; subst; asimpl; econstructor.
+  (* Then, the three subgoals can be finished as follows: *)
+  { autosubst. }
+  { eauto. }
+  { eauto. }
+  (* The proof is now finished (again). *)
+
+  (* For the fun of it, let us redo the proof in an even more expert style.
+     We remark that each of the three subgoals can be proved by [eauto with
+     autosubst], so we can write a fully shared command, where the subgoals
+     are no longer distinguished: *)
+Restart.
+  induction 1; intros; subst; asimpl; econstructor; eauto with autosubst.
+  (* The proof is now finished (yet again). *)
+
+  (* There are several lessons that one can draw from this demo:
+
+     1. The machine helps us by keeping track of what we may assume
+        and what we have to prove.
+
+     2. There are several ways in which a proof can be written. In the
+        beginning, it is advisable to write a step-by-step, simple-minded
+        proof; later on, when the proof is finished and well-understood,
+        it can be revisited for greater compactness and sharing.
+
+     3. The proof of this lemma *can* fit in one line. On paper, one
+        would say that the proof is "by induction" and "immediate".
+        Here, we are able to be almost as concise, yet we have much
+        greater confidence.
+
+     4. The point of the "expert" proof is not just to make the proof
+        more concise: the point is also to make the proof more robust
+        in the face of future evolution. For instance, as an EXERCISE,
+        extend the calculus with pairs and projections, and see how the
+        proof scripts must be extended. You should find that the last
+        "expert" proof above requires no change at all!
+
+  *)
+
+Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(* As another EXERCISE, extend the operational semantics with a rule that
+   allows strong reduction, that is, reduction under a lambda-abstraction.
+   This exercise is more difficult; do not hesitate to ask for help or hints. *)
diff --git a/coq/Makefile b/coq/Makefile
new file mode 100644
index 0000000..2c6ec87
--- /dev/null
+++ b/coq/Makefile
@@ -0,0 +1,2 @@
+COQINCLUDE := -R $(shell pwd) MPRI
+include Makefile.coq
diff --git a/coq/Makefile.coq b/coq/Makefile.coq
new file mode 100644
index 0000000..247f37c
--- /dev/null
+++ b/coq/Makefile.coq
@@ -0,0 +1,188 @@
+############################################################################
+# Requirements.
+
+# We need bash. We use the pipefail option to control the exit code of a
+# pipeline.
+
+SHELL := /usr/bin/env bash
+
+############################################################################
+# Configuration
+#
+#
+# This Makefile relies on the following variables:
+# COQBIN     (default: empty)
+# COQFLAGS   (default: empty) (passed to coqc and coqide, not coqdep)
+# COQINCLUDE (default: empty)
+# V          (default: *.v)
+# V_AUX      (default: undefined/empty)
+# SERIOUS    (default: 1)
+#            (if 0, we produce .vio files)
+#            (if 1, we produce .vo files in the old way)
+# VERBOSE    (default: undefined)
+#            (if defined, commands are displayed)
+
+# We usually refer to the .v files using relative paths (such as Foo.v)
+# but [coqdep -R] produces dependencies that refer to absolute paths
+# (such as /bar/Foo.v). This confuses [make], which does not recognize
+# that these files are the same. As a result, [make] does not respect
+# the dependencies.
+
+# We fix this by using ABSOLUTE PATHS EVERYWHERE. The paths used in targets,
+# in -R options, etc., must be absolute paths.
+
+ifndef V
+	PWD := $(shell pwd)
+	V := $(wildcard $(PWD)/*.v)
+endif
+
+# Typically, $(V) should list only the .v files that we are ultimately
+# interested in checking. $(V_AUX) should list every other .v file in the
+# project. $(VD) is obtained from $(V) and $(V_AUX), so [make] sees all
+# dependencies and can rebuild files anywhere in the project, if needed, and
+# only if needed.
+
+ifndef VD
+	VD  := $(patsubst %.v,%.v.d,$(V) $(V_AUX))
+endif
+
+VIO := $(patsubst %.v,%.vio,$(V))
+VQ  := $(patsubst %.v,%.vq,$(V))
+VO  := $(patsubst %.v,%.vo,$(V))
+
+SERIOUS := 1
+
+############################################################################
+# Binaries
+
+COQC   := $(COQBIN)coqc $(COQFLAGS)
+COQDEP := $(COQBIN)coqdep
+COQIDE := $(COQBIN)coqide $(COQFLAGS)
+
+############################################################################
+# Targets
+
+.PHONY: all proof depend quick proof_vo proof_vq
+
+all: proof
+ifeq ($(SERIOUS),0)
+proof: proof_vq
+else
+proof: proof_vo
+endif
+proof_vq: $(VQ)
+depend: $(VD)
+quick: $(VIO)
+proof_vo: $(VO)
+
+############################################################################
+# Verbosity control.
+
+# Our commands are pretty long (due, among other things, to the use of
+# absolute paths everywhere). So, we hide them by default, and echo a short
+# message instead. However, sometimes one wants to see the command.
+
+# By default, VERBOSE is undefined, so the .SILENT directive is read, so no
+# commands are echoed. If VERBOSE is defined by the user, then the .SILENT
+# directive is ignored, so commands are echoed, unless they begin with an
+# explicit @.
+
+ifndef VERBOSE
+.SILENT:
+endif
+
+############################################################################
+# Verbosity filter.
+
+# Coq is way too verbose when using one of the -schedule-* commands.
+# So, we grep its output and remove any line that contains 'Checking task'.
+
+# We need a pipe that keeps the exit code of the *first* process. In
+# bash, when the pipefail option is set, the exit code is the logical
+# conjunction of the exit codes of the two processes. If we make sure
+# that the second process always succeeds, then we get the exit code
+# of the first process, as desired.
+
+############################################################################
+# Rules
+
+# If B uses A, then the dependencies produced by coqdep are:
+# B.vo:  B.v A.vo
+# B.vio: B.v A.vio
+
+%.v.d: %.v
+	$(COQDEP) $(COQINCLUDE) $< > $@
+
+ifeq ($(SERIOUS),0)
+
+%.vo: %.vio
+	@echo "Compiling `basename $*`..."
+	set -o pipefail; ( \
+	  $(COQC) $(COQINCLUDE) -schedule-vio2vo 1 $* \
+	  2>&1 | (grep -v 'Checking task' || true))
+
+# The recipe for producing %.vio destroys %.vo. In other words, we do not
+# allow a young .vio file to co-exist with an old (possibly out-of-date) .vo
+# file, because this seems to lead Coq into various kinds of problems
+# ("inconsistent assumption" errors, "undefined universe" errors, warnings
+# about the existence of both files, and so on). Destroying %.vo should be OK
+# as long as the user does not try to build a mixture of .vo and .vio files in
+# one invocation of make.
+%.vio: %.v
+	@echo "Digesting `basename $*`..."
+	rm -f $*.vo
+	$(COQC) $(COQINCLUDE) -quick $<
+
+%.vq: %.vio
+	@echo "Checking `basename $*`..."
+	set -o pipefail; ( \
+	  $(COQC) $(COQINCLUDE) -schedule-vio-checking 1 $< \
+	  2>&1 | (grep -v 'Checking task' || true))
+	touch $@
+
+endif
+
+ifeq ($(SERIOUS),1)
+
+%.vo: %.v
+	@echo "Compiling `basename $*`..."
+	$(COQC) $(COQINCLUDE) $<
+
+endif
+
+_CoqProject: .FORCE
+	@echo $(COQINCLUDE) > $@
+
+.FORCE:
+
+############################################################################
+# Dependencies
+
+ifeq ($(findstring $(MAKECMDGOALS),depend clean),)
+-include $(VD)
+endif
+
+############################################################################
+# IDE
+
+.PHONY: ide
+
+.coqide:
+	@echo '$(COQIDE) $(COQINCLUDE) $$*' > .coqide
+	@chmod +x .coqide
+
+ide: _CoqProject
+	$(COQIDE) $(COQINCLUDE)
+
+############################################################################
+# Clean
+
+.PHONY: clean
+
+clean::
+	rm -f *~
+	rm -f $(patsubst %.v,%.v.d,$(V)) # not $(VD)
+	rm -f $(VIO) $(VO) $(VQ)
+	rm -f *.aux .*.aux *.glob *.cache *.crashcoqide
+	rm -rf .coq-native .coqide
+# TEMPORARY *~, *.aux, etc. do not make sense in a multi-directory setting
diff --git a/coq/MyTactics.v b/coq/MyTactics.v
new file mode 100644
index 0000000..fec7992
--- /dev/null
+++ b/coq/MyTactics.v
@@ -0,0 +1,182 @@
+Require Export Omega.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [false] replaces the current goal with [False]. *)
+
+Ltac false :=
+  elimtype False.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [tc] is a shortcut for [eauto with typeclass_instances]. For some reason,
+   it is often necessary to use [rewrite ... by tc]. *)
+
+Ltac tc :=
+  eauto with typeclass_instances.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The tactic [obvious] does nothing by default, but can be extended with hints
+   so as to solve relatively easy goals -- e.g., proving that a term is a value,
+   proving a size inequality, proving that a substitution is a renaming, etc.
+   These predicates are sometimes interrelated (e.g., size is preserved by
+   renamings; the property of being a value is preserved by renamings) so it
+   would be counterproductive to distinguish several hint databases. *)
+
+Create HintDb obvious.
+
+Ltac obvious :=
+  eauto with obvious typeclass_instances.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The tactic [pick R k] picks a hypothesis [h] whose statement is an
+   application of the inductive predicate [R], and passes [h] to the (Ltac)
+   continuation [k]. *)
+
+Ltac pick R k :=
+  match goal with
+  | h: R _         |- _ => k h
+  | h: R _ _       |- _ => k h
+  | h: R _ _ _     |- _ => k h
+  | h: R _ _ _ _   |- _ => k h
+  | h: R _ _ _ _ _ |- _ => k h
+  end.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The tactic [invert h] case-analyzes the hypothesis [h], whose statement
+   should be an application of an inductive predicate. *)
+
+Ltac invert h :=
+  inversion h; clear h; try subst.
+
+(* The tactic [inv R] looks for a hypothesis [h] whose statement is an
+   application of the inductive predicate [R], and case-analyzes this
+   hypothesis. *)
+
+Ltac inv R :=
+  pick R invert.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The tactic [unpack] decomposes conjunctions and existential quantifiers
+   in the hypotheses. Then, it attempts to perform substitutions, if possible. *)
+
+Ltac unpack :=
+  repeat match goal with
+  | h: _ /\ _ |- _ =>
+      destruct h
+  | h: exists _, _ |- _ =>
+      destruct h
+  end;
+  try subst.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The tactic [forward H] introduces the term [H] as a new hypothesis, and
+   unpacks it (if necessary). *)
+
+Ltac forward H :=
+  generalize H; intro; unpack.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [push h] moves the hypothesis [h] into the goal. *)
+
+Ltac push h :=
+  generalize h; clear h.
+
+(* [ltac_Mark] and [ltac_mark] are dummies. They are used as sentinels by
+   certain tactics, to mark a position in the context or in the goal. *)
+
+Inductive ltac_Mark : Type :=
+| ltac_mark : ltac_Mark.
+
+(* [push_until_mark] moves all hypotheses from the context into the goal,
+   starting from the bottom and stopping as soon as a mark (that is, a
+   hypothesis of type [ltac_Mark]) is reached. The mark is thrown away. The
+   tactic fails if no mark appears in the context. *)
+
+Ltac push_until_mark :=
+  match goal with h: ?T |- _ =>
+  match T with
+  | ltac_Mark => clear h
+  | _ => push h; push_until_mark
+  end end.
+
+(** [pop_until_mark] moves all hypotheses from the goal into the context,
+    until a hypothesis of type [ltac_Mark] is reached. The mark is thrown
+    away. The tactic fails if no mark appears in the goal. *)
+
+Ltac pop_until_mark :=
+  match goal with
+  | |- (ltac_Mark -> _) => intros _
+  | _ => intro; pop_until_mark
+  end.
+
+Ltac injections :=
+  (* Place an initial mark, so as to not disturb the goal. *)
+  generalize ltac_mark;
+  (* Look at every equality hypothesis. *)
+  repeat match goal with
+  | h: _ = _ |- _ =>
+      (* Try to apply the primitive tactic [injection] to this hypothesis.
+         If this succeeds, clear [h] and replace it with the results of
+         [injection]. Another mark is used for this purpose. If this fails,
+         just push [h] into the goal, as we do not wish to see it any more. *)
+      first [
+        generalize ltac_mark; injection h; clear h; pop_until_mark
+      | push h ]
+  end;
+  (* Pop all of the hypotheses that have been set aside above. *)
+  pop_until_mark.
+
+(* -------------------------------------------------------------------------- *)
+
+(* The following incantation means that [eauto with omega] can solve a goal
+   of the form [_ < _]. The tactic [zify] is a preprocessor which increases
+   the number of goals that [omega] can accept; e.g., it expands away [min]
+   and [max]. *)
+
+Hint Extern 1 (le _ _) => (zify; omega) : omega.
+
+(* -------------------------------------------------------------------------- *)
+
+(* A little extra help for [eauto with omega]. *)
+
+Lemma arith_le_SS: forall x y, x < y -> S x < S y.
+Proof. intros. omega. Qed.
+Lemma arith_SS_le: forall x y, S x < S y -> x < y.
+Proof. intros. omega. Qed.
+
+Hint Resolve arith_le_SS arith_SS_le : omega.
+
+(* -------------------------------------------------------------------------- *)
+
+(* [dblib_by_cases] simplifies goals in which a decidable integer comparison
+   appears. *)
+
+Ltac dblib_intro_case_clear :=
+  let h := fresh in
+  intro h; case h; clear h.
+
+Ltac dblib_inspect_cases :=
+  match goal with
+  | |- context [le_gt_dec ?n ?n'] =>
+      case (le_gt_dec n n')
+  | h: context [le_gt_dec ?n ?n'] |- _ =>
+      revert h; case (le_gt_dec n n'); intro h
+  | |- context [eq_nat_dec ?n ?n'] =>
+      case (eq_nat_dec n n')
+  | h: context [eq_nat_dec ?n ?n'] |- _ =>
+      revert h; case (eq_nat_dec n n'); intro h
+  | |- context [(lt_eq_lt_dec ?n ?n')] =>
+       case (lt_eq_lt_dec n n'); [ dblib_intro_case_clear | idtac ]
+  | h: context [(lt_eq_lt_dec ?n ?n')] |- _ =>
+       revert h; case (lt_eq_lt_dec n n'); [ dblib_intro_case_clear | idtac ]; intro h
+  end.
+
+Ltac dblib_by_cases :=
+  repeat dblib_inspect_cases; try solve [ intros; elimtype False; omega ]; intros.