Added more examples of inductive types.

parent 83acccfb
......@@ -15,7 +15,7 @@ theory NatExample : ?LFI =


theory TestExample : ?LFI =
//theory TestExample : ?LFI =
rule rules?InductiveTypes ❙
m : type ❙
......@@ -38,3 +38,58 @@ theory NatExample : ?LFI =
q: {x:a} a ⟶ b x ❙


theory InductivelyDefinedTypes : ?LFI =
inductive nat()❘=
n: type
z: n
s: n ⟶ n

plus: nat/n → nat/n → nat/n ❘ = [m, n] ((nat/induct n (nat/n → nat/n) ([x] x) [u] ([x] nat/s (u x))) m) n ❙
times: nat/n → nat/n → nat/n ❘ = plus: nat/n → nat/n → nat/n ❘ = [m, n] ((nat/induct n (nat/n → nat/n) ([x] ❘) [u] ([x] nat/s (u ❘))) m) n ❙
inductive list(a : type) ❘ =
list: type ❙
nil: list a ❙
cons: a → list a → list a ❙
concat: {a : type} list/list a → list/list a ❘ = [a, l, m] (list/induct_list ((list/list a → list/list a) ([tp, ys] ys) [tp, x, xs] ([l] list_cons t x (l ys))) l) m ❙
single: {a : type} a → list/list a ❘ = [a : type, x : a] list/cons x list/nil ❙
reverse:{a: type} list/list a → list/list a ❘ = [a, l] list/induct_list a (list/list a) ([tp] list/nil tp) [tp, x, xs] concat tp (reverse xs) (single x) ❙
length: {a : type} list/list a → nat/nat ❘ = [a, l] list/induct_list a nat/n ([tp] nat/z) [tp, x, xs] nat/s (length xs) ❙
inductive vector(a: type, n: nat/n) ❘ =
vec: {n: nat/n} type ❙
empty: vec a nat/z ❙
add: {n: nat/n} vec a n → a → vec a (nat/s n) ❙
zip: {a: type, b: type, n: nat/n} vec a n → vec b n → vec (a * b) n ❘ = [a, b, n, l, m] ((vector/induct_vec (a*b)) ([l:vector/vec a n, len: nat/n] vec (a*b) n) ([l: vec a n] ([m: vec b n] vector/empty (a*b))) ([l: vec a n] ([len: nat/n, tlm: vec b n, hdm: b] (vector/induct_vec (a*b) ([lenl: nat/n] vec (a*b) lenl) (vector/empty (a*b)) ([lenl: nat/n, tll: vec a lenl, hdl: a] vector/add a n (zip a b n tll tlm) (hdl, hdm))) l)) l) m ❙
inductive_list2() ❘ =
list: type → type ❙
nil: {a: type} list2 a ❙
cons: {a: type} a → list a → list a ❙
length: {a} list a → nat/n ❙
length_nil: {a: type} length (nil a) ≐ nat/z ❙
length_cons: {a:type, hd: a, tl: list a} length a (cons a hd l) ≐ nat/s (length a tl) (nat/s nat/z) ❙
inductive list3() ❘ =
list: type → type ❙
nil: {a : type} list a ❙
cons: {a : type} a → list a → list a ❙
head: {a : type, l:list a} → ⊦ l ≐ nil a → a
head_cons: {a: type, hd: a, tl: list a, P: ⊦ l ≐ nil} ⊦ head a (cons a hd tl) P ≐ hd ❙
induct freeMonoid(a: type) ❘ =
fm: type ❙
gen: a → fm ❙
unit: fm ❙
comp: fm → fm → fm ❘ # 1 . 2 ❙
assoc: {x: fm, y: fm, z: fm} ⊦ (x . y) . z ≐ x . (y . z) ❙
unit_r: {x: fm} ⊦ x . unit ≐ x❙
unit_l: {x: fm} ⊦ unit . x ≐ x❙
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment