coq 中列表 nat 的子集

Question

我在 coq 中为 nat_list 的所有子集定义了一个递归函数 as

Fixpoint subsets (a: list nat) : (list (list nat)) :=
 match a with
  |[] => [[]]
  |h::t => subsets t ++ map (app [h]) (subsets t)
end.

我试图证明

forall (a:list nat), In [] (subsets a).

我试着归纳了一个。基本情况很简单。然而在归纳案例中，我尝试使用内置定理 in_app_or。

Unable to unify "In ?M1396 ?M1394 \/ In ?M1396 ?M1395" with
"(fix In (a : list nat) (l : list (list nat)) {struct l} : Prop := 

match l with
| [] => False
| b :: m => b = a \/ In a m     
end)                                                         
[] (subsets t ++ map (fun m : list nat => h :: m) (subsets t))".

如何证明这样的定理或解决这样的问题？

Answer 1

in_app_or 的问题是具有以下类型：

forall (A : Type) (l m : list A) (a : A),
  In a (l ++ m) -> In a l \/ In a m

引理对目标的应用有效 "backwards"：Coq 将蕴涵 A -> B 的结果 B 与目标相匹配，如果它们可以统一，则剩下有一个新的目标：你需要证明一个（更强的）陈述 A。在您的情况下，A 和 B 的顺序错误（交换），因此您需要改为应用 in_or_app：

in_or_app : forall (A : Type) (l m : list A) (a : A),
  In a l \/ In a m -> In a (l ++ m)

这就是如何使用 in_or_app 证明您的目标：

Goal forall (a:list nat), In [] (subsets a).
  intros.
  induction a; simpl; auto.
  apply in_or_app; auto.
Qed.

coq 中列表 nat 的子集

Subsets of list nat in coq

coq

theorem-proving