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, 109 insertions, 0 deletions

diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
new file mode 100644
index 000000000..d08ce884c
--- /dev/null
+++ b/test-suite/success/Equations.v
@@ -0,0 +1,109 @@
+Require Import Bvector.
+Require Import Program.
+
+Obligation Tactic := try equations.
+
+Equations neg (b : bool) : bool :=
+neg true := false ;
+neg false := true.
+
+Eval compute in neg.
+
+Require Import Coq.Lists.List.
+
+Equations head A (default : A) (l : list A) : A :=
+head A default nil := default ;
+head A default (cons a v) := a.
+
+Eval compute in head.
+
+Equations tail {A} (l : list A) : (list A) :=
+tail A nil := nil ;
+tail A (cons a v) := v.
+
+Eval compute in tail.
+
+Eval compute in (tail _ (cons 1 nil)).
+
+Equations app' {A} (l l' : list A) : (list A) :=
+app' A nil l := l ;
+app' A (cons a v) l := cons a (app v l).
+
+Eval compute in app'.
+
+Fixpoint zip {A} (f : A -> A -> A) (l l' : list A) : list A :=
+  match l, l' with
+    | nil, nil => nil
+    | cons a v, cons b v' => cons (f a b) (zip f v v')
+    | _, _ => nil
+  end.
+
+Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) :=
+zip' A f nil nil := nil ;
+zip' A f (cons a v) (cons b w) := cons (f a b) (zip f v w) ;
+zip' A f nil (cons b w) := nil ;
+zip' A f (cons a v) nil := nil.
+
+Eval compute in zip'.
+
+Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] beta iota zeta in zip'.
+
+Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) :=
+zip'' A f nil nil def := nil ;
+zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip f v w) ;
+zip'' A f nil (cons b w) def := def ;
+zip'' A f (cons a v) nil def := def.
+
+Eval compute in zip''.
+Eval cbv delta [ zip'' ] beta iota zeta in zip''.
+
+Implicit Arguments Vnil [[A]].
+Implicit Arguments Vcons [[A] [n]].
+
+Equations vhead A n (v : vector A (S n)) : A := 
+vhead A n (Vcons a v) := a.
+
+Eval compute in (vhead _ _ (Vcons 2 (Vcons 1 Vnil))).
+
+Axiom cheat : Π A, A.
+
+Equations vmap {A B} (f : A -> B) n (v : vector A n) : (vector B n) :=
+vmap A B f 0 Vnil := Vnil ;
+vmap A B f (S n) (Vcons a v) := Vcons (f a) (cheat _).
+
+Eval compute in (vmap _ _ id _ (@Vnil nat)).
+Eval compute in (vmap _ _ id _ (@Vcons nat 2 _ Vnil)).
+
+Inductive fin : nat -> Set :=
+| fz : Π {n}, fin (S n)
+| fs : Π {n}, fin n -> fin (S n).
+
+Inductive finle : Π (n : nat) (x : fin n) (y : fin n), Prop :=
+| leqz : Π {n j}, finle (S n) fz j
+| leqs : Π {n i j}, finle n i j -> finle (S n) (fs i) (fs j).
+
+Implicit Arguments finle [[n]].
+
+Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k :=
+trans (S n) fz j k leqz q := leqz ;
+trans (S n) (fs i) (fs j) fz (leqs p) q :=! q ;
+trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (cheat _).
+
+Lemma trans_eq1 n (j k : fin (S n)) q : trans (S n) fz j k leqz q = leqz.
+Proof. intros. simplify_equations ; reflexivity. Qed.
+
+Lemma trans_eq2 n i j k p q : trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (cheat _).
+Proof. intros. simplify_equations ; reflexivity. Qed.
+
+Section Image.
+  Context {S T : Type}.
+  Variable f : S -> T.
+  
+  Inductive Imf : T -> Type := imf (s : S) : Imf (f s).
+
+  Equations inv (t : T) (im : Imf t) : S :=
+  inv (f s) (imf s) := s.
+
+  Eval compute in inv.
+
+End Image.
\ No newline at end of file