From 42fe6fb304b322b2bfabab243964375520f46973 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 9 Feb 2024 15:24:57 +0100 Subject: Add some demo files --- tests/lean/Demo/Demo.lean | 148 ++++++++++++++++++++++++++++++++++++++++ tests/lean/Demo/Properties.lean | 68 ++++++++++++++++++ 2 files changed, 216 insertions(+) create mode 100644 tests/lean/Demo/Demo.lean create mode 100644 tests/lean/Demo/Properties.lean (limited to 'tests/lean/Demo') diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean new file mode 100644 index 00000000..01818585 --- /dev/null +++ b/tests/lean/Demo/Demo.lean @@ -0,0 +1,148 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [demo] +import Base +open Primitives + +namespace demo + +/- [demo::choose]: + Source: 'src/demo.rs', lines 5:0-5:70 -/ +def choose + (T : Type) (b : Bool) (x : T) (y : T) : + Result (T × (T → Result (T × T))) + := + if b + then let back_'a := fun ret => Result.ret (ret, y) + Result.ret (x, back_'a) + else let back_'a := fun ret => Result.ret (x, ret) + Result.ret (y, back_'a) + +/- [demo::mul2_add1]: + Source: 'src/demo.rs', lines 13:0-13:31 -/ +def mul2_add1 (x : U32) : Result U32 := + do + let i ← x + x + i + 1#u32 + +/- [demo::use_mul2_add1]: + Source: 'src/demo.rs', lines 17:0-17:43 -/ +def use_mul2_add1 (x : U32) (y : U32) : Result U32 := + do + let i ← mul2_add1 x + i + y + +/- [demo::incr]: + Source: 'src/demo.rs', lines 21:0-21:31 -/ +def incr (x : U32) : Result U32 := + x + 1#u32 + +/- [demo::CList] + Source: 'src/demo.rs', lines 27:0-27:17 -/ +inductive CList (T : Type) := +| CCons : T → CList T → CList T +| CNil : CList T + +/- [demo::list_nth]: + Source: 'src/demo.rs', lines 32:0-32:56 -/ +divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := + match l with + | CList.CCons x tl => + if i = 0#u32 + then Result.ret x + else do + let i1 ← i - 1#u32 + list_nth T tl i1 + | CList.CNil => Result.fail .panic + +/- [demo::list_nth_mut]: + Source: 'src/demo.rs', lines 47:0-47:68 -/ +divergent def list_nth_mut + (T : Type) (l : CList T) (i : U32) : + Result (T × (T → Result (CList T))) + := + match l with + | CList.CCons x tl => + if i = 0#u32 + then + let back_'a := fun ret => Result.ret (CList.CCons ret tl) + Result.ret (x, back_'a) + else + do + let i1 ← i - 1#u32 + let (t, list_nth_mut_back) ← list_nth_mut T tl i1 + let back_'a := + fun ret => + do + let tl1 ← list_nth_mut_back ret + Result.ret (CList.CCons x tl1) + Result.ret (t, back_'a) + | CList.CNil => Result.fail .panic + +/- [demo::list_nth_mut1]: loop 0: + Source: 'src/demo.rs', lines 62:0-71:1 -/ +divergent def list_nth_mut1_loop + (T : Type) (l : CList T) (i : U32) : + Result (T × (T → Result (CList T))) + := + match l with + | CList.CCons x tl => + if i = 0#u32 + then + let back_'a := fun ret => Result.ret (CList.CCons ret tl) + Result.ret (x, back_'a) + else + do + let i1 ← i - 1#u32 + let (t, back_'a) ← list_nth_mut1_loop T tl i1 + let back_'a1 := + fun ret => do + let tl1 ← back_'a ret + Result.ret (CList.CCons x tl1) + Result.ret (t, back_'a1) + | CList.CNil => Result.fail .panic + +/- [demo::list_nth_mut1]: + Source: 'src/demo.rs', lines 62:0-62:77 -/ +def list_nth_mut1 + (T : Type) (l : CList T) (i : U32) : + Result (T × (T → Result (CList T))) + := + do + let (t, back_'a) ← list_nth_mut1_loop T l i + Result.ret (t, back_'a) + +/- [demo::i32_id]: + Source: 'src/demo.rs', lines 73:0-73:28 -/ +divergent def i32_id (i : I32) : Result I32 := + if i = 0#i32 + then Result.ret 0#i32 + else do + let i1 ← i - 1#i32 + let i2 ← i32_id i1 + i2 + 1#i32 + +/- Trait declaration: [demo::Counter] + Source: 'src/demo.rs', lines 83:0-83:17 -/ +structure Counter (Self : Type) where + incr : Self → Result (Usize × Self) + +/- [demo::{usize}::incr]: + Source: 'src/demo.rs', lines 88:4-88:31 -/ +def Usize.incr (self : Usize) : Result (Usize × Usize) := + do + let self1 ← self + 1#usize + Result.ret (self, self1) + +/- Trait implementation: [demo::{usize}] + Source: 'src/demo.rs', lines 87:0-87:22 -/ +def demo.CounterUsizeInst : Counter Usize := { + incr := Usize.incr +} + +/- [demo::use_counter]: + Source: 'src/demo.rs', lines 95:0-95:59 -/ +def use_counter + (T : Type) (CounterTInst : Counter T) (cnt : T) : Result (Usize × T) := + CounterTInst.incr cnt + +end demo diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean new file mode 100644 index 00000000..cdec7332 --- /dev/null +++ b/tests/lean/Demo/Properties.lean @@ -0,0 +1,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 -- cgit v1.2.3