summaryrefslogtreecommitdiff
path: root/tests/lean/Demo/Properties.lean
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