Quick fix for restoring a left-to-right rewriting lemma compatible

with the guard condition + typo in the generation of _rec schemes in
the impredicative case.

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

3 files changed, 54 insertions, 32 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 058abb2b7..a9ced0a69 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -313,24 +313,28 @@ let build_l2r_rew_scheme dep env ind kind =
 	       rel_vect (nrealargs+4) nrealargs;
 	       rel_vect 4 nrealargs;
 	       [|mkRel 2|]])|]]) in
+  let main_body =
+    mkCase (ci,
+      my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
+      applied_sym_C 3,
+      [|mkVar varHC|]) in
   (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
   (my_it_mkLambda_or_LetIn_name realsign
   (mkNamedLambda varP
     (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s)
   (mkNamedLambda varHC applied_PC
   (mkNamedLambda varH (lift 2 applied_ind)
-  (mkCase (cieq,
-     mkLambda (Name varH,lift 3 applied_ind,
-       mkLambda (Anonymous,
-                 mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
-                 applied_PR)),
-     (mkApp (sym_involutive,
-       Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|])),
-     [|mkCase (ci,
-        my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
-        applied_sym_C 3,
-        [|mkVar varHC|])|])))))))
-
+  (if dep then (* we need a coercion *)
+     mkCase (cieq,
+       mkLambda (Name varH,lift 3 applied_ind,
+         mkLambda (Anonymous,
+                   mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
+                   applied_PR)),
+       mkApp (sym_involutive,
+         Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
+       [|main_body|])
+   else
+     main_body))))))
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for hypotheses associated  *)
@@ -529,18 +533,25 @@ let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
   (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
 
-(* Rewrite from left-to-right in conclusion and left-to-right in hypotheses *)
+(* Rewrite from left-to-right in conclusion and right-to-left in hypotheses *)
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun ind ->
-    (* For the non-dependent case, we have two possible choices: *)
-    (* - build_l2r_forward_rew_scheme is ok even for non symmetric *)
-    (*   equality like eq_true but it introduced a beta-expansion blocked *)
-    (*   by the match and thus, it makes the guard condition fragile *)
-    (*   Moreover, its standard form needs the inductive hypothesis not *)
-    (*   in last position what breaks the order of goals and need a fix! *)
-    (* - build_l2r_rew_scheme uses symmetry and is better for guard *)
-    (*   but it does not work for non-symmetric equalities *)
+    (* We cannot use the simply-proved build_l2r_forward_rew_scheme *)
+    (* because it is introduced a beta-expansion blocked by the match *)
+    (* and may thus block in turn guard condition *)
+    build_l2r_rew_scheme false (Global.env()) ind InType)
+
+(* Asymmetric rewrite in hypotheses *)
+let rew_asym_scheme_kind =
+  declare_individual_scheme_object "_rew_r_asym"
+  (fun ind ->
+    (* For the asymmetrical non-dependent case, we (currently) have only *)
+    (* build_l2r_forward_rew_scheme available, though it may break the   *)
+    (* guard condition due to the introduction of a beta-expansion       *)
+    (* blocked by a match.                                               *)
+    (* Moreover, its standard form needs the inductive hypothesis not    *)
+    (* in last position what breaks the order of goals and need a fix!   *)
     fix_l2r_forward_rew_scheme
       (build_l2r_forward_rew_scheme false (Global.env()) ind InType))
 
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index bf72245d6..a6ffe9e21 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -23,6 +23,7 @@ val rew_l2r_forward_dep_scheme_kind : individual scheme_kind
 val rew_r2l_forward_dep_scheme_kind : individual scheme_kind
 val rew_r2l_dep_scheme_kind : individual scheme_kind
 val rew_r2l_scheme_kind : individual scheme_kind
+val rew_asym_scheme_kind : individual scheme_kind
 
 val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
 val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8ad73c672..7db751372 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -176,13 +176,22 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
    eliminate lbeq on sort_of_gl. *)
 
 let find_elim hdcncl lft2rgt dep cls =
-  let scheme_name = match dep, lft2rgt, (cls = None) with
-    | false, true, true | false, false, false -> rew_l2r_scheme_kind
-    | false, false, true | false, true, false -> rew_r2l_scheme_kind
-    | true, true, true -> rew_l2r_dep_scheme_kind
-    | true, true, false -> rew_r2l_forward_dep_scheme_kind
-    | true, false, true -> rew_r2l_dep_scheme_kind
-    | true, false, false -> rew_l2r_forward_dep_scheme_kind
+  let inccl = (cls = None) in
+  let scheme_name = match dep, lft2rgt, inccl with
+    (* Non dependent case with symmetric equality *)
+    | false, Some true, true | false, Some false, false -> rew_l2r_scheme_kind
+    | false, Some false, true | false, Some true, false -> rew_r2l_scheme_kind
+    (* Dependent case with symmetric equality *)
+    | true, Some true, true -> rew_l2r_dep_scheme_kind
+    | true, Some true, false -> rew_r2l_forward_dep_scheme_kind
+    | true, Some false, true -> rew_r2l_dep_scheme_kind
+    | true, Some false, false -> rew_l2r_forward_dep_scheme_kind
+    (* Non dependent case with non-symmetric rewriting lemma *)
+    | false, None, true -> rew_r2l_scheme_kind
+    | false, None, false -> rew_asym_scheme_kind
+    (* Dependent case with non-symmetric rewriting lemma *)
+    | true, None, true -> rew_r2l_dep_scheme_kind
+    | true, None, false -> rew_l2r_forward_dep_scheme_kind
   in
   match kind_of_term hdcncl with
   | Ind ind -> mkConst (find_scheme scheme_name ind)
@@ -195,7 +204,8 @@ let type_of_clause gl = function
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars gl hdcncl =
   let dep = occur_term c (type_of_clause gl cls) in
   let elim = find_elim hdcncl lft2rgt dep cls in
-  general_elim_clause with_evars tac cls sigma c t l lft2rgt
+  general_elim_clause with_evars tac cls sigma c t l
+    (match lft2rgt with None -> false | Some b -> b)
     {elimindex = None; elimbody = (elim,NoBindings)} gl
 
 let adjust_rewriting_direction args lft2rgt =
@@ -204,11 +214,11 @@ let adjust_rewriting_direction args lft2rgt =
     (* more natural to see -> as the rewriting to the constant *)
     if not lft2rgt then
       error "Rewriting non-symmetric equality not allowed from right-to-left.";
-    not lft2rgt
+    None
   end
   else
     (* other equality *)
-    lft2rgt
+    Some lft2rgt
 
 let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 
@@ -1069,7 +1079,7 @@ let swapEquandsInConcl gls =
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim lbeq.eq false false None in
+  let eq_elim = find_elim lbeq.eq (Some false) false None in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)