blob: 396a524c736780e2d09449b59d0d8dcd8f80fe88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
import Verification.Specifications
namespace Implementation
open Primitives
open avl_verification
open Specifications (OrdSpecLinearOrderEq ltOfRustOrder gtOfRustOrder)
instance ScalarU32DecidableLE : DecidableRel (· ≤ · : U32 -> U32 -> Prop) := by
simp [instLEScalar]
-- Lift this to the decidability of the Int version.
infer_instance
instance : LinearOrder (Scalar .U32) where
le_antisymm := fun a b Hab Hba => by
apply (Scalar.eq_equiv a b).2; exact (Int.le_antisymm ((Scalar.le_equiv _ _).1 Hab) ((Scalar.le_equiv _ _).1 Hba))
le_total := fun a b => by
rcases (Int.le_total a b) with H | H
left; exact (Scalar.le_equiv _ _).2 H
right; exact (Scalar.le_equiv _ _).2 H
decidableLE := ScalarU32DecidableLE
instance : OrdSpecLinearOrderEq OrdU32 where
infallible := fun a b => by
unfold Ord.cmp
unfold OrdU32
unfold OrdU32.cmp
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
if hlt : a < b then
use .Less
simp [hlt]
else
if heq: a = b
then
use .Equal
simp [hlt]
rw [heq]
-- TODO: simp [hlt, heq] breaks everything???
else
use .Greater
simp [hlt, heq]
symmetry := fun a b => by
rw [Ordering.toDualOrdering, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
rw [compare, Ord.opposite]
simp [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
split_ifs with hab hba hba' hab' hba'' _ hba₃ _ <;> tauto
exact lt_irrefl _ (lt_trans hab hba)
rw [hba'] at hab; exact lt_irrefl _ hab
rw [hab'] at hba''; exact lt_irrefl _ hba''
-- The order is total, therefore, we have at least one case where we are comparing something.
cases (lt_trichotomy a b) <;> tauto
equivalence := fun a b => by
unfold Ord.cmp
unfold OrdU32
unfold OrdU32.cmp
simp only []
split_ifs <;> simp only [Result.ok.injEq, not_false_eq_true, neq_imp, IsEmpty.forall_iff]; tauto; try assumption
|
