type rewriting / type extensionality?

Stream: new members

[Daniel Fabian]

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]

you can't

[Mario Carneiro]

your theorem is nonsense

[Kenny Lau]

sad HoTT noises

[Mario Carneiro]

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

[Mario Carneiro]

the question is still nonsense though

[Daniel Fabian]

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]

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

[Mario Carneiro]

yes

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Reid Barton]

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

[Reid Barton]

oh hmm

[Mario Carneiro]

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

[Reid Barton]

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

[Daniel Fabian]

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]

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]

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]

I have no clue how to do this

[Kevin Buzzard]

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]

aha I know how to do this

[Kenny Lau]

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]

boom

[Daniel Fabian]

Kevin Buzzard said:

Rule of thumb: don't try to prove that types are equal. My understanding is that in Lean $\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]

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

[Kevin Buzzard]

Yes rw works with =.

[Daniel Fabian]

with = yes

[Daniel Fabian]

but what about simeq

[Kevin Buzzard]

Then you need a tactic.

[Mario Carneiro]

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]

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

[Kevin Buzzard]

Right. I was very surprised about this.

[Kevin Buzzard]

When I realised I couldn't prove $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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Daniel Fabian]

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]

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

[Daniel Fabian]

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

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Daniel Fabian]

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

[Mario Carneiro]

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]

makes a lot of sense.