Zulip Chat Archive

Stream: new members

Topic: definitional equivalence


Jon Eugster (Feb 24 2021 at 15:57):

I'm struggling with things that seem definitionally equivalent to me but either they aren't or I don't know how to replace a term with it's definition...
I have a hypothesis

[h: algebra.finite_type R A]

and if I Ctrl-click on this I get the following two definitions:

@[class]
def algebra.finite_type : Prop := ( : subalgebra R A).fg

def fg (S : subalgebra R A) : Prop :=
 t : finset A, algebra.adjoin R t = S

Inside my begin ... end block I would therefore use h to get a concrete such t, can somebody help me with the syntax for this unravelling definitions?

Bryan Gin-ge Chen (Feb 24 2021 at 16:02):

That sounds right. What do you mean by using h? Are you saying that (something like) rcases h with ⟨t, ht⟩ failed?

Bryan Gin-ge Chen (Feb 24 2021 at 16:03):

Could you provide a #mwe?

Jon Eugster (Feb 24 2021 at 16:05):

Yes that's it, thank you!

Jon Eugster (Feb 24 2021 at 16:23):

@Bryan Gin-ge Chen or maybe it only worked partially. Here is a MWE:

import algebra.field
import algebra.algebra.subalgebra
import ring_theory.finiteness

universe u

lemma finite_alg_has_basis {K L: Type u} [field K] [field L] [algebra K L]
  [h2:  t : finset L, algebra.adjoin K t = (: subalgebra K L)]
  [h1: algebra.finite_type K L]:
   s : finset L, is_basis K (λ x, x : (s : set L)  L)
  :=
  begin
    rcases h1 with t, ht⟩,
    use t,
    sorry
  end

if I do rcases h2 ... it works, but rcases h1 ... doesn't. I thought h2 would be equivalent to h1, it's just merging the two definitions manually.

Bryan Gin-ge Chen (Feb 24 2021 at 16:30):

Putting simp only [algebra.finite_type] at h1, before rcases works.

Rémy Degenne (Feb 24 2021 at 16:30):

This will be of little help since I don't understand what happens, but unfolding algebra.finite_type before doing rcases works:

import algebra.field
import algebra.algebra.subalgebra
import ring_theory.finiteness

universe u

lemma finite_alg_has_basis {K L: Type u} [field K] [field L] [algebra K L]
  [h2:  t : finset L, algebra.adjoin K t = (: subalgebra K L)]
  [h1: algebra.finite_type K L]:
   s : finset L, is_basis K (λ x, x : (s : set L)  L)
  :=
begin
  unfold algebra.finite_type at h1,
  rcases h1 with t, ht⟩,
  use t,
  sorry
end

Without the unfold, the error at the rcases is :

failed to revert 'h1', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)

I put it here in case it helps someone else who can explain what those things are. It is the first time I encounter frozen local instances and I don't know what they are.

Jon Eugster (Feb 24 2021 at 16:35):

Thank you @Bryan Gin-ge Chen and @Rémy Degenne, these are both very useful tactics!

Bryan Gin-ge Chen (Feb 24 2021 at 16:36):

I guess the way using unfreezing is to wrap the rcaseslike this: unfreezingI { rcases h1 with ⟨t, ht⟩, },

Rémy Degenne (Feb 24 2021 at 16:36):

You can also write rw instead of unfold in my solution.

Bryan Gin-ge Chen (Feb 24 2021 at 16:37):

There's more about unfreezingI in our tactic docs here.

Bryan Gin-ge Chen (Feb 24 2021 at 16:40):

Hmm, I guess that page doesn't say much about frozen local instances either, actually. But I guess the error message says the important part: rcases isn't able to work with a frozen local instance, so we have to unfreeze it.

Johan Commelin (Feb 24 2021 at 16:54):

But it shouldn't be necessary to do the unfreezing. There should be a lemma to do this for you. If it's not there, that's a hole in the API which should be fixed.

Johan Commelin (Feb 24 2021 at 16:57):

But it seems to be missing :sad:


Last updated: Dec 20 2023 at 11:08 UTC