michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lua): add is_sorted inductive predicate example

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-30 11:18:50 -07:00
parent 128d668f03
commit 6587d0f8f3
1 changed files with 31 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
tests/lua/sorted.lua Normal file
View file

@ -0,0 +1,31 @@
local env = environment()
local l = mk_param_univ("l")
local A = Local("A", mk_sort(l))
local U_l = mk_sort(l)
local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop
local list_l = Const("list", {l}) -- list.{l}
env = add_inductive(env,
"list", {l}, 1, Pi(A, U_l, U_l1),
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
local cons_l = Const("cons", {l})
local nil_l = Const("nil", {l})
local is_sorted_l = Const("is_sorted", {l})
local a = Local("a", A)
local lt = Local("lt", mk_arrow(A, A, Bool))
local a1 = Local("a1", A)
local a2 = Local("a2", A)
local t = Local("t", list_l(A))
local Hlt = Local("H", lt(a1, a2))
local Hs = Local("Hs", is_sorted_l(A, lt, cons_l(A, a2, t)))
env = add_inductive(env,
"is_sorted", {l}, 2, Pi({A, lt}, mk_arrow(list_l(A), Bool)),
"is_sorted_nil", Pi({A, lt}, is_sorted_l(A, lt, nil_l(A))),
"is_sorted_cons_nil", Pi({A, lt, a}, is_sorted_l(A, lt, cons_l(A, a, nil_l(A)))),
"is_sorted_cons_cons", Pi({A, lt, a1, a2, t, Hlt, Hs}, is_sorted_l(A, lt, cons_l(A, a1, cons_l(A, a2, t)))))
print(env:find("is_sorted_rec"):type())