Update on theories/Numbers. Natural numbers are mostly complete,

need to make NZOrdAxiomsSig a subtype of NAxiomsSig.


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

1 files changed, 21 insertions, 0 deletions

diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index fd9e9aa8b..6d3ad55a9 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -134,6 +134,23 @@ let y := fresh "y" in
 let H := fresh "H" in
   intros x y H; qiff x y H.
 
+Ltac solve_rel_wd :=
+unfold rel_wd, fun2_wd;
+let x1 := fresh "x" in
+let y1 := fresh "y" in
+let H1 := fresh "H" in
+let x2 := fresh "x" in
+let y2 := fresh "y" in
+let H2 := fresh "H" in
+  intros x1 y1 H1 x2 y2 H2;
+  qsetoid_rewrite H1;
+  qiff x2 y2 H2.
+(* The tactic solve_rel_wd is not very efficient because qsetoid_rewrite
+uses qiff to take the formula apart in order to make it quantifier-free,
+and then qiff is called again and takes the formula apart for the second
+time. It is better to analyze the formula once and generalize qiff to take
+a list of equalities that it has to rewrite. *)
+
 (* The following tactic uses solve_predicate_wd to solve the goals
 relating to well-defidedness that are produced by applying induction.
 We declare it to take the tactic that applies the induction theorem
@@ -205,6 +222,10 @@ Ltac rewrite_false P H :=
 setoid_replace P with False using relation iff;
 [| apply -> neg_false; apply H].
 
+Ltac rewrite_true P H :=
+setoid_replace P with True using relation iff;
+[| split; intro; [constructor | apply H]].
+
 Tactic Notation "symmetry" constr(Eq) :=
 lazymatch Eq with
 | ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff;