# Zulip Chat Archive

## 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.

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

https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/

https://xenaproject.wordpress.com/2019/05/25/equality-part-2-syntactic-equality/

#### 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.

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

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

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

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