From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Mar 2009 01:22:58 +0000 Subject: Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/setoid_ring/InitialRing.v | 908 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 908 insertions(+) create mode 100644 plugins/setoid_ring/InitialRing.v (limited to 'plugins/setoid_ring/InitialRing.v') diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v new file mode 100644 index 000000000..e664b3b76 --- /dev/null +++ b/plugins/setoid_ring/InitialRing.v @@ -0,0 +1,908 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + Notation "0" := rO. Notation "1" := rI. + Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). + Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). + Notation "x == y" := (req x y). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid3. + Ltac rrefl := gen_reflexivity Rsth. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + + Fixpoint gen_phiPOS1 (p:positive) : R := + match p with + | xH => 1 + | xO p => (1 + 1) * (gen_phiPOS1 p) + | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p)) + end. + + Fixpoint gen_phiPOS (p:positive) : R := + match p with + | xH => 1 + | xO xH => (1 + 1) + | xO p => (1 + 1) * (gen_phiPOS p) + | xI xH => 1 + (1 +1) + | xI p => 1 + ((1 + 1) * (gen_phiPOS p)) + end. + + Definition gen_phiZ1 z := + match z with + | Zpos p => gen_phiPOS1 p + | Z0 => 0 + | Zneg p => -(gen_phiPOS1 p) + end. + + Definition gen_phiZ z := + match z with + | Zpos p => gen_phiPOS p + | Z0 => 0 + | Zneg p => -(gen_phiPOS p) + end. + Notation "[ x ]" := (gen_phiZ x). + + Definition get_signZ z := + match z with + | Zneg p => Some (Zpos p) + | _ => None + end. + + Lemma get_signZ_th : sign_theory Zopp Zeq_bool get_signZ. + Proof. + constructor. + destruct c;intros;try discriminate. + injection H;clear H;intros H1;subst c'. + simpl. unfold Zeq_bool. rewrite Zcompare_refl. trivial. + Qed. + + + Section ALMOST_RING. + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + + Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. + Proof. + induction x;simpl. + rewrite IHx;destruct x;simpl;norm. + rewrite IHx;destruct x;simpl;norm. + rrefl. + Qed. + + Lemma ARgen_phiPOS_Psucc : forall x, + gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x). + Proof. + induction x;simpl;norm. + rewrite IHx;norm. + add_push 1;rrefl. + Qed. + + Lemma ARgen_phiPOS_add : forall x y, + gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). + Proof. + induction x;destruct y;simpl;norm. + rewrite Pplus_carry_spec. + rewrite ARgen_phiPOS_Psucc. + rewrite IHx;norm. + add_push (gen_phiPOS1 y);add_push 1;rrefl. + rewrite IHx;norm;add_push (gen_phiPOS1 y);rrefl. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl. + rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;rrefl. + rewrite IHx;norm;add_push(gen_phiPOS1 y);rrefl. + add_push 1;rrefl. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl. + Qed. + + Lemma ARgen_phiPOS_mult : + forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y. + Proof. + induction x;intros;simpl;norm. + rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm. + rewrite IHx;rrefl. + Qed. + + End ALMOST_RING. + + Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. + Let ARth := Rth_ARth Rsth Reqe Rth. + Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + +(*morphisms are extensionaly equal*) + Lemma same_genZ : forall x, [x] == gen_phiZ1 x. + Proof. + destruct x;simpl; try rewrite (same_gen ARth);rrefl. + Qed. + + Lemma gen_Zeqb_ok : forall x y, + Zeq_bool x y = true -> [x] == [y]. + Proof. + intros x y H. + assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. + rewrite H1;rrefl. + Qed. + + Lemma gen_phiZ1_add_pos_neg : forall x y, + gen_phiZ1 + match (x ?= y)%positive Eq with + | Eq => Z0 + | Lt => Zneg (y - x) + | Gt => Zpos (x - y) + end + == gen_phiPOS1 x + -gen_phiPOS1 y. + Proof. + intros x y. + assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y). + generalize (Pminus_mask_Gt y x). + replace Eq with (CompOpp Eq);[intro H1;simpl|trivial]. + rewrite <- Pcompare_antisym in H1. + destruct ((x ?= y)%positive Eq). + rewrite H;trivial. rewrite (Ropp_def Rth);rrefl. + destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial. + unfold Pminus; rewrite Heq1;rewrite <- Heq2. + rewrite (ARgen_phiPOS_add ARth);simpl;norm. + rewrite (Ropp_def Rth);norm. + destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial. + unfold Pminus; rewrite Heq1;rewrite <- Heq2. + rewrite (ARgen_phiPOS_add ARth);simpl;norm. + add_push (gen_phiPOS1 h);rewrite (Ropp_def Rth); norm. + Qed. + + Lemma match_compOpp : forall x (B:Type) (be bl bg:B), + match CompOpp x with Eq => be | Lt => bl | Gt => bg end + = match x with Eq => be | Lt => bg | Gt => bl end. + Proof. destruct x;simpl;intros;trivial. Qed. + + Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y]. + Proof. + intros x y; repeat rewrite same_genZ; generalize x y;clear x y. + induction x;destruct y;simpl;norm. + apply (ARgen_phiPOS_add ARth). + apply gen_phiZ1_add_pos_neg. + replace Eq with (CompOpp Eq);trivial. + rewrite <- Pcompare_antisym;simpl. + rewrite match_compOpp. + rewrite (Radd_comm Rth). + apply gen_phiZ1_add_pos_neg. + rewrite (ARgen_phiPOS_add ARth); norm. + Qed. + + Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y]. + Proof. + intros x y;repeat rewrite same_genZ. + destruct x;destruct y;simpl;norm; + rewrite (ARgen_phiPOS_mult ARth);try (norm;fail). + rewrite (Ropp_opp Rsth Reqe Rth);rrefl. + Qed. + + Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. + Proof. intros;subst;rrefl. Qed. + +(*proof that [.] satisfies morphism specifications*) + Lemma gen_phiZ_morph : + ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH) + Zplus Zmult Zminus Zopp Zeq_bool gen_phiZ. + Proof. + assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH) + Zplus Zmult Zeq_bool gen_phiZ). + apply mkRmorph;simpl;try rrefl. + apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok. + apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext). + Qed. + +End ZMORPHISM. + +(** N is a semi-ring and a setoid*) +Lemma Nsth : Setoid_Theory N (@eq N). +Proof (Eqsth N). + +Lemma Nseqe : sring_eq_ext Nplus Nmult (@eq N). +Proof (Eq_s_ext Nplus Nmult). + +Lemma Nth : semi_ring_theory N0 (Npos xH) Nplus Nmult (@eq N). +Proof. + constructor. exact Nplus_0_l. exact Nplus_comm. exact Nplus_assoc. + exact Nmult_1_l. exact Nmult_0_l. exact Nmult_comm. exact Nmult_assoc. + exact Nmult_plus_distr_r. +Qed. + +Definition Nsub := SRsub Nplus. +Definition Nopp := (@SRopp N). + +Lemma Neqe : ring_eq_ext Nplus Nmult Nopp (@eq N). +Proof (SReqe_Reqe Nseqe). + +Lemma Nath : + almost_ring_theory N0 (Npos xH) Nplus Nmult Nsub Nopp (@eq N). +Proof (SRth_ARth Nsth Nth). + +Definition Neq_bool (x y:N) := + match Ncompare x y with + | Eq => true + | _ => false + end. + +Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y. + Proof. + intros x y;unfold Neq_bool. + assert (H:=Ncompare_Eq_eq x y); + destruct (Ncompare x y);intros;try discriminate. + rewrite H;trivial. + Qed. + +Lemma Neq_bool_complete : forall x y, Neq_bool x y = true -> x = y. + Proof. + intros x y;unfold Neq_bool. + assert (H:=Ncompare_Eq_eq x y); + destruct (Ncompare x y);intros;try discriminate. + rewrite H;trivial. + Qed. + +(**Same as above : definition of two,extensionaly equal, generic morphisms *) +(**from N to any semi-ring*) +Section NMORPHISM. + Variable R : Type. + Variable (rO rI : R) (radd rmul: R->R->R). + Variable req : R -> R -> Prop. + Notation "0" := rO. Notation "1" := rI. + Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid4. + Ltac rrefl := gen_reflexivity Rsth. + Variable SReqe : sring_eq_ext radd rmul req. + Variable SRth : semi_ring_theory 0 1 radd rmul req. + Let ARth := SRth_ARth Rsth SRth. + Let Reqe := SReqe_Reqe SReqe. + Let ropp := (@SRopp R). + Let rsub := (@SRsub R radd). + Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). + Notation "x == y" := (req x y). + Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext4. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext5. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite Rsth Reqe ARth. + + Definition gen_phiN1 x := + match x with + | N0 => 0 + | Npos x => gen_phiPOS1 1 radd rmul x + end. + + Definition gen_phiN x := + match x with + | N0 => 0 + | Npos x => gen_phiPOS 1 radd rmul x + end. + Notation "[ x ]" := (gen_phiN x). + + Lemma same_genN : forall x, [x] == gen_phiN1 x. + Proof. + destruct x;simpl. rrefl. + rewrite (same_gen Rsth Reqe ARth);rrefl. + Qed. + + Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y]. + Proof. + intros x y;repeat rewrite same_genN. + destruct x;destruct y;simpl;norm. + apply (ARgen_phiPOS_add Rsth Reqe ARth). + Qed. + + Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y]. + Proof. + intros x y;repeat rewrite same_genN. + destruct x;destruct y;simpl;norm. + apply (ARgen_phiPOS_mult Rsth Reqe ARth). + Qed. + + Lemma gen_phiN_sub : forall x y, [Nsub x y] == [x] - [y]. + Proof. exact gen_phiN_add. Qed. + +(*gen_phiN satisfies morphism specifications*) + Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req + N0 (Npos xH) Nplus Nmult Nsub Nopp Neq_bool gen_phiN. + Proof. + constructor;intros;simpl; try rrefl. + apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult. + rewrite (Neq_bool_ok x y);trivial. rrefl. + Qed. + +End NMORPHISM. + +(* Words on N : initial structure for almost-rings. *) +Definition Nword := list N. +Definition NwO : Nword := nil. +Definition NwI : Nword := 1%N :: nil. + +Definition Nwcons n (w : Nword) : Nword := + match w, n with + | nil, 0%N => nil + | _, _ => n :: w + end. + +Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword := + match w1, w2 with + | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2' + | nil, _ => w2 + | _, nil => w1 + end. + +Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w. + +Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2). + +Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword := + match w with + | m :: w' => (n*m)%N :: Nwscal n w' + | nil => nil + end. + +Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword := + match w1 with + | 0%N::w1' => Nwopp (Nwmul w1' w2) + | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2) + | nil => nil + end. +Fixpoint Nw_is0 (w : Nword) : bool := + match w with + | nil => true + | 0%N :: w' => Nw_is0 w' + | _ => false + end. + +Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool := + match w1, w2 with + | n1::w1', n2::w2' => + if Neq_bool n1 n2 then Nweq_bool w1' w2' else false + | nil, _ => Nw_is0 w2 + | _, nil => Nw_is0 w1 + end. + +Section NWORDMORPHISM. + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + Notation "0" := rO. Notation "1" := rI. + Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). + Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). + Notation "x == y" := (req x y). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid5. + Ltac rrefl := gen_reflexivity Rsth. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext5. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext5. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext5. exact (Ropp_ext Reqe). Qed. + + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + + Fixpoint gen_phiNword (w : Nword) : R := + match w with + | nil => 0 + | n :: nil => gen_phiN rO rI radd rmul n + | N0 :: w' => - gen_phiNword w' + | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w' + end. + + Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0. +Proof. +induction w; simpl in |- *; intros; auto. + reflexivity. + + destruct a. + destruct w. + reflexivity. + + rewrite IHw in |- *; trivial. + apply (ARopp_zero Rsth Reqe ARth). + + discriminate. +Qed. + + Lemma gen_phiNword_cons : forall w n, + gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w. +induction w. + destruct n; simpl in |- *; norm. + + intros. + destruct n; norm. +Qed. + + Lemma gen_phiNword_Nwcons : forall w n, + gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w. +destruct w; intros. + destruct n; norm. + + unfold Nwcons in |- *. + rewrite gen_phiNword_cons in |- *. + reflexivity. +Qed. + + Lemma gen_phiNword_ok : forall w1 w2, + Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2. +induction w1; intros. + simpl in |- *. + rewrite (gen_phiNword0_ok _ H) in |- *. + reflexivity. + + rewrite gen_phiNword_cons in |- *. + destruct w2. + simpl in H. + destruct a; try discriminate. + rewrite (gen_phiNword0_ok _ H) in |- *. + norm. + + simpl in H. + rewrite gen_phiNword_cons in |- *. + case_eq (Neq_bool a n); intros. + rewrite H0 in H. + rewrite <- (Neq_bool_ok _ _ H0) in |- *. + rewrite (IHw1 _ H) in |- *. + reflexivity. + + rewrite H0 in H; discriminate H. +Qed. + + +Lemma Nwadd_ok : forall x y, + gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y. +induction x; intros. + simpl in |- *. + norm. + + destruct y. + simpl Nwadd; norm. + + simpl Nwadd in |- *. + repeat rewrite gen_phiNword_cons in |- *. + rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by + (destruct Reqe; constructor; trivial). + + rewrite IHx in |- *. + norm. + add_push (- gen_phiNword x); reflexivity. +Qed. + +Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x. +simpl in |- *. +unfold Nwopp in |- *; simpl in |- *. +intros. +rewrite gen_phiNword_Nwcons in |- *; norm. +Qed. + +Lemma Nwscal_ok : forall n x, + gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x. +induction x; intros. + norm. + + simpl Nwscal in |- *. + repeat rewrite gen_phiNword_cons in |- *. + rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- * + by (destruct Reqe; constructor; trivial). + + rewrite IHx in |- *. + norm. +Qed. + +Lemma Nwmul_ok : forall x y, + gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y. +induction x; intros. + norm. + + destruct a. + simpl Nwmul in |- *. + rewrite Nwopp_ok in |- *. + rewrite IHx in |- *. + rewrite gen_phiNword_cons in |- *. + norm. + + simpl Nwmul in |- *. + unfold Nwsub in |- *. + rewrite Nwadd_ok in |- *. + rewrite Nwscal_ok in |- *. + rewrite Nwopp_ok in |- *. + rewrite IHx in |- *. + rewrite gen_phiNword_cons in |- *. + norm. +Qed. + +(* Proof that [.] satisfies morphism specifications *) + Lemma gen_phiNword_morph : + ring_morph 0 1 radd rmul rsub ropp req + NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword. +constructor. + reflexivity. + + reflexivity. + + exact Nwadd_ok. + + intros. + unfold Nwsub in |- *. + rewrite Nwadd_ok in |- *. + rewrite Nwopp_ok in |- *. + norm. + + exact Nwmul_ok. + + exact Nwopp_ok. + + exact gen_phiNword_ok. +Qed. + +End NWORDMORPHISM. + +Section GEN_DIV. + + Variables (R : Type) (rO : R) (rI : R) (radd : R -> R -> R) + (rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R) + (req : R -> R -> Prop) (C : Type) (cO : C) (cI : C) + (cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C) + (copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R). + Variable Rsth : Setoid_Theory R req. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req. + Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. + + (* Useful tactics *) + Add Setoid R req Rsth as R_set1. + Ltac rrefl := gen_reflexivity Rsth. + Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac rsimpl := gen_srewrite Rsth Reqe ARth. + + Definition triv_div x y := + if ceqb x y then (cI, cO) + else (cO, x). + + Ltac Esimpl :=repeat (progress ( + match goal with + | |- context [phi cO] => rewrite (morph0 morph) + | |- context [phi cI] => rewrite (morph1 morph) + | |- context [phi (cadd ?x ?y)] => rewrite ((morph_add morph) x y) + | |- context [phi (cmul ?x ?y)] => rewrite ((morph_mul morph) x y) + | |- context [phi (csub ?x ?y)] => rewrite ((morph_sub morph) x y) + | |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x) + end)). + + Lemma triv_div_th : Ring_theory.div_theory req cadd cmul phi triv_div. + Proof. + constructor. + intros a b;unfold triv_div. + assert (X:= morph.(morph_eq) a b);destruct (ceqb a b). + Esimpl. + rewrite X; trivial. + rsimpl. + Esimpl; rsimpl. +Qed. + + Variable zphi : Z -> R. + + Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi ZOdiv_eucl. + Proof. + constructor. + intros; generalize (ZOdiv_eucl_correct a b); case ZOdiv_eucl; intros; subst. + rewrite Zmult_comm; rsimpl. + Qed. + + Variable nphi : N -> R. + + Lemma Ntriv_div_th : div_theory req Nplus Nmult nphi Ndiv_eucl. + constructor. + intros; generalize (Ndiv_eucl_correct a b); case Ndiv_eucl; intros; subst. + rewrite Nmult_comm; rsimpl. + Qed. + +End GEN_DIV. + + (* syntaxification of constants in an abstract ring: + the inverse of gen_phiPOS *) + Ltac inv_gen_phi_pos rI add mul t := + let rec inv_cst t := + match t with + rI => constr:1%positive + | (add rI rI) => constr:2%positive + | (add rI (add rI rI)) => constr:3%positive + | (mul (add rI rI) ?p) => (* 2p *) + match inv_cst p with + NotConstant => constr:NotConstant + | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *) + | ?p => constr:(xO p) + end + | (add rI (mul (add rI rI) ?p)) => (* 1+2p *) + match inv_cst p with + NotConstant => constr:NotConstant + | 1%positive => constr:NotConstant + | ?p => constr:(xI p) + end + | _ => constr:NotConstant + end in + inv_cst t. + +(* The (partial) inverse of gen_phiNword *) + Ltac inv_gen_phiNword rO rI add mul opp t := + match t with + rO => constr:NwO + | _ => + match inv_gen_phi_pos rI add mul t with + NotConstant => constr:NotConstant + | ?p => constr:(Npos p::nil) + end + end. + + +(* The inverse of gen_phiN *) + Ltac inv_gen_phiN rO rI add mul t := + match t with + rO => constr:0%N + | _ => + match inv_gen_phi_pos rI add mul t with + NotConstant => constr:NotConstant + | ?p => constr:(Npos p) + end + end. + +(* The inverse of gen_phiZ *) + Ltac inv_gen_phiZ rO rI add mul opp t := + match t with + rO => constr:0%Z + | (opp ?p) => + match inv_gen_phi_pos rI add mul p with + NotConstant => constr:NotConstant + | ?p => constr:(Zneg p) + end + | _ => + match inv_gen_phi_pos rI add mul t with + NotConstant => constr:NotConstant + | ?p => constr:(Zpos p) + end + end. + +(* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above + are only optimisations that directly returns the reifid constant + instead of resorting to the constant propagation of the simplification + algorithm. *) +Ltac inv_gen_phi rO rI cO cI t := + match t with + | rO => cO + | rI => cI + end. + +(* A simple tactic recognizing no constant *) + Ltac inv_morph_nothing t := constr:NotConstant. + +Ltac coerce_to_almost_ring set ext rspec := + match type of rspec with + | ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec) + | semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec) + | almost_ring_theory _ _ _ _ _ _ _ => rspec + | _ => fail 1 "not a valid ring theory" + end. + +Ltac coerce_to_ring_ext ext := + match type of ext with + | ring_eq_ext _ _ _ _ => ext + | sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext) + | _ => fail 1 "not a valid ring_eq_ext theory" + end. + +Ltac abstract_ring_morphism set ext rspec := + match type of rspec with + | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec) + | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec) + | almost_ring_theory _ _ _ _ _ _ _ => + constr:(gen_phiNword_morph set ext rspec) + | _ => fail 1 "bad ring structure" + end. + +Record hypo : Type := mkhypo { + hypo_type : Type; + hypo_proof : hypo_type + }. + +Ltac gen_ring_pow set arth pspec := + match pspec with + | None => + match type of arth with + | @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req => + constr:(mkhypo (@pow_N_th R rI rmul req set)) + | _ => fail 1 "gen_ring_pow" + end + | Some ?t => constr:(t) + end. + +Ltac gen_ring_sign morph sspec := + match sspec with + | None => + match type of morph with + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi => + constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th) + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi => + constr:(mkhypo (@get_sign_None_th C copp ceqb)) + | _ => fail 2 "ring anomaly : default_sign_spec" + end + | Some ?t => constr:(t) + end. + +Ltac default_div_spec set reqe arth morph := + match type of morph with + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + Z ?c0 ?c1 Zplus Zmult ?csub ?copp ?ceq_b ?phi => + constr:(mkhypo (Ztriv_div_th set phi)) + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + N ?c0 ?c1 Nplus Nmult ?csub ?copp ?ceq_b ?phi => + constr:(mkhypo (Ntriv_div_th set phi)) + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => + constr:(mkhypo (triv_div_th set reqe arth morph)) + | _ => fail 1 "ring anomaly : default_sign_spec" + end. + +Ltac gen_ring_div set reqe arth morph dspec := + match dspec with + | None => default_div_spec set reqe arth morph + | Some ?t => constr:(t) + end. + +Ltac ring_elements set ext rspec pspec sspec dspec rk := + let arth := coerce_to_almost_ring set ext rspec in + let ext_r := coerce_to_ring_ext ext in + let morph := + match rk with + | Abstract => abstract_ring_morphism set ext rspec + | @Computational ?reqb_ok => + match type of arth with + | almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ => + constr:(IDmorph rO rI add mul sub opp set _ reqb_ok) + | _ => fail 2 "ring anomaly" + end + | @Morphism ?m => + match type of m with + | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m + | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ => + constr:(SRmorph_Rmorph set m) + | _ => fail 2 "ring anomaly" + end + | _ => fail 1 "ill-formed ring kind" + end in + let p_spec := gen_ring_pow set arth pspec in + let s_spec := gen_ring_sign morph sspec in + let d_spec := gen_ring_div set ext_r arth morph dspec in + fun f => f arth ext_r morph p_spec s_spec d_spec. + +(* Given a ring structure and the kind of morphism, + returns 2 lemmas (one for ring, and one for ring_simplify). *) + + Ltac ring_lemmas set ext rspec pspec sspec dspec rk := + let gen_lemma2 := + match pspec with + | None => constr:(ring_rw_correct) + | Some _ => constr:(ring_rw_pow_correct) + end in + ring_elements set ext rspec pspec sspec dspec rk + ltac:(fun arth ext_r morph p_spec s_spec d_spec => + match type of morph with + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => + let gen_lemma2_0 := + constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth + C c0 c1 cadd cmul csub copp ceq_b phi morph) in + match p_spec with + | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec => + let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in + match d_spec with + | @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec => + let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in + match s_spec with + | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec => + let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in + let lemma1 := + constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in + fun f => f arth ext_r morph lemma1 lemma2 + | _ => fail 4 "ring: bad sign specification" + end + | _ => fail 3 "ring: bad coefficiant division specification" + end + | _ => fail 2 "ring: bad power specification" + end + | _ => fail 1 "ring internal error: ring_lemmas, please report" + end). + +(* Tactic for constant *) +Ltac isnatcst t := + match t with + O => constr:true + | S ?p => isnatcst p + | _ => constr:false + end. + +Ltac isPcst t := + match t with + | xI ?p => isPcst p + | xO ?p => isPcst p + | xH => constr:true + (* nat -> positive *) + | P_of_succ_nat ?n => isnatcst n + | _ => constr:false + end. + +Ltac isNcst t := + match t with + N0 => constr:true + | Npos ?p => isPcst p + | _ => constr:false + end. + +Ltac isZcst t := + match t with + Z0 => constr:true + | Zpos ?p => isPcst p + | Zneg ?p => isPcst p + (* injection nat -> Z *) + | Z_of_nat ?n => isnatcst n + (* injection N -> Z *) + | Z_of_N ?n => isNcst n + (* *) + | _ => constr:false + end. + + + + + -- cgit v1.2.3