Skip to content

Commit 39072d6

Browse files
gilhurgilhur
committed
Bug fix: generalize the automation in paco_simp_hyp
1 parent 5c5693f commit 39072d6

File tree

2 files changed

+102
-119
lines changed

2 files changed

+102
-119
lines changed

‎metasrc/pacotac_internal.py‎

Lines changed: 12 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -90,13 +90,12 @@
9090
print (' paco_revert_hyp _paco_mark;')
9191
print (' let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);')
9292
print (' clear TP;')
93-
print (' assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;')
94-
print (' first [')
95-
print (' (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;')
96-
print (' try (reflexivity);')
97-
print (' first [eassumption|apply _paco_foo_cons]); fail')
98-
print (' | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;')
99-
print (' (try unfold _paco_id); eauto using _paco_foo_cons)]);')
93+
print (' assert (XP: EP)')
94+
print (' by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;')
95+
print (' repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;')
96+
print (' first [exists x|split; [exists x; apply _paco_foo_cons|]];')
97+
print (' paco_revert_hyp _paco_mark);')
98+
print (' unfold _paco_id; reflexivity);')
10099
print (' unfold EP in *; clear EP CIH; rename XP into CIH.')
101100
print ()
102101
print ('Ltac paco_post_simp CIH :=')
@@ -307,13 +306,12 @@
307306
print (' paco_convert_rev'+str(n)+'; paco_revert_hyp _paco_mark;')
308307
print (' let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);')
309308
print (' clear TP;')
310-
print (' assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;')
311-
print (' first [')
312-
print (' (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;')
313-
print (' [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];')
314-
print (' first [eassumption|apply _paco_foo_cons]); fail')
315-
print (' | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;')
316-
print (' (try unfold _paco_id); eauto using _paco_foo_cons)]);')
309+
print (' assert (XP: EP)')
310+
print (' by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;')
311+
print (' repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;')
312+
print (' first [exists x|split; [exists x; apply _paco_foo_cons|]];')
313+
print (' paco_revert_hyp _paco_mark);')
314+
print (' unfold _paco_id; reflexivity);')
317315
print (' unfold EP in *; clear EP CIH; rename XP into CIH.')
318316
print ()
319317
print ('Ltac paco_post_simp'+str(n)+' CIH :=')

‎src/pacotac_internal.v‎

Lines changed: 90 additions & 105 deletions
Original file line numberDiff line numberDiff line change
@@ -80,13 +80,12 @@ Ltac paco_simp_hyp CIH :=
8080
paco_revert_hyp _paco_mark;
8181
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
8282
clear TP;
83-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
84-
first [
85-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
86-
try (reflexivity);
87-
first [eassumption|apply _paco_foo_cons]); fail
88-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
89-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
83+
assert (XP: EP)
84+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
85+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
86+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
87+
paco_revert_hyp _paco_mark);
88+
unfold _paco_id; reflexivity);
9089
unfold EP in *; clear EP CIH; rename XP into CIH.
9190

9291
Ltac paco_post_simp CIH :=
@@ -1375,13 +1374,12 @@ Ltac paco_simp_hyp1 CIH :=
13751374
paco_convert_rev1; paco_revert_hyp _paco_mark;
13761375
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
13771376
clear TP;
1378-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
1379-
first [
1380-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1381-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
1382-
first [eassumption|apply _paco_foo_cons]); fail
1383-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1384-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
1377+
assert (XP: EP)
1378+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
1379+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
1380+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
1381+
paco_revert_hyp _paco_mark);
1382+
unfold _paco_id; reflexivity);
13851383
unfold EP in *; clear EP CIH; rename XP into CIH.
13861384

13871385
Ltac paco_post_simp1 CIH :=
@@ -1481,13 +1479,12 @@ Ltac paco_simp_hyp2 CIH :=
14811479
paco_convert_rev2; paco_revert_hyp _paco_mark;
14821480
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
14831481
clear TP;
1484-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
1485-
first [
1486-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1487-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
1488-
first [eassumption|apply _paco_foo_cons]); fail
1489-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1490-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
1482+
assert (XP: EP)
1483+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
1484+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
1485+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
1486+
paco_revert_hyp _paco_mark);
1487+
unfold _paco_id; reflexivity);
14911488
unfold EP in *; clear EP CIH; rename XP into CIH.
14921489

14931490
Ltac paco_post_simp2 CIH :=
@@ -1593,13 +1590,12 @@ Ltac paco_simp_hyp3 CIH :=
15931590
paco_convert_rev3; paco_revert_hyp _paco_mark;
15941591
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
15951592
clear TP;
1596-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
1597-
first [
1598-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1599-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
1600-
first [eassumption|apply _paco_foo_cons]); fail
1601-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1602-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
1593+
assert (XP: EP)
1594+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
1595+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
1596+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
1597+
paco_revert_hyp _paco_mark);
1598+
unfold _paco_id; reflexivity);
16031599
unfold EP in *; clear EP CIH; rename XP into CIH.
16041600

16051601
Ltac paco_post_simp3 CIH :=
@@ -1711,13 +1707,12 @@ Ltac paco_simp_hyp4 CIH :=
17111707
paco_convert_rev4; paco_revert_hyp _paco_mark;
17121708
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
17131709
clear TP;
1714-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
1715-
first [
1716-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1717-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
1718-
first [eassumption|apply _paco_foo_cons]); fail
1719-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1720-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
1710+
assert (XP: EP)
1711+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
1712+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
1713+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
1714+
paco_revert_hyp _paco_mark);
1715+
unfold _paco_id; reflexivity);
17211716
unfold EP in *; clear EP CIH; rename XP into CIH.
17221717

17231718
Ltac paco_post_simp4 CIH :=
@@ -1835,13 +1830,12 @@ Ltac paco_simp_hyp5 CIH :=
18351830
paco_convert_rev5; paco_revert_hyp _paco_mark;
18361831
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
18371832
clear TP;
1838-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
1839-
first [
1840-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1841-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
1842-
first [eassumption|apply _paco_foo_cons]); fail
1843-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1844-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
1833+
assert (XP: EP)
1834+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
1835+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
1836+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
1837+
paco_revert_hyp _paco_mark);
1838+
unfold _paco_id; reflexivity);
18451839
unfold EP in *; clear EP CIH; rename XP into CIH.
18461840

18471841
Ltac paco_post_simp5 CIH :=
@@ -1965,13 +1959,12 @@ Ltac paco_simp_hyp6 CIH :=
19651959
paco_convert_rev6; paco_revert_hyp _paco_mark;
19661960
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
19671961
clear TP;
1968-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
1969-
first [
1970-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1971-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
1972-
first [eassumption|apply _paco_foo_cons]); fail
1973-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
1974-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
1962+
assert (XP: EP)
1963+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
1964+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
1965+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
1966+
paco_revert_hyp _paco_mark);
1967+
unfold _paco_id; reflexivity);
19751968
unfold EP in *; clear EP CIH; rename XP into CIH.
19761969

19771970
Ltac paco_post_simp6 CIH :=
@@ -2101,13 +2094,12 @@ Ltac paco_simp_hyp7 CIH :=
21012094
paco_convert_rev7; paco_revert_hyp _paco_mark;
21022095
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
21032096
clear TP;
2104-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
2105-
first [
2106-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2107-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
2108-
first [eassumption|apply _paco_foo_cons]); fail
2109-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2110-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
2097+
assert (XP: EP)
2098+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
2099+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
2100+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
2101+
paco_revert_hyp _paco_mark);
2102+
unfold _paco_id; reflexivity);
21112103
unfold EP in *; clear EP CIH; rename XP into CIH.
21122104

21132105
Ltac paco_post_simp7 CIH :=
@@ -2243,13 +2235,12 @@ Ltac paco_simp_hyp8 CIH :=
22432235
paco_convert_rev8; paco_revert_hyp _paco_mark;
22442236
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
22452237
clear TP;
2246-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
2247-
first [
2248-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2249-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
2250-
first [eassumption|apply _paco_foo_cons]); fail
2251-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2252-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
2238+
assert (XP: EP)
2239+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
2240+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
2241+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
2242+
paco_revert_hyp _paco_mark);
2243+
unfold _paco_id; reflexivity);
22532244
unfold EP in *; clear EP CIH; rename XP into CIH.
22542245

22552246
Ltac paco_post_simp8 CIH :=
@@ -2391,13 +2382,12 @@ Ltac paco_simp_hyp9 CIH :=
23912382
paco_convert_rev9; paco_revert_hyp _paco_mark;
23922383
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
23932384
clear TP;
2394-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
2395-
first [
2396-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2397-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
2398-
first [eassumption|apply _paco_foo_cons]); fail
2399-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2400-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
2385+
assert (XP: EP)
2386+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
2387+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
2388+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
2389+
paco_revert_hyp _paco_mark);
2390+
unfold _paco_id; reflexivity);
24012391
unfold EP in *; clear EP CIH; rename XP into CIH.
24022392

24032393
Ltac paco_post_simp9 CIH :=
@@ -2545,13 +2535,12 @@ Ltac paco_simp_hyp10 CIH :=
25452535
paco_convert_rev10; paco_revert_hyp _paco_mark;
25462536
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
25472537
clear TP;
2548-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
2549-
first [
2550-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2551-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
2552-
first [eassumption|apply _paco_foo_cons]); fail
2553-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2554-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
2538+
assert (XP: EP)
2539+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
2540+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
2541+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
2542+
paco_revert_hyp _paco_mark);
2543+
unfold _paco_id; reflexivity);
25552544
unfold EP in *; clear EP CIH; rename XP into CIH.
25562545

25572546
Ltac paco_post_simp10 CIH :=
@@ -2705,13 +2694,12 @@ Ltac paco_simp_hyp11 CIH :=
27052694
paco_convert_rev11; paco_revert_hyp _paco_mark;
27062695
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
27072696
clear TP;
2708-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
2709-
first [
2710-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2711-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
2712-
first [eassumption|apply _paco_foo_cons]); fail
2713-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2714-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
2697+
assert (XP: EP)
2698+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
2699+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
2700+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
2701+
paco_revert_hyp _paco_mark);
2702+
unfold _paco_id; reflexivity);
27152703
unfold EP in *; clear EP CIH; rename XP into CIH.
27162704

27172705
Ltac paco_post_simp11 CIH :=
@@ -2871,13 +2859,12 @@ Ltac paco_simp_hyp12 CIH :=
28712859
paco_convert_rev12; paco_revert_hyp _paco_mark;
28722860
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
28732861
clear TP;
2874-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
2875-
first [
2876-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2877-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
2878-
first [eassumption|apply _paco_foo_cons]); fail
2879-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
2880-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
2862+
assert (XP: EP)
2863+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
2864+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
2865+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
2866+
paco_revert_hyp _paco_mark);
2867+
unfold _paco_id; reflexivity);
28812868
unfold EP in *; clear EP CIH; rename XP into CIH.
28822869

28832870
Ltac paco_post_simp12 CIH :=
@@ -3043,13 +3030,12 @@ Ltac paco_simp_hyp13 CIH :=
30433030
paco_convert_rev13; paco_revert_hyp _paco_mark;
30443031
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
30453032
clear TP;
3046-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
3047-
first [
3048-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
3049-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
3050-
first [eassumption|apply _paco_foo_cons]); fail
3051-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
3052-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
3033+
assert (XP: EP)
3034+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
3035+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
3036+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
3037+
paco_revert_hyp _paco_mark);
3038+
unfold _paco_id; reflexivity);
30533039
unfold EP in *; clear EP CIH; rename XP into CIH.
30543040

30553041
Ltac paco_post_simp13 CIH :=
@@ -3221,13 +3207,12 @@ Ltac paco_simp_hyp14 CIH :=
32213207
paco_convert_rev14; paco_revert_hyp _paco_mark;
32223208
let con := get_concl in set (TP:=con); revert EP; instantiate (1:= con); destruct FP);
32233209
clear TP;
3224-
assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;
3225-
first [
3226-
(repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
3227-
[..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];
3228-
first [eassumption|apply _paco_foo_cons]); fail
3229-
| (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;
3230-
(try unfold _paco_id); eauto using _paco_foo_cons)]);
3210+
assert (XP: EP)
3211+
by (unfold EP; clear -CIH; generalize _paco_mark_cons; repeat intro; apply CIH; paco_revert_hyp _paco_mark;
3212+
repeat (let x := fresh "x" in intro x; generalize _paco_mark_cons; intros;
3213+
first [exists x|split; [exists x; apply _paco_foo_cons|]];
3214+
paco_revert_hyp _paco_mark);
3215+
unfold _paco_id; reflexivity);
32313216
unfold EP in *; clear EP CIH; rename XP into CIH.
32323217

32333218
Ltac paco_post_simp14 CIH :=

0 commit comments

Comments
 (0)