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, 159 insertions, 0 deletions

diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v
new file mode 100644
index 0000000000..e37669bad0
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NOtherInd.v
@@ -0,0 +1,159 @@
+Require Export NDomain.
+Declare Module Export DomainModule : DomainSignature.
+
+Parameter O : N.
+Parameter S : N -> N.
+
+Notation "0" := O.
+
+Definition induction :=
+forall P : N -> Prop, pred_wd E P ->
+    P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n.
+
+Definition other_induction :=
+forall P : N -> Prop,
+  (forall n : N, n == 0 -> P n) ->
+  (forall n : N, P n -> forall m : N, m == S n -> P m) ->
+  forall n : N, P n.
+
+Theorem other_ind_implies_ind : other_induction -> induction.
+Proof.
+unfold induction, other_induction; intros OI P P_wd Base Step.
+apply OI; unfold pred_wd in P_wd.
+intros; now apply -> (P_wd 0).
+intros n Pn m EmSn; now apply -> (P_wd (S n)); [apply Step|].
+Qed.
+
+Theorem ind_implies_other_ind : induction -> other_induction.
+Proof.
+intros I P Base Step.
+set (Q := fun n => forall m, m == n -> P m).
+cut (forall n, Q n).
+unfold Q; intros H n; now apply (H n).
+apply I.
+unfold pred_wd, Q. intros x y Exy.
+split; intros H m Em; apply H; [now rewrite Exy | now rewrite <- Exy].
+exact Base.
+intros n Qn m EmSn; now apply Step with (n := n); [apply Qn |].
+Qed.
+
+(* This theorem is not really needed. It shows that if we have
+other_induction and we proved the base case and the induction step, we
+can in fact show that the predicate in question is well-defined, and
+therefore we can turn this other induction into the standard one. *)
+Theorem other_ind_implies_pred_wd :
+other_induction ->
+  forall P : N -> Prop,
+    (forall n : N, n == 0 -> P n) ->
+    (forall n : N, P n -> forall m : N, m == S n -> P m) ->
+    pred_wd E P.
+Proof.
+intros OI P Base Step; unfold pred_wd.
+intros x; pattern x; apply OI; clear x.
+(* Base case *)
+intros x H1 y H2.
+assert (y == 0); [rewrite <- H2; now rewrite H1|].
+assert (P x); [now apply Base|].
+assert (P y); [now apply Base|].
+split; now intro.
+(* Step *)
+intros x IH z H y H1.
+rewrite H in H1. symmetry in H1.
+split; (intro H2; eapply Step; [|apply H || apply H1]); now apply OI.
+Qed.
+
+Section Recursion.
+
+Variable A : Set.
+Variable EA : relation A.
+Hypothesis EA_symm : symmetric A EA.
+Hypothesis EA_trans : transitive A EA.
+
+Add Relation A EA
+ symmetry proved by EA_symm
+ transitivity proved by EA_trans
+as EA_rel.
+
+Lemma EA_neighbor : forall a a' : A, EA a a' -> EA a a.
+Proof.
+intros a a' EAaa'.
+apply EA_trans with (y := a'); [assumption | apply EA_symm; assumption].
+Qed.
+
+Parameter recursion : A -> (N -> A -> A) -> N -> A.
+
+Axiom recursion_0 :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a.
+
+Axiom recursion_S :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
+
+Theorem recursion_wd : induction ->
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
+      forall x x' : N, x == x' ->
+        EA (recursion a f x) (recursion a' f' x').
+Proof.
+intros I a a' Eaa' f f' f_wd f'_wd Eff'.
+apply ind_implies_other_ind in I.
+intro x; pattern x; apply I; clear x.
+intros x Ex0 x' Exx'.
+rewrite Ex0 in Exx'; symmetry in Exx'.
+(* apply recursion_0 in Ex0. produces
+Anomaly: type_of: this is not a well-typed term. Please report. *)
+assert (EA (recursion a f x) a).
+apply recursion_0. now apply EA_neighbor with (a' := a'). assumption.
+assert (EA a' (recursion a' f' x')).
+apply EA_symm. apply recursion_0. now apply EA_neighbor with (a' := a). assumption.
+apply EA_trans with (y := a). assumption.
+now apply EA_trans with (y := a').
+intros x IH y H y' H1.
+rewrite H in H1; symmetry in H1.
+assert (EA (recursion a f y) (f x (recursion a f x))).
+apply recursion_S. now apply EA_neighbor with (a' := a').
+assumption. now symmetry.
+assert (EA (f' x (recursion a' f' x)) (recursion a' f' y')).
+symmetry; apply recursion_S. now apply EA_neighbor with (a' := a). assumption.
+now symmetry.
+assert (EA (f x (recursion a f x)) (f' x (recursion a' f' x))).
+apply Eff'. reflexivity. apply IH. reflexivity.
+apply EA_trans with (y := (f x (recursion a f x))). assumption.
+apply EA_trans with (y := (f' x (recursion a' f' x))). assumption.
+assumption.
+Qed.
+
+Axiom recursion_0' :
+  forall (a : A) (f : N -> A -> A),
+    forall x : N, x == 0 -> recursion a f x = a.
+
+Axiom recursion_S' :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
+
+Theorem recursion_wd' : other_induction ->
+  forall a a' : A, EA a a -> EA a' a' -> EA a a' ->
+    forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
+      forall x x' : N, x == x' ->
+        EA (recursion a f x) (recursion a' f' x').
+Proof.
+intros I a a' a_wd a'_wd Eaa' f f' f_wd f'_wd Eff'.
+intro x; pattern x; apply I; clear x.
+intros x Ex0 x' Exx'. rewrite Ex0 in Exx'. symmetry in Exx'.
+replace (recursion a f x) with a. replace (recursion a' f' x') with a'.
+assumption. symmetry; now apply recursion_0'. symmetry; now apply recursion_0'.
+intros x IH y EySx y' Eyy'. rewrite EySx in Eyy'. symmetry in Eyy'.
+apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_S'.
+apply EA_trans with (y := (f' x (recursion a' f' x))).
+apply Eff'. reflexivity. now apply IH.
+symmetry; now apply recursion_S'.
+Qed.
+
+
+
+End Recursion.
+
+Implicit Arguments recursion [A].