simproc_tutorial.lean

import Lean

opaque g (n : Nat) : Nat

@[simp] def f (i n m : Nat) :=
  if i < n then
    f (i+1) n (g m)
  else
    m
termination_by n - i

def p (n : Nat) := n ≤ 3

theorem ex₁ : ¬ (p 4 ∧ f 0 10 y = y) := by
  simp [p, f]

#print ex₁

theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]

open Lean Meta Simp
simproc ↓ shortCircuitAnd (And _ _) := fun e => do
  let_expr And p q := e | return .continue
  let r ← simp p
  let_expr False := r.expr | return .continue
  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
  return .done { expr := r.expr, proof? := some proof }

theorem ex₂ : ¬ (p 4 ∧ f 0 10000 y = y) := by
  simp [p, f]

#print ex₂

/-
`MetaM` basics
-/
open Elab Term
run_elab do
  let s ← `(g 0 + 1)  -- Syntax
  let e ← elabTerm s none -- Expr
  let type ← inferType e
  logInfo m!"{e} : {type}"
  let e' ← whnf e  -- Put `e` in weak head normal form
  logInfo m!"{e'} : {type}"
  assert! (← isDefEq e e')

run_meta do
  let one := toExpr 1 -- Convert a value into a `Expr` representing it.
  let type ← inferType one
  logInfo m!"{one} : {type}"
  let str := toExpr "hello"
  let type ← inferType str
  logInfo m!"{str} : {type}"

run_meta do
  let as := toExpr [1, 2, 3]
  let bs := toExpr [3, 4]
  let append ← mkAppM ``List.append #[as, bs]
  logInfo m!"{append} : {← inferType append}"

run_meta do
  let one := toExpr 1
  let some n ← getNatValue? one | throwError "unexpected {one}"
  logInfo m!"n: {n}"


/-!
Helper lemmas for the `finContra` tactic used by the `match`-compiler.
-/

theorem FinContra.step {a b : Nat} (h₁ : ¬ a = b) (h₂ : a < b + 1) : a < b := by
  omega

theorem FinContra.false_of_lt_zero {a : Nat} (h : a < 0) : False :=
  Nat.not_lt_zero a h

open FinContra in
example (i : Fin 3) (h₁ : i ≠ 0) (h₂ : i ≠ 1) (h₃ : i ≠ 2) : False :=
  false_of_lt_zero (a := i.val) <|
  step (Fin.val_ne_of_ne h₁) <|
  step (Fin.val_ne_of_ne h₂) <|
  step (Fin.val_ne_of_ne h₃) <|
  i.isLt

/-- If `type` is `Fin` with a known dimension, returns the number of elements in the type. -/
def isFinType? (type : Expr) : MetaM (Option Nat) := do
  let_expr Fin n := (← whnfD type) | return none
  getNatValue? n

/--
A disquality of of the form `expr ≠ val` if `inv = false` and `val ≠ expr` if `inv = true`
-/
structure NeFinValInfo where
  inv  : Bool
  expr : Expr
  val  : Nat

/--
Return disequality info if `prop` is a disequality of the form `e ≠ i` or `i ≠ e` where
`i` is a `Fin` literal.
-/
def isNeFinVal? (prop : Expr) : MetaM (Option NeFinValInfo) := do
  let some (_, a, b) ← matchNe? prop | return none
  if let some ⟨_, n⟩ ← getFinValue? a then
    return some { inv := true, expr := b, val := n.val }
  else if let some ⟨_, n⟩ ← getFinValue? b then
    return some { inv := false, expr := a, val := n.val }
  else
    return none

/--
Constructs a proof of `False` using the `diseqs` where
`e : Fin n`, and `diseqs` is an array of size `n`,
and `diseqs[i]` contains a proof for `e ≠ i` where `i` a literal value.
-/
def mkProof (e : Expr) (diseqs : Array (Option Expr)) : MetaM Expr := do
  let mut proof ← mkAppM ``Fin.isLt #[e]
  let n := diseqs.size
  for i in [:diseqs.size] do
    let some diseq := diseqs[n - i - 1]! | unreachable!
    let diseq ← mkAppM ``Fin.val_ne_of_ne #[diseq]
    proof ← mkAppM ``FinContra.step #[diseq, proof]
  mkAppM ``FinContra.false_of_lt_zero #[proof]

/--
Try to construct a proof for `False` using disequalities on `e`
where `e : Fin n` and `numElems = n`.
The method tries to find disequalities `e ≠ i` in the local context.
-/
def cover? (e : Expr) (numElems : Nat) : MetaM (Option Expr) := do
  let mut found := 0
  let mut diseqs : Array (Option Expr) := Array.mkArray numElems none
  for localDecl in (← getLCtx) do
    if let some info ← isNeFinVal? localDecl.type then
      if e == info.expr then
      if h : info.val < diseqs.size then
      if diseqs[info.val].isNone then
        found := found + 1
        let proof ← if info.inv then
          mkAppM ``Ne.symm #[localDecl.toExpr]
        else
          pure localDecl.toExpr
        diseqs := diseqs.set! info.val (some proof)
  if found == numElems then
    return some (← mkProof e diseqs)
  else
    return none

/--
Return `true` if the given goal is contradicatory because
it contains a `Fin` term and disequalities that cover all possibilities.
Example:
```
example (a : Fin 3) (h₁ : a ≠ 0) (h₂ : a ≠ 1) (h₃ : a ≠ 2) : ...
```
-/
def finContra (mvarId : MVarId) : MetaM Bool := mvarId.withContext do
  mvarId.checkNotAssigned `fin_contra
  let mut visited : ExprSet := {}
  for localDecl in (← getLCtx) do
    if let some info ← isNeFinVal? localDecl.type then
      unless visited.contains info.expr do
        visited := visited.insert info.expr
        if let some size ← isFinType? (← inferType info.expr) then
          if let some proofOfFalse ← cover? info.expr size then
            let proof ← mkFalseElim (← mvarId.getType) proofOfFalse
            mvarId.assign proof
            return true
  return false

open Tactic

elab "fin_contra" : tactic => do
  liftMetaTactic fun mvarId => do
    if (← finContra mvarId) then
      return []
    else
      throwError "fin_contra failed to close the goal"

example (i : Fin 3) (h₁ : i ≠ 0) (h₂ : i ≠ 1) (h₃ : i ≠ 2) : False := by
  fin_contra

example (i : Fin 3) (h₂ : i ≠ 1) (h₃ : i ≠ 2) (a : Nat) (_ : a ≠ 0) (h₁ : 0 ≠ i) : False := by
  fin_contra