text:
/-
Copyright (c) 2019 Tim Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tim Baanen

! This file was ported from Lean 3 source module tactic.ring_exp
! leanprover-community/mathlib commit 72e87ce0bf26144ceb122d280a43aa10f1d20abb
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Tactic.NormNum
import Mathbin.Control.Traversable.Basic

/-!
# `ring_exp` tactic

A tactic for solving equations in commutative (semi)rings,
where the exponents can also contain variables.

More precisely, expressions of the following form are supported:
- constants (non-negative integers)
- variables
- coefficients (any rational number, embedded into the (semi)ring)
- addition of expressions
- multiplication of expressions
- exponentiation of expressions (the exponent must have type `ℕ`)
- subtraction and negation of expressions (if the base is a full ring)

The motivating example is proving `2 * 2^n * b = b * 2^(n+1)`,
something that the `ring` tactic cannot do, but `ring_exp` can.

## Implementation notes

The basic approach to prove equalities is to normalise both sides and check for equality.
The normalisation is guided by building a value in the type `ex` at the meta level,
together with a proof (at the base level) that the original value is equal to
the normalised version.
The normalised version and normalisation proofs are also stored in the `ex` type.

The outline of the file:
- Define an inductive family of types `ex`, parametrised over `ex_type`,
  which can represent expressions with `+`, `*`, `^` and rational numerals.
  The parametrisation over `ex_type` ensures that associativity and distributivity are applied,
  by restricting which kinds of subexpressions appear as arguments to the various operators.
- Represent addition, multiplication and exponentiation in the `ex` type,
  thus allowing us to map expressions to `ex` (the `eval` function drives this).
  We apply associativity and distributivity of the operators here (helped by `ex_type`)
  and commutativity as well (by sorting the subterms; unfortunately not helped by anything).
  Any expression not of the above formats is treated as an atom (the same as a variable).

There are some details we glossed over which make the plan more complicated:
- The order on atoms is not initially obvious.
  We construct a list containing them in order of initial appearance in the expression,
  then use the index into the list as a key to order on.
- In the tactic, a normalized expression `ps : ex` lives in the meta-world,
  but the normalization proofs live in the real world.
  Thus, we cannot directly say `ps.orig = ps.pretty` anywhere,
  but we have to carefully construct the proof when we compute `ps`.
  This was a major source of bugs in development!
- For `pow`, the exponent must be a natural number, while the base can be any semiring `α`.
  We swap out operations for the base ring `α` with those for the exponent ring `ℕ`
  as soon as we deal with exponents.
  This is accomplished by the `in_exponent` function and is relatively painless since
  we work in a `reader` monad.
- The normalized form of an expression is the one that is useful for the tactic,
  but not as nice to read. To remedy this, the user-facing normalization calls `ex.simp`.

## Caveats and future work

Subtraction cancels out identical terms, but division does not.
That is: `a - a = 0 := by ring_exp` solves the goal,
but `a / a := 1 by ring_exp` doesn't.
Note that `0 / 0` is generally defined to be `0`,
so division cancelling out is not true in general.

Multiplication of powers can be simplified a little bit further:
`2 ^ n * 2 ^ n = 4 ^ n := by ring_exp` could be implemented
in a similar way that `2 * a + 2 * a = 4 * a := by ring_exp` already works.
This feature wasn't needed yet, so it's not implemented yet.

## Tags

ring, semiring, exponent, power
-/

-- The base ring `α` will have a universe level `u`.
-- We do not introduce `α` as a variable yet,
-- in order to make it explicit or implicit as required.
universe u

namespace Tactic.RingExp

open Nat

/-- The `atom` structure is used to represent atomic expressions:
those which `ring_exp` cannot parse any further.

For instance, `a + (a % b)` has `a` and `(a % b)` as atoms.
The `ring_exp_eq` tactic does not normalize the subexpressions in atoms,
but `ring_exp` does if `ring_exp_eq` was not sufficient.

Atoms in fact represent equivalence classes of expressions,
modulo definitional equality.
The field `index : ℕ` should be a unique number for each class,
while `value : expr` contains a representative of this class.
The function `resolve_atom` determines the appropriate atom
for a given expression.
-/
unsafe structure atom : Type where
  value : expr
  index : ℕ
#align tactic.ring_exp.atom tactic.ring_exp.atom

namespace Atom

/-- The `eq` operation on `atom`s works modulo definitional equality,
ignoring their `value`s.
The invariants on `atom` ensure indices are unique per value.
Thus, `eq` indicates equality as long as the `atom`s come from the same context.
-/
unsafe def eq (a b : atom) : Bool :=
  a.index = b.index
#align tactic.ring_exp.atom.eq tactic.ring_exp.atom.eq

/-- We order `atom`s on the order of appearance in the main expression.
-/
unsafe def lt (a b : atom) : Bool :=
  a.index < b.index
#align tactic.ring_exp.atom.lt tactic.ring_exp.atom.lt

unsafe instance : Repr atom :=
  ⟨fun x => "(atom " ++ repr x.2 ++ ")"⟩

end Atom

section Expression

/-!
### `expression` section

In this section, we define the `ex` type and its basic operations.

First, we introduce the supporting types `coeff`, `ex_type` and `ex_info`.
For understanding the code, it's easier to check out `ex` itself first,
then refer back to the supporting types.

The arithmetic operations on `ex` need additional definitions,
so they are defined in a later section.
-/

/-- Coefficients in the expression are stored in a wrapper structure,
allowing for easier modification of the data structures.
The modifications might be caching of the result of `expr.of_rat`,
or using a different meta representation of numerals.
-/
structure Coeff : Type where
  value : ℚ
  deriving DecidableEq, Inhabited
#align tactic.ring_exp.coeff Tactic.RingExp.Coeff

/-- The values in `ex_type` are used as parameters to `ex` to control the expression's structure. -/
inductive ExType : Type
  | base : ex_type
  | Sum : ex_type
  | Prod : ex_type
  | exp : ex_type
  deriving DecidableEq, Inhabited
#align tactic.ring_exp.ex_type Tactic.RingExp.ExType

open ExType

/-- Each `ex` stores information for its normalization proof.

The `orig` expression is the expression that was passed to `eval`.

The `pretty` expression is the normalised form that the `ex` represents.
(I didn't call this something like `norm`, because there are already
too many things called `norm` in mathematics!)

The field `proof` contains an optional proof term of type `%%orig = %%pretty`.
The value `none` for the proof indicates that everything reduces to reflexivity.
(Which saves space in quite a lot of cases.)
-/
unsafe structure ex_info : Type where
  orig : expr
  pretty : expr
  Proof : Option expr
#align tactic.ring_exp.ex_info tactic.ring_exp.ex_info

/-- The `ex` type is an abstract representation of an expression with `+`, `*` and `^`.
Those operators are mapped to the `sum`, `prod` and `exp` constructors respectively.

The `zero` constructor is the base case for `ex sum`, e.g. `1 + 2` is represented
by (something along the lines of) `sum 1 (sum 2 zero)`.

The `coeff` constructor is the base case for `ex prod`, and is used for numerals.
The code maintains the invariant that the coefficient is never `0`.

The `var` constructor is the base case for `ex exp`, and is used for atoms.

The `sum_b` constructor allows for addition in the base of an exponentiation;
it serves a similar purpose as the parentheses in `(a + b)^c`.
The code maintains the invariant that the argument to `sum_b` is not `zero`
or `sum _ zero`.

All of the constructors contain an `ex_info` field,
used to carry around (arguments to) proof terms.

While the `ex_type` parameter enforces some simplification invariants,
the following ones must be manually maintained at the risk of insufficient power:
- the argument to `coeff` must be nonzero (to ensure `0 = 0 * 1`)
- the argument to `sum_b` must be of the form `sum a (sum b bs)` (to ensure `(a + 0)^n = a^n`)
- normalisation proofs of subexpressions must be `refl ps.pretty`
- if we replace `sum` with `cons` and `zero` with `nil`, the resulting list is sorted
  according to the `lt` relation defined further down; similarly for `prod` and `coeff`
  (to ensure `a + b = b + a`).

The first two invariants could be encoded in a subtype of `ex`,
but aren't (yet) to spare some implementation burden.
The other invariants cannot be encoded because we need the `tactic` monad to check them.
(For example, the correct equality check of `expr` is `is_def_eq : expr → expr → tactic unit`.)
-/
unsafe inductive ex : ExType → 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
#align tactic.ring_exp.ex tactic.ring_exp.ex

/-- Return the proof information associated to the `ex`.
-/
unsafe def ex.info : ∀ {et : ExType} (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
#align tactic.ring_exp.ex.info tactic.ring_exp.ex.info

/-- Return the original, non-normalized version of this `ex`.

Note that arguments to another `ex` are always "pre-normalized":
their `orig` and `pretty` are equal, and their `proof` is reflexivity.
-/
unsafe def ex.orig {et : ExType} (ps : ex et) : expr :=
  ps.info.orig
#align tactic.ring_exp.ex.orig tactic.ring_exp.ex.orig

/-- Return the normalized version of this `ex`.
-/
unsafe def ex.pretty {et : ExType} (ps : ex et) : expr :=
  ps.info.pretty
#align tactic.ring_exp.ex.pretty tactic.ring_exp.ex.pretty

/-- Return the normalisation proof of the given expression.
If the proof is `refl`, we give `none` instead,
which helps to control the size of proof terms.
To get an actual term, use `ex.proof_term`,
or use `mk_proof` with the correct set of arguments.
-/
unsafe def ex.proof {et : ExType} (ps : ex et) : Option expr :=
  ps.info.Proof
#align tactic.ring_exp.ex.proof tactic.ring_exp.ex.proof

/-- Update the `orig` and `proof` fields of the `ex_info`.
Intended for use in `ex.set_info`.
-/
unsafe def ex_info.set (i : ex_info) (o : Option expr) (pf : Option expr) : ex_info :=
  { i with
    orig := o.getD i.pretty
    Proof := pf }
#align tactic.ring_exp.ex_info.set tactic.ring_exp.ex_info.set

/-- Update the `ex_info` of the given expression.

We use this to combine intermediate normalisation proofs.
Since `pretty` only depends on the subexpressions,
which do not change, we do not set `pretty`.
-/
unsafe def ex.set_info : ∀ {et : ExType} (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
#align tactic.ring_exp.ex.set_info tactic.ring_exp.ex.set_info

instance coeffHasRepr : Repr Coeff :=
  ⟨fun x => repr x.1⟩
#align tactic.ring_exp.coeff_has_repr Tactic.RingExp.coeffHasRepr

/-- Convert an `ex` to a `string`. -/
unsafe def ex.repr : ∀ {et : ExType}, 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
#align tactic.ring_exp.ex.repr tactic.ring_exp.ex.repr

unsafe instance {et : ExType} : Repr (ex et) :=
  ⟨ex.repr⟩

/-- Equality test for expressions.

Since equivalence of `atom`s is not the same as equality,
we cannot make a true `(=)` operator for `ex` either.
-/
unsafe def ex.eq : ∀ {et : ExType}, ex et → ex et → Bool
  | Sum, ex.zero _, ex.zero _ => true
  | Sum, ex.zero _, ex.sum _ _ _ => false
  | Sum, ex.sum _ _ _, ex.zero _ => false
  | 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 _ _ _ => false
  | Prod, ex.prod _ _ _, ex.coeff _ _ => false
  | 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 _ _ => false
  | base, ex.sum_b _ _, ex.var _ _ => false
  | 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
#align tactic.ring_exp.ex.eq tactic.ring_exp.ex.eq

/-- The ordering on expressions.

As for `ex.eq`, this is a linear order only in one context.
-/
unsafe def ex.lt : ∀ {et : ExType}, ex et → ex et → Bool
  | Sum, _, ex.zero _ => false
  | Sum, ex.zero _, _ => true
  | 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 _ _, _ => true
  | Prod, _, ex.coeff _ _ => false
  | 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 _ _ => true
  | base, ex.sum_b _ _, ex.var _ _ => false
  | 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
#align tactic.ring_exp.ex.lt tactic.ring_exp.ex.lt

end Expression

section Operations

/-!
### `operations` section

This section defines the operations (on `ex`) that use tactics.
They live in the `ring_exp_m` monad,
which adds a cache and a list of encountered atoms to the `tactic` monad.

Throughout this section, we will be constructing proof terms.
The lemmas used in the construction are all defined over a commutative semiring α.
-/

variable {α : Type u} [CommSemiring α]

open Tactic

open ExType

/-- Stores the information needed in the `eval` function and its dependencies,
so they can (re)construct expressions.

The `eval_info` structure stores this information for one type,
and the `context` combines the two types, one for bases and one for exponents.
-/
unsafe structure eval_info where
  α : expr
  univ : level
  -- Cache the instances for optimization and consistency
  csr_instance : expr
  ha_instance : expr
  hm_instance : expr
  hp_instance : expr
  -- Optional instances (only required for (-) and (/) respectively)
  ring_instance : Option expr
  dr_instance : Option expr
  -- Cache common constants.
  zero : expr
  one : expr
#align tactic.ring_exp.eval_info tactic.ring_exp.eval_info

/-- The `context` contains the full set of information needed for the `eval` function.

This structure has two copies of `eval_info`:
one is for the base (typically some semiring `α`) and another for the exponent (always `ℕ`).
When evaluating an exponent, we put `info_e` in `info_b`.
-/
unsafe structure context where
  info_b : eval_info
  info_e : eval_info
  transp : Transparency
#align tactic.ring_exp.context tactic.ring_exp.context

/-- The `ring_exp_m` monad is used instead of `tactic` to store the context.
-/
unsafe def ring_exp_m (α : Type) : Type :=
  ReaderT context (StateT (List atom) tactic) α deriving Monad, Alternative
#align tactic.ring_exp.ring_exp_m tactic.ring_exp.ring_exp_m

/-- Access the instance cache.
-/
unsafe def get_context : ring_exp_m context :=
  ReaderT.read
#align tactic.ring_exp.get_context tactic.ring_exp.get_context

/-- Lift an operation in the `tactic` monad to the `ring_exp_m` monad.

This operation will not access the cache.
-/
unsafe def lift {α} (m : tactic α) : ring_exp_m α :=
  ReaderT.lift (StateT.lift m)
#align tactic.ring_exp.lift tactic.ring_exp.lift

/-- Change the context of the given computation,
so that expressions are evaluated in the exponent ring,
instead of the base ring.
-/
unsafe def in_exponent {α} (mx : ring_exp_m α) : ring_exp_m α := do
  let ctx ← get_context
  ReaderT.lift <| mx ⟨ctx, ctx, ctx⟩
#align tactic.ring_exp.in_exponent tactic.ring_exp.in_exponent

/-- Specialized version of `mk_app` where the first two arguments are `{α}` `[some_class α]`.
Should be faster because it can use the cached instances.
-/
unsafe def mk_app_class (f : Name) (inst : expr) (args : List expr) : ring_exp_m expr := do
  let ctx ← get_context
  pure <| (@expr.const tt f [ctx] ctx inst).mk_app args
#align tactic.ring_exp.mk_app_class tactic.ring_exp.mk_app_class

/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `ctx -/
/-- Specialized version of `mk_app` where the first two arguments are `{α}` `[comm_semiring α]`.
Should be faster because it can use the cached instances.
 -/
unsafe def mk_app_csr (f : Name) (args : List expr) : ring_exp_m expr := do
  let ctx ← get_context
  mk_app_class f (ctx ctx.info_b.csr_instance) args
#align tactic.ring_exp.mk_app_csr tactic.ring_exp.mk_app_csr

/-- Specialized version of `mk_app ``has_add.add`.
Should be faster because it can use the cached instances.
-/
unsafe def mk_add (args : List expr) : ring_exp_m expr := do
  let ctx ← get_context
  mk_app_class `` Add.add ctx args
#align tactic.ring_exp.mk_add tactic.ring_exp.mk_add

/-- Specialized version of `mk_app ``has_mul.mul`.
Should be faster because it can use the cached instances.
-/
unsafe def mk_mul (args : List expr) : ring_exp_m expr := do
  let ctx ← get_context
  mk_app_class `` Mul.mul ctx args
#align tactic.ring_exp.mk_mul tactic.ring_exp.mk_mul

/-- Specialized version of `mk_app ``has_pow.pow`.
Should be faster because it can use the cached instances.
-/
unsafe def mk_pow (args : List expr) : ring_exp_m expr := do
  let ctx ← get_context
  pure <| (@expr.const tt `` Pow.pow [ctx, ctx] ctx ctx ctx).mk_app args
#align tactic.ring_exp.mk_pow tactic.ring_exp.mk_pow

/-- Construct a normalization proof term or return the cached one. -/
unsafe 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
#align tactic.ring_exp.ex_info.proof_term tactic.ring_exp.ex_info.proof_term

/-- Construct a normalization proof term or return the cached one. -/
unsafe def ex.proof_term {et : ExType} (ps : ex et) : ring_exp_m expr :=
  ps.info.proof_term
#align tactic.ring_exp.ex.proof_term tactic.ring_exp.ex.proof_term

/-- If all `ex_info` have trivial proofs, return a trivial proof.
Otherwise, construct all proof terms.

Useful in applications where trivial proofs combine to another trivial proof,
most importantly to pass to `mk_proof_or_refl`.
-/
unsafe def none_or_proof_term : List ex_info → ring_exp_m (Option (List expr))
  | [] => pure none
  | x :: xs => do
    let xs_pfs ← none_or_proof_term xs
    match (x, xs_pfs) with
      | (none, none) => pure none
      | (some x_pf, none) => do
        let xs_pfs ← traverse ex_info.proof_term xs
        pure (some (x_pf :: xs_pfs))
      | (_, some xs_pfs) => do
        let x_pf ← x
        pure (some (x_pf :: xs_pfs))
#align tactic.ring_exp.none_or_proof_term tactic.ring_exp.none_or_proof_term

/-- Use the proof terms as arguments to the given lemma.
If the lemma could reduce to reflexivity, consider using `mk_proof_or_refl.`
-/
unsafe def mk_proof (lem : Name) (args : List expr) (hs : List ex_info) : ring_exp_m expr := do
  let hs' ← traverse ex_info.proof_term hs
  mk_app_csr lem (args ++ hs')
#align tactic.ring_exp.mk_proof tactic.ring_exp.mk_proof

/-- Use the proof terms as arguments to the given lemma.
Often, we construct a proof term using congruence where reflexivity suffices.
To solve this, the following function tries to get away with reflexivity.
-/
unsafe def mk_proof_or_refl (term : expr) (lem : Name) (args : List expr) (hs : List ex_info) :
    ring_exp_m expr := do
  let 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')
#align tactic.ring_exp.mk_proof_or_refl tactic.ring_exp.mk_proof_or_refl

/-- A shortcut for adding the original terms of two expressions. -/
unsafe def add_orig {et et'} (ps : ex et) (qs : ex et') : ring_exp_m expr :=
  mk_add [ps.orig, qs.orig]
#align tactic.ring_exp.add_orig tactic.ring_exp.add_orig

/-- A shortcut for multiplying the original terms of two expressions. -/
unsafe def mul_orig {et et'} (ps : ex et) (qs : ex et') : ring_exp_m expr :=
  mk_mul [ps.orig, qs.orig]
#align tactic.ring_exp.mul_orig tactic.ring_exp.mul_orig

/-- A shortcut for exponentiating the original terms of two expressions. -/
unsafe def pow_orig {et et'} (ps : ex et) (qs : ex et') : ring_exp_m expr :=
  mk_pow [ps.orig, qs.orig]
#align tactic.ring_exp.pow_orig tactic.ring_exp.pow_orig

/-- Congruence lemma for constructing `ex.sum`. -/
theorem sum_congr {p p' ps ps' : α} : p = p' → ps = ps' → p + ps = p' + ps' := by cc
#align tactic.ring_exp.sum_congr Tactic.RingExp.sum_congr

/-- Congruence lemma for constructing `ex.prod`. -/
theorem prod_congr {p p' ps ps' : α} : p = p' → ps = ps' → p * ps = p' * ps' := by cc
#align tactic.ring_exp.prod_congr Tactic.RingExp.prod_congr

/-- Congruence lemma for constructing `ex.exp`. -/
theorem exp_congr {p p' : α} {ps ps' : ℕ} : p = p' → ps = ps' → p ^ ps = p' ^ ps' := by cc
#align tactic.ring_exp.exp_congr Tactic.RingExp.exp_congr

/-- Constructs `ex.zero` with the correct arguments. -/
unsafe def ex_zero : ring_exp_m (ex Sum) := do
  let ctx ← get_context
  pure <| ex.zero ⟨ctx, ctx, none⟩
#align tactic.ring_exp.ex_zero tactic.ring_exp.ex_zero

/-- Constructs `ex.sum` with the correct arguments. -/
unsafe def ex_sum (p : ex Prod) (ps : ex Sum) : ring_exp_m (ex Sum) := do
  let pps_o ← add_orig p ps
  let pps_p ← mk_add [p.pretty, ps.pretty]
  let 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 none none) (ps none none))
#align tactic.ring_exp.ex_sum tactic.ring_exp.ex_sum

/-- Constructs `ex.coeff` with the correct arguments.

There are more efficient constructors for specific numerals:
if `x = 0`, you should use `ex_zero`; if `x = 1`, use `ex_one`.
-/
unsafe def ex_coeff (x : Rat) : ring_exp_m (ex Prod) := do
  let ctx ← get_context
  let x_p ← lift <| expr.of_rat ctx.info_b.α x
  pure (ex.coeff ⟨x_p, x_p, none⟩ ⟨x⟩)
#align tactic.ring_exp.ex_coeff tactic.ring_exp.ex_coeff

/-- Constructs `ex.coeff 1` with the correct arguments.
This is a special case for optimization purposes.
-/
unsafe def ex_one : ring_exp_m (ex Prod) := do
  let ctx ← get_context
  pure <| ex.coeff ⟨ctx, ctx, none⟩ ⟨1⟩
#align tactic.ring_exp.ex_one tactic.ring_exp.ex_one

/-- Constructs `ex.prod` with the correct arguments. -/
unsafe def ex_prod (p : ex exp) (ps : ex Prod) : ring_exp_m (ex Prod) := do
  let pps_o ← mul_orig p ps
  let pps_p ← mk_mul [p.pretty, ps.pretty]
  let 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 none none) (ps none none))
#align tactic.ring_exp.ex_prod tactic.ring_exp.ex_prod

/-- Constructs `ex.var` with the correct arguments. -/
unsafe def ex_var (p : atom) : ring_exp_m (ex base) :=
  pure (ex.var ⟨p.1, p.1, none⟩ p)
#align tactic.ring_exp.ex_var tactic.ring_exp.ex_var

/-- Constructs `ex.sum_b` with the correct arguments. -/
unsafe def ex_sum_b (ps : ex Sum) : ring_exp_m (ex base) :=
  pure (ex.sum_b ps.info (ps.set_info none none))
#align tactic.ring_exp.ex_sum_b tactic.ring_exp.ex_sum_b

/-- Constructs `ex.exp` with the correct arguments. -/
unsafe def ex_exp (p : ex base) (ps : ex Prod) : ring_exp_m (ex exp) := do
  let ctx ← get_context
  let pps_o ← pow_orig p ps
  let pps_p ← mk_pow [p.pretty, ps.pretty]
  let 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 none none) (ps none none))
#align tactic.ring_exp.ex_exp tactic.ring_exp.ex_exp

theorem base_to_exp_pf {p p' : α} : p = p' → p = p' ^ 1 := by simp
#align tactic.ring_exp.base_to_exp_pf Tactic.RingExp.base_to_exp_pf

/-- Conversion from `ex base` to `ex exp`. -/
unsafe def base_to_exp (p : ex base) : ring_exp_m (ex exp) := do
  let o ← in_exponent <| ex_one
  let ps ← ex_exp p o
  let pf ← mk_proof `` base_to_exp_pf [p.orig, p.pretty] [p.info]
  pure <| ps p pf
#align tactic.ring_exp.base_to_exp tactic.ring_exp.base_to_exp

theorem exp_to_prod_pf {p p' : α} : p = p' → p = p' * 1 := by simp
#align tactic.ring_exp.exp_to_prod_pf Tactic.RingExp.exp_to_prod_pf

/-- Conversion from `ex exp` to `ex prod`. -/
unsafe def exp_to_prod (p : ex exp) : ring_exp_m (ex Prod) := do
  let o ← ex_one
  let ps ← ex_prod p o
  let pf ← mk_proof `` exp_to_prod_pf [p.orig, p.pretty] [p.info]
  pure <| ps p pf
#align tactic.ring_exp.exp_to_prod tactic.ring_exp.exp_to_prod

theorem prod_to_sum_pf {p p' : α} : p = p' → p = p' + 0 := by simp
#align tactic.ring_exp.prod_to_sum_pf Tactic.RingExp.prod_to_sum_pf

/-- Conversion from `ex prod` to `ex sum`. -/
unsafe def prod_to_sum (p : ex Prod) : ring_exp_m (ex Sum) := do
  let z ← ex_zero
  let ps ← ex_sum p z
  let pf ← mk_proof `` prod_to_sum_pf [p.orig, p.pretty] [p.info]
  pure <| ps p pf
#align tactic.ring_exp.prod_to_sum tactic.ring_exp.prod_to_sum

theorem atom_to_sum_pf (p : α) : p = p ^ 1 * 1 + 0 := by simp
#align tactic.ring_exp.atom_to_sum_pf Tactic.RingExp.atom_to_sum_pf

/-- A more efficient conversion from `atom` to `ex sum`.

The result should be the same as `ex_var p >>= base_to_exp >>= exp_to_prod >>= prod_to_sum`,
except we need to calculate less intermediate steps.
-/
unsafe def atom_to_sum (p : atom) : ring_exp_m (ex Sum) := do
  let p' ← ex_var p
  let o ← in_exponent <| ex_one
  let p' ← ex_exp p' o
  let o ← ex_one
  let p' ← ex_prod p' o
  let z ← ex_zero
  let p' ← ex_sum p' z
  let pf ← mk_proof `` atom_to_sum_pf [p.1] []
  pure <| p' p.1 pf
#align tactic.ring_exp.atom_to_sum tactic.ring_exp.atom_to_sum

/-- Compute the sum of two coefficients.
Note that the result might not be a valid expression:
if `p = -q`, then the result should be `ex.zero : ex sum` instead.
The caller must detect when this happens!

The returned value is of the form `ex.coeff _ (p + q)`,
with the proof of `expr.of_rat p + expr.of_rat q = expr.of_rat (p + q)`.
-/
unsafe def add_coeff (p_p q_p : expr) (p q : Coeff) : ring_exp_m (ex Prod) := do
  let ctx ← get_context
  let pq_o ← mk_add [p_p, q_p]
  let (pq_p, pq_pf) ← lift <| norm_num.eval_field pq_o
  pure <| ex.coeff ⟨pq_o, pq_p, pq_pf⟩ ⟨p.1 + q.1⟩
#align tactic.ring_exp.add_coeff tactic.ring_exp.add_coeff

theorem mul_coeff_pf_one_mul (q : α) : 1 * q = q :=
  one_mul q
#align tactic.ring_exp.mul_coeff_pf_one_mul Tactic.RingExp.mul_coeff_pf_one_mul

theorem mul_coeff_pf_mul_one (p : α) : p * 1 = p :=
  mul_one p
#align tactic.ring_exp.mul_coeff_pf_mul_one Tactic.RingExp.mul_coeff_pf_mul_one

/-- Compute the product of two coefficients.

The returned value is of the form `ex.coeff _ (p * q)`,
with the proof of `expr.of_rat p * expr.of_rat q = expr.of_rat (p * q)`.
-/
unsafe 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
    let ctx ← get_context
    let pq_o ← mk_mul [p_p, q_p]
    let pf ← mk_app_csr `` mul_coeff_pf_one_mul [q_p]
    pure <| ex.coeff ⟨pq_o, q_p, pf⟩ ⟨q.1⟩
  | _, ⟨1, 1, _, _⟩ => do
    let ctx ← get_context
    let pq_o ← mk_mul [p_p, q_p]
    let pf ← mk_app_csr `` mul_coeff_pf_mul_one [p_p]
    pure <| ex.coeff ⟨pq_o, p_p, pf⟩ ⟨p.1⟩
  | _, _ => do
    let ctx ← get_context
    let pq' ← mk_mul [p_p, q_p]
    let (pq_p, pq_pf) ← lift <| norm_num.eval_field pq'
    pure <| ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 * q.1⟩
#align tactic.ring_exp.mul_coeff tactic.ring_exp.mul_coeff

section Rewrite

/-! ### `rewrite` section

In this section we deal with rewriting terms to fit in the basic grammar of `eval`.
For example, `nat.succ n` is rewritten to `n + 1` before it is evaluated further.
-/

/-- Given a proof that the expressions `ps_o` and `ps'.orig` are equal,
show that `ps_o` and `ps'.pretty` are equal.

Useful to deal with aliases in `eval`. For instance, `nat.succ p` can be handled
as an alias of `p + 1` as follows:
```
| ps_o@`(nat.succ %%p_o) := do
  ps' ← eval `(%%p_o + 1),
  pf ← lift $ mk_app ``nat.succ_eq_add_one [p_o],
  rewrite ps_o ps' pf
```
-/
unsafe def rewrite (ps_o : expr) (ps' : ex Sum) (pf : expr) : ring_exp_m (ex Sum) := do
  let ps'_pf ← ps'.info.proof_term
  let pf ← lift <| mk_eq_trans pf ps'_pf
  pure <| ps' ps_o pf
#align tactic.ring_exp.rewrite tactic.ring_exp.rewrite

end Rewrite

/-- Represents the way in which two products are equal except coefficient.

This type is used in the function `add_overlap`.
In order to deal with equations of the form `a * 2 + a = 3 * a`,
the `add` function will add up overlapping products,
turning `a * 2 + a` into `a * 3`.
We need to distinguish `a * 2 + a` from `a * 2 + b` in order to do this,
and the `overlap` type carries the information on how it overlaps.

The case `none` corresponds to non-overlapping products, e.g. `a * 2 + b`;
the case `nonzero` to overlapping products adding to non-zero, e.g. `a * 2 + a`
(the `ex prod` field will then look like `a * 3` with a proof that `a * 2 + a = a * 3`);
the case `zero` to overlapping products adding to zero, e.g. `a * 2 + a * -2`.
We distinguish those two cases because in the second, the whole product reduces to `0`.

A potential extension to the tactic would also do this for the base of exponents,
e.g. to show `2^n * 2^n = 4^n`.
-/
unsafe inductive overlap : Type
  | none : overlap
  | nonzero : ex Prod → overlap
  | zero : ex Sum → overlap
#align tactic.ring_exp.overlap tactic.ring_exp.overlap

theorem add_overlap_pf {ps qs pq} (p : α) : ps + qs = pq → p * ps + p * qs = p * pq := fun pq_pf =>
  calc
    p * ps + p * qs = p * (ps + qs) := symm (mul_add _ _ _)
    _ = p * pq := by rw [pq_pf]

#align tactic.ring_exp.add_overlap_pf Tactic.RingExp.add_overlap_pf

theorem add_overlap_pf_zero {ps qs} (p : α) : ps + qs = 0 → p * ps + p * qs = 0 := fun pq_pf =>
  calc
    p * ps + p * qs = p * (ps + qs) := symm (mul_add _ _ _)
    _ = p * 0 := by rw [pq_pf]
    _ = 0 := MulZeroClass.mul_zero _

#align tactic.ring_exp.add_overlap_pf_zero Tactic.RingExp.add_overlap_pf_zero

/-- Given arguments `ps`, `qs` of the form `ps' * x` and `ps' * y` respectively
return `ps + qs = ps' * (x + y)` (with `x` and `y` arbitrary coefficients).
For other arguments, return `overlap.none`.
-/
unsafe def add_overlap : ex Prod → ex Prod → ring_exp_m overlap
  | ex.coeff x_i x, ex.coeff y_i y => do
    let 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
        let z ← ex_zero
        pure <| overlap.zero (z xy xy)
      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
      let pq_ol ← add_overlap ps qs
      let pqs_o ← add_orig pps qqs
      match pq_ol with
        | overlap.none => pure overlap.none
        | overlap.nonzero pq => do
          let pqs ← ex_prod p pq
          let pf ← mk_proof `` add_overlap_pf [ps, qs, pq, p] [pq]
          pure <| overlap.nonzero (pqs pqs_o pf)
        | overlap.zero pq => do
          let z ← ex_zero
          let pf ← mk_proof `` add_overlap_pf_zero [ps, qs, p] [pq]
          pure <| overlap.zero (z pqs_o pf)
    else pure overlap.none
#align tactic.ring_exp.add_overlap tactic.ring_exp.add_overlap

section Addition

theorem add_pf_z_sum {ps qs qs' : α} : ps = 0 → qs = qs' → ps + qs = qs' := fun ps_pf qs_pf =>
  calc
    ps + qs = 0 + qs' := by rw [ps_pf, qs_pf]
    _ = qs' := zero_add _

#align tactic.ring_exp.add_pf_z_sum Tactic.RingExp.add_pf_z_sum

theorem add_pf_sum_z {ps ps' qs : α} : ps = ps' → qs = 0 → ps + qs = ps' := fun ps_pf qs_pf =>
  calc
    ps + qs = ps' + 0 := by rw [ps_pf, qs_pf]
    _ = ps' := add_zero _

#align tactic.ring_exp.add_pf_sum_z Tactic.RingExp.add_pf_sum_z

theorem 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
#align tactic.ring_exp.add_pf_sum_overlap Tactic.RingExp.add_pf_sum_overlap

theorem 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 :=
  fun 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 _

#align tactic.ring_exp.add_pf_sum_overlap_zero Tactic.RingExp.add_pf_sum_overlap_zero

theorem add_pf_sum_lt {pps p ps qqs pqs : α} :
    pps = p + ps → ps + qqs = pqs → pps + qqs = p + pqs := by cc
#align tactic.ring_exp.add_pf_sum_lt Tactic.RingExp.add_pf_sum_lt

theorem add_pf_sum_gt {pps qqs q qs pqs : α} :
    qqs = q + qs → pps + qs = pqs → pps + qqs = q + pqs := by cc
#align tactic.ring_exp.add_pf_sum_gt Tactic.RingExp.add_pf_sum_gt

/-- Add two expressions.

* `0 + qs = 0`
* `ps + 0 = 0`
* `ps * x + ps * y = ps * (x + y)` (for `x`, `y` coefficients; uses `add_overlap`)
* `(p + ps) + (q + qs) = p + (ps + (q + qs))` (if `p.lt q`)
* `(p + ps) + (q + qs) = q + ((p + ps) + qs)` (if not `p.lt q`)
-/
unsafe def add : ex Sum → ex Sum → ring_exp_m (ex Sum)
  | ps@(ex.zero ps_i), qs => do
    let pf ← mk_proof `` add_pf_z_sum [ps.orig, qs.orig, qs.pretty] [ps.info, qs.info]
    let pqs_o ← add_orig ps qs
    pure <| qs pqs_o pf
  | ps, qs@(ex.zero qs_i) => do
    let pf ← mk_proof `` add_pf_sum_z [ps.orig, ps.pretty, qs.orig] [ps.info, qs.info]
    let pqs_o ← add_orig ps qs
    pure <| ps pqs_o pf
  | pps@(ex.sum pps_i p ps), qqs@(ex.sum qqs_i q qs) => do
    let ol ← add_overlap p q
    let ppqqs_o ← add_orig pps qqs
    match ol with
      | overlap.nonzero pq => do
        let pqs ← add ps qs
        let pqqs ← ex_sum pq pqs
        let qqs_pf ← qqs
        let pf ←
          mk_proof `` add_pf_sum_overlap [pps, p, ps, qqs, q, qs, pq, pqs] [pps, qqs, pq, pqs]
        pure <| pqqs ppqqs_o pf
      | overlap.zero pq => do
        let pqs ← add ps qs
        let pf ←
          mk_proof `` add_pf_sum_overlap_zero [pps, p, ps, qqs, q, qs, pqs] [pps, qqs, pq, pqs]
        pure <| pqs ppqqs_o pf
      | overlap.none =>
        if p q then do
          let pqs ← add ps qqs
          let ppqs ← ex_sum p pqs
          let pf ← mk_proof `` add_pf_sum_lt [pps, p, ps, qqs, pqs] [pps, pqs]
          pure <| ppqs ppqqs_o pf
        else do
          let pqs ← add pps qs
          let pqqs ← ex_sum q pqs
          let pf ← mk_proof `` add_pf_sum_gt [pps, qqs, q, qs, pqs] [qqs, pqs]
          pure <| pqqs ppqqs_o pf
#align tactic.ring_exp.add tactic.ring_exp.add

end Addition

section Multiplication

theorem mul_pf_c_c {ps ps' qs qs' pq : α} : ps = ps' → qs = qs' → ps' * qs' = pq → ps * qs = pq :=
  by cc
#align tactic.ring_exp.mul_pf_c_c Tactic.RingExp.mul_pf_c_c

theorem mul_pf_c_prod {ps qqs q qs pqs : α} : qqs = q * qs → ps * qs = pqs → ps * qqs = q * pqs :=
  by cc
#align tactic.ring_exp.mul_pf_c_prod Tactic.RingExp.mul_pf_c_prod

theorem mul_pf_prod_c {pps p ps qs pqs : α} : pps = p * ps → ps * qs = pqs → pps * qs = p * pqs :=
  by cc
#align tactic.ring_exp.mul_pf_prod_c Tactic.RingExp.mul_pf_prod_c

theorem 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 :=
  fun ps_pf qs_pf psqs_pf => by simp [symm psqs_pf, pow_add, ps_pf, qs_pf] <;> ac_rfl
#align tactic.ring_exp.mul_pp_pf_overlap Tactic.RingExp.mul_pp_pf_overlap

theorem mul_pp_pf_prod_lt {pps p ps qqs pqs : α} :
    pps = p * ps → ps * qqs = pqs → pps * qqs = p * pqs := by cc
#align tactic.ring_exp.mul_pp_pf_prod_lt Tactic.RingExp.mul_pp_pf_prod_lt

theorem mul_pp_pf_prod_gt {pps qqs q qs pqs : α} :
    qqs = q * qs → pps * qs = pqs → pps * qqs = q * pqs := by cc
#align tactic.ring_exp.mul_pp_pf_prod_gt Tactic.RingExp.mul_pp_pf_prod_gt

/-- Multiply two expressions.

* `x * y = (x * y)` (for `x`, `y` coefficients)
* `x * (q * qs) = q * (qs * x)` (for `x` coefficient)
* `(p * ps) * y = p * (ps * y)` (for `y` coefficient)
* `(p_b^p_e * ps) * (p_b^q_e * qs) = p_b^(p_e + q_e) * (ps * qs)`
    (if `p_e` and `q_e` are identical except coefficient)
* `(p * ps) * (q * qs) = p * (ps * (q * qs))` (if `p.lt q`)
* `(p * ps) * (q * qs) = q * ((p * ps) * qs)` (if not `p.lt q`)
-/
unsafe def mul_pp : ex Prod → ex Prod → ring_exp_m (ex Prod)
  | ps@(ex.coeff _ x), qs@(ex.coeff _ y) => do
    let pq ← mul_coeff ps.pretty qs.pretty x y
    let pq_o ← mul_orig ps qs
    let 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 pq_o pf
  | ps@(ex.coeff _ x), qqs@(ex.prod _ q qs) => do
    let pqs ← mul_pp ps qs
    let pqqs ← ex_prod q pqs
    let pqqs_o ← mul_orig ps qqs
    let pf ←
      mk_proof `` mul_pf_c_prod [ps.orig, qqs.orig, q.pretty, qs.pretty, pqs.pretty]
          [qqs.info, pqs.info]
    pure <| pqqs pqqs_o pf
  | pps@(ex.prod _ p ps), qs@(ex.coeff _ y) => do
    let pqs ← mul_pp ps qs
    let ppqs ← ex_prod p pqs
    let ppqs_o ← mul_orig pps qs
    let pf ←
      mk_proof `` mul_pf_prod_c [pps.orig, p.pretty, ps.pretty, qs.orig, pqs.pretty]
          [pps.info, pqs.info]
    pure <| ppqs 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
    let ppqqs_o ← mul_orig pps qqs
    let pq_ol ← in_exponent <| add_overlap p_e q_e
    match pq_ol, p_b q_b with
      | overlap.nonzero pq_e, tt => do
        let psqs ← mul_pp ps qs
        let pq ← ex_exp p_b pq_e
        let ppsqqs ← ex_prod pq psqs
        let pf ←
          mk_proof `` mul_pp_pf_overlap [pps, p_b, ps, qqs, qs, ppsqqs, p_e, q_e] [pps, qqs, ppsqqs]
        pure <| ppsqqs ppqqs_o pf
      | _, _ =>
        if p q then do
          let pqs ← mul_pp ps qqs
          let ppqs ← ex_prod p pqs
          let pf ← mk_proof `` mul_pp_pf_prod_lt [pps, p, ps, qqs, pqs] [pps, pqs]
          pure <| ppqs ppqqs_o pf
        else do
          let pqs ← mul_pp pps qs
          let pqqs ← ex_prod q pqs
          let pf ← mk_proof `` mul_pp_pf_prod_gt [pps, qqs, q, qs, pqs] [qqs, pqs]
          pure <| pqqs ppqqs_o pf
#align tactic.ring_exp.mul_pp tactic.ring_exp.mul_pp

theorem mul_p_pf_zero {ps qs : α} : ps = 0 → ps * qs = 0 := fun ps_pf => by
  rw [ps_pf, MulZeroClass.zero_mul]
#align tactic.ring_exp.mul_p_pf_zero Tactic.RingExp.mul_p_pf_zero

theorem mul_p_pf_sum {pps p ps qs ppsqs : α} :
    pps = p + ps → p * qs + ps * qs = ppsqs → pps * qs = ppsqs := fun pps_pf ppsqs_pf =>
  calc
    pps * qs = (p + ps) * qs := by rw [pps_pf]
    _ = p * qs + ps * qs := (add_mul _ _ _)
    _ = ppsqs := ppsqs_pf

#align tactic.ring_exp.mul_p_pf_sum Tactic.RingExp.mul_p_pf_sum

/-- Multiply two expressions.

* `0 * qs = 0`
* `(p + ps) * qs = (p * qs) + (ps * qs)`
-/
unsafe def mul_p : ex Sum → ex Prod → ring_exp_m (ex Sum)
  | ps@(ex.zero ps_i), qs => do
    let z ← ex_zero
    let z_o ← mul_orig ps qs
    let pf ← mk_proof `` mul_p_pf_zero [ps.orig, qs.orig] [ps.info]
    pure <| z z_o pf
  | pps@(ex.sum pps_i p ps), qs => do
    let pqs ← mul_pp p qs >>= prod_to_sum
    let psqs ← mul_p ps qs
    let ppsqs ← add pqs psqs
    let pps_pf ← pps.proof_term
    let ppsqs_o ← mul_orig pps qs
    let ppsqs_pf ← ppsqs.proof_term
    let pf ←
      mk_proof `` mul_p_pf_sum [pps.orig, p.pretty, ps.pretty, qs.orig, ppsqs.pretty]
          [pps.info, ppsqs.info]
    pure <| ppsqs ppsqs_o pf
#align tactic.ring_exp.mul_p tactic.ring_exp.mul_p

theorem mul_pf_zero {ps qs : α} : qs = 0 → ps * qs = 0 := fun qs_pf => by
  rw [qs_pf, MulZeroClass.mul_zero]
#align tactic.ring_exp.mul_pf_zero Tactic.RingExp.mul_pf_zero

theorem mul_pf_sum {ps qqs q qs psqqs : α} :
    qqs = q + qs → ps * q + ps * qs = psqqs → ps * qqs = psqqs := fun qs_pf psqqs_pf =>
  calc
    ps * qqs = ps * (q + qs) := by rw [qs_pf]
    _ = ps * q + ps * qs := (mul_add _ _ _)
    _ = psqqs := psqqs_pf

#align tactic.ring_exp.mul_pf_sum Tactic.RingExp.mul_pf_sum

/-- Multiply two expressions.

* `ps * 0 = 0`
* `ps * (q + qs) = (ps * q) + (ps * qs)`
-/
unsafe def mul : ex Sum → ex Sum → ring_exp_m (ex Sum)
  | ps, qs@(ex.zero qs_i) => do
    let z ← ex_zero
    let z_o ← mul_orig ps qs
    let pf ← mk_proof `` mul_pf_zero [ps.orig, qs.orig] [qs.info]
    pure <| z z_o pf
  | ps, qqs@(ex.sum qqs_i q qs) => do
    let psq ← mul_p ps q
    let psqs ← mul ps qs
    let psqqs ← add psq psqs
    let psqqs_o ← mul_orig ps qqs
    let pf ←
      mk_proof `` mul_pf_sum [ps.orig, qqs.orig, q.orig, qs.orig, psqqs.pretty]
          [qqs.info, psqqs.info]
    pure <| psqqs psqqs_o pf
#align tactic.ring_exp.mul tactic.ring_exp.mul

end Multiplication

section Exponentiation

theorem pow_e_pf_exp {pps p : α} {ps qs psqs : ℕ} :
    pps = p ^ ps → ps * qs = psqs → pps ^ qs = p ^ psqs := fun 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]

#align tactic.ring_exp.pow_e_pf_exp Tactic.RingExp.pow_e_pf_exp

/-- Compute the exponentiation of two coefficients.

The returned value is of the form `ex.coeff _ (p ^ q)`,
with the proof of `expr.of_rat p ^ expr.of_rat q = expr.of_rat (p ^ q)`.
-/
unsafe def pow_coeff (p_p q_p : expr) (p q : Coeff) : ring_exp_m (ex Prod) := do
  let ctx ← get_context
  let pq' ← mk_pow [p_p, q_p]
  let (pq_p, pq_pf) ← lift <| norm_num.eval_pow pq'
  if q ≠ 1 then lift <| throwError "Only integer powers are supported, not {← q}."
    else pure <| ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 ^ q⟩
#align tactic.ring_exp.pow_coeff tactic.ring_exp.pow_coeff

/-- Exponentiate two expressions.

* `(p ^ ps) ^ qs = p ^ (ps * qs)`
-/
unsafe def pow_e : ex exp → ex Prod → ring_exp_m (ex exp)
  | pps@(ex.exp pps_i p ps), qs => do
    let psqs ← in_exponent <| mul_pp ps qs
    let ppsqs ← ex_exp p psqs
    let ppsqs_o ← pow_orig pps qs
    let pf ←
      mk_proof `` pow_e_pf_exp [pps.orig, p.pretty, ps.pretty, qs.orig, psqs.pretty]
          [pps.info, psqs.info]
    pure <| ppsqs ppsqs_o pf
#align tactic.ring_exp.pow_e tactic.ring_exp.pow_e

theorem pow_pp_pf_one {ps : α} {qs : ℕ} : ps = 1 → ps ^ qs = 1 := fun ps_pf => by
  rw [ps_pf, one_pow]
#align tactic.ring_exp.pow_pp_pf_one Tactic.RingExp.pow_pp_pf_one

theorem pow_pf_c_c {ps ps' pq : α} {qs qs' : ℕ} :
    ps = ps' → qs = qs' → ps' ^ qs' = pq → ps ^ qs = pq := by cc
#align tactic.ring_exp.pow_pf_c_c Tactic.RingExp.pow_pf_c_c

theorem pow_pp_pf_c {ps ps' pqs : α} {qs qs' : ℕ} :
    ps = ps' → qs = qs' → ps' ^ qs' = pqs → ps ^ qs = pqs * 1 := by simp <;> cc
#align tactic.ring_exp.pow_pp_pf_c Tactic.RingExp.pow_pp_pf_c

theorem pow_pp_pf_prod {pps p ps pqs psqs : α} {qs : ℕ} :
    pps = p * ps → p ^ qs = pqs → ps ^ qs = psqs → pps ^ qs = pqs * psqs :=
  fun pps_pf pqs_pf psqs_pf =>
  calc
    pps ^ qs = (p * ps) ^ qs := by rw [pps_pf]
    _ = p ^ qs * ps ^ qs := (mul_pow _ _ _)
    _ = pqs * psqs := by rw [pqs_pf, psqs_pf]

#align tactic.ring_exp.pow_pp_pf_prod Tactic.RingExp.pow_pp_pf_prod

/-- Exponentiate two expressions.

* `1 ^ qs = 1`
* `x ^ qs = x ^ qs` (for `x` coefficient)
* `(p * ps) ^ qs = p ^ qs + ps ^ qs`
-/
unsafe def pow_pp : ex Prod → ex Prod → ring_exp_m (ex Prod)
  | ps@(ex.coeff ps_i ⟨⟨1, 1, _, _⟩⟩), qs => do
    let o ← ex_one
    let o_o ← pow_orig ps qs
    let pf ← mk_proof `` pow_pp_pf_one [ps.orig, qs.orig] [ps.info]
    pure <| o o_o pf
  | ps@(ex.coeff ps_i x), qs@(ex.coeff qs_i y) => do
    let pq ← pow_coeff ps.pretty qs.pretty x y
    let pq_o ← pow_orig ps qs
    let pf ←
      mk_proof_or_refl pq.pretty `` pow_pf_c_c [ps.orig, ps.pretty, pq.pretty, qs.orig, qs.pretty]
          [ps.info, qs.info, pq.info]
    pure <| pq pq_o pf
  | ps@(ex.coeff ps_i x), qs => do
    let ps'' ← pure ps >>= prod_to_sum >>= ex_sum_b
    let pqs ← ex_exp ps'' qs
    let pqs_o ← pow_orig ps qs
    let pf ←
      mk_proof_or_refl pqs.pretty `` pow_pp_pf_c
          [ps.orig, ps.pretty, pqs.pretty, qs.orig, qs.pretty] [ps.info, qs.info, pqs.info]
    let pqs' ← exp_to_prod pqs
    pure <| pqs' pqs_o pf
  | pps@(ex.prod pps_i p ps), qs => do
    let pqs ← pow_e p qs
    let psqs ← pow_pp ps qs
    let ppsqs ← ex_prod pqs psqs
    let ppsqs_o ← pow_orig pps qs
    let pf ←
      mk_proof `` pow_pp_pf_prod [pps.orig, p.pretty, ps.pretty, pqs.pretty, psqs.pretty, qs.orig]
          [pps.info, pqs.info, psqs.info]
    pure <| ppsqs ppsqs_o pf
#align tactic.ring_exp.pow_pp tactic.ring_exp.pow_pp

theorem pow_p_pf_one {ps ps' : α} {qs : ℕ} : ps = ps' → qs = succ zero → ps ^ qs = ps' :=
  fun ps_pf qs_pf =>
  calc
    ps ^ qs = ps' ^ 1 := by rw [ps_pf, qs_pf]
    _ = ps' := pow_one _

#align tactic.ring_exp.pow_p_pf_one Tactic.RingExp.pow_p_pf_one

theorem pow_p_pf_zero {ps : α} {qs qs' : ℕ} : ps = 0 → qs = succ qs' → ps ^ qs = 0 :=
  fun ps_pf qs_pf =>
  calc
    ps ^ qs = 0 ^ succ qs' := by rw [ps_pf, qs_pf]
    _ = 0 := zero_pow (succ_pos qs')

#align tactic.ring_exp.pow_p_pf_zero Tactic.RingExp.pow_p_pf_zero

theorem pow_p_pf_succ {ps pqqs : α} {qs qs' : ℕ} :
    qs = succ qs' → ps * ps ^ qs' = pqqs → ps ^ qs = pqqs := fun qs_pf pqqs_pf =>
  calc
    ps ^ qs = ps ^ succ qs' := by rw [qs_pf]
    _ = ps * ps ^ qs' := (pow_succ _ _)
    _ = pqqs := by rw [pqqs_pf]

#align tactic.ring_exp.pow_p_pf_succ Tactic.RingExp.pow_p_pf_succ

theorem pow_p_pf_singleton {pps p pqs : α} {qs : ℕ} : pps = p + 0 → p ^ qs = pqs → pps ^ qs = pqs :=
  fun pps_pf pqs_pf => by rw [pps_pf, add_zero, pqs_pf]
#align tactic.ring_exp.pow_p_pf_singleton Tactic.RingExp.pow_p_pf_singleton

theorem pow_p_pf_cons {ps ps' : α} {qs qs' : ℕ} : ps = ps' → qs = qs' → ps ^ qs = ps' ^ qs' := by cc
#align tactic.ring_exp.pow_p_pf_cons Tactic.RingExp.pow_p_pf_cons

/-- Exponentiate two expressions.

* `ps ^ 1 = ps`
* `0 ^ qs = 0` (note that this is handled *after* `ps ^ 0 = 1`)
* `(p + 0) ^ qs = p ^ qs`
* `ps ^ (qs + 1) = ps * ps ^ qs` (note that this is handled *after* `p + 0 ^ qs = p ^ qs`)
* `ps ^ qs = ps ^ qs` (otherwise)
-/
unsafe def pow_p : ex Sum → ex Prod → ring_exp_m (ex Sum)
  | ps, qs@(ex.coeff qs_i ⟨⟨1, 1, _, _⟩⟩) => do
    let ps_o ← pow_orig ps qs
    let pf ← mk_proof `` pow_p_pf_one [ps.orig, ps.pretty, qs.orig] [ps.info, qs.info]
    pure <| ps ps_o pf
  | ps@(ex.zero ps_i), qs@(ex.coeff qs_i ⟨⟨succ y, 1, _, _⟩⟩) => do
    let ctx ← get_context
    let z ← ex_zero
    let qs_pred ← lift <| expr.of_nat ctx.info_e.α y
    let pf ← mk_proof `` pow_p_pf_zero [ps.orig, qs.orig, qs_pred] [ps.info, qs.info]
    let z_o ← pow_orig ps qs
    pure <| z z_o pf
  | pps@(ex.sum pps_i p (ex.zero _)), qqs => do
    let pqs ← pow_pp p qqs
    let pqs_o ← pow_orig pps qqs
    let pf ←
      mk_proof `` pow_p_pf_singleton [pps.orig, p.pretty, pqs.pretty, qqs.orig] [pps.info, pqs.info]
    prod_to_sum <| pqs pqs_o pf
  | ps, qs@(ex.coeff qs_i ⟨⟨Int.ofNat (succ n), 1, den_pos, _⟩⟩) => do
    let qs' ← in_exponent <| ex_coeff ⟨Int.ofNat n, 1, den_pos, coprime_one_right _⟩
    let pqs ← pow_p ps qs'
    let pqqs ← mul ps pqs
    let pqqs_o ← pow_orig ps qs
    let pf ←
      mk_proof `` pow_p_pf_succ [ps.orig, pqqs.pretty, qs.orig, qs'.pretty] [qs.info, pqqs.info]
    pure <| pqqs pqqs_o pf
  | pps, qqs => do
    let pps'
      ←-- fallback: treat them as atoms
          ex_sum_b
          pps
    let psqs ← ex_exp pps' qqs
    let psqs_o ← pow_orig pps qqs
    let pf ←
      mk_proof_or_refl psqs.pretty `` pow_p_pf_cons [pps.orig, pps.pretty, qqs.orig, qqs.pretty]
          [pps.info, qqs.info]
    exp_to_prod (psqs psqs_o pf) >>= prod_to_sum
#align tactic.ring_exp.pow_p tactic.ring_exp.pow_p

theorem pow_pf_zero {ps : α} {qs : ℕ} : qs = 0 → ps ^ qs = 1 := fun qs_pf =>
  calc
    ps ^ qs = ps ^ 0 := by rw [qs_pf]
    _ = 1 := pow_zero _

#align tactic.ring_exp.pow_pf_zero Tactic.RingExp.pow_pf_zero

theorem pow_pf_sum {ps psqqs : α} {qqs q qs : ℕ} :
    qqs = q + qs → ps ^ q * ps ^ qs = psqqs → ps ^ qqs = psqqs := fun qqs_pf psqqs_pf =>
  calc
    ps ^ qqs = ps ^ (q + qs) := by rw [qqs_pf]
    _ = ps ^ q * ps ^ qs := (pow_add _ _ _)
    _ = psqqs := psqqs_pf

#align tactic.ring_exp.pow_pf_sum Tactic.RingExp.pow_pf_sum

/-- Exponentiate two expressions.

* `ps ^ 0 = 1`
* `ps ^ (q + qs) = ps ^ q * ps ^ qs`
-/
unsafe def pow : ex Sum → ex Sum → ring_exp_m (ex Sum)
  | ps, qs@(ex.zero qs_i) => do
    let o ← ex_one
    let o_o ← pow_orig ps qs
    let pf ← mk_proof `` pow_pf_zero [ps.orig, qs.orig] [qs.info]
    prod_to_sum <| o o_o pf
  | ps, qqs@(ex.sum qqs_i q qs) => do
    let psq ← pow_p ps q
    let psqs ← pow ps qs
    let psqqs ← mul psq psqs
    let psqqs_o ← pow_orig ps qqs
    let pf ←
      mk_proof `` pow_pf_sum [ps.orig, psqqs.pretty, qqs.orig, q.pretty, qs.pretty]
          [qqs.info, psqqs.info]
    pure <| psqqs psqqs_o pf
#align tactic.ring_exp.pow tactic.ring_exp.pow

end Exponentiation

theorem simple_pf_sum_zero {p p' : α} : p = p' → p + 0 = p' := by simp
#align tactic.ring_exp.simple_pf_sum_zero Tactic.RingExp.simple_pf_sum_zero

theorem simple_pf_prod_one {p p' : α} : p = p' → p * 1 = p' := by simp
#align tactic.ring_exp.simple_pf_prod_one Tactic.RingExp.simple_pf_prod_one

theorem simple_pf_prod_neg_one {α} [Ring α] {p p' : α} : p = p' → p * -1 = -p' := by simp
#align tactic.ring_exp.simple_pf_prod_neg_one Tactic.RingExp.simple_pf_prod_neg_one

theorem simple_pf_var_one (p : α) : p ^ 1 = p := by simp
#align tactic.ring_exp.simple_pf_var_one Tactic.RingExp.simple_pf_var_one

theorem simple_pf_exp_one {p p' : α} : p = p' → p ^ 1 = p' := by simp
#align tactic.ring_exp.simple_pf_exp_one Tactic.RingExp.simple_pf_exp_one

/-- Give a simpler, more human-readable representation of the normalized expression.

Normalized expressions might have the form `a^1 * 1 + 0`,
since the dummy operations reduce special cases in pattern-matching.
Humans prefer to read `a` instead.
This tactic gets rid of the dummy additions, multiplications and exponentiations.

Returns a normalized expression `e'` and a proof that `e.pretty = e'`.
-/
unsafe def ex.simple : ∀ {et : ExType}, ex et → ring_exp_m (expr × expr)
  | Sum, pps@(ex.sum pps_i p (ex.zero _)) => do
    let (p_p, p_pf) ← p.simple
    Prod.mk p_p <$> mk_app_csr `` simple_pf_sum_zero [p, p_p, p_pf]
  | Sum, ex.sum pps_i p ps => do
    let (p_p, p_pf) ← p.simple
    let (ps_p, ps_pf) ← ps.simple
    Prod.mk <$> mk_add [p_p, ps_p] <*> mk_app_csr `` sum_congr [p, p_p, ps, ps_p, p_pf, ps_pf]
  | Prod, ex.prod pps_i p (ex.coeff _ ⟨⟨1, 1, _, _⟩⟩) => do
    let (p_p, p_pf) ← p.simple
    Prod.mk p_p <$> mk_app_csr `` simple_pf_prod_one [p, p_p, p_pf]
  | Prod, pps@(ex.prod pps_i p (ex.coeff _ ⟨⟨-1, 1, _, _⟩⟩)) => do
    let ctx ← get_context
    match ctx with
      | none => Prod.mk pps <$> lift (mk_eq_refl pps)
      | some ringi => do
        let (p_p, p_pf) ← p
        Prod.mk <$> lift (mk_app `` Neg.neg [p_p]) <*>
            mk_app_class `` simple_pf_prod_neg_one ringi [p, p_p, p_pf]
  | Prod, ex.prod pps_i p ps => do
    let (p_p, p_pf) ← p.simple
    let (ps_p, ps_pf) ← ps.simple
    Prod.mk <$> mk_mul [p_p, ps_p] <*> mk_app_csr `` prod_congr [p, p_p, ps, ps_p, p_pf, ps_pf]
  | base, ex.sum_b pps_i ps => ps.simple
  | exp, ex.exp pps_i p (ex.coeff _ ⟨⟨1, 1, _, _⟩⟩) => do
    let (p_p, p_pf) ← p.simple
    Prod.mk p_p <$> mk_app_csr `` simple_pf_exp_one [p, p_p, p_pf]
  | exp, ex.exp pps_i p ps => do
    let (p_p, p_pf) ← p.simple
    let (ps_p, ps_pf) ← in_exponent <| ps.simple
    Prod.mk <$> mk_pow [p_p, ps_p] <*> mk_app_csr `` exp_congr [p, p_p, ps, ps_p, p_pf, ps_pf]
  | et, ps => Prod.mk ps.pretty <$> lift (mk_eq_refl ps.pretty)
#align tactic.ring_exp.ex.simple tactic.ring_exp.ex.simple

/-- Performs a lookup of the atom `a` in the list of known atoms,
or allocates a new one.

If `a` is not definitionally equal to any of the list's entries,
a new atom is appended to the list and returned.
The index of this atom is kept track of in the second inductive argument.

This function is mostly useful in `resolve_atom`,
which updates the state with the new list of atoms.
-/
unsafe def resolve_atom_aux (a : expr) : List atom → ℕ → ring_exp_m (atom × List atom)
  | [], n =>
    let atm : atom := ⟨a, n⟩
    pure (atm, [atm])
  | bas@(b :: as), n => do
    let ctx ← get_context
    (lift <| is_def_eq a b ctx >> pure (b, bas)) <|> do
        let (atm, as') ← resolve_atom_aux as (succ n)
        pure (atm, b :: as')
#align tactic.ring_exp.resolve_atom_aux tactic.ring_exp.resolve_atom_aux

/-- Convert the expression to an atom:
either look up a definitionally equal atom,
or allocate it as a new atom.

You probably want to use `eval_base` if `eval` doesn't work
instead of directly calling `resolve_atom`,
since `eval_base` can also handle numerals.
-/
unsafe def resolve_atom (a : expr) : ring_exp_m atom := do
  let atoms ← ReaderT.lift <| StateT.get
  let (atm, atoms') ← resolve_atom_aux a atoms 0
  ReaderT.lift <| StateT.put atoms'
  pure atm
#align tactic.ring_exp.resolve_atom tactic.ring_exp.resolve_atom

/-- Treat the expression atomically: as a coefficient or atom.

Handles cases where `eval` cannot treat the expression as a known operation
because it is just a number or single variable.
-/
unsafe def eval_base (ps : expr) : ring_exp_m (ex Sum) :=
  match ps.to_rat with
  | some ⟨0, 1, _, _⟩ => ex_zero
  | some x => ex_coeff x >>= prod_to_sum
  | none => do
    let a ← resolve_atom ps
    atom_to_sum a
#align tactic.ring_exp.eval_base tactic.ring_exp.eval_base

theorem negate_pf {α} [Ring α] {ps ps' : α} : -1 * ps = ps' → -ps = ps' := by simp
#align tactic.ring_exp.negate_pf Tactic.RingExp.negate_pf

/-- Negate an expression by multiplying with `-1`.

Only works if there is a `ring` instance; otherwise it will `fail`.
-/
unsafe def negate (ps : ex Sum) : ring_exp_m (ex Sum) := do
  let ctx ← get_context
  match ctx with
    | none => lift <| fail "internal error: negate called in semiring"
    | some ring_instance => do
      let minus_one ← ex_coeff (-1) >>= prod_to_sum
      let ps' ← mul minus_one ps
      let ps_pf ← ps'
      let pf ← mk_app_class `` negate_pf ring_instance [ps, ps', ps_pf]
      let ps'_o ← lift <| mk_app `` Neg.neg [ps]
      pure <| ps' ps'_o pf
#align tactic.ring_exp.negate tactic.ring_exp.negate

theorem inverse_pf {α} [DivisionRing α] {ps ps_u ps_p e' e'' : α} :
    ps = ps_u → ps_u = ps_p → ps_p⁻¹ = e' → e' = e'' → ps⁻¹ = e'' := by cc
#align tactic.ring_exp.inverse_pf Tactic.RingExp.inverse_pf

/-- Invert an expression by simplifying, applying `has_inv.inv` and treating the result as an atom.

Only works if there is a `division_ring` instance; otherwise it will `fail`.
-/
unsafe def inverse (ps : ex Sum) : ring_exp_m (ex Sum) := do
  let ctx ← get_context
  let dri ←
    match ctx.info_b.dr_instance with
      | none => lift <| fail "division is only supported in a division ring"
      | some dri => pure dri
  let (ps_simple, ps_simple_pf) ← ps.simple
  let e ← lift <| mk_app `` Inv.inv [ps_simple]
  let (e', e_pf) ← lift (norm_num.derive e) <|> (fun e_pf => (e, e_pf)) <$> lift (mk_eq_refl e)
  let e'' ← eval_base e'
  let ps_pf ← ps.proof_term
  let e''_pf ← e''.proof_term
  let pf ←
    mk_app_class `` inverse_pf dri
        [ps.orig, ps.pretty, ps_simple, e', e''.pretty, ps_pf, ps_simple_pf, e_pf, e''_pf]
  let e''_o ← lift <| mk_app `` Inv.inv [ps.orig]
  pure <| e'' e''_o pf
#align tactic.ring_exp.inverse tactic.ring_exp.inverse

theorem sub_pf {α} [Ring α] {ps qs psqs : α} (h : ps + -qs = psqs) : ps - qs = psqs := by
  rwa [sub_eq_add_neg]
#align tactic.ring_exp.sub_pf Tactic.RingExp.sub_pf

theorem div_pf {α} [DivisionRing α] {ps qs psqs : α} (h : ps * qs⁻¹ = psqs) : ps / qs = psqs := by
  rwa [div_eq_mul_inv]
#align tactic.ring_exp.div_pf Tactic.RingExp.div_pf

end Operations

section Wiring

/-!
### `wiring` section

This section deals with going from `expr` to `ex` and back.

The main attraction is `eval`, which uses `add`, `mul`, etc.
to calculate an `ex` from a given `expr`.
Other functions use `ex`es to produce `expr`s together with a proof,
or produce the context to run `ring_exp_m` from an `expr`.
-/

open Tactic

open ExType

-- failed to format: unknown constant 'term.pseudo.antiquot'
/--
      Compute a normalized form (of type `ex`) from an expression (of type `expr`).

      This is the main driver of the `ring_exp` tactic,
      calling out to `add`, `mul`, `pow`, etc. to parse the `expr`.
      -/
    unsafe
  def
    eval
    : expr → ring_exp_m ( ex Sum )
    | e @ q( $ ( ps ) + $ ( qs ) ) => do let ps' ← eval ps let qs' ← eval qs add ps' qs'
      |
        ps_o @ q( Nat.succ $ ( p_o ) )
        =>
        do
          let ps' ← eval q( $ ( p_o ) + 1 )
            let pf ← lift <| mk_app ` ` Nat.succ_eq_add_one [ p_o ]
            rewrite ps_o ps' pf
      |
        e @ q( $ ( ps ) - $ ( qs ) )
        =>
        (
            do
              let ctx ← get_context
                let
                  ri
                    ←
                    match
                      ctx . info_b . ring_instance
                      with
                      | none => lift <| fail "subtraction is not directly supported in a semiring"
                        | some ri => pure ri
                let ps' ← eval ps
                let qs' ← eval qs >>= negate
                let psqs ← add ps' qs'
                let psqs_pf ← psqs . proof_term
                let pf ← mk_app_class ` ` sub_pf ri [ ps , qs , psqs . pretty , psqs_pf ]
                pure ( psqs e pf )
            )
          <|>
          eval_base e
      | e @ q( - $ ( ps ) ) => do let ps' ← eval ps negate ps' <|> eval_base e
      | e @ q( $ ( ps ) * $ ( qs ) ) => do let ps' ← eval ps let qs' ← eval qs mul ps' qs'
      | e @ q( Inv.inv $ ( ps ) ) => do let ps' ← eval ps inverse ps' <|> eval_base e
      |
        e @ q( $ ( ps ) / $ ( qs ) )
        =>
        do
          let ctx ← get_context
            let
              dri
                ←
                match
                  ctx . info_b . dr_instance
                  with
                  | none => lift <| fail "division is only directly supported in a division ring"
                    | some dri => pure dri
            let ps' ← eval ps
            let qs' ← eval qs
            (
                do
                  let qs'' ← inverse qs'
                    let psqs ← mul ps' qs''
                    let psqs_pf ← psqs
                    let pf ← mk_app_class ` ` div_pf dri [ ps , qs , psqs , psqs_pf ]
                    pure ( psqs e pf )
                )
              <|>
              eval_base e
      |
        e @ q( @ Pow.pow _ _ $ ( hp_instance ) $ ( ps ) $ ( qs ) )
        =>
        do
          let ctx ← get_context
            let ps' ← eval ps
            let qs' ← in_exponent <| eval qs
            let psqs ← pow ps' qs'
            let psqs_pf ← psqs . proof_term
            (
                do
                  lift
                      (
                        is_def_eq hp_instance ctx
                          <|>
                          fail "has_pow instance must be nat.has_pow or monoid.has_pow"
                        )
                    let has_pow_pf ← lift <| mk_eq_refl e
                    let pf ← lift <| mk_eq_trans has_pow_pf psqs_pf
                    pure <| psqs e pf
                )
              <|>
              eval_base e
      | ps => eval_base ps
#align tactic.ring_exp.eval tactic.ring_exp.eval

/-- Run `eval` on the expression and return the result together with normalization proof.

See also `eval_simple` if you want something that behaves like `norm_num`.
-/
unsafe def eval_with_proof (e : expr) : ring_exp_m (ex Sum × expr) := do
  let e' ← eval e
  Prod.mk e' <$> e'
#align tactic.ring_exp.eval_with_proof tactic.ring_exp.eval_with_proof

/-- Run `eval` on the expression and simplify the result.

Returns a simplified normalized expression, together with an equality proof.

See also `eval_with_proof` if you just want to check the equality of two expressions.
-/
unsafe def eval_simple (e : expr) : ring_exp_m (expr × expr) := do
  let (complicated, complicated_pf) ← eval_with_proof e
  let (simple, simple_pf) ← complicated.simple
  Prod.mk simple <$> lift (mk_eq_trans complicated_pf simple_pf)
#align tactic.ring_exp.eval_simple tactic.ring_exp.eval_simple

/-- Compute the `eval_info` for a given type `α`. -/
unsafe def make_eval_info (α : expr) : tactic eval_info := do
  let u ← mk_meta_univ
  infer_type α >>= unify (expr.sort (level.succ u))
  let u ← get_univ_assignment u
  let csr_instance ← mk_app `` CommSemiring [α] >>= mk_instance
  let ring_instance ← some <$> (mk_app `` Ring [α] >>= mk_instance) <|> pure none
  let dr_instance ← some <$> (mk_app `` DivisionRing [α] >>= mk_instance) <|> pure none
  let ha_instance ← mk_app `` Add [α] >>= mk_instance
  let hm_instance ← mk_app `` Mul [α] >>= mk_instance
  let hp_instance ← mk_mapp `` Monoid.Pow [some α, none]
  let z ← mk_mapp `` Zero.zero [α, none]
  let o ← mk_mapp `` One.one [α, none]
  pure ⟨α, u, csr_instance, ha_instance, hm_instance, hp_instance, ring_instance, dr_instance, z, o⟩
#align tactic.ring_exp.make_eval_info tactic.ring_exp.make_eval_info

/-- Use `e` to build the context for running `mx`. -/
unsafe def run_ring_exp {α} (transp : Transparency) (e : expr) (mx : ring_exp_m α) : tactic α := do
  let info_b ← infer_type e >>= make_eval_info
  let info_e ← mk_const `` Nat >>= make_eval_info
  (fun x : _ × _ => x.1) <$> StateT.run (ReaderT.run mx ⟨info_b, info_e, transp⟩) []
#align tactic.ring_exp.run_ring_exp tactic.ring_exp.run_ring_exp

/-- Repeatedly apply `eval_simple` on (sub)expressions. -/
unsafe def normalize (transp : Transparency) (e : expr) : tactic (expr × expr) := do
  let (_, e', pf') ←
    ext_simplify_core () { } simp_lemmas.mk (fun _ => failed)
        (fun _ _ _ _ e => do
          let (e'', pf) ← run_ring_exp transp e <| eval_simple e
          guard ¬e'' == e
          return ((), e'', some pf, ff))
        (fun _ _ _ _ _ => failed) `eq e
  pure (e', pf')
#align tactic.ring_exp.normalize tactic.ring_exp.normalize

end Wiring

end Tactic.RingExp

namespace Tactic.Interactive

open Interactive Interactive.Types Lean.Parser Tactic Tactic.RingExp

-- mathport name: parser.optional
local postfix:1024 "?" => optional

/-- Tactic for solving equations of *commutative* (semi)rings,
allowing variables in the exponent.
This version of `ring_exp` fails if the target is not an equality.

The variant `ring_exp_eq!` will use a more aggressive reducibility setting
to determine equality of atoms.
-/
unsafe def ring_exp_eq (red : parse (tk "!")?) : tactic Unit := do
  let q(Eq $(ps) $(qs)) ← target >>= whnf
  let transp := if red.isSome then semireducible else reducible
  let ((ps', ps_pf), (qs', qs_pf)) ←
    run_ring_exp transp ps <| Prod.mk <$> eval_with_proof ps <*> eval_with_proof qs
  if ps' qs' then do
      let qs_pf_inv ← mk_eq_symm qs_pf
      let pf ← mk_eq_trans ps_pf qs_pf_inv
      tactic.interactive.exact ``($(pf))
    else fail "ring_exp failed to prove equality"
#align tactic.interactive.ring_exp_eq tactic.interactive.ring_exp_eq

/-- Tactic for evaluating expressions in *commutative* (semi)rings, allowing for variables in the
exponent.

This tactic extends `ring`: it should solve every goal that `ring` can solve.
Additionally, it knows how to evaluate expressions with complicated exponents
(where `ring` only understands constant exponents).
The variants `ring_exp!` and `ring_exp_eq!` use a more aggessive reducibility setting to determine
equality of atoms.

For example:
```lean
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring_exp
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring_exp
example (x y : ℕ) : x + id y = y + id x := by ring_exp!
```
-/
unsafe def ring_exp (red : parse (tk "!")?) (loc : parse location) : tactic Unit :=
  (match loc with
    | Interactive.Loc.ns [none] => ring_exp_eq red
    | _ => failed) <|>
    do
    let ns ← loc.get_locals
    let transp := if red.isSome then semireducible else reducible
    let tt ← tactic.replace_at (normalize transp) ns loc.include_goal |
      fail "ring_exp failed to simplify"
    when loc <| try tactic.reflexivity
#align tactic.interactive.ring_exp tactic.interactive.ring_exp

add_tactic_doc
  { Name := "ring_exp"
    category := DocCategory.tactic
    declNames := [`tactic.interactive.ring_exp]
    tags := ["arithmetic", "simplification", "decision procedure"] }

end Tactic.Interactive

namespace Conv.Interactive

open Conv Interactive

open Tactic

open Tactic.Interactive (ring_exp_eq)

open Tactic.RingExp (normalize)

-- mathport name: parser.optional
local postfix:1024 "?" => optional

/-- Normalises expressions in commutative (semi-)rings inside of a `conv` block using the tactic
`ring_exp`.
-/
unsafe def ring_exp (red : parse (lean.parser.tk "!")?) : conv Unit :=
  let transp := if red.isSome then semireducible else reducible
  discharge_eq_lhs (ring_exp_eq red) <|>
    replace_lhs (normalize transp) <|> fail "ring_exp failed to simplify"
#align conv.interactive.ring_exp conv.interactive.ring_exp

end Conv.Interactive


text:
/-
Copyright (c) 2022 Yaël Dillies, Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies, Bhavik Mehta

! This file was ported from Lean 3 source module combinatorics.simple_graph.density
! leanprover-community/mathlib commit a4ec43f53b0bd44c697bcc3f5a62edd56f269ef1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Order.Partition.Finpartition
import Mathlib.Tactic.Positivity

/-!
# Edge density

This file defines the number and density of edges of a relation/graph.

## Main declarations

Between two finsets of vertices,
* `Rel.interedges`: Finset of edges of a relation.
* `Rel.edgeDensity`: Edge density of a relation.
* `SimpleGraph.interedges`: Finset of edges of a graph.
* `SimpleGraph.edgeDensity`: Edge density of a graph.
-/

open Finset

open BigOperators

variable {𝕜 ι κ α β : Type _}

/-! ### Density of a relation -/

namespace Rel

section Asymmetric

variable [LinearOrderedField 𝕜] (r : α → β → Prop) [∀ a, DecidablePred (r a)] {s s₁ s₂ : Finset α}
  {t t₁ t₂ : Finset β} {a : α} {b : β} {δ : 𝕜}

/-- Finset of edges of a relation between two finsets of vertices. -/
def interedges (s : Finset α) (t : Finset β) : Finset (α × β) :=
  (s ×ᶠ t).filter fun e ↦ r e.1 e.2
#align rel.interedges Rel.interedges

/-- Edge density of a relation between two finsets of vertices. -/
def edgeDensity (s : Finset α) (t : Finset β) : ℚ :=
  (interedges r s t).card / (s.card * t.card)
#align rel.edge_density Rel.edgeDensity

variable {r}

theorem mem_interedges_iff {x : α × β} : x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2 := by
  rw [interedges, mem_filter, Finset.mem_product, and_assoc]
#align rel.mem_interedges_iff Rel.mem_interedges_iff

@[simp]
theorem interedges_empty_left (t : Finset β) : interedges r ∅ t = ∅ := by
  rw [interedges, Finset.empty_product, filter_empty]
#align rel.interedges_empty_left Rel.interedges_empty_left

theorem interedges_mono (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) : interedges r s₂ t₂ ⊆ interedges r s₁ t₁ :=
  fun x ↦ by
    simp_rw [mem_interedges_iff]
    exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩
#align rel.interedges_mono Rel.interedges_mono

variable (r)

theorem card_interedges_add_card_interedges_compl (s : Finset α) (t : Finset β) :
    (interedges r s t).card + (interedges (fun x y ↦ ¬r x y) s t).card = s.card * t.card := by
  classical
  rw [← card_product, interedges, interedges, ← card_union_eq, filter_union_filter_neg_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
#align rel.card_interedges_add_card_interedges_compl Rel.card_interedges_add_card_interedges_compl

theorem interedges_disjoint_left {s s' : Finset α} (hs : Disjoint s s') (t : Finset β) :
    Disjoint (interedges r s t) (interedges r s' t) := by
  rw [Finset.disjoint_left] at hs⊢
  intro _ hx hy
  rw [mem_interedges_iff] at hx hy
  exact hs hx.1 hy.1
#align rel.interedges_disjoint_left Rel.interedges_disjoint_left

theorem interedges_disjoint_right (s : Finset α) {t t' : Finset β} (ht : Disjoint t t') :
    Disjoint (interedges r s t) (interedges r s t') := by
  rw [Finset.disjoint_left] at ht⊢
  intro _ hx hy
  rw [mem_interedges_iff] at hx hy
  exact ht hx.2.1 hy.2.1
#align rel.interedges_disjoint_right Rel.interedges_disjoint_right

section DecidableEq

variable [DecidableEq α] [DecidableEq β]

theorem interedges_bunionᵢ_left (s : Finset ι) (t : Finset β) (f : ι → Finset α) :
    interedges r (s.bunionᵢ f) t = s.bunionᵢ fun a ↦ interedges r (f a) t := by
  ext
  simp only [mem_bunionᵢ, mem_interedges_iff, exists_and_right, ← and_assoc]
#align rel.interedges_bUnion_left Rel.interedges_bunionᵢ_left

theorem interedges_bunionᵢ_right (s : Finset α) (t : Finset ι) (f : ι → Finset β) :
    interedges r s (t.bunionᵢ f) = t.bunionᵢ fun b ↦ interedges r s (f b) := by
  ext a
  simp only [mem_interedges_iff, mem_bunionᵢ]
  exact ⟨fun ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩ ↦ ⟨x₂, x₃, x₁, x₄, x₅⟩,
    fun ⟨x₂, x₃, x₁, x₄, x₅⟩ ↦ ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩⟩
#align rel.interedges_bUnion_right Rel.interedges_bunionᵢ_right

theorem interedges_bunionᵢ (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset β) :
    interedges r (s.bunionᵢ f) (t.bunionᵢ g) =
      (s ×ᶠ t).bunionᵢ fun ab ↦ interedges r (f ab.1) (g ab.2) := by
  simp_rw [product_bunionᵢ, interedges_bunionᵢ_left, interedges_bunionᵢ_right]
#align rel.interedges_bUnion Rel.interedges_bunionᵢ

end DecidableEq

theorem card_interedges_le_mul (s : Finset α) (t : Finset β) :
    (interedges r s t).card ≤ s.card * t.card :=
  (card_filter_le _ _).trans (card_product _ _).le
#align rel.card_interedges_le_mul Rel.card_interedges_le_mul

theorem edgeDensity_nonneg (s : Finset α) (t : Finset β) : 0 ≤ edgeDensity r s t := by
  apply div_nonneg <;> exact_mod_cast Nat.zero_le _
#align rel.edge_density_nonneg Rel.edgeDensity_nonneg

theorem edgeDensity_le_one (s : Finset α) (t : Finset β) : edgeDensity r s t ≤ 1 := by
  apply div_le_one_of_le
  · exact_mod_cast card_interedges_le_mul r s t
  · exact_mod_cast Nat.zero_le _
#align rel.edge_density_le_one Rel.edgeDensity_le_one

theorem edgeDensity_add_edgeDensity_compl (hs : s.Nonempty) (ht : t.Nonempty) :
    edgeDensity r s t + edgeDensity (fun x y ↦ ¬r x y) s t = 1 := by
  rw [edgeDensity, edgeDensity, div_add_div_same, div_eq_one_iff_eq]
  · exact_mod_cast card_interedges_add_card_interedges_compl r s t
  · exact_mod_cast (mul_pos hs.card_pos ht.card_pos).ne'
#align rel.edge_density_add_edge_density_compl Rel.edgeDensity_add_edgeDensity_compl

@[simp]
theorem edgeDensity_empty_left (t : Finset β) : edgeDensity r ∅ t = 0 := by
  rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]
#align rel.edge_density_empty_left Rel.edgeDensity_empty_left

@[simp]
theorem edgeDensity_empty_right (s : Finset α) : edgeDensity r s ∅ = 0 := by
  rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]
#align rel.edge_density_empty_right Rel.edgeDensity_empty_right

theorem card_interedges_finpartition_left [DecidableEq α] (P : Finpartition s) (t : Finset β) :
    (interedges r s t).card = ∑ a in P.parts, (interedges r a t).card := by
  classical
  simp_rw [← P.bunionᵢ_parts, interedges_bunionᵢ_left, id.def]
  rw [card_bunionᵢ]
  exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
#align rel.card_interedges_finpartition_left Rel.card_interedges_finpartition_left

theorem card_interedges_finpartition_right [DecidableEq β] (s : Finset α) (P : Finpartition t) :
    (interedges r s t).card = ∑ b in P.parts, (interedges r s b).card := by
  classical
  simp_rw [← P.bunionᵢ_parts, interedges_bunionᵢ_right, id]
  rw [card_bunionᵢ]
  exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)
#align rel.card_interedges_finpartition_right Rel.card_interedges_finpartition_right

theorem card_interedges_finpartition [DecidableEq α] [DecidableEq β] (P : Finpartition s)
    (Q : Finpartition t) :
    (interedges r s t).card = ∑ ab in P.parts ×ᶠ Q.parts, (interedges r ab.1 ab.2).card := by
  rw [card_interedges_finpartition_left _ P, sum_product]
  congr; ext
  rw [card_interedges_finpartition_right]
#align rel.card_interedges_finpartition Rel.card_interedges_finpartition

theorem mul_edgeDensity_le_edgeDensity (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty)
    (ht₂ : t₂.Nonempty) :
    (s₂.card : ℚ) / s₁.card * (t₂.card / t₁.card) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁ := by
  have hst : (s₂.card : ℚ) * t₂.card ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]
  rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel _ hst]
  refine' div_le_div_of_le (by exact_mod_cast (s₁.card * t₁.card).zero_le) _
  exact_mod_cast card_le_of_subset (interedges_mono hs ht)
#align rel.mul_edge_density_le_edge_density Rel.mul_edgeDensity_le_edgeDensity

theorem edgeDensity_sub_edgeDensity_le_one_sub_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty)
    (ht₂ : t₂.Nonempty) :
    edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁ ≤ 1 - s₂.card / s₁.card * (t₂.card / t₁.card) := by
  refine' (sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans _
  refine' le_trans _ (mul_le_of_le_one_right _ (edgeDensity_le_one r s₂ t₂))
  · rw [sub_mul, one_mul]
  refine' sub_nonneg_of_le (mul_le_one _ _ _)
  · exact div_le_one_of_le ((@Nat.cast_le ℚ).2 (card_le_of_subset hs)) (Nat.cast_nonneg _)
  · apply div_nonneg <;> exact_mod_cast Nat.zero_le _
  · exact div_le_one_of_le ((@Nat.cast_le ℚ).2 (card_le_of_subset ht)) (Nat.cast_nonneg _)
#align rel.edge_density_sub_edge_density_le_one_sub_mul Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul

theorem abs_edgeDensity_sub_edgeDensity_le_one_sub_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁)
    (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
    |edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - s₂.card / s₁.card * (t₂.card / t₁.card) := by
  refine' abs_sub_le_iff.2 ⟨edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂ ht₂, _⟩
  rw [← add_sub_cancel (edgeDensity r s₁ t₁) (edgeDensity (fun x y ↦ ¬r x y) s₁ t₁),
    ← add_sub_cancel (edgeDensity r s₂ t₂) (edgeDensity (fun x y ↦ ¬r x y) s₂ t₂),
    edgeDensity_add_edgeDensity_compl _ (hs₂.mono hs) (ht₂.mono ht),
    edgeDensity_add_edgeDensity_compl _ hs₂ ht₂, sub_sub_sub_cancel_left]
  exact edgeDensity_sub_edgeDensity_le_one_sub_mul _ hs ht hs₂ ht₂
#align rel.abs_edge_density_sub_edge_density_le_one_sub_mul Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul

theorem abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁)
    (hδ₀ : 0 ≤ δ) (hδ₁ : δ < 1) (hs₂ : (1 - δ) * s₁.card ≤ s₂.card)
    (ht₂ : (1 - δ) * t₁.card ≤ t₂.card) :
    |(edgeDensity r s₂ t₂ : 𝕜) - edgeDensity r s₁ t₁| ≤ 2 * δ - δ ^ 2 := by
  have hδ' : 0 ≤ 2 * δ - δ ^ 2 := by
    rw [sub_nonneg, sq]
    exact mul_le_mul_of_nonneg_right (hδ₁.le.trans (by norm_num)) hδ₀
  rw [← sub_pos] at hδ₁
  obtain rfl | hs₂' := s₂.eq_empty_or_nonempty
  · rw [Finset.card_empty, Nat.cast_zero] at hs₂
    simpa [edgeDensity, (nonpos_of_mul_nonpos_right hs₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
  obtain rfl | ht₂' := t₂.eq_empty_or_nonempty
  · rw [Finset.card_empty, Nat.cast_zero] at ht₂
    simpa [edgeDensity, (nonpos_of_mul_nonpos_right ht₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
  have hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ) := by
    -- Porting note: Originally `by ring`
    rw [mul_sub_left_distrib, mul_one, sub_sub, sub_sub_cancel, mul_sub_right_distrib, one_mul,
      two_mul, pow_two, add_sub_assoc]
  rw [hr]
  norm_cast
  refine'
    (Rat.cast_le.2 <| abs_edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂' ht₂').trans _
  push_cast
  have h₁ := hs₂'.mono hs
  have h₂ := ht₂'.mono ht
  refine' sub_le_sub_left (mul_le_mul ((le_div_iff _).2 hs₂) ((le_div_iff _).2 ht₂) hδ₁.le _) _
  · exact_mod_cast h₁.card_pos
  · exact_mod_cast h₂.card_pos
  · apply div_nonneg <;> exact_mod_cast Nat.zero_le _
#align rel.abs_edge_density_sub_edge_density_le_two_mul_sub_sq Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq

/-- If `s₂ ⊆ s₁`, `t₂ ⊆ t₁` and they take up all but a `δ`-proportion, then the difference in edge
densities is at most `2 * δ`. -/
theorem abs_edgeDensity_sub_edgeDensity_le_two_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hδ : 0 ≤ δ)
    (hscard : (1 - δ) * s₁.card ≤ s₂.card) (htcard : (1 - δ) * t₁.card ≤ t₂.card) :
    |(edgeDensity r s₂ t₂ : 𝕜) - edgeDensity r s₁ t₁| ≤ 2 * δ := by
  cases' lt_or_le δ 1 with h h
  · exact (abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq r hs ht hδ h hscard htcard).trans
      ((sub_le_self_iff _).2 <| sq_nonneg δ)
  rw [two_mul]
  refine' (abs_sub _ _).trans (add_le_add (le_trans _ h) (le_trans _ h)) <;>
    · rw [abs_of_nonneg]
      exact_mod_cast edgeDensity_le_one r _ _
      exact_mod_cast edgeDensity_nonneg r _ _
#align rel.abs_edge_density_sub_edge_density_le_two_mul Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul

end Asymmetric

section Symmetric

variable (r : α → α → Prop) [DecidableRel r] {s s₁ s₂ t t₁ t₂ : Finset α} {a b : α}

variable {r} (hr : Symmetric r)

-- include hr -- Porting note: Commented out.

@[simp]
theorem swap_mem_interedges_iff {x : α × α} : x.swap ∈ interedges r s t ↔ x ∈ interedges r t s := by
  rw [mem_interedges_iff, mem_interedges_iff, hr.iff]
  exact and_left_comm
#align rel.swap_mem_interedges_iff Rel.swap_mem_interedges_iff

theorem mk_mem_interedges_comm : (a, b) ∈ interedges r s t ↔ (b, a) ∈ interedges r t s :=
  @swap_mem_interedges_iff _ _ _ _ _ hr (b, a)
#align rel.mk_mem_interedges_comm Rel.mk_mem_interedges_comm

theorem card_interedges_comm (s t : Finset α) : (interedges r s t).card = (interedges r t s).card :=
  Finset.card_congr (fun (x : α × α) _ ↦ x.swap) (fun _ ↦ (swap_mem_interedges_iff hr).2)
    (fun _ _ _ _ h ↦ Prod.swap_injective h) fun x h ↦
    ⟨x.swap, (swap_mem_interedges_iff hr).2 h, x.swap_swap⟩
#align rel.card_interedges_comm Rel.card_interedges_comm

theorem edgeDensity_comm (s t : Finset α) : edgeDensity r s t = edgeDensity r t s := by
  rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]
#align rel.edge_density_comm Rel.edgeDensity_comm

end Symmetric

end Rel

open Rel

/-! ### Density of a graph -/

namespace SimpleGraph

variable (G : SimpleGraph α) [DecidableRel G.Adj] {s s₁ s₂ t t₁ t₂ : Finset α} {a b : α}

/-- Finset of edges of a relation between two finsets of vertices. -/
def interedges (s t : Finset α) : Finset (α × α) :=
  Rel.interedges G.Adj s t
#align simple_graph.interedges SimpleGraph.interedges

/-- Density of edges of a graph between two finsets of vertices. -/
def edgeDensity : Finset α → Finset α → ℚ :=
  Rel.edgeDensity G.Adj
#align simple_graph.edge_density SimpleGraph.edgeDensity

theorem interedges_def (s t : Finset α) :
    G.interedges s t = (s ×ᶠ t).filter fun e ↦ G.Adj e.1 e.2 :=
  rfl
#align simple_graph.interedges_def SimpleGraph.interedges_def

theorem edgeDensity_def (s t : Finset α) :
    G.edgeDensity s t = (G.interedges s t).card / (s.card * t.card) :=
  rfl
#align simple_graph.edge_density_def SimpleGraph.edgeDensity_def

@[simp]
theorem card_interedges_div_card (s t : Finset α) :
    ((G.interedges s t).card : ℚ) / (s.card * t.card) = G.edgeDensity s t :=
  rfl
#align simple_graph.card_interedges_div_card SimpleGraph.card_interedges_div_card

theorem mem_interedges_iff {x : α × α} : x ∈ G.interedges s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ G.Adj x.1 x.2 :=
  Rel.mem_interedges_iff
#align simple_graph.mem_interedges_iff SimpleGraph.mem_interedges_iff

theorem mk_mem_interedges_iff : (a, b) ∈ G.interedges s t ↔ a ∈ s ∧ b ∈ t ∧ G.Adj a b :=
  Rel.mk_mem_interedges_iff
#align simple_graph.mk_mem_interedges_iff SimpleGraph.mk_mem_interedges_iff

@[simp]
theorem interedges_empty_left (t : Finset α) : G.interedges ∅ t = ∅ :=
  Rel.interedges_empty_left _
#align simple_graph.interedges_empty_left SimpleGraph.interedges_empty_left

theorem interedges_mono : s₂ ⊆ s₁ → t₂ ⊆ t₁ → G.interedges s₂ t₂ ⊆ G.interedges s₁ t₁ :=
  Rel.interedges_mono
#align simple_graph.interedges_mono SimpleGraph.interedges_mono

theorem interedges_disjoint_left (hs : Disjoint s₁ s₂) (t : Finset α) :
    Disjoint (G.interedges s₁ t) (G.interedges s₂ t) :=
  Rel.interedges_disjoint_left _ hs _
#align simple_graph.interedges_disjoint_left SimpleGraph.interedges_disjoint_left

theorem interedges_disjoint_right (s : Finset α) (ht : Disjoint t₁ t₂) :
    Disjoint (G.interedges s t₁) (G.interedges s t₂) :=
  Rel.interedges_disjoint_right _ _ ht
#align simple_graph.interedges_disjoint_right SimpleGraph.interedges_disjoint_right

section DecidableEq

variable [DecidableEq α]

theorem interedges_bunionᵢ_left (s : Finset ι) (t : Finset α) (f : ι → Finset α) :
    G.interedges (s.bunionᵢ f) t = s.bunionᵢ fun a ↦ G.interedges (f a) t :=
  Rel.interedges_bunionᵢ_left _ _ _ _
#align simple_graph.interedges_bUnion_left SimpleGraph.interedges_bunionᵢ_left

theorem interedges_bunionᵢ_right (s : Finset α) (t : Finset ι) (f : ι → Finset α) :
    G.interedges s (t.bunionᵢ f) = t.bunionᵢ fun b ↦ G.interedges s (f b) :=
  Rel.interedges_bunionᵢ_right _ _ _ _
#align simple_graph.interedges_bUnion_right SimpleGraph.interedges_bunionᵢ_right

theorem interedges_bunionᵢ (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset α) :
    G.interedges (s.bunionᵢ f) (t.bunionᵢ g) =
      (s ×ᶠ t).bunionᵢ fun ab ↦ G.interedges (f ab.1) (g ab.2) :=
  Rel.interedges_bunionᵢ _ _ _ _ _
#align simple_graph.interedges_bUnion SimpleGraph.interedges_bunionᵢ

theorem card_interedges_add_card_interedges_compl (h : Disjoint s t) :
    (G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card := by
  rw [← card_product, interedges_def, interedges_def]
  have : ((s ×ᶠ t).filter fun e ↦ Gᶜ.Adj e.1 e.2) = (s ×ᶠ t).filter fun e ↦ ¬G.Adj e.1 e.2 := by
    refine' filter_congr fun x hx ↦ _
    rw [mem_product] at hx
    rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
  rw [this, ← card_union_eq, filter_union_filter_neg_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
#align simple_graph.card_interedges_add_card_interedges_compl SimpleGraph.card_interedges_add_card_interedges_compl

theorem edgeDensity_add_edgeDensity_compl (hs : s.Nonempty) (ht : t.Nonempty) (h : Disjoint s t) :
    G.edgeDensity s t + Gᶜ.edgeDensity s t = 1 := by
  rw [edgeDensity_def, edgeDensity_def, div_add_div_same, div_eq_one_iff_eq]
  · exact_mod_cast card_interedges_add_card_interedges_compl _ h
  -- Porting note: Wrote a workaround for `positivity` tactic.
  · apply mul_ne_zero <;> exact_mod_cast Nat.pos_iff_ne_zero.1 (Nonempty.card_pos ‹_›)
#align simple_graph.edge_density_add_edge_density_compl SimpleGraph.edgeDensity_add_edgeDensity_compl

end DecidableEq

theorem card_interedges_le_mul (s t : Finset α) : (G.interedges s t).card ≤ s.card * t.card :=
  Rel.card_interedges_le_mul _ _ _
#align simple_graph.card_interedges_le_mul SimpleGraph.card_interedges_le_mul

theorem edgeDensity_nonneg (s t : Finset α) : 0 ≤ G.edgeDensity s t :=
  Rel.edgeDensity_nonneg _ _ _
#align simple_graph.edge_density_nonneg SimpleGraph.edgeDensity_nonneg

theorem edgeDensity_le_one (s t : Finset α) : G.edgeDensity s t ≤ 1 :=
  Rel.edgeDensity_le_one _ _ _
#align simple_graph.edge_density_le_one SimpleGraph.edgeDensity_le_one

@[simp]
theorem edgeDensity_empty_left (t : Finset α) : G.edgeDensity ∅ t = 0 :=
  Rel.edgeDensity_empty_left _ _
#align simple_graph.edge_density_empty_left SimpleGraph.edgeDensity_empty_left

@[simp]
theorem edgeDensity_empty_right (s : Finset α) : G.edgeDensity s ∅ = 0 :=
  Rel.edgeDensity_empty_right _ _
#align simple_graph.edge_density_empty_right SimpleGraph.edgeDensity_empty_right

@[simp]
theorem swap_mem_interedges_iff {x : α × α} : x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s :=
  Rel.swap_mem_interedges_iff G.symm
#align simple_graph.swap_mem_interedges_iff SimpleGraph.swap_mem_interedges_iff

theorem mk_mem_interedges_comm : (a, b) ∈ G.interedges s t ↔ (b, a) ∈ G.interedges t s :=
  Rel.mk_mem_interedges_comm G.symm
#align simple_graph.mk_mem_interedges_comm SimpleGraph.mk_mem_interedges_comm

theorem edgeDensity_comm (s t : Finset α) : G.edgeDensity s t = G.edgeDensity t s :=
  Rel.edgeDensity_comm G.symm s t
#align simple_graph.edge_density_comm SimpleGraph.edgeDensity_comm

end SimpleGraph

/- Porting note: Commented out `Tactic` namespace.
namespace Tactic

open Positivity

/-- Extension for the `positivity` tactic: `Rel.edgeDensity` and `SimpleGraph.edgeDensity` are
always nonnegative. -/
@[positivity]
unsafe def positivity_edge_density : expr → tactic strictness
  | q(Rel.edgeDensity $(r) $(s) $(t)) =>
    nonnegative <$> mk_mapp `` Rel.edgeDensity_nonneg [none, none, r, none, s, t]
  | q(SimpleGraph.edgeDensity $(G) $(s) $(t)) =>
    nonnegative <$> mk_mapp `` SimpleGraph.edgeDensity_nonneg [none, G, none, s, t]
  | e =>
    pp e >>=
      fail ∘
        format.bracket "The expression `"
          "` isn't of the form `Rel.edgeDensity r s t` nor `SimpleGraph.edgeDensity G s t`"
#align tactic.positivity_edge_density Tactic.positivity_edge_density

end Tactic
-/

author: leanprover-community


text:
/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen

! This file was ported from Lean 3 source module ring_theory.adjoin.power_basis
! leanprover-community/mathlib commit 825edd3cd735e87495b0c2a2114fc3929eefce41
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.RingTheory.Adjoin.Basic
import Mathbin.RingTheory.PowerBasis
import Mathbin.LinearAlgebra.Matrix.Basis

/-!
# Power basis for `algebra.adjoin R {x}`

This file defines the canonical power basis on `algebra.adjoin R {x}`,
where `x` is an integral element over `R`.
-/

variable {K S : Type _} [Field K] [CommRing S] [Algebra K S]

namespace Algebra

open Polynomial

open PowerBasis

open BigOperators

/-- The elements `1, x, ..., x ^ (d - 1)` for a basis for the `K`-module `K[x]`,
where `d` is the degree of the minimal polynomial of `x`. -/
noncomputable def adjoin.powerBasisAux {x : S} (hx : IsIntegral K x) :
    Basis (Fin (minpoly K x).natDegree) K (adjoin K ({x} : Set S)) :=
  by
  have hST : Function.Injective (algebraMap (adjoin K ({x} : Set S)) S) := Subtype.coe_injective
  have hx' :
    IsIntegral K (show adjoin K ({x} : Set S) from ⟨x, subset_adjoin (Set.mem_singleton x)⟩) :=
    by
    apply (isIntegral_algebraMap_iff hST).mp
    convert hx
    infer_instance
  have minpoly_eq := minpoly.eq_of_algebraMap_eq hST hx' rfl
  apply
    @Basis.mk (Fin (minpoly K x).natDegree) _ (adjoin K {x}) fun i =>
      ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ)
  · have := linearIndependent_pow _
    rwa [minpoly_eq] at this
  · rintro ⟨y, hy⟩ _
    have := hx'.mem_span_pow
    rw [minpoly_eq] at this
    apply this
    · rw [adjoin_singleton_eq_range_aeval] at hy
      obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
      use f
      ext
      exact aeval_algebra_map_apply S (⟨x, _⟩ : adjoin K {x}) _
#align algebra.adjoin.power_basis_aux Algebra.adjoin.powerBasisAux

/-- The power basis `1, x, ..., x ^ (d - 1)` for `K[x]`,
where `d` is the degree of the minimal polynomial of `x`. See `algebra.adjoin.power_basis'` for
a version over a more general base ring. -/
@[simps gen dim]
noncomputable def adjoin.powerBasis {x : S} (hx : IsIntegral K x) :
    PowerBasis K (adjoin K ({x} : Set S))
    where
  gen := ⟨x, subset_adjoin (Set.mem_singleton x)⟩
  dim := (minpoly K x).natDegree
  Basis := adjoin.powerBasisAux hx
  basis_eq_pow := Basis.mk_apply _ _
#align algebra.adjoin.power_basis Algebra.adjoin.powerBasis

end Algebra

open Algebra

/-- The power basis given by `x` if `B.gen ∈ adjoin K {x}`. See `power_basis.of_gen_mem_adjoin'`
for a version over a more general base ring. -/
@[simps]
noncomputable def PowerBasis.ofGenMemAdjoin {x : S} (B : PowerBasis K S) (hint : IsIntegral K x)
    (hx : B.gen ∈ adjoin K ({x} : Set S)) : PowerBasis K S :=
  (Algebra.adjoin.powerBasis hint).map <|
    (Subalgebra.equivOfEq _ _ <| PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx).trans
      Subalgebra.topEquiv
#align power_basis.of_gen_mem_adjoin PowerBasis.ofGenMemAdjoin

section IsIntegral

namespace PowerBasis

open Polynomial

open Polynomial

variable {R : Type _} [CommRing R] [Algebra R S] [Algebra R K] [IsScalarTower R K S]

variable {A : Type _} [CommRing A] [Algebra R A] [Algebra S A]

variable [IsScalarTower R S A] {B : PowerBasis S A} (hB : IsIntegral R B.gen)

include hB

/-- If `B : power_basis S A` is such that `is_integral R B.gen`, then
`is_integral R (B.basis.repr (B.gen ^ n) i)` for all `i` if
`minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)`. This is the case if `R` is a GCD domain
and `S` is its fraction ring. -/
theorem repr_gen_pow_isIntegral [IsDomain S]
    (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
    ∀ i, IsIntegral R (B.Basis.repr (B.gen ^ n) i) :=
  by
  intro i
  let Q := X ^ n %ₘ minpoly R B.gen
  have : B.gen ^ n = aeval B.gen Q :=
    by
    rw [← @aeval_X_pow R _ _ _ _ B.gen, ← mod_by_monic_add_div (X ^ n) (minpoly.monic hB)]
    simp
  by_cases hQ : Q = 0
  · simp [this, hQ, isIntegral_zero]
  have hlt : Q.nat_degree < B.dim :=
    by
    rw [← B.nat_degree_minpoly, hmin, (minpoly.monic hB).natDegree_map,
      nat_degree_lt_nat_degree_iff hQ]
    letI : Nontrivial R := nontrivial.of_polynomial_ne hQ
    exact degree_mod_by_monic_lt _ (minpoly.monic hB)
    infer_instance
  rw [this, aeval_eq_sum_range' hlt]
  simp only [LinearEquiv.map_sum, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finset.sum_apply']
  refine' IsIntegral.sum _ fun j hj => _
  replace hj := Finset.mem_range.1 hj
  rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ←
    Algebra.smul_def, LinearEquiv.map_smul]
  simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
  by_cases hij : (⟨j, hj⟩ : Fin _) = i
  · simp only [hij, eq_self_iff_true, if_true]
    rw [Algebra.smul_def, mul_one]
    exact isIntegral_algebraMap
  · simp [hij, isIntegral_zero]
#align power_basis.repr_gen_pow_is_integral PowerBasis.repr_gen_pow_isIntegral

variable {B}

/-- Let `B : power_basis S A` be such that `is_integral R B.gen`, and let `x y : A` be elements with
integral coordinates in the base `B.basis`. Then `is_integral R ((B.basis.repr (x * y) i)` for all
`i` if `minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)`. This is the case if `R` is a GCD
domain and `S` is its fraction ring. -/
theorem repr_mul_isIntegral [IsDomain S] {x y : A} (hx : ∀ i, IsIntegral R (B.Basis.repr x i))
    (hy : ∀ i, IsIntegral R (B.Basis.repr y i))
    (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) :
    ∀ i, IsIntegral R (B.Basis.repr (x * y) i) :=
  by
  intro i
  rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, Finset.sum_mul_sum, LinearEquiv.map_sum,
    Finset.sum_apply']
  refine' IsIntegral.sum _ fun I hI => _
  simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, LinearEquiv.map_smulₛₗ,
    RingHom.id_apply, Finsupp.coe_smul, Pi.smul_apply, id.smul_eq_mul]
  refine' isIntegral_mul (hy _) (isIntegral_mul (hx _) _)
  simp only [coe_basis, ← pow_add]
  refine' repr_gen_pow_is_integral hB hmin _ _
#align power_basis.repr_mul_is_integral PowerBasis.repr_mul_isIntegral

/-- Let `B : power_basis S A` be such that `is_integral R B.gen`, and let `x : A` be and element
with integral coordinates in the base `B.basis`. Then `is_integral R ((B.basis.repr (x ^ n) i)` for
all `i` and all `n` if `minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)`. This is the case
if `R` is a GCD domain and `S` is its fraction ring. -/
theorem repr_pow_isIntegral [IsDomain S] {x : A} (hx : ∀ i, IsIntegral R (B.Basis.repr x i))
    (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
    ∀ i, IsIntegral R (B.Basis.repr (x ^ n) i) :=
  by
  nontriviality A using Subsingleton.elim (x ^ n) 0, isIntegral_zero
  revert hx
  refine' Nat.case_strong_induction_on n _ fun n hn => _
  · intro hx i
    rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow,
      B.basis.repr_self_apply]
    split_ifs
    · exact isIntegral_one
    · exact isIntegral_zero
  · intro hx
    rw [pow_succ]
    exact repr_mul_is_integral hB hx (fun _ => hn _ le_rfl (fun _ => hx _) _) hmin
#align power_basis.repr_pow_is_integral PowerBasis.repr_pow_isIntegral

/-- Let `B B' : power_basis K S` be such that `is_integral R B.gen`, and let `P : R[X]` be such that
`aeval B.gen P = B'.gen`. Then `is_integral R (B.basis.to_matrix B'.basis i j)` for all `i` and `j`
if `minpoly K B.gen = (minpoly R B.gen).map (algebra_map R L)`. This is the case
if `R` is a GCD domain and `K` is its fraction ring. -/
theorem toMatrix_isIntegral {B B' : PowerBasis K S} {P : R[X]} (h : aeval B.gen P = B'.gen)
    (hB : IsIntegral R B.gen) (hmin : minpoly K B.gen = (minpoly R B.gen).map (algebraMap R K)) :
    ∀ i j, IsIntegral R (B.Basis.toMatrix B'.Basis i j) :=
  by
  intro i j
  rw [B.basis.to_matrix_apply, B'.coe_basis]
  refine' repr_pow_is_integral hB (fun i => _) hmin _ _
  rw [← h, aeval_eq_sum_range, LinearEquiv.map_sum, Finset.sum_apply']
  refine' IsIntegral.sum _ fun n hn => _
  rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def,
    LinearEquiv.map_smul, algebraMap_smul]
  exact isIntegral_smul _ (repr_gen_pow_is_integral hB hmin _ _)
#align power_basis.to_matrix_is_integral PowerBasis.toMatrix_isIntegral

end PowerBasis

end IsIntegral


text:
import testbed.graph_theory
import get_theorems

import tactic
open simple_graph tactic

--------------------  TACTIC: ADD A THEOREM TO CURRENT HYPOTHESIS --------------------

meta def add_theorem_to_hypothesis (n : name) : tactic unit := do {
  d ← get_thm_decl n,
  let statement := d.type, -- get theorem statement
  let proof := d.value, -- get theorem proof

  note n statement proof,-- add to hypothesis

  skip
}

example : true :=
begin
  add_theorem_to_hypothesis `degree_sum,
  trivial
end

--------------------  TACTIC: CHECK IF THEOREM IS IN CURRENT HYPOTHESIS --------------------

--checks if the theorem by name n is already in the hypothesis (potentially under a different name)
meta def in_hypothesis (n : name) : tactic bool := do {
  hyps ← local_context,
  (hyps.mfirst $ λ h, do {
    h_name ← get_local h.local_pp_name,
    h_type ←   infer_type h_name,
    n_type ←  get_thm_statement n,
    if (h_type = n_type) then skip else failed,
    return tt
  }) <|> return ff
}

example : true :=
begin
  in_hypothesis ``degree_sum >>= trace, -- ff
  add_theorem_to_hypothesis `degree_sum,
  in_hypothesis `degree_sum >>= trace, -- tt
  in_hypothesis `degree_sum_even >>= trace, -- ff
  trivial
end

--------------------  TACTIC: GIVEN A LIST OF THEOREM NAMES, RETURN THE FIRST ONE THAT'S NOT IN THE HYPOTHESIS

meta def get_thm_not_in_hypothesis (l : list name) : tactic name := do {
  -- return the first theorem in the list that's not already in the problem state
  (l.mfirst $ λ n, do {
    in_hyp ← in_hypothesis n,
    guard ¬in_hyp,
    return n
  })
  -- otherwise, all of them were already included
  <|>  fail "All theorems in list are already in the hypothesis."
}

example : 1=1 :=
begin
  get_thm_not_in_hypothesis [`degree_sum, `degree_sum_even] >>= trace,
  add_theorem_to_hypothesis `degree_sum,
  add_theorem_to_hypothesis `degree_sum_even,
  get_thm_not_in_hypothesis [`degree_sum, `degree_sum_even], -- should fail, because all theorems are in hypothesis
end

author: Human-Oriented-ATP

repo: lean-tactics


text:
example (P Q : Prop) : Q → (P ∨ Q) :=
begin
intro q, right, exact q,
end

author: nicholaspun

repo: natural-number-game-solutions


text:
import tactic.simp_command
import analysis.special_functions.trigonometric.deriv

/- Turn off trace messages only if the statements are simplified to true: -/
set_option trace.silence_simp_if_true true

/-!
Tests for the #simp command.
-/

#simp 5 - 5 = 0

section arith

def f (x : ℤ) := x + (x - x)
#simp [f] f 3 = 3

mk_simp_attribute test ""
attribute [test] f
-- You can use the optional `:` to separate
-- the simp lemmas and attributes from the expression to simplify.
#simp with test : (f 3) = 3

attribute [simp] f
#simp f 3 = 3
#simp only [f, eq_self_iff_true] f 3 = 3 + (3 - 3)

local attribute [simp] sub_self

variables (x : ℤ)

#simp with test : (f x) = x
#simp f x = x
#simp only [f, eq_self_iff_true] f x = x + (x - x)
#simp only [f, sub_self, eq_self_iff_true] f x = x + 0

end arith

section real

open real
#simp [exp_ne_zero] : (λ x, deriv (λ x, (sin x) / (exp x)) x) =
  (λ (x : ℝ), (cos x * exp x - sin x * exp x) / exp x ^ 2)

variables (x : ℝ)

-- You can refer to local variables, rather than having to use lambdas.
open real
#simp [exp_ne_zero] : deriv (λ x, (sin x) / (exp x)) x = (cos x * exp x - sin x * exp x) / exp x ^ 2

end real

section func_hyp

variables (f : ℕ → ℕ) (hf : f 3 = 0) (hg : 9 = 55)

#simp only [hg, eq_self_iff_true] : 9 = 55
#simp only [hf, add_zero, eq_self_iff_true] : 1 + f 3 = 1

end func_hyp

namespace inst

class magic_data (n : ℕ) :=
(dummy : ℕ)

axiom spell (t : ℤ) (k : ℕ) [magic_data k] : (k = 3) ↔ (k = 77)

variables (t : ℤ) (k : ℕ) [magic_data k] [ii : magic_data k] (h : k = 77 ↔ k = 8)

-- We want to be able to emulate this:
example : (t = t) ∧ (h = h) ∧ ((k = 3) ↔ (k = 8)) :=
begin
  simp [spell t, h]
end

-- Check that we can:

#simp [spell t, h, ii] : (k = 3) ↔ (k = 8)
#simp [spell t, h] : (k = 3) ↔ (k = 8)

theorem spell' (k : ℕ) [magic_data k] : (k = 3) ↔ (k = 77) := spell 1 k

attribute [simp] spell'

#simp [h, ii] : (k = 3) ↔ (k = 8)
#simp [h] : (k = 3) ↔ (k = 8)

-- Check that the `#simp` resolver can handle depth > 2 recursive inclusions

class doubly_magic_data (n : ℕ) [magic_data n] :=
(dummy : ℕ)

variables (n : ℕ) [magic_data n] [doubly_magic_data n] (h₂ : n = 77 ↔ n = 8)

@[simp] axiom spell2 (n : ℕ) [magic_data n] [doubly_magic_data n] : (n = 4) ↔ (n = 77)

example : (h₂ = h₂) ∧ ((n = 4) ↔ (n = 8)) :=
begin
  simp [h₂],
end

#simp [h₂, ii] : (n = 4) ↔ (n = 8)
#simp [h₂] : (n = 4) ↔ (n = 8)

end inst

repo: mathlib