时间戳

首页 > 解决方案 > 证明在两个列表中找到相同元素的属性

coq - 证明在两个列表中找到相同元素的属性

问题描述

我是 Coq 的新手。我有一个函数findshare可以在两个列表中找到相同的元素。引理sameElements证明了函数findshare在两个列表的连接上的结果等于函数在每个列表上的结果的连接。我有点坚持证明 lemma sameElements。

Require Import List .
Fixpoint findshare(s1 s2: list nat): list nat:=
      match s1 with
        | nil => nil
        | v :: tl =>
           if ( existsb  (Nat.eqb v)  s2)
            then v :: findshare tl s2
            else findshare tl s2
      end.

 Lemma sameElements l1 l2 tl :
  (findshare tl (l1++l2)) =
  (findshare tl (l1))++ (findshare tl (l2)).
Proof.

标签： coq

解决方案

您遇到了麻烦，因为您的陈述并不完全正确：它包含矛盾。更准确地说，它意味着[1; 2] = [2; 1]：

Require Import List .
Fixpoint findshare(s1 s2: list nat): list nat:=
      match s1 with
        | nil => nil
        | v :: tl =>
           if ( existsb  (Nat.eqb v)  s2)
            then v :: findshare tl s2
            else findshare tl s2
      end.

Lemma sameElements l1 l2 tl :
  (findshare tl (l1++l2)) =
  (findshare tl (l1))++ (findshare tl (l2)).
Admitted.

Import ListNotations.

Lemma contra : False.
Proof.
pose proof (sameElements [1] [2] [2;1]).
simpl in H.
discriminate.
Qed.

您应该能够通过tl与和交换来证明引理l1，并通过归纳继续进行。l2l1 ++ l2l1

推荐阅读