Skip to main content

General-Purpose Tactics

untilNthEmptyLine​

generalTactics.lean
def NEWLINE : char := char.of_nat 10

def untilNthEmptyLine_core : option nat → list string → string
| _ [] := ""
| (some num) (""::rest) := if num=0 then "" else 
     "\n" ++ untilNthEmptyLine_core (some(num-1)) rest
| none (line::rest) :=
    line ++ "\n" ++ untilNthEmptyLine_core none rest
| (some num) (line::rest) :=  if num=0 then "" else 
    line ++ "\n" ++ untilNthEmptyLine_core (some num) rest 

def untilNthEmptyLine (onum : option nat) (s : string) : string :=
  untilNthEmptyLine_core onum $ list.drop 1 $ s.split_on NEWLINE

Trace Goal​

generalTactics.lean
meta def trace_goal_core (o : option nat) (iden : string) : tactic unit :=
  trace ("\n-- " ++ iden ++ " --") >>
  tactic.read >>= trace ∘ (untilNthEmptyLine o) ∘ format.to_string ∘ to_fmt
generalTactics.lean
meta def trace_goal : string → tactic unit :=
  trace_goal_core (some 1) 
meta def trace_goals (num : nat) : string → tactic unit :=
  trace_goal_core (some num) 
meta def trace_all_goals : string → tactic unit :=
  trace_goal_core none

Count Goals​

generalTactics.lean
meta def count_goals : tactic nat :=
  tactic.get_goals >>= (return ∘ list.length)

Repeat-Assume Tactics​

Name generation​

generalTactics.lean
def varFormat (baseName : name) (i : nat) : name :=
  name.append_suffix baseName (nat.has_repr.repr i)
def gen_nameList (baseName : name) (n : nat) : list name := 
  list.map (varFormat baseName) (list.range n)

repeat-assume​

generalTactics.lean
meta def repeat_assume : list name → tactic unit :=
  list.foldr (λ nm rest, intro nm >> rest) skip

repeat-assume-pair (helper tactic)​

generalTactics.lean
meta def repeat_assume_pair : list name → tactic (list (name × expr))
| [] := return []
| (nm::nms) :=
  (do
    temp_nm ← mk_fresh_name,
    e ← intro temp_nm,
    rest ← repeat_assume_pair nms,
    return $ (nm,e)::rest)

repeat-assume-then-induct​

generalTactics.lean
meta def repeat_assume_then_induct (T : tactic unit) (N : list name) : tactic unit :=
  do
    assumptionList ← repeat_assume_pair N,
    T,
    let cmb := λ nm e (res : tactic unit), (induction e [nm]) >> res,
    list.foldr (function.uncurry cmb) skip assumptionList
generalTactics.lean
meta def repeat_assume_induct : list name →  tactic unit :=
  repeat_assume_then_induct skip

repeat-assume-replace​

generalTactics.lean
meta def repeat_assume_replace (F : parse ident) (N : list name) : tactic unit :=
do
  f ← resolve_name F,
  assumptionList ← repeat_assume_pair N,
  let cmb := λ (nm : name) (e : expr) (res:tactic unit),
    (do
      «have» nm none ``(%%f %%e),
      clear e,
      res),
  list.foldr (function.uncurry cmb) skip assumptionList