Skip to content

Commit edee1e1

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Proof debt/standards 132 batch (#66)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 0eb9709 commit edee1e1

42 files changed

Lines changed: 3169 additions & 0 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎src/Proven/SafeAngle/Proofs.idr‎

Lines changed: 231 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,231 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
||| Safety proofs for SafeAngle unit-tagged angle operations.
4+
|||
5+
||| The `Proven.SafeAngle` module ships unit-tagged angles plus
6+
||| conversion / normalisation / trigonometric wrappers but no
7+
||| machine-checked theorem that the conversions and gates are
8+
||| consistent. This file discharges the type-level reducible
9+
||| invariants:
10+
|||
11+
||| * `AngleUnit` enum self-equality under the hand-written `Eq`
12+
||| instance (all 4 constructors).
13+
||| * `AngleUnit` cross-pair inequality witness (anchors the
14+
||| `_ == _ = False` fall-through).
15+
||| * `toRadians` / `toDegrees` / `toGradians` / `toTurns` identity
16+
||| on their own unit (no spurious scaling when the unit is
17+
||| already correct).
18+
||| * `fromDegrees` / `fromRadians` constructor record-projection
19+
||| (built angle round-trips its own unit).
20+
||| * `safeAsin` / `safeAcos` boundary rejection on out-of-range
21+
||| inputs (validates the domain gate).
22+
||| * `normalize` preserves the unit tag (the gate keeps you in
23+
||| the unit you started in — no silent conversion).
24+
|||
25+
||| Items NOT covered here (explicit OWED markers):
26+
|||
27+
||| * `Double` value-level equalities (e.g. `toDegrees (fromDegrees 90) = 90`).
28+
||| Idris2 0.8.0 cannot `Refl`-decide arbitrary IEEE-754 doubles;
29+
||| this needs an external numerical-equivalence tactic.
30+
|||
31+
||| Zero `believe_me` / `idris_crash`.
32+
module Proven.SafeAngle.Proofs
33+
34+
import Proven.SafeAngle
35+
36+
%default total
37+
38+
--------------------------------------------------------------------------------
39+
-- AngleUnit self-equality (4 constructors)
40+
--------------------------------------------------------------------------------
41+
42+
||| `Degrees` is self-equal under `Eq AngleUnit`.
43+
public export
44+
degreesSelfEq : Degrees == Degrees = True
45+
degreesSelfEq = Refl
46+
47+
||| `Radians` is self-equal under `Eq AngleUnit`.
48+
public export
49+
radiansSelfEq : Radians == Radians = True
50+
radiansSelfEq = Refl
51+
52+
||| `Gradians` is self-equal under `Eq AngleUnit`.
53+
public export
54+
gradiansSelfEq : Gradians == Gradians = True
55+
gradiansSelfEq = Refl
56+
57+
||| `Turns` is self-equal under `Eq AngleUnit`.
58+
public export
59+
turnsSelfEq : Turns == Turns = True
60+
turnsSelfEq = Refl
61+
62+
||| Distinct units are unequal — sample pair anchors the
63+
||| `_ == _ = False` fall-through.
64+
public export
65+
degreesNotRadians : Degrees == Radians = False
66+
degreesNotRadians = Refl
67+
68+
||| `Gradians` and `Turns` are distinct.
69+
public export
70+
gradiansNotTurns : Gradians == Turns = False
71+
gradiansNotTurns = Refl
72+
73+
--------------------------------------------------------------------------------
74+
-- Conversion identity on own unit
75+
--------------------------------------------------------------------------------
76+
77+
||| `toRadians` of a `Radians`-tagged angle is the underlying value
78+
||| unchanged.
79+
public export
80+
toRadiansOnRadians : (v : Double) -> toRadians (MkAngle v Radians) = v
81+
toRadiansOnRadians v = Refl
82+
83+
||| `toDegrees` of a `Degrees`-tagged angle is the underlying value
84+
||| unchanged.
85+
public export
86+
toDegreesOnDegrees : (v : Double) -> toDegrees (MkAngle v Degrees) = v
87+
toDegreesOnDegrees v = Refl
88+
89+
||| `toGradians` of a `Gradians`-tagged angle is the underlying value
90+
||| unchanged.
91+
public export
92+
toGradiansOnGradians : (v : Double) -> toGradians (MkAngle v Gradians) = v
93+
toGradiansOnGradians v = Refl
94+
95+
||| `toTurns` of a `Turns`-tagged angle is the underlying value
96+
||| unchanged.
97+
public export
98+
toTurnsOnTurns : (v : Double) -> toTurns (MkAngle v Turns) = v
99+
toTurnsOnTurns v = Refl
100+
101+
--------------------------------------------------------------------------------
102+
-- Constructors record-project as declared
103+
--------------------------------------------------------------------------------
104+
105+
||| `fromDegrees d` records `unit = Degrees`.
106+
public export
107+
fromDegreesUnit : (d : Double) -> (fromDegrees d).unit = Degrees
108+
fromDegreesUnit d = Refl
109+
110+
||| `fromDegrees d` records `value = d`.
111+
public export
112+
fromDegreesValue : (d : Double) -> (fromDegrees d).value = d
113+
fromDegreesValue d = Refl
114+
115+
||| `fromRadians r` records `unit = Radians`.
116+
public export
117+
fromRadiansUnit : (r : Double) -> (fromRadians r).unit = Radians
118+
fromRadiansUnit r = Refl
119+
120+
||| `fromRadians r` records `value = r`.
121+
public export
122+
fromRadiansValue : (r : Double) -> (fromRadians r).value = r
123+
fromRadiansValue r = Refl
124+
125+
--------------------------------------------------------------------------------
126+
-- `normalize` preserves the unit tag
127+
--------------------------------------------------------------------------------
128+
129+
||| `normalize` on a `Degrees`-tagged angle stays in degrees.
130+
public export
131+
normalizePreservesDegrees : (v : Double)
132+
-> (normalize (MkAngle v Degrees)).unit = Degrees
133+
normalizePreservesDegrees v = Refl
134+
135+
||| `normalize` on a `Radians`-tagged angle stays in radians.
136+
public export
137+
normalizePreservesRadians : (v : Double)
138+
-> (normalize (MkAngle v Radians)).unit = Radians
139+
normalizePreservesRadians v = Refl
140+
141+
||| `normalize` on a `Gradians`-tagged angle stays in gradians.
142+
public export
143+
normalizePreservesGradians : (v : Double)
144+
-> (normalize (MkAngle v Gradians)).unit = Gradians
145+
normalizePreservesGradians v = Refl
146+
147+
||| `normalize` on a `Turns`-tagged angle stays in turns.
148+
public export
149+
normalizePreservesTurns : (v : Double)
150+
-> (normalize (MkAngle v Turns)).unit = Turns
151+
normalizePreservesTurns v = Refl
152+
153+
--------------------------------------------------------------------------------
154+
-- `safeAsin` / `safeAcos` domain gate
155+
--------------------------------------------------------------------------------
156+
157+
||| `safeAsin` rejects input above 1.0 (returns `Nothing`).
158+
public export
159+
safeAsinRejectsAbove : safeAsin 2.0 = Nothing
160+
safeAsinRejectsAbove = Refl
161+
162+
||| `safeAsin` rejects input below -1.0 (returns `Nothing`).
163+
public export
164+
safeAsinRejectsBelow : safeAsin (-2.0) = Nothing
165+
safeAsinRejectsBelow = Refl
166+
167+
||| `safeAcos` rejects input above 1.0 (returns `Nothing`).
168+
public export
169+
safeAcosRejectsAbove : safeAcos 2.0 = Nothing
170+
safeAcosRejectsAbove = Refl
171+
172+
||| `safeAcos` rejects input below -1.0 (returns `Nothing`).
173+
public export
174+
safeAcosRejectsBelow : safeAcos (-2.0) = Nothing
175+
safeAcosRejectsBelow = Refl
176+
177+
--------------------------------------------------------------------------------
178+
-- Constructors of derived angles record their declared unit
179+
--------------------------------------------------------------------------------
180+
181+
||| `safeAtan` always returns a `Radians`-tagged angle.
182+
public export
183+
safeAtanIsRadians : (x : Double) -> (safeAtan x).unit = Radians
184+
safeAtanIsRadians x = Refl
185+
186+
||| `safeAtan2` always returns a `Radians`-tagged angle.
187+
public export
188+
safeAtan2IsRadians : (y, x : Double) -> (safeAtan2 y x).unit = Radians
189+
safeAtan2IsRadians y x = Refl
190+
191+
||| `addAngle` returns a `Radians`-tagged angle.
192+
public export
193+
addAngleIsRadians : (a, b : Angle) -> (addAngle a b).unit = Radians
194+
addAngleIsRadians a b = Refl
195+
196+
||| `subAngle` returns a `Radians`-tagged angle.
197+
public export
198+
subAngleIsRadians : (a, b : Angle) -> (subAngle a b).unit = Radians
199+
subAngleIsRadians a b = Refl
200+
201+
||| `scaleAngle` returns a `Radians`-tagged angle.
202+
public export
203+
scaleAngleIsRadians : (s : Double) -> (a : Angle) -> (scaleAngle s a).unit = Radians
204+
scaleAngleIsRadians s a = Refl
205+
206+
||| `angleDifference` returns a `Radians`-tagged angle.
207+
public export
208+
angleDifferenceIsRadians : (a, b : Angle) -> (angleDifference a b).unit = Radians
209+
angleDifferenceIsRadians a b = Refl
210+
211+
--------------------------------------------------------------------------------
212+
-- Explicit OWED postulates (named, erased, discoverable)
213+
--
214+
-- Idris2 0.8.0 cannot Refl-decide Double value-level equalities; the
215+
-- claim "toDegrees (fromDegrees 90.0) = 90.0" needs an external IEEE-754
216+
-- numerical-equivalence tactic. Stated as named, erased postulates so
217+
-- the residual debt is visible.
218+
--------------------------------------------------------------------------------
219+
220+
||| OWED: `fromDegrees` round-trips through `toDegrees`. Blocked on
221+
||| the absence of a numerical-equivalence tactic for `Double` literals
222+
||| in Idris2 0.8.0.
223+
public export
224+
0 fromToDegreesRoundtrip :
225+
(d : Double) -> toDegrees (fromDegrees d) = d
226+
227+
||| OWED: `fromRadians` round-trips through `toRadians`. Same blocker
228+
||| as `fromToDegreesRoundtrip`.
229+
public export
230+
0 fromToRadiansRoundtrip :
231+
(r : Double) -> toRadians (fromRadians r) = r

0 commit comments

Comments
 (0)