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 rcases
like 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