From 399dee93ae548e83447a514917cf5409ab7c2c8f Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Mon, 10 Jul 2017 18:15:14 -0700 Subject: [PATCH] coqPackages.autosubst: New expression --- .../0001-changes-to-work-with-Coq-8.6.patch | 134 ++++++++++++++++++ .../coq-modules/autosubst/default.nix | 27 ++++ pkgs/top-level/all-packages.nix | 2 + 3 files changed, 163 insertions(+) create mode 100644 pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch create mode 100644 pkgs/development/coq-modules/autosubst/default.nix diff --git a/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch b/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch new file mode 100644 index 000000000000..dde0e2e03eb6 --- /dev/null +++ b/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch @@ -0,0 +1,134 @@ +From 5b40a32e35fe446cda20ed34c756a010856f39ce Mon Sep 17 00:00:00 2001 +From: Theo Giannakopoulos +Date: Wed, 5 Apr 2017 15:48:55 -0400 +Subject: [PATCH] changes to work with Coq 8.6 + +--- + theories/Autosubst_Derive.v | 12 ++++++++++++ + theories/Autosubst_MMap.v | 3 ++- + 2 files changed, 14 insertions(+), 1 deletion(-) + +diff --git a/theories/Autosubst_Derive.v b/theories/Autosubst_Derive.v +index 61995de..cf87f67 100644 +--- a/theories/Autosubst_Derive.v ++++ b/theories/Autosubst_Derive.v +@@ -18,6 +18,7 @@ Hint Extern 0 (Ids _) => derive_Ids : derive. + + Ltac derive_Rename := + match goal with [ |- Rename ?term ] => ++ let inst := fresh "inst" in + hnf; fix inst 2; change _ with (Rename term) in inst; + intros xi s; change (annot term s); destruct s; + match goal with +@@ -66,6 +67,7 @@ Ltac has_var s := + Ltac derive_Subst := + match goal with [ |- Subst ?term ] => + require_instance (Rename term); ++ let inst := fresh "inst" in + hnf; fix inst 2; change _ with (Subst term) in inst; + intros sigma s; change (annot term s); destruct s; + match goal with +@@ -107,6 +109,7 @@ Hint Extern 0 (Subst _) => derive_Subst : derive. + Ltac derive_HSubst := + match goal with [ |- HSubst ?inner ?outer ] => + require_instance (Subst inner); ++ let inst := fresh "inst" in + hnf; fix inst 2; change _ with (HSubst inner outer) in inst; + intros sigma s; change (annot outer s); destruct s; + match goal with +@@ -327,6 +330,7 @@ Ltac derive_SubstLemmas := + assert (up_upren_n : + forall xi n, upn n (ren xi) = ren (iterate upren n xi)) by + (apply up_upren_n_internal, up_upren); ++ let ih := fresh "ih" in + fix ih 2; intros xi s; destruct s; try reflexivity; simpl; f_equal; + try apply mmap_ext; intros; rewrite ?up_upren, ?up_upren_n; apply ih); + +@@ -337,6 +341,7 @@ Ltac derive_SubstLemmas := + (apply up_id_internal; reflexivity); + assert (up_id_n : forall n, upn n ids = ids) by + (apply up_id_n_internal, up_id); ++ let ih := fresh "ih" in + fix ih 1; intros s; destruct s; simpl; f_equal; try reflexivity; + rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; apply ih); + +@@ -344,6 +349,7 @@ Ltac derive_SubstLemmas := + + assert (ren_subst_comp : + forall xi sigma (s : term), (rename xi s).[sigma] = s.[xi >>> sigma]) by( ++ let ih := fresh "ih" in + fix ih 3; intros xi sigma s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_comp_ren_subst, ?up_comp_ren_subst_n, ?mmap_comp; + try apply mmap_ext; intros; apply ih); +@@ -357,6 +363,7 @@ Ltac derive_SubstLemmas := + assert (up_comp_subst_ren_n : + forall sigma xi n, upn n (sigma >>> rename xi) = upn n sigma >>> rename (iterate upren n xi)) + by (apply up_comp_subst_ren_n_internal; apply up_comp_subst_ren); ++ let ih := fresh "ih" in + fix ih 3; intros sigma xi s; destruct s; try reflexivity; simpl; + f_equal; rewrite ?up_comp_subst_ren, ?up_comp_subst_ren_n, ?mmap_comp; + try (rewrite hcomp_ren_internal; [|apply rename_subst]); +@@ -368,6 +375,7 @@ Ltac derive_SubstLemmas := + by (apply up_comp_internal; [reflexivity|apply ren_subst_comp|apply subst_ren_comp]); + assert (up_comp_n : forall sigma tau n, upn n (sigma >> tau) = upn n sigma >> upn n tau) + by (apply up_comp_n_internal; apply up_comp); ++ let ih := fresh "ih" in + fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_comp, ?up_comp_n, ?mmap_comp, ?hcomp_dist_internal; + try apply mmap_ext; intros; apply ih); +@@ -382,6 +390,7 @@ Ltac derive_HSubstLemmas := + let ids := constr:(ids : var -> inner) in + + assert (hsubst_id : forall (s : outer), s.|[ids] = s) by ( ++ let ih := fresh "ih" in + fix ih 1; intros s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; + (apply subst_id || apply ih) +@@ -390,6 +399,7 @@ Ltac derive_HSubstLemmas := + assert (hsubst_comp : forall (theta eta : var -> inner) (s : outer), + s.|[theta].|[eta] = s.|[theta >> eta]) + by ( ++ let ih := fresh "ih" in + fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; + rewrite <- ?up_comp, <- ?up_comp_n, ?mmap_comp; try apply mmap_ext; intros; + (apply subst_comp || apply ih) +@@ -405,6 +415,7 @@ Ltac derive_SubstHSubstComp := + assert (ren_hsubst_comp : forall xi (theta : var -> inner) (s : outer), + rename xi s.|[theta] = (rename xi s).|[theta] + ) by ( ++ let ih := fresh "ih" in + fix ih 3; intros xi theta s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?mmap_comp; try apply mmap_ext; intros; simpl; apply ih + ); +@@ -421,6 +432,7 @@ Ltac derive_SubstHSubstComp := + apply up_hcomp_n_internal; apply up_hcomp + ); + ++ let ih := fresh "ih" in + fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_hcomp, ?up_hcomp_n, ?hcomp_lift_n_internal, ?mmap_comp; + try apply mmap_ext; intros; apply ih +diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v +index f8387e7..7af7902 100644 +--- a/theories/Autosubst_MMap.v ++++ b/theories/Autosubst_MMap.v +@@ -23,7 +23,7 @@ Arguments mmap {A B _} f !s /. + Class MMapExt (A B : Type) `{MMap A B} := + mmap_ext : forall f g, + (forall t, f t = g t) -> forall s, mmap f s = mmap g s. +-Arguments mmap_ext {A B _ _ f g} H s. ++Arguments mmap_ext {A B H' _ f g} H s : rename. + + Class MMapLemmas (A B : Type) `{MMap A B} := { + mmap_id x : mmap id x = x; +@@ -123,6 +123,7 @@ Tactic Notation "msimpl" "in" "*" := (in_all msimplH); msimpl. + + Ltac derive_MMap := + hnf; match goal with [ |- (?A -> ?A) -> ?B -> ?B ] => ++ let map := fresh "map" in + intros f; fix map 1; intros xs; change (annot B xs); destruct xs; + match goal with + | [ |- annot _ ?ys ] => +-- +2.13.2 + diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix new file mode 100644 index 000000000000..d27ba0052994 --- /dev/null +++ b/pkgs/development/coq-modules/autosubst/default.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchgit, coq, mathcomp }: + +stdenv.mkDerivation rec { + + name = "coq-autosubst-${coq.coq-version}-${version}"; + version = "5b40a32e"; + + src = fetchgit { + url = git://github.com/uds-psl/autosubst.git; + rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034"; + sha256 = "1wqfzc9az85fvx71xxfii502jgc3mp0r3xwfb8vnb03vkk625ln0"; + }; + + propagatedBuildInputs = [ mathcomp ]; + + patches = [./0001-changes-to-work-with-Coq-8.6.patch]; + + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + + meta = with stdenv.lib; { + homepage = https://www.ps.uni-saarland.de/autosubst/; + description = "Automation for de Bruijn syntax and substitution in Coq"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 5e4d76a9c874..491d11ca9f00 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -18013,6 +18013,7 @@ with pkgs; }; coqPackages = coqPackages_8_5; + autosubst = callPackage ../development/coq-modules/autosubst {}; coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {}; coquelicot = callPackage ../development/coq-modules/coquelicot {}; dpdgraph = callPackage ../development/coq-modules/dpdgraph {}; @@ -18031,6 +18032,7 @@ with pkgs; coq = callPackage ../applications/science/logic/coq {}; coqPackages = coqPackages_8_6; + autosubst = callPackage ../development/coq-modules/autosubst {}; coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {}; coquelicot = callPackage ../development/coq-modules/coquelicot {}; dpdgraph = callPackage ../development/coq-modules/dpdgraph {};