module
@[expose] public section -- TODO: remove after we fix congr_eq
/-
`grind` is inspired by automated reasoning techniques developed in the world of Satisfiability Modulo Theories (SMT).

However, it is not an SMT solver and is not designed to solve massive combinatorial problems.
For example, it would crash if we tried to feed it some of the bit-blasted formulas produced by
`bv_decide`.

At the core of grind, we use a custom congruence closure algorithm for dependent type theory.
We accumulate terms that are known to be equal. You should think of it as a blackboard where
we keep all the facts we know about the current goal.
Remark: Terms known to be true (false) belong to the equivalence class of the term `True` (`False`).
-/

example (a b c : α) (f : α → α) : f a = c → a = b → c = f b := by
  grind

/-
`grind` normalizes terms before adding them to the `grind` state.
Goals:
- We want to minimize the number of different things we need to handle.
- We want to canonicalize instances, implicit terms, etc.
- We want to hash cons terms, i.e., structural equality == pointer equality (performance).
- ...
-/

set_option trace.grind.assert true in -- Trace asserted facts
example : a = 1 + 2 → b = 3 → a = b := by
  grind

/-
`grind` applies many "constraint" propagation rules. They are used
to apply many builtin principles such as
- Injectivity of constructors.
- Beta reduction
- Extensionality theorems.
- Logical connectives.
- ...
-/

set_option trace.grind.eqc true in -- Trace equivalence classes being merged
example (f : Nat → List Nat) : f a = [1, 2] → f b = [] → a ≠ b := by
  grind

/-
`grind` does not case-split like a SMT solver. It uses the structure of the formula,
and splits on `if-then-else`-expressions, `match`-expressions, inductive predicates
marked with `[grind cases]`, etc.
-/
set_option trace.grind.split true in -- Trace case-splits performed by `grind`
example : (match x with
           | 0 => 1
           | _ + 1 => 2) > 0 := by
  grind

example : (match x with
           | 0 => 1
           | _ + 1 => 2) > 0 := by
  fail_if_success grind (splits := 0) -- `grind` fails if we don't allow it case-split.
  sorry

/-
`grind` shows you the case-splits performed when it fails.
-/
example : (match x with
           | 0 => 1
           | _ + 1 => 2) > 1 := by
  fail_if_success grind
  sorry

/-
`simp` uses theorems as rewriting rules.
`grind` instantiates the theorems using E-matching.
Each theorem is annotated with patterns.
Whenever, it finds an instance of the pattern modulo
the equalities in its state, it instantites the theorem.
There is no rewriting happening. It is just accumulating facts.
-/

opaque f : Nat → Nat
opaque g : Nat → Nat
-- `[grind =]` instructs `grind` to use the left-hand side of the conclusion as the pattern.
@[grind =] theorem fg : f (g x) = x := sorry

set_option trace.grind.assert true in
set_option trace.grind.ematch.instance true in
example : f a = b → a = g c → b = c := by
  grind

/-
We have the following variants:
- `[grind =_]`: use right-hand side of the conclusion.
- `[grind _=_]`: use both right and left-hand side of the conclusion.
- `[grind →]`: use terms in the antecedents as patterns. "Forward reasoning"
- `[grind ←]`: use terms in the conclusion as patterns. "Backward reasoning"
- `[grind =>]`: look for patterns from left to right.
- `[grind <=]`: look for patterns from right to left.
-/

opaque R : Nat → Nat → Prop
@[grind →] theorem Rtrans : R x y → R y z → R x z := sorry
@[grind →] theorem Rsymm : R x y → R y x := sorry

set_option trace.grind.assert true in
example : R a b → R c b → R d c → R a d := by
  grind

/-
The attributes above are for convenience.
If an user wants total control over the selected pattern
they may use the command `grind_pattern`.
-/

opaque bla : Nat → Nat
theorem blaThm : bla (bla x) = bla x := sorry

grind_pattern blaThm => bla (bla x)

set_option trace.grind.assert true in
example : bla a = b → bla b = b := by
  grind


/-
We also have
- `[grind ←=]`: equality driven backward reasoning.
-/

opaque U : Type
axiom mul : U → U → U
axiom one : U
axiom inv : U → U

/--
In the following example, `grind` instantiates the theorem
whenever it learns a disequality `t = s` where `t` or `s` E-matches `inv a`
-/
@[grind ←=] theorem inv_of_mul : mul a b = one → inv a = b :=
  sorry

/-
Like `simp`, we also have `grind only`
-/
example : R a b → R c b → R d c → R a d := by
  fail_if_success grind only -- `Rtrans` and `Rsymm` were not applied
  sorry

example : R a b → R c b → R d c → R a d := by
  grind only [→ Rtrans, → Rsymm]

example : R a b → R c b → R d c → R a d := by
  grind only [Rtrans, ← Rsymm]

/-
We also have `grind?`.

We currently do not try to minimize the number of generated arguments, but
we will do it in the future.
It behaves like `simp?`. If something was used, it will appear in the result.
-/

example : R a b → R c b → R d c → R a d := by
  grind?


/-
We can instruct `grind` to case-split on inductive predicates and types,
and use the constructors of an inductive predicate as E-matching theorems.
-/

abbrev Variable := String
def State := Variable → Nat
inductive Stmt : Type where
  | skip : Stmt
  | assign : Variable → (State → Nat) → Stmt
  | seq : Stmt → Stmt → Stmt
  | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt
  | whileDo : (State → Prop) → Stmt → Stmt
infix:60 ";; " => Stmt.seq
export Stmt (skip assign seq ifThenElse whileDo)
set_option quotPrecheck false in
notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v)
inductive BigStep : Stmt → State → State → Prop where
  | skip (s : State) : BigStep skip s s
  | assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s])
  | seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) :
    BigStep (S;; T) s u
  | if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) :
    BigStep (ifThenElse B S T) s t
  | if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) :
    BigStep (ifThenElse B S T) s t
  | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) :
    BigStep (whileDo B S) s u
  | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s
notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t

example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
  grind [cases BigStep]

theorem cases_if_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
  grind [cases BigStep]

theorem cases_if_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t → (T, s) ==> t := by
  grind [cases BigStep]

theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
  grind [cases BigStep, intro BigStep]

example {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
  grind [BigStep] -- shortcut for `cases BigStep` and `intro BigStep`

/-
`grind` already has support for offset equalities and inequalities:
- `x + k ≤ y`, `x ≤ y + k`, `x + k = y`, ... where `k` is a numeral.
- Efficient algorithm.
- Very compact proofs.
- Exhaustive propagation, but it does not case-split on disequalities.

Very effective for examples using the notation `a[i]`
-/

-- Standard library will be
attribute [grind =] Array.size_set Array.getElem_set_self Array.getElem_set_ne

example (as bs cs ds : Array α) (v₁ v₂ v₃ : α)
        (i₁ i₂ i₃ j : Nat)
        (h₁ : i₁ < as.size)
        (h₂ : as.set i₁ v₁ = bs)
        (h₃ : i₂ < bs.size)
        (h₃ : bs.set i₂ v₂ = cs)
        (h₄ : i₃ < cs.size)
        (h₅ : ds = cs.set i₃ v₃)
        (h₆ : j ≠ i₁ ∧ j ≠ i₂ ∧ i₃ ≠ j)
        (h₇ : j < ds.size)
        (h₈ : j < as.size)
        : ds[j] = as[j] := by
  set_option diagnostics true in
  grind

/-
`grind` has support for splitting on `match`-expressions with overlapping patterns.
It is quite complex in the dependent case, and many `cast`-operations have to be performed.
-/
namespace Ex
def f : List Nat → List Nat → Nat
  | _, 1 :: _ :: _ => 1
  | _, a :: _ => if a > 1 then 2 else 3
  | _, _  => 0

example : z = a :: as → y = z → f x y > 0 := by
  grind [f.eq_def]
end Ex

/- It gets quite messy with dependent pattern matching. -/
inductive Vec (α : Type u) : Nat → Type u
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n+1)

def h (v w : Vec α n) : Nat :=
  match v, w with
  | _, .cons _ (.cons _ _) => 20
  | .nil, _  => 30
  | _, _    => 40

example : b = .cons 1 .nil → h a b = 40 := by
  grind [h.eq_def]

/-
`try?` tactic is a driver around `grind` (and other tactics).
It tries many different things (e.g., applies function induction principle for you)
-/
def app : List α → List α → List α
  | [], bs => bs
  | a::as, bs => a :: app as bs

theorem app_assoc : app as (app bs cs) = app (app as bs) cs := by
  try?

/-
`grind` has a notion of term "generation". It is useful for avoiding
unbounded instantiation.
-/
opaque bomb : Nat → Nat
@[grind =] theorem bombEx : bomb x = bomb (bomb x) + 1 := sorry

example : bomb x > 10 := by
  fail_if_success grind
  sorry

/-
Roadmap:
- Improve `try?`
- Improve diagnostics. There are so many possible improvements.
- Improve heuristics (e.g., "weights", `grind` specific `[grind ext]`).
- Bug fixes.
- Linear integer arithmetic.
- More examples like `constProp.lean`.
- Commutative rings support (Q2).
- Annotate standard library (Q2).
- `grind?` argument minimization (Q2).
- Fixing `induction a <;> grind?` (Q2).
- `bv_decide` integration (Q2).
- E-matching modulo associativity and commutativity?
-/