def axes_facts
bendtorch-core@0.1.0.0 · src/tensor/transpose_PROOF.bend:31
import bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend as TransposePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
31def axes_facts(+dims: List<&2, U32>, +a: Nat, +b: Nat, +bound: Shape.LE(Shape.rank_dimensions(dims), 4n),
32 +inside: {True{} == Transpose.axes_valid(Shape.rank_dimensions(dims), a, b) : Bool}) -> AxesFacts<dims, a, b>:
33 match dims a b:
34 case Nil{} 0n 0n:
35 Certified{{==}, {==}, {==}}
36 case Nil{} 1n+p b:
37 Empty.absurd(AxesFacts<Nil{}, 1n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n)), inside))))
38 case Nil{} a 1n+p:
39 Empty.absurd(AxesFacts<Nil{}, a, 1n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n)), inside))))
40 case +d0 <> Nil{} 0n 0n:
41 Certified{{==}, {==}, {==}}
42 case +d0 <> Nil{} 1n+p b:
43 Empty.absurd(AxesFacts<d0 <> Nil{}, 1n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n)), inside))))
44 case +d0 <> Nil{} a 1n+p:
45 Empty.absurd(AxesFacts<d0 <> Nil{}, a, 1n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n)), inside))))
46 case +d0 <> +d1 <> Nil{} 0n 0n:
47 Certified{{==}, {==}, {==}}
48 case +d0 <> +d1 <> Nil{} 0n 1n:
49 Certified{{==}, {==}, {==}}
50 case +d0 <> +d1 <> Nil{} 1n 0n:
51 Certified{{==}, {==}, {==}}
52 case +d0 <> +d1 <> Nil{} 1n 1n:
53 Certified{{==}, {==}, {==}}
54 case +d0 <> +d1 <> Nil{} 2n+p b:
55 Empty.absurd(AxesFacts<d0 <> d1 <> Nil{}, 2n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(2n+p, 2n), Nat.is_lt(b, 2n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(2n+p, 2n), Nat.is_lt(b, 2n)), inside))))
56 case +d0 <> +d1 <> Nil{} a 2n+p:
57 Empty.absurd(AxesFacts<d0 <> d1 <> Nil{}, a, 2n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 2n), Nat.is_lt(2n+p, 2n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 2n), Nat.is_lt(2n+p, 2n)), inside))))
58 case +d0 <> +d1 <> +d2 <> Nil{} 0n 0n:
59 Certified{{==}, {==}, {==}}
60 case +d0 <> +d1 <> +d2 <> Nil{} 0n 1n:
61 Certified{{==}, {==}, {==}}
62 case +d0 <> +d1 <> +d2 <> Nil{} 0n 2n:
63 Certified{{==}, {==}, {==}}
64 case +d0 <> +d1 <> +d2 <> Nil{} 1n 0n:
65 Certified{{==}, {==}, {==}}
66 case +d0 <> +d1 <> +d2 <> Nil{} 1n 1n:
67 Certified{{==}, {==}, {==}}
68 case +d0 <> +d1 <> +d2 <> Nil{} 1n 2n:
69 Certified{{==}, {==}, {==}}
70 case +d0 <> +d1 <> +d2 <> Nil{} 2n 0n:
71 Certified{{==}, {==}, {==}}
72 case +d0 <> +d1 <> +d2 <> Nil{} 2n 1n:
73 Certified{{==}, {==}, {==}}
74 case +d0 <> +d1 <> +d2 <> Nil{} 2n 2n:
75 Certified{{==}, {==}, {==}}
76 case +d0 <> +d1 <> +d2 <> Nil{} 3n+p b:
77 Empty.absurd(AxesFacts<d0 <> d1 <> d2 <> Nil{}, 3n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Nat.is_lt(b, 3n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(3n+p, 3n), Nat.is_lt(b, 3n)), inside))))
78 case +d0 <> +d1 <> +d2 <> Nil{} a 3n+p:
79 Empty.absurd(AxesFacts<d0 <> d1 <> d2 <> Nil{}, a, 3n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 3n), Nat.is_lt(3n+p, 3n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 3n), Nat.is_lt(3n+p, 3n)), inside))))
80 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 0n:
81 Certified{{==}, {==}, {==}}
82 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 1n:
83 Certified{{==}, {==}, {==}}
84 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 2n:
85 Certified{{==}, {==}, {==}}
86 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 3n:
87 Certified{{==}, {==}, {==}}
88 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 0n:
89 Certified{{==}, {==}, {==}}
90 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 1n:
91 Certified{{==}, {==}, {==}}
92 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 2n:
93 Certified{{==}, {==}, {==}}
94 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 3n:
95 Certified{{==}, {==}, {==}}
96 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 0n:
97 Certified{{==}, {==}, {==}}
98 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 1n:
99 Certified{{==}, {==}, {==}}
100 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 2n:
101 Certified{{==}, {==}, {==}}
102 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 3n:
103 Certified{{==}, {==}, {==}}
104 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 0n:
105 Certified{{==}, {==}, {==}}
106 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 1n:
107 Certified{{==}, {==}, {==}}
108 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 2n:
109 Certified{{==}, {==}, {==}}
110 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 3n:
111 Certified{{==}, {==}, {==}}
112 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 4n+p b:
113 Empty.absurd(AxesFacts<d0 <> d1 <> d2 <> d3 <> Nil{}, 4n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Nat.is_lt(b, 4n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(4n+p, 4n), Nat.is_lt(b, 4n)), inside))))
114 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} a 4n+p:
115 Empty.absurd(AxesFacts<d0 <> d1 <> d2 <> d3 <> Nil{}, a, 4n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 4n), Nat.is_lt(4n+p, 4n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 4n), Nat.is_lt(4n+p, 4n)), inside))))
116 case +d0 <> +d1 <> +d2 <> +d3 <> +d4 <> +tail a b:
117 match bound: