From 3d6f36702e8d5e70963a7e0fa14ad759b85950cc Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 25 Oct 2006 11:30:36 +0000 Subject: conflit de nom (Field_theory) modulo la casse git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9273 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 86 ++--- .depend.coq | 10 +- Makefile | 4 +- contrib/field/Field_Compl.v | 38 --- contrib/field/Field_Theory.v | 650 ------------------------------------- contrib/field/LegacyField.v | 8 +- contrib/field/LegacyField_Compl.v | 38 +++ contrib/field/LegacyField_Theory.v | 650 +++++++++++++++++++++++++++++++++++++ contrib/field/field.ml4 | 2 +- 9 files changed, 749 insertions(+), 737 deletions(-) delete mode 100644 contrib/field/Field_Compl.v delete mode 100644 contrib/field/Field_Theory.v create mode 100644 contrib/field/LegacyField_Compl.v create mode 100644 contrib/field/LegacyField_Theory.v diff --git a/.depend b/.depend index 18778724dc..25db9cebe1 100644 --- a/.depend +++ b/.depend @@ -292,7 +292,7 @@ tactics/equality.cmi: kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi proofs/tacexpr.cmo \ kernel/sign.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ pretyping/pattern.cmi kernel/names.cmi tactics/hipattern.cmi \ - pretyping/evd.cmi kernel/environ.cmi + interp/genarg.cmi pretyping/evd.cmi kernel/environ.cmi tactics/evar_tactics.cmi: kernel/term.cmi proofs/tacmach.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi kernel/names.cmi tactics/extraargs.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ @@ -590,8 +590,8 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ config/coq_config.cmx toplevel/cerrors.cmx ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi -ide/find_phrase.cmo: ide/ideutils.cmi -ide/find_phrase.cmx: ide/ideutils.cmx +ide/find_phrase.cmo: ide/preferences.cmi ide/ideutils.cmi +ide/find_phrase.cmx: ide/preferences.cmx ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi ide/highlight.cmx: ide/ideutils.cmx ide/ideutils.cmo: ide/utf8_convert.cmo lib/system.cmi ide/preferences.cmi \ @@ -695,13 +695,13 @@ interp/syntax_def.cmx: lib/util.cmx interp/topconstr.cmx library/summary.cmx \ kernel/names.cmx library/nameops.cmx library/libobject.cmx \ library/libnames.cmx library/lib.cmx interp/syntax_def.cmi interp/topconstr.cmo: lib/util.cmi kernel/term.cmi pretyping/rawterm.cmi \ - lib/pp.cmi kernel/names.cmi library/nameops.cmi kernel/mod_subst.cmi \ - library/libnames.cmi pretyping/evd.cmi lib/dyn.cmi pretyping/detyping.cmi \ - lib/bigint.cmi interp/topconstr.cmi + lib/pp.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ + kernel/mod_subst.cmi library/libnames.cmi pretyping/evd.cmi lib/dyn.cmi \ + pretyping/detyping.cmi lib/bigint.cmi interp/topconstr.cmi interp/topconstr.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ - lib/pp.cmx kernel/names.cmx library/nameops.cmx kernel/mod_subst.cmx \ - library/libnames.cmx pretyping/evd.cmx lib/dyn.cmx pretyping/detyping.cmx \ - lib/bigint.cmx interp/topconstr.cmi + lib/pp.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ + kernel/mod_subst.cmx library/libnames.cmx pretyping/evd.cmx lib/dyn.cmx \ + pretyping/detyping.cmx lib/bigint.cmx interp/topconstr.cmi kernel/cbytecodes.cmo: kernel/term.cmi kernel/names.cmi kernel/cbytecodes.cmi kernel/cbytecodes.cmx: kernel/term.cmx kernel/names.cmx kernel/cbytecodes.cmi kernel/cbytegen.cmo: lib/util.cmi kernel/term.cmi kernel/pre_env.cmi \ @@ -764,10 +764,12 @@ kernel/indtypes.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \ kernel/entries.cmx kernel/declarations.cmx kernel/indtypes.cmi kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \ kernel/term.cmi kernel/sign.cmi kernel/reduction.cmi kernel/names.cmi \ - kernel/environ.cmi kernel/declarations.cmi kernel/inductive.cmi + kernel/environ.cmi kernel/declarations.cmi kernel/closure.cmi \ + kernel/inductive.cmi kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \ kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \ - kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi + kernel/environ.cmx kernel/declarations.cmx kernel/closure.cmx \ + kernel/inductive.cmi kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \ kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ @@ -1317,7 +1319,7 @@ pretyping/cases.cmo: lib/util.cmi kernel/typeops.cmi kernel/type_errors.cmi \ library/nameops.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \ library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ pretyping/evarconv.cmi kernel/environ.cmi kernel/declarations.cmi \ - pretyping/coercion.cmi pretyping/cases.cmi + pretyping/coercion.cmi kernel/closure.cmi pretyping/cases.cmi pretyping/cases.cmx: lib/util.cmx kernel/typeops.cmx kernel/type_errors.cmx \ pretyping/termops.cmx kernel/term.cmx kernel/sign.cmx \ pretyping/retyping.cmx pretyping/reductionops.cmx pretyping/rawterm.cmx \ @@ -1325,7 +1327,7 @@ pretyping/cases.cmx: lib/util.cmx kernel/typeops.cmx kernel/type_errors.cmx \ library/nameops.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \ library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ pretyping/evarconv.cmx kernel/environ.cmx kernel/declarations.cmx \ - pretyping/coercion.cmx pretyping/cases.cmi + pretyping/coercion.cmx kernel/closure.cmx pretyping/cases.cmi pretyping/cbv.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi pretyping/evd.cmi kernel/esubst.cmi kernel/environ.cmi \ kernel/conv_oracle.cmi kernel/closure.cmi pretyping/cbv.cmi @@ -1366,18 +1368,18 @@ pretyping/clenv.cmx: lib/util.cmx pretyping/unification.cmx \ kernel/mod_subst.cmx library/global.cmx pretyping/evd.cmx \ pretyping/evarutil.cmx kernel/environ.cmx pretyping/coercion.cmx \ pretyping/clenv.cmi -pretyping/coercion.cmo: lib/util.cmi kernel/typeops.cmi kernel/term.cmi \ - pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ - pretyping/recordops.cmi pretyping/rawterm.cmi \ - pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \ - pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \ - kernel/environ.cmi pretyping/classops.cmi pretyping/coercion.cmi -pretyping/coercion.cmx: lib/util.cmx kernel/typeops.cmx kernel/term.cmx \ - pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \ - pretyping/recordops.cmx pretyping/rawterm.cmx \ - pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \ - pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \ - kernel/environ.cmx pretyping/classops.cmx pretyping/coercion.cmi +pretyping/coercion.cmo: lib/util.cmi kernel/typeops.cmi pretyping/termops.cmi \ + kernel/term.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \ + kernel/reduction.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \ + pretyping/pretype_errors.cmi kernel/names.cmi pretyping/evd.cmi \ + pretyping/evarutil.cmi pretyping/evarconv.cmi kernel/environ.cmi \ + pretyping/classops.cmi pretyping/coercion.cmi +pretyping/coercion.cmx: lib/util.cmx kernel/typeops.cmx pretyping/termops.cmx \ + kernel/term.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \ + kernel/reduction.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \ + pretyping/pretype_errors.cmx kernel/names.cmx pretyping/evd.cmx \ + pretyping/evarutil.cmx pretyping/evarconv.cmx kernel/environ.cmx \ + pretyping/classops.cmx pretyping/coercion.cmi pretyping/detyping.cmo: lib/util.cmi kernel/univ.cmi pretyping/termops.cmi \ kernel/term.cmi kernel/sign.cmi pretyping/rawterm.cmi lib/pp.cmi \ lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ @@ -1785,13 +1787,15 @@ tactics/btermdn.cmo: tactics/termdn.cmi kernel/term.cmi pretyping/pattern.cmi \ tactics/btermdn.cmx: tactics/termdn.cmx kernel/term.cmx pretyping/pattern.cmx \ library/libnames.cmx tactics/dn.cmx tactics/btermdn.cmi tactics/contradiction.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ - tactics/tacticals.cmi proofs/tacmach.cmi pretyping/reductionops.cmi \ - pretyping/rawterm.cmi proofs/proof_type.cmi tactics/hipattern.cmi \ - interp/coqlib.cmi tactics/contradiction.cmi + tactics/tacticals.cmi proofs/tacmach.cmi pretyping/retyping.cmi \ + pretyping/reductionops.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ + tactics/hipattern.cmi pretyping/evd.cmi kernel/environ.cmi \ + interp/coqlib.cmi pretyping/coercion.cmi tactics/contradiction.cmi tactics/contradiction.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ - tactics/tacticals.cmx proofs/tacmach.cmx pretyping/reductionops.cmx \ - pretyping/rawterm.cmx proofs/proof_type.cmx tactics/hipattern.cmx \ - interp/coqlib.cmx tactics/contradiction.cmi + tactics/tacticals.cmx proofs/tacmach.cmx pretyping/retyping.cmx \ + pretyping/reductionops.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ + tactics/hipattern.cmx pretyping/evd.cmx kernel/environ.cmx \ + interp/coqlib.cmx pretyping/coercion.cmx tactics/contradiction.cmi tactics/decl_interp.cmo: lib/util.cmi interp/topconstr.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \ tactics/tacinterp.cmi pretyping/rawterm.cmi pretyping/pretyping.cmi \ @@ -3104,6 +3108,14 @@ contrib/funind/invfun.cmx: toplevel/vernacentries.cmx lib/util.cmx \ kernel/entries.cmx kernel/declarations.cmx library/decl_kinds.cmx \ interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \ toplevel/cerrors.cmx +contrib/funind/merge.cmo: lib/util.cmi kernel/term.cmi \ + contrib/funind/tacinvutils.cmi tactics/tacinterp.cmi kernel/names.cmi \ + pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \ + pretyping/evd.cmi kernel/environ.cmi kernel/declarations.cmi +contrib/funind/merge.cmx: lib/util.cmx kernel/term.cmx \ + contrib/funind/tacinvutils.cmx tactics/tacinterp.cmx kernel/names.cmx \ + pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \ + pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ pretyping/inductiveops.cmi contrib/funind/indfun_common.cmi \ @@ -3780,14 +3792,14 @@ contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ toplevel/cerrors.cmx contrib/subtac/subtac.cmi contrib/subtac/subtac_obligations.cmo: lib/util.cmi kernel/term.cmi \ library/summary.cmi contrib/subtac/subtac_utils.cmi lib/pp.cmi \ - kernel/names.cmi library/libobject.cmi library/libnames.cmi \ - kernel/entries.cmi library/declare.cmi library/decl_kinds.cmo \ - toplevel/command.cmi + lib/options.cmi kernel/names.cmi library/libobject.cmi \ + library/libnames.cmi kernel/entries.cmi library/declare.cmi \ + library/decl_kinds.cmo toplevel/command.cmi contrib/subtac/subtac_obligations.cmx: lib/util.cmx kernel/term.cmx \ library/summary.cmx contrib/subtac/subtac_utils.cmx lib/pp.cmx \ - kernel/names.cmx library/libobject.cmx library/libnames.cmx \ - kernel/entries.cmx library/declare.cmx library/decl_kinds.cmx \ - toplevel/command.cmx + lib/options.cmx kernel/names.cmx library/libobject.cmx \ + library/libnames.cmx kernel/entries.cmx library/declare.cmx \ + library/decl_kinds.cmx toplevel/command.cmx contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \ kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \ kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \ diff --git a/.depend.coq b/.depend.coq index e4ec4b5ce3..3fe8e475c2 100644 --- a/.depend.coq +++ b/.depend.coq @@ -348,10 +348,10 @@ contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo -contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v theories/Lists/List.vo -contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Lists/List.vo theories/Arith/Peano_dec.vo contrib/ring/LegacyRing.vo contrib/field/Field_Compl.vo -contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v theories/Lists/List.vo contrib/ring/LegacyRing.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo -contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo +contrib/field/LegacyField_Compl.vo: contrib/field/LegacyField_Compl.v theories/Lists/List.vo +contrib/field/LegacyField_Theory.vo: contrib/field/LegacyField_Theory.v theories/Lists/List.vo theories/Arith/Peano_dec.vo contrib/ring/LegacyRing.vo contrib/field/LegacyField_Compl.vo +contrib/field/LegacyField_Tactic.vo: contrib/field/LegacyField_Tactic.v theories/Lists/List.vo contrib/ring/LegacyRing.vo contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo +contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo contrib/field/LegacyField_Tactic.vo contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo @@ -371,6 +371,6 @@ contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo -contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo +contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v theories/Reals/Raxioms.vo theories/Reals/Rdefinitions.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/Field.vo diff --git a/Makefile b/Makefile index c03681aeee..831f703337 100644 --- a/Makefile +++ b/Makefile @@ -1048,8 +1048,8 @@ RINGVO=\ contrib/ring/Setoid_ring.vo contrib/ring/Setoid_ring_theory.vo FIELDVO=\ - contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo \ - contrib/field/Field_Tactic.vo contrib/field/LegacyField.vo + contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo \ + contrib/field/LegacyField_Tactic.vo contrib/field/LegacyField.vo NEWRINGVO=\ contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_theory.vo \ diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v deleted file mode 100644 index 746e7c9976..0000000000 --- a/contrib/field/Field_Compl.v +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* e2}) - (lst:list (prod A B)) {struct lst} : - B -> A -> A := - fun (key:B) (default:A) => - match lst with - | nil => default - | (v,e) :: l => - match eq_dec e key with - | left _ => v - | right _ => assoc_2nd_rec A B eq_dec l key default - end - end). - -Definition mem := - (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) - (a:A) (l:list A) {struct l} : bool := - match l with - | nil => false - | a1 :: l1 => - match eq_dec a a1 with - | left _ => true - | right _ => mem A eq_dec a l1 - end - end). diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v deleted file mode 100644 index a54c54a0bd..0000000000 --- a/contrib/field/Field_Theory.v +++ /dev/null @@ -1,650 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A -> A; - Amult : A -> A -> A; - Aone : A; - Azero : A; - Aopp : A -> A; - Aeq : A -> A -> bool; - Ainv : A -> 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}. - -(* The reflexion structure *) -Inductive ExprA : Set := - | EAzero : ExprA - | EAone : ExprA - | EAplus : ExprA -> ExprA -> ExprA - | EAmult : ExprA -> ExprA -> ExprA - | EAopp : ExprA -> ExprA - | EAinv : ExprA -> ExprA - | EAvar : nat -> ExprA. - -(**** Decidability of equality ****) - -Lemma eqExprA_O : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}. -Proof. - double induction e1 e2; try intros; - try (left; reflexivity) || (try (right; discriminate)). - elim (H1 e0); intro y; elim (H2 e); intro y0; - try - (left; rewrite y; rewrite y0; auto) || - (right; red in |- *; intro; inversion H3; auto). - elim (H1 e0); intro y; elim (H2 e); intro y0; - try - (left; rewrite y; rewrite y0; auto) || - (right; red in |- *; intro; inversion H3; auto). - elim (H0 e); intro y. - left; rewrite y; auto. - right; red in |- *; intro; inversion H1; auto. - elim (H0 e); intro y. - left; rewrite y; auto. - right; red in |- *; intro; inversion H1; auto. - elim (eq_nat_dec n n0); intro y. - left; rewrite y; auto. - right; red in |- *; intro; inversion H; auto. -Defined. - -Definition eq_nat_dec := Eval compute in eq_nat_dec. -Definition eqExprA := Eval compute in eqExprA_O. - -(**** Generation of the multiplier ****) - -Fixpoint mult_of_list (e:list ExprA) : ExprA := - match e with - | nil => EAone - | e1 :: l1 => EAmult e1 (mult_of_list l1) - end. - -Section Theory_of_fields. - -Variable T : Field_Theory. - -Let AT := A T. -Let AplusT := Aplus T. -Let AmultT := Amult T. -Let AoneT := Aone T. -Let AzeroT := Azero T. -Let AoppT := Aopp T. -Let AeqT := Aeq T. -Let AinvT := Ainv T. -Let RTT := RT T. -Let Th_inv_defT := Th_inv_def T. - -Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) ( - Azero T) (Aopp T) (Aeq T) (RT T). - -Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT. - -(***************************) -(* Lemmas to be used *) -(***************************) - -Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1. -Proof. - intros; legacy ring. -Qed. - -Notation AplusT_sym := AplusT_comm (only parsing). (* Compatibility *) - -Lemma AplusT_assoc : - forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1. -Proof. - intros; legacy ring. -Qed. - -Notation AmultT_sym := AmultT_comm (only parsing). (* Compatibility *) - -Lemma AmultT_assoc : - forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r. -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r. -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT. -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_AplusT_distr : - forall r1 r2 r3:AT, - AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2. -Proof. - intros; transitivity (AplusT (AplusT (AoppT r) r) r1). - legacy ring. - transitivity (AplusT (AplusT (AoppT r) r) r2). - repeat rewrite AplusT_assoc; rewrite <- H; reflexivity. - legacy ring. -Qed. - -Lemma r_AmultT_mult : - forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2. -Proof. - intros; transitivity (AmultT (AmultT (AinvT r) r) r1). - rewrite Th_inv_defT; [ symmetry in |- *; apply AmultT_1l; auto | auto ]. - transitivity (AmultT (AmultT (AinvT r) r) r2). - repeat rewrite AmultT_assoc; rewrite H; trivial. - rewrite Th_inv_defT; [ apply AmultT_1l; auto | auto ]. -Qed. - -Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT. -Proof. - intro; legacy ring. -Qed. - -Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT. -Proof. - intro; legacy ring. -Qed. - -Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r. -Proof. - intro; legacy ring. -Qed. - -Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT. -Proof. - intros; rewrite AmultT_comm; apply Th_inv_defT; auto. -Qed. - -Lemma Rmult_neq_0_reg : - forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT. -Proof. - intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; legacy ring. -Qed. - -(************************) -(* Interpretation *) -(************************) - -(**** ExprA --> A ****) - -Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} : - AT := - match e with - | EAzero => AzeroT - | EAone => AoneT - | EAplus e1 e2 => AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2) - | EAmult e1 e2 => AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2) - | EAopp e => Aopp T (interp_ExprA lvar e) - | EAinv e => Ainv T (interp_ExprA lvar e) - | EAvar n => assoc_2nd AT nat eq_nat_dec lvar n AzeroT - end. - -(************************) -(* Simplification *) -(************************) - -(**** Associativity ****) - -Definition merge_mult := - (fix merge_mult (e1:ExprA) : ExprA -> ExprA := - fun e2:ExprA => - match e1 with - | EAmult t1 t2 => - match t2 with - | EAmult t2 t3 => EAmult t1 (EAmult t2 (merge_mult t3 e2)) - | _ => EAmult t1 (EAmult t2 e2) - end - | _ => EAmult e1 e2 - end). - -Fixpoint assoc_mult (e:ExprA) : ExprA := - match e with - | EAmult e1 e3 => - match e1 with - | EAmult e1 e2 => - merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2)) - (assoc_mult e3) - | _ => EAmult e1 (assoc_mult e3) - end - | _ => e - end. - -Definition merge_plus := - (fix merge_plus (e1:ExprA) : ExprA -> ExprA := - fun e2:ExprA => - match e1 with - | EAplus t1 t2 => - match t2 with - | EAplus t2 t3 => EAplus t1 (EAplus t2 (merge_plus t3 e2)) - | _ => EAplus t1 (EAplus t2 e2) - end - | _ => EAplus e1 e2 - end). - -Fixpoint assoc (e:ExprA) : ExprA := - match e with - | EAplus e1 e3 => - match e1 with - | EAplus e1 e2 => - merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3) - | _ => EAplus (assoc_mult e1) (assoc e3) - end - | _ => assoc_mult e - end. - -Lemma merge_mult_correct1 : - 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. -intros e1 e2; generalize e1; generalize e2; clear e1 e2. -simple induction e2; auto; intros. -unfold merge_mult at 1 in |- *; fold merge_mult in |- *; - unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; - fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; - fold interp_ExprA in |- *; auto. -Qed. - -Lemma merge_mult_correct : - 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. -elim e0; try (intros; simpl in |- *; legacy ring). -unfold interp_ExprA in H2; fold interp_ExprA in H2; - cut - (AmultT (interp_ExprA lvar e2) - (AmultT (interp_ExprA lvar e4) - (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))) = - AmultT - (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4)) - (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). -intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1; - simpl in |- *; legacy ring. -legacy ring. -Qed. - -Lemma assoc_mult_correct1 : - 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)). -Proof. -simple induction e1; auto; intros. -rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct; - simpl in |- *; rewrite merge_mult_correct; simpl in |- *; - auto. -Qed. - -Lemma assoc_mult_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e. -Proof. -simple induction e; auto; intros. -elim e0; intros. -intros; simpl in |- *; legacy ring. -simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); - rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite merge_mult_correct; simpl in |- *; - rewrite merge_mult_correct; simpl in |- *; rewrite AmultT_assoc; - rewrite assoc_mult_correct1; rewrite H2; simpl in |- *; - rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1; - fold interp_ExprA in H1; rewrite (H0 lvar) in H1; - rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1)); - rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; - legacy ring. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -Qed. - -Lemma merge_plus_correct1 : - 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. -intros e1 e2; generalize e1; generalize e2; clear e1 e2. -simple induction e2; auto; intros. -unfold merge_plus at 1 in |- *; fold merge_plus in |- *; - unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; - fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; - fold interp_ExprA in |- *; auto. -Qed. - -Lemma merge_plus_correct : - 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. -elim e0; try intros; try (simpl in |- *; legacy ring). -unfold interp_ExprA in H2; fold interp_ExprA in H2; - cut - (AplusT (interp_ExprA lvar e2) - (AplusT (interp_ExprA lvar e4) - (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))) = - AplusT - (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4)) - (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). -intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1; - simpl in |- *; legacy ring. -legacy ring. -Qed. - -Lemma assoc_plus_correct : - 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. -simple induction e1; auto; intros. -rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct; - simpl in |- *; rewrite merge_plus_correct; simpl in |- *; - auto. -Qed. - -Lemma assoc_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (assoc e) = interp_ExprA lvar e. -Proof. -simple induction e; auto; intros. -elim e0; intros. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite merge_plus_correct; simpl in |- *; - rewrite merge_plus_correct; simpl in |- *; rewrite AplusT_assoc; - rewrite assoc_plus_correct; rewrite H2; simpl in |- *; - apply - (r_AplusT_plus (interp_ExprA lvar (assoc e1)) - (AplusT (interp_ExprA lvar (assoc e2)) - (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1))) - (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3)) - (interp_ExprA lvar e1))); rewrite <- AplusT_assoc; - rewrite - (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2))) - ; rewrite assoc_plus_correct; rewrite H1; simpl in |- *; - rewrite (H0 lvar); - rewrite <- - (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1)) - (interp_ExprA lvar e3) (interp_ExprA lvar e1)) - ; - rewrite - (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1) - (interp_ExprA lvar e3)); - rewrite (AplusT_comm (interp_ExprA lvar e1) (interp_ExprA lvar e3)); - rewrite <- - (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3) - (interp_ExprA lvar e1)); apply AplusT_comm. -unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; - fold interp_ExprA in |- *; rewrite assoc_mult_correct; - rewrite (H0 lvar); simpl in |- *; auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; - fold interp_ExprA in |- *; rewrite assoc_mult_correct; - simpl in |- *; auto. -Qed. - -(**** Distribution *****) - -Fixpoint distrib_EAopp (e:ExprA) : ExprA := - match e with - | EAplus e1 e2 => EAplus (distrib_EAopp e1) (distrib_EAopp e2) - | EAmult e1 e2 => EAmult (distrib_EAopp e1) (distrib_EAopp e2) - | EAopp e => EAmult (EAopp EAone) (distrib_EAopp e) - | e => e - end. - -Definition distrib_mult_right := - (fix distrib_mult_right (e1:ExprA) : ExprA -> ExprA := - fun e2:ExprA => - match e1 with - | EAplus t1 t2 => - EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2) - | _ => EAmult e1 e2 - end). - -Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA := - match e1 with - | EAplus t1 t2 => - EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2) - | _ => distrib_mult_right e2 e1 - end. - -Fixpoint distrib_main (e:ExprA) : ExprA := - match e with - | EAmult e1 e2 => distrib_mult_left (distrib_main e1) (distrib_main e2) - | EAplus e1 e2 => EAplus (distrib_main e1) (distrib_main e2) - | EAopp e => EAopp (distrib_main e) - | _ => e - end. - -Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e). - -Lemma distrib_mult_right_correct : - 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. -simple induction e1; try intros; simpl in |- *; auto. -rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar); - rewrite (H0 e2 lvar); legacy ring. -Qed. - -Lemma distrib_mult_left_correct : - 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. -simple induction e1; try intros; simpl in |- *. -rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl in |- *; - apply AmultT_Or. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite AmultT_comm; - rewrite - (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e) - (interp_ExprA lvar e0)); - rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e)); - rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0)); - rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -Qed. - -Lemma distrib_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (distrib e) = interp_ExprA lvar e. -Proof. -simple induction e; intros; auto. -simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); - unfold distrib in |- *; simpl in |- *; auto. -simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); - unfold distrib in |- *; simpl in |- *; apply distrib_mult_left_correct. -simpl in |- *; fold AoppT in |- *; rewrite <- (H lvar); - unfold distrib in |- *; simpl in |- *; rewrite distrib_mult_right_correct; - simpl in |- *; fold AoppT in |- *; legacy ring. -Qed. - -(**** Multiplication by the inverse product ****) - -Lemma mult_eq : - 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. -Proof. - simpl in |- *; intros; - apply - (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1) - (interp_ExprA lvar e2)); assumption. -Qed. - -Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA := - match e with - | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2) - | _ => EAmult a e - end. - -Definition multiply (e:ExprA) : ExprA := - match e with - | EAmult a e1 => multiply_aux a e1 - | _ => e - end. - -Lemma multiply_aux_correct : - 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. -simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct; - auto. - simpl in |- *; rewrite (H0 lvar); legacy ring. -Qed. - -Lemma multiply_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (multiply e) = interp_ExprA lvar e. -Proof. - simple induction e; simpl in |- *; auto. - intros; apply multiply_aux_correct. -Qed. - -(**** Permutations and simplification ****) - -Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA := - match m with - | EAmult m0 m1 => - match eqExprA m0 (EAinv a) with - | left _ => m1 - | right _ => EAmult m0 (monom_remove a m1) - end - | _ => - match eqExprA m (EAinv a) with - | left _ => EAone - | right _ => EAmult a m - end - end. - -Definition monom_simplif_rem := - (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA := - fun m:ExprA => - match a with - | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m) - | _ => monom_remove a m - end). - -Definition monom_simplif (a m:ExprA) : ExprA := - match m with - | EAmult a' m' => - match eqExprA a a' with - | left _ => monom_simplif_rem a m' - | right _ => m - end - | _ => m - end. - -Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA := - match e with - | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2) - | _ => monom_simplif a e - end. - -Lemma monom_remove_correct : - 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). -Proof. -simple induction e; intros. -simpl in |- *; case (eqExprA EAzero (EAinv a)); intros; - [ inversion e0 | simpl in |- *; trivial ]. -simpl in |- *; case (eqExprA EAone (EAinv a)); intros; - [ inversion e0 | simpl in |- *; trivial ]. -simpl in |- *; case (eqExprA (EAplus e0 e1) (EAinv a)); intros; - [ inversion e2 | simpl in |- *; trivial ]. -simpl in |- *; case (eqExprA e0 (EAinv a)); intros. -rewrite e2; simpl in |- *; fold AinvT in |- *. -rewrite <- - (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a)) - (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ]. -simpl in |- *; rewrite H0; auto; legacy ring. -simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a)); - intros; [ inversion e1 | simpl in |- *; trivial ]. -unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros. -case (eqExprA e0 a); intros. -rewrite e2; simpl in |- *; fold AinvT in |- *; rewrite AinvT_r; auto. -inversion e1; simpl in |- *; elimtype False; auto. -simpl in |- *; trivial. -unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros; - [ inversion e0 | simpl in |- *; trivial ]. -Qed. - -Lemma monom_simplif_rem_correct : - 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). -Proof. -simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct; - auto. -elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1); - intros. -rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto. -legacy ring. -Qed. - -Lemma monom_simplif_correct : - 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. -simple induction e; intros; auto. -simpl in |- *; case (eqExprA a e0); intros. -rewrite <- e2; apply monom_simplif_rem_correct; auto. -simpl in |- *; trivial. -Qed. - -Lemma inverse_correct : - 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. -simple induction e; intros; auto. -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. diff --git a/contrib/field/LegacyField.v b/contrib/field/LegacyField.v index 5d08c57f46..ee1ddd477b 100644 --- a/contrib/field/LegacyField.v +++ b/contrib/field/LegacyField.v @@ -8,8 +8,8 @@ (* $Id$ *) -Require Export Field_Compl. -Require Export Field_Theory. -Require Export Field_Tactic. +Require Export LegacyField_Compl. +Require Export LegacyField_Theory. +Require Export LegacyField_Tactic. -(* Command declarations are moved to the ML side *) \ No newline at end of file +(* Command declarations are moved to the ML side *) diff --git a/contrib/field/LegacyField_Compl.v b/contrib/field/LegacyField_Compl.v new file mode 100644 index 0000000000..746e7c9976 --- /dev/null +++ b/contrib/field/LegacyField_Compl.v @@ -0,0 +1,38 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* e2}) + (lst:list (prod A B)) {struct lst} : + B -> A -> A := + fun (key:B) (default:A) => + match lst with + | nil => default + | (v,e) :: l => + match eq_dec e key with + | left _ => v + | right _ => assoc_2nd_rec A B eq_dec l key default + end + end). + +Definition mem := + (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) + (a:A) (l:list A) {struct l} : bool := + match l with + | nil => false + | a1 :: l1 => + match eq_dec a a1 with + | left _ => true + | right _ => mem A eq_dec a l1 + end + end). diff --git a/contrib/field/LegacyField_Theory.v b/contrib/field/LegacyField_Theory.v new file mode 100644 index 0000000000..5516f92fac --- /dev/null +++ b/contrib/field/LegacyField_Theory.v @@ -0,0 +1,650 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* A -> A; + Amult : A -> A -> A; + Aone : A; + Azero : A; + Aopp : A -> A; + Aeq : A -> A -> bool; + Ainv : A -> 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}. + +(* The reflexion structure *) +Inductive ExprA : Set := + | EAzero : ExprA + | EAone : ExprA + | EAplus : ExprA -> ExprA -> ExprA + | EAmult : ExprA -> ExprA -> ExprA + | EAopp : ExprA -> ExprA + | EAinv : ExprA -> ExprA + | EAvar : nat -> ExprA. + +(**** Decidability of equality ****) + +Lemma eqExprA_O : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}. +Proof. + double induction e1 e2; try intros; + try (left; reflexivity) || (try (right; discriminate)). + elim (H1 e0); intro y; elim (H2 e); intro y0; + try + (left; rewrite y; rewrite y0; auto) || + (right; red in |- *; intro; inversion H3; auto). + elim (H1 e0); intro y; elim (H2 e); intro y0; + try + (left; rewrite y; rewrite y0; auto) || + (right; red in |- *; intro; inversion H3; auto). + elim (H0 e); intro y. + left; rewrite y; auto. + right; red in |- *; intro; inversion H1; auto. + elim (H0 e); intro y. + left; rewrite y; auto. + right; red in |- *; intro; inversion H1; auto. + elim (eq_nat_dec n n0); intro y. + left; rewrite y; auto. + right; red in |- *; intro; inversion H; auto. +Defined. + +Definition eq_nat_dec := Eval compute in eq_nat_dec. +Definition eqExprA := Eval compute in eqExprA_O. + +(**** Generation of the multiplier ****) + +Fixpoint mult_of_list (e:list ExprA) : ExprA := + match e with + | nil => EAone + | e1 :: l1 => EAmult e1 (mult_of_list l1) + end. + +Section Theory_of_fields. + +Variable T : Field_Theory. + +Let AT := A T. +Let AplusT := Aplus T. +Let AmultT := Amult T. +Let AoneT := Aone T. +Let AzeroT := Azero T. +Let AoppT := Aopp T. +Let AeqT := Aeq T. +Let AinvT := Ainv T. +Let RTT := RT T. +Let Th_inv_defT := Th_inv_def T. + +Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) ( + Azero T) (Aopp T) (Aeq T) (RT T). + +Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT. + +(***************************) +(* Lemmas to be used *) +(***************************) + +Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1. +Proof. + intros; legacy ring. +Qed. + +Notation AplusT_sym := AplusT_comm (only parsing). (* Compatibility *) + +Lemma AplusT_assoc : + forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3). +Proof. + intros; legacy ring. +Qed. + +Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1. +Proof. + intros; legacy ring. +Qed. + +Notation AmultT_sym := AmultT_comm (only parsing). (* Compatibility *) + +Lemma AmultT_assoc : + forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3). +Proof. + intros; legacy ring. +Qed. + +Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r. +Proof. + intros; legacy ring. +Qed. + +Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r. +Proof. + intros; legacy ring. +Qed. + +Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT. +Proof. + intros; legacy ring. +Qed. + +Lemma AmultT_AplusT_distr : + forall r1 r2 r3:AT, + AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3). +Proof. + intros; legacy ring. +Qed. + +Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2. +Proof. + intros; transitivity (AplusT (AplusT (AoppT r) r) r1). + legacy ring. + transitivity (AplusT (AplusT (AoppT r) r) r2). + repeat rewrite AplusT_assoc; rewrite <- H; reflexivity. + legacy ring. +Qed. + +Lemma r_AmultT_mult : + forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2. +Proof. + intros; transitivity (AmultT (AmultT (AinvT r) r) r1). + rewrite Th_inv_defT; [ symmetry in |- *; apply AmultT_1l; auto | auto ]. + transitivity (AmultT (AmultT (AinvT r) r) r2). + repeat rewrite AmultT_assoc; rewrite H; trivial. + rewrite Th_inv_defT; [ apply AmultT_1l; auto | auto ]. +Qed. + +Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT. +Proof. + intro; legacy ring. +Qed. + +Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT. +Proof. + intro; legacy ring. +Qed. + +Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r. +Proof. + intro; legacy ring. +Qed. + +Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT. +Proof. + intros; rewrite AmultT_comm; apply Th_inv_defT; auto. +Qed. + +Lemma Rmult_neq_0_reg : + forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT. +Proof. + intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; legacy ring. +Qed. + +(************************) +(* Interpretation *) +(************************) + +(**** ExprA --> A ****) + +Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} : + AT := + match e with + | EAzero => AzeroT + | EAone => AoneT + | EAplus e1 e2 => AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2) + | EAmult e1 e2 => AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2) + | EAopp e => Aopp T (interp_ExprA lvar e) + | EAinv e => Ainv T (interp_ExprA lvar e) + | EAvar n => assoc_2nd AT nat eq_nat_dec lvar n AzeroT + end. + +(************************) +(* Simplification *) +(************************) + +(**** Associativity ****) + +Definition merge_mult := + (fix merge_mult (e1:ExprA) : ExprA -> ExprA := + fun e2:ExprA => + match e1 with + | EAmult t1 t2 => + match t2 with + | EAmult t2 t3 => EAmult t1 (EAmult t2 (merge_mult t3 e2)) + | _ => EAmult t1 (EAmult t2 e2) + end + | _ => EAmult e1 e2 + end). + +Fixpoint assoc_mult (e:ExprA) : ExprA := + match e with + | EAmult e1 e3 => + match e1 with + | EAmult e1 e2 => + merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2)) + (assoc_mult e3) + | _ => EAmult e1 (assoc_mult e3) + end + | _ => e + end. + +Definition merge_plus := + (fix merge_plus (e1:ExprA) : ExprA -> ExprA := + fun e2:ExprA => + match e1 with + | EAplus t1 t2 => + match t2 with + | EAplus t2 t3 => EAplus t1 (EAplus t2 (merge_plus t3 e2)) + | _ => EAplus t1 (EAplus t2 e2) + end + | _ => EAplus e1 e2 + end). + +Fixpoint assoc (e:ExprA) : ExprA := + match e with + | EAplus e1 e3 => + match e1 with + | EAplus e1 e2 => + merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3) + | _ => EAplus (assoc_mult e1) (assoc e3) + end + | _ => assoc_mult e + end. + +Lemma merge_mult_correct1 : + 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. +intros e1 e2; generalize e1; generalize e2; clear e1 e2. +simple induction e2; auto; intros. +unfold merge_mult at 1 in |- *; fold merge_mult in |- *; + unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; + rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; + fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; + fold interp_ExprA in |- *; auto. +Qed. + +Lemma merge_mult_correct : + 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. +elim e0; try (intros; simpl in |- *; legacy ring). +unfold interp_ExprA in H2; fold interp_ExprA in H2; + cut + (AmultT (interp_ExprA lvar e2) + (AmultT (interp_ExprA lvar e4) + (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))) = + AmultT + (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4)) + (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). +intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1; + simpl in |- *; legacy ring. +legacy ring. +Qed. + +Lemma assoc_mult_correct1 : + 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)). +Proof. +simple induction e1; auto; intros. +rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct; + simpl in |- *; rewrite merge_mult_correct; simpl in |- *; + auto. +Qed. + +Lemma assoc_mult_correct : + forall (e:ExprA) (lvar:list (AT * nat)), + interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e. +Proof. +simple induction e; auto; intros. +elim e0; intros. +intros; simpl in |- *; legacy ring. +simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); + rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite merge_mult_correct; simpl in |- *; + rewrite merge_mult_correct; simpl in |- *; rewrite AmultT_assoc; + rewrite assoc_mult_correct1; rewrite H2; simpl in |- *; + rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1; + fold interp_ExprA in H1; rewrite (H0 lvar) in H1; + rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1)); + rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; + legacy ring. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +Qed. + +Lemma merge_plus_correct1 : + 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. +intros e1 e2; generalize e1; generalize e2; clear e1 e2. +simple induction e2; auto; intros. +unfold merge_plus at 1 in |- *; fold merge_plus in |- *; + unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; + rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; + fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; + fold interp_ExprA in |- *; auto. +Qed. + +Lemma merge_plus_correct : + 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. +elim e0; try intros; try (simpl in |- *; legacy ring). +unfold interp_ExprA in H2; fold interp_ExprA in H2; + cut + (AplusT (interp_ExprA lvar e2) + (AplusT (interp_ExprA lvar e4) + (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))) = + AplusT + (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4)) + (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). +intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1; + simpl in |- *; legacy ring. +legacy ring. +Qed. + +Lemma assoc_plus_correct : + 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. +simple induction e1; auto; intros. +rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct; + simpl in |- *; rewrite merge_plus_correct; simpl in |- *; + auto. +Qed. + +Lemma assoc_correct : + forall (e:ExprA) (lvar:list (AT * nat)), + interp_ExprA lvar (assoc e) = interp_ExprA lvar e. +Proof. +simple induction e; auto; intros. +elim e0; intros. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite merge_plus_correct; simpl in |- *; + rewrite merge_plus_correct; simpl in |- *; rewrite AplusT_assoc; + rewrite assoc_plus_correct; rewrite H2; simpl in |- *; + apply + (r_AplusT_plus (interp_ExprA lvar (assoc e1)) + (AplusT (interp_ExprA lvar (assoc e2)) + (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1))) + (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3)) + (interp_ExprA lvar e1))); rewrite <- AplusT_assoc; + rewrite + (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2))) + ; rewrite assoc_plus_correct; rewrite H1; simpl in |- *; + rewrite (H0 lvar); + rewrite <- + (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1)) + (interp_ExprA lvar e3) (interp_ExprA lvar e1)) + ; + rewrite + (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1) + (interp_ExprA lvar e3)); + rewrite (AplusT_comm (interp_ExprA lvar e1) (interp_ExprA lvar e3)); + rewrite <- + (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3) + (interp_ExprA lvar e1)); apply AplusT_comm. +unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; + fold interp_ExprA in |- *; rewrite assoc_mult_correct; + rewrite (H0 lvar); simpl in |- *; auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; + fold interp_ExprA in |- *; rewrite assoc_mult_correct; + simpl in |- *; auto. +Qed. + +(**** Distribution *****) + +Fixpoint distrib_EAopp (e:ExprA) : ExprA := + match e with + | EAplus e1 e2 => EAplus (distrib_EAopp e1) (distrib_EAopp e2) + | EAmult e1 e2 => EAmult (distrib_EAopp e1) (distrib_EAopp e2) + | EAopp e => EAmult (EAopp EAone) (distrib_EAopp e) + | e => e + end. + +Definition distrib_mult_right := + (fix distrib_mult_right (e1:ExprA) : ExprA -> ExprA := + fun e2:ExprA => + match e1 with + | EAplus t1 t2 => + EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2) + | _ => EAmult e1 e2 + end). + +Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA := + match e1 with + | EAplus t1 t2 => + EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2) + | _ => distrib_mult_right e2 e1 + end. + +Fixpoint distrib_main (e:ExprA) : ExprA := + match e with + | EAmult e1 e2 => distrib_mult_left (distrib_main e1) (distrib_main e2) + | EAplus e1 e2 => EAplus (distrib_main e1) (distrib_main e2) + | EAopp e => EAopp (distrib_main e) + | _ => e + end. + +Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e). + +Lemma distrib_mult_right_correct : + 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. +simple induction e1; try intros; simpl in |- *; auto. +rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar); + rewrite (H0 e2 lvar); legacy ring. +Qed. + +Lemma distrib_mult_left_correct : + 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. +simple induction e1; try intros; simpl in |- *. +rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl in |- *; + apply AmultT_Or. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +rewrite AmultT_comm; + rewrite + (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e) + (interp_ExprA lvar e0)); + rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e)); + rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0)); + rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +Qed. + +Lemma distrib_correct : + forall (e:ExprA) (lvar:list (AT * nat)), + interp_ExprA lvar (distrib e) = interp_ExprA lvar e. +Proof. +simple induction e; intros; auto. +simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); + unfold distrib in |- *; simpl in |- *; auto. +simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); + unfold distrib in |- *; simpl in |- *; apply distrib_mult_left_correct. +simpl in |- *; fold AoppT in |- *; rewrite <- (H lvar); + unfold distrib in |- *; simpl in |- *; rewrite distrib_mult_right_correct; + simpl in |- *; fold AoppT in |- *; legacy ring. +Qed. + +(**** Multiplication by the inverse product ****) + +Lemma mult_eq : + 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. +Proof. + simpl in |- *; intros; + apply + (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1) + (interp_ExprA lvar e2)); assumption. +Qed. + +Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA := + match e with + | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2) + | _ => EAmult a e + end. + +Definition multiply (e:ExprA) : ExprA := + match e with + | EAmult a e1 => multiply_aux a e1 + | _ => e + end. + +Lemma multiply_aux_correct : + 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. +simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct; + auto. + simpl in |- *; rewrite (H0 lvar); legacy ring. +Qed. + +Lemma multiply_correct : + forall (e:ExprA) (lvar:list (AT * nat)), + interp_ExprA lvar (multiply e) = interp_ExprA lvar e. +Proof. + simple induction e; simpl in |- *; auto. + intros; apply multiply_aux_correct. +Qed. + +(**** Permutations and simplification ****) + +Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA := + match m with + | EAmult m0 m1 => + match eqExprA m0 (EAinv a) with + | left _ => m1 + | right _ => EAmult m0 (monom_remove a m1) + end + | _ => + match eqExprA m (EAinv a) with + | left _ => EAone + | right _ => EAmult a m + end + end. + +Definition monom_simplif_rem := + (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA := + fun m:ExprA => + match a with + | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m) + | _ => monom_remove a m + end). + +Definition monom_simplif (a m:ExprA) : ExprA := + match m with + | EAmult a' m' => + match eqExprA a a' with + | left _ => monom_simplif_rem a m' + | right _ => m + end + | _ => m + end. + +Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA := + match e with + | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2) + | _ => monom_simplif a e + end. + +Lemma monom_remove_correct : + 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). +Proof. +simple induction e; intros. +simpl in |- *; case (eqExprA EAzero (EAinv a)); intros; + [ inversion e0 | simpl in |- *; trivial ]. +simpl in |- *; case (eqExprA EAone (EAinv a)); intros; + [ inversion e0 | simpl in |- *; trivial ]. +simpl in |- *; case (eqExprA (EAplus e0 e1) (EAinv a)); intros; + [ inversion e2 | simpl in |- *; trivial ]. +simpl in |- *; case (eqExprA e0 (EAinv a)); intros. +rewrite e2; simpl in |- *; fold AinvT in |- *. +rewrite <- + (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a)) + (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ]. +simpl in |- *; rewrite H0; auto; legacy ring. +simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a)); + intros; [ inversion e1 | simpl in |- *; trivial ]. +unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros. +case (eqExprA e0 a); intros. +rewrite e2; simpl in |- *; fold AinvT in |- *; rewrite AinvT_r; auto. +inversion e1; simpl in |- *; elimtype False; auto. +simpl in |- *; trivial. +unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros; + [ inversion e0 | simpl in |- *; trivial ]. +Qed. + +Lemma monom_simplif_rem_correct : + 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). +Proof. +simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct; + auto. +elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1); + intros. +rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto. +legacy ring. +Qed. + +Lemma monom_simplif_correct : + 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. +simple induction e; intros; auto. +simpl in |- *; case (eqExprA a e0); intros. +rewrite <- e2; apply monom_simplif_rem_correct; auto. +simpl in |- *; trivial. +Qed. + +Lemma inverse_correct : + 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. +simple induction e; intros; auto. +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. diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 2da5e9fbd7..b8a978d84e 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -86,7 +86,7 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth Ring.add_theory true true false a None None None aplus amult aone azero (Some aopp) aeq rth Quote.ConstrSet.empty with | UserError("Add Semi Ring",_) -> ()); - let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"), + let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"), [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in begin let _ = type_of (Global.env ()) Evd.empty th in (); -- cgit v1.2.3