From 845312be456b17defdd91e1320a2f2b11362a4a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= Date: Thu, 21 Sep 2017 15:40:42 +0200 Subject: [PATCH] Coq demo. --- coq/.gitignore | 7 ++ coq/DemoSyntaxReduction.v | 226 ++++++++++++++++++++++++++++++++++++++ coq/Makefile | 2 + coq/Makefile.coq | 188 +++++++++++++++++++++++++++++++ coq/MyTactics.v | 182 ++++++++++++++++++++++++++++++ 5 files changed, 605 insertions(+) create mode 100644 coq/.gitignore create mode 100644 coq/DemoSyntaxReduction.v create mode 100644 coq/Makefile create mode 100644 coq/Makefile.coq create mode 100644 coq/MyTactics.v 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.