Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Cring.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 Export List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Export Morphisms Setoid Bool.
Require Import ZArith_base.
Require Export Algebra_syntax.
Require Export Ncring.
Require Export Ncring_initial.
Require Export Ncring_tac.

Class Cring {R:Type}`{Rr:Ring R} :=
cring_mul_comm: forall x y:R, x * y == y * x.

Ltac reify_goal lvar lexpr lterm:=
  (*idtac lvar; idtac lexpr; idtac lterm;*)
  match lexpr with
     nil => idtac
   | ?e1::?e2::_ =>
        match goal with
          |- (?op ?u1 ?u2) =>
           change (op
             (@Ring_polynom.PEeval
               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
               (@Ring_theory.pow_N _ 1 multiplication) lvar e1)
             (@Ring_polynom.PEeval
               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
               (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
        end
  end.

Section cring.
Context {R:Type}`{Rr:Cring R}.

Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.
Proof.
intros. apply mk_reqe; solve_proper.
Defined.

Lemma cring_almost_ring_theory:
   almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.
intros. apply mk_art ;intros.
rewrite ring_add_0_l; reflexivity.
rewrite ring_add_comm; reflexivity.
rewrite ring_add_assoc; reflexivity.
rewrite ring_mul_1_l; reflexivity.
apply ring_mul_0_l.
rewrite cring_mul_comm; reflexivity.
rewrite ring_mul_assoc; reflexivity.
rewrite ring_distr_l; reflexivity.
rewrite ring_opp_mul_l; reflexivity.
apply ring_opp_add.
rewrite ring_sub_def ; reflexivity. Defined.

Lemma cring_morph:
  ring_morph  zero one _+_ _*_ _-_ -_ _==_
             0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
             Ncring_initial.gen_phiZ.
intros. apply mkmorph ; intros; simpl; try reflexivity.
rewrite Ncring_initial.gen_phiZ_add; reflexivity.
rewrite ring_sub_def. unfold Z.sub. rewrite Ncring_initial.gen_phiZ_add.
rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
rewrite Ncring_initial.gen_phiZ_mul; reflexivity.
rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
rewrite (Zeqb_ok x y H). reflexivity. Defined.

Lemma cring_power_theory :
  @Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n)
  (@Ring_theory.pow_N _  1 multiplication).
intros; apply Ring_theory.mkpow_th. reflexivity. Defined.

Lemma cring_div_theory:
  div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem.
intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
simpl.   apply ring_setoid. Defined.

End cring.

Ltac cring_gen :=
  match goal with
    |- ?g => let lterm := lterm_goal g in
        match eval red in (list_reifyl (lterm:=lterm)) with
          | (?fv, ?lexpr) =>
           (*idtac "variables:";idtac fv;
           idtac "terms:"; idtac lterm;
           idtac "reifications:"; idtac lexpr; *)
           reify_goal fv lexpr lterm;
           match goal with
             |- ?g =>
               generalize
                 (@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_
                        ring_setoid
                        cring_eq_ext
                        cring_almost_ring_theory
                        Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
                        Ncring_initial.gen_phiZ
                        cring_morph
                        N
                        (fun n:N => n)
                        (@Ring_theory.pow_N _  1 multiplication)
                        cring_power_theory
                        Z.quotrem
                        cring_div_theory
                        O fv nil);
                 let rc := fresh "rc"in
                   intro rc; apply rc
           end
        end
  end.

Ltac cring_compute:= vm_compute; reflexivity.

Ltac cring:=
  intros;
  cring_gen;
  cring_compute.

Instance Zcri: (Cring (Rr:=Zr)).
red. exact Z.mul_comm. Defined.

(* Cring_simplify *)

Ltac cring_simplify_aux lterm fv lexpr hyp :=
    match lterm with
      | ?t0::?lterm =>
    match lexpr with
      | ?e::?le =>
        let t := constr:(@Ring_polynom.norm_subst
          Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.quotrem O nil e) in
        let te :=
          constr:(@Ring_polynom.Pphi_dev
            _ 0 1 _+_ _*_ _-_ -_

            Z 0%Z 1%Z Zeq_bool
            Ncring_initial.gen_phiZ
            get_signZ fv t) in
        let eq1 := fresh "ring" in
        let nft := eval vm_compute in t in
        let t':= fresh "t" in
        pose (t' := nft);
        assert (eq1 : t = t');
        [vm_cast_no_check (eq_refl t')|
        let eq2 := fresh "ring" in
        assert (eq2:(@Ring_polynom.PEeval
          _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
          (@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
        [let eq3 := fresh "ring" in
          generalize (@ring_rw_correct _ 0 1 _+_ _*_ _-_ -_ _==_
            ring_setoid
            cring_eq_ext
            cring_almost_ring_theory
            Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
            Ncring_initial.gen_phiZ
            cring_morph
            N
            (fun n:N => n)
            (@Ring_theory.pow_N _ 1 multiplication)
            cring_power_theory
            Z.quotrem
            cring_div_theory
            get_signZ get_signZ_th
            O nil fv I nil (eq_refl nil) );
          intro eq3; apply eq3; reflexivity|
              match hyp with
                | 1%nat => rewrite eq2
                | ?H => try rewrite eq2 in H
              end];
        let P:= fresh "P" in
        match hyp with
          | 1%nat =>
            rewrite eq1;
            pattern (@Ring_polynom.Pphi_dev
            _ 0 1 _+_ _*_ _-_ -_

            Z 0%Z 1%Z Zeq_bool
            Ncring_initial.gen_phiZ
            get_signZ fv t');
            match goal with
              |- (?p ?t) => set (P:=p)
            end;
              unfold t' in *; clear t' eq1 eq2;
              unfold Pphi_dev, Pphi_avoid; simpl;
                repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
                  mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
                  mkpow;simpl)
          | ?H =>
               rewrite eq1 in H;
               pattern (@Ring_polynom.Pphi_dev
            _ 0 1 _+_ _*_ _-_ -_

            Z 0%Z 1%Z Zeq_bool
            Ncring_initial.gen_phiZ
            get_signZ fv t') in H;
               match type of H with
                  | (?p ?t)  => set (P:=p) in H
               end;
               unfold t' in *; clear t' eq1 eq2;
               unfold Pphi_dev, Pphi_avoid in H; simpl in H;
                repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
                  mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
                  mkpow in H;simpl in H)
        end; unfold P in *; clear P
        ]; cring_simplify_aux lterm fv le hyp
      | nil => idtac
    end
    | nil => idtac
    end.

Ltac set_variables fv :=
  match fv with
    | nil => idtac
    | ?t::?fv =>
        let v := fresh "X" in
        set (v:=t) in *; set_variables fv
  end.

Ltac deset n:=
   match n with
    | 0%nat => idtac
    | S ?n1 =>
      match goal with
        | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1
      end
   end.

(* a est soit un terme de l'anneau, soit une liste de termes.
J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list
dans Tactic Notation *)

Ltac cring_simplify_gen a hyp :=
  let lterm :=
    match a with
      | _::_ => a
      | _ => constr:(a::nil)
    end in
    match eval red in (list_reifyl (lterm:=lterm)) with
      | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
      let n := eval compute in (length fv) in
      idtac n;
      let lt:=fresh "lt" in
      set (lt:= lterm);
      let lv:=fresh "fv" in
      set (lv:= fv);
      (* les termes de fv sont remplacés par des variables
         pour pouvoir utiliser simpl ensuite sans risquer
         des simplifications indésirables *)
      set_variables fv;
      let lterm1 := eval unfold lt in lt in
      let lv1 := eval unfold lv in lv in
        idtac lterm1; idtac lv1;
      cring_simplify_aux lterm1 lv1 lexpr hyp;
      clear lt lv;
      (* on remet les termes de fv *)
      deset n
    end.

Tactic Notation "cring_simplify" constr(lterm):=
cring_simplify_gen lterm 1%nat.

Tactic Notation "cring_simplify" constr(lterm) "in" ident(H):=
cring_simplify_gen lterm H.

¤ Dauer der Verarbeitung: 0.3 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.