eliminating fintype

Stream: Is there code for X?

[James Gallicchio]

I can't seem to find this (straightforward?) lemma about Fintype, and loogle/moogle/apply? don't seem to know either :frowning:

import Mathlib.Data.Fintype.Basic

def foo [Fintype V] (f : (L : List V) → (∀ v, v ∈ L) → β)
      (h : ∀ L1 h1 L2 h2, f L1 h1 = f L2 h2) : β := sorry

I also am failing to write it myself. Is this function not possible?

[Yakov Pechersky]

How can you construct a value of the type of h1 or h2 without being over a fintype?

[James Gallicchio]

I'm not sure what you mean -- Fintype V is one of the arguments

[James Gallicchio]

The idea is just to get access to both the concrete list AND a proof that it is complete, all within the quotient being eliminated. I guess I'm looking for some sort of quotient version of attach?

[Yakov Pechersky]

Oh, sorry, I misread the question. I read it as trying to get rid of the Fintype constraint.

[Yakov Pechersky]

You can define the multiset function via a dependent lift I think

[James Gallicchio]

actually, maybe that's also my question -- I don't see a dependent lift function; is it even possible to define a dependent lift over quotients?

[Yakov Pechersky]

Yes, the lift is creating the function from prop to beta. You'll likely have to go through Quotient.recOn

[James Gallicchio]

maybe some progress:

import Mathlib.Data.Fintype.Basic

def foo [Fintype V] (f : (L : List V) → (∀ v, v ∈ L) → β)
      (h : ∀ L1 h1 L2 h2, f L1 h1 = f L2 h2) : β :=
  Quotient.recOn (motive := fun (q : Multiset V) => (∀ v, v ∈ q) → β)
    Fintype.elems.val
    (fun L h => f L (by simp at h; exact h))
    (fun a b p => by
      simp; funext h
      simp [HasEquiv.Equiv, Setoid.r] at p
      sorry)
    Fintype.complete

I'll take another stab tomorrow, unless someone who understands Quotient.recOn gets to it by then :sweat_smile:

[Kyle Miller]

def foo [Fintype V] (f : (L : List V) → (∀ v, v ∈ L) → β)
      (h : ∀ L1 h1 L2 h2, f L1 h1 = f L2 h2) : β :=
  Quotient.hrecOn (motive := fun (q : Multiset V) => (∀ v, v ∈ q) → β)
    Finset.univ.val
    f
    (fun L1 L2 p => by
      apply Function.hfunext
      · congr! 1
        exact List.Perm.mem_iff p
      intros
      apply heq_of_eq
      apply h)
    Fintype.complete

[James Gallicchio]

thank you kyle!! my code is now sorry-less, much appreciated

[Timo Carlin-Burns]

I came up with a version that uses some new lemmas for Quotient.

import Mathlib.Data.Fintype.Basic

def Quotient.toTrunc {α : Sort*} [s : Setoid α] (q : Quotient s) : Trunc { a // ⟦a⟧ = q } :=
  q.recOn (fun a ↦ Trunc.mk ⟨a, rfl⟩) (fun _ _ _ ↦ Trunc.eq ..)

def Quotient.elim {α β : Sort*} [s : Setoid α] (q : Quotient s)
    (f : (a : α) → ⟦a⟧ = q → β) (h : ∀ a b ha hb, f a ha = f b hb)
    : β :=
  q.toTrunc.lift (fun x ↦ f x.val x.prop) (fun _ _ ↦ h ..)

def Multiset.elim {α β : Type*} (s : Multiset α) (f : (L : List α) → L = s → β)
    (h : ∀ a b ha hb, f a ha = f b hb) : β :=
  Quotient.elim s f h

def foo {α β : Type*} [Fintype α] (f : (L : List α) → (∀ a, a ∈ L) → β)
    (h : ∀ L1 h1 L2 h2, f L1 h1 = f L2 h2) : β :=
  Finset.univ.val.elim
    (fun L hL ↦ f L fun a ↦ by rw [←Multiset.mem_coe, hL]; simp)
    (by intros; apply h)

Should these be PRed?

[Eric Wieser]

A slight golf of the first one:

def Quotient.toTrunc {α : Sort*} [s : Setoid α] (q : Quotient s) : Trunc { a // ⟦a⟧ = q } :=
  q.recOnSubsingleton fun a ↦ ⟦⟨a, rfl⟩⟧

[James Gallicchio]

ooh, I do like that implementation. does this make it easier to prove this lemma?

theorem Multiset.elim_eq_forall {α β : Type*} {s : Multiset α} {f : (L : List α) → L = s → β} {h}
    (motive : Prop) (hmotive : ∀ {L hL}, Multiset.elim s f h = f L hL → motive) : motive :=
  sorry

[Timo Carlin-Burns]

theorem Multiset.elim_eq_forall {α β : Type*} {s : Multiset α} {f : (L : List α) → L = s → β} {h}
    (motive : Prop) (hmotive : ∀ {L hL}, Multiset.elim s f h = f L hL → motive) : motive := by
  induction s using Quotient.inductionOn
  exact hmotive rfl

[James Gallicchio]

Thank y'all for the quick help, I get lost so quickly with quotients :tear: