cakeml/translator/okasaki-examples/okasaki_miscScript.sml at master · ericlp/cakeml · GitHub

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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
(*
  Lemmas used in Okasaki examples.
*)
open preamble
open relationTheory bagLib bagTheory;

val fs = full_simp_tac (srw_ss ())
val rw = srw_tac []

val _ = new_theory "okasaki_misc"

Theorem WeakLinearOrder_neg:
 !leq x y. WeakLinearOrder leq ⇒ (~leq x y <=> leq y x ∧ x ≠ y)
Proof
metis_tac [WeakLinearOrder, WeakOrder, trichotomous, reflexive_def,
           antisymmetric_def]
QED

Theorem BAG_EVERY_DIFF:
 !P b1 b2. BAG_EVERY P b1 ⇒ BAG_EVERY P (BAG_DIFF b1 b2)
Proof
rw [BAG_EVERY] >>
metis_tac [BAG_IN_DIFF_E]
QED

Theorem BAG_EVERY_EL:
 !P x. BAG_EVERY P (EL_BAG x) = P x
Proof
rw [BAG_EVERY, EL_BAG]
QED

Theorem BAG_INN_BAG_DIFF:
 !x m b1 b2.
  BAG_INN x m (BAG_DIFF b1 b2) =
  ∃n1 n2. (m = n1 - n2) ∧
          BAG_INN x n1 b1 ∧ BAG_INN x n2 b2 ∧ ~BAG_INN x (n2 + 1) b2
Proof
rw [BAG_INN, BAG_DIFF] >>
EQ_TAC >>
rw [] >|
[qexists_tac `b2 x + m` >>
     qexists_tac `b2 x` >>
     decide_tac,
 qexists_tac `0` >>
     qexists_tac `b2 x` >>
     decide_tac,
 decide_tac]
QED

Theorem BAG_DIFF_INSERT2:
 !x b. BAG_DIFF (BAG_INSERT x b) (EL_BAG x) = b
Proof
rw [BAG_DIFF, BAG_INSERT, EL_BAG, FUN_EQ_THM, EMPTY_BAG] >>
cases_on `x' = x` >>
rw []
QED

val list_to_bag_def = Define `
(list_to_bag [] = {||}) ∧
(list_to_bag (h::t) = BAG_INSERT h (list_to_bag t))`;

Theorem list_to_bag_filter:
 ∀P l. list_to_bag (FILTER P l) = BAG_FILTER P (list_to_bag l)
Proof
Induct_on `l` >>
rw [list_to_bag_def]
QED

Theorem list_to_bag_append:
 ∀l1 l2. list_to_bag (l1 ++ l2) = BAG_UNION (list_to_bag l1) (list_to_bag l2)
Proof
Induct_on `l1` >>
srw_tac [BAG_ss] [list_to_bag_def, BAG_INSERT_UNION]
QED

val list_to_bag_to_perm = Q.prove (
`!l1 l2. PERM l1 l2 ⇒ (list_to_bag l1 = list_to_bag l2)`,
HO_MATCH_MP_TAC PERM_IND >>
srw_tac [BAG_ss] [list_to_bag_def, BAG_INSERT_UNION]);

val perm_to_list_to_bag_lem = Q.prove (
`!l1 l2 x.
  (list_to_bag (FILTER ($= x) l1) = list_to_bag (FILTER ($= x) l2))
  ⇒
  (FILTER ($= x) l1 = FILTER ($= x) l2)`,
induct_on `l1` >>
rw [] >>
induct_on `l2` >>
rw [] >>
fs [list_to_bag_def]);

val perm_to_list_to_bag = Q.prove (
`!l1 l2. (list_to_bag l1 = list_to_bag l2) ⇒ PERM l1 l2`,
rw [PERM_DEF] >>
metis_tac [perm_to_list_to_bag_lem, list_to_bag_filter]);

Theorem list_to_bag_perm:
 !l1 l2. (list_to_bag l1 = list_to_bag l2) = PERM l1 l2
Proof
metis_tac [perm_to_list_to_bag, list_to_bag_to_perm]
QED

val sorted_reverse_lem = Q.prove (
`!R l. transitive R ∧ SORTED R l ⇒ SORTED (\x y. R y x) (REVERSE l)`,
induct_on `l` >>
rw [SORTED_DEF] >>
qmatch_goalsub_abbrev_tac ‘SORTED RR’ >>
‘transitive RR’ by (fs [transitive_def] >> metis_tac []) >>
unabbrev_all_tac >>
rw [SORTED_DEF,SORTED_APPEND] >>
metis_tac [SORTED_EQ]);

Theorem sorted_reverse:
 !R l. transitive R ⇒ (SORTED R (REVERSE l) = SORTED (\x y. R y x) l)
Proof
rw [] >>
EQ_TAC >>
rw [] >>
imp_res_tac sorted_reverse_lem >>
fs [transitive_def] >>
`(\x y. R x y) = R` by metis_tac [] >>
fs [] >>
metis_tac []
QED

val _ = export_theory ();