From a47b49b11d17add5ca1ea5e650d2f344219b4f7e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 5 Feb 2016 15:24:42 -0500
Subject: Update build process to use COQPATH & _CoqProject

Removed all of the files not built by default; they can be resurrected from git
history.  _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile.  COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).
---
 coqprime/Coqprime/Tactic.v | 84 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 coqprime/Coqprime/Tactic.v

(limited to 'coqprime/Coqprime/Tactic.v')

diff --git a/coqprime/Coqprime/Tactic.v b/coqprime/Coqprime/Tactic.v
new file mode 100644
index 000000000..93a244149
--- /dev/null
+++ b/coqprime/Coqprime/Tactic.v
@@ -0,0 +1,84 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+
+(**********************************************************************
+       Tactic.v                                                                                    
+          Useful tactics                                                                       
+ **********************************************************************)
+
+(**************************************
+  A simple tactic to end a proof 
+**************************************)
+Ltac  finish := intros; auto; trivial; discriminate.
+
+
+(**************************************
+ A tactic for proof by contradiction
+     with contradict H 
+         H: ~A |-   B      gives           |-   A
+         H: ~A |- ~ B     gives  H: B |-   A
+         H:   A |-   B      gives           |- ~ A
+         H:   A |-   B      gives           |- ~ A
+         H:   A |- ~ B     gives  H: A |- ~ A
+**************************************)
+
+Ltac  contradict name := 
+     let term := type of name in (
+     match term with 
+       (~_) => 
+          match goal with 
+            |- ~ _  => let x := fresh in
+                     (intros x; case name; 
+                      generalize x; clear x name;
+                      intro name)
+          | |- _    => case name; clear name
+          end
+     | _ => 
+          match goal with 
+            |- ~ _  => let x := fresh in
+                    (intros x;  absurd term;
+                       [idtac | exact name]; generalize x; clear x name;
+                       intros name)
+          | |- _    => generalize name; absurd term;
+                       [idtac | exact name]; clear name
+          end
+     end).
+
+
+(**************************************
+  A tactic to do case analysis keeping the equality
+**************************************)
+
+Ltac case_eq name :=
+  generalize (refl_equal name); pattern name at -1 in |- *; case name.
+
+
+(**************************************
+ A tactic to use f_equal? theorems 
+**************************************)
+
+Ltac eq_tac := 
+ match goal with
+      |-  (?g _ = ?g _) => apply f_equal with (f := g)
+ |     |-  (?g ?X _ = ?g  ?X _) => apply f_equal with (f := g X)
+ |     |-  (?g _ _ = ?g  _ _) => apply f_equal2 with (f := g)
+ |     |-  (?g ?X ?Y _ = ?g ?X ?Y _) => apply f_equal with (f := g X Y)
+ |     |-  (?g ?X _ _ = ?g ?X _ _) => apply f_equal2 with (f := g X)
+ |     |-  (?g _ _ _ = ?g _ _ _) => apply f_equal3 with (f := g)
+ |     |-  (?g ?X ?Y ?Z _ = ?g ?X ?Y ?Z _) => apply f_equal with (f := g X Y Z)
+ |     |-  (?g ?X ?Y _ _ = ?g ?X ?Y _ _) => apply f_equal2 with (f := g X Y)
+ |     |-  (?g ?X _ _ _ = ?g ?X _ _ _) => apply f_equal3 with (f := g X)
+ |     |-  (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g)
+ end.
+
+(************************************** 
+ A stupid tactic that tries auto also after applying sym_equal
+**************************************)
+
+Ltac sauto := (intros; apply sym_equal; auto; fail) || auto.
-- 
cgit v1.2.3