Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: InitialRing.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Zbool.
Require Import BinInt.
Require Import BinNat.
Require Import Setoid.
Require Import Ring_theory.
Require Import Ring_polynom.
Import List.

Set Implicit Arguments.
(* Set Universe Polymorphism. *)

Import RingSyntax.

(* An object to return when an expression is not recognized as a constant *)
Definition NotConstant := false.

(** Z is a ring and a setoid*)

Lemma Zsth : Setoid_Theory Z (@eq Z).
Proof (Eqsth Z).

Lemma Zeqe : ring_eq_ext Z.add Z.mul Z.opp (@eq Z).
Proof (Eq_ext Z.add Z.mul Z.opp).

Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).
Proof.
constructor. exact Z.add_0_l. exact Z.add_comm. exact Z.add_assoc.
exact Z.mul_1_l. exact Z.mul_comm. exact Z.mul_assoc.
exact Z.mul_add_distr_r. trivial. exact Z.sub_diag.
Qed.

(** Two generic morphisms from Z to (abrbitrary) rings, *)
(**second one is more convenient for proofs but they are ext. equal*)
Section ZMORPHISM.
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 Parametric Relation : R req
       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
      as R_setoid3.
     Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
   Proof. exact (Radd_ext Reqe). Qed.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
   Proof. exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp with signature (req ==> req) as ropp_ext3.
   Proof. 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 Z.opp Zeq_bool get_signZ.
Proof.
  constructor.
  destruct c;intros;try discriminate.
  injection H as <-.
  simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
Qed.

Section ALMOST_RING.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3.
   Proof. 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 (Pos.succ 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 Pos.add_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 with signature (req ==> req ==> req) as rsub_ext4.
   Proof. 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 extensionally 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_pos_sub : forall x y,
gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
Proof.
  intros x y.
  rewrite Z.pos_sub_spec.
  case Pos.compare_spec; intros H; simpl.
  rewrite H. rewrite (Ropp_def Rth);rrefl.
  rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
  rewrite (ARgen_phiPOS_add ARth);simpl;norm.
  rewrite (Ropp_def Rth);norm.
  rewrite <- (Pos.sub_add x y H) at 2.
  rewrite (ARgen_phiPOS_add ARth);simpl;norm.
  add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
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.
  destruct x, y; simpl; norm.
  apply (ARgen_phiPOS_add ARth).
  apply gen_phiZ1_pos_sub.
  rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
  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)
   Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ.
Proof.
  assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH)
                  Z.add Z.mul 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 N.add N.mul (@eq N).
Proof (Eq_s_ext N.add N.mul).

Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).
Proof.
constructor. exact N.add_0_l. exact N.add_comm. exact N.add_assoc.
exact N.mul_1_l. exact N.mul_0_l. exact N.mul_comm. exact N.mul_assoc.
exact N.mul_add_distr_r.
Qed.

Definition Nsub := SRsub N.add.
Definition Nopp := (@SRopp N).

Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
Proof (SReqe_Reqe Nseqe).

Lemma Nath :
almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).
Proof (SRth_ARth Nsth Nth).

Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.

(**Same as above : definition of two, extensionally 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 Parametric Relation : R req
       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
       transitivity proved by (@Equivalence_Transitive _ _ 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 with signature (req ==> req ==> req) as radd_ext4.
   Proof. exact (Radd_ext Reqe). Qed.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4.
   Proof. exact (Rmul_ext Reqe). Qed.
   Ltac norm := gen_srewrite_sr 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. reflexivity.
  now rewrite (same_gen Rsth Reqe ARth).
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
                           0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
Proof.
  constructor; simpl; try reflexivity.
  apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
  intros x y EQ. apply N.eqb_eq in EQ. now subst.
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 N.eqb 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 Parametric Relation : R req
       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
      as R_setoid5.
     Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
   Proof. exact (Radd_ext Reqe). Qed.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5.
   Proof. exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp with signature (req ==> req) as ropp_ext5.
   Proof. exact (Ropp_ext Reqe). Qed.

Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7.
   Proof. 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; intros; auto.
reflexivity.

destruct a.
  destruct w.
   reflexivity.

   rewrite IHw; 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; 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.
rewrite gen_phiNword_cons.
reflexivity.
Qed.

Lemma gen_phiNword_ok : forall w1 w2,
   Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
induction w1; intros.
simpl.
rewrite (gen_phiNword0_ok _ H).
reflexivity.

rewrite gen_phiNword_cons.
destruct w2.
  simpl in H.
  destruct a; try  discriminate.
  rewrite (gen_phiNword0_ok _ H).
  norm.

  simpl in H.
  rewrite gen_phiNword_cons.
  case_eq (N.eqb a n); intros H0.
   rewrite H0 in H.
   apply N.eqb_eq in H0. rewrite <- H0.
   rewrite (IHw1 _ H).
   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.
norm.

destruct y.
  simpl Nwadd; norm.

  simpl Nwadd.
  repeat rewrite gen_phiNword_cons.
  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) by
    (destruct Reqe; constructor; trivial).

  rewrite IHx.
  norm.
  add_push (- gen_phiNword x); reflexivity.
Qed.

Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
simpl.
unfold Nwopp; simpl.
intros.
rewrite gen_phiNword_Nwcons; 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.
repeat rewrite gen_phiNword_cons.
rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth))
   by (destruct Reqe; constructor; trivial).

  rewrite IHx.
  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.
  rewrite Nwopp_ok.
  rewrite IHx.
  rewrite gen_phiNword_cons.
  norm.

  simpl Nwmul.
  unfold Nwsub.
  rewrite Nwadd_ok.
  rewrite Nwscal_ok.
  rewrite Nwopp_ok.
  rewrite IHx.
  rewrite gen_phiNword_cons.
  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.
rewrite Nwadd_ok.
rewrite Nwopp_ok.
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 Parametric Relation : R req
    reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
    symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
    transitivity proved by (@Equivalence_Transitive _ _ Rsth)
   as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
  Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
  Proof. exact (Radd_ext Reqe). Qed.
  Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
  Proof. exact (Rmul_ext Reqe). Qed.
  Add Morphism ropp with signature (req ==> req) as ropp_ext.
  Proof. exact (Ropp_ext Reqe). Qed.
  Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
  Proof. 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_eq morph 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 Z.add Z.mul zphi Z.quotrem.
Proof.
  constructor.
  intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
  rewrite Z.mul_comm; rsimpl.
Qed.

Variable nphi : N -> R.

Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
  constructor.
  intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst.
  rewrite N.mul_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 reified 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 Z.add Z.mul ?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 N.add N.mul ?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 coefficient 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 *)
  | Pos.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.

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.