## Stream: new members

### Topic: Resolve coercion in hypothesis

#### Henning Dieterichs (Dec 05 2020 at 16:37):

I have h: ↥p. How do I rewrite it to h: p = tt? Neither rw coe nor simp worked.

#### Kevin Buzzard (Dec 05 2020 at 16:38):

p is a bool, presumably? You could do cases on it I guess, but there is probably a one-liner.

#### Henning Dieterichs (Dec 05 2020 at 16:39):

yes, p is a bool ;) Would love to have a one-liner at hand to deal with coercions!

#### Kevin Buzzard (Dec 05 2020 at 16:40):

example (p : bool) (hp : p) : p = tt :=
begin
cases p,
{ cases hp },
{ refl },
end

#### Henning Dieterichs (Dec 05 2020 at 16:42):

Why is cases hp closing the goal?

#### Henning Dieterichs (Dec 05 2020 at 16:43):

Ah, because it is an empty inductive type

#### Kevin Buzzard (Dec 05 2020 at 16:43):

because there are no cases, so there are no goals after it's done :-)

#### Henning Dieterichs (Dec 05 2020 at 16:43):

but how does it resolve the coercion?

#### Kevin Buzzard (Dec 05 2020 at 16:44):

If p is a random bool then Lean doesn't know what ↥p is, but if p is tt or ff then it knows.

#### Kevin Buzzard (Dec 05 2020 at 16:45):

no I just checked the definition and what I just said is false.

#### Kevin Buzzard (Dec 05 2020 at 16:46):

I had assumed the coercion would be defined by cases, but ↥p := p = tt

#### Kevin Buzzard (Dec 05 2020 at 16:46):

import tactic

example (p : bool) (hp : p) : p = tt :=
begin
exact hp,
end

#### Henning Dieterichs (Dec 05 2020 at 16:46):

hmm, I guess exact is doing some kind of reduction then?

#### Kevin Buzzard (Dec 05 2020 at 16:47):

They are definitionally equal. You can use change to change one to the other. Sorry for misleading you!

#### Kevin Buzzard (Dec 05 2020 at 16:47):

example (p : bool) (hp : p) : p = tt := hp

#### Henning Dieterichs (Dec 05 2020 at 16:48):

no problem, thank you very much for helping me reducing my confusion ;)

#### Henning Dieterichs (Dec 05 2020 at 16:48):

does definitionionally equal mean they are equal after rewriting definitions?

#### Henning Dieterichs (Dec 05 2020 at 16:49):

why does this unfolding of definitions happen automatically, while I have to unfold all my definitions manually or with simp?

#### Kevin Buzzard (Dec 05 2020 at 16:49):

In term mode Lean can see through all definitions.

#### Kevin Buzzard (Dec 05 2020 at 16:49):

You need to talk to someone who knows something about computers really.

#### Kevin Buzzard (Dec 05 2020 at 16:50):

https://leanprover.github.io/reference/expressions.html#computation is something I found useful

#### Marc Huisinga (Dec 05 2020 at 16:50):

Kevin Buzzard said:

You need to talk to someone who knows something about computers really.

i remember that you wrote a pretty good blog post on the matter yourself

#### Kevin Buzzard (Dec 05 2020 at 16:50):

but you might know it already. You might want to hear something about #reduce but this is something I never use or think about.

#### Kevin Buzzard (Dec 05 2020 at 16:51):

Lean won't unfold a definition automatically, but if I say x = y and the proof is rfl, then at that point Lean will start to try and prove x and y are definitionally equal and it will happily unfold anything.

#### Kevin Buzzard (Dec 05 2020 at 16:52):

In fact you can hang Lean by giving it two complicated terms which aren't equal and then telling it to try and prove them by rfl. The exact tactic will presumably just be a wrapper around rfl.

#### Henning Dieterichs (Dec 05 2020 at 16:53):

ah so rfl is the tactic I can use to show that two syntactically different terms are definitionally equivalent?

#### Kevin Buzzard (Dec 05 2020 at 16:53):

rfl is the term, refl is the tactic.

thanks a lot!

#### Kevin Buzzard (Dec 05 2020 at 16:55):

(strictly speaking refl is a bit stronger, it will attempt to prove any goal of the form R a b where R is a reflexive predicate which has been tagged with the @[refl] attribute by invoking reflexivity of R and then trying to prove a = b; for example you can prove $2 \le 2$ with refl in tactic mode but not with rfl in term mode, which is strictly for equality)

#### Kevin Buzzard (Dec 05 2020 at 16:56):

example : 2 + 2 = 4 := rfl (because both reduce to S(S(S(S(0))))

#### Marc Huisinga (Dec 05 2020 at 16:58):

if you care about implementation details, rfl is just eq.refl (https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L231), where eq.refl is described in TPIL (https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#inductive-families), and definitional equality is built into the kernel

#### Kevin Buzzard (Dec 05 2020 at 16:58):

example (p : bool) : p = tt = ↥p := rfl

#### Kevin Buzzard (Dec 05 2020 at 16:59):

and the contradiction is that definitional equality is undecidable but rfl is a computer program :-) There's an example in the reference manual where two things are definitionally equal but rfl doesn't prove it, but this is very much an edge case.

#### Henning Dieterichs (Dec 05 2020 at 17:05):

But why is refl able to solve this:

example (p: bool): tt && p = p :=
begin
refl,
end

?

#### Kevin Buzzard (Dec 05 2020 at 17:06):

Here's how I'd diagnose this.

#### Kevin Buzzard (Dec 05 2020 at 17:07):

#print notation && -- it's notation for band

#check band -- and now right click and peek definition

#### Kevin Buzzard (Dec 05 2020 at 17:08):

I find

def band : bool  bool  bool
| tt b := b
| ff b := ff

#### Kevin Buzzard (Dec 05 2020 at 17:08):

so tt && p is by definition p.

#### Henning Dieterichs (Dec 05 2020 at 17:08):

So I guess there is some kind of reduction β and refl solves R a b by checking whether β a is syntactically equal to β b? Can I somehow invoke this reduction β manually to make terms simpler in hypothesis/goals?

#### Kevin Buzzard (Dec 05 2020 at 17:09):

yeah you need to talk to a computers person. I have no idea how all this works.

#### Marc Huisinga (Dec 05 2020 at 17:10):

https://leanprover-community.github.io/mathlib_docs/tactics.html#dsimp

#### Kevin Buzzard (Dec 05 2020 at 17:10):

If I want to unfold things I just unfold them. As a mathematician I believe that definitional equality is a weird implementation issue which I should not be using; I don't like the fact that n + 0 = n is definitional and 0 + n = n is not because this upsets my view of the universe as a beautiful symmetric thing. In short, I try not to think about definitional equality. But for what you're doing it's probably super-important!

#### Mario Carneiro (Dec 05 2020 at 17:21):

Henning Dieterichs said:

So I guess there is some kind of reduction β and refl solves R a b by checking whether β a is syntactically equal to β b? Can I somehow invoke this reduction β manually to make terms simpler in hypothesis/goals?

The tactic for this is called whnf

#### Mario Carneiro (Dec 05 2020 at 17:21):

but it's not great for interactive use

prefer simp

#### Henning Dieterichs (Dec 05 2020 at 17:22):

But still, this does not work to get rid of the coercion operator:

example (p : bool) (hp : p) : p = tt :=
begin
simp at hp,
sorry
end

#### Henning Dieterichs (Dec 05 2020 at 17:23):

I don't want to prove that two terms are equal, I want to obtain p = tt, so I can rewrite that term at a different hypothesis

#### Mario Carneiro (Dec 05 2020 at 17:25):

there should be a theorem that says that

#### Kevin Buzzard (Dec 05 2020 at 17:55):

import tactic

example (p : bool) (hp : p) : p = tt :=
begin
unfold_coes at hp,
assumption
end

works but goes a little against the way things are supposed to work.

#### Kevin Buzzard (Dec 05 2020 at 17:56):

(and of course the assumption tactic works without unfold_coes anyway, because it also relies on rfl ;-) )

#### Calle Sönne (Dec 05 2020 at 19:21):

I think I have a very similar problem to this one. I also need to "unfold" a coercion, but in my specific situation I am unsure how to enter tactic mode to be able to try the above suggestions. Here is my code:

def limit_cone (F : J  Profinite) : cone F :=
{ X := { to_Top := {
α := (F  Profinite_to_Top  forget Top).sections,
str := topological_space.induced
(@set.inclusion _ (F  Profinite_to_Top  (forget Top)).sections set.univ (set.subset_univ _))
(@Pi.topological_space J ((F  Profinite_to_Top  (forget Top)).obj)
(λ j, ((F  Profinite_to_Top).obj j).str))
},
is_compact := _,
is_t2 := _,
is_totally_disconnected := _ },
π := _ }

And I get the following error:

type mismatch at application
topological_space.induced (set.inclusion _) Pi.topological_space
term
Pi.topological_space
has type
topological_space (Π (a : J), (F  Profinite_to_Top  forget Top).obj a)
but is expected to have type
topological_space set.univ

and set.univ is just: set (Π (j : J), (F ⋙ Profinite_to_Top ⋙ forget Top).obj j).

So is there some way of "wrapping" the Pi.topological_space line in tactic mode and then rewriting it in there? Or is there a theorem I can use directly in term mode?

#### Kevin Buzzard (Dec 05 2020 at 19:23):

I suspect that ↥set.univ is not _definitionally_ equal to (Π (a : J), (F ⋙ Profinite_to_Top ⋙ forget Top).obj a).

#### Calle Sönne (Dec 05 2020 at 19:25):

When I have my cursor on the Pi.topological_space line and press set.univ in the infoview that is what I get

#### Calle Sönne (Dec 05 2020 at 19:27):

Or I get that set.univ is set (Π (j : J), (F ⋙ Profinite_to_Top ⋙ forget Top).obj j) but maybe I dont understand what the coercion is doing. I assume that coe_sort will give me (Π (j : J), (F ⋙ Profinite_to_Top ⋙ forget Top).obj j)

#### Kevin Buzzard (Dec 05 2020 at 19:42):

No it won't, it will give you a type which bijects with that but which is not equal to that.

#### Kevin Buzzard (Dec 05 2020 at 19:42):

import tactic

example (X : Type) : X = (set.univ : set X) :=
begin
refl -- fails
end

#### Kevin Buzzard (Dec 05 2020 at 19:44):

The coercion will give you a subtype of X corresponding to all the terms in X for which true is true, so in particular it will give you a different but isomorphic type.

#### Kevin Buzzard (Dec 05 2020 at 19:45):

What happens if you just delete str completely? Does type class inference fill it in?

#### Calle Sönne (Dec 05 2020 at 19:48):

Kevin Buzzard said:

What happens if you just delete str completely? Does type class inference fill it in?

unfortunately not

#### Kevin Buzzard (Dec 05 2020 at 19:49):

What is the goal in str := begin sorry end?

#### Calle Sönne (Dec 05 2020 at 19:49):

Kevin Buzzard said:

The coercion will give you a subtype of X corresponding to all the terms in X for which true is true, so in particular it will give you a different but isomorphic type.

That is interesting. So I should look for some lemma which puts a topology on an isomorphic type? Maybe that will be hard to work with in practice though

#### Kevin Buzzard (Dec 05 2020 at 19:49):

Maybe something like str := by unfold sections; apply_instance will work? Can you post some working code which I can run at my end?

#### Calle Sönne (Dec 05 2020 at 19:49):

topological_space ((F  Profinite_to_Top  forget Top).sections)

#### Kenny Lau (Dec 05 2020 at 19:50):

@Calle Sönne if you want to do this in real time you can stream in Xena

Last updated: May 06 2021 at 20:13 UTC