coqPackages.autosubst: New expression

3 files changed, 163 insertions, 0 deletions

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 <theo.giannakopoulos@baesystems.com>
+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 {};