feat(Logic/Function/FromTypes): Add curried heterogeneous function ty…

…pes (#10394)

See #10389

Mathlib.lean

@@ -2620,6 +2620,7 @@ import Mathlib.Logic.Equiv.Set
 import Mathlib.Logic.Equiv.TransferInstance
 import Mathlib.Logic.Function.Basic
 import Mathlib.Logic.Function.Conjugate
+import Mathlib.Logic.Function.FromTypes
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Logic.Function.OfArity
 import Mathlib.Logic.Hydra

Mathlib/Data/Fin/Tuple/Curry.lean

@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Eric Wieser
+Authors: Eric Wieser, Brendan Murphy
 -/
 import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Logic.Equiv.Fin
 import Mathlib.Logic.Function.OfArity
 
 /-!
@@ -17,55 +18,120 @@ n-ary generalizations of the binary `curry` and `uncurry`.
 
 * `Function.OfArity.uncurry`: convert an `n`-ary function to a function from `Fin n → α`.
 * `Function.OfArity.curry`: convert a function from `Fin n → α` to an `n`-ary function.
+* `Function.FromTypes.uncurry`: convert an `p`-ary heterogeneous function to a
+  function from `(i : Fin n) → p i`.
+* `Function.FromTypes.curry`: convert a function from `(i : Fin n) → p i` to a
+  `p`-ary heterogeneous function.
 
 -/
 
-universe u
+universe u v w w'
 
-variable {α β : Type u}
+namespace Function.FromTypes
 
-namespace Function.OfArity
+open Matrix (vecCons vecHead vecTail vecEmpty)
 
-/-- Uncurry all the arguments of `Function.OfArity α n` to get a function from a tuple.
+/-- Uncurry all the arguments of `Function.FromTypes p τ` to get
+a function from a tuple.
 
-Note this can be used on raw functions if used-/
-def uncurry {n} (f : Function.OfArity α β n) : (Fin n → α) → β :=
-  match n with
-  | 0 => fun _ => f
-  | _ + 1 => fun args => (f (args 0)).uncurry (args ∘ Fin.succ)
+Note this can be used on raw functions if used. -/
+def uncurry : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} →
+    (f : Function.FromTypes p τ) → ((i : Fin n) → p i) → τ
+  | 0    , _, _, f => fun _    => f
+  | _ + 1, _, _, f => fun args => (f (args 0)).uncurry (args ∘' Fin.succ)
 
-/-- Uncurry all the arguments of `Function.OfArity α β n` to get a function from a tuple. -/
-def curry {n} (f : (Fin n → α) → β) : Function.OfArity α β n :=
-  match n with
-  | 0 => f Fin.elim0
-  | _ + 1 => fun a => curry (fun args => f (Fin.cons a args))
+/-- Curry all the arguments of `Function.FromTypes p τ` to get a function from a tuple. -/
+def curry : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} →
+    (((i : Fin n) → p i) → τ) → Function.FromTypes p τ
+  | 0    , _, _, f => f isEmptyElim
+  | _ + 1, _, _, f => fun a => curry (fun args => f (Fin.cons a args))
 
 @[simp]
-theorem curry_uncurry {n} (f : Function.OfArity α β n) :
-    curry (uncurry f) = f :=
-  match n with
-  | 0 => rfl
-  | n + 1 => funext fun a => by
-    dsimp [curry, uncurry, Function.comp_def]
-    simp only [Fin.cons_zero, Fin.cons_succ]
-    rw [curry_uncurry]
+theorem uncurry_apply_cons {n : ℕ} {α} {p : Fin n → Type u} {τ : Type u}
+    (f : Function.FromTypes (vecCons α p) τ) (a : α) (args : (i : Fin n) → p i) :
+    uncurry f (Fin.cons a args) = @uncurry _ p _ (f a) args := rfl
+
+@[simp low]
+theorem uncurry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u}
+    (f : Function.FromTypes p τ) (args : (i : Fin (n + 1)) → p i) :
+    uncurry f args = uncurry (f (args 0)) (Fin.tail args) :=
+  @uncurry_apply_cons n (p 0) (vecTail p) τ f (args 0) (Fin.tail args)
 
 @[simp]
-theorem uncurry_curry {n} (f : (Fin n → α) → β) :
+theorem curry_apply_cons {n : ℕ} {α} {p : Fin n → Type u} {τ : Type u}
+    (f : ((i : Fin (n + 1)) → (vecCons α p) i) → τ) (a : α) :
+    curry f a = @curry _ p _ (f ∘' Fin.cons a) := rfl
+
+@[simp low]
+theorem curry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u}
+    (f : ((i : Fin (n + 1)) → p i) → τ) (a : p 0) :
+    curry f a = curry (f ∘ Fin.cons a) := rfl
+
+variable {n : ℕ} {p : Fin n → Type u} {τ : Type u}
+
+@[simp]
+theorem curry_uncurry (f : Function.FromTypes p τ) : curry (uncurry f) = f := by
+  induction n with
+  | zero => rfl
+  | succ n ih => exact funext (ih $ f .)
+
+@[simp]
+theorem uncurry_curry (f : ((i : Fin n) → p i) → τ) :
     uncurry (curry f) = f := by
   ext args
-  induction args using Fin.consInduction with
-  | h0 => rfl
-  | h a as ih =>
-    dsimp [curry, uncurry, Function.comp_def]
-    simp only [Fin.cons_zero, Fin.cons_succ, ih (f <| Fin.cons a ·)]
+  induction n with
+  | zero => exact congrArg f (Subsingleton.allEq _ _)
+  | succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))
 
-/-- `Equiv.curry` for n-ary functions. -/
+/-- `Equiv.curry` for `p`-ary heterogeneous functions. -/
 @[simps]
-def curryEquiv (n : ℕ) : ((Fin n → α) → β) ≃ OfArity α β n where
+def curryEquiv (p : Fin n → Type u) : (((i : Fin n) → p i) → τ) ≃ FromTypes p τ where
   toFun := curry
   invFun := uncurry
   left_inv := uncurry_curry
   right_inv := curry_uncurry
 
+lemma curry_two_eq_curry {p : Fin 2 → Type u} {τ : Type u}
+    (f : ((i : Fin 2) → p i) → τ) :
+    curry f = Function.curry (f ∘ (piFinTwoEquiv p).symm) := rfl
+
+lemma uncurry_two_eq_uncurry (p : Fin 2 → Type u) (τ : Type u)
+    (f : Function.FromTypes p τ) :
+    uncurry f = Function.uncurry f ∘ piFinTwoEquiv p := rfl
+
+end Function.FromTypes
+
+namespace Function.OfArity
+
+variable {α β : Type u}
+
+/-- Uncurry all the arguments of `Function.OfArity α n` to get a function from a tuple.
+
+Note this can be used on raw functions if used. -/
+def uncurry {n} (f : Function.OfArity α β n) : (Fin n → α) → β := FromTypes.uncurry f
+
+/-- Curry all the arguments of `Function.OfArity α β n` to get a function from a tuple. -/
+def curry {n} (f : (Fin n → α) → β) : Function.OfArity α β n := FromTypes.curry f
+
+@[simp]
+theorem curry_uncurry {n} (f : Function.OfArity α β n) :
+    curry (uncurry f) = f := FromTypes.curry_uncurry f
+
+@[simp]
+theorem uncurry_curry {n} (f : (Fin n → α) → β) :
+    uncurry (curry f) = f := FromTypes.uncurry_curry f
+
+/-- `Equiv.curry` for n-ary functions. -/
+@[simps!]
+def curryEquiv (n : ℕ) : ((Fin n → α) → β) ≃ OfArity α β n :=
+  FromTypes.curryEquiv _
+
+lemma curry_two_eq_curry {α β : Type u} (f : ((i : Fin 2) → α) → β) :
+    curry f = Function.curry (f ∘ (finTwoArrowEquiv α).symm) :=
+  FromTypes.curry_two_eq_curry f
+
+lemma uncurry_two_eq_uncurry {α β : Type u} (f : OfArity α β 2) :
+    uncurry f = Function.uncurry f ∘ (finTwoArrowEquiv α) :=
+  FromTypes.uncurry_two_eq_uncurry _ _ f
+
 end Function.OfArity

Mathlib/Logic/Function/FromTypes.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 Brendan Murphy. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Brendan Murphy
+-/
+
+import Mathlib.Data.Fin.VecNotation
+
+/-! # Function types of a given heterogeneous arity
+
+This provides `Function.FromTypes`, such that `FromTypes ![α, β] τ = α → β → τ`.
+Note that it is often preferable to use `((i : Fin n) → p i) → τ` in place of `FromTypes p τ`.
+
+## Main definitions
+
+* `Function.FromTypes p τ`: `n`-ary function `p 0 → p 1 → ... → p (n - 1) → β`.
+-/
+
+universe u
+
+namespace Function
+
+open Matrix (vecCons vecHead vecTail vecEmpty)
+
+/-- The type of `n`-ary functions `p 0 → p 1 → ... → p (n - 1) → τ`. -/
+def FromTypes : {n : ℕ} → (Fin n → Type u) → Type u → Type u
+  | 0    , _, τ => τ
+  | n + 1, p, τ => vecHead p → @FromTypes n (vecTail p) τ
+
+theorem fromTypes_zero (p : Fin 0 → Type u) (τ : Type u) : FromTypes p τ = τ := rfl
+
+theorem fromTypes_nil (τ : Type u) : FromTypes ![] τ = τ := fromTypes_zero ![] τ
+
+-- prefer `fromTypes_cons` when it (syntactically) applies
+theorem fromTypes_succ {n} (p : Fin (n + 1) → Type u) (τ : Type u) :
+    FromTypes p τ = (vecHead p → FromTypes (vecTail p) τ) := rfl
+
+theorem fromTypes_cons {n} (α : Type u) (p : Fin n → Type u) (τ : Type u) :
+    FromTypes (vecCons α p) τ = (α → FromTypes p τ) := fromTypes_succ _ τ
+
+/-- The definitional equality between `0`-ary heterogeneous functions into `τ` and `τ`. -/
+@[simps!]
+def fromTypes_zero_equiv (p : Fin 0 → Type u) (τ : Type u) :
+    FromTypes p τ ≃ τ := Equiv.refl _
+
+/-- The definitional equality between `![]`-ary heterogeneous functions into `τ` and `τ`. -/
+@[simps!]
+def fromTypes_nil_equiv (τ : Type u) : FromTypes ![] τ ≃ τ :=
+  fromTypes_zero_equiv ![] τ
+
+/-- The definitional equality between `p`-ary heterogeneous functions into `τ`
+  and function from `vecHead p` to `(vecTail p)`-ary heterogeneous functions into `τ`. -/
+@[simps!]
+def fromTypes_succ_equiv {n} (p : Fin (n + 1) → Type u) (τ : Type u) :
+    FromTypes p τ ≃ (vecHead p → FromTypes (vecTail p) τ) := Equiv.refl _
+
+/-- The definitional equality between `(vecCons α p)`-ary heterogeneous functions into `τ`
+  and function from `α` to `p`-ary heterogeneous functions into `τ`. -/
+@[simps!]
+def fromTypes_cons_equiv {n} (α : Type u) (p : Fin n → Type u) (τ : Type u) :
+    FromTypes (vecCons α p) τ ≃ (α → FromTypes p τ) := fromTypes_succ_equiv _ _
+
+namespace FromTypes
+
+/-- Constant `n`-ary function with value `t`. -/
+def const : {n : ℕ} → (p : Fin n → Type u) → {τ : Type u} → (t : τ) → FromTypes p τ
+  | 0,     _, _, t => t
+  | n + 1, p, τ, t => fun _ => @const n (vecTail p) τ t
+
+@[simp]
+theorem const_zero (p : Fin 0 → Type u) {τ : Type u} (t : τ) : const p t = t :=
+  rfl
+
+@[simp]
+theorem const_succ {n} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) :
+    const p t = fun _ => const (vecTail p) t := rfl
+
+theorem const_succ_apply {n} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ)
+    (x : p 0) : const p t x = const (vecTail p) t := rfl
+
+instance FromTypes.inhabited {n} {p : Fin n → Type u} {τ} [Inhabited τ] :
+    Inhabited (FromTypes p τ) := ⟨const p default⟩
+
+end FromTypes
+
+end Function

Mathlib/Logic/Function/OfArity.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
-import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Mathport.Rename
+import Mathlib.Logic.Function.FromTypes
 
 /-! # Function types of a given arity
 
@@ -26,49 +26,56 @@ namespace Function
 
 Note that this is not universe polymorphic, as this would require that when `n=0` we produce either
 `Unit → β` or `ULift β`. -/
-def OfArity (α β : Type u) : ℕ → Type u
-  | 0 => β
-  | n + 1 => α → OfArity α β n
+abbrev OfArity (α β : Type u) (n : ℕ) : Type u := FromTypes (fun (_ : Fin n) => α) β
 #align arity Function.OfArity
 
 @[simp]
-theorem ofArity_zero (α β : Type u) : OfArity α β 0 = β :=
-  rfl
+theorem ofArity_zero (α β : Type u) : OfArity α β 0 = β := fromTypes_zero _ _
 #align arity_zero Function.ofArity_zero
 
 @[simp]
-theorem ofArity_succ (α β : Type u) (n : ℕ) : OfArity α β n.succ = (α → OfArity α β n) :=
-  rfl
+theorem ofArity_succ (α β : Type u) (n : ℕ) :
+    OfArity α β n.succ = (α → OfArity α β n) := fromTypes_succ _ _
 #align arity_succ Function.ofArity_succ
 
 namespace OfArity
 
-/-- Constant `n`-ary function with value `a`. -/
-def const (α : Type u) {β : Type u} (b : β) : ∀ n, OfArity α β n
-  | 0 => b
-  | n + 1 => fun _ => const _ b n
+/-- Constant `n`-ary function with value `b`. -/
+def const (α : Type u) {β : Type u} (b : β) (n : ℕ) : OfArity α β n :=
+  FromTypes.const (fun _ => α) b
 #align arity.const Function.OfArity.const
 
 @[simp]
 theorem const_zero (α : Type u) {β : Type u} (b : β) : const α b 0 = b :=
-  rfl
+  FromTypes.const_zero (fun _ => α) b
 #align arity.const_zero Function.OfArity.const_zero
 
 @[simp]
 theorem const_succ (α : Type u) {β : Type u} (b : β) (n : ℕ) :
     const α b n.succ = fun _ => const _ b n :=
-  rfl
+  FromTypes.const_succ (fun _ => α) b
 #align arity.const_succ Function.OfArity.const_succ
 
 theorem const_succ_apply (α : Type u) {β : Type u} (b : β) (n : ℕ) (x : α) :
-    const α b n.succ x = const _ b n :=
-  rfl
+    const α b n.succ x = const _ b n := FromTypes.const_succ_apply _ b x
 #align arity.const_succ_apply Function.OfArity.const_succ_apply
 
 instance OfArity.inhabited {α β n} [Inhabited β] : Inhabited (OfArity α β n) :=
-  ⟨const _ default _⟩
+  inferInstanceAs (Inhabited (FromTypes (fun _ => α) β))
 #align arity.arity.inhabited Function.OfArity.OfArity.inhabited
 
 end OfArity
 
+namespace FromTypes
+
+lemma fromTypes_fin_const (α β : Type u) (n : ℕ) :
+    FromTypes (fun (_ : Fin n) => α) β = OfArity α β n := rfl
+
+/-- The definitional equality between heterogeneous functions with constant
+domain and `n`-ary functions with that domain. -/
+def fromTypes_fin_const_equiv (α β : Type u) (n : ℕ) :
+    FromTypes (fun (_ : Fin n) => α) β ≃ OfArity α β n := .refl _
+
+end FromTypes
+
 end Function

Mathlib/SetTheory/ZFC/Basic.lean

@@ -618,7 +618,7 @@ noncomputable def allDefinable : ∀ {n} (F : OfArity ZFSet ZFSet n), Definable
     let p := @Quotient.exists_rep PSet _ F
     @Definable.EqMk 0 ⟨choose p, Equiv.rfl⟩ _ (choose_spec p)
   | n + 1, (F : OfArity ZFSet ZFSet (n + 1)) => by
-    have I := fun x => allDefinable (F x)
+    have I : (x : ZFSet) → Definable (Nat.add n 0) (F x) := fun x => allDefinable (F x)
     refine' @Definable.EqMk (n + 1) ⟨fun x : PSet => (@Definable.Resp _ _ (I ⟦x⟧)).1, _⟩ _ _
     · dsimp [Arity.Equiv]
       intro x y h
@@ -1330,7 +1330,7 @@ theorem mem_funs {x y f : ZFSet.{u}} : f ∈ funs x y ↔ IsFunc x y f := by sim
    suggests it shouldn't be. -/
 @[nolint unusedArguments]
 noncomputable instance mapDefinableAux (f : ZFSet → ZFSet) [Definable 1 f] :
-    Definable 1 fun y => pair y (f y) :=
+    Definable 1 fun (y : ZFSet) => pair y (f y) :=
   @Classical.allDefinable 1 _
 #align Set.map_definable_aux ZFSet.mapDefinableAux