blob: cdec73323b4353e542151e7ed16702e91465cae8 (
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
58
59
60
61
62
63
64
65
66
67
68
|
import Base
import Demo.Demo
open Primitives
open Result
namespace demo
#check U32.add_spec
-- @[pspec]
theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
: ∃ y, mul2_add1 x = ret y ∧
↑y = 2 * ↑x + (1 : Int)
:= by
rw [mul2_add1]
progress with U32.add_spec as ⟨ i ⟩
progress as ⟨ i' ⟩
simp; scalar_tac
theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
∃ z, use_mul2_add1 x y = ret z ∧
↑z = 2 * ↑x + (1 : Int) + ↑y := by
rw [use_mul2_add1]
progress with mul2_add1_spec as ⟨ i ⟩
progress as ⟨ i' ⟩
simp; scalar_tac
open CList
@[simp] def CList.to_list {α : Type} (x : CList α) : List α :=
match x with
| CNil => []
| CCons hd tl => hd :: tl.to_list
theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
(h : ↑i < l.to_list.len) :
∃ x, list_nth T l i = ret x ∧
x = l.to_list.index ↑i
:= by
rw [list_nth]
match l with
| CNil =>
simp_all; scalar_tac
| CCons hd tl =>
simp_all
if hi: i = 0#u32 then
simp_all
else
simp_all
progress as ⟨ i1 ⟩
progress as ⟨ x ⟩
simp_all
theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
∃ y, i32_id x = ret y ∧ x.val = y.val := by
rw [i32_id]
if hx : x = 0#i32 then
simp_all
else
simp_all
progress as ⟨ x1 ⟩
progress as ⟨ x2 ⟩
progress
simp_all
termination_by x.val.toNat
decreasing_by scalar_decr_tac
end demo
|
