Initial implementation of a new command to define (dependent) functions by

equations.
It is essentially an implementation of the "Eliminating Dependent
Pattern-Matching" paper by Goguen, McBride and McKinna, relying on the
new dependent eliminations tactics. The bulk is in
contrib/subtac/equations.ml4. It implements a tree splitting on a set of
clauses and the generation of a corresponding proof term along with some
obligations at each splitting node. The obligations are solved by
driving the dependent elimination tactic and you get a complete proof
term at the end with the code given by the equations at the right spots,
the rest of the cases being pruned automatically.
Does not support recursion yet, a file with examples is in the
test-suite. With recursion, it would be similar to Agda 2's pattern
matching, except it won't reduce in Coq due to JMeq's/K.
Incidentally, the simplification tactics after dependent elimination 
have been improved, resulting in a clearer and more space efficient
implementation.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11352 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 0 deletions

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 49b8833424..7fe5211afe 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -11,6 +11,19 @@
 (** This module implements various tactics used to simplify the goals produced by Program,
    which are also generally useful. *)
 
+(** The [do] tactic but using a Coq-side nat. *)
+
+Ltac do_nat n tac :=
+  match n with
+    | 0 => idtac
+    | S ?n' => tac ; do_nat n' tac
+  end.
+
+(** Do something on the last hypothesis, or fail *)
+
+Ltac on_last_hyp tac :=
+  match goal with [ H : _ |- _ ] => tac H || fail 1 end.
+
 (** Destructs one pair, without care regarding naming. *)
 
 Ltac destruct_one_pair :=