NyaOJ

题目描述

prefixes 函数计算了一个列表的所有前缀。例如：

prefixes [1, 2] = [[], [1], [1, 2]]

prefixes [0, 1, 2] = [] :: map (cons 0) (prefixes [1, 2])
                   = [] :: [0 :: [], 0 :: [1], 0 :: [1, 2]]
                   = [[], [0], [0, 1], [0, 1, 2]]

任务

请证明 prefixes l 中的确实是 l 的全部前缀：

1. in_prefixes (20 分)

theorem in_prefixes {A : Type} (l1 l2 : List A) : l1 ∈ prefixes (l1 ++ l2)

2. in_prefixes_inv (20 分)

theorem in_prefixes_inv {A : Type} (l1 l : List A) :
    l1 ∈ prefixes l → ∃ l2, l1 ++ l2 = l

sublists 定义了列表中的所有连续段。请证明 sublists l 的元素确实是 l 中的所有连续段。

提示：必要时可以添加并证明一些前置引理帮助完成证明。

3. in_sublists (30 分)

theorem in_sublists {A : Type} (l1 l2 l3 : List A) :
    l2 ∈ sublists (l1 ++ l2 ++ l3)

4. in_sublists_inv (30 分)

theorem in_sublists_inv {A : Type} (l1 l : List A) :
    l1 ∈ sublists l → ∃ l2 l3, l2 ++ l1 ++ l3 = l

分值

in_prefixes: 20 分
in_prefixes_inv: 20 分
in_sublists: 30 分
in_sublists_inv: 30 分

总计: 100 分