Added the directory theories/Numbers where axiomatizations and implementations (unary, binary, etc.) of different number classes (natural, integer, rational, real, complex, etc.) will be stored.Currently there are axiomatized natural numbers with two implementations and axiomatized integers. Modified Makefile accordingly but dod not include the new files in THEORIESVO yet.

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

1 files changed, 324 insertions, 0 deletions

diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
new file mode 100644
index 000000000..2fe547681
--- /dev/null
+++ b/theories/Numbers/NumPrelude.v
@@ -0,0 +1,324 @@
+Require Export Setoid.
+
+(*
+Contents:
+- Coercion from bool to Prop
+- An attempt to extend setoid rewrite to formulas with quantifiers
+- Extentional properties of predicates, relations and functions
+  (well-definedness and equality)
+- Relations on cartesian product
+- Some boolean functions on nat
+- Miscellaneous
+*)
+
+(** Coercion from bool to Prop *)
+
+Definition eq_bool := (@eq bool).
+
+Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
+Coercion eq_true : bool >-> Sortclass.
+
+Theorem neg_eq_true : forall x : bool, ~ x -> x = false.
+Proof.
+intros x H; destruct x; [elim (H is_eq_true) | reflexivity].
+Qed.
+
+(** An attempt to extend setoid rewrite to formulas with quantifiers *)
+
+(* The following algorithm was explained to me by Bruno Barras.
+
+In the future, we need to prove that some predicates are
+well-defined w.r.t. a setoid relation, i.e., we need to prove theorems
+of the form "forall x y, x == y -> (P x <-> P y)". The reason is that it
+makes sense to do induction only on predicates that satisfy this
+property. Ideally, such goal should be proved by saying "intros x y H;
+rewrite H; reflexivity".
+
+Now, such predicates P may contain quantifiers besides setoid
+morphisms. However, the tactic "rewrite" (which in this case stands
+for "setoid_rewrite") currently cannot handle universal quantifiers as
+well as lambda abstractions, which are part of the existential
+quantifier notation (recall that "exists x, P" stands for "ex (fun x
+=> p)").
+
+Therefore, to prove that P x <-> P y, we proceed as follows. Suppose
+that P x is C[forall z, Q[x,z]] where C is a context, i.e., a term
+with a hole. We assume that the hole of C does not occur inside
+another quantifier, i.e., that forall z, Q[x,z] is a top-level
+quantifier in P. The notation Q[x,z] means that the term Q contains
+free occurrences of variables x and z. We prove that forall z, Q[x,z]
+<-> forall z, Q[y,z]. To do this, we show that forall z, Q[x,z] <->
+Q[y,z]. After performing "intro z", this goal is handled recursively,
+until no more quantifiers are left in Q.
+
+After we obtain the goal
+
+H : x == y
+H1 : forall z, Q[x,z] <-> forall z, Q[y,z]
+=================================
+C[forall z, Q[x,z]] <-> C[forall z, Q[y,z]]
+
+we say "rewrite H1". Repeating this for other quantifier subformulas
+in P, we make them all identical in P x and P y. After that, saying
+"rewrite H" solves the goal.
+
+To implement this algorithm, we need the following theorems:
+
+Theorem forall_morphism :
+  forall (A : Set) (P Q : A -> Prop),
+    (forall x : A, P x <-> Q x) -> ((forall x : A, P x) <-> (forall x : A, Q x)).
+
+Theorem exists_morphism :
+  forall (A : Set) (P Q : A -> Prop),
+    (forall x : A, P x <-> Q x) -> (ex P <-> ex Q)
+
+Below, we obtain them by registering the universal and existential
+quantifiers as setoid morphisms, though they can be proved without any
+reference to setoids. Ideally, registering quantifiers as morphisms
+should take care of setoid rewriting in the presence of quantifiers,
+but as described above, this is currently not so, and we have to
+handle quantifiers manually.
+
+The job of deriving P x <-> P y from x == y is done by the tactic
+qmorphism x y below. *)
+
+Section Quantifiers.
+
+Variable A : Set.
+
+Definition predicate := A -> Prop.
+
+Definition equiv_predicate : relation predicate :=
+  fun (P1 P2 : predicate) => forall x : A, P1 x <-> P2 x.
+
+Theorem equiv_predicate_refl : reflexive predicate equiv_predicate.
+Proof.
+unfold reflexive, equiv_predicate. reflexivity.
+Qed.
+
+Theorem equiv_predicate_symm : symmetric predicate equiv_predicate.
+Proof.
+firstorder.
+Qed.
+
+Theorem equiv_predicate_trans : transitive predicate equiv_predicate.
+Proof.
+firstorder.
+Qed.
+
+Add Relation predicate equiv_predicate
+  reflexivity proved by equiv_predicate_refl
+  symmetry proved by equiv_predicate_symm
+  transitivity proved by equiv_predicate_trans
+as equiv_predicate_rel.
+
+Add Morphism (@ex A)
+  with signature equiv_predicate ==> iff
+  as exists_morphism.
+Proof.
+firstorder.
+Qed.
+
+Add Morphism (fun P : predicate => forall x : A, P x)
+  with signature equiv_predicate ==> iff
+  as forall_morphism.
+Proof.
+firstorder.
+Qed.
+
+End Quantifiers.
+
+(* replace x by y in t *)
+Ltac repl x y t :=
+match t with
+| context C [x] => let t' := (context C [y]) in repl x y t'
+| _ => t
+end.
+
+Ltac qmorphism x y :=
+lazymatch goal with
+| |- ?P <-> ?P => reflexivity
+| |- context [ex ?P] =>
+  match P with
+  | context [x] =>
+    let P' := repl x y P in
+      setoid_replace (ex P) with (ex P') using relation iff;
+      [qmorphism x y |
+       apply exists_morphism; unfold equiv_predicate; intros; qmorphism x y]
+  end
+| |- context [forall z, @?P z] =>
+  match P with
+  | context [x] =>
+    let P' := repl x y P in
+      setoid_replace (forall z, P z) with (forall z, P' z) using relation iff;
+      [qmorphism x y |
+       apply forall_morphism; unfold equiv_predicate; intros; qmorphism x y]
+  end
+| _ => setoid_replace x with y; [reflexivity | assumption]
+end.
+
+(** Extentional properties of predicates, relations and functions *)
+
+Section ExtensionalProperties.
+
+Variables A B C : Set.
+Variable EA : relation A.
+Variable EB : relation B.
+Variable EC : relation C.
+
+(* "wd" stands for "well-defined" *)
+
+Definition fun_wd (f : A -> B) := forall x y : A, EA x y -> EB (f x) (f y).
+
+Definition fun2_wd (f : A -> B -> C) :=
+  forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f x' y').
+
+Definition pred_wd (P : predicate A) :=
+  forall x y, EA x y -> (P x <-> P y).
+
+Definition rel_wd (R : relation A) :=
+  forall x x', EA x x' -> forall y y', EA y y' -> (R x y <-> R x' y').
+
+Definition eq_fun : relation (A -> B) :=
+  fun f f' => forall x x' : A, EA x x' -> EB (f x) (f' x').
+
+(* Note that reflexivity of eq_fun means that every function
+is well-defined w.r.t. EA and EB, i.e.,
+forall x x' : A, EA x x' -> EB (f x) (f x') *)
+
+Definition eq_fun2 (f f' : A -> B -> C) :=
+  forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f' x' y').
+
+End ExtensionalProperties.
+
+Implicit Arguments fun_wd [A B].
+Implicit Arguments fun2_wd [A B C].
+Implicit Arguments eq_fun [A B].
+Implicit Arguments eq_fun2 [A B C].
+Implicit Arguments pred_wd [A].
+Implicit Arguments rel_wd [A].
+
+(** Relations on cartesian product. Used in MiscFunct for defining
+functions whose domain is a product of sets by primitive recursion *)
+
+Section RelationOnProduct.
+
+Variables A B : Set.
+Variable EA : relation A.
+Variable EB : relation B.
+
+Hypothesis EA_equiv : equiv A EA.
+Hypothesis EB_equiv : equiv B EB.
+
+Definition prod_rel : relation (A * B) :=
+  fun p1 p2 => EA (fst p1) (fst p2) /\ EB (snd p1) (snd p2).
+
+Lemma prod_rel_refl : reflexive (A * B) prod_rel.
+Proof.
+unfold reflexive, prod_rel.
+destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
+Qed.
+
+Lemma prod_rel_symm : symmetric (A * B) prod_rel.
+Proof.
+unfold symmetric, prod_rel.
+destruct x; destruct y;
+split; [apply (proj2 (proj2 EA_equiv)) | apply (proj2 (proj2 EB_equiv))]; simpl in *; tauto.
+Qed.
+
+Lemma prod_rel_trans : transitive (A * B) prod_rel.
+Proof.
+unfold transitive, prod_rel.
+destruct x; destruct y; destruct z; simpl.
+intros; split; [apply (proj1 (proj2 EA_equiv)) with (y := a0) |
+apply (proj1 (proj2 EB_equiv)) with (y := b0)]; tauto.
+Qed.
+
+Theorem prod_rel_equiv : equiv (A * B) prod_rel.
+Proof.
+unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]].
+Qed.
+
+End RelationOnProduct.
+
+Implicit Arguments prod_rel [A B].
+Implicit Arguments prod_rel_equiv [A B].
+
+(** Some boolean functions on nat. Their analogs are available in the
+standard library; however, we provide simpler definitions. Used in
+defining  implementations of natural numbers. *)
+
+Fixpoint eq_nat_bool (x y : nat) {struct x} : bool :=
+match x, y with
+| 0, 0 => true
+| S x', S y' => eq_nat_bool x' y'
+| _, _ => false
+end.
+
+Theorem eq_nat_bool_implies_eq : forall x y, eq_nat_bool x y -> x = y.
+Proof.
+induction x; destruct y; simpl; intro H; try (reflexivity || inversion H).
+apply IHx in H; now rewrite H.
+Qed.
+
+Theorem eq_nat_bool_refl : forall x, eq_nat_bool x x.
+Proof.
+induction x; now simpl.
+Qed.
+
+(* The boolean less function can be defined as
+fun n m => proj1_sig (nat_lt_ge_bool n m)
+using the standard library.
+However, this definitionseems too complex. First, there are many
+functions involved: nat_lt_ge_bool is defined (in Coq.Arith.Bool_nat)
+using bool_of_sumbool and
+lt_ge_dec : forall x y : nat, {x < y} + {x >= y},
+where the latter function is defined using sumbool_not and
+le_lt_dec : forall n m : nat, {n <= m} + {m < n}.
+Second, this definition is not the most efficient, especially since
+le_lt_dec is proved using tactics, not by giving the explicit proof term. *)
+
+Fixpoint lt_bool (n m : nat) {struct n} : bool :=
+match n, m with
+| 0, S _ => true
+| S n', S m' => lt_bool n' m'
+| _, 0 => false
+end.
+
+(* The following properties are used both in Peano.v and in MPeano.v *)
+
+Theorem lt_bool_0 : forall x, ~ (lt_bool x 0).
+Proof.
+destruct x as [|x]; simpl; now intro.
+Qed.
+
+Theorem lt_bool_S : forall x y, lt_bool x (S y) <-> lt_bool x y \/ x = y.
+Proof.
+induction x as [| x IH]; destruct y as [| y]; simpl.
+split; [now right | now intro].
+split; [now left | now intro].
+split; [intro H; false_hyp H lt_bool_0 |
+intro H; destruct H as [H | H]; now auto].
+assert (H : x = y <-> S x = S y); [split; auto|].
+rewrite <- H; apply IH.
+Qed.
+
+(** Miscellaneous *)
+
+Definition less_than (x : comparison) : bool :=
+match x with Lt => true | _ => false end.
+
+Definition LE_Set : forall A : Set, relation A := (@eq).
+
+Lemma eq_equiv : forall A : Set, equiv A (LE_Set A).
+Proof.
+intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive.
+repeat split; [exact (@trans_eq A) | exact (@sym_eq A)].
+(* It is interesting how the tactic split proves reflexivity *)
+Qed.
+
+Add Relation (fun A : Set => A) LE_Set
+ reflexivity proved by (fun A : Set => (proj1 (eq_equiv A)))
+ symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A))))
+ transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A))))
+as EA_rel.