diff options
author | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-11 18:46:35 +0000 |
---|---|---|
committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-11 18:46:35 +0000 |
commit | c86d78c0f18fb28f74bb6b192c03ebe73117cf03 (patch) | |
tree | 99294164215016607e4056e5730a2d6c91043dbf /contrib/setoid_ring/Ring_theory.v | |
parent | 70c88a5f6d7e1ef184d70512969a6221eec8d11e (diff) |
Changement dans le kernel :
- essai de suppression des dependances debiles. (echec)
- Application des patch debian.
Pour ring et field :
- introduciton de la function de sign et de puissance.
- Correction de certains bug.
- supression de ring_replace ....
Pour exact_no_check :
- ajout de la tactic : vm_cast_no_check (t)
qui remplace "exact_no_check (t<: type of Goal)"
(cette version forcais l'evaluation du cast dans le
pretypage).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/setoid_ring/Ring_theory.v')
-rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 101 |
1 files changed, 99 insertions, 2 deletions
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 2f7378eb0..dd63cf6d5 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -7,6 +7,9 @@ (************************************************************************) Require Import Setoid. +Require Import BinPos. +Require Import BinNat. + Set Implicit Arguments. Module RingSyntax. @@ -27,6 +30,71 @@ Reserved Notation "x == y" (at level 70, no associativity). End RingSyntax. Import RingSyntax. +Section Power. + Variable R:Type. + Variable rI : R. + Variable rmul : R -> R -> R. + Variable req : R -> R -> Prop. + Variable Rsth : Setoid_Theory R req. + Notation "x * y " := (rmul x y). + Notation "x == y" := (req x y). + + Hypothesis mul_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2. + Hypothesis mul_comm : forall x y, x * y == y * x. + Hypothesis mul_assoc : forall x y z, x * (y * z) == (x * y) * z. + Add Setoid R req Rsth as R_set_Power. + Add Morphism rmul : rmul_ext_Power. exact mul_ext. Qed. + + + Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow_pos x i in rmul p p + | xI i => let p := pow_pos x i in rmul (rmul x p) p + end. + + Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j. + Proof. + induction j;simpl. + rewrite IHj. + set (w:= x*pow_pos x j);unfold w at 2. + rewrite (mul_comm x (pow_pos x j));unfold w. + rewrite (mul_comm x (x * pow_pos x j * pow_pos x j)). + repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + apply (Seq_refl _ _ Rsth). + Qed. + + Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j. + Proof. + intro x;induction i;intros. + rewrite xI_succ_xO;rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. + simpl;repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi;rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc; + simpl. apply (Seq_refl _ _ Rsth). + Qed. + + Definition pow_N (x:R) (p:N) := + match p with + | N0 => rI + | Npos p => pow_pos x p + end. + + Definition id_phi_N (x:N) : N := x. + + Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n. + Proof. + intros; apply (Seq_refl _ _ Rsth). + Qed. + +End Power. + Section DEFINITIONS. Variable R : Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). @@ -126,6 +194,19 @@ Section DEFINITIONS. morph_opp : forall x, [-!x] == -[x]; morph_eq : forall x y, x?=!y = true -> [x] == [y] }. + + Section SIGN. + Variable get_sign : C -> option C. + Record sign_theory : Prop := mksign_th { + sign_spec : forall c c', get_sign c = Some c' -> [c] == - [c'] + }. + End SIGN. + + Definition get_sign_None (c:C) := @None C. + + Lemma get_sign_None_th : sign_theory get_sign_None. + Proof. constructor;intros;discriminate. Qed. + End MORPHISM. (** Identity is a morphism *) @@ -140,6 +221,20 @@ Section DEFINITIONS. try apply (Seq_refl _ _ Rsth);auto. Qed. + (** Specification of the power function *) + Section POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + + Record power_theory : Prop := mkpow_th { + rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) + }. + + End POWER. + + Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). + End DEFINITIONS. @@ -437,11 +532,12 @@ Qed. End ALMOST_RING. + Section AddRing. - Variable R : Type. +(* Variable R : Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable req : R -> R -> Prop. + Variable req : R -> R -> Prop. *) Inductive ring_kind : Type := | Abstract @@ -461,6 +557,7 @@ Inductive ring_kind : Type := (_ : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi). + End AddRing. |