From 13719588ca7e06d8e86fa81b33321a4fa626563f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 23 Nov 2008 08:34:29 +0000
Subject: Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b
 (if ever necessary).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml       | 15 +++++++++++++--
 theories/Init/Datatypes.v | 20 ++++++++++++++++++--
 2 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 641e274af7..e3914b8c51 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -105,6 +105,15 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c l with_evars gl hdcncl
       error ("Cannot find rewrite principle "^rwr_thm^".")
   in general_elim_clause with_evars cls sigma c l (elim,NoBindings) gl
 
+let adjust_rewriting_direction args lft2rgt =
+  if List.length args = 1 then
+    (* equality to a constant, like in eq_true *)
+    (* more natural to see -> as the rewriting to the constant *)
+    not lft2rgt
+  else
+    (* other equality *)
+    lft2rgt
+
 let leibniz_eq = Lazy.lazy_from_fun build_coq_eq
 
 let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_bindings) with_evars gl =
@@ -117,13 +126,15 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_
     let ctype = get_type_of env sigma c' in 
     let rels, t = decompose_prod (whd_betaiotazeta ctype) in
       match match_with_equality_type t with
-      | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *)
+      | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *)
+	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 	  leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl
       | None ->
 	  let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in
 	  let _,t' = splay_prod env' sigma t in (* Search for underlying eq *)
 	    match match_with_equality_type t' with
-	    | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *)
+	    | Some (hdcncl,args) -> (* Maybe a setoid relation with eq inside *)
+		let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		if l = NoBindings && !is_applied_setoid_relation t then
 		  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
 		else
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 45228073a0..beda128af9 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -72,9 +72,25 @@ Hint Resolve andb_true_intro: bool v62.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
-(** Technical lemma: identify -> rewriting on eq_true with <- rewriting *)
+(** Additional rewriting lemmas about [eq_true] *)
 
-Definition eq_true_ind_r := eq_true_ind.
+Lemma eq_true_ind_r :
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true.
+Proof.
+  intros P b H H0; destruct H0 in H; assumption.
+Defined.
+
+Lemma eq_true_rec_r :
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true.
+Proof.
+  intros P b H H0; destruct H0 in H; assumption.
+Defined.
+
+Lemma eq_true_rect_r :
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true.
+Proof.
+  intros P b H H0; destruct H0 in H; assumption.
+Defined.
 
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.
-- 
cgit v1.2.3