mathlib

mathlib copied to clipboard

The idea would be to have an attribute to force a theorem to avoid classical logic, which would detect regressions caused by classical simp lemmas unexpectedly firing. From Zulip:

meta def environment.is_builtin (env : environment) (n : name) : bool :=
env.is_inductive n || env.is_recursor n || env.is_constructor n ||
to_bool (n ∈ [``quot, ``quot.lift, ``quot.ind, ``quot.mk])

meta def tactic.get_axioms_used_aux (env : environment) : name →
  list name × name_set → tactic (list name × name_set)
| n p@(l, ns) := if ns.contains n then pure p else do
  d ← env.get n,
  let ns := ns.insert n,
  let process (v : expr) : tactic (list name × name_set) := (do
    v.mfold (l, ns) $ λ e _ p,
      if e.is_constant then tactic.get_axioms_used_aux e.const_name p else pure p),
  match d with
  | (declaration.defn _ _ _ v _ _) := process v
  | (declaration.thm _ _ _ v)      := process v.get
  | _ := pure $ if env.is_builtin n then (l, ns) else (n::l, ns)
  end

meta def tactic.get_axioms_used (n : name) : tactic (list name) :=
do env ← tactic.get_env,
  prod.fst <$> tactic.get_axioms_used_aux env n ([], mk_name_set)

#eval tactic.get_axioms_used `classical.em >>= tactic.trace
-- [propext, quot.sound, classical.choice]

@[user_attribute]
meta def intuit_attr : user_attribute unit unit :=
{ name   := `intuit,
  descr  := "intuit",
  after_set := some $ λ n _ _, do
    l ← tactic.get_axioms_used n,
    guard (``classical.choice ∉ l) <|>
    tactic.fail "ERROR: classical axioms used" }

@[intuit] theorem bad (p) : ¬ (p ↔ ¬ p) := -- fail
by by_cases p; simp

@[intuit] theorem good (p) : ¬ (p ↔ ¬ p) := -- ok
λ h, have ¬ p, from λ i, h.1 i i, this (h.2 this)

I think this would be good to have available in some form, even though most of mathlib doesn't care at all about using choice.