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.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy 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.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy 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
intros E.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
E: 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
eapply Quoting.eval_eqquote.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
E: 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))
Quoting.eval R (Quoting.merge R l l')
  (Quoting.expr_map inl (Quoting.eqquote_l R)) =
Quoting.eval R (Quoting.merge R l l')
  (Quoting.eqquote_r R)
etransitivity;[symmetry;apply (eval_toPol _)|].C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
E: 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))
eval phi (Quoting.merge R l l')
  (toPol (Quoting.expr_map inl (Quoting.eqquote_l R))) =
Quoting.eval R (Quoting.merge R l l')
  (Quoting.eqquote_r R)
etransitivity;[|apply (eval_toPol _)].C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
E: 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))
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))
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.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
(toPol (Quoting.expr_map inl (Quoting.eqquote_l R)) =?
 toPol (Quoting.eqquote_r R)) = true -> n = m
Proof.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
(toPol (Quoting.expr_map inl (Quoting.eqquote_l R)) =?
 toPol (Quoting.eqquote_r R)) = true -> n = m
intros E.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
E: (toPol
   (Quoting.expr_map inl (Quoting.eqquote_l R)) =?
 toPol (Quoting.eqquote_r R)) = true
n = m
apply normalize_eq.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
l: V -> R
n, m: R
V': Type0
l': V' -> R
Q: Quoting.EqQuote R l n m l'
Vlt: Relation V
H1: Trichotomy Vlt
Vlt': Relation V'
H2: Trichotomy Vlt'
E: (toPol
   (Quoting.expr_map inl (Quoting.eqquote_l R)) =?
 toPol (Quoting.eqquote_r R)) = true
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))
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.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
Vlt: Relation V
H1: Trichotomy Vlt
a, b: Quoting.Expr V
vs: V -> R
eval phi vs (toPol a) = eval phi vs (toPol b) ->
Quoting.eval R vs a = Quoting.eval R vs b
Proof.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
Vlt: Relation V
H1: Trichotomy Vlt
a, b: Quoting.Expr V
vs: V -> R
eval phi vs (toPol a) = eval phi vs (toPol b) ->
Quoting.eval R vs a = Quoting.eval R vs b
rewrite !(eval_toPol _).C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
Vlt: Relation V
H1: Trichotomy Vlt
a, b: Quoting.Expr V
vs: V -> R
Quoting.eval R vs a = Quoting.eval R vs b ->
Quoting.eval R vs a = Quoting.eval R vs b
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.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
Vlt: Relation V
H1: Trichotomy Vlt
a, b: Quoting.Expr V
vs: V -> R
(toPol a =? toPol b) = true ->
Quoting.eval R vs a = Quoting.eval R vs b
Proof.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
Vlt: Relation V
H1: Trichotomy Vlt
a, b: Quoting.Expr V
vs: V -> R
(toPol a =? toPol b) = true ->
Quoting.eval R vs a = Quoting.eval R vs b
intros.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
Vlt: Relation V
H1: Trichotomy Vlt
a, b: Quoting.Expr V
vs: V -> R
X: (toPol a =? toPol b) = true
Quoting.eval R vs a = Quoting.eval R vs b
apply normalize_prequoted.C: Type
H: DecidablePaths C
R: Type
phi: C -> R
Aplus: Plus C
Bplus: Plus R
Amult: Mult C
Bmult: Mult R
Azero: Zero C
Bzero: Zero R
Aone: One C
Bone: One R
Aneg: AlmostNegate C
Bneg: AlmostNegate R
H0: AlmostRingPreserving phi
AlmostRing0: AlmostRing C
AlmostRing1: AlmostRing R
V: Type0
Vlt: Relation V
H1: Trichotomy Vlt
a, b: Quoting.Expr V
vs: V -> R
X: (toPol a =? toPol b) = true
eval phi vs (toPol a) = eval phi vs (toPol b)
apply eval_eqb;trivial.
Qed.

End content.

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

Instance negate_almostneg `{Aneg : Negate A} : AlmostNegate A
  := (-).
Arguments negate_almostneg _ _ _ /.

Instance semiring_almostring `{IsSemiCRing A} : AlmostRing A | 10.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
H: IsSemiCRing A
AlmostRing A
Proof.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
H: IsSemiCRing A
AlmostRing A
split;try exact _.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
H: IsSemiCRing A
forall x : A, almost_negate x = almost_negate 1 * x
intros.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
H: IsSemiCRing A
x: A
almost_negate x = almost_negate 1 * x unfold almost_negate;simpl.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
H: IsSemiCRing A
x: A
0 = 0 * x
symmetry;apply mult_0_l.
Qed.

Instance ring_almostring `{IsCRing A} : AlmostRing A.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
AlmostRing A
Proof.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
AlmostRing A
split;try exact _.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
forall x : A, almost_negate x = almost_negate 1 * x
intros.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
x: A
almost_negate x = almost_negate 1 * x unfold almost_negate;simpl.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
x: A
- x = -1 * x
apply negate_mult_l.
Qed.

Instance sr_mor_almostring_mor `{IsSemiRingPreserving A B f}
  : AlmostRingPreserving f | 10.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
AlmostRingPreserving f
Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
AlmostRingPreserving f
split;try exact _.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
forall x : A,
f (almost_negate x) = almost_negate (f x)
unfold almost_negate;simpl.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
A -> f 0 = 0 intros _.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 0 = 0 exact preserves_0.
Qed.

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

#[export] Instance ring_mor_almostring_mor : AlmostRingPreserving f.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsCRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving f
AlmostRingPreserving f
Proof.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsCRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving f
AlmostRingPreserving f
split;try exact _.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsCRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving f
forall x : A,
f (almost_negate x) = almost_negate (f x)
unfold almost_negate;simpl.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsCRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving f
forall x : A, f (- x) = - f x exact 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.