1

lequivColor 库 中的等价定义 ( )：http: //color.inria.fr/doc/CoLoR.Util.List.ListUtil.html

Require Import List.
Variable A : Type.
Definition lequiv (l1 l2: list A) : Prop := l1 [= l2 /\ l2 [= l1.
Infix "[=]" := lequiv (at level 70).

我想证明下面的引理。这是我的证明：

Lemma equiv_app_equiv: forall l1 l2 l3 : list A, l1 ++ l2 [=] l3 -> 
l1 [=] l3 /\ l2 [=] l3.
Proof.
unfold lequiv in |- *; simpl in |- *. intuition.
apply incl_appr_incl in H0. apply H0.

  A : Type
  l1 : list A
  l2 : list A
  l3 : list A
  H0 : l1 ++ l2 [=l3
  H1 : l3 [=l1 ++ l2
  ============================
   l3 [=l1

在这个目标上，我不知道如何走得更远，我想知道H1: l3 [= l1 ++ l2它可以重写为的假设：l3 [= l1 /\ l3 [= l2？我在 Coq 的库（List).

请你帮助我好吗？我的引理中缺少什么吗？它可以证明吗？非常感谢你。

4

1 回答 1

0
于 2013-01-14T14:09:27.133 回答