failed tactic super

Stream: new members

[Victor Porton]

Why does the tactic super fail in the following code?

import super
import tactic

section

def option_to_subfunc {α β: Type} (f: α → option β) :
  {x:α // option.is_some (f x)} → β | ⟨x, h⟩ := option.get h

open_locale classical

noncomputable def subfunc_to_option {α β: Type} {c: set α} --[decidable_pred c]
(f: {x:α // x ∈ c} → β) : α → option β :=
λ y:α, if h: y ∈ c then option.some (f ⟨y, h⟩) else none

theorem inv2 {α β: Type} (f: β → option α): subfunc_to_option (option_to_subfunc f) = f := by super

end

[Victor Porton]

The idea is to go from a function to option monad to a function on a subset and back.

[Kevin Buzzard]

Does super know about functional extensionality? I have no idea

[Patrick Johnson]

theorem inv2 {α β : Type} (f : β → option α) : subfunc_to_option (option_to_subfunc f) = f :=
begin
  funext x, -- Two functions are equal if their results are equal for all arguments
  simp [subfunc_to_option], -- Unfold the definition of `subfunc_to_option` and simplify
  split_ifs, -- Split into two cases
  { simp [option_to_subfunc, h] }, -- For the `some` case, simplifier can handle that
  { change ¬(f x).is_some at h, -- Unfold the definition of set membership
    rw [option.is_some_iff_exists, not_exists] at h, -- Simplify and push negation
    by_contra h₁, -- Proof by contradiction
    cases f x; try { specialize h val }; contradiction }, -- Split `f x` into cases
end

[Victor Porton]

Conclusion: super is not all-powerful and proofs still need to be done manually picking tactics.

[Patrick Johnson]

Proving a theorem is NP-hard. There is no "all-powerful" tactic and there will never be. Isabelle theorem prover, for instance, has more automation, but it's far from proving any theorem using a single tactic.

[Mario Carneiro]

proving a theorem is undecidable

[Julian Berman]

The zulip tactic is pretty good though

[Kyle Miller]

I think one of the complexities here is that there was a subtle misuse of the set API. The subfunc_to_option function was being applied to something that used a predicate directly rather than something that was strictly a set.

import tactic

section

def option_to_subfunc {α β: Type} (f: α → option β) :
  {x:α // option.is_some (f x)} → β | ⟨x, h⟩ := option.get h
--                ^--- this is not a `set`, instead it's defining a predicate

open_locale classical

noncomputable def subfunc_to_option {α β: Type} {c: α → Prop} -- switched to predicate rather than `set`
(f: {x:α // c x} → β) : α → option β :=
λ y:α, if h: c y then option.some (f ⟨y, h⟩) else none

theorem inv2 {α β: Type} (f: β → option α): subfunc_to_option (option_to_subfunc f) = f :=
begin
  ext x,
  cases h : f x;  simp [subfunc_to_option, option_to_subfunc, h],
end

end

[Victor Porton]

Patrick Johnson said:

Proving a theorem is NP-hard. There is no "all-powerful" tactic and there will never be. Isabelle theorem prover, for instance, has more automation, but it's far from proving any theorem using a single tactic.

I know. But for a human inv2 theorem is obvious.

[Kevin Buzzard]

When theorem provers are as good at humans at closing obvious goals quickly it will be a great relief. Until then I learn the tactics.

[Adam Topaz]

If you want to write a new tactic that solves all trivial goals, I'm sure that would be a very welcomed addition to mathlib.