Skip to content
Browse files

Imported from rippling-0.1.zip.

This is the (reorganized) import of the code available from

http://homepages.inf.ed.ac.uk/s0091720/
  • Loading branch information...
0 parents commit 5e52f320a74cd8754266d9fcdaba7cfc53eaf08d Sean Wilson committed with Apr 9, 2010
Showing with 4,256 additions and 0 deletions.
  1. +46 −0 README
  2. +40 −0 coreless-auto.patch
  3. +644 −0 demo.v
  4. +176 −0 discover.v
  5. +129 −0 general_tactics.v
  6. +113 −0 rippling.v
  7. +2,729 −0 rippling_plugin.ml
  8. +295 −0 tools.v
  9. +84 −0 unit_testing.v
46 README
@@ -0,0 +1,46 @@
+Inductive proof automation for Coq, version 0.1
+by Sean Wilson
+
+This package contains an inductive proof automation plugin for Coq. This automation
+includes a rippling tactic, generalisation heuristics and a counterexample finder tool.
+This file explains how to compile the code and run the demo file (see theory/demo.v),
+which includes many examples of theorems that can be automated. See here for documentation
+about how the automation works:
+http://homepages.inf.ed.ac.uk/s0091720/
+
+For installation, you will need SVN and OCaml installed, as well as several OCaml libraries
+you need for compiling Coq, such as liblablgtk2-ocaml, liblablgtk2-ocaml-dev and campl5.
+If there are any compilation problems, consult documentation on how to compile the
+regular Coq source code.
+
+To get everything running, you need to download the Coq source code, copy the plugin
+into the Coq source code folder and then compile Coq. This can be done with the following
+commands:
+
+- First, open the "Makefile" file in a text editor and alter the variables at the top if
+ you are unhappy with any of the installation paths.
+
+- To checkout a version of the Coq source code that is known work with this plugin run:
+ make checkoutcoq
+
+- To copy the plugin into the Coq source code directory run:
+ make copy
+
+- To configure Coq for compiling run:
+ make configurecoq
+
+- Check the output from the last command says everything is fine and Coq IDE will be built.
+
+- To compile Coq with the plugin run:
+ make buildcoq
+
+ This can take 30 minutes or so.
+
+- To run the demo:
+ make demo
+
+These tactics are still in development. The code and the installation process should
+hopefully be simplified in the future.
+
+Note that this code has only been tested under Linux so far.
+
40 coreless-auto.patch
@@ -0,0 +1,40 @@
+diff --git a/tactics/auto.ml b/tactics/auto.ml
+index d03c527..ecfa77d 100644
+--- a/tactics/auto.ml
++++ b/tactics/auto.ml
+@@ -1127,7 +1127,7 @@ let search = search_gen 0
+
+ let default_search_depth = ref 5
+
+-let delta_auto mod_delta n lems dbnames gl =
++let delta_auto ?(use_core_db=true) mod_delta n lems dbnames gl =
+ let db_list =
+ List.map
+ (fun x ->
+@@ -1135,11 +1135,11 @@ let delta_auto mod_delta n lems dbnames gl =
+ searchtable_map x
+ with Not_found ->
+ error_no_such_hint_database x)
+- ("core"::dbnames)
++ (if use_core_db then "core"::dbnames else dbnames)
+ in
+ tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
+
+-let auto = delta_auto false
++let auto ?(use_core_db=true) = delta_auto ~use_core_db false
+
+ let new_auto = delta_auto true
+
+diff --git a/tactics/auto.mli b/tactics/auto.mli
+index cd8808b..54131aa 100644
+--- a/tactics/auto.mli
++++ b/tactics/auto.mli
+@@ -192,7 +192,7 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
+
+ (** The Auto tactic *)
+
+-val auto : int -> open_constr list -> hint_db_name list -> tactic
++val auto : ?use_core_db:bool -> int -> open_constr list -> hint_db_name list -> tactic
+
+ (** Auto with more delta. *)
+
644 demo.v
@@ -0,0 +1,644 @@
+(*
+
+This demo script demonstrates new tactics for inductive proof automation for Coq. The
+automation can be used to discharge goals that involve inductively defined data types
+and recursively defined functions. This includes proofs that involve case splitting and
+multiple inductive hypotheses. We give examples of proofs involving trees, lists,
+higher-order functions and Peano arithmatic.
+
+The main features of the automation are as follows:
+
+- A tactic that implements "rippling". Rippling is used to control the use of rewrite
+ rules in step case goals of inductive proofs. See the following FAQ for a
+ general overview of rippling:
+ http://dream.dai.ed.ac.uk/projects/ripple-faq.html
+
+- Automated generalisation heuristics.
+
+- Techniques for caching lemmas found during proof search and reusing these
+ lemmas in future proof attempts.
+
+- A QuickCheck-like counterexample finder.
+
+More documentation be found on:
+http://homepages.inf.ed.ac.uk/s0091720/
+
+The automation is composed of the following modular tactics:
+
+- simp: Attempts to simplify the current goal. Briefly, this is done by normalising
+ the goal, using and discarding any equational assumptions, performing case splits
+ when there are subterms of the form "match x..." and exhaustively rewriting with
+ a set of rules chosen simplification.
+
+- triv: Tries to prove the current goal outright using "tauto" and cached lemmas.
+
+- ind0/ind1/ind2/...: Begins an inductive proof on the nth variable in the conclusion.
+ Universal introduction and reintroduction is performed prior to induction so as to
+ strengthen the inductive hypotheses.
+
+- ripple: Identifies assumptions that share syntactic similiarities with the conclusion
+ and succeeds when the conclusion can be modified so that these assumptions can be used
+ to rewrite the conclusion.
+
+- gen: Attempts to generalise the current goal.
+
+- qc: Succeeds when it cannot find a counterexample to the current goal.
+
+The top-level tactic which makes use of these tactics is called "d" (we really need
+a better name for this!). The ripple', simp', triv' and d' tactics are versions
+of the above tactics that do not use cached lemmas and only rely on basic definitions.
+
+*)
+
+(********************************************************************************)
+(* Overview *)
+(********************************************************************************)
+
+(*
+First, we use an example proof to give an overview of the general search strategy
+used by the top-level proof automation. This proof only involves the use of basic
+definitions, where the automation is able to conjecture the needed lemmas.
+
+Note: Open this script in CoqIDE launched from a console. The console will contain
+useful proof search feedback.
+*)
+
+Load "tools.v".
+Require Import List.
+
+(*
+Before using the "ripple" tactic, we must call the "AddWaveRule" command on each
+function definition we are going to use in our script. This command generates basic
+equations from function definitions for use as rewrite rules by "ripple" tactic.
+*)
+AddWaveRule app.
+AddWaveRule rev.
+
+Goal forall (A:Type) (x y:list A), rev (x ++ y) = rev y ++ rev x.
+
+(* The automation first attempts a trivial proof by calling "simp" and "triv" in
+sequence. No progress is made here. *)
+simp'; triv'.
+
+(* If this fails, an attempt is made to generalise the goal. Backtracking to the
+point before generalising the goal is allowed. No generalisation is found here. *)
+try gen.
+
+(* Induction is then performed on some variable in the goal. If the inductive proof
+fails, induction is attempted on another variable until all choices are exhausted. *)
+ind2.
+
+ (* Step cases are attempted first *)
+ Focus 2.
+ (* When a goal contains assumptions that have syntactic similarities to the conclusion,
+ rippling is used is rewrite the conclusion so that these assumptions can be used to
+ rewrite the conclusion. Rippling must succeed to continue.
+
+ Rippling succeeds in this case. See the console output to see how rippling moves
+ the terms in the conclusion that are different to the inductive hypothesis
+ (coloured green) towards the top of the term tree of the conclusion until the
+ inductive hypothesis can be used to rewrite the conclusion *)
+ ripple'.
+
+ (* The strategy above is followed on each of the remaining goals to finish the proof *)
+ simp'; triv'.
+ (* This time, two common subterms ("rev y" and "rev l") are identified and generalised. *)
+ gen.
+
+ ind0.
+ (* Step case *)
+ Focus 2.
+ ripple'.
+ simp'; triv'.
+
+ (* Base case *)
+ Focus 2.
+ simp'; triv'.
+
+ (* Base case *)
+ simp'; triv'.
+ gen.
+ ind0.
+ Focus 2.
+ (* Step case *)
+ ripple'.
+ simp'; triv'.
+
+ (* Base case *)
+ simp'; triv'.
+Qed.
+
+(*
+Here, we prove the same goal again but with the top-level proof automation tactic.
+Look at the standard output from your console after the tactic call to see the
+trace of the proof search, where the indentation represents search depth.
+*)
+Goal forall (A:Type) (x y:list A), rev (x ++ y) = rev y ++ rev x.
+d'.
+Qed.
+
+(* We now give several examples of proofs that can be fully automated from only
+basic definitions *)
+
+(********************************************************************************)
+(* Arithmatic theorem examples *)
+(********************************************************************************)
+
+Fixpoint pow (r:nat) (n:nat) {struct n} : nat :=
+ match n with
+ | O => 1
+ | S n => r * pow r n
+ end.
+Infix "^" := pow : type_scope.
+
+AddWaveRule plus.
+AddWaveRule pow.
+AddWaveRule mult.
+
+Goal forall x y, x + y = y + x.
+d'.
+Qed.
+
+Goal forall x y, x * y = y * x.
+d'.
+Qed.
+
+Goal forall x y z, x * (y + z) = x * y + x * z.
+d'.
+Qed.
+
+Goal forall x n m, x ^ (n + m) = x ^ n * x ^ m.
+d'.
+Qed.
+
+(********************************************************************************)
+(* List theorem examples *)
+(********************************************************************************)
+
+AddWaveRule length.
+
+Goal forall (A:Type) (x y z:list A), (x ++ y) ++ z = x ++ y ++ z.
+d'.
+Qed.
+
+Goal forall (A:Type) (a b:list A), length (a ++ b) = length a + length b.
+d'.
+Qed.
+
+Goal forall (A:Type) (a:list A), length (rev a) = length a.
+d'.
+Qed.
+
+Goal forall (A:Type) (a:list A), rev (rev a) = a.
+d'.
+Qed.
+
+Goal forall (A:Type) (x y:list A), rev (x ++ y) = rev y ++ rev x.
+d'.
+Qed.
+
+(********************************************************************************)
+(* Higher-order theorem examples *)
+(********************************************************************************)
+
+Fixpoint sum (a:list nat) : nat :=
+ match a with
+ | [] => 0
+ | h :: t => h + sum t
+ end.
+
+AddWaveRule sum.
+AddWaveRule seq.
+AddWaveRule fold_left.
+AddWaveRule map.
+
+Goal forall (a:list nat), fold_left plus a 0 = sum a.
+d'.
+Qed.
+
+Goal forall (A B:Type) (f:A -> B) (x y:list A), map f (x ++ y) = map f x ++ map f y.
+d'.
+Qed.
+
+Goal forall (A B:Type) (f:A -> B) (x y:list A),
+ rev (map f (x ++ y)) = rev (map f y) ++ rev (map f x).
+d'.
+Qed.
+
+Goal forall len start, map S (seq start len) = seq (S start) len.
+d'.
+Qed.
+
+(********************************************************************************)
+(* Binary tree theorem examples *)
+(********************************************************************************)
+
+Section BTree.
+Variable A : Type.
+
+Inductive btree : Type :=
+| empty : btree
+| node : A -> btree -> btree -> btree.
+End BTree.
+
+Implicit Arguments empty [A].
+Notation "'leaf' x" := (node x (empty) (empty)) (at level 20).
+
+Section BTreeFunctions.
+Variable A : Type.
+
+Fixpoint num_nodes (a : btree A) : nat :=
+ match a with
+ | empty => 0
+ | node v l r => S ((num_nodes l) + (num_nodes r))
+ end.
+
+Fixpoint mirror (a : btree A) : btree A :=
+ match a with
+ | empty => empty
+ | node v l r => node v (mirror r) (mirror l)
+ end.
+
+Fixpoint inorder (a:btree A) : list A :=
+ match a with
+ | empty => []
+ | node v l r => (inorder l) ++ [v] ++ (inorder r)
+ end.
+
+Fixpoint postorder (a : btree A) : list A :=
+ match a with
+ | empty => []
+ | node v l r => (postorder l) ++ (postorder r) ++ [v]
+ end.
+
+Fixpoint preorder (a : btree A) : list A :=
+ match a with
+ | empty => []
+ | node v l r => v::((preorder l) ++ (preorder r))
+ end.
+Require Import Arith.Max.
+
+Fixpoint height (a : btree A) : nat :=
+ match a with
+ | empty => 0
+ | node v l r => 1 + max (height l) (height r)
+ end.
+End BTreeFunctions.
+
+AddWaveRule num_nodes.
+AddWaveRule mirror.
+AddWaveRule postorder.
+AddWaveRule preorder.
+AddWaveRule inorder.
+AddWaveRule height.
+AddWaveRule max.
+
+(* In these proofs, the "ripple" tactic must consider two inductive hypotheses
+in step cases goals *)
+
+Goal forall (A:Type)(a : btree A), mirror (mirror a) = a.
+d'.
+Qed.
+
+Goal forall (A:Type)(a : btree A), height (mirror a) = height a.
+d'.
+Qed.
+
+Goal forall (A:Type)(a : btree A), postorder (mirror a) = rev (preorder a).
+d'.
+Qed.
+
+Goal forall (A:Type)(a : btree A), length (inorder a) = num_nodes a.
+d'.
+Qed.
+
+(********************************************************************************)
+(* Case splitting examples *)
+(********************************************************************************)
+
+(* In these examples, case splits are required during step case proofs *)
+
+Variable A:Set.
+Variable leA : relation A.
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {x = y} + {x <> y}.
+Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+
+AddWaveRule count_occ.
+Notation l_perm x y :=
+ (forall n, count_occ eqA_dec x n = count_occ eqA_dec y n) (only parsing).
+
+Goal forall x y, max x y = max y x.
+d'.
+Qed.
+
+Goal forall x y z, max x (max y z) = max (max x y) z.
+d'.
+Qed.
+
+Goal forall x y, l_perm (x ++ y) (y ++ x).
+d'.
+Qed.
+
+Goal forall x, l_perm (rev x) x.
+d'.
+Qed.
+
+(* Properties of insertion sort *)
+
+Fixpoint insert (x:A) (a:list A) : list A :=
+ match a with
+ | nil => [x]
+ | h::t => if leA_dec x h then x::a else h::(insert x t)
+ end.
+
+Fixpoint insertion_sort (a:list A) : list A :=
+ match a with
+ | nil => []
+ | h::t => insert h (insertion_sort t)
+ end.
+
+AddWaveRule insert.
+AddWaveRule insertion_sort.
+
+Goal forall a, length (insertion_sort a) = length a.
+d'.
+Qed.
+
+Goal forall a, l_perm (insertion_sort a) a.
+d'.
+Qed.
+
+(*
+
+Limitations:
+
+- The proof automation does not offer much support for goals involving inductive
+predicates (e.g. "<", "In") at the moment.
+
+- The conclusion of the goal must generally be an equation. We hope to support
+user-defined relations in the future.
+
+- We do not currently support proofs that require piecewise fertilisation. This
+is needed when the inductive hypothesis contains an implication, such as when
+induction is performed on "x" in the following goal:
+
+forall x y z, list perm (x ++ y) z -> length x < S (length z)
+
+*)
+
+(********************************************************************************)
+(* Lemma caching *)
+(********************************************************************************)
+
+(* All inductive proofs are cached for reuse in later proof attempts. A single proof
+can involve several inductive proofs. We find cached lemmas are typically general
+and reusable. For example:
+*)
+
+Goal forall x y, x * y = y * x.
+d.
+Qed.
+
+(* Lemmas cached:
+forall x y, x * y = y * x
+forall x y z, x + (y + z) = y + (x + z))
+forall x y, x * S y = x + x * y
+forall x, x * 0 = 0
+*)
+
+Goal forall (A:Type) (x y:list A), rev (x ++ y) = rev y ++ rev x.
+d.
+Qed.
+
+(*
+Lemmas cached:
+forall x y, rev (x ++ y) = rev y ++ rev x
+forall (A::Type) (x y z:list A), (x ++ y) ++ z = x ++ y ++ z
+forall (A:Type) (x:list A0), x = x ++ []
+forall (A:Type) (x y:list A0), rev (x ++ y) = rev y ++ rev x
+*)
+
+(*
+All cached lemmas are inserted into the "cache" database for use by the "triv" tactic.
+*)
+Print HintDb cache.
+
+(*
+Most cached lemmas are inserted into the "ripple_cached" database for use by the
+"ripple" tactic. We do not add rules that only serve to make rippling less efficient:
+the rule "X = Y" is not added as a left-to-right rewrite rule when X is a ground
+term or when Y can be decorated with terms so that Y is the same term as X.
+*)
+
+PrintHints ripple_cached.
+
+(*
+The "ripple_basic" database contains only the rules added by "AddWaveRule" and is
+used by the "ripple" tatic. This is for when we only want to make use of basic
+definitions when searching for proofs.
+*)
+PrintHints ripple_basic.
+
+(*
+Rewrite rules that can be used for simplification are inserted into the "simp"
+database for use by the "simp" tactic. When caching proofs, the equation X = Y
+will be automatically added as a left-to-right simplification rule when either
+of the following are true:
+
+1) Y is a ground term e.g. (forall x * 0 = 0), (forall x, min x 0 = 0)
+
+2) terms can be added to Y such that X is the same term as Y
+ e.g. (forall x, x ++ [] = x), (forall x, rev (rev x)),
+ (forall f a, length (map f a) = length a)
+
+We find this heuristic is good at identifying obvious simplification rules.
+*)
+PrintHints simp.
+
+(*
+The reuse of cached lemmas can increase proof converage and make proof search
+more effecient. For example:
+*)
+
+Goal forall (A:Type) (x y:list A), rev ((rev x) ++ y) = rev y ++ x.
+(* A proof without using cached lemmas fails here *)
+try d'.
+
+(* Cached lemmas are helpful when proving this goal by induction on "x" *)
+ind2.
+ (* Step case *)
+ Focus 2.
+ (* Rippling without cached lemmas fails here *)
+ try ripple'.
+ (* Rippling with the cached lemmas from above succeeds, with the
+ use of the lemma for associativity of ++. *)
+ ripple.
+ reflexivity.
+
+ (* The base is proven by "triv" as a more general version of this goal has already
+ been proven *)
+ simp'.
+ triv.
+Qed.
+
+(********************************************************************************)
+(* Automated generalisation examples *)
+(********************************************************************************)
+
+(* Generalising the common subterms "rev x" and "rev y" *)
+Goal forall (A:Type) (x y:list A),
+ length (rev x ++ rev y) = length (rev x) + length (rev y).
+intros; gen.
+d'.
+Qed.
+
+(* Generalising apart "x" *)
+Goal forall x y, (x * x) * y = x * (y * x).
+intros; gen.
+d.
+Qed.
+
+(* Generalisation apart "x" *)
+Goal forall (A:Type) (x:list A), length (x ++ x) = length x + length x.
+intros; gen.
+d'.
+Qed.
+
+(********************************************************************************)
+(* Testing tool *)
+(********************************************************************************)
+
+(*
+
+The testing tool searches for a counterexample to the current Coq goal by:
+
+- (Generate) Simply typed "Set" variables are instantiated with randomly
+ generated terms.
+
+- (Test) A counterexample is found when all Prop assumptions are provable and the
+ conclusion is not provable. When checking this, we only support propositions that
+ make use of "=", "<>", "/\", "\/", "<", "<=", ">" and ">=", and propositions cannot
+ contain quantifiers.
+
+The proof automation makes use of this tool to identify overgeneralisations. The
+testing tool is also useful in manual proofs.
+
+Uncomment the "try" in each example below to see the counterexample found.
+When a counterexample is found, an evaluation trace is shown.
+*)
+
+(* A non-theorem *)
+Goal forall x, (x - 1) + 1 = x.
+try qc.
+(*
+*** COUNTEREXAMPLE FOUND ***
+
+Variable instantiations:
+x := 0
+
+Instantiated and simplified conclusion showing the contradiction:
+(x - 1 + 1 = x)
+(0 - 1 + 1 = 0)
+(0 + 1 = 0)
+(1 = 0)
+*)
+Admitted.
+
+(* The counterexample above indicates a missing side-condition. The testing
+tool can be used to check we have now written a theorem statement. *)
+Goal forall x, x <> 0 -> (x - 1) + 1 = x.
+qc.
+intuition.
+Qed.
+
+Goal True.
+(* Tells the testing tool to replace (A:Type) in goals with (A:nat) when testing *)
+ReplaceInTests T nat.
+Admitted.
+
+Goal forall (T:Type) (x y:list T), rev (x ++ y) = rev x ++ rev y.
+try qc.
+(*
+*** COUNTEREXAMPLE FOUND ***
+
+Variable instantiations:
+y := [0; 0]
+x := [1]
+
+Instantiated and simplified conclusion showing the contradiction:
+(rev (x ++ y) = rev x ++ rev y)
+(rev ([1] ++ [0; 0]) = rev [1] ++ rev [0; 0])
+(rev [1; 0; 0] = [1] ++ [0; 0])
+([0; 0; 1] = [1; 0; 0])
+*)
+Admitted.
+
+Goal forall (T:Type) (x y:list T), rev (x ++ y) = rev y ++ rev x.
+qc.
+d'.
+Qed.
+
+Goal forall (T:Type)(a : btree T), postorder (mirror a) = rev (postorder a).
+try qc.
+(*
+*** COUNTEREXAMPLE FOUND ***
+
+Variable instantiations:
+a := (node 1 (leaf 0) (leaf 0))
+
+Instantiated and simplified conclusion showing the contradiction:
+(postorder (mirror a) = rev (postorder a))
+(postorder (mirror (node 1 (leaf 0) (leaf 0))) =
+ rev (postorder (node 1 (leaf 0) (leaf 0))))
+(postorder (node 1 (leaf 0) (leaf 0)) = rev [0; 0; 1])
+([0; 0; 1] = [1; 0; 0])
+*)
+Admitted.
+
+Goal forall (T:Type)(a : btree T), postorder (mirror a) = rev (preorder a).
+qc.
+d.
+Qed.
+
+Goal forall (S T:Type) (f:S -> T) (x y:list S),
+ rev (map f (x ++ y)) = rev (map f x) ++ rev (map f y).
+ReplaceInTests S nat.
+ReplaceInTests T nat.
+(* Randomly instantiate variables with type (nat -> nat) to "S" or "pred" *)
+Generator (nat -> nat) [S; pred].
+try qc.
+(*
+*** COUNTEREXAMPLE FOUND ***
+
+Variable instantiations:
+y := [1]
+x := [0]
+f := S
+
+Instantiated and simplified conclusion showing the contradiction:
+(rev (map f (x ++ y)) = rev (map f x) ++ rev (map f y))
+(rev (map S ([0] ++ [1])) = rev (map S [0]) ++ rev (map S [1]))
+(rev (map S [0; 1]) = rev [1] ++ rev [2])
+(rev [1; 2] = [1] ++ [2])
+([2; 1] = [1; 2])
+*)
+Admitted.
+
+(*
+Limitations:
+
+- Term generation only works for simply typed inductive data types.
+
+- Tests that involve large terms can crash Coq. For example, power and factorial
+functions can generate large terms during testing.
+
+- User-defined inductive predicates are not supported. For example, we cannot test
+if "In 0 [0]" is provable. One workaround is to define a function that is equilavent
+to the inductive predicate you want to use and use "setoid_rewrite" to rewrite the
+latter to the former before testing.
+
+- There are no support yet for writing custom term generators. This can
+make it difficult to find counterexamples when the goal assumptions express
+conditions that are hard to satisfy with random variable instantiations.
+*)
176 discover.v
@@ -0,0 +1,176 @@
+(* Some testing on auto discovering obvious lemmas for operators from templates *)
+
+Require Import Omega.
+
+Ltac solver2 := admit. (* a very reliable solver! *)
+Ltac solver := d.
+
+(* Tries to prove and cache a conjecture using a tactic *)
+Ltac discover3 conjecture prover :=
+idtac "Trying to prove" conjecture;
+assert conjecture; clear;
+[
+ let lemma_name := fresh "discovered" in
+ (* Trick: New goal created after conjectured subgoal. If the proof progresses
+ to proving the second subgoal, we know the conjecture has been proven *)
+ cut True;
+ [
+ intro; clear;
+ abstract prover lemma_name
+ |
+ let t := type of lemma_name in
+ idtac "discovered " lemma_name " : "t;
+ constructor
+ ]
+|
+ idtac].
+
+Ltac discover2 conjecture :=
+ let prover := (intros; solver) in
+try (if assert conjecture; clear;
+qc_no_trace
+then
+fail
+else
+ (*idtac "discover: Counterexample found! ";*)
+ fail 2);
+ idtac "discover: Trying to prove ";
+ hint' conjecture prover;
+ idtac "discover: *********************************** Proven! " conjecture.
+
+Ltac get_base t :=
+match t with
+ nat => 0
+| list _ => nil
+end.
+
+(*(* need base case values *)
+
+(* identity element *)
+try discover2 (forall x, op x b = x);
+try discover2 (forall y, op b y = y);
+
+(* absorbing element *)
+try discover2 (forall x, op x b = b);
+try discover2 (forall y, op b y = b);
+
+try discover2 (op b = b);
+*)
+
+Ltac discover f :=
+(* f = arity 1 *)
+(* involution *)
+try discover2 (forall x, f (f x) = x);
+(* injectivity *)
+(*try discover2 (forall x y, f x = f y <-> x = y);*)
+(* TODO: need to do a check that f is not being used in curried form match f x => *)
+
+(* f = arity 2 *)
+(* commutativity *)
+try discover2 (forall x y, f x y = f y x);
+(* associativity *)
+try discover2 (forall x y z, f (f x y) z = f x (f y z))
+
+(* associativity varients *)
+(*try discover2 (forall x y z, f (f x y) z = f x (f z y));
+try discover2 (forall x y z, f (f x y) z = f y (f x z));
+try discover2 (forall x y z, f (f x y) z = f y (f z x));
+try discover2 (forall x y z, f (f x y) z = f z (f x y));
+try discover2 (forall x y z, f (f x y) z = f z (f y x));
+try discover2 (forall x y z, f (f x y) z = f (f y x) z)*)
+.
+
+Ltac discoverfg f g :=
+(* f = arity 2 *)
+(* g = arity 2 *)
+try discover2 (forall x y z, f x (g y z) = g (f x y) (f x z));
+try discover2 (forall x y z, f (g y z) x = g (f y x) (f z x));
+
+(* f = arity 2 *)
+(* g = arity 1 *)
+try discover2 (forall x y, f x (g y) = f (g x) (y));
+try discover2 (forall x y, f x (g y) = g (f x y));
+try discover2 (forall x y, g (f x y) = f (g x) (g y));
+try discover2 (forall x, g (f x) = g (x))
+.
+
+Ltac discoverfgh' f g h :=
+idtac "discover" f g h;
+(* f = arity 2 *)
+(* g = arity 2 *)
+try discover2 (forall x y z, f (g x y) = h (f x) (f y)).
+
+Ltac discoverfgh f g h :=
+discoverfgh' f g h;
+discoverfgh' f h g;
+discoverfgh' g f h;
+discoverfgh' g h f;
+discoverfgh' h f g;
+discoverfgh' h g f.
+
+Ltac discoverb f g :=
+try discoverfg f g;
+try discoverfg g f.
+
+Ltac discover_with_1 pairs :=
+(*idtac "discover: pair" pairs;*)
+ match pairs with
+ | [] => idtac
+ | (?f=_)::?t => try discover f; discover_with_1 t
+ end.
+
+Ltac discover_with_pair2 pairs :=
+(*idtac "discover: pair" pairs;*)
+ match pairs with
+ | [] => idtac
+ | (?h=_, (?f=_, ?g=_))::?t =>
+ try discoverfgh f g h; discover_with_pair2 t
+ end.
+
+Ltac discover_with_pair pairs :=
+(*idtac "discover: pair" pairs;*)
+ match pairs with
+ | [] => idtac
+ | (?f=_, ?g=_)::?t => try discoverb f g; discover_with_pair t
+ end.
+
+Ltac discoverL functions :=
+idtac "discover:";
+idtac "discover: starting discovery process";
+ let pairs := eval simpl in (list_prod functions functions) in
+ discover_with_pair pairs;
+ let pairs2 := eval simpl in (list_prod functions pairs) in
+ discover_with_pair2 pairs2;
+ discover_with_1 functions.
+Ltac idt d := idtac d;discover2 d.
+Ltac appass f :=
+idt (forall x, f (f x) = x).
+
+(*
+Goal forall(T:Type), True. intros.
+ReplaceInTests T nat.
+discover mult.
+discover plus.
+discoverL
+[app(A:=T)=app(A:=T);
+length(A:=T)=length(A:=T);
+plus=plus].
+discoverL
+([app(A:=T)=app(A:=T);
+rev(A:=T)=rev(A:=T);
+length(A:=T)=length(A:=T);
+mult=mult;
+plus=plus;
+S=S;
+cons (A:=T)=cons (A:=T);
+postorder (A:=T)=postorder (A:=T);
+inorder (A:=T)=inorder (A:=T);
+preorder (A:=T)=preorder (A:=T);
+postorder (A:=T)=postorder (A:=T);
+mirror (A:=T)=mirror (A:=T);
+(*min =min ;
+max =max ;*)
+height (A:=T)=height (A:=T);
+num_nodes (A:=T)= num_nodes (A:=T)
+]).
+*)
129 general_tactics.v
@@ -0,0 +1,129 @@
+(* Automatically coerce bool terms to Prop terms when a Prop term is required *)
+(* Coercion is_true (b:bool) : Prop := if b then True else False.*)
+(* Do not hide function call added when coercion is used *)
+(* Set Printing Coercion is_true.*)
+
+(* Returns current goal *)
+Ltac get_goal := match goal with |- ?g => g end.
+
+(* Returns the head of a function application term *)
+Ltac fun_name t :=
+ match t with
+ | ?f ?a ?b ?c ?d ?e => f
+ | ?f ?a ?b ?c ?d => f
+ | ?f ?a ?b ?c => f
+ | ?f ?a ?b => f
+ | ?f ?a => f
+ | ?f => f (* FIXME: This will match anything! *)
+ end.
+
+(* try to solve the goal with a basic method *)
+Ltac easy :=
+ simpl in *;
+ try subst; (* substs will fail if there is a non-recursive equality. It succeeds if it does nothing. *)
+ reflexivity.
+
+Ltac typeof x := let r:= (type of x) in let q:= (type of r) in q.
+
+Ltac clear_rewrite x := rewrite x in *; clear x.
+Ltac clear_rewrite2 x := rewrite <- x in *; clear x.
+
+Ltac inject_subst x := injection x; intros; subst.
+
+Ltac freshname name label :=
+ let newname := fresh name label in newname.
+
+(* Instanitates first meta variable *)
+Ltac inst x := instantiate (1:=x).
+
+Ltac elim_call c :=
+(* Eliminate the function call *)
+ case c;
+ (* There will now be proj1_sig ( exists ... ) terms to simplify *)
+ simpl proj1_sig in *;
+ (* Introduce the sig type term and proof with nice names *)
+ let a := fresh "sig_term0" in let b := fresh "sig_proof0" in
+ intros a b;
+ let f:= (fun_name c) in
+ (* Try to eliminate the eliminated function call assumption *)
+ try clear f;
+ (* name the Set and Prop sig terms after the term they came from *)
+ try rename_after a f "_s"; try rename_after b f "_p".
+
+(* Eliminates inner most proj1_sig term in x *)
+Ltac elim_inner_proj1 x :=
+match x with
+| context [proj1_sig ?c] =>
+ (* Look for another match but use the current match if this fails. This finds the inner most match *)
+ elim_inner_proj1 c ||
+ elim_call c
+end.
+
+(* Eliminates all proj1_sig terms in goal. Useful when dealing with proof obligations produces by Program tactic. *)
+Ltac elim_proj1 :=
+ repeat elim_inner_proj1 get_goal.
+
+Ltac destruct_proj1 := elim_proj1.
+
+(* Performs destructs that are usually safe *)
+Ltac safe_destruct :=
+repeat match goal with
+| [ H: ex ?x |- _] => destruct H
+| [ H: ?x /\ ?y |- _] => destruct H
+| [ H: prod ?x ?y |- _] => destruct H
+| [ H: sig ?s |- _] =>
+ (* FIXME: Want to rename terms after s, but can't... *)
+ let a:= fresh in let b:= fresh in destruct H;
+ (* (proj1_sig s) terms will now simplify *)
+ simpl proj1_sig in *
+end.
+
+(* Try to find a contradiction with omega *)
+Ltac absurd_omega :=
+ solve [simpl in *; absurd (0 <> 0); omega].
+
+(* Tries to prove absurdity by trying inversion on all assumptions to find one that's impossible to construct *)
+Ltac absurd_inversion :=
+match goal with
+H:_ |- _ => inversion H; fail
+end.
+
+Ltac any_rewrite :=
+match goal with
+| [ H: ?x = ?y |- _] => idtac "rewrite" H ":" x "=" y; first [rewrite <- H | rewrite H]
+end.
+
+(* Easy inductive proof tactic. Tries to fertilise inductive step with any rewrites it finds *)
+Ltac trivial_induction x :=
+ induction x;
+ simpl;
+ try any_rewrite;
+ simpl;
+ reflexivity.
+
+Ltac destruct_exists :=
+match goal with
+| |- ex ?x => econstructor
+end.
+
+Ltac tidy3 :=
+ intros;
+ try safe_destruct;
+ simpl in *;
+ try elim_proj1;
+ simpl in *;
+ subst;
+ simpl in *.
+
+Ltac tidy4 :=
+ intros;
+ repeat safe_destruct;
+ elim_proj1;
+ simpl in *;
+ subst;
+ simpl in *.
+
+Ltac safe_tidy :=
+ intros;
+ elim_proj1;
+ subst.
113 rippling.v
@@ -0,0 +1,113 @@
+(* Initialises rippling *)
+
+(* Hides wave annotation type parameters *)
+Set Implicit Arguments.
+
+(* Wave annotations (identity functions *)
+Definition wave_out := (fun (A:Type) (x:A) => x).
+Definition wave_in := (fun (A:Type) (x:A) => x).
+Definition wave_hole := (fun (A:Type) (x:A) => x).
+Definition wave_sink := (fun (A:Type) (x:A) => x).
+
+(* Wave annotation notations *)
+Notation "'__' x '__'" := (wave_hole x) (at level 20, right associativity) : type_scope.
+Notation "<| x |>" := (wave_out x) (at level 20, right associativity) : type_scope.
+Notation ">| x |<" := (wave_in x) (at level 20, right associativity) : type_scope.
+Notation "& x &" := (wave_sink x) (at level 20, right associativity) : type_scope.
+
+Lemma fertilise_rewrite : forall (A:Type)(x y:A), x = y -> __ x __ = __ y __.
+tauto.
+Qed.
+
+(* FIXME: Hack to tell rippling what annotation functions to use. These should really be loaded from OCaml. *)
+Goal True.
+init_rippling wave_out wave_in wave_hole wave_sink fertilise_rewrite.
+Admitted.
+
+(* Ripples goal to a given *)
+Ltac ripple_to given db :=
+ let t := type of given in
+ ripple t.
+
+(* Ripples to a given, rewrites with given then makes attempt to solve goal *)
+Ltac go given db :=
+ ripple_to given db;
+ rewrite given;
+ tauto.
+
+(* Displays embedding between assumption and goal *)
+Ltac show_embeddings a :=
+ let x := type of a in match goal with |- ?g => let y := type of g in embeds x g end.
+
+(* Displays embedding between assumption and goal before and after tactic is applied (does not change goal) *)
+Ltac embeds_after_tactic a t :=
+ idtac "Before";
+ show_embeddings a;
+ try
+ (t;
+ idtac "After";
+ show_embeddings a; fail).
+
+(* Applies a tactic and displays embedding between assumption and goal before and after *)
+Ltac embeds_after_tactic2 a t :=
+ embeds_after_tactic a t;
+ t.
+
+Tactic Notation "ripple_progress" constr(a) tactic(t) := embeds_after_tactic2 a t.
+
+Tactic Notation "embeds" constr(a) :=
+ let x := type of a in match goal with |- ?g => let y := type of g in embeds x g end.
+
+Tactic Notation "embeds_after_tactic" constr(a) tactic(t):=
+ embeds_after_tactic a t.
+
+Tactic Notation "embeds_after_tactic2" constr(a) tactic(t):=
+ embeds_after_tactic2 a t.
+
+Ltac rewrite_l2r_in R A := rewrite R in A.
+Ltac rewrite_r2l_in R A := rewrite <- R in A.
+
+(* Fertilises the only the term marked by __ __ markers *)
+Ltac fert given dir :=
+ let E := fresh in
+ let T := fresh in
+
+ (* Given has form ... -> x = y *)
+ (* Goal should have the term x to fertilise into marked as __ x __ *)
+ (* First we create an assumption of the form __ x __ = x *)
+ (* Then we fertilise the RHS of this assumption to get __ x __ = y *)
+ (* Then we fertilise the conclusion with this assumption *)
+ (* This makes sure we only alter the parts of the conclusion we are meant to *)
+
+match goal with | _ : _ |- context [__ ?t __] =>
+ assert (E : __ t __ = t); [reflexivity | idtac];
+
+ (* Hide LHS of the assumption then fertilise it *)
+ set (T := t) in E at 1;
+ dir given E;
+
+ subst T;
+ rewrite E;
+ clear E
+ end.
+
+Ltac fert_l2r given := fert given rewrite_l2r_in.
+Ltac fert_r2l given := fert given rewrite_r2l_in.
+
+(* Use given from l2r/r2l to rewrite every matching occurance
+on lhs/rhs. *)
+Ltac fert2_side given dir :=
+ let E := fresh in
+ let T := fresh in
+
+ match goal with | _ : _ |- context [ ?lhs = ?rhs] =>
+ match dir with
+ false => set (T := rhs); rewrite given
+ | true => set (T := lhs); rewrite <- given
+ end;
+subst T
+end.
+
+Ltac fert2 given := (fert2_side given false || fert2_side given true).
+
+
2,729 rippling_plugin.ml
2,729 additions, 0 deletions not shown because the diff is too large. Please use a local Git client to view these changes.
295 tools.v
@@ -0,0 +1,295 @@
+(* Setup file for all proof automation tools and other useful things *)
+Require Import List.
+Require Export Syntax. (* put after "Import List" for [1;2] style list notation *)
+Require Import Program.
+Require Import Setoid.
+Require Import Bool.
+Require Import Omega.
+Require Import Arith.Compare_dec.
+
+Notation nat_eq_dec := eq_nat_decide.
+Notation bool_eq_dec := bool_dec.
+
+(* Test lots of examples; useful for when not finding a counterexample is
+expensive e.g. not identifying a program error for the user. Gives counterexample trace *)
+Ltac qc := intros; quickcheck 0 50 0 1.
+(* Check only a few examples with tracing off; useful for when a brief check is good enough
+e.g. after generalisation when it's usually easy to find counterexamples, as
+long as there are no side-conditions. Setting this too low can cause
+non-theorems to slip thru, too high and testing takes up more time *)
+Ltac fast_qc := intros; quickcheck 0 20 0 0.
+(* Checks more examples and gives no trace *)
+Ltac qc_no_trace := intros; quickcheck 0 50 0 0.
+
+Goal True.
+(* Quickcheck generators for common types *)
+Generator (forall x y:nat, {x=y}+{x<>y}) [eq_nat_decide].
+Generator (forall x y:bool, {x=y}+{x<>y}) [bool_dec].
+Generator (nat -> nat) [S].
+Generator (nat -> nat -> nat) [plus; mult].
+Admitted.
+
+Load "general_tactics.v".
+Load "rippling.v".
+Load "unit_testing.v".
+
+(* Removes ` notation for proj1_sig *)
+(*Notation "'proj1_sig' x" := (proj1_sig x) (at level 10).*)
+
+(*
+(* Turn off Program tactic proof automation *)
+Obligations Tactic := idtac.
+*)
+
+(*
+From: http://www.lix.polytechnique.fr/cocorico/if/then/else (tactical)
+"if t then t1 else t2 is equivalent to t; t1 if t does not fail and is equivalent to t2 otherwise."
+*)
+Tactic Notation
+ "if" tactic(t)
+ "then" tactic(t1)
+ "else" tactic(t2) :=
+ first [ t; first [ t1 | fail 2 ] | t2 ].
+
+(* Succeeds if c is a constant. c must be a constructor call with only
+ other constructors or type variables as parameters *)
+(* Extra fails are to stop backtracking on outer "match" *)
+Ltac constant c :=
+idtac;
+ match c with
+ | ?f ?x => idtac ;
+ first [constant f | fail 2];
+ first
+ [
+ constant x
+ |
+ let t := type of x in
+ match t with
+ | Type => idtac
+ | _ => fail
+ end
+ | fail 2]
+ | ?x => is_constructor x
+ | _ => fail 1
+end.
+
+Ltac constant_lhs := match goal with |- ?x = ?y => constant x end.
+Ltac constant_rhs := match goal with |- ?x = ?y => constant y end.
+
+
+(* Reverts all assumptions. Useful to do this so you can copy/paste the current goal as the conjecture for a new named lemma. *)
+Ltac revert_all := repeat match goal with [ H : _ |- _ ] => revert H end.
+
+(* Displays current goal in a format that can be copy/pasted as a stand alone lemma declaration e.g. Goal (forall x, x = x + 0). *)
+Ltac print_goal :=
+ try (revert_all; let g := get_goal in idtac "Copy/paste this to declare as a stand alone lemma:"; idtac "Goal"g"."; fail).
+
+(* Clears all assumptions that mention variable "x" *)
+Ltac clear_dep_ass x := match goal with H : context [ x ] |- _ => clear H end.
+
+(* For each assumption R, if R can be used in any direction as a rewrite rule, this tactic does so then clears the assumption *)
+Ltac use_equations :=
+ repeat match goal with
+ [ R: _ |- _ ] => (rewrite R in * || rewrite <- R in *); clear R; idtac "Used and discarded equation: " R
+ end.
+
+(* Like subst, but does not fail when it finds a recursive equation *)
+Ltac sub := repeat (match goal with x : _ |- _ => subst x end).
+
+(* Creates a new subgoal that is a copy of the current goal. This is useful
+if you e.g. want to write a hand proof and an automated proof of a theorem
+for testing or demonstration reasons. *)
+Ltac copy :=
+ match goal with
+ [ |- ?g ] => let f := fresh in cut g; [intro f;clear f | idtac]
+ end.
+
+(* Uses injection to simplify then (if possible) discard any equational assumptions *)
+Ltac auto_injection :=
+ repeat
+ match goal with
+ [ H : ?x = ?y |- _ ] =>
+ injection H;
+ match goal with
+ (* Original equation appears in conclusion if injection could not simplify it *)
+ | [ |- x = y -> _ ] => fail 1
+ | _ => let I := fresh in intro I; try clear H
+ end
+ end.
+
+Goal forall x y, S(x+1) = S(y+1) -> S x = S y -> True.
+intros.
+auto_injection.
+auto_injection.
+Admitted.
+
+Ltac auto_discriminate :=
+ match goal with
+ [ H : ?x = ?y |- _ ] => discriminate H
+ end.
+
+Goal 1 = 0 -> True.
+intros.
+auto_discriminate.
+Defined.
+
+(* Clears, if possible, unuseful equations of the form n = n *)
+Ltac remove_n_eq_n :=
+ repeat progress
+ match goal with
+ [ H : ?n = ?n |- _ ] => clear H
+ end.
+
+Ltac general :=
+ intros; generalise_goal; qc.
+
+Ltac rip := ripple.
+Ltac gen := generalise_goal; intros; irrelevant.
+
+Create HintDb cache discriminated.
+Create HintDb ripple discriminated.
+Create HintDb simp discriminated.
+
+(* destructs any proj1_sig terms in hypotheses *)
+Ltac destruct_proj1_hyp :=
+ repeat
+ match goal with
+ H := context [proj1_sig ?R] |- _ =>
+ let p := fresh "p" in
+ let s := fresh "s" in
+ destruct R as [s p];
+ simpl proj1_sig in H
+ | _ => fail 1
+ end.
+
+(* Eliminates (proj1_sig r) when this proof obligation was generated when
+ defining r. Works by assuming there will be an assumption with the name "r"
+ in the goal *)
+Ltac elim_rec_proj1 :=
+ match goal with
+ |- context [ proj1_sig ?c] =>
+ elim_call c;
+ let f := fun_name c in
+ clear f (* will fail if f is not an assumption *)
+ end.
+
+Ltac recursive_call :=
+ sub; (* subtitute pattern matching equations *)
+ elim_rec_proj1;
+ ripple.
+
+(* Simplifies initial Program tactic proof obligations without destroying any
+embeddings *)
+Ltac tidy :=
+ (* destruct calls to functions that return subset types *)
+ destruct_proj1;
+ destruct_proj1_hyp;
+ (* Boby of assumptions like "v := s : list t * list t" is lost if they are
+ destructed. substs these first *)
+ sub;
+ (* destruct subset types and others *)
+ safe_destruct;
+ sub.
+
+(* A basic simplification tactic *)
+Ltac simp_basic' :=
+ simpl in *;
+ unfold not; (* change ~P into P -> False *)
+ intros; (* must intro a var before "case" can be called on it *)
+ try case_concl; (* this can introduce implications and equations to the conclusion *)
+ intros;
+ try sub;
+ try split;
+ try auto_injection.
+
+Ltac simp_basic := repeat progress simp_basic'.
+
+Print HintDb core.
+
+Hint Resolve conj eq_refl eq_sym : cache.
+
+Ltac triv' :=
+ try tauto;
+ try auto_discriminate;
+ try absurd_inversion
+(* ;try omega*)
+ .
+
+(* A fast tactic to solve goals that do not need induction
+ (cached lemma usage factored out for testing reasons) *)
+Ltac triv :=
+ triv';
+ (* prove with "trivial". simpl first because only exact matches allowed *)
+ let t := auto_without_core with cache in (* don't use core *)
+ (* let t := trivial with cache in (* use core too *) *)
+ try solve [simpl; t]
+ .
+
+Ltac simp' :=
+ tidy;
+ repeat progress
+ (
+ simp_basic;
+ try use_equations (* try this last as this is unsafe and should be avoided *)
+ )
+ ; remove_n_eq_n (* remove n = n equations as these can be identified as pointless ripple targets *)
+ .
+
+(* A simplification tactic that performs case splits and uses autorewrite db *)
+Ltac simp :=
+ simp'
+ ; try (autorewrite with simp) (* need try because db might not exist *)
+ .
+
+(* Inverse functionality (e.g. S x = S y => x = y), restricted to when only one
+ subgoal is generated (e.g. this avoids x + y = y + x => x = y /\ y = x).
+ *)
+Ltac f_simp :=
+ repeat progress (simple apply f_equal).
+
+(* default solver configuration *)
+Ltac dt := super 5 (triv) (simp) (fast_qc) 1 with ripple_basic ripple_cached.
+(* same but without quickcheck (useful when you expect quickcheck to take too long) *)
+Ltac dn := super 5 (triv) (simp) (idtac) 1 with ripple_basic ripple_cached.
+(* basic solver that never uses cached lemmas *)
+Ltac d' := super 5 (triv') (simp') (fast_qc) 0 with ripple_basic.
+(* default solver plus initial descriptive counterexample check *)
+Ltac d :=
+ sub (*remove pattern matching equations first first to help quickcheck*);
+ qc;
+ try recursive_call; (* try recursive call proof pattern first *)
+ dt.
+Ltac ps := tidy; d.
+
+Tactic Notation "ind0" := induction_nth 0.
+Tactic Notation "ind1" := induction_nth 1.
+Tactic Notation "ind2" := induction_nth 2.
+Tactic Notation "ind3" := induction_nth 3.
+Tactic Notation "ind4" := induction_nth 4.
+
+Tactic Notation "indr1" :=
+ induction_nth 1; try (simp;triv;fail); try ripple.
+Tactic Notation "indr0" :=
+ induction_nth 0; try (simp;triv;fail); try ripple.
+Tactic Notation "indr2" :=
+ induction_nth 2; try (simp;triv;fail); try ripple.
+Tactic Notation "indr3" :=
+ induction_nth 3; try (simp;triv;fail); try ripple.
+Tactic Notation "indr4" :=
+ induction_nth 4; try (simp;triv;fail); try ripple.
+
+Ltac should_solve := solve_or_admit d.
+(* Tries to prove a lemma and add it as a rippling hint *)
+Ltac hint' lemma solver :=
+ let C := fresh "c" in
+ assert (C : lemma);
+ [clear;
+ (* This line only needed if solver does not cache e.g. if omega/admit was used.
+ Otherwise, lemma will be cached twice if used *)
+ (* lemma_cache *)
+ solver | idtac; clear C].
+Ltac hint lemma := hint' lemma d.
+
+Ltac case_split := case_concl; intros; sub.
+
+Load "discover.v".
84 unit_testing.v
@@ -0,0 +1,84 @@
+(* Useful functions for unit testing Coq scripts *)
+
+(* Make the printing width bigger so longer unit test output line are not broken up *)
+Set Printing Width 300.
+
+(* Used to abandon the current goal in tests *)
+Ltac admitted := idtac "************ GOAL ADMITTED ************"; admit.
+
+(* Display unit test success message *)
+Ltac unit_success_message :=
+ match goal with
+ [|- ?g] => idtac;idtac "<successtest goal='" g "'/>"
+ end.
+
+(* Display unit test fail message *)
+Ltac unit_fail_message :=
+ match goal with
+ [|- ?g] => idtac;idtac "*** FAILURE: <failedtest goal='" g "'/>"
+ end.
+
+(* If t succeeds display success message, otherwise display failure message. *)
+Ltac unit_succeeds t :=
+ try ((t; unit_success_message; fail 1) || unit_fail_message).
+
+(* Fails if goal is not equal to g *)
+Ltac goal_equals g:=
+ match goal with
+ [|-g] => idtac
+ | [|-?m] => fail
+ end.
+
+(* Checks goal equals g *)
+Ltac assert_goal g:=
+ match goal with
+ [|-g] => unit_success_message
+ | [|-?m] => unit_fail_message; idtac "<message>Goal is " " when it is expected to be " g ".</message>"
+ end.
+
+(* Unit test succeeds if tactic fails *)
+Tactic Notation "assert_fail" tactic(t) := try ((t; unit_fail_message; idtac "<message>Tactic succeeded when it was expected to fail.</message>"; fail 1) || unit_success_message).
+
+(* Unit test succeeds if tactic succeeds *)
+Tactic Notation "assert_success" tactic(t) := try ((t; unit_success_message;fail 1) || unit_fail_message).
+
+(* Expects t to succeed and changes the goal to g. This tactic does not modify the proof state. *)
+Tactic Notation "assert_result" tactic(t) constr(g) :=
+ try ((t;
+ match goal with
+ [|-g] => unit_success_message; fail 2
+ | [|-?m] => unit_fail_message; idtac "<message>Goal is " m " when it is expected to be " g ".</message>"; fail 2
+ end) || (unit_fail_message; idtac "<message>Tactic call failed when it was expected to succeed</message>")).
+
+(*
+Goal True.
+assert_result (fail) (True).
+assert_result (fail) (False).
+assert_result (idtac) (True).
+assert_result (idtac) (False).
+Admitted.
+*)
+
+Ltac solve_or_admit t :=
+(* Hack: creates a new goal the same as the current one, displays success if t solves this,
+ then admits the original goal. This trick is needed display the success message when t
+ solves as tactic execution stops when the proof is finished. *)
+(match goal with [|- ?g] => assert g;[t | unit_success_message; assumption] end)
+||
+(unit_fail_message; admitted).
+Tactic Notation "solve_or_admit" tactic(t) := solve_or_admit t.
+
+(* Succeds when assumption is present in the current list of assumptions. *)
+(* FIXME: "type of" will succed if the goal contains a variable called _unused_name
+ (i.e. not the name you pass to the tactic, the actual name "_usued_name"!). Using
+ obscure parameter name to avoid this bug. *)
+Ltac present _unused_name := try ((let t := type of _unused_name in fail 1) ||
+ fail 1 "<message>Assumption " _unused_name " was was unexpectedly missing.</message>").
+
+(* Succeeds when assumption is missing in the current list of assumptions *)
+Ltac missing a :=
+ try (present a; fail 1 "<message>Assumption " a " was was unexpectedly present.</message>").
+
+Ltac unit_missing a := let t:= missing a in assert_success t.
+Ltac unit_present a := let t:= present a in assert_success t.
+

0 comments on commit 5e52f32

Please sign in to comment.
Something went wrong with that request. Please try again.