src/autograd/sum_to_size_PROOF.bend
bendtorch-core@0.1.0.0 · 120 lines · 11 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
4import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
5import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
6import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
7import bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend as ConstructionLaws
8import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionProof
9import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
10import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
11import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws
12import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReduceProof
13import bendtorch-core@0.1.0.0/src/autograd/sum_to_size.bend as SumToSize
14import bendtorch-core@0.1.0.0/src/autograd/sum_to_size_LAWS.bend as Laws
15
16type Holds<-P: Type> is Data:
17 Holds{-proof: P}
18
19def FirstKept(-shape: Shape.Shape, -original: Core.Tensor<shape>, pair: Core.Tensor<shape> & Core.Tensor<shape>) -> Type:
20 (@+index: U32 -> {ConstructionLaws.clone_first_checked(shape, pair, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}) &
21 (@+index: U32 -> {ConstructionLaws.clone_first_model(shape, pair, index) == Core.observe(shape, original, index) : Maybe<&2, F32>})
22
23def SecondKept(-shape: Shape.Shape, -original: Core.Tensor<shape>, pair: Core.Tensor<shape> & Core.Tensor<shape>) -> Type:
24 (@+index: U32 -> {ConstructionLaws.clone_second_checked(shape, pair, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}) &
25 (@+index: U32 -> {ConstructionLaws.clone_second_model(shape, pair, index) == Core.observe(shape, original, index) : Maybe<&2, F32>})
26
27def first_kept(+shape: Shape.Shape, original: Core.Tensor<shape>) -> Holds<FirstKept(shape, original, Core.clone(shape, original))>:
28 {\{ConstructionLaws.CloneMeaning: first_checked => second_checked => first_model => second_model =>
29 Holds{(first_checked, first_model)}} :
30 ConstructionLaws.CloneMeaning<shape, original> -> Holds<FirstKept(shape, original, Core.clone(shape, original))>}(
31 ConstructionLaws.public_clone_elements(shape, original))
32
33def second_kept(+shape: Shape.Shape, original: Core.Tensor<shape>) -> Holds<SecondKept(shape, original, Core.clone(shape, original))>:
34 {\{ConstructionLaws.CloneMeaning: first_checked => second_checked => first_model => second_model =>
35 Holds{(second_checked, second_model)}} :
36 ConstructionLaws.CloneMeaning<shape, original> -> Holds<SecondKept(shape, original, Core.clone(shape, original))>}(
37 ConstructionLaws.public_clone_elements(shape, original))
38
39def first_property(+property: Totality.Property, -shape: Shape.Shape, -original: Core.Tensor<shape>, -first: Core.Tensor<shape>,
40 checked: @+index: U32 -> {Core.checked_observe(shape, first, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>},
41 model: @+index: U32 -> {Core.observe(shape, first, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}) ->
42 {Totality.inspect(property, Core.Packed{shape, first}) == Totality.inspect(property, Core.Packed{shape, original}) : Totality.Inspection}:
43 match property:
44 case Totality.Dimensions{}:
45 {==}
46 case Totality.Checked{+index}:
47 Equal.cong(Maybe<&2, F32>, Totality.Inspection, value => Totality.Value{value},
48 Core.checked_observe(shape, first, index), Core.checked_observe(shape, original, index), checked(index))
49 case Totality.Raw{+index}:
50 Equal.cong(Maybe<&2, F32>, Totality.Inspection, value => Totality.Value{value},
51 Core.observe(shape, first, index), Core.observe(shape, original, index), model(index))
52
53def cloned_retains(+shape: Shape.Shape, -original: Core.Tensor<shape>, pair: Core.Tensor<shape> & Core.Tensor<shape>,
54 -kept: FirstKept(shape, original, pair)) ->
55 ReduceLaws.Retained<Core.Packed{shape, original}, SumToSize.cloned(shape, pair)>:
56 (first, second) = pair
57 ReduceLaws.Retained{property => first_property(property, shape, original, first,
58 Pair.fst(@+index: U32 -> {Core.checked_observe(shape, first, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, first, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept), Pair.snd(@+index: U32 -> {Core.checked_observe(shape, first, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, first, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept))}
59
60def decided_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, same: Bool) ->
61 ReduceLaws.Retained<Core.Packed{shape, tensor}, SumToSize.decided(shape, tensor, target, same)>:
62 match same:
63 case False{}:
64 ReduceLaws.reduce_retains_input(Core.Packed{shape, tensor}, target)
65 case True{}:
66 cloned_retains(shape, tensor, Core.clone(shape, tensor),
67 {\{Holds: proof => proof} : Holds<FirstKept(shape, tensor, Core.clone(shape, tensor))> -> FirstKept(shape, tensor, Core.clone(shape, tensor))}(
68 first_kept(shape, tensor)))
69
70def Laws.sum_to_size_retains_input(input, target):
71 Core.Packed{+shape, tensor} = input
72 decided_retains(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)))
73
74def cloned_identity(+shape: Shape.Shape, -original: Core.Tensor<shape>, +target: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>,
75 -same: {Shape.dimensions(shape) == Shape.dimensions(target) : List<&2, U32>},
76 -kept: SecondKept(shape, original, pair)) ->
77 Holds<Laws.Identity(Core.Packed{shape, original}, target, SumToSize.cloned(shape, pair))>:
78 (first, second) = pair
79 Holds{(same, index => (Pair.fst(@+index: U32 -> {Core.checked_observe(shape, second, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, second, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept)(index), Pair.snd(@+index: U32 -> {Core.checked_observe(shape, second, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, second, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept)(index)))}
80
81def decided_identity(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, flag: Bool,
82 -decided: {flag == Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)) : Bool},
83 -same: {Shape.dimensions(shape) == Shape.dimensions(target) : List<&2, U32>}) ->
84 Holds<Laws.Identity(Core.Packed{shape, tensor}, target, SumToSize.decided(shape, tensor, target, flag))>:
85 match flag:
86 case False{}:
87 Holds{Empty.absurd(Laws.Identity(Core.Packed{shape, tensor}, target, SumToSize.decided(shape, tensor, target, False{})),
88 Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)), True{}, decided,
89 %same : {Layout.words_same(Shape.dimensions(shape), _) == True{} : Bool}
90 TransformProof.words_same_refl(Shape.dimensions(shape)))))}
91 case True{}:
92 cloned_identity(shape, tensor, target, Core.clone(shape, tensor), same,
93 {\{Holds: proof => proof} : Holds<SecondKept(shape, tensor, Core.clone(shape, tensor))> -> SecondKept(shape, tensor, Core.clone(shape, tensor))}(
94 second_kept(shape, tensor)))
95
96def Laws.sum_to_size_identity(input, target, same):
97 Core.Packed{+shape, tensor} = input
98 Laws.IdentityModel{
99 {\{Holds: proof => proof} :
100 Holds<Laws.Identity(Core.Packed{shape, tensor}, target,
101 SumToSize.decided(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target))))> ->
102 Laws.Identity(Core.Packed{shape, tensor}, target, SumToSize.sum_to_size(Core.Packed{shape, tensor}, target))}(
103 decided_identity(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)), {==}, same))}
104
105def decided_reduces(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, flag: Bool,
106 decided: {flag == Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)) : Bool},
107 differ: {Shape.dimensions(shape) != Shape.dimensions(target) : List<&2, U32>}) ->
108 {SumToSize.decided(shape, tensor, target, flag) == Reduce.reduce_to(Core.Packed{shape, tensor}, target) :
109 Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}:
110 match flag:
111 case False{}:
112 {==}
113 case True{}:
114 Empty.absurd({SumToSize.decided(shape, tensor, target, True{}) == Reduce.reduce_to(Core.Packed{shape, tensor}, target) :
115 Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>},
116 differ(TransformProof.words_equal(Shape.dimensions(shape), Shape.dimensions(target), decided)))
117
118def Laws.sum_to_size_reduces(input, target, differ):
119 Core.Packed{+shape, tensor} = input
120 decided_reduces(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)), {==}, differ)