(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* constr:(t1::t2::nil) | ring_eq ?t1 ?t2 -> ?g => let lvar := lterm_goal g in constr:(t1::t2::lvar) end. Ltac reify_goal lvar lexpr lterm:= (* idtac lvar; idtac lexpr; idtac lterm;*) match lexpr with nil => idtac | ?e::?lexpr1 => match lterm with ?t::?lterm1 => (* idtac "t="; idtac t;*) let x := fresh "T" in set (x:= t); change x with (@PEeval Z Zr _ _ (@gen_phiZ_morph _ _) N (fun n:N => n) (@Ring_theory.pow_N _ ring1 ring_mult) lvar e); clear x; reify_goal lvar lexpr1 lterm1 end end. Existing Instance gen_phiZ_morph. Existing Instance Zr. Lemma comm: forall (R:Type)(Rr:Ring R)(c : Z) (x : R), x * [c] == [c] * x. induction c. intros. ring_simpl. gen_ring_rewrite. simpl. intros. ring_rewrite_rev same_gen. induction p. simpl. gen_ring_rewrite. ring_rewrite IHp. rrefl. simpl. gen_ring_rewrite. ring_rewrite IHp. rrefl. simpl. gen_ring_rewrite. simpl. intros. ring_rewrite_rev same_gen. induction p. simpl. generalize IHp. clear IHp. gen_ring_rewrite. intro IHp. ring_rewrite IHp. rrefl. simpl. generalize IHp. clear IHp. gen_ring_rewrite. intro IHp. ring_rewrite IHp. rrefl. simpl. gen_ring_rewrite. Qed. Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. intros x y H. rewrite (Zeq_bool_eq x y H). rrefl. Qed. Ltac ring_gen := match goal with |- ?g => let lterm := lterm_goal g in (* les variables *) 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 => set_ring_notations; apply (@ring_correct Z Zr _ _ (@gen_phiZ_morph _ _) (@comm _ _) Zeq_bool Zeqb_ok N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication)); [apply mkpow_th; rrefl |vm_compute; reflexivity] end end end. Ltac ring2:= unset_ring_notations; intros; match goal with |- (@ring_eq ?r ?rd _ _ ) => simpl; ring_gen end. Variable R: Type. Variable Rr: Ring R. Existing Instance Rr. Goal forall x y z:R, x == x . ring2. Qed. Goal forall x y z:R, x * y * z == x * (y * z). ring2. Qed. Goal forall x y z:R, [3]* x *([2]* y * z) == [6] * (x * y) * z. ring2. Qed. Goal forall x y z:R, 3 * x * (2 * y * z) == 6 * (x * y) * z. ring2. Qed. (* Fails with Multiplication: A -> B -> C. Goal forall x:R, 2%Z * (x * x) == 3%Z * x. Admitted. *)