From 2e447bf4843184af454c626982ca32bf1f5536c6 Mon Sep 17 00:00:00 2001 From: Podkopaev Anton Date: Thu, 30 Aug 2018 12:33:17 +0300 Subject: [PATCH 1/3] Added OPAM related files. Modified module name in _CoqProject. --- _CoqProject | 2 +- descr | 1 + opam | 14 ++++++++++++++ 3 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 descr create mode 100644 opam diff --git a/_CoqProject b/_CoqProject index e6294ee..28f7dda 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,4 @@ --R . Top +-R . hahn Hahn.v HahnBase.v HahnFun.v HahnSets.v HahnList.v HahnRelationsBasic.v HahnEquational.v HahnRewrite.v diff --git a/descr b/descr new file mode 100644 index 0000000..8dff6e1 --- /dev/null +++ b/descr @@ -0,0 +1 @@ +Hahn is a Coq library that contains a useful collection of lemmas and tactics about lists and binary relations. diff --git a/opam b/opam new file mode 100644 index 0000000..c321484 --- /dev/null +++ b/opam @@ -0,0 +1,14 @@ +opam-version: "1.2" +name: "coq-hahn" +maintainer: "Viktor Vafeiadis " +authors: "Viktor Vafeiadis" +homepage: "https://github.com/vafeiadis/hahn" +bug-reports: "https://github.com/vafeiadis/hahn/issues" +license: "MIT" +dev-repo: "https://github.com/vafeiadis/hahn.git" +build: [make "-j%{jobs}%"] +install: [make "-f Makefile.coq install"] +remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/hahn"] +depends: [ + "coq" { (>= "8.8.1" & < "8.9~") | (= "dev") } +] From a039671d1036c5b792709d167e19b230383fc640 Mon Sep 17 00:00:00 2001 From: Podkopaev Anton Date: Mon, 3 Sep 2018 12:52:46 +0300 Subject: [PATCH 2/3] autounfold -> repeat unfold. Workaround for https://github.com/coq/coq/issues/8390 --- HahnRewrite.v | 2 +- HahnSets.v | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/HahnRewrite.v b/HahnRewrite.v index b7158d3..5272bdd 100644 --- a/HahnRewrite.v +++ b/HahnRewrite.v @@ -553,7 +553,7 @@ Tactic Notation "unfolder_prepare" "in" hyp(H) := repeat hahn_rewrite <- id_union in H. Tactic Notation "unfolder" := - unfolder_prepare; autounfold with unfolderDb. + unfolder_prepare; repeat autounfold with unfolderDb. Tactic Notation "unfolder" "in" hyp(H) := unfolder_prepare in H; autounfold with unfolderDb in H. diff --git a/HahnSets.v b/HahnSets.v index c677f3b..f91f90b 100644 --- a/HahnSets.v +++ b/HahnSets.v @@ -75,7 +75,8 @@ Hint Unfold set_collect set_bunion set_disjoint : unfolderDb. Section SetProperties. Local Ltac u := - autounfold with unfolderDb in *; ins; try solve [tauto | firstorder | split; ins; tauto]. + repeat autounfold with unfolderDb in *; + ins; try solve [tauto | firstorder | split; ins; tauto]. Variables A B C : Type. Implicit Type a : A. @@ -523,7 +524,7 @@ Lemma set_finite_coinfinite_nat (s: nat -> Prop) : Proof. assert (LT: forall l x, In x l -> x <= fold_right Init.Nat.add 0 l). induction l; ins; desf; try apply IHl in H; omega. - autounfold with unfolderDb; red; ins; desf. + repeat autounfold with unfolderDb; red; ins; desf. tertium_non_datur (s (S (fold_right plus 0 findom + fold_right plus 0 findom0))) as [X|X]; [apply H in X | apply H0 in X]; apply LT in X; omega. Qed. @@ -531,7 +532,7 @@ Qed. Lemma set_coinfinite_fresh (s: nat -> Prop) (COINF: set_coinfinite s) : exists b, ~ s b /\ set_coinfinite (s ∪₁ eq b). Proof. - autounfold with unfolderDb in *. + repeat autounfold with unfolderDb in *. tertium_non_datur (forall b, s b). by destruct COINF; exists nil; ins; desf. exists n; splits; red; ins; desf. @@ -587,7 +588,7 @@ Proof. autounfold with unfolderDb; ins; desf; eauto. Qed. Add Parametric Morphism A B : (@set_collect A B) with signature eq ==> set_equiv ==> set_equiv as set_collect_more. -Proof. autounfold with unfolderDb; splits; ins; desf; eauto. Qed. +Proof. repeat autounfold with unfolderDb; splits; ins; desf; eauto. Qed. Add Parametric Morphism A : (@set_disjoint A) with signature set_subset --> set_subset --> Basics.impl as set_disjoint_mori. From e44b33d86b1a4f68c7c59a16b25c9c16c34fe88c Mon Sep 17 00:00:00 2001 From: Podkopaev Anton Date: Tue, 4 Sep 2018 12:10:48 +0300 Subject: [PATCH 3/3] minor --- opam | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/opam b/opam index c321484..53fe724 100644 --- a/opam +++ b/opam @@ -1,13 +1,14 @@ opam-version: "1.2" name: "coq-hahn" -maintainer: "Viktor Vafeiadis " -authors: "Viktor Vafeiadis" +version: "1.1" +maintainer: "Anton Podkopaev " +authors: "Viktor Vafeiadis " homepage: "https://github.com/vafeiadis/hahn" bug-reports: "https://github.com/vafeiadis/hahn/issues" license: "MIT" dev-repo: "https://github.com/vafeiadis/hahn.git" build: [make "-j%{jobs}%"] -install: [make "-f Makefile.coq install"] +install: [make "-f" "Makefile.coq" "install"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/hahn"] depends: [ "coq" { (>= "8.8.1" & < "8.9~") | (= "dev") }