Inductive types vs structures for unknown vector functions

Stream: new members

[Plamen Dimitrov]

Hi all, I need to define an unknown rq quantity that will either produce a given vector output (as a property) or produce vector outputs based on a rule (alternative property to build propositions from). I can achieve this with both structures like

import Mathlib

structure Rq (y₁ y₂ x: Fin C) where
  val : Fin C → ℚ

def rq_rule (C : ℕ) : Type := Fin C → Fin C → Fin C → Fin C → ℚ
structure RqFromRule (y₁ y₂ x: Fin C) (f: rq_rule C) where
  val : Rq y₁ y₂ x := ⟨f y₁ y₂ x⟩

/--An unknown rq quantity that will produce a given vector output.-/
def rq0 (y₁ y₂ x: Fin C) (v: Fin C → ℚ) := (⟨v⟩: Rq y₁ y₂ x).val
/--An unknown rq quantity that will produce vector outputs based on a function rule.-/
def rq (y₁ y₂ x: Fin C) (f: rq_rule C) := (⟨(⟨f y₁ y₂ x⟩: Rq y₁ y₂ x)⟩: RqFromRule y₁ y₂ x f).val.val

def zero_lemma (k: Fin C) (y x: Fin C) (f: rq_rule C) : Prop := rq y y x f k = 0

or via inductive types like

import Mathlib

inductive Rq (y₁ y₂ x : Fin C) : Type where
  | mk : (Fin C → ℚ) → Rq y₁ y₂ x
def Rq.val {y₁ y₂ x : Fin C} (rq : Rq y₁ y₂ x) : Fin C → ℚ :=
  match rq with
  | .mk f => f

def rq_rule (C : ℕ) : Type := Fin C → Fin C → Fin C → Fin C → ℚ
inductive RqFromRule (y₁ y₂ x: Fin C) (f: rq_rule C) : Type where
  | mk : RqFromRule y₁ y₂ x f
def RqFromRule.val {y₁ y₂ x : Fin C} {f : rq_rule C} (rq : RqFromRule y₁ y₂ x f) : Fin C → ℚ :=
  match rq with
  | .mk => f y₁ y₂ x

/--An unknown rq quantity that will produce a given vector output.-/
def rq0 (y₁ y₂ x : Fin C) (v : Fin C → ℚ) := Rq.val (Rq.mk v : Rq y₁ y₂ x)
/--An unknown rq quantity that will produce vector outputs based on a function rule.-/
def rq (y₁ y₂ x : Fin C) (f : rq_rule C) := RqFromRule.val (RqFromRule.mk : RqFromRule y₁ y₂ x f)

def zero_lemma (k : Fin C) (y x: Fin C) (f : rq_rule C) : Prop := rq y y x f k = 0

Are there any pros and cons for using one versus the other? Structures for instance might require some ⟨...⟩ unpacking and repacking while inductive types bring in their own syntax overhead. Are there any significant advantages of either method you could recommend?

[Robin Arnez]

structures are inductive types + some additional functions. In other words, everything you'd find from inductive types (Rq.mk, matches) are present on structures and most things from structures (.1, ⟨x⟩) are also present on inductive types of the right shape. So, since structures are just strictly more than inductives (bringing the { val := _ } syntax and projection functions), I'd just go with structures.