Zulip Chat Archive

Stream: general

Topic: injection on types


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

view this post on Zulip Simon Hudon (Apr 11 2019 at 16:15):

No you can't

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:15):

you can, but you'll have to work

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:15):

you can count both sides, right?

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

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:16):

There's a trick in this particular case though

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:16):

Don't you think?

view this post on Zulip Simon Hudon (Apr 11 2019 at 16:16):

You mean proving a bijection?

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:17):

Something should work, shouldn't it?

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

view this post on Zulip Reid Barton (Apr 11 2019 at 16:18):

It is true but not trivial by Lean standards

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

view this post on Zulip Scott Olson (Apr 11 2019 at 16:19):

Yeah, that makes sense

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

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

view this post on Zulip Simon Hudon (Apr 11 2019 at 16:23):

Thanks @Chris Hughes!

view this post on Zulip Scott Olson (Apr 11 2019 at 16:23):

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

view this post on Zulip Scott Olson (Apr 11 2019 at 16:23):

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

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

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

view this post on Zulip Scott Olson (Apr 11 2019 at 16:26):

Oh right, that by_contradiction uses the decidable instance

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

view this post on Zulip Scott Olson (Apr 11 2019 at 16:27):

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

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

view this post on Zulip Chris Hughes (Apr 11 2019 at 16:30):

I want a prop valued fintype for this stuff.

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:30):

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

view this post on Zulip Chris Hughes (Apr 11 2019 at 16:31):

Because it's set.finite

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:31):

Oh yes!

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:31):

So it's just nonempty (fintype X)?

view this post on Zulip Chris Hughes (Apr 11 2019 at 16:33):

Yes.

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 16:34):

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

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

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 17:05):

h2 is an equality of two terms of type fintype n

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

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

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

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

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

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

view this post on Zulip Chris Hughes (Apr 11 2019 at 18:17):

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

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

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

view this post on Zulip François G. Dorais (Apr 11 2019 at 19:53):

What is an "argument of parametricity"?

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

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

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

view this post on Zulip Kevin Buzzard (Apr 11 2019 at 22:11):

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

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

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

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

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

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

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

view this post on Zulip 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: May 11 2021 at 14:11 UTC