tobast/mpri-funcprog-project
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Coq demo.

Browse source
This commit is contained in:
François Pottier 2017-09-21 15:40:42 +02:00
parent 906c153fb9
commit 845312be45
5 changed files with 605 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
coq/.gitignore vendored Normal file
View file

@ -0,0 +1,7 @@
*.vo
*.glob
*.v.d
.*.aux
.coq-native
_CoqProject
*~

226
coq/DemoSyntaxReduction.v Normal file
View file

@ -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. *)

2
coq/Makefile Normal file
View file

@ -0,0 +1,2 @@
COQINCLUDE := -R $(shell pwd) MPRI
include Makefile.coq

188
coq/Makefile.coq Normal file
View file

@ -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

182
coq/MyTactics.v Normal file
View file

@ -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.