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

6 files changed, 1073 insertions, 37 deletions

diff --git a/Makefile.common b/Makefile.common
index e323e2d9b..08ae6f835 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -309,8 +309,8 @@ SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \
   contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_cases.cmo \
   contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \
   contrib/subtac/subtac_command.cmo contrib/subtac/subtac_classes.cmo \
-  contrib/subtac/subtac.cmo \
-  contrib/subtac/g_subtac.cmo
+  contrib/subtac/subtac.cmo contrib/subtac/g_subtac.cmo \
+  contrib/subtac/equations.cmo
 
 RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 	contrib/rtauto/g_rtauto.cmo
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
new file mode 100644
index 000000000..15ea15f35
--- /dev/null
+++ b/contrib/subtac/equations.ml4
@@ -0,0 +1,782 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*) 
+
+(* $Id: subtac_cases.ml 11198 2008-07-01 17:03:43Z msozeau $ *)
+
+open Cases
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Inductiveops
+open Environ
+open Sign
+open Reductionops
+open Typeops
+open Type_errors
+
+open Rawterm
+open Retyping
+open Pretype_errors
+open Evarutil
+open Evarconv
+open List
+open Libnames
+
+type pat =
+  | PRel of int
+  | PCstr of constructor * pat list
+  | PInnac of constr
+      
+let rec constr_of_pat = function
+  | PRel i -> mkRel i
+  | PCstr (c, p) -> 
+      let c' = mkConstruct c in
+	mkApp (c', Array.of_list (constrs_of_pats p))
+  | PInnac r -> r
+      
+and constrs_of_pats l = map constr_of_pat l
+
+let rec pat_vars = function
+  | PRel i -> Intset.singleton i
+  | PCstr (c, p) -> pats_vars p
+  | PInnac _ -> Intset.empty
+
+and pats_vars l = 
+  fold_left (fun vars p -> 
+    let pvars = pat_vars p in
+    let inter = Intset.inter pvars vars in
+      if inter = Intset.empty then
+	Intset.union pvars vars
+      else error ("Non-linear pattern: variable " ^
+		     string_of_int (Intset.choose inter) ^ " appears twice"))
+    Intset.empty l
+
+let rec pats_of_constrs l = map pat_of_constr l
+and pat_of_constr c = 
+  match kind_of_term c with
+  | Rel i -> PRel i
+  | App (f, args) when isConstruct f -> 
+      PCstr (destConstruct f, pats_of_constrs (Array.to_list args))
+  | Construct f -> PCstr (f, [])
+  | _ -> PInnac c
+
+let innacs_of_constrs l = map (fun x -> PInnac x) l
+
+exception Conflict
+
+let rec pmatch p c =
+  match p, kind_of_term c with
+  | PRel i, t -> [i, c]
+  | PCstr (c, pl), App (c', l') when kind_of_term c' = Construct c -> 
+      pmatches pl (Array.to_list l')
+  | PCstr (c, []), Construct c' when c' = c -> []
+  | PInnac _, _ -> []
+  | _, _ -> raise Conflict
+
+and pmatches pl l =
+  match pl, l with
+  | [], [] -> []
+  | hd :: tl, hd' :: tl' -> pmatch hd hd' @ pmatches tl tl'
+  | _ -> raise Conflict
+
+let pattern_matches pl l = pmatches pl l
+
+(** Specialize by a substitution. *)
+
+let subst_tele s = replace_vars (List.map (fun (id, _, t) -> id, t) s)
+
+let subst_rel_subst k s c = 
+  let rec aux depth c =
+    match kind_of_term c with
+    | Rel n -> 
+	let k = n - depth in 
+	  if k >= 0 then 
+	    try lift depth (assoc k s) 
+	    with Not_found -> c
+	  else c
+    | _ -> map_constr_with_binders succ aux depth c
+  in aux k c
+    
+let subst_context s ctx =
+  let (_, ctx') = fold_right 
+    (fun (id, b, t) (k, ctx') ->
+      (succ k, (id, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx'))
+    ctx (0, [])
+  in ctx'
+
+let subst_rel_context k cstr ctx = 
+  let (_, ctx') = fold_right 
+    (fun (id, b, t) (k, ctx') ->
+      (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
+    ctx (k, [])
+  in ctx'
+
+let rec lift_pat n k p = 
+  match p with
+  | PRel i ->
+      if i >= k then PRel (i + n)
+      else p
+  | PCstr(c, pl) -> PCstr (c, lift_pats n k pl)
+  | PInnac r -> PInnac (liftn n k r)
+      
+and lift_pats n k = map (lift_pat n k)
+
+let rec subst_pat k t p = 
+  match p with
+  | PRel i -> 
+      if i = k then t
+      else if i > k then PRel (pred i)
+      else p
+  | PCstr(c, pl) ->
+      PCstr (c, subst_pats k t pl)
+  | PInnac r -> PInnac (substnl [constr_of_pat t] k r)
+
+and subst_pats k t = map (subst_pat k t)
+
+let rec specialize s p = 
+  match p with
+  | PRel i -> 
+      if mem_assoc i s then PInnac (assoc i s)
+      else p
+  | PCstr(c, pl) ->
+      PCstr (c, specialize_pats s pl)
+  | PInnac r -> PInnac (specialize_constr s r)
+
+and specialize_constr s c = subst_rel_subst 0 s c
+and specialize_pats s = map (specialize s)
+
+let lift_contextn n k sign =
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+    | [] -> []
+  in
+  liftrec (rel_context_length sign + k) sign
+
+type program = 
+  signature * clause list
+
+and signature = identifier * rel_context * constr
+
+and clause = rel_context * constr list * (constr, identifier located) rhs
+
+and lhs = pat list
+
+and ('a, 'b) rhs = 
+  | Program of 'a
+  | Empty of 'b
+
+type splitting = 
+  | Compute of rel_context * lhs * (constr, int) rhs
+  | Split of rel_context * lhs * int * inductive_family *
+      unification_result array * splitting option array
+
+and unification_result = 
+  rel_context * rel_context * constr * pat * substitution option
+
+and substitution = (int * constr) list
+
+type problem = rel_context * identifier * pat list
+
+(* let vars_of_tele = map (fun (id, _, _) -> mkVar id) *)
+
+let rels_of_tele tele = rel_list 0 (List.length tele)
+
+let patvars_of_tele tele = map (fun c -> PRel (destRel c)) (rels_of_tele tele)
+
+let split_solves split (delta, id, pats) =
+  match split with
+  | Compute (ctx, lhs, rhs) -> delta = ctx && pats = lhs
+  | Split (ctx, lhs, id, indf, us, ls) -> delta = ctx && pats = lhs
+
+let ids_of_constr c = 
+  let rec aux vars c = 
+    match kind_of_term c with
+    | Var id -> Idset.add id vars
+    | _ -> fold_constr aux vars c
+  in aux Idset.empty c
+
+let ids_of_constrs = 
+  fold_left (fun acc x -> Idset.union (ids_of_constr x) acc) Idset.empty
+
+let idset_of_list =
+  fold_left (fun s x -> Idset.add x s) Idset.empty
+
+let intset_of_list =
+  fold_left (fun s x -> Intset.add x s) Intset.empty
+
+let solves split (delta, id, pats as prob) = 
+  split_solves split prob && 
+  Intset.equal (pats_vars pats) (intset_of_list (map destRel (rels_of_tele delta)))
+
+let check_judgment ctx c t =
+  ignore(Typing.check (push_rel_context ctx (Global.env ())) Evd.empty c t); true
+
+let check_context env ctx =
+  fold_right
+    (fun (_, _, t as decl) env -> 
+      ignore(Typing.sort_of env Evd.empty t); push_rel decl env)
+    ctx env
+
+let split_context n c =
+  let after, before = list_chop n c in
+    match before with
+    | hd :: tl -> after, hd, tl
+    | [] -> raise (Invalid_argument "split_context")
+	
+let split_tele n ctx =
+  let rec aux after n l =
+    match n, l with
+    | 0, decl :: before -> before, decl, List.rev after
+    | n, decl :: before -> aux (decl :: after) (pred n) before
+    | _ -> raise (Invalid_argument "split_tele")
+  in aux [] n ctx
+
+let add_var_subst subst n c =
+  if mem_assoc n subst then 
+    if eq_constr (assoc n subst) c then subst
+    else raise Conflict
+  else (n, c) :: subst
+    
+let rec unify env subst x y =
+  match kind_of_term x, kind_of_term y with
+  | Rel n, _ -> add_var_subst subst n y
+  | _, Rel n -> add_var_subst subst n x
+  | App (c, l), App (c', l') when eq_constr c c' ->
+      unify_constrs env subst (Array.to_list l) (Array.to_list l')
+  | _, _ -> if eq_constr x y then subst else raise Conflict
+
+and unify_constrs env subst l l' = 
+  if List.length l = List.length l' then
+    fold_left2 (unify env) subst l l'
+  else raise Conflict
+
+let substituted_context subst ctx =
+  let substitute_in_ctx n c ctx =
+    let rec aux k after = function
+      | [] -> assert false
+      | decl :: before -> 
+	  if k = n then subst_rel_context 0 c (rev after) @ before
+	  else aux (succ k) (decl :: after) before
+    in aux 1 [] ctx
+  in
+  let substitute_in_subst n c s =
+    map (fun (k', c') ->
+      let k' = if k' < n then k' else pred k' in
+	(k', substnl [c] (pred n) c'))
+      s
+  in
+  let recsubst = Array.of_list (list_map_i (fun i _ -> mkRel i) 1 ctx) in
+  let record_subst k t =
+    Array.iteri (fun i c ->
+      if i < k then recsubst.(i) <- substnl [t] (succ (k - i)) c
+      else if i = k then recsubst.(i) <- t
+      else recsubst.(i) <- lift (-1) c)
+      recsubst
+  in
+  let rec aux ctx' = function
+    | [] -> ctx'
+    | (k, t) :: rest ->
+	let t' = lift (-k) t in (* caution, not always well defined *)
+	let ctx' = substitute_in_ctx k t' ctx' in
+	let rest' = substitute_in_subst k t' rest in
+	  record_subst (pred k) (lift (-1) t);
+	  aux ctx' rest'
+  in
+  let ctx' = aux ctx subst in
+    filter (fun (i, c) -> if isRel c then i <> destRel c else true)
+      (Array.to_list (Array.mapi (fun i x -> (succ i, x)) recsubst)), ctx'
+    
+let unify_type before ty =
+  try
+    let envb = push_rel_context before (Global.env()) in
+    let IndType (indf, args) = find_rectype envb Evd.empty ty in
+    let ind, params = dest_ind_family indf in
+(*     let vs = params @ args in *)
+    let vs = args in
+    let cstrs = Inductiveops.arities_of_constructors envb ind in
+    let cstrs = 
+      Array.mapi (fun i ty ->
+	let ty = prod_applist ty params in
+	let ctx, ty = decompose_prod_assum ty in
+	let env' = push_rel_context ctx (Global.env ()) in
+	let IndType (indf, args) = find_rectype env' Evd.empty ty in
+	let ind, params = dest_ind_family indf in
+	let constr = applist (mkConstruct (ind, succ i), params @ rels_of_tele ctx) in
+	let constrpat = PCstr ((ind, succ i), innacs_of_constrs params @ patvars_of_tele ctx) in
+	  env', ctx, constr, constrpat, (* params @  *)args)
+	cstrs
+    in
+      Array.map (fun (env', ctxc, c, cpat, us) -> 
+	let beforelen = length before and ctxclen = length ctxc in
+	let fullctx = (* lift_contextn beforelen 1  *)ctxc @ before in
+(* 	let c = liftn beforelen (succ ctxclen) c and cpat = lift_pat beforelen ctxclen cpat in *)
+	  try
+	    let fullenv = push_rel_context fullctx (Global.env ()) in
+	    let vs' = map (lift ctxclen) vs 
+	    and us' = map (liftn beforelen (succ ctxclen)) us in
+	    let subst = unify_constrs fullenv [] us' vs' in
+	    let subst', ctx' = substituted_context subst fullctx in
+	      (ctx', ctxc, c, cpat, Some subst')
+	  with Conflict -> 
+	    (fullctx, ctxc, c, cpat, None)) cstrs, indf
+  with Not_found -> (* not an inductive type *)
+    raise (Invalid_argument "unify_type: Not an inductive type")
+
+let rec id_of_rel n l =
+  match n, l with
+  | 0, (Name id, _, _) :: tl -> id
+  | n, _ :: tl -> id_of_rel (pred n) tl
+  | _, _ -> raise (Invalid_argument "id_of_rel")
+      
+let rec valid_splitting (f, delta, t, pats) tree = 
+  split_solves tree (delta, f, pats) && 
+    valid_splitting_tree (f, delta, t) tree
+    
+and valid_splitting_tree (f, delta, t) = function
+  | Compute (ctx, lhs, Program rhs) -> 
+      let subst = constrs_of_pats lhs in 
+	ignore(check_judgment ctx rhs (substl subst t)); true
+
+  | Compute (ctx, lhs, Empty split) -> 
+      let before, (x, _, ty), after = split_context split ctx in
+      let unify, _ = unify_type before ty in
+	array_for_all (fun (_, _, _, _, x) -> x = None) unify
+	  
+  | Split (ctx, lhs, rel, indf, unifs, ls) -> 
+      let before, (id, _, ty), after = split_tele (pred rel) ctx in
+      let unify, indf' = unify_type before ty in
+	assert(indf = indf');
+	if not (array_exists (fun (_, _, _, _, x) -> x <> None) unify) then false
+	else
+	  let ok, splits = 
+	    Array.fold_left (fun (ok, splits as acc) (ctx', ctxc, cstr, cstrpat, subst) -> 
+	      match subst with
+	      | None -> acc
+	      | Some subst ->
+(* 		  let env' = push_rel_context ctx' (Global.env ()) in *)
+(* 		  let ctx_correct =  *)
+(* 		    ignore(check_context env' (subst_context subst ctxc)); *)
+(* 		    ignore(check_context env' (subst_context subst before)); *)
+(* 		    true *)
+(* 		  in  *)
+		  let newdelta = 
+		    subst_context subst (subst_rel_context 0 cstr 
+					    (lift_contextn (length ctxc) 0 after)) @ before in
+		  let liftpats = lift_pats (length ctxc) rel lhs in
+		  let newpats = specialize_pats subst (subst_pats rel cstrpat liftpats) in
+		    (ok, (f, newdelta, newpats) :: splits))
+	      (true, []) unify
+	  in
+	  let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta (constrs_of_pats lhs) in
+	  let t' = replace_vars subst t in
+	    ok && for_all 
+	      (fun (f, delta', pats') -> 
+		array_exists (function None -> false | Some tree -> valid_splitting (f, delta', t', pats') tree) ls) splits
+	      
+let valid_tree (f, delta, t) tree = 
+  valid_splitting (f, delta, t, patvars_of_tele delta) tree
+
+let find_split curpats patcs =
+  let rec find_split_pat curpat patc =
+    match kind_of_term patc with
+    | Rel _ -> (* The pattern's a variable, don't split *) None
+    | App (f, args) when isConstruct f ->
+	let f = destConstruct f in
+	  (match curpat with
+	  | PCstr (f', args') when f = f' -> (* Already split at this level, continue *)
+	      find_split_pats args' (Array.to_list args)
+	  | PRel i -> (* Split on i *) Some i
+	  | _ -> None)
+    | Construct f ->
+	(match curpat with
+	| PCstr (f', []) when f = f' -> (* Already split at this level, no args *) None
+	| PRel i -> (* Split on i *) Some i
+	| _ -> None)
+    | _ -> None
+
+  and find_split_pats curpats patcs =
+    assert(List.length curpats = List.length patcs);
+    fold_left2 (fun acc -> 
+      match acc with
+      | None -> find_split_pat | _ -> fun _ _ -> acc)
+      None curpats patcs
+  in find_split_pats curpats patcs
+      
+open Pp
+open Termops
+
+let pr_constr_pat env c =
+  let pr = print_constr_env env c in
+    match kind_of_term c with
+    | App _ -> str "(" ++ pr ++ str ")"
+    | _ -> pr
+
+let pr_clause env (delta, patcs, rhs) =
+  let env = push_rel_context delta env in
+    prlist_with_sep spc (pr_constr_pat env) patcs 
+
+let pr_clauses env =
+  prlist_with_sep fnl (pr_clause env)
+
+let rec split_on env fdt var delta curpats clauses =
+  let before, (id, _, ty), after = split_tele (pred var) delta in
+  let unify, indf = unify_type before ty in
+  let clauses = ref clauses in
+  let splits = 
+    Array.map (fun (ctx', ctxc, cstr, cstrpat, s) ->
+      match s with
+      | None -> None
+      | Some s -> 
+	  (* ctx' |- s cstr, s cstrpat *)
+	  let newdelta =
+	    subst_context s (subst_rel_context 0 cstr 
+				(lift_contextn (length ctxc) 1 after)) @ ctx' in
+	  let liftpats = 
+	    (* delta |- curpats -> before; ctxc; id; after |- liftpats *)
+	    lift_pats (length ctxc) (succ var) curpats 
+	  in
+	  let liftpat = (* before; ctxc |- cstrpat -> before; ctxc; after |- liftpat *)
+	    lift_pat (pred var) 1 cstrpat
+	  in
+	  let substpat = (* before; ctxc; after |- liftpats[id:=liftpat] *)
+	    subst_pats var liftpat liftpats 
+	  in
+	  let lifts = (* before; ctxc |- s : newdelta ->
+			 before; ctxc; after |- lifts : newdelta ; after *)
+	    map (fun (k,x) -> (pred var + k, lift (pred var) x)) s
+	  in
+	  let newpats = specialize_pats lifts substpat in
+	  let matching, rest = partition (fun (delta', patcs, rhs) ->
+	    try ignore(pattern_matches newpats patcs); true with Conflict -> false)
+	    !clauses
+	  in
+	    clauses := rest;
+	    if matching = [] then (
+	      (* Try finding a splittable variable *)
+	      let (id, _) = 
+		fold_right (fun (id, _, ty as decl) (accid, ctx) -> 
+		  match accid with 
+		  | Some _ -> (accid, ctx)
+		  | None -> 
+		      let unify, indf = unify_type ctx ty in
+			if array_for_all (fun (_, _, _, _, x) -> x = None) unify then
+			  (Some id, ctx)
+			else (None, decl :: ctx))
+		  newdelta (None, [])
+	      in 
+		match id with
+		| None ->
+		    errorlabstrm "deppat"
+	      	      (str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++
+	      		  pr_clause env (newdelta, constrs_of_pats newpats, Empty var))
+		| Some id -> 
+		    Some (Compute (newdelta, newpats, 
+				  Empty (fst (lookup_rel_id (out_name id) newdelta))))
+	    ) else (
+	      let splitting = make_split_aux env fdt newdelta newpats matching in
+		Some splitting))
+      unify
+  in
+    assert(!clauses = []);
+    Split (delta, curpats, var, indf, unify, splits)
+      
+and make_split_aux env (f, d, t as fdt) delta curpats clauses =
+  match clauses with
+  (delta', patcs, rhs) :: clauses' ->
+    (match find_split curpats patcs with
+    | None -> (* No need to split anymore *)
+	let res = Compute (delta', pats_of_constrs patcs, rhs) in
+	  if clauses' <> [] then 
+	    errorlabstrm "make_split_aux"
+	      (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses)
+	  else res
+    | Some var -> split_on env fdt var delta curpats clauses)
+  | [] -> error "No clauses left"
+
+let make_split env (f, delta, t) clauses =
+  make_split_aux env (f, delta, t) delta (patvars_of_tele delta) clauses
+    
+open Evd
+open Evarutil
+
+let lift_substitution n s = map (fun (k, x) -> (k + n, x)) s
+let map_substitution s t = map (subst_rel_subst 0 s) t
+
+let term_of_tree isevar env (i, delta, ty) tree =
+  let rec aux = function
+    | Compute (ctx, lhs, Program rhs) -> 
+	let ty' = substl (rev (constrs_of_pats lhs)) ty in
+	let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_LetIn ty' ctx in
+	  mkCast(body, DEFAULTcast, typ), typ
+
+    | Compute (ctx, lhs, Empty split) ->
+	let ty' = substl (rev (constrs_of_pats lhs)) ty in
+	let split = (Name (id_of_string "split"), 
+		    Some (Class_tactics.coq_nat_of_int (1 + (length ctx - split))),
+		    Lazy.force Class_tactics.coq_nat)
+	in
+	let ty' = it_mkProd_or_LetIn ty' ctx in
+	let let_ty' = mkLambda_or_LetIn split (lift 1 ty') in
+	let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark true) let_ty' in
+	  term, ty'
+	    
+    | Split (ctx, lhs, rel, indf, unif, sp) -> 
+	let before, decl, after = split_tele (pred rel) ctx in
+	let ty' = substl (rev (constrs_of_pats lhs)) ty in
+	let branches = 
+	  array_map2 (fun (ctx', ctxc, cstr, cstrpat, subst) split -> 
+	    match split with
+	    | Some s -> aux s
+	    | None -> 
+		(* dead code, inversion will find a proof of False by splitting on the rel'th hyp *)
+		Class_tactics.coq_nat_of_int rel, Lazy.force Class_tactics.coq_nat)
+	    unif sp 
+	in
+	let branches_ctx =
+	  Array.mapi (fun i (br, brt) -> (id_of_string ("m_" ^ string_of_int i), Some br, brt))
+	    branches
+	in
+	let n, branches_lets = 
+	  Array.fold_left (fun (n, lets) (id, b, t) -> 
+	    (succ n, (Name id, Option.map (lift n) b, lift n t) :: lets))
+	    (0, []) branches_ctx
+	in
+	let liftctx = lift_contextn (Array.length branches) 0 ctx in
+	let case =
+	  let ty = it_mkProd_or_LetIn ty' liftctx in
+	  let ty = it_mkLambda_or_LetIn ty branches_lets in
+	  let nbbranches = (Name (id_of_string "branches"), 
+			   Some (Class_tactics.coq_nat_of_int (length branches_lets)),
+			   Lazy.force Class_tactics.coq_nat)
+	  in
+	  let nbdiscr = (Name (id_of_string "target"), 
+			Some (Class_tactics.coq_nat_of_int (length before)),
+			Lazy.force Class_tactics.coq_nat)
+	  in
+	  let ty = it_mkLambda_or_LetIn ty [nbbranches;nbdiscr] in
+	  let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark true) ty in
+	    term
+	in       
+	let casetyp = it_mkProd_or_LetIn ty' ctx in
+	  mkCast(case, DEFAULTcast, casetyp), casetyp
+
+  in aux tree
+
+open Topconstr
+open Constrintern
+open Decl_kinds
+
+type equation = identifier located * constr_expr list * (constr_expr, identifier located) rhs
+
+let locate_reference qid =
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> true
+    | SyntacticDef kn -> true
+
+let is_global id =
+  try 
+    locate_reference (make_short_qualid id)
+  with Not_found -> 
+    false
+
+let is_freevar ids env x =
+  try
+    if Idset.mem x ids then false
+    else
+      try ignore(Environ.lookup_named x env) ; false
+      with _ -> not (is_global x)
+  with _ -> true
+  
+let ids_of_patc c ?(bound=Idset.empty) l = 
+  let found id bdvars l =
+    if not (is_freevar bdvars (Global.env ()) (snd id)) then l
+    else if List.exists (fun (_, id') -> id' = snd id) l then l 
+    else id :: l 
+  in
+  let rec aux bdvars l c = match c with
+    | CRef (Ident lid) -> found lid bdvars l
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
+    | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+  in aux bound l c
+    
+let interp_pats isevar env impls pats sign =
+  let vars = fold_left (fun acc patc -> ids_of_patc patc acc) [] pats in
+  let varsctx, env' = 
+    fold_right (fun (loc, id) (ctx, env) ->
+      let decl =
+	let ty = e_new_evar isevar env ~src:(loc, BinderType (Name id)) (new_Type ()) in
+	  (Name id, None, ty) 
+      in
+	decl::ctx, push_rel decl env)
+      vars ([], env)
+  in
+  let patcs = 
+    fold_left2 (fun subst pat (_, _, ty) -> 
+      let ty = substl subst ty in
+	interp_casted_constr_evars isevar env' ~impls pat ty :: subst)
+      [] pats (List.rev sign)
+  in
+    isevar := nf_evar_defs !isevar;
+    (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, 
+    nf_env_evar (Evd.evars_of !isevar) env',
+    map (nf_evar (Evd.evars_of !isevar)) patcs)
+      
+let interp_eqn isevar env impls sign arity (idl, pats, rhs) =
+  let ctx, env', patcs = interp_pats isevar env impls pats sign in
+  let rhs' = match rhs with
+    | Program p -> 
+	Program (interp_casted_constr_evars isevar env' ~impls p (substl patcs arity))
+    | Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx))
+  in (ctx, rev patcs, rhs')	
+
+open Entries
+
+let define_by_eqs i l t eqs =
+  let env = Global.env () in
+  let isevar = ref (create_evar_defs Evd.empty) in
+  let (env', sign), impls = interp_context_evars isevar env l in
+  let arity = interp_type_evars isevar env' t in
+  let equations = map (interp_eqn isevar env ([],[]) sign arity) eqs in
+  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
+  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let prob = (i, sign, arity) in
+  let split = make_split env prob equations in
+    (* if valid_tree prob split then *)
+  let t, ty = term_of_tree isevar env prob split in
+  let undef = undefined_evars !isevar in
+  let obls, t', ty' = Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 t ty in
+    ignore(Subtac_obligations.add_definition i t' ty' obls)
+      
+module Gram = Pcoq.Gram
+module Vernac = Pcoq.Vernac_
+module Tactic = Pcoq.Tactic
+
+module DeppatGram =
+struct
+  let gec s = Gram.Entry.create ("Deppat."^s)
+
+  let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations"
+
+  let binders_let2 : local_binder list Gram.Entry.e = gec "binders_let2"
+end
+
+open Rawterm
+open DeppatGram 
+open Util
+open Pcoq
+open Prim
+open Constr
+
+GEXTEND Gram
+  GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2;
+ 
+  deppat_equations:
+    [ [ l = LIST1 equation SEP ";" -> l ] ]
+  ;
+
+  binders_let2:
+    [ [ l = binders_let -> l ] ]
+  ;
+
+  equation:
+    [ [ c = Constr.lconstr; r=rhs ->
+      match c with
+      | CApp (loc, (None, CRef (Ident lid)), l) ->
+	  (lid, List.map fst l, r)
+      | _ -> error "Error parsing equation" ] ]
+  ;
+
+  rhs:
+    [ [ ":=!"; id = identref -> Empty id
+      |":="; c = Constr.lconstr -> Program c
+    ] ]
+  ;
+  
+  END
+
+type 'a deppat_equations_argtype = (equation list, 'a) Genarg.abstract_argument_type
+
+let (wit_deppat_equations : Genarg.tlevel deppat_equations_argtype),
+  (globwit_deppat_equations : Genarg.glevel deppat_equations_argtype),
+  (rawwit_deppat_equations : Genarg.rlevel deppat_equations_argtype) =
+  Genarg.create_arg "deppat_equations"
+
+type 'a binders_let2_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+
+let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype),
+  (globwit_binders_let2 : Genarg.glevel binders_let2_argtype),
+  (rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) =
+  Genarg.create_arg "binders_let2"
+
+
+VERNAC COMMAND EXTEND Define_equations
+| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs) ] ->
+    [ define_by_eqs i l t eqs ]
+END
+
+open Tacmach
+open Tacexpr
+open Tactics
+open Tacticals
+
+let contrib_tactics_path =
+  make_dirpath (List.map id_of_string ["Equality";"Program";"Coq"])
+
+let tactics_tac s =
+  lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
+
+let destruct_last args =
+  Tacinterp.eval_tactic (TacArg(TacCall(dummy_loc, 
+				       ArgArg(dummy_loc, Lazy.force (tactics_tac "destruct_last")),args)))
+    
+let rec int_of_coq_nat c = 
+  match kind_of_term c with
+  | App (f, [| arg |]) -> succ (int_of_coq_nat arg)
+  | _ -> 0
+
+let solve_equations_goal tac gl =
+  let concl = pf_concl gl in
+  let targetn, branchesn, targ, brs, b =
+    match kind_of_term concl with
+    | LetIn (Name target, targ, _, b) ->
+	(match kind_of_term b with
+	| LetIn (Name branches, brs, _, b) ->
+	    target, branches, int_of_coq_nat targ, int_of_coq_nat brs, b
+	| _ -> error "Unnexpected goal")
+    | _ -> error "Unnexpected goal"
+  in
+  let branches, b = 
+    let rec aux n c =
+      if n = 0 then [], c
+      else match kind_of_term c with
+      | LetIn (Name id, br, brt, b) -> 
+	  let rest, b = aux (pred n) b in
+	    (id, br, brt) :: rest, b
+      | _ -> error "Unnexpected goal"
+    in aux brs b
+  in 
+  let ids = targetn :: branchesn :: map pi1 branches in
+  let cleantac = tclTHEN (intros_using ids) (thin ids) in
+  let dotac = tclDO (succ targ) intro in
+  let subtacs = 
+    tclTHENS (destruct_last [])
+      (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br onConcl) tac) branches)
+  in tclTHENLIST [cleantac ; dotac ; subtacs] gl
+      
+TACTIC EXTEND solve_equations
+  [ "solve_equations" tactic(tac) ] -> [ solve_equations_goal (snd tac) ]
+END
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index fd49517d7..e44d4cc7b 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -206,8 +206,8 @@ module SearchProblem = struct
       prlist (pr_ev evars) (sig_it gls)
 	
   let filter_tactics (glls,v) l =
-    let glls,nv = apply_tac_list tclNORMEVAR glls in
-    let v p = v (nv p) in
+(*     let glls,nv = apply_tac_list tclNORMEVAR glls in *)
+(*     let v p = v (nv p) in *)
     let rec aux = function
       | [] -> []
       | (tac,pri,pptac) :: tacl -> 
@@ -239,10 +239,16 @@ module SearchProblem = struct
       []
     else      
       let (cut, do_cut, ldb as hdldb) = List.hd s.localdb in
-	if !cut then []
+	if !cut then
+(* 	  let {it=gls; sigma=sigma} = fst s.tacres in *)
+(* 	    msg (str"cut:" ++ pr_ev sigma (List.hd gls) ++ str"\n"); *)
+	    []
 	else begin
-	  Option.iter (fun r -> r := true) do_cut;
 	  let {it=gl; sigma=sigma} = fst s.tacres in 
+	    Option.iter (fun r ->
+(*  	      msg (str"do cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
+	      r := true) do_cut;
+	  let gl = List.map (Evarutil.nf_evar_info sigma) gl in
 	  let nbgl = List.length gl in
 	  let g = { it = List.hd gl ; sigma = sigma } in
 	  let new_db, localdb = 
@@ -250,12 +256,14 @@ module SearchProblem = struct
 	      match tl with
 	      | [] -> hdldb, tl
 	      | (cut', do', ldb') :: rest ->
-		  if not (is_dep (Evarutil.nf_evar_info sigma (List.hd gl)) (List.tl gl)) then
+		  if not (is_dep (List.hd gl) (List.tl gl)) then
 		    let fresh = ref false in
-		      if do' = None then 
+		      if do' = None then (
+(*  			msg (str"adding a cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
 			(fresh, None, ldb), (cut', Some fresh, ldb') :: rest
-		      else 
-			(cut', None, ldb), tl
+		      ) else (
+(* 			msg (str"keeping the previous cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
+			(cut', None, ldb), tl )
 		  else hdldb, tl
 	  in let localdb = new_db :: localdb in
 	  let assumption_tacs = 
@@ -1689,21 +1697,23 @@ let (wit_constrexpr : Genarg.tlevel constr_expr_argtype),
 open Environ
 open Refiner
 
+let typeclass_app t gl =
+  let nprod = nb_prod (pf_concl gl) in
+  let env = pf_env gl in
+  let evars = ref (create_evar_defs (project gl)) in
+  let j = Pretyping.Default.understand_judgment_tcc evars env t in
+  let n = nb_prod j.uj_type - nprod in
+    if n<0 then error "Apply_tc: theorem has not enough premisses.";
+    Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !evars))
+      (fun gl ->
+	let clause = make_clenv_binding_apply gl (Some n) (j.uj_val,j.uj_type) NoBindings in
+	let cl' = evar_clenv_unique_resolver true ~flags:default_unify_flags clause gl in
+	let evd' = Typeclasses.resolve_typeclasses cl'.env ~fail:true cl'.evd in
+	  Clenvtac.clenv_refine true {cl' with evd = evd'} gl) gl
+      
 TACTIC EXTEND apply_typeclasses
-   [ "typeclass_app" raw(t) ] -> [ fun gl ->
-     let nprod = nb_prod (pf_concl gl) in
-     let env = pf_env gl in
-     let evars = ref (create_evar_defs (project gl)) in
-     let j = Pretyping.Default.understand_judgment_tcc evars env t in
-     let n = nb_prod j.uj_type - nprod in
-       if n<0 then error "Apply_tc: theorem has not enough premisses.";
-       Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !evars))
-	 (fun gl ->
-	   let clause = make_clenv_binding_apply gl (Some n) (j.uj_val,j.uj_type) NoBindings in
-	   let cl' = evar_clenv_unique_resolver true ~flags:default_unify_flags clause gl in
-	   let evd' = Typeclasses.resolve_typeclasses cl'.env ~fail:true cl'.evd in
-	     Clenvtac.clenv_refine true {cl' with evd = evd'} gl) gl
-   ]
+   [ "typeclass_app" raw(t) ] -> [ typeclass_app t ]
+(*  | [ "app" raw(t) ] -> [ typeclass_app t ] *)
 END
 
 let rec head_of_constr t =
@@ -1735,6 +1745,7 @@ let freevars c =
 
 let coq_zero =  lazy (gen_constant ["Init"; "Datatypes"] "O")
 let coq_succ =  lazy (gen_constant ["Init"; "Datatypes"] "S")
+let coq_nat =  lazy (gen_constant ["Init"; "Datatypes"] "nat")
 
 let rec coq_nat_of_int = function
   | 0 -> Lazy.force coq_zero
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
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index c569f743d..44d2f4f7e 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -30,7 +30,7 @@ Ltac on_JMeq tac :=
 (** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
 
 Ltac simpl_one_JMeq :=
-  on_JMeq ltac:(fun H => replace_hyp H (JMeq_eq H)).
+  on_JMeq ltac:(fun H => apply JMeq_eq in H).
 
 (** Repeat it for every possible hypothesis. *)
 
@@ -189,29 +189,29 @@ Ltac simplify_eqs :=
 Ltac simpl_IH_eq H :=
   match type of H with
     | @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H (JMeq_refl x))
+      specialize (H (JMeq_refl x))
     | _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ (JMeq_refl x))
+      specialize (H _ (JMeq_refl x))
     | _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ (JMeq_refl x))
+      specialize (H _ _ (JMeq_refl x))
     | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ _ (JMeq_refl x))
+      specialize (H _ _ _ (JMeq_refl x))
     | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ _ _ (JMeq_refl x))
+      specialize (H _ _ _ _ (JMeq_refl x))
     | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ _ _ _ (JMeq_refl x))
+      specialize (H _ _ _ _ _ (JMeq_refl x))
     | ?x = _ -> _ =>
-      refine_hyp (H (refl_equal x))
+      specialize (H (refl_equal x))
     | _ -> ?x = _ -> _ =>
-      refine_hyp (H _ (refl_equal x))
+      specialize (H _ (refl_equal x))
     | _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ (refl_equal x))
+      specialize (H _ _ (refl_equal x))
     | _ -> _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ _ (refl_equal x))
+      specialize (H _ _ _ (refl_equal x))
     | _ -> _ -> _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ _ _ (refl_equal x))
+      specialize (H _ _ _ _ (refl_equal x))
     | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ _ _ _ (refl_equal x))
+      specialize (H _ _ _ _ _ (refl_equal x))
   end.
 
 Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
@@ -306,3 +306,124 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c ; intros) H.
 
+(** Support for the [Equations] command.
+   These tactics implement the necessary machinery to solve goals produced by the 
+   [Equations] command relative to dependent pattern-matching. 
+   It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by
+   Goguen, McBride and McKinna.
+   
+*)
+
+(** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)
+
+Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x).
+Proof. intros; subst; assumption. Defined.
+
+Lemma solution_right : Π A (B : A -> Type) (t : A), B t -> (Π x, t = x -> B x).
+Proof. intros; subst; assumption. Defined.
+
+Lemma deletion : Π A B (t : A), B -> (t = t -> B).
+Proof. intros; assumption. Defined.
+
+Lemma simplification_heq : Π A B (x y : A), (x = y -> B) -> (JMeq x y -> B).
+Proof. intros; apply X; apply (JMeq_eq H). Defined.
+
+Lemma simplification_existT : Π A (P : A -> Type) B  (p : A) (x y : P p),
+  (x = y -> B) -> (existT P p x = existT P p y -> B).
+Proof. intros. apply X. apply inj_pair2. exact H. Defined.
+
+(** This hint database and the following tactic can be used with [autosimpl] to 
+   unfold everything to [eq_rect]s. *)
+
+Hint Unfold solution_left solution_right deletion simplification_heq simplification_existT : equations.
+Hint Unfold eq_rect_r eq_rec eq_ind : equations.
+
+(** Simply unfold as much as possible. *)
+
+Ltac unfold_equations := repeat progress autosimpl with equations.
+
+(** The tactic [simplify_equations] is to be used when a program generated using [Equations] 
+   is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *) 
+
+Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs). 
+
+(** Using these we can make a simplifier that will perform the unification 
+   steps needed to put the goal in normalised form (provided there are only
+   constructor forms). Compare with the lemma 16 of the paper.
+   We don't have a [noCycle] procedure yet. *) 
+
+Ltac simplify_one_dep_elim_term c :=
+  match c with
+    | @JMeq ?A ?a ?A ?b -> _ => refine (simplification_heq _ _ _ _ _)
+    | ?t = ?t -> _ => intros _
+    | eq (existT ?P ?p _) (existT ?P ?p _) -> _ => refine (simplification_existT _ _ _ _ _ _ _)
+    | ?f ?x = ?f ?y -> _ => let H := fresh in intros H ; injection H ; clear H
+    | ?x = ?y -> _ =>
+      (let hyp := fresh in intros hyp ; 
+        move dependent hyp before x ; 
+          generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) ||
+      (let hyp := fresh in intros hyp ; 
+        move dependent hyp before y ; 
+          generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0)
+    | ?t = ?u -> _ => let hyp := fresh in
+      intros hyp ; elimtype False ; discriminate
+    | _ => intro
+  end.
+
+Ltac simplify_one_dep_elim :=
+  match goal with
+    | [ |- ?gl ] => simplify_one_dep_elim_term gl
+  end.
+
+(** Repeat until no progress is possible. By construction, it should leave the goal with
+   no remaining equalities generated by the [generalize_eqs] tactic. *)
+
+Ltac simplify_dep_elim := repeat simplify_one_dep_elim.
+
+(** To dependent elimination on some hyp. *)
+
+Ltac depelim id :=
+  generalize_eqs id ; destruct id ; simplify_dep_elim.
+
+(** Do dependent elimination of the last hypothesis, but not simplifying yet
+   (used internally). *)
+
+Ltac destruct_last :=
+  on_last_hyp ltac:(fun id => generalize_eqs id ; destruct id).
+
+(** The rest is support tactics for the [Equations] command. *)
+
+(** Do as much as possible to apply a method, trying to get the arguments right. *)
+
+Ltac try_intros m :=
+  (eapply m ; eauto) || (intro ; try_intros m).
+
+(** To solve a goal by inversion on a particular target. *)
+
+Ltac solve_empty target :=
+  do_nat target intro ; elimtype False ; destruct_last ; simplify_dep_elim.
+
+Ltac simplify_method H := clear H ; simplify_dep_elim ; reverse.
+
+(** Solving a method call: we must refine the goal until the body 
+   can be applied or just solve it by splitting on an empty family member. *)
+    
+Ltac solve_method :=
+  match goal with
+    | [ H := ?body : nat |- _ ] => simplify_method H ; solve_empty body
+    | [ H := ?body |- _ ] => simplify_method H ; try_intros body
+  end.
+
+(** Impossible cases, by splitting on a given target. *)
+
+Ltac solve_split :=
+  match goal with 
+    | [ |- let split := ?x : nat in _ ] => intros _ ; solve_empty x
+  end.
+
+(** The [equations] tactic is the toplevel tactic for solving goals generated
+   by [Equations]. *)
+
+Ltac equations := 
+  solve [ solve_split ] || solve [solve_equations solve_method] || fail "Unnexpcted equations goal".
+
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 49b883342..7fe5211af 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 :=