class DY.ALaCarte.FunctorSizeOf (f : Type → Type) : Type 1

Compute the sum of sizeOf on the t contained by Functor. This is needed to prove Representable.sizeOf_eq.

• sizeOf {t : Type} [SizeOf t] : f t → Nat

class DY.ALaCarte.SubFunctor (f : Type → Type) (g : semiOutParam (Type → Type)) [FunctorSizeOf f] [semiOutParam (FunctorSizeOf g)] : Type 1

• inj {a : Type} : f a → g a
• proj {a : Type} : g a → Option (f a)
• proj_inj {a : Type} (x : f a) : proj (inj x) = some x
• inj_proj {a : Type} (x : g a) : match proj x with | some y => inj y = x | none => True
• sizeOf_inj {a : Type} [SizeOf a] (x : f a) : FunctorSizeOf.sizeOf (inj x) = FunctorSizeOf.sizeOf x

class DY.ALaCarte.SubFunctorTC (f g : Type → Type) [FunctorSizeOf f] [FunctorSizeOf g] : Type 1

• inj {a : Type} : f a → g a
• proj {a : Type} : g a → Option (f a)
• proj_inj {a : Type} (x : f a) : proj (inj x) = some x
• inj_proj {a : Type} (x : g a) : match proj x with | some y => inj y = x | none => True
• sizeOf_inj {a : Type} [SizeOf a] (x : f a) : FunctorSizeOf.sizeOf (inj x) = FunctorSizeOf.sizeOf x

@[instance_reducible]

instance DY.ALaCarte.instSubFunctorTC (f : Type → Type) [FunctorSizeOf f] : SubFunctorTC f f

Equations

• DY.ALaCarte.instSubFunctorTC f = { inj := fun {a : Type} (x : f a) => x, proj := fun {a : Type} (x : f a) => some x, proj_inj := ⋯, inj_proj := ⋯, sizeOf_inj := ⋯ }

@[instance_reducible]

instance DY.ALaCarte.instSubFunctorTCOfSubFunctor {f g h : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [FunctorSizeOf h] [SubFunctor f g] [SubFunctorTC g h] : SubFunctorTC f h

Equations

• One or more equations did not get rendered due to their size.

structure DY.ALaCarte.Ctor : Type 1

A constructor of a functor / an inductive is characterized by the fixed types it contains, and the number of time it recurses. For example, the constructor

| foo: Nat → String → α → α → MyFunctor α

of a functor, or equivalently the constructor

| foo: Nat → String → MyInductive → MyInductive → MyInductive

of an inductive is described by the Ctor

{ Data := Nat × String nRec := 2 }

• Data : Type
• nRec : Nat

@[reducible, inline]

abbrev DY.ALaCarte.Ctors (CtorId : Type) : Type 1

Equations

• DY.ALaCarte.Ctors CtorId = (CtorId → DY.ALaCarte.Ctor)

structure DY.ALaCarte.FunctorRepr {CtorId : Type} (ctors : Ctors CtorId) (a : Type) : Type

• id : CtorId
• data : (ctors self.id).Data
• as : Vector a (ctors self.id).nRec

@[instance_reducible]

noncomputable instance DY.ALaCarte.instFunctorSizeOfFunctorRepr {CtorId : Type} (ctors : Ctors CtorId) : FunctorSizeOf (FunctorRepr ctors)

Equations

• One or more equations did not get rendered due to their size.

class DY.ALaCarte.Representable (f : Type → Type) [FunctorSizeOf f] : Type 1

A functor is "representable" when there exists a set of Ctor such that the functor is isomorphic to FunctorRepr with this set of Ctor.

• CtorId : Type
• ctors : Ctors (CtorId f)
• toRepr {a : Type} : f a → FunctorRepr ctors a
• fromRepr {a : Type} : FunctorRepr ctors a → f a
• from_to {a : Type} (x : f a) : fromRepr (toRepr x) = x
• to_from {a : Type} (x : FunctorRepr ctors a) : toRepr (fromRepr x) = x
• sizeOf_eq {a : Type} [SizeOf a] (x : f a) : FunctorSizeOf.sizeOf x = FunctorSizeOf.sizeOf (toRepr x)

structure DY.ALaCarte.BareContainer {CtorId : Type} (ctors : Ctors CtorId) : Type

• id : CtorId
• data : (ctors self.id).Data
• as : Array (BareContainer ctors)

@[irreducible]

def DY.ALaCarte.BareContainer.wf {CtorId : Type} {ctors : Ctors CtorId} (x : BareContainer ctors) : Prop

Equations

• x.wf = (x.as.size = (ctors x.id).nRec ∧ ∀ (y : DY.ALaCarte.BareContainer ctors), y ∈ x.as → y.wf)

@[reducible, inline]

abbrev DY.ALaCarte.Container {CtorId : Type} (ctors : Ctors CtorId) : Type

Container ctors is a type that is, by construction, isomorphic to FunctorRepr ctors (Container ctors).

Equations

• DY.ALaCarte.Container ctors = Subtype DY.ALaCarte.BareContainer.wf

@[reducible, inline]

abbrev DY.ALaCarte.ContainerFor (f : Type → Type) [FunctorSizeOf f] [Representable f] : Type

When a functor is Representable, we can use ContainerFor as a shorthand for Container. It has the property that ContainerFor f is isomorphic to f (ContainerFor f):

ContainerFor f

= Container ctors [by unfolding ContainerFor] ≅ FunctorRepr ctors (Container ctors) [by property of Container] = FunctorRepr ctors (ContainerFor f) [by refolding ContainerFor] ≅ f (ContainerFor f) [by f being Representable]

Equations

• DY.ALaCarte.ContainerFor f = DY.ALaCarte.Container DY.ALaCarte.Representable.ctors

structure DY.ALaCarte.FunctorUnion {a : Type} (Functors : a → Type → Type) (t : Type) : Type

When we have a collection of functors, we can create the union using FunctorUnion. Such an union is representable, and each functor will then be a sub-functor of this union.

• id : a
• val : Functors self.id t

structure DY.ALaCarte.FunctorUnion.CtorId {a : Type} (Functors : a → Type → Type) [(id : a) → FunctorSizeOf (Functors id)] [(id : a) → Representable (Functors id)] : Type

• idHead : a
• idTail : Representable.CtorId (Functors self.idHead)

@[instance_reducible]

instance DY.ALaCarte.instFunctorSizeOfFunctorUnion {a : Type} (Functors : a → Type → Type) [(id : a) → FunctorSizeOf (Functors id)] : FunctorSizeOf (FunctorUnion Functors)

Equations

• DY.ALaCarte.instFunctorSizeOfFunctorUnion Functors = { sizeOf := fun {t : Type} [SizeOf t] (x : DY.ALaCarte.FunctorUnion Functors t) => DY.ALaCarte.FunctorSizeOf.sizeOf x.val }

@[instance_reducible]

instance DY.ALaCarte.instRepresentableFunctorUnion {a : Type} (Functors : a → Type → Type) [(id : a) → FunctorSizeOf (Functors id)] [(id : a) → Representable (Functors id)] : Representable (FunctorUnion Functors)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.ALaCarte.instSubFunctorFunctorUnionOfDecidableEq {a : Type} [DecidableEq a] (Functors : a → Type → Type) [(id : a) → FunctorSizeOf (Functors id)] (id : a) : SubFunctor (Functors id) (FunctorUnion Functors)

Equations

• One or more equations did not get rendered due to their size.

def DY.ALaCarte.Container.pack (f : Type → Type) {g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [SubFunctorTC f g] [Representable g] (x : f (ContainerFor g)) : ContainerFor g

Equations

• DY.ALaCarte.Container.pack f x = DY.ALaCarte.Container.fromFunctor✝ (DY.ALaCarte.Representable.toRepr (DY.ALaCarte.SubFunctorTC.inj x))

def DY.ALaCarte.Container.view (f : Type → Type) {g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [SubFunctorTC f g] [Representable g] (x : ContainerFor g) : Option (f (ContainerFor g))

Equations

• DY.ALaCarte.Container.view f x = DY.ALaCarte.SubFunctorTC.proj (DY.ALaCarte.Representable.fromRepr (DY.ALaCarte.Container.intoFunctor✝ x))

theorem DY.ALaCarte.Container.view_pack (f : Type → Type) {g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [SubFunctorTC f g] [Representable g] (x : f (ContainerFor g)) : view f (pack f x) = some x

theorem DY.ALaCarte.Container.pack_view (f : Type → Type) {g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [SubFunctorTC f g] [Representable g] (x : ContainerFor g) : match view f x with | none => True | some y => pack f y = x

theorem DY.ALaCarte.Container.sizeOf_pack (f : Type → Type) {g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [SubFunctorTC f g] [Representable g] (x : f (ContainerFor g)) : FunctorSizeOf.sizeOf x ≤ sizeOf (pack f x)

theorem DY.ALaCarte.Container.sizeOf_view (f : Type → Type) {g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [SubFunctorTC f g] [Representable g] (x : ContainerFor g) : match view f x with | none => True | some y => FunctorSizeOf.sizeOf y ≤ sizeOf x

@[reducible, inline]

abbrev DY.ALaCarte.Container.PartialFunDep (f : Type → Type) {g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [Representable g] [SubFunctorTC f g] (motive : ContainerFor g → Sort u) : Sort u

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DY.ALaCarte.Container.PartialFun (f g : Type → Type) [FunctorSizeOf f] [FunctorSizeOf g] [Representable g] (a : Type) : Type

Equations

• DY.ALaCarte.Container.PartialFun f g a = ((x : f (DY.ALaCarte.ContainerFor g)) → ((y : DY.ALaCarte.ContainerFor g) → sizeOf y ≤ DY.ALaCarte.FunctorSizeOf.sizeOf x → a) → a)

@[irreducible]

def DY.ALaCarte.Container.rec {f : Type → Type} [FunctorSizeOf f] [Representable f] {motive : ContainerFor f → Sort u} (pf : PartialFunDep f motive) (x : ContainerFor f) : motive x

Generic recursion principle on Container. This allows to define functions, predicates, and to do proofs.

Equations

• One or more equations did not get rendered due to their size.

class DY.ALaCarte.SubPartialFun {f g h : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [FunctorSizeOf h] [Representable h] [SubFunctor f g] {a : Type} (f1 : Container.PartialFun f h a) (f2 : semiOutParam (Container.PartialFun g h a)) : Prop

• pf (x : f (ContainerFor h)) (rec : (y : ContainerFor h) → sizeOf y ≤ FunctorSizeOf.sizeOf x → a) : f1 x rec = f2 (SubFunctor.inj x) fun (y : ContainerFor h) (h_1 : sizeOf y ≤ FunctorSizeOf.sizeOf (SubFunctor.inj x)) => rec y ⋯

class DY.ALaCarte.SubPartialFunTC {f g h : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [FunctorSizeOf h] [Representable h] [SubFunctorTC f g] {a : Type} (f1 : Container.PartialFun f h a) (f2 : Container.PartialFun g h a) : Prop

• pf (x : f (ContainerFor h)) (rec : (y : ContainerFor h) → sizeOf y ≤ FunctorSizeOf.sizeOf x → a) : f1 x rec = f2 (SubFunctorTC.inj x) fun (y : ContainerFor h) (h_1 : sizeOf y ≤ FunctorSizeOf.sizeOf (SubFunctorTC.inj x)) => rec y ⋯

instance DY.ALaCarte.instSubPartialFunTC {f : Type → Type} [FunctorSizeOf f] [Representable f] {a : Type} (f✝ : Container.PartialFun f f a) : SubPartialFunTC f✝ f✝

instance DY.ALaCarte.instSubPartialFunTCOfSubPartialFun {f g h i : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [FunctorSizeOf h] [FunctorSizeOf i] [Representable i] [SubFunctor f g] [SubFunctorTC g h] {a : Type} (f1 : Container.PartialFun f i a) (f2 : Container.PartialFun g i a) (f3 : Container.PartialFun h i a) [SubPartialFun f1 f2] [SubPartialFunTC f2 f3] : SubPartialFunTC f1 f3

theorem DY.ALaCarte.Container.rec_eq {f g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [SubFunctorTC f g] [Representable g] {a : Type} (partialFun : PartialFun f g a) (totalFun : PartialFun g g a) [SubPartialFunTC partialFun totalFun] (x : f (ContainerFor g)) : rec totalFun (pack f x) = partialFun x fun (y : ContainerFor g) (x : sizeOf y ≤ FunctorSizeOf.sizeOf x) => rec totalFun y

def DY.ALaCarte.Container.PartialFun.combine {t : Type} [DecidableEq t] {functors : t → Type → Type} [(id : t) → FunctorSizeOf (functors id)] {g : Type → Type} [FunctorSizeOf g] [Representable g] {a : Type} (funs : (id : t) → PartialFun (functors id) g a) : PartialFun (FunctorUnion functors) g a

Equations

• DY.ALaCarte.Container.PartialFun.combine funs { id := id, val := val } rec_2 = funs id val rec_2

def DY.ALaCarte.Container.PartialFunDep.combine {t : Type} [DecidableEq t] {functors : t → Type → Type} [(id : t) → FunctorSizeOf (functors id)] {g : Type → Type} [FunctorSizeOf g] [Representable g] [SubFunctorTC (FunctorUnion functors) g] {motive : ContainerFor g → Sort u} (funs : (id : t) → PartialFunDep (functors id) motive) : PartialFunDep (FunctorUnion functors) motive

Equations

• DY.ALaCarte.Container.PartialFunDep.combine funs { id := id, val := val } rec_2 = funs id val rec_2

instance DY.ALaCarte.instSubPartialFunFunctorUnionCombine {t : Type} [DecidableEq t] {functors : t → Type → Type} [(id : t) → FunctorSizeOf (functors id)] {g : Type → Type} [FunctorSizeOf g] [Representable g] {a : Type} (funs : (id : t) → Container.PartialFun (functors id) g a) (id : t) : SubPartialFun (funs id) (Container.PartialFun.combine funs)

def DY.ALaCarte.Container.PartialProof1 {f g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [Representable g] {a : Type} (fn : PartialFun f g a) (rec : ContainerFor g → a) (p : a → Prop) : Prop

Helper to write a modular proof on one modular function

Equations

• One or more equations did not get rendered due to their size.

theorem DY.ALaCarte.Container.PartialProof1.into {f : Type → Type} [FunctorSizeOf f] [Representable f] {a : Type} {fn : PartialFun f f a} {p : a → Prop} (pf : PartialProof1 fn (rec fn) p) : PartialFunDep f fun (x : ContainerFor f) => p (rec fn x)

theorem DY.ALaCarte.Container.PartialProof1.combine {t : Type} [DecidableEq t] {functors : t → Type → Type} [(id : t) → FunctorSizeOf (functors id)] {g : Type → Type} [FunctorSizeOf g] [Representable g] {a : Type} {rec : ContainerFor g → a} {p : a → Prop} {funs : (id : t) → PartialFun (functors id) g a} (pfs : ∀ (id : t), PartialProof1 (funs id) rec p) : PartialProof1 (PartialFun.combine funs) rec p

def DY.ALaCarte.Container.PartialProof2 {f g : Type → Type} [FunctorSizeOf f] [FunctorSizeOf g] [Representable g] {a b : Type} (fn1 : PartialFun f g a) (fn2 : PartialFun f g b) (rec1 : ContainerFor g → a) (rec2 : ContainerFor g → b) (p : a × b → Prop) : Prop

Helper to write a modular proof on two modular functions

Equations

• One or more equations did not get rendered due to their size.

theorem DY.ALaCarte.Container.PartialProof2.into {f : Type → Type} [FunctorSizeOf f] [Representable f] {a b : Type} {fn1 : PartialFun f f a} {fn2 : PartialFun f f b} {p : a × b → Prop} (pf : PartialProof2 fn1 fn2 (rec fn1) (rec fn2) p) : PartialFunDep f fun (x : ContainerFor f) => p (rec fn1 x, rec fn2 x)

theorem DY.ALaCarte.Container.PartialProof2.combine {t : Type} [DecidableEq t] {functors : t → Type → Type} [(id : t) → FunctorSizeOf (functors id)] {g : Type → Type} [FunctorSizeOf g] [Representable g] {a b : Type} {rec1 : ContainerFor g → a} {rec2 : ContainerFor g → b} {p : a × b → Prop} {funs1 : (id : t) → PartialFun (functors id) g a} {funs2 : (id : t) → PartialFun (functors id) g b} (pfs : ∀ (id : t), PartialProof2 (funs1 id) (funs2 id) rec1 rec2 p) : PartialProof2 (PartialFun.combine funs1) (PartialFun.combine funs2) rec1 rec2 p