injection on types

Stream: general

[Scott Olson]

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

[Simon Hudon]

No you can't

[Kevin Buzzard]

you can, but you'll have to work

[Kevin Buzzard]

you can count both sides, right?

[Kevin Buzzard]

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

[Simon Hudon]

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

[Kevin Buzzard]

There's a trick in this particular case though

[Kevin Buzzard]

Don't you think?

[Simon Hudon]

You mean proving a bijection?

[Kevin Buzzard]

Something should work, shouldn't it?

[Scott Olson]

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]

It is true but not trivial by Lean standards

[Simon Hudon]

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

[Scott Olson]

Yeah, that makes sense

[Reid Barton]

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

[Chris Hughes]

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]

Thanks @Chris Hughes!

[Scott Olson]

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

[Scott Olson]

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

[Chris Hughes]

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]

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]

Oh right, that by_contradiction uses the decidable instance

[Scott Olson]

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

[Scott Olson]

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

[Kevin Buzzard]

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]

I want a prop valued fintype for this stuff.

[Kevin Buzzard]

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

[Chris Hughes]

Because it's set.finite

[Kevin Buzzard]

Oh yes!

[Kevin Buzzard]

So it's just nonempty (fintype X)?

[Chris Hughes]

Yes.

[Kevin Buzzard]

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

[Chris Hughes]

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]

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]

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]

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]

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]

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]

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]

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]

h2 is an equality of two terms of type fintype n

[Chris Hughes]

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]

@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]

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

[Scott Olson]

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]

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

[Scott Olson]

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]

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

[Scott Olson]

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]

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]

What is an "argument of parametricity"?

[Scott Olson]

@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]

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]

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]

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

[Kevin Buzzard]

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]

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]

@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]

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]

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]

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]

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