Resolve coercion in hypothesis

Stream: new members

[Henning Dieterichs]

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

[Kevin Buzzard]

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

[Henning Dieterichs]

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

[Kevin Buzzard]

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

[Henning Dieterichs]

Why is cases hp closing the goal?

[Henning Dieterichs]

Ah, because it is an empty inductive type

[Kevin Buzzard]

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

[Henning Dieterichs]

but how does it resolve the coercion?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

import tactic

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

[Henning Dieterichs]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Henning Dieterichs]

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

[Henning Dieterichs]

does definitionionally equal mean they are equal after rewriting definitions?

[Henning Dieterichs]

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

[Kevin Buzzard]

In term mode Lean can see through all definitions.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Marc Huisinga]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

rfl is the term, refl is the tactic.

[Henning Dieterichs]

thanks a lot!

[Kevin Buzzard]

(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]

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

[Marc Huisinga]

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]

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

[Kevin Buzzard]

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]

But why is refl able to solve this:

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

?

[Kevin Buzzard]

Here's how I'd diagnose this.

[Kevin Buzzard]

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

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

[Kevin Buzzard]

I find

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

[Kevin Buzzard]

so tt && p is by definition p.

[Henning Dieterichs]

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]

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

[Marc Huisinga]

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

[Kevin Buzzard]

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]

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]

but it's not great for interactive use

[Mario Carneiro]

prefer simp

[Henning Dieterichs]

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]

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]

there should be a theorem that says that

[Kevin Buzzard]

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]

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

[Calle Sönne]

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]

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

[Calle Sönne]

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]

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]

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

[Kevin Buzzard]

import tactic

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

[Kevin Buzzard]

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]

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

[Calle Sönne]

Kevin Buzzard said:

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

unfortunately not

[Kevin Buzzard]

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

[Calle Sönne]

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]

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]

topological_space ↥((F ⋙ Profinite_to_Top ⋙ forget Top).sections)

[Kenny Lau]

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