src/tensor/axis_PROOF.bend
bendtorch-core@0.1.0.0 · 108 lines · 6 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
4import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
5import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
6import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as Algebra
7import bendtorch-core@0.1.0.0/src/tensor/axis_LAWS.bend as Laws
8
9def inverse_selected(-rank: Nat, -axes: List<&2, Nat>, certificate: Algebra.Facts<rank, axes>) ->
10 {Axis.inverse(rank, axes) == Some{Axis.inverse_axes(rank, axes)} : Maybe<&2, List<&2, Nat>>}:
11 Algebra.Certified{iv, selected, restored, lists, product, fit} = certificate
12 selected
13
14def inverse_involution(-rank: Nat, -axes: List<&2, Nat>, certificate: Algebra.Facts<rank, axes>) ->
15 {Axis.inverse_axes(rank, Axis.inverse_axes(rank, axes)) == axes : List<&2, Nat>}:
16 Algebra.Certified{iv, selected, restored, lists, product, fit} = certificate
17 restored
18
19def reverse_composition(-A: Data, -rank: Nat, -axes: List<&2, Nat>, -items: List<&2, A>, certificate: Algebra.ListFacts<A, rank, axes, items>) ->
20 {Axis.order(A, Axis.order(A, items, Axis.inverse_axes(rank, axes)), axes) == items : List<&2, A>}:
21 Algebra.Lists{selected, ranked, scattered, restored, reverse_restored, scatter_restored} = certificate
22 reverse_restored
23
24def coordinate_fit(-rank: Nat, -axes: List<&2, Nat>, +dimensions: List<&2, Nat>, +coordinates: List<&2, Nat>,
25 dimensions_length: {List.length(&2, Nat, dimensions) == rank : Nat}, coordinates_length: {List.length(&2, Nat, coordinates) == rank : Nat}, certificate: Algebra.Facts<rank, axes>) ->
26 {Shape.fit(Axis.order(Nat, dimensions, axes), Axis.order(Nat, coordinates, axes)) == Shape.fit(dimensions, coordinates) : Bool}:
27 Algebra.Certified{iv, selected, restored, lists, product, fit} = certificate
28 fit(dimensions, coordinates, dimensions_length, coordinates_length)
29
30def plan_valid(-shape: Shape.Shape, -axes: List<&2, U32>, plan: Layout.Plan<shape, axes>) -> {True{} == Layout.bijective(shape, axes) : Bool}:
31 Layout.Permutation{output, valid, ordered, count} = plan
32 valid
33
34def permutation_rejects(+shape: Shape.Shape, +axes: List<&2, U32>, result: Result<&2, &2, Layout.Error, Layout.Plan<shape, axes>>, rejected: {False{} == Layout.bijective(shape, axes) : Bool}) ->
35 {Laws.axis_plan_succeeded(shape, axes, result) == False{} : Bool}:
36 match result:
37 case Fail{error}:
38 {==}
39 case Done{plan}:
40 Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Layout.bijective(shape, axes), plan_valid(shape, axes, plan), rejected))
41
42def Laws.axis_lookup_refines(items, index):
43 Algebra.lookup(items, index)
44
45def Laws.axis_gather_refines(axes, items):
46 Algebra.reorder(axes, items)
47
48def Laws.axis_scatter_refines(shape, axes, coordinates):
49 Algebra.inverse_coordinates(shape, axes, coordinates)
50
51def Laws.axis_validity_refines(shape, axes, accepted):
52 Algebra.valid(shape, axes, accepted)
53
54def Laws.axis_lookup_complete(A, items, index, bound):
55 Algebra.lookup_complete(A, items, index, bound)
56
57def Laws.axis_permutation_complete(shape, axes, accepted):
58 Algebra.permutation_complete(shape, axes, accepted)
59
60def Laws.axis_permutation_rejects(shape, axes, rejected):
61 permutation_rejects(shape, axes, Layout.permutation(shape, axes), rejected)
62
63def Laws.axis_dimension_rank(shape, axes, accepted):
64 Algebra.permutation_rank(shape, axes, accepted)
65
66def Laws.axis_dimension_product(shape, axes, accepted):
67 Algebra.permutation_product(shape, axes, accepted)
68
69def Laws.axis_scatter_complete(shape, axes, coordinates, accepted, length):
70 Algebra.scatter_complete(shape, axes, coordinates, accepted, length)
71
72def Laws.axis_scatter_gather(shape, axes, coordinates, accepted, length):
73 Algebra.scatter_gather(shape, axes, coordinates, accepted, length)
74
75def Laws.axis_inverse_valid(rank, axes, bound, accepted):
76 Algebra.inverse_valid(rank, axes, bound, accepted)
77
78def Laws.axis_inverse_selected(rank, axes, bound, accepted):
79 inverse_selected(rank, axes, Algebra.facts(rank, axes, bound, accepted))
80
81def Laws.axis_inverse_involution(rank, axes, bound, accepted):
82 inverse_involution(rank, axes, Algebra.facts(rank, axes, bound, accepted))
83
84def Laws.axis_inverse_list_composition(A, rank, axes, items, bound, accepted, length):
85 Algebra.inverse_composition(A, rank, axes, items, bound, accepted, length)
86
87def Laws.axis_inverse_reverse_composition(A, rank, axes, items, bound, accepted, length):
88 reverse_composition(A, rank, axes, items, Algebra.facts_lists(A, rank, axes, items, length, Algebra.facts(rank, axes, bound, accepted)))
89
90def Laws.axis_inverse_scatter_composition(A, rank, axes, items, bound, accepted, length):
91 Algebra.inverse_scatter_composition(A, rank, axes, items, bound, accepted, length)
92
93def Laws.axis_coordinate_fit(rank, axes, dimensions, coordinates, bound, accepted, dimensions_length, coordinates_length):
94 coordinate_fit(rank, axes, dimensions, coordinates, dimensions_length, coordinates_length, Algebra.facts(rank, axes, bound, accepted))
95
96def Laws.axis_scatter_fit(rank, axes, dimensions, coordinates, bound, accepted, dimensions_length, coordinates_length, fits):
97 Equal.trans(Bool, True{}, Shape.fit(Axis.order(Nat, dimensions, axes), coordinates), Shape.fit(dimensions, Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))), fits,
98 Equal.trans(Bool, Shape.fit(Axis.order(Nat, dimensions, axes), coordinates),
99 Shape.fit(Axis.order(Nat, Axis.order(Nat, dimensions, axes), Axis.inverse_axes(rank, axes)), Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))),
100 Shape.fit(dimensions, Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))),
101 Equal.sym(Bool, Shape.fit(Axis.order(Nat, Axis.order(Nat, dimensions, axes), Axis.inverse_axes(rank, axes)), Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))),
102 Shape.fit(Axis.order(Nat, dimensions, axes), coordinates),
103 coordinate_fit(rank, Axis.inverse_axes(rank, axes), Axis.order(Nat, dimensions, axes), coordinates,
104 Algebra.ranked(Nat, rank, axes, dimensions, Algebra.facts_lists(Nat, rank, axes, dimensions, dimensions_length, Algebra.facts(rank, axes, bound, accepted))),
105 coordinates_length, Algebra.facts(rank, Axis.inverse_axes(rank, axes), bound, Algebra.inverse_valid(rank, axes, bound, accepted)))),
106 Equal.cong(List<&2, Nat>, Bool, dims => Shape.fit(dims, Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))),
107 Axis.order(Nat, Axis.order(Nat, dimensions, axes), Axis.inverse_axes(rank, axes)), dimensions,
108 Algebra.inverse_composition(Nat, rank, axes, dimensions, bound, accepted, dimensions_length))))