Some more debugging of [Equations], unification still not perfect.

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

2 files changed, 409 insertions, 54 deletions

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index d17fbbf257..38009ba81e 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -86,19 +86,21 @@ exception Conflict
 
 let rec pmatch p c =
   match p, c with
-  | PRel i, t -> true
-(*   | _, PRel i -> true *)
+  | PRel i, t -> [i, t]
+(*   | PCstr _, PRel i -> [] *)
   | PCstr (c, pl), PCstr (c', pl') when c = c' -> pmatches pl pl'
-  | PInac _, _ -> true
-  | _, _ -> false
+  | PInac _, _ -> []
+  | _, PInac _ -> []
+  | _, _ -> raise Conflict
 
 and pmatches pl l =
   match pl, l with
-  | [], [] -> true
-  | hd :: tl, hd' :: tl' -> pmatch hd hd' && pmatches tl tl'
-  | _ -> false
-
-let pattern_matches pl l = pmatches pl l
+  | [], [] -> []
+  | hd :: tl, hd' :: tl' -> 
+      pmatch hd hd' @ pmatches tl tl'
+  | _ -> raise Conflict
+      
+let pattern_matches pl l = try Some (pmatches pl l) with Conflict -> None
 
 (* let rec pmatch p c = *)
 (*   match p, kind_of_term c with *)
@@ -291,11 +293,124 @@ and unify_constrs (env : env) subst l l' =
     fold_left2 (unify env) subst l l'
   else raise Conflict
 
-let substituted_context subst ctx =
+let fold_rel_context_with_binders f ctx init =
+  snd (List.fold_right (fun decl (depth, acc) ->
+    (succ depth, f depth decl acc)) ctx (0, init))
+    
+let dependent_rel_context (ctx : rel_context) k =
+  fold_rel_context_with_binders
+    (fun depth (n,b,t) acc -> 
+      let r = mkRel (depth + k) in
+	acc || dependent r t ||
+	  (match b with
+	  | Some b -> dependent r b
+	  | None -> false))
+    ctx false
+
+let liftn_between n k p c =
+  let rec aux depth c = match kind_of_term c with
+    | Rel i -> 
+	if i <= depth then c
+	else if i-depth > p then c
+	else mkRel (i - n)
+    | _ -> map_constr_with_binders succ aux depth c
+  in aux k c
+    
+let liftn_rel_context 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 (k + rel_context_length sign) sign
+
+let substnl_rel_context n l =
+  map_rel_context_with_binders (fun k -> substnl l (n+k-1))
+
+let reduce_rel_context (ctx : rel_context) (subst : (int * int) list) =
+  let _, s, ctx' =
+    fold_left (fun (k, s, ctx') (n, b, t as decl) ->
+      match b with
+      | None -> (succ k, mkRel k :: s, ctx' @ [decl])
+      | Some t -> (k, lift (pred k) t :: map (substnl [t] (pred k)) s, subst_rel_context 0 t ctx'))
+      (1, [], []) ctx
+  in
+  let s = rev s in
+  let s' = map (fun (korig, knew) -> korig, substl s (mkRel knew)) subst in
+    s', ctx'
+    
+(* let substituted_context (subst : (int * constr) list) (ctx : rel_context) = *)
+(*   let substitute_in_ctx n c ctx = *)
+(*     let rec aux k after = function *)
+(*       | [] -> [] *)
+(*       | (name, b, t as decl) :: before -> *)
+(* 	  if k = n then rev after @ (name, Some c, t) :: before *)
+(* 	  else aux (succ k) (decl :: after) before *)
+(*     in aux 1 [] ctx *)
+(*   in *)
+(*   let _, subst =  *)
+(*     fold_left (fun (k, s) _ -> *)
+(*       try let t = assoc k subst in *)
+(* 	    (succ k, (k, (k, t)) :: s) *)
+(*       with Not_found -> *)
+(* 	(succ k, (k, (k, mkRel k)) :: s)) *)
+(*       (1, []) ctx *)
+(*   in *)
+(*   let rec aux ctx' subst' = function *)
+(*     | [] -> ctx', subst' *)
+(*     | (korig, (k, t)) :: rest -> *)
+(* 	if t = mkRel k then  *)
+(* 	  aux ctx' ((korig, k)::subst') rest *)
+(* 	else if noccur_between 0 k t then *)
+(* 	  (\* The term to substitute refers only to previous variables. *\) *)
+(* 	  let t' = lift (-k) t in *)
+(* 	  let ctx' = substitute_in_ctx k t' ctx' in *)
+(* 	    aux ctx' ((korig, k)::subst') rest *)
+(* 	else (\* The term refers to variables declared after [k], so we move [k] *)
+(* 		after them *\) *)
+(* 	  let min = Intset.min_elt (free_rels t) in *)
+(* 	  let before, (n, b, ty), after = split_tele (pred k) ctx' in *)
+(* 	  let afterrest, aftermin = list_chop (pred min) (after : rel_context) in *)
+(* 	  let after' = *)
+(* 	    if dependent_rel_context aftermin 1 then *)
+(* 	      error "Unnable to build a merged context" *)
+(* 	    else substl_rel_context [t] aftermin *)
+(* 	  in *)
+(* 	  let afterrest' = *)
+(* 	    substnl_rel_context (2 + length after') [mkRel min] *)
+(* 	      (liftn_rel_context 2 0 afterrest) *)
+(* 	  in *)
+(* 	  let kdecl' = (n, Some (lift (-min) t), lift (length aftermin) ty) in *)
+(* 	  let ctx' = afterrest' @ (kdecl' :: after') @ before in *)
+(* 	  let substsubst (k', t') = *)
+(* 	    if k' > k then (\* Do nothing *\) (k', t') *)
+(* 	    else  *)
+(* 	      if k' >= min then (succ k, substnl [t] (pred k) t') *)
+(* 	    else *)
+(* 	      (\* Lift to get past the new decl *\) *)
+(* 	      (k, liftn_between 1 0 (length aftermin) t') *)
+(* 	  in  *)
+(* 	  let rest' = map (fun (korig, s) -> korig, substsubst s) rest in *)
+(* 	  let accsubst = map (fun (korig, knew) -> *)
+(* 	    let knew' = *)
+(* 	      if knew > k || knew < min then knew  *)
+(* 	      else if knew = k then min else pred knew  *)
+(* 	    in korig, knew') subst'  *)
+(* 	  in aux ctx' ((korig, min)::accsubst) rest' *)
+(*   in *)
+(*   let ctx', subst' = aux ctx [] subst in *)
+(*     reduce_rel_context ctx' subst' *)
+    
+    
+(*     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 substituted_context subst (ctx : rel_context) =
   let substitute_in_ctx n c ctx =
     let rec aux k after = function
       | [] -> []
-      | decl :: before -> 
+      | 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
@@ -309,7 +424,7 @@ let substituted_context subst ctx =
   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
+      if i < k then recsubst.(i) <- substnl [t] k c
       else if i = k then recsubst.(i) <- t
       else recsubst.(i) <- lift (-1) c)
       recsubst
@@ -317,7 +432,7 @@ let substituted_context subst ctx =
   let rec aux ctx' = function
     | [] -> ctx'
     | (k, t) :: rest ->
-	let t' = lift (-k) t in (* caution, not always well defined *)
+	let t' = lift (-k) t in
 	let ctx' = substitute_in_ctx k t' ctx' in
 	let rest' = substitute_in_subst k t' rest in
 	  record_subst (pred k) (liftn (-1) k t);
@@ -326,7 +441,7 @@ let substituted_context subst ctx =
   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
@@ -536,7 +651,13 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
 	  in
 	  let newpats = specialize_pats lifts substpat in
 	  let newlhs = (newdelta, f, newpats) in
-	  let matching, rest = partition (fun (lhs, rhs) -> lhs_matches newlhs lhs) !clauses in
+	  let matching, rest = 
+	    fold_right (fun (lhs, rhs as clause) (matching, rest) -> 
+	      match lhs_matches newlhs lhs with
+	      | Some _ -> (clause :: matching, rest)
+	      | None -> (matching, clause :: rest))
+	      !clauses ([], [])
+	  in
 	    clauses := rest;
 	    if matching = [] then (
 	      (* Try finding a splittable variable *)
@@ -582,18 +703,17 @@ and make_split_aux env lhs clauses =
     | None ->
 	(match clauses with
 	| [] -> error "No clauses left"
-	| [(lhs, rhs)] ->
-	    (* No need to split anymore *)
+	| [(lhs', rhs)] ->
 	    Compute (lhs, rhs)
-(* 	    (match rhs with *)
-(* 	    | Program _ -> *)
-(* 		Compute (delta', pats_of_constrs patcs, rhs) *)
-(* 	    | Empty split -> (\* TODO : Check unify_type inductive type *\) *)
-(* 		Compute (delta', pats_of_constrs patcs, rhs) *)
-		  (* 	    	errorlabstrm "deppat" *)
-		  (* 		  (str "Splitting on " ++ pr_id x ++ str " of type " ++  *)
-		  (* 		      pr_constr_env (push_rel_context before env)  *)
-		  (* 		      an empty type, on variable)) *)
+	    (* No need to split anymore, fix the environments so that they are correctly aligned. *)
+(* 	    (match lhs_matches lhs' lhs with *)
+(* 	    | Some s ->  *)
+(* 		let s = map (fun (x, p) -> x, constr_of_pat ~inacc:false env p) s in *)
+(* 		let rhs' = match rhs with  *)
+(* 		  | Program c -> Program (specialize_constr s c) *)
+(* 		  | Empty i -> Empty (destRel (assoc i s)) *)
+(* 		in Compute ((pi1 lhs, pi2 lhs, specialize_pats s (pi3 lhs')), rhs') *)
+(* 	    | None -> anomaly "Non-matching clauses at a leaf of the splitting tree") *)
 	| _ ->
 	    errorlabstrm "make_split_aux"
 	      (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses))
@@ -738,7 +858,8 @@ let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
   let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
   let rhs' = match rhs with
     | Program p -> 
-	Program (interp_casted_constr_evars isevar env' ~impls p (substl patcs arity))
+	let ty = nf_isevar !isevar (substl patcs arity) in
+	  Program (interp_casted_constr_evars isevar env' ~impls p ty)
     | Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx))
   in ((ctx, i, pats_of_constrs (rev patcs)), rhs')	
 
@@ -766,7 +887,7 @@ let define_by_eqs i l t nt eqs =
   let (env', sign), impls = interp_context_evars isevar env l in
   let arity = interp_type_evars isevar env' t in
   let ty = it_mkProd_or_LetIn arity sign in
-  let data = Command.compute_interning_datas env [] [i] [ty] [impls] in
+  let data = Command.compute_interning_datas env Constrintern.Recursive [] [i] [ty] [impls] in
   let fixdecls = [(Name i, None, ty)] in
   let fixenv = push_rel_context fixdecls env in
   let equations = 
@@ -920,4 +1041,47 @@ let solve_equations_goal destruct_tac tac gl =
     
 TACTIC EXTEND solve_equations
   [ "solve_equations" tactic(destruct) tactic(tac) ] -> [ solve_equations_goal (snd destruct) (snd tac) ]
+    END
+
+let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
+let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
+
+let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
+
+let simplify_hyp id gl =
+  let env = pf_env gl in
+  let ty = pf_get_hyp_typ gl id in
+  let evars = ref (create_evar_defs (project gl)) in
+  let rec aux in_eqs acc ty =
+    match kind_of_term ty with
+    | Prod (_, t, b) -> 
+	(match kind_of_term t with
+	| App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
+	    let pt = mkApp (Lazy.force coq_eq, [| eqty; x; x |]) in
+	    let p = mkApp (Lazy.force coq_eq_refl, [| eqty; x |]) in
+	      if e_conv env evars pt t then
+		aux true (mkApp (acc, [| p |])) (subst1 p b)
+	      else error "Unconvertible members of an homogeneous equality"
+	| App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
+	    let pt = mkApp (Lazy.force coq_heq, [| eqty; x; eqty; x |]) in
+	    let p = mkApp (Lazy.force coq_heq_refl, [| eqty; x |]) in
+	      if e_conv env evars pt t then
+		aux true (mkApp (acc, [| p |])) (subst1 p b)
+	      else error "Unconvertible members of an heterogeneous equality"
+	| _ -> 
+	    if in_eqs then acc, ty
+	    else 
+	      let e = e_new_evar evars env t in
+		aux false (mkApp (acc, [| e |])) (subst1 e b))
+    | t -> acc, ty
+  in 
+  let acc, ty = aux false (mkVar id) ty in
+  let ty = Evarutil.nf_isevar !evars ty in
+    tclTHENFIRST
+      (fun g -> Tacmach.internal_cut true id ty g)
+      (exact_no_check (Evarutil.nf_isevar !evars acc)) gl
+      
+TACTIC EXTEND simplify_hyp
+[ "simplify_hyp" ident(id) ] -> [ simplify_hyp id ]
 END
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
index 1609401855..f452aeadb8 100644
--- a/test-suite/success/Equations.v
+++ b/test-suite/success/Equations.v
@@ -1,4 +1,3 @@
-Require Import Bvector.
 Require Import Program.
 
 Equations neg (b : bool) : bool :=
@@ -54,6 +53,19 @@ zip'' A f (cons a v) nil def := def.
 
 Eval compute in @zip''.
 
+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]].
+
+
+Require Import Bvector.
+
 Implicit Arguments Vnil [[A]].
 Implicit Arguments Vcons [[A] [n]].
 
@@ -71,15 +83,169 @@ Eval compute in (vmap id (@Vnil nat)).
 Eval compute in (vmap id (@Vcons nat 2 _ Vnil)).
 Eval compute in @vmap.
 
-Inductive fin : nat -> Set :=
-| fz : Π {n}, fin (S n)
-| fs : Π {n}, fin n -> fin (S n).
+Record vlast_comp (A : Type) (n : nat) (v : vector A (S n)) : Type := { vlast_return : A }.
 
-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).
+Class Comp (comp : Type) :=
+  return_type : comp -> Type ; call : Π c : comp, return_type c.
 
-Implicit Arguments finle [[n]].
+Instance vlast_Comp A n v : Comp (vlast_comp A n v) :=
+  return_type := λ c, A ;
+  call := λ c, vlast_return A n v c.
+
+Ltac ind v := 
+  intros until v ; generalize_eqs_vars v ; induction v ; simplify_dep_elim.
+
+
+Tactic Notation "rec" ident(v) "as" simple_intropattern(p) :=
+  (try intros until v) ; generalize_eqs_vars v ; induction v as p ; simplify_dep_elim ; 
+    simpl_IH_eqs.
+
+Tactic Notation "rec" hyp(v) :=
+  (try intros until v) ; generalize_eqs_vars v ; induction v ; simplify_dep_elim ; 
+    simpl_IH_eqs.
+
+Tactic Notation "case" "*" hyp(v) "as" simple_intropattern(p) :=
+  (try intros until v) ; generalize_eqs_vars v ; destruct v as p ; simplify_dep_elim.
+
+Tactic Notation "case" "*" hyp(v) :=
+  (try intros until v) ; generalize_eqs_vars v ; destruct v ; simplify_dep_elim.
+
+Tactic Notation "=>" constr(v) := 
+  constructor ; 
+    match goal with
+      | [ |- ?T ] => refine (v:T)
+    end.
+
+Ltac make_refls_term c app :=
+  match c with
+    | _ = _ -> ?c' => make_refls_term (app (@refl_equal _ _))
+    | @JMeq _ _ _ _ -> ?c' => make_refls_term (app (@JMeq_refl _ _))
+    | _ => constr:app
+  end.
+
+Ltac make_refls_IH c app :=
+  match c with
+    | Π x : _, ?c' => make_refls_IH (app _)
+    | _ => make_refls_term c app
+  end.
+
+Ltac simpl_IH H :=
+  let ty := type of H in
+    make_refls_IH ty H.
+
+Ltac move_top H :=
+  match reverse goal with [ H' : _ |- _ ] => move H after H' end.
+
+Ltac simplify_dep_elim_hyp H evhyp :=
+  let ev := eval compute in evhyp in
+    subst evhyp ; intros evhyp ; move_top evhyp ; simplify_dep_elim ; 
+      try clear H ; reverse ; intro evhyp ; eapply evhyp.
+
+(* Tactic Notation "strengthen" hyp(H) := *)
+(*   let strhyp := fresh "H'" in *)
+(*   let ty := type of H in *)
+(*     on_last_hyp ltac:(fun id => *)
+(*       reverse ; evar (strhyp:Type) ; intros until id). *)
+
+(*         assert(strhyp -> ty) ; [ simplify_dep_elim_hyp strhyp | intros ]). *)
+
+
+Equations Below_nat (P : nat -> Type) (n : nat) : Type :=
+Below_nat P 0 := unit ;
+Below_nat P (S n) := prod (P n) (Below_nat P n).
+
+Equations below_nat (P : nat -> Type) n (step : Π (n : nat), Below_nat P n -> P n) : Below_nat P n :=
+below_nat P 0 step := tt ;
+below_nat P (S n) step := let rest := below_nat P n step in
+  (step n rest, rest).
+
+Class BelowPack (A : Type) :=
+  Below : Type ; below : Below.
+
+Instance nat_BelowPack : BelowPack nat :=
+  Below := Π P n step, Below_nat P n ;
+  below := λ P n step, below_nat P n (step P).
+
+Definition rec_nat (P : nat -> Type) n (step : Π n, Below_nat P n -> P n) : P n :=
+  step n (below_nat P n step).
+
+Fixpoint Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type :=
+  match v with Vnil => unit | Vcons a n' v' => prod (P A n' v') (Below_vector P A n' v') end.
+
+(* Equations Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type := *)
+(* Below_vector P A ?(0) Vnil := unit ; *)
+(* Below_vector P A ?(S n) (Vcons a v) := prod (P A n v) (Below_vector P A n v). *)
+
+Equations below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n)
+  (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : Below_vector P A n v :=
+below_vector P A 0 Vnil step := tt ;
+below_vector P A (S n) (Vcons a v) step := 
+  let rest := below_vector P A n v step in
+    (step A n v rest, rest).
+
+Instance vector_BelowPack : BelowPack (Π A n, vector A n) :=
+  Below := Π P A n v step, Below_vector P A n v ;
+  below := λ P A n v step, below_vector P A n v (step P).
+
+Instance vector_noargs_BelowPack A n : BelowPack (vector A n) :=
+  Below := Π P v step, Below_vector P A n v ;
+  below := λ P v step, below_vector P A n v (step P).
+
+Definition rec_vector (P : Π A n, vector A n -> Type) A n v
+  (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : P A n v :=
+  step A n v (below_vector P A n v step).
+
+Class Recursor (A : Type) (BP : BelowPack A) := 
+  rec_type : Π x : A, Type ; rec : Π x : A, rec_type x.
+
+Instance nat_Recursor : Recursor nat nat_BelowPack :=
+  rec_type := λ n, Π P step, P n ;
+  rec := λ n P step, rec_nat P n (step P).
+
+(* Instance vect_Recursor : Recursor (Π A n, vector A n) vector_BelowPack := *)
+(*   rec_type := Π (P : Π A n, vector A n -> Type) step A n v, P A n v; *)
+(*   rec := λ P step A n v, rec_vector P A n v step. *)
+
+Instance vect_Recursor_noargs A n : Recursor (vector A n) (vector_noargs_BelowPack A n) :=
+  rec_type := λ v, Π (P : Π A n, vector A n -> Type) step, P A n v;
+  rec := λ v P step, rec_vector P A n v step.
+
+Implicit Arguments Below_vector [P A n].
+
+Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
+
+Ltac idify := match goal with [ |- ?T ] => change (id T) end.
+
+(*  induction v as [ | a v']; simplify_dep_elim. *)
+(*   on_last_hyp ltac:(fun id => *)
+(*     let strhyp := fresh "H'" in *)
+(*     let ty := type of IHv in *)
+(*       reverse ; evar (strhyp:Type) ; intros ; *)
+(*         let newhyp := fresh "IHv''" in *)
+(*           assert(ty = strhyp) ; [ idtac (* simplify_dep_elim_hyp IHv strhyp *) | idtac ]). *)
+(* (*         subst strhyp ; intros ; try (apply newhyp in IHv) ]). *) *)
+
+Ltac simpl_rec X :=
+  match type of X with
+    | ?f (?c ?x) =>  
+      let X1 := fresh in
+      let X2 := fresh in
+        hnf in X ; destruct X as [X1 X2] ; simplify_hyp X1
+    | _ => idtac
+  end.
+
+Ltac recur v :=
+  try intros until v ; generalize_eqs_vars v ; reverse ;
+  intros until v ; assert (recv:=rec v) ; simpl in recv ;
+    eapply recv; clear ; simplify_dep_elim.
+
+Definition vlast {A} {n} (v : vector A (S n)) : vlast_comp A n v.
+recur v. case* v0. case* v0. => a. simpl_rec X.
+=> (call H).
+Defined.
+  
+Record trans_comp {n:nat} {i j k : fin n} (p : finle i j) (q : finle j k) :=  {
+  return_comp : finle i k }.
 
 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 ;
@@ -160,14 +326,14 @@ Equations tabulate {A} {n} (f : fin n -> A) : vector A n :=
 tabulate A 0 f := Vnil ;
 tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)).
 
-Equations vlast {A} {n} (v : vector A (S n)) : A :=
-vlast A 0 (Vcons a Vnil) := a ;
-vlast A (S n) (Vcons a v) := vlast v.
+Equations vlast' {A} {n} (v : vector A (S n)) : A :=
+vlast' A 0 (Vcons a Vnil) := a ;
+vlast' A (S n) (Vcons a v) := vlast' v.
 
-Lemma vlast_equation1 A (a : A) : vlast (Vcons a Vnil) = a.
+Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a.
 Proof. intros. compute ; reflexivity. Qed.
 
-Lemma vlast_equation2 A n a v : @vlast A (S n) (Vcons a v) = vlast v.
+Lemma vlast_equation2 A n a v : @vlast' A (S n) (Vcons a v) = vlast' v.
 Proof. intros. compute ; reflexivity. Qed.
 
 Print Assumptions vlast.
@@ -188,10 +354,10 @@ Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x
 Proof. intros until y. simplify_dep_elim. reflexivity. Qed.
 
 Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop :=
-NoConfusion_fin P (S n) fz fz := P -> P ;
-NoConfusion_fin P (S n) fz (fs y) := P ;
-NoConfusion_fin P (S n) (fs x) fz := P ;
-NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P.
+NoConfusion_fin P ?(S n) fz fz := P -> P ;
+NoConfusion_fin P ?(S n) fz (fs y) := P ;
+NoConfusion_fin P ?(S n) (fs x) fz := P ;
+NoConfusion_fin P ?(S n) (fs x) (fs y) := (x = y -> P) -> P.
 
 Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y :=
 noConfusion_fin P (S n) fz fz refl := λ p, p ;
@@ -201,14 +367,39 @@ Equations NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop :=
 NoConfusion_vect P A 0 Vnil Vnil := P -> P ;
 NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P.
 
-Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y :=
-noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ;
-noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl.
+(* Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y := *)
+(* noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ; *)
+(* noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl. *)
+
+(* Instance fin_noconf n : NoConfusionPackage (fin n) := *)
+(*   NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ; *)
+(*   noConfusion := λ P x y, noConfusion_fin P n x y. *)
+
+(* Instance vect_noconf A n : NoConfusionPackage (vector A n) := *)
+(*   NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ; *)
+(*   noConfusion := λ P x y, noConfusion_vect P A n x y. *)
+
+Equations fog {n} (f : fin n) : nat :=
+fog (S n) fz := 0 ; fog (S n) (fs f) := S (fog f).
+
+About vapp.
+
+Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set :=
+  append : Π (xs : vector X m)(ys : vector X n), Split (vapp xs ys).
+
+Implicit Arguments Split [[X]].
+
+Equations split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs :=
+split X 0    n xs := append Vnil xs ;
+split X (S m) n (Vcons x xs) := 
+  let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in
+    append (Vcons x xs') ys'.
+
+Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))).
+Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))).
+
+Extraction Inline split_obligation_1 split_obligation_2.
 
-Instance fin_noconf n : NoConfusionPackage (fin n) :=
-  NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ;
-  noConfusion := λ P x y, noConfusion_fin P n x y.
+Recursive Extraction split.
 
-Instance vect_noconf A n : NoConfusionPackage (vector A n) :=
-  NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ;
-  noConfusion := λ P x y, noConfusion_vect P A n x y.
+Eval compute in @split.