Skip to content

Commit c00ada4

Browse files
gilhurgilhur
committed
Remove unused imports and tactics
1 parent 0d9b1cd commit c00ada4

File tree

2 files changed

+4
-178
lines changed

2 files changed

+4
-178
lines changed

‎metasrc/pacotac_internal.py‎

Lines changed: 2 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88

99
relsize = int(sys.argv[1])
1010

11-
print ('Require Import JMeq.')
1211
print ('From Paco Require Import hpattern.')
1312
print ('From Paco Require Export paconotation_internal paconotation.')
1413
print ('Set Implicit Arguments.')
@@ -31,88 +30,6 @@
3130
print ()
3231
print ('Definition _paco_id {A} (a : A) : A := a.')
3332
print ()
34-
print ('Lemma paco_eq_JMeq: forall A (a b: A), a = b -> _paco_id (JMeq a b).')
35-
print ('Proof. intros; subst; apply JMeq_refl. Defined.')
36-
print ()
37-
print ('Lemma paco_JMeq_eq: forall (A : Type) (x y : A), _paco_id (JMeq x y) -> _paco_id (x = y).')
38-
print ('Proof. intros; apply JMeq_eq; auto. Defined.')
39-
print ()
40-
print ('Ltac simplJM :=')
41-
print (' repeat match goal with [H: ?x |- _] =>')
42-
print (' match x with')
43-
print (' | _paco_id (JMeq _ _) => apply paco_JMeq_eq in H')
44-
print (' | _paco_id (?a = _) => unfold _paco_id in H; subst a')
45-
print (' end')
46-
print (' end.')
47-
print ()
48-
print ('Tactic Notation "hrewrite_internal" constr(eqn) "at" int_or_var(occ) :=')
49-
print (' first[hrewrite eqn at occ | rewrite eqn].')
50-
print ('Ltac hrewrite_last e H := let x := fresh "_paco_x_" in')
51-
print (' first [try (set (x:=e) at 17; fail 1);')
52-
print (' first [try (set (x:=e) at 9; fail 1);')
53-
print (' first [try (set (x:=e) at 5; fail 1);')
54-
print (' first [try (set (x:=e) at 3; fail 1);')
55-
print (' first [try (set (x:=e) at 2; fail 1);')
56-
print (' try (hrewrite_internal H at 1)')
57-
print (' | try (hrewrite_internal H at 2) ]')
58-
print (' | first [try (set (x:=e) at 4; fail 1);')
59-
print (' try (hrewrite_internal H at 3)')
60-
print (' | try (hrewrite_internal H at 4) ] ]')
61-
print (' | first [try (set (x:=e) at 7; fail 1);')
62-
print (' first [try (set (x:=e) at 6; fail 1);')
63-
print (' try (hrewrite_internal H at 5)')
64-
print (' | try (hrewrite_internal H at 6)]')
65-
print (' | first [try (set (x:=e) at 8; fail 1);')
66-
print (' try (hrewrite_internal H at 7)')
67-
print (' | try (hrewrite_internal H at 8) ] ] ]')
68-
print (' | first [try (set (x:=e) at 13; fail 1);')
69-
print (' first [try (set (x:=e) at 11; fail 1);')
70-
print (' first [try (set (x:=e) at 10; fail 1);')
71-
print (' try (hrewrite_internal H at 9)')
72-
print (' | try (hrewrite_internal H at 10) ]')
73-
print (' | first [try (set (x:=e) at 12; fail 1);')
74-
print (' try (hrewrite_internal H at 11)')
75-
print (' | try (hrewrite_internal H at 12) ] ]')
76-
print (' | first [try (set (x:=e) at 15; fail 1);')
77-
print (' first [try (set (x:=e) at 14; fail 1);')
78-
print (' try (hrewrite_internal H at 13)')
79-
print (' | try (hrewrite_internal H at 14)]')
80-
print (' | first [try (set (x:=e) at 16; fail 1);')
81-
print (' try (hrewrite_internal H at 15)')
82-
print (' | try (hrewrite_internal H at 16) ] ] ] ]')
83-
print (' | first [try (set (x:=e) at 25; fail 1);')
84-
print (' first [try (set (x:=e) at 21; fail 1);')
85-
print (' first [try (set (x:=e) at 19; fail 1);')
86-
print (' first [try (set (x:=e) at 18; fail 1);')
87-
print (' try (hrewrite_internal H at 17)')
88-
print (' | try (hrewrite_internal H at 18) ]')
89-
print (' | first [try (set (x:=e) at 20; fail 1);')
90-
print (' try (hrewrite_internal H at 19)')
91-
print (' | try (hrewrite_internal H at 20) ] ]')
92-
print (' | first [try (set (x:=e) at 23; fail 1);')
93-
print (' first [try (set (x:=e) at 22; fail 1);')
94-
print (' try (hrewrite_internal H at 21)')
95-
print (' | try (hrewrite_internal H at 22)]')
96-
print (' | first [try (set (x:=e) at 24; fail 1);')
97-
print (' try (hrewrite_internal H at 23)')
98-
print (' | try (hrewrite_internal H at 24) ] ] ]')
99-
print (' | first [try (set (x:=e) at 29; fail 1);')
100-
print (' first [try (set (x:=e) at 27; fail 1);')
101-
print (' first [try (set (x:=e) at 26; fail 1);')
102-
print (' try (hrewrite_internal H at 25)')
103-
print (' | try (hrewrite_internal H at 26) ]')
104-
print (' | first [try (set (x:=e) at 28; fail 1);')
105-
print (' try (hrewrite_internal H at 27)')
106-
print (' | try (hrewrite_internal H at 28) ] ]')
107-
print (' | first [try (set (x:=e) at 31; fail 1);')
108-
print (' first [try (set (x:=e) at 30; fail 1);')
109-
print (' try (hrewrite_internal H at 29)')
110-
print (' | try (hrewrite_internal H at 30)]')
111-
print (' | first [try (set (x:=e) at 32; fail 1);')
112-
print (' try (hrewrite_internal H at 31)')
113-
print (' | try (hrewrite_internal H at 32) ] ] ] ] ]')
114-
print ('.')
115-
print ()
11633
print ('Ltac paco_generalize_hyp mark :=')
11734
print (' let y := fresh "_paco_rel_" in')
11835
print (' match goal with')
@@ -130,10 +47,6 @@
13047
print (' end')
13148
print (' end.')
13249
print ()
133-
print ('Ltac paco_convert e x EQ :=')
134-
print (' generalize (eq_refl e); generalize e at 2; intros x EQ;')
135-
print (' hrewrite_last e EQ; apply eq_sym, paco_eq_JMeq in EQ; revert x EQ.')
136-
print ()
13750
print ('Ltac paco_destruct_hyp mark :=')
13851
print (' match goal with')
13952
print (' | [x: ?A |- _] =>')
@@ -173,7 +86,7 @@
17386
print (' assert (TP: False -> PP) by (')
17487
print (' intros FP; generalize _paco_mark_cons;')
17588
print (' repeat intro; paco_rename_last; paco_destruct_hyp _paco_mark;')
176-
print (' simplJM; paco_revert_hyp _paco_mark;')
89+
print (' paco_revert_hyp _paco_mark;')
17790
print (' let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);')
17891
print (' clear TP;')
17992
print (' assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;')
@@ -192,7 +105,7 @@
192105
print (' let TMP := fresh "_paco_TMP_" in')
193106
print (' generalize _paco_mark_cons; intro TMP;')
194107
print (' repeat intro; paco_rename_last; paco_destruct_hyp _paco_mark;')
195-
print (' simplJM; paco_revert_hyp _paco_mark')
108+
print (' paco_revert_hyp _paco_mark')
196109
print (' ].')
197110
print ()
198111
print ('Ltac paco_ren_r nr cr :=')

‎src/pacotac_internal.v‎

Lines changed: 2 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
Require Import JMeq.
21
From Paco Require Import hpattern.
32
From Paco Require Export paconotation_internal paconotation.
43
Set Implicit Arguments.
@@ -21,88 +20,6 @@ Inductive _paco_foo := _paco_foo_cons.
2120

2221
Definition _paco_id {A} (a : A) : A := a.
2322

24-
Lemma paco_eq_JMeq: forall A (a b: A), a = b -> _paco_id (JMeq a b).
25-
Proof. intros; subst; apply JMeq_refl. Defined.
26-
27-
Lemma paco_JMeq_eq: forall (A : Type) (x y : A), _paco_id (JMeq x y) -> _paco_id (x = y).
28-
Proof. intros; apply JMeq_eq; auto. Defined.
29-
30-
Ltac simplJM :=
31-
repeat match goal with [H: ?x |- _] =>
32-
match x with
33-
| _paco_id (JMeq _ _) => apply paco_JMeq_eq in H
34-
| _paco_id (?a = _) => unfold _paco_id in H; subst a
35-
end
36-
end.
37-
38-
Tactic Notation "hrewrite_internal" constr(eqn) "at" int_or_var(occ) :=
39-
first[hrewrite eqn at occ | rewrite eqn].
40-
Ltac hrewrite_last e H := let x := fresh "_paco_x_" in
41-
first [try (set (x:=e) at 17; fail 1);
42-
first [try (set (x:=e) at 9; fail 1);
43-
first [try (set (x:=e) at 5; fail 1);
44-
first [try (set (x:=e) at 3; fail 1);
45-
first [try (set (x:=e) at 2; fail 1);
46-
try (hrewrite_internal H at 1)
47-
| try (hrewrite_internal H at 2) ]
48-
| first [try (set (x:=e) at 4; fail 1);
49-
try (hrewrite_internal H at 3)
50-
| try (hrewrite_internal H at 4) ] ]
51-
| first [try (set (x:=e) at 7; fail 1);
52-
first [try (set (x:=e) at 6; fail 1);
53-
try (hrewrite_internal H at 5)
54-
| try (hrewrite_internal H at 6)]
55-
| first [try (set (x:=e) at 8; fail 1);
56-
try (hrewrite_internal H at 7)
57-
| try (hrewrite_internal H at 8) ] ] ]
58-
| first [try (set (x:=e) at 13; fail 1);
59-
first [try (set (x:=e) at 11; fail 1);
60-
first [try (set (x:=e) at 10; fail 1);
61-
try (hrewrite_internal H at 9)
62-
| try (hrewrite_internal H at 10) ]
63-
| first [try (set (x:=e) at 12; fail 1);
64-
try (hrewrite_internal H at 11)
65-
| try (hrewrite_internal H at 12) ] ]
66-
| first [try (set (x:=e) at 15; fail 1);
67-
first [try (set (x:=e) at 14; fail 1);
68-
try (hrewrite_internal H at 13)
69-
| try (hrewrite_internal H at 14)]
70-
| first [try (set (x:=e) at 16; fail 1);
71-
try (hrewrite_internal H at 15)
72-
| try (hrewrite_internal H at 16) ] ] ] ]
73-
| first [try (set (x:=e) at 25; fail 1);
74-
first [try (set (x:=e) at 21; fail 1);
75-
first [try (set (x:=e) at 19; fail 1);
76-
first [try (set (x:=e) at 18; fail 1);
77-
try (hrewrite_internal H at 17)
78-
| try (hrewrite_internal H at 18) ]
79-
| first [try (set (x:=e) at 20; fail 1);
80-
try (hrewrite_internal H at 19)
81-
| try (hrewrite_internal H at 20) ] ]
82-
| first [try (set (x:=e) at 23; fail 1);
83-
first [try (set (x:=e) at 22; fail 1);
84-
try (hrewrite_internal H at 21)
85-
| try (hrewrite_internal H at 22)]
86-
| first [try (set (x:=e) at 24; fail 1);
87-
try (hrewrite_internal H at 23)
88-
| try (hrewrite_internal H at 24) ] ] ]
89-
| first [try (set (x:=e) at 29; fail 1);
90-
first [try (set (x:=e) at 27; fail 1);
91-
first [try (set (x:=e) at 26; fail 1);
92-
try (hrewrite_internal H at 25)
93-
| try (hrewrite_internal H at 26) ]
94-
| first [try (set (x:=e) at 28; fail 1);
95-
try (hrewrite_internal H at 27)
96-
| try (hrewrite_internal H at 28) ] ]
97-
| first [try (set (x:=e) at 31; fail 1);
98-
first [try (set (x:=e) at 30; fail 1);
99-
try (hrewrite_internal H at 29)
100-
| try (hrewrite_internal H at 30)]
101-
| first [try (set (x:=e) at 32; fail 1);
102-
try (hrewrite_internal H at 31)
103-
| try (hrewrite_internal H at 32) ] ] ] ] ]
104-
.
105-
10623
Ltac paco_generalize_hyp mark :=
10724
let y := fresh "_paco_rel_" in
10825
match goal with
@@ -120,10 +37,6 @@ Ltac paco_generalize_hyp mark :=
12037
end
12138
end.
12239

123-
Ltac paco_convert e x EQ :=
124-
generalize (eq_refl e); generalize e at 2; intros x EQ;
125-
hrewrite_last e EQ; apply eq_sym, paco_eq_JMeq in EQ; revert x EQ.
126-
12740
Ltac paco_destruct_hyp mark :=
12841
match goal with
12942
| [x: ?A |- _] =>
@@ -163,7 +76,7 @@ Ltac paco_simp_hyp CIH :=
16376
assert (TP: False -> PP) by (
16477
intros FP; generalize _paco_mark_cons;
16578
repeat intro; paco_rename_last; paco_destruct_hyp _paco_mark;
166-
simplJM; paco_revert_hyp _paco_mark;
79+
paco_revert_hyp _paco_mark;
16780
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
16881
clear TP;
16982
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
@@ -182,7 +95,7 @@ Ltac paco_post_simp CIH :=
18295
let TMP := fresh "_paco_TMP_" in
18396
generalize _paco_mark_cons; intro TMP;
18497
repeat intro; paco_rename_last; paco_destruct_hyp _paco_mark;
185-
simplJM; paco_revert_hyp _paco_mark
98+
paco_revert_hyp _paco_mark
18699
].
187100

188101
Ltac paco_ren_r nr cr :=

0 commit comments

Comments
 (0)