data.fintype.card_embedding !4#2166

Stream: mathlib4

[Alex Kassil]

Ok, so taking my stab at card embedding https://github.com/leanprover-community/mathlib4/pull/2166 and I am a bit stuck.

Can someone help me understand the error message?

target
  inst✝²
has type
  Fintype α : Type u_1
but is expected to have type
  Type ?u.18390 : Type (?u.18390 + 1)

and the erroring line is

induction' ‹Fintype α› using Fintype.induction_empty_option with α₁ α₂ h₂ e ih α h ih

Here is induction_empty_option https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fintype/Option.lean#L93

/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
@[elab_as_elim]
theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
    (of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›)
    (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u)
    [Fintype α] : P α := by
   ...

induction_empty_option above seems to take a
Unsure what this error means, I think it means that ‹Fintype α› is type Fintype α : Type u_1 but needs to be Type _ : Type _, but i don't know what lean means by Type ?u.18390 : Type (?u.18390 + 1), a type of types or something

[Johan Commelin]

@Alex Kassil does refine' Fintype.induction_empty_option _ _ _ work, instead of the induction' line?

[Alex Kassil]

@Johan Commelin thanks, that unblocks me!

[Alex Kassil]

Another step another error message. Can anyone help me make heads of tails of this?
error:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ‖α₂ ↪ β‖
case refine'_1
α : Type u_1
β : Type u_2
a : Fintype α
b : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = descFactorial ‖β‖ ‖α₁‖
this : Fintype α₁ := ofEquiv α₂ (Equiv.symm e)
v1 : β ≃ β := Equiv.refl β
v2 : (α₁ ↪ β) ≃ (α₂ ↪ β) := Equiv.embeddingCongr e v1
v3 : ‖α₁ ↪ β‖ = ‖α₂ ↪ β‖ := card_congr v2
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ‖α₂ ↪ β‖
case refine'_1
α : Type u_1
β : Type u_2
a : Fintype α
b : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = descFactorial ‖β‖ ‖α₁‖
this : Fintype α₁ := ofEquiv α₂ (Equiv.symm e)
v1 : β ≃ β := Equiv.refl β
v2 : (α₁ ↪ β) ≃ (α₂ ↪ β) := Equiv.embeddingCongr e v1
v3 : ‖α₁ ↪ β‖ = ‖α₂ ↪ β‖ := card_congr v2
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖

Code

    · intro α₁ α₂ h₂ e ih
      letI := Fintype.ofEquiv α₂ e.symm
      let v1 := (Equiv.refl β)
      let v2 := (Equiv.embeddingCongr e v1)
      let v3 := card_congr v2
      rw [←v3, ih, card_congr e]

What confuses me is I see in the goal state ‖α₂ ↪ β‖, so I should be able to just rw with v3

[Johan Commelin]

Does erw work instead of rw?

[Johan Commelin]

Also, you can maybe set pp.implicit to true. To see if implicit arguments line up.

[Alex Kassil]

@Johan Commelin

No, same error with erw.
Do I set pp.implicit to true with set_option autoImplicit true? or set_option pp.explicit false? I don't seem to have a pp.implicit option

[Alex Kassil]

I also just pushed my local state so far in case that makes it easier to see what I have tried https://github.com/leanprover-community/mathlib4/pull/2166/commits/4feaff521e651201c8e71aba20e8075177e68b1d

[Alex Kassil]

Setting pp.explicit to true might hint at the error?

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  @card (α₂ ↪ β)
    (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b))
case refine'_1
α : Type u_1
β : Type u_2
a : Fintype α
b : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : @Eq ℕ (@card (α₁ ↪ β) emb) (descFactorial (@card β b) (@card α₁ a))
this : Fintype α₁ := @ofEquiv α₁ α₂ h₂ (@Equiv.symm α₁ α₂ e)
v1 : β ≃ β := Equiv.refl β
v2 : (α₁ ↪ β) ≃ (α₂ ↪ β) := @Equiv.embeddingCongr α₁ α₂ β β e v1
v3 : @Eq ℕ
  (@card (α₁ ↪ β)
    (@Embedding.fintype α₁ β this b (fun a b => Classical.propDecidable (@Eq α₁ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b)))
  (@card (α₂ ↪ β)
    (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b))) :=
  @card_congr (α₁ ↪ β) (α₂ ↪ β)
    (@Embedding.fintype α₁ β this b (fun a b => Classical.propDecidable (@Eq α₁ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b))
    (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b))
    v2
⊢ @Eq ℕ (@card (α₂ ↪ β) emb) (descFactorial (@card β b) (@card α₂ a))Lean 4

[Johan Commelin]

aah, it's now called pp.explicit in Lean 4. Yes, that's the option I meant.

[Johan Commelin]

You can try to convert v3.symm.

[Alex Kassil]

Still unable to crack this

α: Type u_1
β: Type u_2
a: Fintype α
b: Fintype β
emb: Fintype (α ↪ β)
α₁α₂: Type u_1
h₂: Fintype α₂
e: α₁ ≃ α₂
ih: @Eq ℕ (@card (α₁ ↪ β) emb) (descFactorial (@card β b) (@card α₁ a))
v0: Fintype α₁ := @ofEquiv α₁ α₂ h₂ (@Equiv.symm α₁ α₂ e)
v1: β ≃ β := Equiv.refl β
v2: (α₁ ↪ β) ≃ (α₂ ↪ β) := @Equiv.embeddingCongr α₁ α₂ β β e v1
v3: @Eq ℕ
  (@card (α₁ ↪ β)
    (@Embedding.fintype α₁ β v0 b (fun a b => Classical.propDecidable (@Eq α₁ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b)))
  (@card (α₂ ↪ β)
    (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b))) := @card_congr (α₁ ↪ β) (α₂ ↪ β)
  (@Embedding.fintype α₁ β v0 b (fun a b => Classical.propDecidable (@Eq α₁ a b)) fun a b =>
    Classical.propDecidable (@Eq β a b))
  (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
    Classical.propDecidable (@Eq β a b))
  v2
⊢ @Eq ℕ
  (@card (α₂ ↪ β)
    (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b)))
  (@card (α₂ ↪ β) emb)

type mismatch
  @HEq.rfl ?m.22040 ?m.22041
has type
  @HEq ?m.22040 ?m.22041 ?m.22040 ?m.22041 : Prop
but is expected to have type
  @Eq ℕ
    (@card (α₂ ↪ β)
      (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
        Classical.propDecidable (@Eq β a b)))
    (@card (α₂ ↪ β) emb) : Prop

The issue seems to be that the two embeddings are slightly different, unsure why or how to fix :(

[Alex Kassil]

my code

theorem card_embedding_eq {α β : Type _} [a : Fintype α] [b : Fintype β] [emb: Fintype (α ↪ β)] :
    ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖ := by
  classical
    -- letI := 1
    refine' Fintype.induction_empty_option _ _ _ α
    -- intro α₁ α₂ h₂ e ih

    -- induction' ‹Fintype α› using Fintype.induction_empty_option with α₁ α₂ h₂ e ih α h ih
    · intro α₁ α₂ h₂ e ih
      let v0 := Fintype.ofEquiv α₂ e.symm
      let v1 := (Equiv.refl β)
      let v2 := (Equiv.embeddingCongr e v1)
      let v3 := card_congr v2
      convert ←v3.symm
      · rfl
      · rw [ih]

[Johan Commelin]

Huh, is that left-arrow legal in that convert line?

[Alex Kassil]

well it seems to be legal
image.png

[Alex Kassil]

if I do it without arrow, still works,but my goal again has two different embeddings

⊢ @Eq ℕ (@card (α₂ ↪ β) emb)
  (@card (α₂ ↪ β)
    (@Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b =>
      Classical.propDecidable (@Eq β a b)))

[Johan Commelin]

Those are the same, but in a different order, right?

[Johan Commelin]

Does congr make progress here? Ideally this would be congr; apply Subsingleton.elim

[Reid Barton]

The <- is supposed to just reverse the order of the resulting equalities

[Johan Commelin]

That seems to match reality (-;

[Johan Commelin]

But I didn't know about that feature.

[Alex Kassil]

congr doesn't seem to do anything

[Alex Kassil]

Gonna go to sleep soon, but will leave my pr as help wanted

[Alex Kassil]

also pushed my current state to my branch https://github.com/leanprover-community/mathlib4/pull/2166 if anyone is willing to take another look :)

[Johan Commelin]

It is quite surprising that refine' congr_arg (@card (α₂ ↪ β)) _ doesn't make progress

[Johan Commelin]

Huh! The goal seems to be not well-typed! Because emb has type Fintype (α ↪ β).

[Alex Kassil]

Yea somehow we need to related @Embedding.fintype α₂ β h₂ b (fun a b => Classical.propDecidable (@Eq α₂ a b)) fun a b => Classical.propDecidable (@Eq β a b)) and Fintype (α ↪ β)

[Eric Wieser]

Alex Kassil said:

Ok, so taking my stab at card embedding https://github.com/leanprover-community/mathlib4/pull/2166 and I am a bit stuck.

Can someone help me understand the error message?

target
  inst✝²
has type
  Fintype α : Type u_1
but is expected to have type
  Type ?u.18390 : Type (?u.18390 + 1)

and the erroring line is

induction' ‹Fintype α› using Fintype.induction_empty_option with α₁ α₂ h₂ e ih α h ih

Here is induction_empty_option https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fintype/Option.lean#L93

/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
@[elab_as_elim]
theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
    (of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›)
    (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u)
    [Fintype α] : P α := by
   ...

induction_empty_option above seems to take a
Unsure what this error means, I think it means that ‹Fintype α› is type Fintype α : Type u_1 but needs to be Type _ : Type _, but i don't know what lean means by Type ?u.18390 : Type (?u.18390 + 1), a type of types or something

This sounds like a bug in the induction tactic

[Alex Kassil]

I will let someone else take over this file port due to the seeming bug.

[Johan Commelin]

I'm sorry that this file with only 3 lemmas turned out to be so complicated!

[Alex Kassil]

All good!! And all part of the fun

[Kevin Buzzard]

Five years ago some of my basic 1st year "intro to proofs" problem sheets turned out to be very complicated to do in Lean, and my interpretation was that indeed this was all part of the fun (or part of the challenge, if you like).

[Eric Rodriguez]

as the writer of the original file, thought I'd dive in and try find some workaround - I can now get most things working, but rw gives me a deterministic timeout at whnf?! this is way above my paygrade, sadly, but I pushed what I had

[Eric Rodriguez]

I think this proof would work better with Nat.card and Finite, now that that all exists, as I think some of the issues are the amount of Fintype instances I have to juggle...

[Jon Eugster]

not on a computer atm, but timeout at "whnf" sounds like somerhing that might be fixed by merging todays master with the new lean bump:fingers_crossed:

[Eric Rodriguez]

sadly not fully (altohugh stuff feels faster!)

[Eric Rodriguez]

image.png

[Eric Rodriguez]

for some reason Lean just doesn't like this term

[Eric Rodriguez]

whenever I try to do anything to it it gets really annoyed at me

[Eric Rodriguez]

(the heartbeats are lower but I can bump them up to any number I want and still stuff breaks)

[Eric Rodriguez]

(there's some shadowed variables in this screenshot, and I thought this may have been related - it's not)

[Eric Rodriguez]

this is really weird: Lean thinks this term has a metavariable, but it doesn't, h is in the context:

image.png

[Eric Rodriguez]

for the purposes of debugging, is there some tactic that I can run that says "set this metavariable to X" and see if this fixes it?

[Eric Rodriguez]

(also, @mods, is there any chance the preceding discussion could be moved to a thread specific to this PR?)

[Notification Bot]

44 messages were moved here from #mathlib4 > Addin @alexkassil on github for port by Johan Commelin.

[Jireh Loreaux]

I ran into a whnf timeout a week or two ago and the issue was that Lean couldn't unify. Providing the correct type ascription fixed it. I used #whnf and #check to figure things out. The check showed me there was a variable in one of the expressions and then I realized it wasn't unifying. So maybe try that?

[Eric Rodriguez]

I fixed it by changing other stuff, but I'm not really happy about my fix

[Eric Rodriguez]

I also made docs#function.embedding.fintype just be noncomputable and not have decidable_eqs, they were causing unresolvable problems as far as I can tell

[Eric Rodriguez]

Eric Rodriguez said:

for the purposes of debugging, is there some tactic that I can run that says "set this metavariable to X" and see if this fixes it?

i'm still curious about this, fwiw

[Eric Rodriguez]

and separately, this PR is ready for review - sorry that I didn't set the labels correctly before!

[Alex Kassil]

PR is merged :D