prod

Prod.assocFwd

def assocFwd {A B C : Type} (p : A × (B × C)) : (A × B) × C

Reassociates a right-nested triple A × (B × C) into the left-nested (A × B) × C.

Prod.assocBwd

def assocBwd {A B C : Type} (p : (A × B) × C) : A × (B × C)

Reassociates a left-nested triple (A × B) × C into the right-nested A × (B × C).

Prod.swap

def swap {A B : Type} (p : A × B) : B × A

Swaps the two components of a pair.

Prod.mapFst

def mapFst {A B C : Type} (f : A -> C) (p : A × B) : C × B

Applies a function to the first component of a pair, keeping the second.

Prod.mapSnd

def mapSnd {A B D : Type} (g : B -> D) (p : A × B) : A × D

Applies a function to the second component of a pair, keeping the first.

Prod.prodSwapSwap

theorem prodSwapSwap {A B : Type} (p : A × B) : Prod.swap (Prod.swap p) = p

Swapping a pair twice gives back the original pair.

Prod.prodAssocFwdBwd

theorem prodAssocFwdBwd {A B C : Type} (p : A × (B × C)) : Prod.assocBwd (Prod.assocFwd p) = p

Reassociating right-to-left and back is the identity on right-nested triples.

Prod.prodAssocBwdFwd

theorem prodAssocBwdFwd {A B C : Type} (p : (A × B) × C) : Prod.assocFwd (Prod.assocBwd p) = p

Reassociating left-to-right and back is the identity on left-nested triples.

Prod.prodMapFstId

theorem prodMapFstId {A B : Type} (p : A × B) : Prod.mapFst (fun (a : A) => a) p = p

Mapping the identity over the first component leaves a pair unchanged.

Prod.prodMapSndId

theorem prodMapSndId {A B : Type} (p : A × B) : Prod.mapSnd (fun (b : B) => b) p = p

Mapping the identity over the second component leaves a pair unchanged.

Prod.prodMapCompose

theorem prodMapCompose {A B C D E F : Type} (f1 : A -> C) (f2 : C -> E) (g1 : B -> D) (g2 : D -> F) (p : A × B) : prodMap f2 g2 (prodMap f1 g1 p) = prodMap (fun (a : A) => f2 (f1 a)) (fun (b : B) => g2 (g1 b)) p

Mapping over a pair twice equals mapping once with the composed functions.

Prod.pairEta

theorem pairEta {A B : Type} (p : A × B) : (fst p, snd p) = p

Eta for pairs: rebuilding a pair from its projections gives the same pair.

Prod.curry

def curry {A B C : Type} (f : A × B -> C) (a : A) (b : B) : C

Curries a function on pairs into a two-argument function.

Prod.uncurry

def uncurry {A B C : Type} (f : A -> B -> C) (p : A × B) : C

Uncurries a two-argument function into a function on pairs.

Prod.diag

def diag {A : Type} (a : A) : A × A

Diagonal map: duplicates a value into a pair.

Prod.constFst

def constFst {A B : Type} (p : A × B) : A

First projection of a pair, as a named function.

Prod.constSnd

def constSnd {A B : Type} (p : A × B) : B

Second projection of a pair, as a named function.

Prod.bimap

def bimap {A B C D : Type} (f : A -> C) (g : B -> D) (p : A × B) : C × D

Applies one function to each component of a pair (same as prodMap).

Prod.apply

def apply {A B C D : Type} (fg : (A -> C) × (B -> D)) (p : A × B) : C × D

Applies a pair of functions componentwise to a pair of arguments.

Prod.fanout

def fanout {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : B × C

Applies two functions to the same input and pairs the results.

Prod.dup

def dup {A B : Type} (f : A -> B) (p : A × A) : B × B

Applies one function to both components of a homogeneous pair.

Prod.flip

def flip {A B C : Type} (f : A × B -> C) (p : B × A) : C

Turns a function on A × B into a function on B × A by swapping the input.

Prod.id

def id {A B : Type} (p : A × B) : A × B

Identity function on pairs.

Prod.composeFst

def composeFst {A B C : Type} (f : B -> C) (p : A × B) : A × C

Applies a function to the second component of a pair, keeping the first.

Prod.composeSnd

def composeSnd {A B C : Type} (f : A -> C) (p : A × B) : C × B

Applies a function to the first component of a pair, keeping the second.

Prod.nestRight

def nestRight {A B C : Type} (a : A) (b : B) (c : C) : A × (B × C)

Builds a right-nested triple A × (B × C) from three values.

Prod.nestLeft

def nestLeft {A B C : Type} (a : A) (b : B) (c : C) : (A × B) × C

Builds a left-nested triple (A × B) × C from three values.

Prod.strengthL

def strengthL {A B : Type} (a : A) (b : B) : A × B

Pairs a value with a fixed first component (the plain pair constructor).

Prod.strengthR

def strengthR {A B : Type} (a : A) (b : B) : A × B

Pairs a value with a fixed second component (the plain pair constructor).

Prod.distribFst

def distribFst {A B C : Type} (f : A -> B -> C) (p : A × B) : C

Applies a two-argument function to the components of a pair.

Prod.prodCurryCompute

theorem prodCurryCompute {A B C : Type} (f : A × B -> C) (a : A) (b : B) : Prod.curry f a b = f (a, b)

Prod.curry f a b computes to f (a, b).

Prod.prodUncurryCompute

theorem prodUncurryCompute {A B C : Type} (f : A -> B -> C) (a : A) (b : B) : Prod.uncurry f (a, b) = f a b

Prod.uncurry f (a, b) computes to f a b.

Prod.prodCurryUncurry

theorem prodCurryUncurry {A B C : Type} (f : A -> B -> C) (a : A) (b : B) : Prod.curry (Prod.uncurry f) a b = f a b

Currying an uncurried function gives back the original function pointwise.

Prod.prodUncurryCurry

theorem prodUncurryCurry {A B C : Type} (f : A × B -> C) (a : A) (b : B) : Prod.uncurry (Prod.curry f) (a, b) = f (a, b)

Uncurrying a curried function gives back the original function on every pair.

Prod.prodDiagFst

theorem prodDiagFst {A : Type} (a : A) : fst (Prod.diag a) = a

The first component of the diagonal pair is the original value.

Prod.prodDiagSnd

theorem prodDiagSnd {A : Type} (a : A) : snd (Prod.diag a) = a

The second component of the diagonal pair is the original value.

Prod.prodDiagCompute

theorem prodDiagCompute {A : Type} (a : A) : Prod.diag a = (a, a)

Prod.diag a computes to (a, a).

Prod.prodSwapDiag

theorem prodSwapDiag {A : Type} (a : A) : Prod.swap (Prod.diag a) = Prod.diag a

Swapping a diagonal pair leaves it unchanged.

Prod.prodBimapCompute

theorem prodBimapCompute {A B C D : Type} (f : A -> C) (g : B -> D) (a : A) (b : B) : Prod.bimap f g (a, b) = (f a, g b)

Prod.bimap f g (a, b) computes to (f a, g b).

Prod.prodBimapId

theorem prodBimapId {A B : Type} (p : A × B) : Prod.bimap (fun (a : A) => a) (fun (b : B) => b) p = p

Prod.bimap with identity functions leaves a pair unchanged.

Prod.prodBimapCompose

theorem prodBimapCompose {A B C D E F : Type} (f1 : A -> C) (f2 : C -> E) (g1 : B -> D) (g2 : D -> F) (p : A × B) : Prod.bimap f2 g2 (Prod.bimap f1 g1 p) = Prod.bimap (fun (a : A) => f2 (f1 a)) (fun (b : B) => g2 (g1 b)) p

Applying Prod.bimap twice equals applying it once with the composed functions.

Prod.prodBimapEqProdMap

theorem prodBimapEqProdMap {A B C D : Type} (f : A -> C) (g : B -> D) (p : A × B) : Prod.bimap f g p = prodMap f g p

Prod.bimap agrees with prodMap.

Prod.prodFanoutCompute

theorem prodFanoutCompute {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : Prod.fanout f g a = (f a, g a)

Prod.fanout f g a computes to (f a, g a).

Prod.prodFanoutFst

theorem prodFanoutFst {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : fst (Prod.fanout f g a) = f a

The first component of Prod.fanout f g a is f a.

Prod.prodFanoutSnd

theorem prodFanoutSnd {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : snd (Prod.fanout f g a) = g a

The second component of Prod.fanout f g a is g a.

Prod.prodApplyCompute

theorem prodApplyCompute {A B C D : Type} (f : A -> C) (g : B -> D) (a : A) (b : B) : Prod.apply (f, g) (a, b) = (f a, g b)

Prod.apply (f, g) (a, b) computes to (f a, g b).

Prod.prodDupCompute

theorem prodDupCompute {A B : Type} (f : A -> B) (a1 : A) (a2 : A) : Prod.dup f (a1, a2) = (f a1, f a2)

Prod.dup f (a1, a2) computes to (f a1, f a2).

Prod.prodDupId

theorem prodDupId {A : Type} (p : A × A) : Prod.dup (fun (a : A) => a) p = p

Prod.dup with the identity leaves a pair unchanged.

Prod.prodFlipCompute

theorem prodFlipCompute {A B C : Type} (f : A × B -> C) (a : A) (b : B) : Prod.flip f (b, a) = f (a, b)

Prod.flip f on a swapped pair (b, a) computes to f (a, b).

Prod.prodIdCompute

theorem prodIdCompute {A B : Type} (p : A × B) : Prod.id p = p

Prod.id returns its argument.

Prod.prodNestRightCompute

theorem prodNestRightCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.nestRight a b c = (a, (b, c))

Prod.nestRight a b c computes to (a, (b, c)).

Prod.prodNestLeftCompute

theorem prodNestLeftCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.nestLeft a b c = ((a, b), c)

Prod.nestLeft a b c computes to ((a, b), c).

Prod.prodNestRightFst

theorem prodNestRightFst {A B C : Type} (a : A) (b : B) (c : C) : fst (Prod.nestRight a b c) = a

The first component of a right-nested triple is its first value.

Prod.prodNestLeftSnd

theorem prodNestLeftSnd {A B C : Type} (a : A) (b : B) (c : C) : snd (Prod.nestLeft a b c) = c

The second component of a left-nested triple is its last value.

Prod.prodDistribFstCompute

theorem prodDistribFstCompute {A B C : Type} (f : A -> B -> C) (a : A) (b : B) : Prod.distribFst f (a, b) = f a b

Prod.distribFst f (a, b) computes to f a b.

Prod.prodComposeFstCompute

theorem prodComposeFstCompute {A B C : Type} (f : B -> C) (a : A) (b : B) : Prod.composeFst f (a, b) = (a, f b)

Prod.composeFst f (a, b) computes to (a, f b).

Prod.prodComposeSndCompute

theorem prodComposeSndCompute {A B C : Type} (f : A -> C) (a : A) (b : B) : Prod.composeSnd f (a, b) = (f a, b)

Prod.composeSnd f (a, b) computes to (f a, b).

Prod.prodSwapMap

theorem prodSwapMap {A B C D : Type} (f : A -> C) (g : B -> D) (p : A × B) : Prod.swap (prodMap f g p) = prodMap g f (Prod.swap p)

Swapping after mapping equals mapping with the functions exchanged after swapping.

Prod.fstProdSwap

theorem fstProdSwap {A B : Type} (p : A × B) : fst (Prod.swap p) = snd p

The first component of a swapped pair is the original second component.

Prod.sndProdSwap

theorem sndProdSwap {A B : Type} (p : A × B) : snd (Prod.swap p) = fst p

The second component of a swapped pair is the original first component.

Prod.prodSwapPair

theorem prodSwapPair {A B : Type} (a : A) (b : B) : Prod.swap (a, b) = (b, a)

Prod.swap (a, b) computes to (b, a).

Prod.prodAssocFwdPair

theorem prodAssocFwdPair {A B C : Type} (a : A) (b : B) (c : C) : Prod.assocFwd (a, (b, c)) = ((a, b), c)

Prod.assocFwd (a, (b, c)) computes to ((a, b), c).

Prod.prodAssocBwdPair

theorem prodAssocBwdPair {A B C : Type} (a : A) (b : B) (c : C) : Prod.assocBwd ((a, b), c) = (a, (b, c))

Prod.assocBwd ((a, b), c) computes to (a, (b, c)).

Prod.prodMapFstCompose

theorem prodMapFstCompose {A B C D : Type} (f : A -> C) (g : C -> D) (p : A × B) : Prod.mapFst g (Prod.mapFst f p) = Prod.mapFst (fun (a : A) => g (f a)) p

Mapping the first component twice equals mapping it once with the composed function.

Prod.prodMapSndCompose

theorem prodMapSndCompose {A B C D : Type} (f : B -> C) (g : C -> D) (p : A × B) : Prod.mapSnd g (Prod.mapSnd f p) = Prod.mapSnd (fun (b : B) => g (f b)) p

Mapping the second component twice equals mapping it once with the composed function.

Prod.prodMapFstPair

theorem prodMapFstPair {A B C : Type} (f : A -> C) (a : A) (b : B) : Prod.mapFst f (a, b) = (f a, b)

Prod.mapFst f (a, b) computes to (f a, b).

Prod.prodMapSndPair

theorem prodMapSndPair {A B D : Type} (g : B -> D) (a : A) (b : B) : Prod.mapSnd g (a, b) = (a, g b)

Prod.mapSnd g (a, b) computes to (a, g b).

Prod.first

def first {A B C : Type} (p : A × (B × C)) : A

First component of a right-nested triple.

Prod.second

def second {A B C : Type} (p : A × (B × C)) : B

Second component of a right-nested triple.

Prod.third

def third {A B C : Type} (p : A × (B × C)) : C

Third component of a right-nested triple.

Prod.mkTriple

def mkTriple {A B C : Type} (a : A) (b : B) (c : C) : A × (B × C)

Builds a right-nested triple from three values.

Prod.mapTriple

def mapTriple {A B C D E F : Type} (f : A -> D) (g : B -> E) (h : C -> F) (p : A × (B × C)) : D × (E × F)

Applies three functions componentwise to a right-nested triple.

Prod.swapTriple12

def swapTriple12 {A B C : Type} (p : A × (B × C)) : B × (A × C)

Swaps the first and second components of a right-nested triple.

Prod.swapTriple13

def swapTriple13 {A B C : Type} (p : A × (B × C)) : C × (B × A)

Swaps the first and third components of a right-nested triple.

Prod.swapTriple23

def swapTriple23 {A B C : Type} (p : A × (B × C)) : A × (C × B)

Swaps the second and third components of a right-nested triple.

Prod.replFst

def replFst {A B C : Type} (c : C) (p : A × B) : C × B

Replaces the first component of a pair with a given value.

Prod.replSnd

def replSnd {A B C : Type} (c : C) (p : A × B) : A × C

Replaces the second component of a pair with a given value.

Prod.zipWith

def zipWith {A B C D E F : Type} (f : A -> C -> E) (g : B -> D -> F) (p1 : A × B) (p2 : C × D) : E × F

Combines two pairs componentwise using one binary function per component.

Prod.const2

def const2 {A B : Type} (a : A) (b : B) : A × B

Pairs two given values (the plain pair constructor).

Prod.prodFirstCompute

theorem prodFirstCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.first (a, (b, c)) = a

Prod.first (a, (b, c)) computes to a.

Prod.prodSecondCompute

theorem prodSecondCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.second (a, (b, c)) = b

Prod.second (a, (b, c)) computes to b.

Prod.prodThirdCompute

theorem prodThirdCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.third (a, (b, c)) = c

Prod.third (a, (b, c)) computes to c.

Prod.prodMkTripleCompute

theorem prodMkTripleCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.mkTriple a b c = (a, (b, c))

Prod.mkTriple a b c computes to (a, (b, c)).

Prod.prodFirstMkTriple

theorem prodFirstMkTriple {A B C : Type} (a : A) (b : B) (c : C) : Prod.first (Prod.mkTriple a b c) = a

Prod.first of a triple built by Prod.mkTriple is its first value.

Prod.prodSecondMkTriple

theorem prodSecondMkTriple {A B C : Type} (a : A) (b : B) (c : C) : Prod.second (Prod.mkTriple a b c) = b

Prod.second of a triple built by Prod.mkTriple is its second value.

Prod.prodThirdMkTriple

theorem prodThirdMkTriple {A B C : Type} (a : A) (b : B) (c : C) : Prod.third (Prod.mkTriple a b c) = c

Prod.third of a triple built by Prod.mkTriple is its third value.

Prod.prodMapTripleCompute

theorem prodMapTripleCompute {A B C D E F : Type} (f : A -> D) (g : B -> E) (h : C -> F) (a : A) (b : B) (c : C) : Prod.mapTriple f g h (a, (b, c)) = (f a, (g b, h c))

Prod.mapTriple f g h applies each function to the matching component.

Prod.prodMapTripleId

theorem prodMapTripleId {A B C : Type} (p : A × (B × C)) : Prod.mapTriple (fun (a : A) => a) (fun (b : B) => b) (fun (c : C) => c) p = p

Prod.mapTriple with identity functions leaves a triple unchanged.

Prod.prodSwapTriple12Compute

theorem prodSwapTriple12Compute {A B C : Type} (a : A) (b : B) (c : C) : Prod.swapTriple12 (a, (b, c)) = (b, (a, c))

Prod.swapTriple12 (a, (b, c)) computes to (b, (a, c)).

Prod.prodSwapTriple13Compute

theorem prodSwapTriple13Compute {A B C : Type} (a : A) (b : B) (c : C) : Prod.swapTriple13 (a, (b, c)) = (c, (b, a))

Prod.swapTriple13 (a, (b, c)) computes to (c, (b, a)).

Prod.prodSwapTriple23Compute

theorem prodSwapTriple23Compute {A B C : Type} (a : A) (b : B) (c : C) : Prod.swapTriple23 (a, (b, c)) = (a, (c, b))

Prod.swapTriple23 (a, (b, c)) computes to (a, (c, b)).

Prod.prodReplFstCompute

theorem prodReplFstCompute {A B C : Type} (c : C) (a : A) (b : B) : Prod.replFst c (a, b) = (c, b)

Prod.replFst c (a, b) computes to (c, b).

Prod.prodReplSndCompute

theorem prodReplSndCompute {A B C : Type} (c : C) (a : A) (b : B) : Prod.replSnd c (a, b) = (a, c)

Prod.replSnd c (a, b) computes to (a, c).

Prod.fstReplFst

theorem fstReplFst {A B C : Type} (c : C) (p : A × B) : fst (Prod.replFst c p) = c

After replacing the first component, the first projection is the new value.

Prod.sndReplFst

theorem sndReplFst {A B C : Type} (c : C) (p : A × B) : snd (Prod.replFst c p) = snd p

Replacing the first component leaves the second component unchanged.

Prod.fstReplSnd

theorem fstReplSnd {A B C : Type} (c : C) (p : A × B) : fst (Prod.replSnd c p) = fst p

Replacing the second component leaves the first component unchanged.

Prod.sndReplSnd

theorem sndReplSnd {A B C : Type} (c : C) (p : A × B) : snd (Prod.replSnd c p) = c

After replacing the second component, the second projection is the new value.

Prod.prodZipWithCompute

theorem prodZipWithCompute {A B C D E F : Type} (f : A -> C -> E) (g : B -> D -> F) (a : A) (b : B) (c : C) (d : D) : Prod.zipWith f g (a, b) (c, d) = (f a c, g b d)

Prod.zipWith f g (a, b) (c, d) computes to (f a c, g b d).

Prod.fst3L

def fst3L {A B C : Type} (p : (A × B) × C) : A

First component of a left-nested triple.

Prod.snd3L

def snd3L {A B C : Type} (p : (A × B) × C) : B

Second component of a left-nested triple.

Prod.thd3L

def thd3L {A B C : Type} (p : (A × B) × C) : C

Third component of a left-nested triple.

Prod.mapAll

def mapAll {A B : Type} (f : A -> B) (p : A × A) : B × B

Applies one function to both components of a homogeneous pair.

Prod.fold

def fold {A B : Type} (f : A -> A -> B) (p : A × A) : B

Combines the two components of a homogeneous pair with a binary function.

Prod.rotateL

def rotateL {A B C : Type} (p : A × (B × C)) : B × (C × A)

Rotates a right-nested triple left: (a, (b, c)) becomes (b, (c, a)).

Prod.rotateR

def rotateR {A B C : Type} (p : A × (B × C)) : C × (A × B)

Rotates a right-nested triple right: (a, (b, c)) becomes (c, (a, b)).

Prod.prodFst3LCompute

theorem prodFst3LCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.fst3L ((a, b), c) = a

Prod.fst3L ((a, b), c) computes to a.

Prod.prodSnd3LCompute

theorem prodSnd3LCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.snd3L ((a, b), c) = b

Prod.snd3L ((a, b), c) computes to b.

Prod.prodThd3LCompute

theorem prodThd3LCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.thd3L ((a, b), c) = c

Prod.thd3L ((a, b), c) computes to c.

Prod.prodMapAllCompute

theorem prodMapAllCompute {A B : Type} (f : A -> B) (a1 : A) (a2 : A) : Prod.mapAll f (a1, a2) = (f a1, f a2)

Prod.mapAll f (a1, a2) computes to (f a1, f a2).

Prod.prodMapAllId

theorem prodMapAllId {A : Type} (p : A × A) : Prod.mapAll (fun (a : A) => a) p = p

Prod.mapAll with the identity leaves a pair unchanged.

Prod.prodFoldCompute

theorem prodFoldCompute {A B : Type} (f : A -> A -> B) (a1 : A) (a2 : A) : Prod.fold f (a1, a2) = f a1 a2

Prod.fold f (a1, a2) computes to f a1 a2.

Prod.prodRotateLCompute

theorem prodRotateLCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.rotateL (a, (b, c)) = (b, (c, a))

Prod.rotateL (a, (b, c)) computes to (b, (c, a)).

Prod.prodRotateRCompute

theorem prodRotateRCompute {A B C : Type} (a : A) (b : B) (c : C) : Prod.rotateR (a, (b, c)) = (c, (a, b))

Prod.rotateR (a, (b, c)) computes to (c, (a, b)).

Prod.prodRotateL3

theorem prodRotateL3 {A B C : Type} (a : A) (b : B) (c : C) : Prod.rotateL (Prod.rotateL (Prod.rotateL (a, (b, c)))) = (a, (b, c))

Rotating a triple left three times gives back the original triple.

Prod.prodRotateR3

theorem prodRotateR3 {A B C : Type} (a : A) (b : B) (c : C) : Prod.rotateR (Prod.rotateR (Prod.rotateR (a, (b, c)))) = (a, (b, c))

Rotating a triple right three times gives back the original triple.

Prod.unitLFwd

def unitLFwd {A : Type} (p : A × Unit) : A

Forward map of A × Unit ≅ A: drops the unit component.

Prod.unitLBwd

def unitLBwd {A : Type} (a : A) : A × Unit

Backward map of A × Unit ≅ A: pairs a value with unit.

Prod.unitRFwd

def unitRFwd {A : Type} (p : Unit × A) : A

Forward map of Unit × A ≅ A: drops the unit component.

Prod.unitRBwd

def unitRBwd {A : Type} (a : A) : Unit × A

Backward map of Unit × A ≅ A: pairs unit with a value.

Prod.prodUnitLRoundTrip

theorem prodUnitLRoundTrip {A : Type} (a : A) : Prod.unitLFwd (Prod.unitLBwd a) = a

Pairing with unit on the right and then dropping it gives back the value.

Prod.prodUnitRRoundTrip

theorem prodUnitRRoundTrip {A : Type} (a : A) : Prod.unitRFwd (Prod.unitRBwd a) = a

Pairing with unit on the left and then dropping it gives back the value.

Prod.flatten4RtoL

def flatten4RtoL {A B C D : Type} (p : A × (B × (C × D))) : ((A × B) × C) × D

Reassociates a right-nested quadruple into a left-nested one.

Prod.flatten4LtoR

def flatten4LtoR {A B C D : Type} (p : ((A × B) × C) × D) : A × (B × (C × D))

Reassociates a left-nested quadruple into a right-nested one.

Prod.prodFlatten4RoundTrip1

theorem prodFlatten4RoundTrip1 {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : Prod.flatten4LtoR (Prod.flatten4RtoL (a, (b, (c, d)))) = (a, (b, (c, d)))

Reassociating a right-nested quadruple to the left and back gives it back.

Prod.prodFlatten4RoundTrip2

theorem prodFlatten4RoundTrip2 {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : Prod.flatten4RtoL (Prod.flatten4LtoR (((a, b), c), d)) = (((a, b), c), d)

Reassociating a left-nested quadruple to the right and back gives it back.

Prod.prodMapIdId

theorem prodMapIdId {A B : Type} (p : A × B) : prodMap (fun (a : A) => a) (fun (b : B) => b) p = p

Functor identity law: prodMap with identity functions leaves a pair unchanged.

Prod.prodMapPair

theorem prodMapPair {A B C D : Type} (f : A -> C) (g : B -> D) (a : A) (b : B) : prodMap f g (a, b) = (f a, g b)

prodMap f g (a, b) computes to (f a, g b).

Prod.pairCongFst

def pairCongFst {A B : Type} (a1 : A) (a2 : A) (b : B) (h : a1 = a2) : (a1, b) = (a2, b)

Equal first components give equal pairs with the same second component.

Prod.pairCongSnd

def pairCongSnd {A B : Type} (a : A) (b1 : B) (b2 : B) (h : b1 = b2) : (a, b1) = (a, b2)

Equal second components give equal pairs with the same first component.

Prod.prodCurryApp

theorem prodCurryApp {A B C : Type} (f : A × B -> C) (p : A × B) : Prod.curry f (fst p) (snd p) = f p

Currying a function and applying it to a pair’s components equals applying the function to the pair.

Prod.prodUncurrySwapNat

theorem prodUncurrySwapNat (a : Nat) (b : Nat) : Prod.uncurry (fun (x : Nat) => fun (y : Nat) => add y x) (a, b) = add b a

Example: uncurrying addition with swapped arguments on (a, b) gives add b a.

Prod.prodSwapAssocFwd

theorem prodSwapAssocFwd {A B C : Type} (a : A) (b : B) (c : C) : Prod.swap (Prod.assocFwd (a, (b, c))) = (c, (a, b))

Swapping after reassociating (a, (b, c)) to the left gives (c, (a, b)).

Prod.prodSwapAssocBwd

theorem prodSwapAssocBwd {A B C : Type} (a : A) (b : B) (c : C) : Prod.swap (Prod.assocBwd ((a, b), c)) = ((b, c), a)

Swapping after reassociating ((a, b), c) to the right gives ((b, c), a).

Prod.both

def both {A B : Type} (f : A -> B) (p : A × A) : B × B

Applies one function to both components of a homogeneous pair (same as Prod.mapAll).

Prod.unpair

def unpair {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : B × C

Splits a value into a pair using two functions (same as Prod.fanout).

Prod.elim

def elim {A B C : Type} (f : A -> B -> C) (p : A × B) : C

Combines the components of a pair with a two-argument function (same as Prod.uncurry).

Prod.const

def const {A : Type} (a : A) : A × A

Duplicates a value into a pair (same as Prod.diag).

Prod.arrowPair

def arrowPair {A B C : Type} (f : A -> B -> C) (p : A × B) (q : A × B) : C × C

Applies a two-argument function to the components of each of two pairs and pairs the results.

Prod.prodBothCompute

theorem prodBothCompute {A B : Type} (f : A -> B) (a1 : A) (a2 : A) : Prod.both f (a1, a2) = (f a1, f a2)

Prod.both f (a1, a2) computes to (f a1, f a2).

Prod.prodBothId

theorem prodBothId {A : Type} (p : A × A) : Prod.both (fun (a : A) => a) p = p

Prod.both with the identity leaves a pair unchanged.

Prod.prodUnpairCompute

theorem prodUnpairCompute {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : Prod.unpair f g a = (f a, g a)

Prod.unpair f g a computes to (f a, g a).

Prod.prodWithCompute

theorem prodWithCompute {A B C : Type} (f : A -> B -> C) (a : A) (b : B) : Prod.elim f (a, b) = f a b

Prod.elim f (a, b) computes to f a b.

Prod.prodConstCompute

theorem prodConstCompute {A : Type} (a : A) : Prod.const a = (a, a)

Prod.const a computes to (a, a).

Prod.prodArrowPairCompute

theorem prodArrowPairCompute {A B C : Type} (f : A -> B -> C) (a1 : A) (b1 : B) (a2 : A) (b2 : B) : Prod.arrowPair f (a1, b1) (a2, b2) = (f a1 b1, f a2 b2)

Prod.arrowPair f (a1, b1) (a2, b2) computes to (f a1 b1, f a2 b2).

Prod.mkQuad

def mkQuad {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : A × (B × (C × D))

Builds a right-nested quadruple from four values.

Prod.quadFst

def quadFst {A B C D : Type} (p : A × (B × (C × D))) : A

First component of a right-nested quadruple.

Prod.quadSnd

def quadSnd {A B C D : Type} (p : A × (B × (C × D))) : B

Second component of a right-nested quadruple.

Prod.quadThd

def quadThd {A B C D : Type} (p : A × (B × (C × D))) : C

Third component of a right-nested quadruple.

Prod.quadFth

def quadFth {A B C D : Type} (p : A × (B × (C × D))) : D

Fourth component of a right-nested quadruple.

Prod.mapQuad

def mapQuad {A B C D E F G H : Type} (f : A -> E) (g : B -> F) (h : C -> G) (k : D -> H) (p : A × (B × (C × D))) : E × (F × (G × H))

Applies four functions componentwise to a right-nested quadruple.

Prod.prodMkQuadCompute

theorem prodMkQuadCompute {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : Prod.mkQuad a b c d = (a, (b, (c, d)))

Prod.mkQuad a b c d computes to (a, (b, (c, d))).

Prod.prodQuadFstCompute

theorem prodQuadFstCompute {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : Prod.quadFst (Prod.mkQuad a b c d) = a

Prod.quadFst of a quadruple built by Prod.mkQuad is its first value.

Prod.prodQuadSndCompute

theorem prodQuadSndCompute {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : Prod.quadSnd (Prod.mkQuad a b c d) = b

Prod.quadSnd of a quadruple built by Prod.mkQuad is its second value.

Prod.prodQuadThdCompute

theorem prodQuadThdCompute {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : Prod.quadThd (Prod.mkQuad a b c d) = c

Prod.quadThd of a quadruple built by Prod.mkQuad is its third value.

Prod.prodQuadFthCompute

theorem prodQuadFthCompute {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : Prod.quadFth (Prod.mkQuad a b c d) = d

Prod.quadFth of a quadruple built by Prod.mkQuad is its fourth value.

Prod.prodMapQuadCompute

theorem prodMapQuadCompute {A B C D E F G H : Type} (f : A -> E) (g : B -> F) (h : C -> G) (k : D -> H) (a : A) (b : B) (c : C) (d : D) : Prod.mapQuad f g h k (a, (b, (c, d))) = (f a, (g b, (h c, k d)))

Prod.mapQuad f g h k applies each function to the matching component.

Prod.prodMapQuadId

theorem prodMapQuadId {A B C D : Type} (p : A × (B × (C × D))) : Prod.mapQuad (fun (a : A) => a) (fun (b : B) => b) (fun (c : C) => c) (fun (d : D) => d) p = p

Prod.mapQuad with identity functions leaves a quadruple unchanged.

Prod.prodBothCompose

theorem prodBothCompose {A B C : Type} (f : A -> B) (g : B -> C) (p : A × A) : Prod.both g (Prod.both f p) = Prod.both (fun (a : A) => g (f a)) p

Applying Prod.both twice equals applying it once with the composed function.

Prod.prodWithEqUncurry

theorem prodWithEqUncurry {A B C : Type} (f : A -> B -> C) (p : A × B) : Prod.elim f p = Prod.uncurry f p

Prod.elim agrees with Prod.uncurry.

Prod.prodUnpairEqFanout

theorem prodUnpairEqFanout {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : Prod.unpair f g a = Prod.fanout f g a

Prod.unpair agrees with Prod.fanout.

Prod.prodConstEqDiag

theorem prodConstEqDiag {A : Type} (a : A) : Prod.const a = Prod.diag a

Prod.const agrees with Prod.diag.

Prod.prodBothEqDup

theorem prodBothEqDup {A B : Type} (f : A -> B) (p : A × A) : Prod.both f p = Prod.dup f p

Prod.both agrees with Prod.dup.