From b3444f48d29197077c5ca2f80dd6e032f2d67217 Mon Sep 17 00:00:00 2001 From: t Date: Thu, 28 Apr 2016 16:08:49 -0400 Subject: [PATCH 1/3] Using coq_makefile for the Coq sources compilation, with namespace --- .gitignore | 2 ++ AssocList.v | 8 ++++---- AssumeList.v | 35 +++++++++++++++++------------------ Attic/MetatheoryEnv.v | 10 +++++----- Attic/MyAssumeList.v | 5 +++++ CoqListFacts.v | 8 ++++---- CoqUniquenessTacEx.v | 8 ++++---- FSetExtra.v | 2 +- FSetWeakNotin.v | 2 +- Fsub_LetSum_Definitions.v | 2 +- Fsub_LetSum_Infrastructure.v | 2 +- Fsub_LetSum_Lemmas.v | 2 +- Fsub_LetSum_Soundness.v | 2 +- LibLNgen.v | 4 ++-- Makefile | 24 +++++++++++++++++++++--- Metatheory.v | 12 ++++++------ MetatheoryAlt.v | 12 ++++++------ MetatheoryAtom.v | 10 +++++----- STLC.v | 6 +++--- STLCsol.v | 6 +++--- 20 files changed, 93 insertions(+), 69 deletions(-) diff --git a/.gitignore b/.gitignore index fcb275d..63ef418 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,5 @@ /*.vo /*.glob /.*.aux +CoqSrc.mk +_CoqProject diff --git a/AssocList.v b/AssocList.v index e010dba..25946ba 100644 --- a/AssocList.v +++ b/AssocList.v @@ -20,9 +20,9 @@ Require Import Coq.FSets.FSets. Require Import Coq.Lists.List. Require Import Coq.Logic.Decidable. -Require Import CoqFSetDecide. -Require Import CoqListFacts. -Require Import LibTactics. +Require Import Metalib.CoqFSetDecide. +Require Import Metalib.CoqListFacts. +Require Import Metalib.LibTactics. (* *********************************************************************** *) @@ -635,7 +635,7 @@ Section BindsProperties. binds x a (y ~ b) -> x = y. Proof. - clear. intros H. inversion H as [HEq | HIn]. + clear. intros H. inversion H as [HEq | HIn]. inversion HEq; intuition. inversion HIn. Qed. diff --git a/AssumeList.v b/AssumeList.v index 50bbb54..bdfd64e 100644 --- a/AssumeList.v +++ b/AssumeList.v @@ -14,13 +14,13 @@ Require Import Coq.FSets.FSets. Require Import Coq.Lists.List. Require Import Coq.Logic.Decidable. -Require Import CoqFSetDecide. -Require Import CoqListFacts. -Require Import LibTactics. +Require Import Metalib.CoqFSetDecide. +Require Import Metalib.CoqListFacts. +Require Import Metalib.LibTactics. -Require Import MetatheoryAtom. +Require Import Metalib.MetatheoryAtom. Import AtomSetImpl. -Require Import LibTactics. +Require Import Metalib.LibTactics. (* *********************************************************************** *) @@ -65,7 +65,7 @@ Require Import LibTactics. . Definition map (f1 : A -> A) (f2: B -> B) (E : list (asn A B)) : list (asn A B) := - List.map (fun x => match x with + List.map (fun x => match x with | VarAsn _ x a => VarAsn B x (f1 a) | AltAsn _ b => AltAsn A (f2 b) end) E. @@ -96,17 +96,17 @@ Require Import LibTactics. uniq E -> x `notin` dom E -> uniq ((x ~~ a) ++ E) - | uniq_alt : forall b E, - uniq E -> + | uniq_alt : forall b E, + uniq E -> uniq (one (AltAsn A b) ++ E). Fixpoint erase (E : list (asn A B)) : list B := - match E with + match E with | nil => nil | (AltAsn _ b) :: E => b :: erase E - | (VarAsn _ x a) :: E => erase E + | (VarAsn _ x a) :: E => erase E end. - + Unset Implicit Arguments. End Definitions. @@ -462,7 +462,7 @@ Require Import LibTactics. uniq (E ++ F) -> uniq E. Proof. clear. intros H; induction E as [ | a E']; simpl_asnlist in *. - apply uniq_nil. + apply uniq_nil. destruct a. apply uniq_push; inversion H; subst. auto. @@ -507,7 +507,7 @@ Require Import LibTactics. intuition. rewrite disjoint_one_l in Hd. simpl_asnlist. fsetdec. apply uniq_alt. - inversion HE; subst. + inversion HE; subst. intuition. Qed. @@ -870,9 +870,9 @@ Require Import LibTactics. unfold binds in *. simpl. intros [? | ?]. destruct a0. inversion H; subst. - left. congruence. + left. congruence. inversion H. - destruct a0. + destruct a0. right. auto. right. auto. Qed. @@ -889,8 +889,8 @@ Require Import LibTactics. clear. induction E as [ | y ? F ]; intros J; simpl_asnlist. analyze_binds J. analyze_binds J; subst; auto with set. - inversion H0;subst. simpl. fsetdec. - inversion H. + inversion H0;subst. simpl. fsetdec. + inversion H. Qed. Lemma fresh_app_l : @@ -917,4 +917,3 @@ Require Import LibTactics. - \ No newline at end of file diff --git a/Attic/MetatheoryEnv.v b/Attic/MetatheoryEnv.v index 5085597..b2214ab 100644 --- a/Attic/MetatheoryEnv.v +++ b/Attic/MetatheoryEnv.v @@ -19,13 +19,13 @@ Require Import Coq.FSets.FSets. Require Import Coq.Lists.List. Require Import Coq.Logic.Decidable. -Require Import CoqFSetDecide. -Require Import CoqListFacts. +Require Import Metalib.CoqFSetDecide. +Require Import Metalib.CoqListFacts. -Require Import AssocList. -Require Import MetatheoryAtom. +Require Import Metalib.AssocList. +Require Import Metalib.MetatheoryAtom. Import AtomSetImpl. -Require Import LibTactics. +Require Import Metalib.LibTactics. (* *********************************************************************** *) diff --git a/Attic/MyAssumeList.v b/Attic/MyAssumeList.v index 8f10ea0..8fa9514 100644 --- a/Attic/MyAssumeList.v +++ b/Attic/MyAssumeList.v @@ -126,6 +126,8 @@ Open Scope list_scope. (** [dom] computes the domain of an assumption list, i.e., the set consisting of its keys. *) +(* FIXME: commented out by simplicity, but the code should be fixed *) +(* Fixpoint dom (A B : Type) (E : list (asn A B)) : KeySet.t := @@ -1552,4 +1554,7 @@ Hint Resolve @binds_weaken. Hint Immediate @binds_remove_mid @binds_In. +*) + End Make. + diff --git a/CoqListFacts.v b/CoqListFacts.v index 06e2be9..e3f0d72 100644 --- a/CoqListFacts.v +++ b/CoqListFacts.v @@ -10,7 +10,7 @@ Require Import Coq.Lists.List. Require Import Coq.Lists.SetoidList. -Require Import CoqUniquenessTac. +Require Import Metalib.CoqUniquenessTac. Open Scope list_scope. @@ -126,7 +126,7 @@ Qed. Lemma InA_iff_In : forall (A : Type) (x : A) (xs : list A), InA (@eq _) x xs <-> In x xs. -Proof. +Proof. split; auto using InA_In. apply SetoidList.In_InA. apply eq_equivalence. Qed. @@ -230,7 +230,7 @@ Section Uniqueness_Of_SetoidList_Proofs. Theorem lelistA_unique : forall (x : A) (xs : list A) (p q : lelistA R x xs), p = q. - Proof. induction p using lelistA_ind'; uniqueness 1. Qed. + Proof. induction p using lelistA_ind'; uniqueness 1. Qed. Theorem sort_unique : forall (xs : list A) (p q : sort R xs), p = q. @@ -238,6 +238,6 @@ Section Uniqueness_Of_SetoidList_Proofs. Theorem eqlistA_unique : forall (xs ys : list A) (p q : eqlistA R xs ys), p = q. - Proof. induction p using eqlistA_ind'; uniqueness 2. Qed. + Proof. induction p using eqlistA_ind'; uniqueness 2. Qed. End Uniqueness_Of_SetoidList_Proofs. diff --git a/CoqUniquenessTacEx.v b/CoqUniquenessTacEx.v index f8e0f2f..0ebe7d4 100644 --- a/CoqUniquenessTacEx.v +++ b/CoqUniquenessTacEx.v @@ -9,7 +9,7 @@ Require Import Coq.Arith.Peano_dec. Require Import Coq.Lists.SetoidList. Require Import Coq.omega.Omega. -Require Import CoqUniquenessTac. +Require Import Metalib.CoqUniquenessTac. (* *********************************************************************** *) @@ -31,8 +31,8 @@ Proof. induction p using le_ind'; uniqueness 1; assert False by omega; intuition. - -Qed. + +Qed. (* ********************************************************************** *) @@ -64,7 +64,7 @@ Section Uniqueness_Of_SetoidList_Proofs. Theorem eqlistA_unique : forall (xs ys : list A) (p q : eqlistA R xs ys), p = q. - Proof. induction p using eqlistA_ind'; uniqueness 2. Qed. + Proof. induction p using eqlistA_ind'; uniqueness 2. Qed. End Uniqueness_Of_SetoidList_Proofs. diff --git a/FSetExtra.v b/FSetExtra.v index 6ffa783..eb998a6 100644 --- a/FSetExtra.v +++ b/FSetExtra.v @@ -8,7 +8,7 @@ Require Import Coq.FSets.FSets. -Require Import CoqFSetInterface. +Require Import Metalib.CoqFSetInterface. (* *********************************************************************** *) diff --git a/FSetWeakNotin.v b/FSetWeakNotin.v index 33a20ad..1fbd5bf 100644 --- a/FSetWeakNotin.v +++ b/FSetWeakNotin.v @@ -14,7 +14,7 @@ Require Import Coq.FSets.FSetInterface. -Require Import CoqFSetDecide. +Require Import Metalib.CoqFSetDecide. (* *********************************************************************** *) diff --git a/Fsub_LetSum_Definitions.v b/Fsub_LetSum_Definitions.v index d7524d2..8bb73f9 100644 --- a/Fsub_LetSum_Definitions.v +++ b/Fsub_LetSum_Definitions.v @@ -16,7 +16,7 @@ - #Automation# *) -Require Export Metatheory. +Require Export Metalib.Metatheory. (* ********************************************************************** *) diff --git a/Fsub_LetSum_Infrastructure.v b/Fsub_LetSum_Infrastructure.v index 5d50d62..1e7f302 100644 --- a/Fsub_LetSum_Infrastructure.v +++ b/Fsub_LetSum_Infrastructure.v @@ -19,7 +19,7 @@ - #Automation# - #Properties of body_e# *) -Require Export Fsub_LetSum_Definitions. +Require Export Metalib.Fsub_LetSum_Definitions. (* ********************************************************************** *) diff --git a/Fsub_LetSum_Lemmas.v b/Fsub_LetSum_Lemmas.v index 55209a5..55e70b3 100644 --- a/Fsub_LetSum_Lemmas.v +++ b/Fsub_LetSum_Lemmas.v @@ -21,7 +21,7 @@ - #Regularity lemmas# - #Automation# *) -Require Export Fsub_LetSum_Infrastructure. +Require Export Metalib.Fsub_LetSum_Infrastructure. (* ********************************************************************** *) diff --git a/Fsub_LetSum_Soundness.v b/Fsub_LetSum_Soundness.v index 04f639f..c688be7 100644 --- a/Fsub_LetSum_Soundness.v +++ b/Fsub_LetSum_Soundness.v @@ -12,7 +12,7 @@ - #Preservation# - #Progress# *) -Require Export Fsub_LetSum_Lemmas. +Require Export Metalib.Fsub_LetSum_Lemmas. (* ********************************************************************** *) diff --git a/LibLNgen.v b/LibLNgen.v index 52cfa4e..170bd32 100644 --- a/LibLNgen.v +++ b/LibLNgen.v @@ -7,8 +7,8 @@ (** A library of code for supporting LNgen. *) -Require Export LibDefaultSimp. -Require Import Metatheory. +Require Export Metalib.LibDefaultSimp. +Require Import Metalib.Metatheory. Require Import Omega. diff --git a/Makefile b/Makefile index d807cdd..0f30cf1 100644 --- a/Makefile +++ b/Makefile @@ -25,6 +25,15 @@ COQC = coqc COQDEP = coqdep COQDOC = coqdoc + +## Library name used for the imports in Coq + +LIBNAME=Metalib + +## Name of the submakefile generated by coq_makefile + +COQMKFILENAME=CoqSrc.mk + ## Include directories, one per line. INCDIRS = \ @@ -35,6 +44,7 @@ INCDIRS = \ DOCDIR = doc/html ## List of files to be compiled and documented. +# TODO: should be useless once we get coq_makefile to compile the documentation as well FILES = \ AssocList \ @@ -75,10 +85,17 @@ INCFLAGS = $(foreach i, $(INCDIRS), -I $(i)) .PHONY: all clean coq dist doc documentation gens .SUFFIXES: .v .vo -all: Metatheory.vo MetatheoryAlt.vo LibLNgen.vo +all: coq # Metatheory.vo MetatheoryAlt.vo LibLNgen.vo + +#coq: $(VOFILES) +coq: $(COQMKFILENAME) + # FIXME: loose integration right now, but when the doc works we should be able to simply include the generated makefile + @$(MAKE) -f CoqSrc.mk -coq: $(VOFILES) +$(COQMKFILENAME): Makefile + { echo "-R . $(LIBNAME) " ; find -name '*.v' -print; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME) +# TODO: in theory, coq_makefile creates targets for documentation, so we should be able to use it instead of handwritten rules doc: +make documentation @@ -87,7 +104,8 @@ documentation: $(DOCDIR) $(VOFILES) cp -f custom.css $(DOCDIR)/coqdoc.css clean: - rm -f *.vo *.glob *.cmi *.cmx *.o + #rm -f *.vo *.glob *.cmi *.cmx *.o + @$(MAKE) -f CoqSrc.mk clean rm -rf $(DOCDIR) ############################################################################ diff --git a/Metatheory.v b/Metatheory.v index 199c0eb..7106b1d 100644 --- a/Metatheory.v +++ b/Metatheory.v @@ -10,11 +10,11 @@ Require Export Coq.Arith.Arith. Require Export Coq.FSets.FSets. Require Export Coq.Lists.List. -Require Export AssocList. -Require Export CoqEqDec. -Require Export CoqListFacts. -Require Export LibTactics. -Require Export MetatheoryAtom. +Require Export Metalib.AssocList. +Require Export Metalib.CoqEqDec. +Require Export Metalib.CoqListFacts. +Require Export Metalib.LibTactics. +Require Export Metalib.MetatheoryAtom. (* ********************************************************************** *) @@ -292,5 +292,5 @@ Ltac apply_fresh_base H gather_vars atom_name := (* SCW added this one for list support *) Set Implicit Arguments. -Definition union_map (A:Set) (f:A -> vars) (l:list A) := +Definition union_map (A:Set) (f:A -> vars) (l:list A) := (List.fold_right (fun t acc => f t \u acc) {}) l. diff --git a/MetatheoryAlt.v b/MetatheoryAlt.v index 5b8b515..6e9cdda 100644 --- a/MetatheoryAlt.v +++ b/MetatheoryAlt.v @@ -10,13 +10,13 @@ Require Export Coq.Arith.Arith. Require Export Coq.FSets.FSets. Require Export Coq.Lists.List. -Require Export CoqEqDec. -Require Export CoqListFacts. -Require Export LibTactics. -Require Export MetatheoryAtom. +Require Export Metalib.CoqEqDec. +Require Export Metalib.CoqListFacts. +Require Export Metalib.LibTactics. +Require Export Metalib.MetatheoryAtom. (* Require Export MetatheoryEnv. *) -Require Export AssumeList. +Require Export Metalib.AssumeList. (* ********************************************************************** *) (** * Decidable equality *) @@ -94,7 +94,7 @@ Open Scope set_hs_scope. standard recursive notation for lists, e.g., the one found in the Program library of Coq's standard library. *) -(* Notation "[ x ]" := (EnvImpl.one x) : env_scope. +(* Notation "[ x ]" := (EnvImpl.one x) : env_scope. Open Scope env_scope. *) diff --git a/MetatheoryAtom.v b/MetatheoryAtom.v index 3664f90..6c48242 100644 --- a/MetatheoryAtom.v +++ b/MetatheoryAtom.v @@ -12,11 +12,11 @@ Require Import Coq.Classes.EquivDec. Require Import Coq.Lists.List. Require Import Coq.Structures.DecidableTypeEx. -Require Import CoqFSetDecide. -Require Import CoqListFacts. -Require Import FSetExtra. -Require Import FSetWeakNotin. -Require Import LibTactics. +Require Import Metalib.CoqFSetDecide. +Require Import Metalib.CoqListFacts. +Require Import Metalib.FSetExtra. +Require Import Metalib.FSetWeakNotin. +Require Import Metalib.LibTactics. Require Import Omega. diff --git a/STLC.v b/STLC.v index 8658251..36f3991 100644 --- a/STLC.v +++ b/STLC.v @@ -56,7 +56,7 @@ directory to compile the Metatheory library. *) -Require Import Metatheory. +Require Import Metalib.Metatheory. (*************************************************************************) @@ -1215,7 +1215,7 @@ Proof. induction H; intros G Eq Uniq; subst. (* FILL IN HERE (and delete "Admitted") *) Admitted. - + (** *** Example @@ -1339,7 +1339,7 @@ Lemma typing_c_subst : forall (E F : env) e u S T (z : atom), Proof. (* FILL IN HERE (and delete "Admitted") *) Admitted. - + (** *** Exercise Complete the proof of the substitution lemma stated in the form we diff --git a/STLCsol.v b/STLCsol.v index 1e15401..f89fad6 100644 --- a/STLCsol.v +++ b/STLCsol.v @@ -56,7 +56,7 @@ directory to compile the Metatheory library. *) -Require Import Metatheory. +Require Import Metalib.Metatheory. (*************************************************************************) @@ -1330,7 +1330,7 @@ Proof. apply binds_weaken. apply H0. Case "typing_abs_c". - + pick fresh x and apply typing_abs_c. rewrite_env (((x ~ T1) ++ G) ++ F ++ E). apply H0. @@ -1494,7 +1494,7 @@ Proof. subst. simpl. - + pick fresh y and apply typing_abs_c. rewrite subst_open_var_c. rewrite_env (((y ~ T1) ++ F) ++ E). From ee61e9d916d6a5438f967e6cb162fdcb80d881a4 Mon Sep 17 00:00:00 2001 From: Stephanie Weirich Date: Wed, 4 May 2016 14:35:26 -0400 Subject: [PATCH 2/3] find to ls --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 0f30cf1..bafd6d7 100644 --- a/Makefile +++ b/Makefile @@ -93,7 +93,7 @@ coq: $(COQMKFILENAME) @$(MAKE) -f CoqSrc.mk $(COQMKFILENAME): Makefile - { echo "-R . $(LIBNAME) " ; find -name '*.v' -print; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME) + { echo "-R . $(LIBNAME) " ; ls *.v ; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME) # TODO: in theory, coq_makefile creates targets for documentation, so we should be able to use it instead of handwritten rules doc: From e417b18c846273dfced9ab8d0cdfa271ef141a5c Mon Sep 17 00:00:00 2001 From: Antal Spector-Zabusky Date: Wed, 15 Jun 2016 14:01:43 -0400 Subject: [PATCH 3/3] Ingore `.d` files --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 63ef418..4633a6a 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ /*.vo /*.glob /.*.aux +/*.v.d CoqSrc.mk _CoqProject