Coq中的列表nat的子集

Dhananjay raju

我为coq中的nat_list的所有子集定义了一个递归函数,如下所示:

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))".

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

安东·特鲁诺夫(Anton Trunov)

问题in_app_or在于它具有以下类型:

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

引理在目标上的应用是“向后的”:CoqB将隐含的结果A -> B与目标匹配,如果可以将它们统一,那么您将得到一个新的目标:您需要证明(更强的)陈述A并且在您的情况下,AandB的顺序错误(交换),因此您需要申请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.

本文收集自互联网,转载请注明来源。

如有侵权,请联系 [email protected] 删除。

编辑于
0

我来说两句

0 条评论
登录 后参与评论

相关文章