Toy demo for delab path to textual porting

ToyDelab.lean

import Lean
import Std.Data.HashSet

open Lean Lean.PrettyPrinter.Delaborator
open Std (HashSet)

namespace CollectTerms

structure State where
  visitedExpr : HashSet Expr  := {}
  terms       : HashSet Expr  := {}
  deriving Inhabited

abbrev CollectM := StateRefT State MetaM

def collect (e : Expr) : CollectM Unit := do
  if (← get).visitedExpr.contains e then return ()
  match e with
  | Expr.const n _ _     => modify fun s => { s with terms := s.terms.insert e }
  | Expr.proj _ _ e _    => collect e
  | Expr.forallE _ d b _ => collect d *> collect b
  | Expr.lam _ d b _     => collect d *> collect b
  | Expr.app f a _       => collect f *> collect a
  | Expr.mdata _ b _     => collect b
  | Expr.letE _ t v b _  => collect t *> collect v *> collect b
  | Expr.fvar fvarId _   => modify fun s => { s with terms := s.terms.insert e }
  | _                    => pure ()
  modify fun s => { s with visitedExpr := s.visitedExpr.insert e }

def collectTerms (e : Expr) : MetaM (HashSet Expr) := do
  let ⟨_, s⟩ ← (collect e).run {}
  s.terms

end CollectTerms

export CollectTerms (collectTerms)

namespace Delab.Simp

def blacklist : HashSet Name :=
  ({} : HashSet Name)
    |>.insert `ofEqTrue
    |>.insert `congrArg
    |>.insert `congrFun
    |>.insert `Eq
    |>.insert `Eq.trans
    |>.insert `True
    |>.insert `False
    |>.insert `eqSelf

def collectSimpNames (e : Expr) : MetaM (HashSet Name) := do
  -- TODO: subtract the names that are in the default simp set
  let mut names : HashSet Name := {}
  for term in (← collectTerms e).toArray do
    if !(← Meta.isProp (← Meta.inferType term)) then continue
    match term with
    | Expr.const n .. =>
      if blacklist.contains n then continue
      names := names.insert n
    | _ => names := names.insert (← Meta.getFVarLocalDecl term).userName
  return names

@[delab app.ofEqTrue]
def delabSimp : Delab := do
  -- TODO: this is incredibly incomplete!
  let e ← getExpr
  let names := (← collectSimpNames e).toArray
  let simpLemmas : Array Syntax := names.map mkIdent
  let stx : Syntax ← `(by simp [$[$simpLemmas:term],*])
  pure stx

@[delab app.Eq.mp]
def delabSimpHyp : Delab := do
  -- TODO: this is incredibly incomplete!
  let e ← getExpr
  if !e.isAppOfArity `Eq.mp 4 then failure
  let arg := e.appArg!
  if !arg.isFVar then failure
  let h := mkIdent (← Meta.getFVarLocalDecl arg).userName
  let pf := e.getArg! 2
  let names := (← collectSimpNames pf).toArray
  let simpLemmas : Array Syntax := names.map mkIdent
  let stx : Syntax ← `(by simp only [$[$simpLemmas:term],*] at $h:ident; exact $h:term)
  pure stx

end Delab.Simp

def double : Nat → Nat
  | 0   => 0
  | n+1 => double n + 2

axiom Nat.doubleTimesTwo (n : Nat) : double n = 2 * n
axiom Nat.timesTwoAddSelf (n : Nat) : 2 * n = n + n

theorem foo (n : Nat) : double n = n + n := by
  simp [Nat.doubleTimesTwo, Nat.timesTwoAddSelf]

#print foo
/-
theorem foo : ∀ (n : Nat), double n = n + n :=
fun (n : Nat) =>
  by
    simp [Nat.doubleTimesTwo, Nat.timesTwoAddSelf]
-/
theorem bar (n : Nat) (h₁ : double n = n + n) (h₂ : double n = n + n) : 2 * n = n + n ∧ n + n = n + n := by
  simp only [Nat.doubleTimesTwo] at h₁
  simp only [Nat.doubleTimesTwo, Nat.timesTwoAddSelf] at h₂
  exact ⟨h₁, h₂⟩

#print bar
/-
theorem bar : ∀ (n : Nat), double n = n + n → double n = n + n → 2 * n = n + n ∧ n + n = n + n :=
fun (n : Nat) (h₁ h₂ : double n = n + n) =>
  { left :=
      by
        simp only [Nat.doubleTimesTwo]at h₁;
        exact h₁,
    right :=
      by
        simp only [Nat.doubleTimesTwo, Nat.timesTwoAddSelf]at h₂;
        exact h₂ }
-/

theorem baz (n : Nat) (h₁ : double n = n + n) (h₂ : double n = n + n) : n + n = n + n := by
  simp only [h₁] at h₂
  exact h₂

#print baz
/-
theorem baz : ∀ (n : Nat), double n = n + n → double n = n + n → n + n = n + n :=
fun (n : Nat) (h₁ h₂ : double n = n + n) =>
  by
    simp only [h₁]at h₂;
    exact h₂
-/