证明在两个列表中找到相同元素的性质 [英] Prove a property of finding the same elements in two lists

问题描述

我是Coq的新手.我有一个 findshare 函数，该函数在两个列表中查找相同的元素.引理 sameElements 证明函数 findshare 的结果在两个列表的串联上等于对每个列表应用的函数的结果串联.我在证明引理 sameElements 上有些卡住.

I'm new to Coq. I have a function findshare which finds the same elements in two lists. Lemma sameElements proves that the result of function findshare on the concatenation of two lists is equal to the concatenation of the results of the function applied to each one of them. I'm a bit stuck in proving 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.

推荐答案

您遇到了麻烦，因为您的陈述不太正确:这带来了矛盾.更确切地说，它暗示 [1;2] = [2;1] :

You are having trouble because the statement you have is not quite correct: it entails a contradiction. More precisely, it implies that [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 ， l2 和 l1 ++ l2 ，然后在 l1 上进行归纳.

You should be able to prove the lemma by swapping tl with l1, l2 and l1 ++ l2, and proceeding by induction on l1.

这篇关于证明在两个列表中找到相同元素的性质的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！