Library Coq.setoid_ring.Ncring_tac
Require Import List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Export Morphisms Setoid Bool.
Require Import ZArith.
Require Import Algebra_syntax.
Require Export Ncring.
Require Import Ncring_polynom.
Require Import Ncring_initial.
Set Implicit Arguments.
Class nth (R:Type) (t:R) (l:list R) (i:nat).
Instance Ifind0 (R:Type) (t:R) l
: nth t(t::l) 0.
Defined.
Instance IfindS (R:Type) (t2 t1:R) l i
{_:nth t1 l i}
: nth t1 (t2::l) (S i) | 1.
Defined.
Class closed (T:Type) (l:list T).
Instance Iclosed_nil T
: closed (T:=T) nil.
Defined.
Instance Iclosed_cons T t (l:list T)
{_:closed l}
: closed (t::l).
Defined.
Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R).
Instance reify_zero (R:Type) lvar op
`{Ring (T:=R)(ring0:=op)}
: reify (ring0:=op)(PEc 0%Z) lvar op.
Defined.
Instance reify_one (R:Type) lvar op
`{Ring (T:=R)(ring1:=op)}
: reify (ring1:=op) (PEc 1%Z) lvar op.
Defined.
Instance reifyZ0 (R:Type) lvar
`{Ring (T:=R)}
: reify (PEc Z0) lvar Z0|11.
Defined.
Instance reifyZpos (R:Type) lvar (p:positive)
`{Ring (T:=R)}
: reify (PEc (Zpos p)) lvar (Zpos p)|11.
Defined.
Instance reifyZneg (R:Type) lvar (p:positive)
`{Ring (T:=R)}
: reify (PEc (Zneg p)) lvar (Zneg p)|11.
Defined.
Instance reify_add (R:Type)
e1 lvar t1 e2 t2 op
`{Ring (T:=R)(add:=op)}
{_:reify (add:=op) e1 lvar t1}
{_:reify (add:=op) e2 lvar t2}
: reify (add:=op) (PEadd e1 e2) lvar (op t1 t2).
Defined.
Instance reify_mul (R:Type)
e1 lvar t1 e2 t2 op
`{Ring (T:=R)(mul:=op)}
{_:reify (mul:=op) e1 lvar t1}
{_:reify (mul:=op) e2 lvar t2}
: reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10.
Defined.
Instance reify_mul_ext (R:Type) `{Ring R}
lvar (z:Z) e2 t2
`{Ring (T:=R)}
{_:reify e2 lvar t2}
: reify (PEmul (PEc z) e2) lvar
(@multiplication Z _ _ z t2)|9.
Defined.
Instance reify_sub (R:Type)
e1 lvar t1 e2 t2 op
`{Ring (T:=R)(sub:=op)}
{_:reify (sub:=op) e1 lvar t1}
{_:reify (sub:=op) e2 lvar t2}
: reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2).
Defined.
Instance reify_opp (R:Type)
e1 lvar t1 op
`{Ring (T:=R)(opp:=op)}
{_:reify (opp:=op) e1 lvar t1}
: reify (opp:=op) (PEopp e1) lvar (op t1).
Defined.
Instance reify_pow (R:Type) `{Ring R}
e1 lvar t1 n
`{Ring (T:=R)}
{_:reify e1 lvar t1}
: reify (PEpow e1 n) lvar (pow_N t1 n)|1.
Defined.
Instance reify_var (R:Type) t lvar i
`{nth R t lvar i}
`{Rr: Ring (T:=R)}
: reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t
| 100.
Defined.
Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R)
(lterm:list R).
Instance reify_nil (R:Type) lvar
`{Rr: Ring (T:=R)}
: reifylist (Rr:= Rr) nil lvar (@nil R).
Defined.
Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2
`{Rr: Ring (T:=R)}
{_:reify (Rr:= Rr) e1 lvar t1}
{_:reifylist (Rr:= Rr) lexpr2 lvar lterm2}
: reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2).
Defined.
Definition list_reifyl (R:Type) lexpr lvar lterm
`{Rr: Ring (T:=R)}
{_:reifylist (Rr:= Rr) lexpr lvar lterm}
`{closed (T:=R) lvar} := (lvar,lexpr).
Unset Implicit Arguments.
Ltac lterm_goal g :=
match g with
| ?t1 == ?t2 => constr:(t1::t2::nil)
| ?t1 = ?t2 => constr:(t1::t2::nil)
| (_ ?t1 ?t2) => constr:(t1::t2::nil)
end.
Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
Ltac reify_goal lvar lexpr lterm:=
match lexpr with
nil => idtac
| ?e1::?e2::_ =>
match goal with
|- (?op ?u1 ?u2) =>
change (op
(@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
(fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
lvar e1)
(@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
(fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
lvar e2))
end
end.
Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R),
x * (gen_phiZ c) == (gen_phiZ c) * x.
Ltac ring_gen :=
match goal with
|- ?g => let lterm := lterm_goal g in
match eval red in (list_reifyl (lterm:=lterm)) with
| (?fv, ?lexpr) =>
reify_goal fv lexpr lterm;
match goal with
|- ?g =>
apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
(@gen_phiZ _ _ _ _ _ _ _ _ _) _
(@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n)
(@pow_N _ _ _ _ _ _ _ _ _));
[apply mkpow_th; reflexivity
|vm_compute; reflexivity]
end
end
end.
Ltac non_commutative_ring:=
intros;
ring_gen.
Ltac ring_simplify_aux lterm fv lexpr hyp :=
match lterm with
| ?t0::?lterm =>
match lexpr with
| ?e::?le =>
let t := constr:(@Ncring_polynom.norm_subst
Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z) Zops Zeq_bool e) in
let te :=
constr:(@Ncring_polynom.Pphi Z
_ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ 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:(@Ncring_polynom.PEeval Z
_ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
[apply (@Ncring_polynom.norm_subst_ok
Z _ 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z)
_ _ 0 1 _+_ _*_ _-_ -_ _==_ _ _ Ncring_initial.gen_phiZ _
(@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Zeqb_ok);
apply mkpow_th; 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 => idtac "ok";
rewrite eq1;
pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_
_ Ncring_initial.gen_phiZ fv t');
match goal with
|- (?p ?t) => set (P:=p)
end;
unfold t' in *; clear t' eq1 eq2; simpl
| ?H =>
rewrite eq1 in H;
pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_
_ Ncring_initial.gen_phiZ fv t') in H;
match type of H with
| (?p ?t) => set (P:=p) in H
end;
unfold t' in *; clear t' eq1 eq2; simpl in H
end; unfold P in *; clear P
]; ring_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.
Ltac ring_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);
set_variables fv;
let lterm1 := eval unfold lt in lt in
let lv1 := eval unfold lv in lv in
idtac lterm1; idtac lv1;
ring_simplify_aux lterm1 lv1 lexpr hyp;
clear lt lv;
deset n
end.
Tactic Notation "non_commutative_ring_simplify" constr(lterm):=
ring_simplify_gen lterm 1%nat.
Tactic Notation "non_commutative_ring_simplify" constr(lterm) "in" ident(H):=
ring_simplify_gen lterm H.