diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/field/Field_Theory.v | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/field/Field_Theory.v')
-rw-r--r-- | contrib/field/Field_Theory.v | 53 |
1 files changed, 27 insertions, 26 deletions
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v index 2c954652..fff3c414 100644 --- a/contrib/field/Field_Theory.v +++ b/contrib/field/Field_Theory.v @@ -6,8 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Field_Theory.v 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: Field_Theory.v 8866 2006-05-28 16:21:04Z herbelin $ *) +Require Import List. Require Import Peano_dec. Require Import Ring. Require Import Field_Compl. @@ -21,8 +22,8 @@ Record Field_Theory : Type := Aopp : A -> A; Aeq : A -> A -> bool; Ainv : A -> A; - Aminus : field_rel_option A; - Adiv : field_rel_option A; + Aminus : option (A -> A -> A); + Adiv : option (A -> A -> A); RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq; Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}. @@ -66,10 +67,10 @@ Definition eqExprA := Eval compute in eqExprA_O. (**** Generation of the multiplier ****) -Fixpoint mult_of_list (e:listT ExprA) : ExprA := +Fixpoint mult_of_list (e:list ExprA) : ExprA := match e with - | nilT => EAone - | consT e1 l1 => EAmult e1 (mult_of_list l1) + | nil => EAone + | e1 :: l1 => EAmult e1 (mult_of_list l1) end. Section Theory_of_fields. @@ -191,7 +192,7 @@ Qed. (**** ExprA --> A ****) -Fixpoint interp_ExprA (lvar:listT (prodT AT nat)) (e:ExprA) {struct e} : +Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} : AT := match e with | EAzero => AzeroT @@ -257,7 +258,7 @@ Fixpoint assoc (e:ExprA) : ExprA := end. Lemma merge_mult_correct1 : - forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) = interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)). Proof. @@ -271,7 +272,7 @@ unfold merge_mult at 1 in |- *; fold merge_mult in |- *; Qed. Lemma merge_mult_correct : - forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2). Proof. simple induction e1; auto; intros. @@ -290,7 +291,7 @@ ring. Qed. Lemma assoc_mult_correct1 : - forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2:ExprA) (lvar:list (AT * nat)), AmultT (interp_ExprA lvar (assoc_mult e1)) (interp_ExprA lvar (assoc_mult e2)) = interp_ExprA lvar (assoc_mult (EAmult e1 e2)). @@ -302,7 +303,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct; Qed. Lemma assoc_mult_correct : - forall (e:ExprA) (lvar:listT (prodT AT nat)), + forall (e:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e. Proof. simple induction e; auto; intros. @@ -325,7 +326,7 @@ simpl in |- *; rewrite (H0 lvar); auto. Qed. Lemma merge_plus_correct1 : - forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) = interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)). Proof. @@ -339,7 +340,7 @@ unfold merge_plus at 1 in |- *; fold merge_plus in |- *; Qed. Lemma merge_plus_correct : - forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2). Proof. simple induction e1; auto; intros. @@ -358,7 +359,7 @@ ring. Qed. Lemma assoc_plus_correct : - forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2:ExprA) (lvar:list (AT * nat)), AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) = interp_ExprA lvar (assoc (EAplus e1 e2)). Proof. @@ -369,7 +370,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct; Qed. Lemma assoc_correct : - forall (e:ExprA) (lvar:listT (prodT AT nat)), + forall (e:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (assoc e) = interp_ExprA lvar e. Proof. simple induction e; auto; intros. @@ -448,7 +449,7 @@ Fixpoint distrib_main (e:ExprA) : ExprA := Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e). Lemma distrib_mult_right_correct : - forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (distrib_mult_right e1 e2) = AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2). Proof. @@ -458,7 +459,7 @@ rewrite AmultT_sym; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar); Qed. Lemma distrib_mult_left_correct : - forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (distrib_mult_left e1 e2) = AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2). Proof. @@ -480,7 +481,7 @@ rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym. Qed. Lemma distrib_correct : - forall (e:ExprA) (lvar:listT (prodT AT nat)), + forall (e:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (distrib e) = interp_ExprA lvar e. Proof. simple induction e; intros; auto. @@ -496,7 +497,7 @@ Qed. (**** Multiplication by the inverse product ****) Lemma mult_eq : - forall (e1 e2 a:ExprA) (lvar:listT (prodT AT nat)), + forall (e1 e2 a:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar a <> AzeroT -> interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) -> interp_ExprA lvar e1 = interp_ExprA lvar e2. @@ -520,7 +521,7 @@ Definition multiply (e:ExprA) : ExprA := end. Lemma multiply_aux_correct : - forall (a e:ExprA) (lvar:listT (prodT AT nat)), + forall (a e:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (multiply_aux a e) = AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). Proof. @@ -530,7 +531,7 @@ simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct; Qed. Lemma multiply_correct : - forall (e:ExprA) (lvar:listT (prodT AT nat)), + forall (e:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (multiply e) = interp_ExprA lvar e. Proof. simple induction e; simpl in |- *; auto. @@ -578,7 +579,7 @@ Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA := end. Lemma monom_remove_correct : - forall (e a:ExprA) (lvar:listT (prodT AT nat)), + forall (e a:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar a <> AzeroT -> interp_ExprA lvar (monom_remove a e) = AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). @@ -608,7 +609,7 @@ unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros; Qed. Lemma monom_simplif_rem_correct : - forall (a e:ExprA) (lvar:listT (prodT AT nat)), + forall (a e:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar a <> AzeroT -> interp_ExprA lvar (monom_simplif_rem a e) = AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). @@ -622,7 +623,7 @@ ring. Qed. Lemma monom_simplif_correct : - forall (e a:ExprA) (lvar:listT (prodT AT nat)), + forall (e a:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar a <> AzeroT -> interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e. Proof. @@ -633,7 +634,7 @@ simpl in |- *; trivial. Qed. Lemma inverse_correct : - forall (e a:ExprA) (lvar:listT (prodT AT nat)), + forall (e a:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar a <> AzeroT -> interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e. Proof. @@ -642,4 +643,4 @@ simpl in |- *; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto. unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto. Qed. -End Theory_of_fields.
\ No newline at end of file +End Theory_of_fields. |