Zulip Chat Archive

Stream: new members

Topic: type rewriting / type extensionality?


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?

Mario Carneiro (May 25 2020 at 10:35):

you can't

Mario Carneiro (May 25 2020 at 10:35):

your theorem is nonsense

Kenny Lau (May 25 2020 at 10:38):

sad HoTT noises

Mario Carneiro (May 25 2020 at 10:38):

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

Mario Carneiro (May 25 2020 at 10:38):

the question is still nonsense though

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

Reid Barton (May 25 2020 at 10:38):

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

Mario Carneiro (May 25 2020 at 10:38):

yes

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.

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

Mario Carneiro (May 25 2020 at 10:39):

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

Reid Barton (May 25 2020 at 10:40):

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

Reid Barton (May 25 2020 at 10:40):

oh hmm

Mario Carneiro (May 25 2020 at 10:40):

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

Reid Barton (May 25 2020 at 10:40):

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

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?

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?

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

Kenny Lau (May 25 2020 at 10:46):

I have no clue how to do this

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.

Kenny Lau (May 25 2020 at 10:47):

aha I know how to do this

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

Kenny Lau (May 25 2020 at 10:48):

boom

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?

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 :-)

Kevin Buzzard (May 25 2020 at 10:48):

Yes rw works with =.

Daniel Fabian (May 25 2020 at 10:48):

with = yes

Daniel Fabian (May 25 2020 at 10:48):

but what about simeq

Kevin Buzzard (May 25 2020 at 10:49):

Then you need a tactic.

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

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

Kevin Buzzard (May 25 2020 at 10:51):

Right. I was very surprised about this.

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.

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.

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

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.

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.

Daniel Fabian (May 25 2020 at 10:54):

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

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.

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

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.

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.

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.

Daniel Fabian (May 25 2020 at 10:58):

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

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.

Reid Barton (May 25 2020 at 10:59):

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

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.

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

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.

Daniel Fabian (May 25 2020 at 11:05):

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

Daniel Fabian (May 25 2020 at 11:05):

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

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

Daniel Fabian (May 25 2020 at 11:08):

makes a lot of sense.


Last updated: Dec 20 2023 at 11:08 UTC