Zulip Chat Archive

Stream: new members

Topic: Word in reduced form

Giacomo Maletto (Nov 16 2021 at 21:18):

Suppose I'm working with an element of free_group α and I want to express "let v=v1ϵ1vkϵkv = v_1^{\epsilon_1} \dots v_k^{\epsilon_k} be its reduced form". If α has decidable_eq I think I can use the reduce function together with theorem reduce.self, but is it possible to prove a general statement like "a word always admits reduced form"?

David Wärn (Nov 16 2021 at 21:25):

Yes, every type has decidable equality if you're working classically

Reid Barton (Nov 16 2021 at 21:26):

And if every word has a reduced form then α must have decidable equality, because given xx and yy you can look at the reduced form of xy1xy^{-1} to decide whether x=yx = y

Giacomo Maletto (Nov 16 2021 at 21:28):

Interesting, and how do you tell Lean that every type has decidable equality?

Giacomo Maletto (Nov 16 2021 at 21:30):

That is to say, how can I use that fact in a proof?

Kevin Buzzard (Nov 16 2021 at 21:36):

Use the classical tactic in your proof

Last updated: Dec 20 2023 at 11:08 UTC