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