在对列表上证明子集关系的一个属性 [英] Proving a property of Subset relation on list of pairs

问题描述

我正在证明有关子集的简单数学属性，例如：A子集B；这与以下事实有关：将成员添加到集合B不会影响此关系。在程序中，A和B是对的列表。 entity_IN_listPair 检查特定对是否在配对列表中，而 listPairEqual 检查两个配对对是否相等。我有点卡住了如何进行引理的证明引理addtolistPairSUB ：

I'm proving a simple mathematical property about subsets, for example : A subset B; which is about the fact that adding a member to set B cannot affect this relation. In the program, A and B are list of pairs. entity_IN_listPair checks if a specific pair is in a list of pair and listPairEqual checks equality of two list of pairs. I am a bit stuck how to proceed in the proof of lemma Lemma addtolistPairSUB:

Require Import List.
Require Import Bool.

Definition entity := nat.
Definition entityID := nat.
Definition listPair : Set :=
   list  (entity * entityID).

(* Nat equality *)
Fixpoint Entity_eq (X:_) (a b:_) : bool :=
   match a with
  | O => match b with
         | O => true
         | S m' => false
         end
  | S n' => match b with
            | O => false
            | S m' => ( Entity_eq nat (n')( m'))
            end
    end.

(* checking if an  entity is in an listPair *)
Fixpoint  entity_IN_listPair
  (entit: entity ) (lispair: listPair) : bool :=
match lispair with 
  |first::body =>               match first with
                                        |(p_one,ptwo)=> (Entity_eq (nat)(entit)(p_one )) 
                                             ||  entity_IN_listPair entit body

                                       end
 |nil => false
 end.

(* checking the equality of two listPair *)
Fixpoint  listPairSUB
           (first second: listPair) : bool :=
   match first with 
  |head::tail => match head with
                                 |(part1,part2)=> if (entity_IN_listPair part1 second)
                                                 then  listPairSUB tail second
                                                 else false
                                 end
   |nil => true
       end. 

Definition listPairEqual (firstL secondL:listPair) :=
   (listPairSUB firstL secondL) && (listPairSUB secondL firstL).

 Lemma  addtolistPairSUB: 
 forall (a b: listPair ) (c:entity * entityID),
        listPairSUB a b = true->listPairSUB (a) (c::b) = true .
Proof.
induction a.

推荐答案

在这里。 （我自由地重构了您的代码。）

Here it is. (I took the liberty of refactoring your code a little bit.)

Require Import List.
Require Import Bool.

Definition entity := nat.
Definition entityID := nat.
Definition listPair : Set :=
  list (entity * entityID).

Fixpoint in_listpair e (l : listPair) :=
  match l with
  | nil          => false
  | (x, y) :: l' => Nat.eqb e x || in_listpair e l'
  end.

Fixpoint subset_listpair (l1 l2 : listPair) :=
  match l1 with
  | nil => true
  | (x1, _) :: l1 => in_listpair x1 l2 && subset_listpair l1 l2
  end.

Lemma subset_listpair_cons l1 l2 p :
  subset_listpair l1 l2 = true ->
  subset_listpair l1 (p :: l2) = true.
Proof.
induction l1 as [|[x1 y1] l1 IH]; simpl; trivial.
destruct p as [x2 y2]; simpl.
destruct (in_listpair x1 l2); simpl; try easy.
intros H; rewrite IH; trivial.
now rewrite orb_true_r.
Qed.

这篇关于在对列表上证明子集关系的一个属性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！