From 5a38bcf22fdf8ae46274282f092ba2f59df8281e Mon Sep 17 00:00:00 2001 From: Minki Cho Date: Fri, 19 Mar 2021 03:18:53 +0900 Subject: [PATCH] Fix pcofix bug #41 --- metasrc/pacotac_internal.py | 2 +- src/pacotac_internal.v | 28 ++++++++++++++-------------- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/metasrc/pacotac_internal.py b/metasrc/pacotac_internal.py index 81a7ec6..2f82188 100755 --- a/metasrc/pacotac_internal.py +++ b/metasrc/pacotac_internal.py @@ -309,7 +309,7 @@ print (' assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH;') print (' first [') print (' (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;') - print (' try (reflexivity);') + print (' [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end];') print (' first [eassumption|apply _paco_foo_cons]); fail') print (' | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end;') print (' (try unfold _paco_id); eauto using _paco_foo_cons)]);') diff --git a/src/pacotac_internal.v b/src/pacotac_internal.v index aab1cc1..33ccb6f 100644 --- a/src/pacotac_internal.v +++ b/src/pacotac_internal.v @@ -1377,7 +1377,7 @@ Ltac paco_simp_hyp1 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -1483,7 +1483,7 @@ Ltac paco_simp_hyp2 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -1595,7 +1595,7 @@ Ltac paco_simp_hyp3 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -1713,7 +1713,7 @@ Ltac paco_simp_hyp4 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -1837,7 +1837,7 @@ Ltac paco_simp_hyp5 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -1967,7 +1967,7 @@ Ltac paco_simp_hyp6 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -2103,7 +2103,7 @@ Ltac paco_simp_hyp7 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -2245,7 +2245,7 @@ Ltac paco_simp_hyp8 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -2393,7 +2393,7 @@ Ltac paco_simp_hyp9 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -2547,7 +2547,7 @@ Ltac paco_simp_hyp10 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -2707,7 +2707,7 @@ Ltac paco_simp_hyp11 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -2873,7 +2873,7 @@ Ltac paco_simp_hyp12 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -3045,7 +3045,7 @@ Ltac paco_simp_hyp13 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]); @@ -3223,7 +3223,7 @@ Ltac paco_simp_hyp14 CIH := assert (XP: EP) by (unfold EP; clear -CIH; repeat intro; apply CIH; first [ (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; - try (reflexivity); + [..|match goal with [|-_paco_id (?a = ?b)] => unfold _paco_id; reflexivity end]; first [eassumption|apply _paco_foo_cons]); fail | (repeat match goal with | [ |- @ex _ _ ] => eexists | [ |- _ /\ _ ] => split end; (try unfold _paco_id); eauto using _paco_foo_cons)]);