Finish debugging the unification machinery in [Equations]. Do the _comp

dance when defining a new program by default, which forces use of JMeq
but makes for much more robust tactics. Everything in success/Equations 
works except for limitations due to JMeq or the guardness checker (one
example seems to actually diverge...).


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

3 files changed, 146 insertions, 126 deletions

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index 6e16d01a9f..515a78280e 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -368,16 +368,25 @@ let subst_telescope k cstr ctx =
     (k, []) ctx
   in rev ctx'
 
+let lift_telescope n k sign =
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (succ k) sign)
+    | [] -> []
+  in liftrec k sign
+    
 type ('a,'b) either = Inl of 'a | Inr of 'b
-
+  
 let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (int * (int, int) either) list =
   let rels = dependencies_of_term ctx t in
   let len = length ctx in
-  let lifting = len - Intset.cardinal rels in (* Number of variables not linked to t *)
+  let nbdeps = Intset.cardinal rels in
+  let lifting = len - nbdeps in (* Number of variables not linked to t *)
   let rec aux k n acc m rest s = function
     | decl :: ctx' ->
 	if Intset.mem k rels then
-	  aux (succ k) (succ n) (decl :: acc) m (subst_telescope 0 (mkRel (succ n + lifting - m)) rest) ((k, Inl n) :: s) ctx'
+	  let rest' = subst_telescope 0 (mkRel (nbdeps + lifting - pred m)) rest in
+	    aux (succ k) (succ n) (decl :: acc) m rest' ((k, Inl n) :: s) ctx'
 	else aux (succ k) n (subst_telescope 0 mkProp acc) (succ m) (decl :: rest) ((k, Inr m) :: s) ctx'
     | [] -> rev acc, rev rest, s
   in aux 1 1 [] 1 [] [] ctx
@@ -395,16 +404,44 @@ let merge_subst (ctx', rest, s) =
 
 let compose_subst s' s =
   map (fun (k, (b, t)) -> (k, (b, specialize_constr s' t))) s
-      
+
+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
+    
+let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) list) (cursubst : (int * (bool * constr)) list) =
+  match cursubst with
+  | [] -> ctx, substacc
+  | (k, (b, t)) :: rest ->
+      if t = mkRel k then reduce_subst ctx substacc rest
+      else if noccur_between 1 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
+	  reduce_subst ctx' substacc rest
+      else (* The term refers to variables declared after [k], so we have 
+	      to move these dependencies before [k]. *)
+	let (minctx, ctxrest, subst as str) = strengthen ctx t in
+	  match assoc k subst with
+	  | Inl _ -> error "Occurs check in substituted_context"
+	  | Inr k' ->
+	      let s = merge_subst str in
+	      let ctx' = ctxrest @ minctx in
+	      let rest' =
+		let substsubst (k', (b, t')) =
+		  match kind_of_term (snd (assoc k' s)) with
+		  | Rel k'' -> (k'', (b, specialize_constr s t'))
+		  | _ -> error "Non-variable substituted for variable by strenghtening"
+		in map substsubst ((k, (b, t)) :: rest)
+	      in
+		reduce_subst ctx' (compose_subst s substacc) rest' (* (compose_subst s ((k, (b, t)) :: rest)) *)
+		  
+		  
 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
@@ -413,33 +450,7 @@ let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
 	(succ k, ((k, (false, mkRel k)) :: s)))
       (1, []) ctx
   in
-  let rec aux ctx' subst' = function
-    | [] -> ctx', subst'
-    | (k, (b, t)) :: rest ->
-	if t = mkRel k then
-	  aux ctx' 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' subst' rest
-	else (* The term refers to variables declared after [k], so we have 
-		to move these dependencies before [k]. *)
-	  let (minctx, ctxrest, subst as str) = strengthen ctx' t in
-	    match assoc k subst with
-	    | Inl _ -> error "Occurs check in substituted_context"
-	    | Inr k' ->
-		let s = merge_subst str in
-		let ctx' = ctxrest @ minctx in
-		let rest' = 
-		  let substsubst (k', (b, t')) =
-		    match kind_of_term (snd (assoc k' s)) with
-		    | Rel k'' -> (k'', (b, specialize_constr s t'))
-		    | _ -> error "Non-variable substituted for variable by strenghtening"
-		  in map substsubst ((k, (b, t)) :: rest)
-		in aux ctx' (compose_subst s subst') rest'
-  in
-  let ctx', subst' = aux ctx subst subst in
+  let ctx', subst' = reduce_subst ctx subst subst in
     reduce_rel_context ctx' subst'
     
 let unify_type before ty =
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
index 955ecc93b6..4503455243 100644
--- a/test-suite/success/Equations.v
+++ b/test-suite/success/Equations.v
@@ -61,22 +61,18 @@ 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]].
+Scheme finle_ind_dep := Induction for finle Sort Prop.
+
+Instance finle_ind_pack n x y : DependentEliminationPackage (finle n x y) :=
+  elim_type := _ ; elim := finle_ind_dep.
 
+Implicit Arguments finle [[n]].
 
 Require Import Bvector.
 
 Implicit Arguments Vnil [[A]].
 Implicit Arguments Vcons [[A] [n]].
 
-Ltac do_case p ::= destruct p.
-
-Ltac simpl_intros m := (apply m ; auto) || (intro ; simpl_intros m).
-
-Ltac try_intros m ::= 
-  solve [ intros ; unfold Datatypes.id ; refine m || apply m ] || 
-  solve [ unfold Datatypes.id ; simpl_intros m ].
-
 Equations vhead {A n} (v : vector A (S n)) : A := 
 vhead A n (Vcons a v) := a.
 
@@ -148,36 +144,11 @@ Implicit Arguments Below_vector [P A n].
 
 Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
 
-(* 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) (fs k) (leqs p) (leqs q) := leqs (trans p q). *)
-
-(* Obligation Tactic := idtac. *)
-(* Solve Obligations using unfold trans_comp ; equations. *)
-
-(* Next Obligation. intro recc. *)
-(*   info solve_equations (case_last) idtac. *)
-(*   solve_method intro. *)
-(*   clear m_1 ; clear ; simplify_method idtac.  *)
-(*   unfold Datatypes.id. intros. until p. *)
-(*   case_last ; simplify_dep_elim. simpl. *)
-(* ; solve_empty 2. *)
-(*   solve_method intro. *)
-  
-
-(*   subst m_1 ; clear. *)
-(*   simplify_method idtac. *)
-(*   intros. generalize_eqs p. case p. *)
-(*  solve_empty 2. *)
-
-(*   simplify_dep_elim. unfold Datatypes.id. intros. *)
-(*   apply m_0. *)
-(*   Debug Off. *)
-(*   pose (m_0:=(λ (H : nat) (j k : fin (S H)) (_ : finle j k), leqz) : Π (H : nat) (j k : fin (S H)), finle j k -> finle fz k). *)
-(*   intros. *)
-
-(*   solve_method intro. *)
+(** Won't pass the guardness check which diverges anyway. *)
 
+(* 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) ?(fs k) (leqs p) (leqs q) := leqs (trans p q). *)
 
 (* Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. *)
 (* Proof. intros. simplify_equations ; reflexivity. Qed. *)
@@ -219,8 +190,6 @@ Eval compute in (foo ubool false).
 Eval compute in (foo (uarrow ubool ubool) negb).
 Eval compute in (foo (uarrow ubool ubool) id).
 
-(* Overlap. *)
-
 Inductive foobar : Set := bar | baz.
 
 Equations bla (f : foobar) : bool :=
@@ -238,8 +207,6 @@ K A x P p refl := p.
 Equations eq_sym {A} (x y : A) (H : x = y) : y = x :=
 eq_sym A x x refl := refl.
 
-(* Obligation Tactic := idtac. *)
-
 Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z :=
 eq_trans A x x x refl refl := refl.
 
@@ -254,9 +221,15 @@ 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 (n:=S n) v) := vlast v.
+
+Print Assumptions vlast.
+
 Equations vlast' {A} {n} (v : vector A (S n)) : A :=
-vlast' A ?(0) (@Vcons A a 0 Vnil) := a ;
-vlast' A ?(S n) (@Vcons A a (S n) v) := vlast' v.
+vlast' A ?(0) (Vcons a Vnil) := a ;
+vlast' A ?(S n) (Vcons a (n:=S n) v) := vlast' v.
 
 Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a.
 Proof. intros. simplify_equations. reflexivity. Qed.
@@ -266,7 +239,10 @@ Proof. intros. simplify_equations ; reflexivity. Qed.
 
 Print Assumptions vlast'.
 Print Assumptions nth. 
-Print Assumptions tabulate. 
+Print Assumptions tabulate.
+
+Extraction vlast.
+Extraction vlast'.
 
 Equations vliat {A} {n} (v : vector A (S n)) : vector A n :=
 vliat A 0 (Vcons a Vnil) := Vnil ;
@@ -289,18 +265,22 @@ Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
 Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y).
 Proof. intros until y. simplify_dep_elim. reflexivity. Qed.
 
-Equations_nocomp NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop :=
+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.
 
 Eval compute in NoConfusion_fin.
+Eval compute in NoConfusion_fin_comp.
+
 Print Assumptions NoConfusion_fin.
 
-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 ;
-noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl.
+Eval compute in (fun P n => NoConfusion_fin P (n:=S n) fz fz).
+
+(* 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 ; *)
+(* noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl. *)
 
 Equations_nocomp NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop :=
 NoConfusion_vect P A 0 Vnil Vnil := P -> P ;
@@ -310,9 +290,9 @@ Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoCon
 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 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 ;
@@ -326,17 +306,16 @@ Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set :=
 
 Implicit Arguments Split [[X]].
 
-(* Equations_nocomp 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))). *)
+Equations_nocomp 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'.
 
-(* Extraction Inline split_obligation_1 split_obligation_2. *)
+Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))).
+Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))).
 
-(* Recursive Extraction split. *)
+Extraction Inline split_obligation_1 split_obligation_2.
+Recursive Extraction split.
 
-(* Eval compute in @split. *)
+Eval compute in @split.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 4b17235f28..c83b5d38dc 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -315,6 +315,40 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "
    It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by
    Goguen, McBride and McKinna. *)
 
+
+(** The NoConfusionPackage class provides a method for making progress on proving a property
+   [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given
+   [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where 
+   [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P].
+   This gives a general method for simplifying by discrimination or injectivity of constructors.
+   
+   Some actual instances are defined later in the file using the more primitive [discriminate] and
+   [injection] tactics on which we can always fall back.
+   *)
+  
+Class NoConfusionPackage (I : Type) := NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P.
+
+(** The [DependentEliminationPackage] provides the default dependent elimination principle to
+   be used by the [equations] resolver. It is especially useful to register the dependent elimination
+   principles for things in [Prop] which are not automatically generated. *)
+
+Class DependentEliminationPackage (A : Type) :=
+  elim_type : Type ; elim : elim_type.
+
+(** A higher-order tactic to apply a registered eliminator. *)
+
+Ltac elim_tac tac p := 
+  let ty := type of p in
+  let eliminator := eval simpl in (elim (A:=ty)) in
+    tac p eliminator.
+
+(** Specialization to do case analysis or induction. 
+   Note: the [equations] tactic tries [case] before [elim_case]: there is no need to register 
+   generated induction principles. *)
+
+Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p.
+Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.
+
 (** 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).
@@ -336,18 +370,6 @@ Proof. intros. apply X. apply inj_pair2. exact H. Defined.
 Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p).
 Proof. intros. rewrite (UIP_refl A). assumption. Defined.
 
-(** The NoConfusionPackage class provides a method for making progress on proving a property
-   [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given
-   [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where 
-   [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P].
-   This gives a general method for simplifying by discrimination or injectivity of constructors.
-   
-   Some actual instances are defined later in the file using the more primitive [discriminate] and
-   [injection] tactics on which we can always fall back.
-   *)
-  
-Class NoConfusionPackage (I : Type) := NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P.
-
 (** This hint database and the following tactic can be used with [autosimpl] to 
    unfold everything to [eq_rect]s. *)
 
@@ -439,13 +461,17 @@ Ltac reverse_local :=
     | _ => idtac
   end.
 
-(** Do as much as possible to apply a method, trying to get the arguments right. *)
+(** Do as much as possible to apply a method, trying to get the arguments right.
+   !!Unsafe!! We use [auto] for the [_nocomp] variant of [Equations], in which case some 
+   non-dependent arguments of the method can remain after [apply]. *)
 
-Ltac simpl_apply m := refine m.  (* || apply m || simpl ; apply m. *)
+Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m).
 
-Ltac try_intros m := unfold Datatypes.id ; refine m || apply m.  (* (repeat simpl_apply m || intro). *)
-(* Ltac try_intros m := intros ; unfold Datatypes.id ;  *)
-(*   repeat (apply m ; intro) ; let meth := fresh in pose(meth:=m). *)
+(** Hopefully the first branch suffices. *)
+
+Ltac try_intros m :=
+  solve [ intros ; unfold id ; refine m || apply m ] ||
+  solve [ unfold id ; simpl_intros m ].
 
 (** To solve a goal by inversion on a particular target. *)
 
@@ -478,14 +504,18 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac do_case p := case p ; clear p.
+Ltac do_case p := destruct p || elim_case p.
 
-Ltac case_last :=
-  match goal with
-    | [ p : ?x = ?x |- ?T ] => change (id T) ; revert p ; refine (simplification_K _ x _ _)
-    | [ p : ?x = ?y |- ?T ] => change (id T) ; revert p
-    | [ p : _ |- ?T ] => simpl in p ; change (id T) ; generalize_eqs p ; do_case p
-  end.
+Ltac idify := match goal with [ |- ?T ] => change (id T) end.
+
+Ltac case_last := idify ;
+  on_last_hyp ltac:(fun p => 
+    let ty := type of p in
+      match ty with
+        | ?x = ?x => revert p ; refine (simplification_K _ x _ _)
+        | ?x = ?y => revert p
+        | _ => simpl in p ; generalize_eqs p ; do_case p
+      end).
 
 Ltac nonrec_equations := 
   solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ]