import tactic.norm_num

import control.traversable.basic

universes u

namespace tactic.ring_exp

open nat

meta structure atom : Type := (value : expr) (index : ℕ)

namespace atom

meta def eq (a b : atom) : bool := a.index = b.index

meta def lt (a b : atom) : bool := a.index < b.index

meta instance : has_repr atom := ⟨λ x, "(atom " ++ repr x.2 ++ ")"⟩

end atom

section expression

structure coeff : Type := (value : ℚ)

inductive ex_type : Type

| base : ex_type

| sum : ex_type

| prod : ex_type

| exp : ex_type

open ex_type

meta structure ex_info : Type :=

(orig : expr) (pretty : expr) (proof : option expr)

meta inductive ex : ex_type → Type

| zero (info : ex_info) : ex sum

| sum (info : ex_info) : ex prod → ex sum → ex sum

| coeff (info : ex_info) : coeff → ex prod

| prod (info : ex_info) : ex exp → ex prod → ex prod

| var (info : ex_info) : atom → ex base

| sum_b (info : ex_info) : ex sum → ex base

| exp (info : ex_info) : ex base → ex prod → ex exp

meta def ex.info : Π {et : ex_type} (ps : ex et), ex_info

| sum (ex.zero i) := i

| sum (ex.sum i _ _) := i

| prod (ex.coeff i _) := i

| prod (ex.prod i _ _) := i

| base (ex.var i _) := i

| base (ex.sum_b i _) := i

| exp (ex.exp i _ _) := i

meta def ex.orig {et : ex_type} (ps : ex et) : expr := ps.info.orig

meta def ex.pretty {et : ex_type} (ps : ex et) : expr := ps.info.pretty

meta def ex.proof {et : ex_type} (ps : ex et) : option expr := ps.info.proof

meta def ex_info.set (i : ex_info) (o : option expr) (pf : option expr) : ex_info :=

{orig := o.get_or_else i.pretty, proof := pf, .. i}

meta def ex.set_info : Π {et : ex_type} (ps : ex et), option expr → option expr → ex et

| sum (ex.zero i) o pf := ex.zero (i.set o pf)

| sum (ex.sum i p ps) o pf := ex.sum (i.set o pf) p ps

| prod (ex.coeff i x) o pf := ex.coeff (i.set o pf) x

| prod (ex.prod i p ps) o pf := ex.prod (i.set o pf) p ps

| base (ex.var i x) o pf := ex.var (i.set o pf) x

| base (ex.sum_b i ps) o pf := ex.sum_b (i.set o pf) ps

| exp (ex.exp i p ps) o pf := ex.exp (i.set o pf) p ps

instance coeff_has_repr : has_repr coeff := ⟨λ x, repr x.1⟩

meta def ex.repr : Π {et : ex_type}, ex et → string

| sum (ex.zero _) := "0"

| sum (ex.sum _ p ps) := ex.repr p ++ " + " ++ ex.repr ps

| prod (ex.coeff _ x) := repr x

| prod (ex.prod _ p ps) := ex.repr p ++ " * " ++ ex.repr ps

| base (ex.var _ x) := repr x

| base (ex.sum_b _ ps) := "(" ++ ex.repr ps ++ ")"

| exp (ex.exp _ p ps) := ex.repr p ++ " ^ " ++ ex.repr ps

meta instance {et : ex_type} : has_repr (ex et) := ⟨ex.repr⟩

meta def ex.eq : Π {et : ex_type}, ex et → ex et → bool

| sum (ex.zero _) (ex.zero _) := tt

| sum (ex.zero _) (ex.sum _ _ _) := ff

| sum (ex.sum _ _ _) (ex.zero _) := ff

| sum (ex.sum _ p ps) (ex.sum _ q qs) := p.eq q && ps.eq qs

| prod (ex.coeff _ x) (ex.coeff _ y) := x = y

| prod (ex.coeff _ _) (ex.prod _ _ _) := ff

| prod (ex.prod _ _ _) (ex.coeff _ _) := ff

| prod (ex.prod _ p ps) (ex.prod _ q qs) := p.eq q && ps.eq qs

| base (ex.var _ x) (ex.var _ y) := x.eq y

| base (ex.var _ _) (ex.sum_b _ _) := ff

| base (ex.sum_b _ _) (ex.var _ _) := ff

| base (ex.sum_b _ ps) (ex.sum_b _ qs) := ps.eq qs

| exp (ex.exp _ p ps) (ex.exp _ q qs) := p.eq q && ps.eq qs

meta def ex.lt : Π {et : ex_type}, ex et → ex et → bool

| sum _ (ex.zero _) := ff

| sum (ex.zero _) _ := tt

| sum (ex.sum _ p ps) (ex.sum _ q qs) := p.lt q || (p.eq q && ps.lt qs)

| prod (ex.coeff _ x) (ex.coeff _ y) := x.1 < y.1

| prod (ex.coeff _ _) _ := tt

| prod _ (ex.coeff _ _) := ff

| prod (ex.prod _ p ps) (ex.prod _ q qs) := p.lt q || (p.eq q && ps.lt qs)

| base (ex.var _ x) (ex.var _ y) := x.lt y

| base (ex.var _ _) (ex.sum_b _ _) := tt

| base (ex.sum_b _ _) (ex.var _ _) := ff

| base (ex.sum_b _ ps) (ex.sum_b _ qs) := ps.lt qs

| exp (ex.exp _ p ps) (ex.exp _ q qs) := p.lt q || (p.eq q && ps.lt qs)

end expression

section operations

variables {α : Type u} [comm_semiring α]

open tactic

open ex_type

meta structure eval_info :=

(α : expr) (univ : level)

(csr_instance : expr) (ha_instance : expr) (hm_instance : expr) (hp_instance : expr)

(ring_instance : option expr) (dr_instance : option expr)

(zero : expr) (one : expr)

meta structure context :=

(info_b : eval_info) (info_e : eval_info) (transp : transparency)

@[derive [monad, alternative]]

meta def ring_exp_m (α : Type) : Type := reader_t context (state_t (list atom) tactic) α

meta def get_context : ring_exp_m context := reader_t.read

meta def lift {α} (m : tactic α) : ring_exp_m α := reader_t.lift (state_t.lift m)

meta def in_exponent {α} (mx : ring_exp_m α) : ring_exp_m α := do

ctx ← get_context,

reader_t.lift $ mx.run ⟨ctx.info_e, ctx.info_e, ctx.transp⟩

meta def mk_app_class (f : name) (inst : expr) (args : list expr) : ring_exp_m expr := do

ctx ← get_context,

pure $ (@expr.const tt f [ctx.info_b.univ] ctx.info_b.α inst).mk_app args

meta def mk_app_csr (f : name) (args : list expr) : ring_exp_m expr := do

ctx ← get_context,

mk_app_class f (ctx.info_b.csr_instance) args

meta def mk_add (args : list expr) : ring_exp_m expr := do

ctx ← get_context,

mk_app_class ``has_add.add ctx.info_b.ha_instance args

meta def mk_mul (args : list expr) : ring_exp_m expr := do

ctx ← get_context,

mk_app_class ``has_mul.mul ctx.info_b.hm_instance args

meta def mk_pow (args : list expr) : ring_exp_m expr := do

ctx ← get_context,

pure $ (@expr.const tt ``has_pow.pow

[ctx.info_b.univ, ctx.info_e.univ]

ctx.info_b.α ctx.info_e.α

ctx.info_b.hp_instance).mk_app args

meta def ex_info.proof_term (ps : ex_info) : ring_exp_m expr :=

match ps.proof with

| none := lift $ tactic.mk_eq_refl ps.pretty

| (some p) := pure p

meta def ex.proof_term {et : ex_type} (ps : ex et) : ring_exp_m expr := ps.info.proof_term

meta def none_or_proof_term : list ex_info → ring_exp_m (option (list expr))

| [] := pure none

| (x :: xs) := do

xs_pfs ← none_or_proof_term xs,

match (x.proof, xs_pfs) with

| (none, none) := pure none

| (some x_pf, none) := do

xs_pfs ← traverse ex_info.proof_term xs,

pure (some (x_pf :: xs_pfs))

| (_, some xs_pfs) := do

x_pf ← x.proof_term,

pure (some (x_pf :: xs_pfs))

end

meta def mk_proof (lem : name) (args : list expr) (hs : list ex_info) : ring_exp_m expr := do

hs' ← traverse ex_info.proof_term hs,

mk_app_csr lem (args ++ hs')

meta def mk_proof_or_refl (term : expr) (lem : name) (args : list expr) (hs : list ex_info) :

ring_exp_m expr := do

hs_full ← none_or_proof_term hs,

match hs_full with

| none := lift $ mk_eq_refl term

| (some hs') := mk_app_csr lem (args ++ hs')

end

meta def add_orig {et et'} (ps : ex et) (qs : ex et') : ring_exp_m expr :=

mk_add [ps.orig, qs.orig]

meta def mul_orig {et et'} (ps : ex et) (qs : ex et') : ring_exp_m expr :=

mk_mul [ps.orig, qs.orig]

meta def pow_orig {et et'} (ps : ex et) (qs : ex et') : ring_exp_m expr :=

mk_pow [ps.orig, qs.orig]

lemma sum_congr {p p' ps ps' : α} : p = p' → ps = ps' → p + ps = p' + ps' := by cc

lemma prod_congr {p p' ps ps' : α} : p = p' → ps = ps' → p * ps = p' * ps' := by cc

lemma exp_congr {p p' : α} {ps ps' : ℕ} : p = p' → ps = ps' → p ^ ps = p' ^ ps' := by cc

meta def ex_zero : ring_exp_m (ex sum) := do

ctx ← get_context,

pure $ ex.zero ⟨ctx.info_b.zero, ctx.info_b.zero, none⟩

meta def ex_sum (p : ex prod) (ps : ex sum) : ring_exp_m (ex sum) := do

pps_o ← add_orig p ps,

pps_p ← mk_add [p.pretty, ps.pretty],

pps_pf ← mk_proof_or_refl pps_p ``sum_congr

[p.orig, p.pretty, ps.orig, ps.pretty]

[p.info, ps.info],

pure (ex.sum ⟨pps_o, pps_p, pps_pf⟩ (p.set_info none none) (ps.set_info none none))

meta def ex_coeff (x : rat) : ring_exp_m (ex prod) := do

ctx ← get_context,

x_p ← lift $ expr.of_rat ctx.info_b.α x,

pure (ex.coeff ⟨x_p, x_p, none⟩ ⟨x⟩)

meta def ex_one : ring_exp_m (ex prod) := do

ctx ← get_context,

pure $ ex.coeff ⟨ctx.info_b.one, ctx.info_b.one, none⟩ ⟨1⟩

meta def ex_prod (p : ex exp) (ps : ex prod) : ring_exp_m (ex prod) := do

pps_o ← mul_orig p ps,

pps_p ← mk_mul [p.pretty, ps.pretty],

pps_pf ← mk_proof_or_refl pps_p ``prod_congr

[p.orig, p.pretty, ps.orig, ps.pretty]

[p.info, ps.info],

pure (ex.prod ⟨pps_o, pps_p, pps_pf⟩ (p.set_info none none) (ps.set_info none none))

meta def ex_var (p : atom) : ring_exp_m (ex base) := pure (ex.var ⟨p.1, p.1, none⟩ p)

meta def ex_sum_b (ps : ex sum) : ring_exp_m (ex base) :=

pure (ex.sum_b ps.info (ps.set_info none none))

meta def ex_exp (p : ex base) (ps : ex prod) : ring_exp_m (ex exp) := do

ctx ← get_context,

pps_o ← pow_orig p ps,

pps_p ← mk_pow [p.pretty, ps.pretty],

pps_pf ← mk_proof_or_refl pps_p ``exp_congr

[p.orig, p.pretty, ps.orig, ps.pretty]

[p.info, ps.info],

pure (ex.exp ⟨pps_o, pps_p, pps_pf⟩ (p.set_info none none) (ps.set_info none none))

lemma base_to_exp_pf {p p' : α} : p = p' → p = p' ^ 1 := by simp

meta def base_to_exp (p : ex base) : ring_exp_m (ex exp) := do

o ← in_exponent $ ex_one,

ps ← ex_exp p o,

pf ← mk_proof ``base_to_exp_pf [p.orig, p.pretty] [p.info],

pure $ ps.set_info p.orig pf

lemma exp_to_prod_pf {p p' : α} : p = p' → p = p' * 1 := by simp

meta def exp_to_prod (p : ex exp) : ring_exp_m (ex prod) := do

o ← ex_one,

ps ← ex_prod p o,

pf ← mk_proof ``exp_to_prod_pf [p.orig, p.pretty] [p.info],

pure $ ps.set_info p.orig pf

lemma prod_to_sum_pf {p p' : α} : p = p' → p = p' + 0 := by simp

meta def prod_to_sum (p : ex prod) : ring_exp_m (ex sum) := do

z ← ex_zero,

ps ← ex_sum p z,

pf ← mk_proof ``prod_to_sum_pf [p.orig, p.pretty] [p.info],

pure $ ps.set_info p.orig pf

lemma atom_to_sum_pf (p : α) : p = p ^ 1 * 1 + 0 := by simp

meta def atom_to_sum (p : atom) : ring_exp_m (ex sum) := do

p' ← ex_var p,

o ← in_exponent $ ex_one,

p' ← ex_exp p' o,

o ← ex_one,

p' ← ex_prod p' o,

z ← ex_zero,

p' ← ex_sum p' z,

pf ← mk_proof ``atom_to_sum_pf [p.1] [],

pure $ p'.set_info p.1 pf

meta def add_coeff (p_p q_p : expr) (p q : coeff) : ring_exp_m (ex prod) := do

ctx ← get_context,

pq_o ← mk_add [p_p, q_p],

(pq_p, pq_pf) ← lift $ norm_num.eval_field pq_o,

pure $ ex.coeff ⟨pq_o, pq_p, pq_pf⟩ ⟨p.1 + q.1⟩

lemma mul_coeff_pf_one_mul (q : α) : 1 * q = q := one_mul q

lemma mul_coeff_pf_mul_one (p : α) : p * 1 = p := mul_one p

meta def mul_coeff (p_p q_p : expr) (p q : coeff) : ring_exp_m (ex prod) :=

match p.1, q.1 with -- Special case to speed up multiplication with 1.

| ⟨1, 1, _, _⟩, _ := do

ctx ← get_context,

pq_o ← mk_mul [p_p, q_p],

pf ← mk_app_csr ``mul_coeff_pf_one_mul [q_p],

pure $ ex.coeff ⟨pq_o, q_p, pf⟩ ⟨q.1⟩

| _, ⟨1, 1, _, _⟩ := do

ctx ← get_context,

pq_o ← mk_mul [p_p, q_p],

pf ← mk_app_csr ``mul_coeff_pf_mul_one [p_p],

pure $ ex.coeff ⟨pq_o, p_p, pf⟩ ⟨p.1⟩

| _, _ := do

ctx ← get_context,

pq' ← mk_mul [p_p, q_p],

(pq_p, pq_pf) ← lift $ norm_num.eval_field pq',

pure $ ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 * q.1⟩

section rewrite

meta def rewrite (ps_o : expr) (ps' : ex sum) (pf : expr) : ring_exp_m (ex sum) :=

ps'_pf ← ps'.info.proof_term,

pf ← lift $ mk_eq_trans pf ps'_pf,

pure $ ps'.set_info ps_o pf

end rewrite

meta inductive overlap : Type

| none : overlap

| nonzero : ex prod → overlap

| zero : ex sum → overlap

lemma add_overlap_pf {ps qs pq} (p : α) : ps + qs = pq → p * ps + p * qs = p * pq := λ pq_pf, calc

p * ps + p * qs = p * (ps + qs) : symm (mul_add _ _ _)

... = p * pq : by rw pq_pf

lemma add_overlap_pf_zero {ps qs} (p : α) : ps + qs = 0 → p * ps + p * qs = 0 := λ pq_pf, calc

p * ps + p * qs = p * (ps + qs) : symm (mul_add _ _ _)

... = p * 0 : by rw pq_pf

... = 0 : mul_zero _

meta def add_overlap : ex prod → ex prod → ring_exp_m overlap

| (ex.coeff x_i x) (ex.coeff y_i y) := do

xy@(ex.coeff _ xy_c) ← add_coeff x_i.pretty y_i.pretty x y

| lift $ fail "internal error: add_coeff should return ex.coeff",

if xy_c.1 = 0

then do

z ← ex_zero,

pure $ overlap.zero (z.set_info xy.orig xy.proof)

else pure $ overlap.nonzero xy

| (ex.prod _ _ _) (ex.coeff _ _) := pure overlap.none

| (ex.coeff _ _) (ex.prod _ _ _) := pure overlap.none

| pps@(ex.prod _ p ps) qqs@(ex.prod _ q qs) := if p.eq q

then do

pq_ol ← add_overlap ps qs,

pqs_o ← add_orig pps qqs,

match pq_ol with

| overlap.none := pure overlap.none

| (overlap.nonzero pq) := do

pqs ← ex_prod p pq,

pf ← mk_proof ``add_overlap_pf

[ps.pretty, qs.pretty, pq.pretty, p.pretty]

[pq.info],

pure $ overlap.nonzero (pqs.set_info pqs_o pf)

| (overlap.zero pq) := do

z ← ex_zero,

pf ← mk_proof ``add_overlap_pf_zero

[ps.pretty, qs.pretty, p.pretty]

[pq.info],

pure $ overlap.zero (z.set_info pqs_o pf)

end

else pure overlap.none

section addition

lemma add_pf_z_sum {ps qs qs' : α} : ps = 0 → qs = qs' → ps + qs = qs' := λ ps_pf qs_pf, calc

ps + qs = 0 + qs' : by rw [ps_pf, qs_pf]

... = qs' : zero_add _

lemma add_pf_sum_z {ps ps' qs : α} : ps = ps' → qs = 0 → ps + qs = ps' := λ ps_pf qs_pf, calc

ps + qs = ps' + 0 : by rw [ps_pf, qs_pf]

... = ps' : add_zero _

lemma add_pf_sum_overlap {pps p ps qqs q qs pq pqs : α} :

pps = p + ps → qqs = q + qs → p + q = pq → ps + qs = pqs → pps + qqs = pq + pqs := by cc

lemma add_pf_sum_overlap_zero {pps p ps qqs q qs pqs : α} :

pps = p + ps → qqs = q + qs → p + q = 0 → ps + qs = pqs → pps + qqs = pqs :=

λ pps_pf qqs_pf pq_pf pqs_pf, calc

pps + qqs = (p + ps) + (q + qs) : by rw [pps_pf, qqs_pf]

... = (p + q) + (ps + qs) : by cc

... = 0 + pqs : by rw [pq_pf, pqs_pf]

... = pqs : zero_add _

lemma add_pf_sum_lt {pps p ps qqs pqs : α} :

pps = p + ps → ps + qqs = pqs → pps + qqs = p + pqs := by cc

lemma add_pf_sum_gt {pps qqs q qs pqs : α} :

qqs = q + qs → pps + qs = pqs → pps + qqs = q + pqs := by cc

meta def add : ex sum → ex sum → ring_exp_m (ex sum)

| ps@(ex.zero ps_i) qs := do

pf ← mk_proof ``add_pf_z_sum [ps.orig, qs.orig, qs.pretty] [ps.info, qs.info],

pqs_o ← add_orig ps qs,

pure $ qs.set_info pqs_o pf

| ps qs@(ex.zero qs_i) := do

pf ← mk_proof ``add_pf_sum_z [ps.orig, ps.pretty, qs.orig] [ps.info, qs.info],

pqs_o ← add_orig ps qs,

pure $ ps.set_info pqs_o pf

| pps@(ex.sum pps_i p ps) qqs@(ex.sum qqs_i q qs) := do

ol ← add_overlap p q,

ppqqs_o ← add_orig pps qqs,

match ol with

| (overlap.nonzero pq) := do

pqs ← add ps qs,

pqqs ← ex_sum pq pqs,

qqs_pf ← qqs.proof_term,

pf ← mk_proof ``add_pf_sum_overlap

[pps.orig, p.pretty, ps.pretty, qqs.orig, q.pretty, qs.pretty, pq.pretty, pqs.pretty]

[pps.info, qqs.info, pq.info, pqs.info],

pure $ pqqs.set_info ppqqs_o pf

| (overlap.zero pq) := do

pqs ← add ps qs,

pf ← mk_proof ``add_pf_sum_overlap_zero

[pps.orig, p.pretty, ps.pretty, qqs.orig, q.pretty, qs.pretty, pqs.pretty]

[pps.info, qqs.info, pq.info, pqs.info],

pure $ pqs.set_info ppqqs_o pf

| overlap.none := if p.lt q

then do

pqs ← add ps qqs,

ppqs ← ex_sum p pqs,

pf ← mk_proof ``add_pf_sum_lt

[pps.orig, p.pretty, ps.pretty, qqs.orig, pqs.pretty]

[pps.info, pqs.info],

pure $ ppqs.set_info ppqqs_o pf

else do

pqs ← add pps qs,

pqqs ← ex_sum q pqs,

pf ← mk_proof ``add_pf_sum_gt

[pps.orig, qqs.orig, q.pretty, qs.pretty, pqs.pretty]

[qqs.info, pqs.info],

pure $ pqqs.set_info ppqqs_o pf

end

end addition

section multiplication

lemma mul_pf_c_c {ps ps' qs qs' pq : α} :

ps = ps' → qs = qs' → ps' * qs' = pq → ps * qs = pq := by cc

lemma mul_pf_c_prod {ps qqs q qs pqs : α} :

qqs = q * qs → ps * qs = pqs → ps * qqs = q * pqs := by cc

lemma mul_pf_prod_c {pps p ps qs pqs : α} :

pps = p * ps → ps * qs = pqs → pps * qs = p * pqs := by cc

lemma mul_pp_pf_overlap {pps p_b ps qqs qs psqs : α} {p_e q_e : ℕ} :

pps = p_b ^ p_e * ps → qqs = p_b ^ q_e * qs →

p_b ^ (p_e + q_e) * (ps * qs) = psqs → pps * qqs = psqs

:= λ ps_pf qs_pf psqs_pf, by simp [symm psqs_pf, pow_add, ps_pf, qs_pf]; ac_refl

lemma mul_pp_pf_prod_lt {pps p ps qqs pqs : α} :

pps = p * ps → ps * qqs = pqs → pps * qqs = p * pqs := by cc

lemma mul_pp_pf_prod_gt {pps qqs q qs pqs : α} :

qqs = q * qs → pps * qs = pqs → pps * qqs = q * pqs := by cc

meta def mul_pp : ex prod → ex prod → ring_exp_m (ex prod)

| ps@(ex.coeff _ x) qs@(ex.coeff _ y) := do

pq ← mul_coeff ps.pretty qs.pretty x y,

pq_o ← mul_orig ps qs,

pf ← mk_proof_or_refl pq.pretty ``mul_pf_c_c

[ps.orig, ps.pretty, qs.orig, qs.pretty, pq.pretty]

[ps.info, qs.info, pq.info],

pure $ pq.set_info pq_o pf

| ps@(ex.coeff _ x) qqs@(ex.prod _ q qs) := do

pqs ← mul_pp ps qs,

pqqs ← ex_prod q pqs,

pqqs_o ← mul_orig ps qqs,

pf ← mk_proof ``mul_pf_c_prod

[ps.orig, qqs.orig, q.pretty, qs.pretty, pqs.pretty]

[qqs.info, pqs.info],

pure $ pqqs.set_info pqqs_o pf

| pps@(ex.prod _ p ps) qs@(ex.coeff _ y) := do

pqs ← mul_pp ps qs,

ppqs ← ex_prod p pqs,

ppqs_o ← mul_orig pps qs,

pf ← mk_proof ``mul_pf_prod_c

[pps.orig, p.pretty, ps.pretty, qs.orig, pqs.pretty]

[pps.info, pqs.info],

pure $ ppqs.set_info ppqs_o pf

| pps@(ex.prod _ p@(ex.exp _ p_b p_e) ps) qqs@(ex.prod _ q@(ex.exp _ q_b q_e) qs) := do

ppqqs_o ← mul_orig pps qqs,

pq_ol ← in_exponent $ add_overlap p_e q_e,

match pq_ol, p_b.eq q_b with

| (overlap.nonzero pq_e), tt := do

psqs ← mul_pp ps qs,

pq ← ex_exp p_b pq_e,

ppsqqs ← ex_prod pq psqs,

pf ← mk_proof ``mul_pp_pf_overlap

[pps.orig, p_b.pretty, ps.pretty, qqs.orig, qs.pretty, ppsqqs.pretty, p_e.pretty, q_e.pretty]

[pps.info, qqs.info, ppsqqs.info],

pure $ ppsqqs.set_info ppqqs_o pf

| _, _ := if p.lt q then do

pqs ← mul_pp ps qqs,

ppqs ← ex_prod p pqs,

pf ← mk_proof ``mul_pp_pf_prod_lt

[pps.orig, p.pretty, ps.pretty, qqs.orig, pqs.pretty]

[pps.info, pqs.info],

pure $ ppqs.set_info ppqqs_o pf

else do

pqs ← mul_pp pps qs,

pqqs ← ex_prod q pqs,

pf ← mk_proof ``mul_pp_pf_prod_gt

[pps.orig, qqs.orig, q.pretty, qs.pretty, pqs.pretty]

[qqs.info, pqs.info],

pure $ pqqs.set_info ppqqs_o pf

end

lemma mul_p_pf_zero {ps qs : α} : ps = 0 → ps * qs = 0 :=

λ ps_pf, by rw [ps_pf, zero_mul]

lemma mul_p_pf_sum {pps p ps qs ppsqs : α} : pps = p + ps →

p * qs + ps * qs = ppsqs → pps * qs = ppsqs := λ pps_pf ppsqs_pf, calc

pps * qs = (p + ps) * qs : by rw [pps_pf]

... = p * qs + ps * qs : add_mul _ _ _

... = ppsqs : ppsqs_pf

meta def mul_p : ex sum → ex prod → ring_exp_m (ex sum)

| ps@(ex.zero ps_i) qs := do

z ← ex_zero,

z_o ← mul_orig ps qs,

pf ← mk_proof ``mul_p_pf_zero [ps.orig, qs.orig] [ps.info],

pure $ z.set_info z_o pf

| pps@(ex.sum pps_i p ps) qs := do

pqs ← mul_pp p qs >>= prod_to_sum,

psqs ← mul_p ps qs,

ppsqs ← add pqs psqs,

pps_pf ← pps.proof_term,

ppsqs_o ← mul_orig pps qs,

ppsqs_pf ← ppsqs.proof_term,

pf ← mk_proof ``mul_p_pf_sum

[pps.orig, p.pretty, ps.pretty, qs.orig, ppsqs.pretty]

[pps.info, ppsqs.info],

pure $ ppsqs.set_info ppsqs_o pf

lemma mul_pf_zero {ps qs : α} : qs = 0 → ps * qs = 0 :=

λ qs_pf, by rw [qs_pf, mul_zero]

lemma mul_pf_sum {ps qqs q qs psqqs : α} : qqs = q + qs → ps * q + ps * qs = psqqs →

ps * qqs = psqqs := λ qs_pf psqqs_pf, calc

ps * qqs = ps * (q + qs) : by rw [qs_pf]

... = ps * q + ps * qs : mul_add _ _ _

... = psqqs : psqqs_pf

meta def mul : ex sum → ex sum → ring_exp_m (ex sum)

| ps qs@(ex.zero qs_i) := do

z ← ex_zero,

z_o ← mul_orig ps qs,

pf ← mk_proof ``mul_pf_zero [ps.orig, qs.orig] [qs.info],

pure $ z.set_info z_o pf

| ps qqs@(ex.sum qqs_i q qs) := do

psq ← mul_p ps q,

psqs ← mul ps qs,

psqqs ← add psq psqs,

psqqs_o ← mul_orig ps qqs,

pf ← mk_proof ``mul_pf_sum

[ps.orig, qqs.orig, q.orig, qs.orig, psqqs.pretty]

[qqs.info, psqqs.info],

pure $ psqqs.set_info psqqs_o pf

end multiplication

section exponentiation

lemma pow_e_pf_exp {pps p : α} {ps qs psqs : ℕ} :

pps = p ^ ps → ps * qs = psqs → pps ^ qs = p ^ psqs :=

λ pps_pf psqs_pf, calc

pps ^ qs = (p ^ ps) ^ qs : by rw [pps_pf]

... = p ^ (ps * qs) : symm (pow_mul _ _ _)

... = p ^ psqs : by rw [psqs_pf]