Stream: general

Topic: injection on types

Scott Olson (Apr 11 2019 at 16:14):

If I have the hypothesis h : fin n = fin m, am I allowed to conclude n = m? If so, how?

No you can't

Kevin Buzzard (Apr 11 2019 at 16:15):

you can, but you'll have to work

Kevin Buzzard (Apr 11 2019 at 16:15):

you can count both sides, right?

Kevin Buzzard (Apr 11 2019 at 16:16):

Note however that equality of types is evil, so what you are doing might not be the best idea.

Simon Hudon (Apr 11 2019 at 16:16):

You would need for fin to be an injective function and inductive types are not assumed to be injective. Only their constructors

Kevin Buzzard (Apr 11 2019 at 16:16):

There's a trick in this particular case though

Don't you think?

Simon Hudon (Apr 11 2019 at 16:16):

You mean proving a bijection?

Kevin Buzzard (Apr 11 2019 at 16:17):

Something should work, shouldn't it?

Scott Olson (Apr 11 2019 at 16:18):

I may not need this, but it came up in a larger proof I was struggling with and I was curious if I was missing something obvious or if it was truly non-trivial

Reid Barton (Apr 11 2019 at 16:18):

It is true but not trivial by Lean standards

Simon Hudon (Apr 11 2019 at 16:18):

It is non-trivial. In general, it is not possible. I'm not convinced that it's possible in this case

Scott Olson (Apr 11 2019 at 16:19):

Yeah, that makes sense

Reid Barton (Apr 11 2019 at 16:21):

Also, what Kevin said--if you find yourself needing this then most likely something went wrong earlier

Chris Hughes (Apr 11 2019 at 16:21):

lemma fin_injective {n m : ℕ} (h : fin n = fin m) : n = m :=
by_contradiction $λ hnm, have hcard : fintype.card (fin n) ≠ fintype.card (fin m), by simpa, have hm : fintype.card (fin m) = m, by simp, hcard$ by simp [h]; convert hm


Simon Hudon (Apr 11 2019 at 16:23):

Thanks @Chris Hughes!

Scott Olson (Apr 11 2019 at 16:23):

@Reid Barton That's also good to know, thanks

Scott Olson (Apr 11 2019 at 16:23):

Interesting, so it's classically provable, I guess?

Chris Hughes (Apr 11 2019 at 16:25):

It shouldn't need classical logic. Equality of naturals is decidable, so by_contradiction is fine. My theorem does use classical logic, but only because mathlib uses it where it's totally unnecessary.

Kevin Buzzard (Apr 11 2019 at 16:26):

I think the more interesting question is why you were faced with this goal in the first place. We just got lucky in this case. We can't prove ℕ ≠ ℤ for example. Equality of types is not at all well-behaved in dependent type theory.

Scott Olson (Apr 11 2019 at 16:26):

Oh right, that by_contradiction uses the decidable instance

Scott Olson (Apr 11 2019 at 16:26):

Yeah, I expect I'll be back later with a question closer to the actual problem I'm dealing with

Scott Olson (Apr 11 2019 at 16:27):

In my experience it is typically simp which makes every theorem use every axiom

Kevin Buzzard (Apr 11 2019 at 16:29):

import data.fintype

example (m n : ℕ) (h : fin m = fin n) : n = m :=
begin
have hm : fintype.card (fin m) = m := by simp,
have hn : fintype.card (fin n) = n := by simp,
simp [h] at hm, -- phew
convert hm,
convert hn.symm, -- phew
end


Chris Hughes (Apr 11 2019 at 16:30):

I want a prop valued fintype for this stuff.

Kevin Buzzard (Apr 11 2019 at 16:30):

finite isn't good enough because you lose the size?

Chris Hughes (Apr 11 2019 at 16:31):

Because it's set.finite

Oh yes!

Kevin Buzzard (Apr 11 2019 at 16:31):

So it's just nonempty (fintype X)?

Yes.

Kevin Buzzard (Apr 11 2019 at 16:34):

And then you'll have some noncomputable prop_fintype.card?

Chris Hughes (Apr 11 2019 at 16:36):

Something like that. I don't know if this is a good approach though. I guess coq with its non definitional proof irrelevance must have good tactics for dealing with this.

Scott Olson (Apr 11 2019 at 16:38):

Inspired by @Kevin Buzzard's, I realized the reasoning is pretty direct:

example (m n : ℕ) (h : fin n = fin m) : n = m := calc
n = fintype.card (fin n) : (fintype.card_fin n).symm
... = fintype.card (fin m) : by { congr, exact h }
... = m                    : fintype.card_fin m


Kevin Buzzard (Apr 11 2019 at 16:51):

The middle equality is the ropey one. Look at this:

example (m n : ℕ) (h : fin m = fin n) : fintype.card (fin m) = fintype.card (fin n) :=
begin
--  rw h, -- fails!
--  erw h, -- fails!
simp [h], -- works...
-- ⊢ fintype.card (fin n) = n
exact fintype.card_fin n, -- fails!
end


The failure error is:

invalid type ascription, term has type
@fintype.card (fin n) (fin.fintype n) = n
but is expected to have type
@fintype.card (fin n) (@eq.rec Type (fin m) (λ (α : Type), fintype α) (fin.fintype m) (fin n) h) = n


Lean has switched on pp.all so you can see the problem. When Lean says fintype.card X it really means @fintype.card X (term of type fintype X), and the hidden terms are not definitionally equal.

Kevin Buzzard (Apr 11 2019 at 16:52):

On the other hand, this works:

example (m n : ℕ) (h : fin m = fin n) : fintype.card (fin m) = fintype.card (fin n) :=
begin
simp [h],
-- ⊢ fintype.card (fin n) = n
convert fintype.card_fin n,
end


When you're playing fast and loose with type equality like this, I've seen situations where exact doesn't close the goal but convert does.

Kevin Buzzard (Apr 11 2019 at 16:55):

The point is that fintype is not a proposition, but it is a subsingleton, so there can be at most one term of type fintype X. However, if my understanding is correct, then if you have two terms of type fintype X then in contrast to propositions, the fact that they are equal might be a theorem, rather than definitional.

instance (α : Type*) : subsingleton (fintype α) :=
⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext, h₁, h₂]⟩


In the proof that fintype X is a subsingleton in the library, congr is used.

Scott Olson (Apr 11 2019 at 16:58):

If you dump the proof term of my proof you see this: (congr (eq.refl (fintype.card α_1)) (subsingleton.elim (eq.rec _inst_1 e_1) _inst_1_1))) which is relating two different instances of fintype and mentions subsingleton =)

Reid Barton (Apr 11 2019 at 16:58):

congr knows about subsingletons and will automatically take care of goals that would have been generated that say that two values of a subsingleton are equal. That's why Scott's congr proof worked, because of the subsingleton instance that Kevin just mentioned. It's also why using convert worked, because convert uses congr internally.

Kevin Buzzard (Apr 11 2019 at 17:04):

example (m n : ℕ) (h : fin m = fin n) : fintype.card (fin m) = fintype.card (fin n) :=
begin
simp [h],
-- ⊢ fintype.card (fin n) = n but there's a horrible term of type fintype (fin n) in there
have h2 : (@eq.rec Type (fin m) (λ (α : Type), fintype α) (fin.fintype m) (fin n) h) = fin.fintype n,
--    refl, -- fails
apply subsingleton.elim, -- works
rw h2, -- horrible invisible term now replaced by correct term
exact fintype.card_fin n, -- now works
end


Here I manually do the rewrite, so I can get exact to work.

Kevin Buzzard (Apr 11 2019 at 17:05):

h2 is an equality of two terms of type fintype n

Chris Hughes (Apr 11 2019 at 17:13):

Maybe equivs are easier than type equalities.

lemma fin_injective {n m : ℕ} (h : fin n = fin m) : n = m :=
have e : fin n ≃ fin m, by rw h,
by rw [← fintype.card_fin n, fintype.card_congr e, fintype.card_fin]


Kevin Buzzard (Apr 11 2019 at 17:17):

@Scott Olson Chris' approach is much better, because if you have two types which you personally think are equal, then dependent type theory wants them not to be equal but to be equiv. Nobody has mentioned this yet in this thread! equiv of types (which is data) is the correct notion of type equality. Chris takes your crazy equality, translates it into an equiv of types, and then the proof is straightforward with no weird stuff going on under the hood.

Kevin Buzzard (Apr 11 2019 at 17:19):

Actually, here the congr is hidden in the application of fintype.card_congr so there is still some dirty work going on.

Scott Olson (Apr 11 2019 at 17:21):

Yeah, for sure, I wouldn't intentionally try to bring type equalities into my proof but they came up automatically during a few attempts and I got curious about the limits of those

Scott Olson (Apr 11 2019 at 17:23):

An example of another true one that's probably harder or impossible to solve is list a = list b -> a = b

Scott Olson (Apr 11 2019 at 17:33):

Whereas with equivalences it might be provable by building an equivalence of a and b that goes through single-element lists and proves they must roundtrip properly because of the left/right inverse properties

Chris Hughes (Apr 11 2019 at 18:17):

For lists, it doesn't work with equivalences if a and b are finite or countable.

Scott Olson (Apr 11 2019 at 18:26):

Well, if they are used completely parametrically the list a \equiv list b equivalence can't know if they're finite/countable or not, but then it turns into an argument of parametricity, another set of things that tend to be true but unprovable in current dependent type systems

Reid Barton (Apr 11 2019 at 18:35):

You don't really want parametricity statements to be theorems internally, because they aren't true in the "standard" model that we usually want to interpret Lean into.

François G. Dorais (Apr 11 2019 at 19:53):

What is an "argument of parametricity"?

Scott Olson (Apr 11 2019 at 21:04):

@François G. Dorais parametricity is the property that functions which are completely generic over some type are restricted in what they could possibly do with them, e.g. I can argue that ∀ {α : Type}, α → α must be the identity function

Scott Olson (Apr 11 2019 at 21:04):

Not sure of a good link off the top of my head, but there's a bit of a wikipedia article https://en.wikipedia.org/wiki/Parametricity

Kevin Buzzard (Apr 11 2019 at 22:10):

You could argue this but it's not provable, right? And in Lean's type theory it's not even true, if you allow me to switch on decidability of all propositions and then say that it's the identity except on bool when it switches true and false

Kevin Buzzard (Apr 11 2019 at 22:11):

Maybe that's a concrete version of what Reid is saying

Kevin Buzzard (Apr 11 2019 at 22:12):

Why are we even talking about this? If you have the hypothesis list a = list b then my impression is that you have made a design error of some sort

matt rice (Apr 11 2019 at 22:46):

I put some rather self contained identity stuff here, which I guess is intended to show some trouble https://gist.github.com/ratmice/eb771aa05ff9106ff0bb07dca6e6eecb

Scott Olson (Apr 11 2019 at 23:17):

@Kevin Buzzard Yeah, I brought it up as a more likely unprovable example to support the idea that this should be avoided.

And right, the parametricity argument is not provable in most current systems of dependent types I've seen. There are a few papers on designing systems where you actually get the "Theorems for Free" for free.

Scott Olson (Apr 11 2019 at 23:18):

I hadn't thought about classical reasoning breaking parametricity but that makes sense. Anything that lets you match on opaque types in some way means you don't actually have parametric polymophism, you have ad hoc polymorphism.

Scott Olson (Apr 12 2019 at 00:42):

To make things completely concrete, this is the classical counterexample to parametricity I didn't think about that was mentioned:

local attribute [instance] classical.prop_decidable

noncomputable def non_id {α : Type} (x : α) : α :=
if h : α = bool
then h.mpr (bnot (h.mp x))
else x


Mario Carneiro (Apr 12 2019 at 00:46):

Notably, this definition is noncomputable. It is believed (but not proven, I think) that any computable definition of id is defeq to the obvious one

Mario Carneiro (Apr 12 2019 at 01:02):

ah, no defeq is the wrong notion for that. Here's a counterexample:

noncomputable def stuck_id {α : Sort*} (x : α) : α :=
bool.rec x x (@classical.choice bool ⟨tt⟩)

theorem stuck_id_eq {α : Sort*} (x : α) : stuck_id x = x :=
by unfold stuck_id; cases @classical.choice bool ⟨tt⟩; refl

def foo {α : Type} (x : α) : α :=
cast (show stuck_id α = α, from (stuck_id_eq α)) \$
cast (show α = stuck_id α, from (stuck_id_eq α).symm) x

set_option pp.proofs true
#reduce @foo
-- λ {α : Type} (x : α),
--   eq.rec
--     (eq.rec x
--        (eq.rec (eq.refl (bool.rec α α (classical.choice (nonempty.intro tt))))
--           (bool.rec (eq.refl α) (eq.refl α) (classical.choice (nonempty.intro tt)))))
--     (bool.rec (eq.refl α) (eq.refl α) (classical.choice (nonempty.intro tt)))

-- Lean VM doesn't know what the big deal is...
#eval @foo ℕ 3 -- 3


Last updated: Dec 20 2023 at 11:08 UTC