Zulip Chat Archive

Stream: new members

Topic: Resolve coercion in hypothesis


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:40):

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

view this post on Zulip Henning Dieterichs (Dec 05 2020 at 16:42):

Why is cases hp closing the goal?

view this post on Zulip Henning Dieterichs (Dec 05 2020 at 16:43):

Ah, because it is an empty inductive type

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:43):

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

view this post on Zulip Henning Dieterichs (Dec 05 2020 at 16:43):

but how does it resolve the coercion?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:45):

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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:46):

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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:46):

import tactic

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

view this post on Zulip Henning Dieterichs (Dec 05 2020 at 16:46):

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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:47):

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

view this post on Zulip Henning Dieterichs (Dec 05 2020 at 16:48):

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

view this post on Zulip Henning Dieterichs (Dec 05 2020 at 16:48):

does definitionionally equal mean they are equal after rewriting definitions?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:49):

In term mode Lean can see through all definitions.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:49):

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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:50):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:53):

rfl is the term, refl is the tactic.

view this post on Zulip Henning Dieterichs (Dec 05 2020 at 16:54):

thanks a lot!

view this post on Zulip 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 222 \le 2 with refl in tactic mode but not with rfl in term mode, which is strictly for equality)

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:56):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 16:58):

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

view this post on Zulip 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.

view this post on Zulip 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

?

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 17:06):

Here's how I'd diagnose this.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 17:07):

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

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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 17:08):

I find

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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 17:08):

so tt && p is by definition p.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Dec 05 2020 at 17:10):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 05 2020 at 17:21):

but it's not great for interactive use

view this post on Zulip Mario Carneiro (Dec 05 2020 at 17:21):

prefer simp

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 05 2020 at 17:25):

there should be a theorem that says that

view this post on Zulip 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.

view this post on Zulip 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 ;-) )

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 19:42):

import tactic

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 19:45):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 19:49):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Calle Sönne (Dec 05 2020 at 19:49):

topological_space ((F  Profinite_to_Top  forget Top).sections)

view this post on Zulip 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