diff options
author | Son Ho | 2024-03-19 04:52:36 +0100 |
---|---|---|
committer | Son Ho | 2024-03-19 04:52:36 +0100 |
commit | d6efe5bd2878135bf1fc3fc31fec66322c5b8a86 (patch) | |
tree | d159905f81d12d64ccac0a0a33e2e5b531ca9125 /tests/lean/Demo/Properties.lean | |
parent | a24f42ff7f0ae3c2aeb51decb0d0c90d6e50ffac (diff) |
Update the demo
Diffstat (limited to 'tests/lean/Demo/Properties.lean')
-rw-r--r-- | tests/lean/Demo/Properties.lean | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index cdec7332..e514ac3e 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -65,4 +65,20 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : termination_by x.val.toNat decreasing_by scalar_decr_tac +theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) : + ∃ back, list_tail T l = ret (CList.CNil, back) ∧ + ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by + rw [list_tail] + match l with + | CNil => + simp_all + | CCons hd tl => + simp_all + progress as ⟨ back ⟩ + simp + -- Proving the backward function + intro tl' + progress + simp_all + end demo |