1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
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
|