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.
Ltac reify_as_var_aux n lvar term :=
lazymatch lvar with
| @cons _ ?t0 ?tl =>
let conv :=
match goal with
| _ => let _ := match goal with _ => convert term t0 end in open_constr:(true)
| _ => open_constr:(false)
end
in
match conv with
| true => n
| false => reify_as_var_aux open_constr:(S n) tl term
end
| _ =>
let _ := open_constr:(eq_refl : lvar = @cons _ term _) in
n
end.
Ltac reify_as_var lvar term := reify_as_var_aux Datatypes.O lvar term.
Ltac close_varlist lvar :=
match lvar with
| @nil _ => idtac
| @cons _ _ ?tl => close_varlist tl
| _ => let _ := constr:(eq_refl : lvar = @nil _) in idtac
end.
Ltac extra_reify term := open_constr:((false,tt)).
Ltac reify_term Tring lvar term :=
match open_constr:((Tring, term)) with
| (_, Z0) => open_constr:(PEc 0%Z)
| (_, Zpos ?p) => open_constr:(PEc (Zpos p))
| (_, Zneg ?p) => open_constr:(PEc (Zneg p))
| (Ring (ring0:=?op), _) =>
let _ := match goal with _ => convert op term end in
open_constr:(PEc 0%Z)
| (Ring (ring1:=?op), _) =>
let _ := match goal with _ => convert op term end in
open_constr:(PEc 1%Z)
| (Ring (T:=?R) (add:=?add) (mul:=?mul) (sub:=?sub), ?op ?t1 ?t2) =>
let _ := open_constr:(t1 : R) in
let _ := open_constr:(t2 : R) in
match tt with
| _ =>
let _ := match goal with _ => convert add op end in
let et1 := reify_term Tring lvar t1 in
let et2 := reify_term Tring lvar t2 in
open_constr:(PEadd et1 et2)
| _ =>
let _ := match goal with _ => convert mul op end in
let et1 := reify_term Tring lvar t1 in
let et2 := reify_term Tring lvar t2 in
open_constr:(PEmul et1 et2)
| _ =>
let _ := match goal with _ => convert sub op end in
let et1 := reify_term Tring lvar t1 in
let et2 := reify_term Tring lvar t2 in
open_constr:(PEsub et1 et2)
end
| (Ring (T:=?R) (opp:=?opp), ?op ?t) =>
let _ := match goal with _ => convert opp op end in
let et := reify_term Tring lvar t in
open_constr:(PEopp et)
| (_, @multiplication Z _ _ ?z ?t) =>
let et := reify_term Tring lvar t in
open_constr:(PEmul (PEc z) et)
| (_, pow_N ?t ?n) =>
let et := reify_term Tring lvar t in
open_constr:(PEpow et n)
| (_, @power _ _ power_ring ?t ?n) =>
let et := reify_term Tring lvar t in
open_constr:(PEpow et (ZN n))
| _ =>
let extra := extra_reify term in
lazymatch extra with
| (false,_) =>
let n := reify_as_var lvar term in
open_constr:(PEX Z (Pos.of_succ_nat n))
| (true,?v) => v
end
end.
Ltac list_reifyl_core Tring lvar lterm :=
match lterm with
| @nil _ => open_constr:(@nil (PExpr Z))
| @cons _ ?t ?tl =>
let et := reify_term Tring lvar t in
let etl := list_reifyl_core Tring lvar tl in
open_constr:(@cons (PExpr Z) et etl)
end.
Ltac list_reifyl lvar lterm :=
match lterm with
| @cons ?R _ _ =>
let R_ring := constr:(_ :> Ring (T:=R)) in
let Tring := type of R_ring in
let lexpr := list_reifyl_core Tring lvar lterm in
let _ := match goal with _ => close_varlist lvar end in
constr:((lvar,lexpr))
end.
Ltac list_reifyl0 lterm :=
match lterm with
| @cons ?R _ _ =>
let lvar := open_constr:(_ :> list R) in
list_reifyl lvar lterm
end.
Class ReifyL {R:Type} (lvar lterm : list R) := list_reifyl : (list R * list (PExpr Z)).
Arguments list_reifyl {R lvar lterm _}.
Global Hint Extern 0 (ReifyL ?lvar ?lterm) => let reif := list_reifyl lvar lterm in exact reif : typeclass_instances.
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
let reif := list_reifyl0 lterm in
match reif 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
let reif := list_reifyl0 lterm in
match reif 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.