Zulip Chat Archive

Stream: new members

Topic: type rewriting / type extensionality?


view this post on Zulip Daniel Fabian (May 25 2020 at 10:34):

I'm playing around with Pi types and I've come across something where I don't know how to tell lean what to do.

import tactic

variable {α : Type*}
instance list_as_func : has_coe_to_fun (list α) :=
⟨λ xs, {i // i < xs.length}  α, λ xs i, xs.nth_le i.val i.property

example : (Π i : {i // i < 2}, ) = Π i, [, ] i :=
begin
    let xs := [1, 2],
    let f : Π i : {i // i < 2},  := by {
        rintro i, hi,
        cases i, exact xs 0, hi,
        cases i, exact xs 1, hi,
        apply absurd hi,
        simp [show i.succ.succ = i + 2, by simp],
    },
    let g : Π i, [, ] i := by {
        rintro i, hi,
        cases i, exact xs 0, hi,
        cases i, exact xs 1, hi,
        apply absurd hi,
        simp [show i.succ.succ = i + 2, by simp],
    },
    sorry
end

How can I show that two Pi types are the same?

view this post on Zulip Mario Carneiro (May 25 2020 at 10:35):

you can't

view this post on Zulip Mario Carneiro (May 25 2020 at 10:35):

your theorem is nonsense

view this post on Zulip Kenny Lau (May 25 2020 at 10:38):

sad HoTT noises

view this post on Zulip Mario Carneiro (May 25 2020 at 10:38):

Actually, looking at it carefully I think this theorem might be true

view this post on Zulip Mario Carneiro (May 25 2020 at 10:38):

the question is still nonsense though

view this post on Zulip Daniel Fabian (May 25 2020 at 10:38):

But I have seen lean go ahead and simplify things in the type, too. Like for instance it does understand that { i // i < [nat, nat] i} is the same as {i // i < 0 + 1 + 1}.

view this post on Zulip Reid Barton (May 25 2020 at 10:38):

If it's true then the proof should be rfl, right?

view this post on Zulip Mario Carneiro (May 25 2020 at 10:38):

yes

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:39):

Rule of thumb: don't try to prove that types are equal. My understanding is that in Lean N=Z\mathbb{N}=\mathbb{Z} is undecidable. Prove your types are equiv instead.

view this post on Zulip Mario Carneiro (May 25 2020 at 10:39):

It is okay to prove types are equal by defeq, but if they aren't then you shouldn't be trying to prove an equality

view this post on Zulip Mario Carneiro (May 25 2020 at 10:39):

This is definitely an #xy question though. What are you trying to do?

view this post on Zulip Reid Barton (May 25 2020 at 10:40):

I think they're not equal because you need funext & cases on i to prove it

view this post on Zulip Reid Barton (May 25 2020 at 10:40):

oh hmm

view this post on Zulip Mario Carneiro (May 25 2020 at 10:40):

The first components are defeq, the second are regular eq, so it's provable

view this post on Zulip Reid Barton (May 25 2020 at 10:40):

In that case I guess maybe they are non-definitionally equal yes

view this post on Zulip Daniel Fabian (May 25 2020 at 10:43):

I know that we can use a proof x=y to rewrite using rw, but that only works on the term level, not on the type level.

Is there a deep reason, why if I can prove something like forall i, [nat, nat] i = nat, I shouldn't be allowed to do a rewrite of the pi type?

view this post on Zulip Daniel Fabian (May 25 2020 at 10:45):

I understand, that it would want a proof, of course, because it would have to go and apply a potentially large amount of unfolding and whatnot and it may not be decidable. But if I have the proof, shouldn't it be possible to do the rewrites?

view this post on Zulip Kenny Lau (May 25 2020 at 10:46):

mwe:

universes u v

theorem pi_congr {ι : Type u} {f g : ι  Type v} (h :  i, f i = g i) :
  (Π i, f i) = Π i, g i :=
sorry

view this post on Zulip Kenny Lau (May 25 2020 at 10:46):

I have no clue how to do this

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:47):

But the real question is why someone would want to do this. = is overrated. It's not the right concept anyway, for types. It's a random equivalence relation, which seems very different to the equivalence relations on mathematical objects which mathematicians carry around in their heads.

view this post on Zulip Kenny Lau (May 25 2020 at 10:47):

aha I know how to do this

view this post on Zulip Kenny Lau (May 25 2020 at 10:48):

universes u v

theorem pi_congr {ι : Type u} {f g : ι  Type v} (h :  i, f i = g i) :
  (Π i, f i) = Π i, g i :=
by rw show f = g, from funext h

view this post on Zulip Kenny Lau (May 25 2020 at 10:48):

boom

view this post on Zulip Daniel Fabian (May 25 2020 at 10:48):

Kevin Buzzard said:

Rule of thumb: don't try to prove that types are equal. My understanding is that in Lean N=Z\mathbb{N}=\mathbb{Z} is undecidable. Prove your types are equiv instead.

Say I do this (in my case it would be easy to show the equivalence), what then? Can you use it to rewrite terms with it?

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:48):

Maybe they'd want to do it because they're an UG in the summer with nothing better to do :-)

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:48):

Yes rw works with =.

view this post on Zulip Daniel Fabian (May 25 2020 at 10:48):

with = yes

view this post on Zulip Daniel Fabian (May 25 2020 at 10:48):

but what about simeq

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:49):

Then you need a tactic.

view this post on Zulip Mario Carneiro (May 25 2020 at 10:49):

example : (Π i : {i // i < 2}, ) = Π i, [, ] i :=
suffices  i : {i // i < 2},  = [, ] i,
from congr_arg (λ f : {i // i < 2}  Type, Π x, f x) (funext this),
λ i, match i with
| 0, _⟩ := rfl
| 1, _⟩ := rfl
| n+2, h := by cases not_le_of_lt h (nat.le_add_left _ _)
end

view this post on Zulip Mario Carneiro (May 25 2020 at 10:50):

I think you are barking up the wrong tree. You probably don't need to rewrite across equivs either

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:51):

Right. I was very surprised about this.

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:52):

When I realised I couldn't prove R[1/fg]=R[1/f][1/g]R[1/fg]=R[1/f][1/g] in Lean (these are two rings which a mathematician would call equal, but if you put a gun to their head they might confess that they are merely canonically isomorphic) I instantly started banging on about an equiv_rw tactic being of utmost importance -- and Scott Morrison even made a start on one.

view this post on Zulip Reid Barton (May 25 2020 at 10:53):

The problem with these equalities of types isn't proving them, it's everything that comes after that.

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:53):

But then when Ramon Fernandez Mir started work on schemes, he didn't need the tactic anyway, he just worked with the universal property instead

view this post on Zulip Reid Barton (May 25 2020 at 10:53):

If you have a type A and you proved that h : A = A' and you want to rewrite along h, presumably you also have a value of type A and that value will not just come along for the ride.

view this post on Zulip Daniel Fabian (May 25 2020 at 10:53):

The origin of this whole mess was this:

def prod_to_pi {α β : Type*}: α × β  Π i, [α, β] i
| a,_⟩ 0, _⟩ := a
| ⟨_,b 1, _⟩ := b
| _ i + 2, hi := by norm_num at hi; linarith

So it comes from choosing a crappy index type. Using boolean instead would simplify type.

view this post on Zulip Daniel Fabian (May 25 2020 at 10:54):

but I just wanted to explore what can be done, really.

view this post on Zulip Daniel Fabian (May 25 2020 at 10:54):

not proving anything too meaningful, but more like trying to figure out how to write things down so that the proofs are easy to deal with.

view this post on Zulip Mario Carneiro (May 25 2020 at 10:54):

that is properly an equiv, and you should use either bool or a bespoke inductive type for the index type

view this post on Zulip Daniel Fabian (May 25 2020 at 10:55):

To do that, I basically have to try things out and see where (and more importantly why) they fail.

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:55):

This is exactly how I got my understanding of = within my domain -- I just tried to make a bunch of pure mathematical objects and learnt a lot.

view this post on Zulip Daniel Fabian (May 25 2020 at 10:58):

So yes, sorry for the question being not meaningful for practical purposes. Now I basically learnt, that it's not really useful to talk about definitional equality of types.

I had an exists ... that I wanted to instantiate using my type. And it said it couldn't unify, precisely because it didn't know the types were the same. The expression was the same.

view this post on Zulip Daniel Fabian (May 25 2020 at 10:58):

Split by cases twice and then eliminate the 3rd case.

view this post on Zulip Reid Barton (May 25 2020 at 10:59):

Definitional equality of types is fine. Because if A is definitionally equal to A' and a : A then also a : A'.
It's the non-definitional equality of types that is problematic.

view this post on Zulip Reid Barton (May 25 2020 at 10:59):

Even when you can prove it, you probably shouldn't.

view this post on Zulip Kevin Buzzard (May 25 2020 at 11:00):

The problem is that as a mathematician I don't want to think about "the" definition of an object -- I only care about the specification of the object, and its implementation is a matter for the CS people. I never quite know how much weight to put on definitional equality.

view this post on Zulip Mario Carneiro (May 25 2020 at 11:01):

inductive index | left | right

def index.elim {α} (a b : α) : index  α
| index.left := a
| index.right := b

def prod_to_pi {α β : Type*} : α × β  Π i, index.elim α β i
| a, _⟩ index.left := a
| ⟨_, b index.right := b

def pi_to_prod {α β : Type*} (f : Π i, index.elim α β i) : α × β := (f index.left, f index.right)

def prod_equiv_pi {α β : Type*} : α × β  Π i, index.elim α β i :=
prod_to_pi, pi_to_prod, by rintro a,b⟩; refl, λ f, by ext (_|_); refl

view this post on Zulip Daniel Fabian (May 25 2020 at 11:04):

yes, clearly having my own DU is the right way to go. And I knew that the moment, I realised that {i // i < 2} is NOT a type consisting of two elements, but rather nat with a proof of i < 2.

view this post on Zulip Daniel Fabian (May 25 2020 at 11:05):

So any pattern matching requires me to prove the impossible case.

view this post on Zulip Daniel Fabian (May 25 2020 at 11:05):

The Pi extensionality, if you will, was more like a curiosity after that.

view this post on Zulip Mario Carneiro (May 25 2020 at 11:06):

I mean, it is a type with two elements, you can prove that, but when it comes to equations in types you really want things to be defeq and that means using inductive types and recursive definitions such that everything evaluates smoothly

view this post on Zulip Daniel Fabian (May 25 2020 at 11:08):

makes a lot of sense.


Last updated: May 08 2021 at 19:11 UTC