From 0019d8634dd3ff26d2b32ce38e1df1458a0f1c36 Mon Sep 17 00:00:00 2001 From: Garo Brik Date: Thu, 8 Dec 2016 11:38:40 -0500 Subject: [PATCH] Separate out tactics into a new file, add some lemmas --- lemmas.v | 12 ++---------- tactics.v | 31 +++++++++++++++++++++++++++++++ 2 files changed, 33 insertions(+), 10 deletions(-) create mode 100644 tactics.v diff --git a/lemmas.v b/lemmas.v index 6f74162..3e891ce 100644 --- a/lemmas.v +++ b/lemmas.v @@ -3,15 +3,7 @@ Require Export Coq.Lists.List. Require Export Arith.EqNat. Require Export Program.Equality. Require Export Coq.Logic.ProofIrrelevance. - -Ltac inverts n := - match n with - | S ?n' => match goal with - | [ H : _ |- _ ] => try (inversion H; subst; inverts n') - | _ => idtac - end - | _ => idtac - end. +Require Export tactics. Module E. Require Coq.Sets.Ensembles. @@ -542,4 +534,4 @@ Proof. Qed. Hint Resolve In_set_from_list_In_list. -Hint Resolve nth_error_In. \ No newline at end of file +Hint Resolve nth_error_In. Hint Resolve in_map_iff. \ No newline at end of file diff --git a/tactics.v b/tactics.v new file mode 100644 index 0000000..aa30675 --- /dev/null +++ b/tactics.v @@ -0,0 +1,31 @@ +Ltac decomp := + repeat match goal with + | [ H : _ /\ _ |- _ ] => destruct H + | [ H : exists _, _ |- _ ] => destruct H + end. + +Ltac inverts n := + match n with + | S ?n' => match goal with + | [ H : _ |- _ ] => try (inversion H; subst; inverts n') + | _ => idtac + end + | _ => idtac + end. + +Ltac split_rec n := + match n with + | S ?n' => match goal with + |[ |- exists _, _ ] => eexists; split_rec n' + |[ |- _ /\ _] => split; split_rec n' + | _ => idtac + end + | 0 => idtac + end. + +Ltac subst_some := + repeat match goal with + | [ G : ?x = Some ?y, + H : ?x = Some ?z |- _ ] => rewrite G in H + | [ H : Some ?x = Some ?y |- _ ] => inversion H; subst; clear H + end. \ No newline at end of file