Complete destruction tactic

Stream: Is there code for X?

[Yaël Dillies]

Is there a tactic that completely destructs a structure? I want something like obtain/rcases, but where it recursively destructs every field that's a structure.

My use case is for bundled homs instances, because new structure inheritance means that in general you can't just do cases on a bundled whatever-hom and get the underlying map. Instead, I'm resorting to writing brittle code like
coe_injective' := λ f g h, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' }
which will break as soon as the hom hierarchy changes.

[Yaël Dillies]

Any opinion, @Anne Baanen?

[Patrick Massot]

Do you know about rintros? and rcases??

[Patrick Massot]

You can at least take inspiration from the code doing that.

[Yaël Dillies]

Yup, but once again they require me to write different things every time the precise inheritance order changes, something which will happen a lot when we build the hierarchy and also when we port to Lean 4 (because we'll give up on old inheritance for good).

[Yaël Dillies]

I wish docs#tactic.destruct was I wanted.

[Reid Barton]

Your use case sounds like the territory of ext

[Yaël Dillies]

I think ext is unfortunately both too powerful and too demanding: I explicitly don't want the ext lemmas (they come from the instances I'm trying to prove) and if I had them it would apply ext onto the functions, which I don't want either.

[Yaël Dillies]

In contrast, ext1 is not powerful enough, as reaching the correct level of destruction will require several applications of it, and a variable number of them, which is what I'm trying to avoid.

[Reid Barton]

Maybe it would help to give an actual example of what you want to do?

[Bhavik Mehta]

Yaël Dillies said:

I think ext is unfortunately both too powerful and too demanding: I explicitly don't want the ext lemmas (they come from the instances I'm trying to prove) and if I had them it would apply ext onto the functions, which I don't want either.

Does ext : 3 (or some other number) work?

[Yaël Dillies]

Even if it does, that's not what I want, because I don't want to have to tweak the number.

[Reid Barton]

This kind of issue also seems implicit in what you're asking for though--how much destruction is "complete"?

[Yaël Dillies]

when no field is a structure anymore

[Yaël Dillies]

Actually, we could weaken that to "no Type-valued structure"

[Reid Barton]

But I guess I don't really buy that next week, you'll have the same problem but instead of having a function inside you have another structure, which you don't want to destruct this time, etc

[Yaël Dillies]

I totally get that, but it doesn't happen in my case. What I'm asking for is probably quite specific.

[Reid Barton]

OK well assuming you're trying to prove coe_injective' for e.g. ring_hom--is there a reason ring_hom doesn't have @[ext]?

[Reid Barton]

If it did then ext1 should be the correct amount of cases, right? And we could just not prove the extensionality lemma manually later.

[Yaël Dillies]

The reason is that extensionality for ring_hom comes from docs#fun_like.ext through docs#ring_hom.ring_hom_class

[Reid Barton]

It doesn't come from docs#ring_hom.ext?

[Yaël Dillies]

Oh in that case it seems it does :thinking:

[Reid Barton]

I might be too simple-minded here because I don't know anything about this fun_like stuff.

[Kyle Miller]

I learned about tactic#destruct recently, which might be helpful. You can set up a destruction loop to completely break something apart. It likely will break things up too much, though.

example {P Q R : Prop} : ((P ∧ Q) ∧ R) ↔ (P ∧ (Q ∧ R)) :=
begin
  split;
  repeat { intro h, try { destruct h }, };
  repeat { split };
  assumption,
end

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/generated.20names/near/268491636

[Anne Baanen]

Reid Barton said:

OK well assuming you're trying to prove coe_injective' for e.g. ring_hom--is there a reason ring_hom doesn't have @[ext]?

Do you mean something like @[ext] structure ring_hom extends monoid_hom, add_monoid_hom? That attribute generates the wrong ext lemma since it involves the fields, f.to_fun = g.to_fun instead of the coercions ⇑ f = ⇑ g.

[Anne Baanen]

Yaël Dillies said:

Oh in that case it seems it does :thinking:

Every morphism still has its own ext lemma. I copied this from set_like, as I understand the ext tactic doesn't do a typeclass search to look for lemmas, so it can't find docs#fun_like.ext.

[Yaël Dillies]

Ah I was missing that part!

[Anne Baanen]

I think we can get quite far by adapting the code implementing attribute#ext, let me see if I can quickly assemble something...

[Anne Baanen]

Still needs a bit of cleanup:

import algebra.ring.basic

@[ext]
structure ring_hom' (α : Type*) (β : Type*) [non_assoc_semiring α] [non_assoc_semiring β] :=
(to_hom : monoid_hom α β)
(map_add' : ∀ {x y : α}, to_hom (x + y) = to_hom x + to_hom y)

open tactic

/-- Does `struct_name` refer to a `Type`-valued structure?

That is, is `struct_name` an inductive type with one constructor,
living in some universe `Type*` instead of `Prop`?
-/
meta def is_Type_valued_struct (struct_name : name) : tactic bool :=
do
   env ← get_env,
   match env.structure_fields struct_name with  -- TODO: is this the best way to check that it is a struct?
   | none := pure ff
   | (some _) := do
     struct_decl ← get_decl struct_name,
     struct_name_full ← resolve_constant struct_name,
     let a := @expr.const tt struct_name_full $ struct_decl.univ_params.map level.param,
     t ← infer_type a,
     s ← infer_type t,
     pure $ s ≠ `(Prop)
   end

/-- `struct_bash_step h`: splits the `Type`-valued structure `h` into all its fields;
it does nothing if `h` is `Prop`-valued or not a structure.

Returns the newly created fields.

Useful for extensionality-like proofs.
-/
meta def struct_bash_step (h : expr) : tactic (list expr) :=
do struct_type ← infer_type h >>= head_beta,
   if !(struct_type.is_app && struct_type.get_app_fn.is_constant) then pure []
   else do
     let struct_name := struct_type.get_app_fn.const_name,
     is_struct ← is_Type_valued_struct struct_name,
     if is_struct then do
       new_exprs ← cases h,
       pure (new_exprs >>= (λ x, x.2))
     else pure []

/-- `struct_bash structs`: recursively splits each `Type`-valued structure in `structs` into all its fields;
it does nothing if a structure is `Prop`-valued or not a structure.

Useful for extensionality-like proofs.
-/
meta def struct_bash : list expr → tactic unit
| initial_structs :=
do new_structs ← initial_structs.mmap (λ h, list.reverse <$> struct_bash_step h),
   match new_structs with
   | [] := pure ()
   | _ := struct_bash new_structs.join
   end

namespace tactic.interactive


/-- `struct_bash s`: recursively splits the `Type`-valued structure `s` into all its fields;
it does nothing if `s` is `Prop`-valued or not a structure.

Useful for extensionality-like proofs.
-/
meta def struct_bash (h : interactive.parse (lean.parser.many lean.parser.ident)) : tactic unit :=
do initial_structs ← h.mmap get_local,
   _root_.struct_bash initial_structs

end tactic.interactive

instance ring_hom.fun_like' {α β} [non_assoc_semiring α] [non_assoc_semiring β] :
  fun_like (ring_hom' α β) α (λ _, β) :=
{ coe := λ f, f.to_hom.to_fun,
  coe_injective' := λ f g h, by { struct_bash f g, congr' } }

[Anne Baanen]

@Jannis Limperg, I remember you had trouble too with the case tactic renaming your locals in the presence of dependencies, how did you end up fixing that?

[Jannis Limperg]

Sorry what's the issue exactly?

[Anne Baanen]

I have a list of hypotheses (: list expr) to apply tactic.cases on, however if you do cases h1 and h2 depends on h1 then h2 gets reverted and re-introduced, so the expression h2 doesn't refer to anything in the context anymore.

[Jannis Limperg]

Ah yes, that issue. Afaict there are two ways to address this:

• Identify hypotheses by their user names. You can rename before and after to make sure these are unique, though this messes up error messages, so ideally you only rename when necessary. This is what I ended up doing.
• Maintain a mapping between the old and new unique names of these hyps and update them in the relevant expressions. This is what Lean 4 does with its FVSubsts. Not all primitive tactics report such mappings, but cases does afair.

[Anne Baanen]

Aha, so in that first approach you'd do h ← get_local h right before you call cases h, and then map expr.const_name over the new locals : expr that cases h returns.

[Jannis Limperg]

I guess local_pp_name instead of const_name; other than that sounds good. But beware of duplicate pp names.