Uncurrying n-times, but for imp

Stream: Is there code for X?

[Robert Maxton]

Is there a version of docs#Function.HasUncurry for implications/functions into Prop? I'm trying to check if a given theorem has the type ... → TFAE ?l for an arbitrary number of parameters and some list ?l; so far the recursive uncurry is the closest existing function I've found, but it only works on functions into Type u.

[Timo Carlin-Burns]

Is this what you want?

import Mathlib.Tactic

class HasUncurry' (α : Sort*) (β : outParam (Sort*)) (γ : outParam (β → Sort*)) where
  uncurry : α → (b : β) → γ b

instance hasUncurryBase (α : Sort*) (β : α → Sort*) : HasUncurry' ((a : α) → β a) α β :=
  ⟨id⟩

instance hasUncurrySubtype (α : Sort*) (β : α → Sort*) (γ : α → Prop) (δ : (a : α) → γ a → Sort*)
    [∀ a, HasUncurry' (β a) (γ a) (δ a)] :
    HasUncurry' ((a : α) → β a) { a : α // γ a } fun ⟨a, h⟩ => δ a h :=
  ⟨fun f ⟨a, h⟩ ↦ HasUncurry'.uncurry (f a) h⟩

instance hasUncurrySigma (α : Type*) (β : α → Sort*) (γ : α → Type*) (δ : (a : α) → γ a → Sort*)
    [∀ a, HasUncurry' (β a) (γ a) (δ a)] :
    HasUncurry' ((a : α) → β a) ((a : α) × γ a) fun ⟨a, g⟩ => δ a g :=
  ⟨fun f ⟨a, g⟩ ↦ HasUncurry'.uncurry (f a) g⟩

-- An example with TFAE

#check (List.tfae_of_forall)
-- ∀ (b : Prop) (l : List Prop), (∀ a ∈ l, a ↔ b) → List.TFAE l

#synth HasUncurry' (∀ (b : Prop) (l : List Prop), (∀ a ∈ l, a ↔ b) → List.TFAE l) ((b : Prop) × {l : List Prop // (∀ a ∈ l, a ↔ b)}) fun ⟨_, l, _⟩ => List.TFAE l

[Robert Maxton]

Timo Carlin-Burns

Ooh, you did it for Sigmas too! Thanks!

[Eric Wieser]

This sounds slightly like an XY problem; are you sure you actually care about doing this within Lean's type theory? Metaprogramming would be easier

[Robert Maxton]

I did end up doing that specific thing a different way, but I've already run into a different case where the class/construction would be useful, so I'm still glad to have it :p