ring_tac.v

Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.tactics.ring_quote
  HoTT.Classes.tactics.ring_pol
  HoTT.Classes.theory.rings
  HoTT.Classes.orders.sum
  HoTT.Classes.interfaces.naturals
  HoTT.Classes.interfaces.integers.


Generalizable Variables A B C R V f l n m Vlt.


Import Quoting.Instances.


Section content.

Context `{DecidablePaths C}.


Context `(phi : C -> R) `{AlmostRingPreserving C R phi}
  `{!AlmostRing C} `{!AlmostRing R}.


Lemma normalize_eq `{Q : @Quoting.EqQuote R _ _ _ _ _ V l n m V' l'}
  `{Trichotomy V Vlt} `{Trichotomy V' Vlt'}
  : eval phi (Quoting.merge R l l')
  (toPol (Quoting.expr_map inl (Quoting.eqquote_l R)))
  = eval phi (Quoting.merge R l l') (toPol (Quoting.eqquote_r R))
  -> n = m.

Proof.

intros E.

eapply Quoting.eval_eqquote.

etransitivity;[symmetry;apply (eval_toPol _)|].

etransitivity;[|apply (eval_toPol _)].

exact E.

Qed.


Lemma by_quoting `{Q : @Quoting.EqQuote R _ _ _ _ _ V l n m V' l'}
  `{Trichotomy V Vlt} `{Trichotomy V' Vlt'}
  : toPol (Quoting.expr_map inl (@Quoting.eqquote_l R _ _ _ _ _ _ _ _ _ _ _ Q))
  =? toPol (@Quoting.eqquote_r R  _ _ _ _ _ _ _ _ _ _ _ Q) = true
  -> n = m.

Proof.

intros E.

apply normalize_eq.

apply eval_eqb,E.

Qed.


Lemma normalize_prequoted `{Trichotomy V Vlt} (a b : Quoting.Expr V) vs
  : eval phi vs (toPol a) = eval phi vs (toPol b) ->
  Quoting.eval _ vs a = Quoting.eval _ vs b.

Proof.

rewrite !(eval_toPol _).

trivial.

Qed.


Lemma prove_prequoted `{Trichotomy V Vlt} (a b : Quoting.Expr V) vs
  : toPol a =? toPol b = true -> Quoting.eval _ vs a = Quoting.eval _ vs b.

Proof.

intros.

apply normalize_prequoted.

apply eval_eqb;trivial.

Qed.


End content.


Global Instance default_almostneg `{Zero A} : AlmostNegate A | 20
  := fun _ => 0.

Arguments default_almostneg _ _ _ /.


Global Instance negate_almostneg `{Aneg : Negate A} : AlmostNegate A
  := (-).

Arguments negate_almostneg _ _ _ /.


Global Instance semiring_almostring `{IsSemiCRing A} : AlmostRing A | 10.

Proof.

split;try apply _.

intros.

 unfold almost_negate;simpl.

symmetry;apply mult_0_l.

Qed.


Global Instance ring_almostring `{IsCRing A} : AlmostRing A.

Proof.

split;try apply _.

intros.

 unfold almost_negate;simpl.

apply negate_mult_l.

Qed.


Global Instance sr_mor_almostring_mor `{IsSemiRingPreserving A B f}
  : AlmostRingPreserving f | 10.

Proof.

split;try apply _.

unfold almost_negate;simpl.

 intros _.

 apply preserves_0.

Qed.


Section VarSec.

Context `{IsCRing A} `{IsCRing B} {f : A -> B} `{!IsSemiRingPreserving f}.


Global Instance ring_mor_almostring_mor : AlmostRingPreserving f.

Proof.

split;try apply _.

unfold almost_negate;simpl.

 apply preserves_negate.

Qed.


End VarSec.


Arguments normalize_eq {C _ R} phi
  {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _} _.

Arguments by_quoting {C _ R} phi
  {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _} _.


Ltac ring_with_nat :=
  match goal with
  |- @paths ?R _ _ =>
    ((pose proof (_ : IsSemiCRing R)) || fail "target equality not on a semiring");
    apply (by_quoting (naturals_to_semiring nat R));
    reflexivity
  end.


Ltac ring_with_integers Z :=
  match goal with
  |- @paths ?R _ _ =>
    ((pose proof (_ : IsCRing R)) || fail "target equality not on a ring");
    apply (by_quoting (integers_to_ring Z R));
    reflexivity
  end.


Ltac ring_with_self :=
  match goal with
  |- @paths ?R _ _ =>
    ((pose proof (_ : IsSemiCRing R)) || fail "target equality not on a ring");
    apply (by_quoting (@id R));
    reflexivity
  end.


Ltac ring_repl a b :=
  let Hrw := fresh "Hrw" in
  assert (Hrw : a = b);[ring_with_nat|rewrite Hrw;clear Hrw].


Tactic Notation "ring_replace" constr(x) "with" constr(y) := ring_repl x y.

Timings for ring_tac.v