Zulip Chat Archive

Stream: new members

Topic: failed tactic super


Victor Porton (Apr 02 2022 at 02:43):

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 (Apr 02 2022 at 02:44):

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

Kevin Buzzard (Apr 02 2022 at 07:05):

Does super know about functional extensionality? I have no idea

Patrick Johnson (Apr 02 2022 at 09:52):

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 (Apr 02 2022 at 10:52):

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

Patrick Johnson (Apr 02 2022 at 12:00):

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 (Apr 02 2022 at 12:27):

proving a theorem is undecidable

Julian Berman (Apr 02 2022 at 16:08):

The zulip tactic is pretty good though

Kyle Miller (Apr 02 2022 at 18:53):

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 (Apr 02 2022 at 21:05):

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 (Apr 02 2022 at 23:28):

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 (Apr 02 2022 at 23:40):

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.


Last updated: Dec 20 2023 at 11:08 UTC