CODEWITHSUNDEEP
coq
Tom And.
Tom And.

Reputation: 125

Proving a property of Subset relation on list of pairs

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.

Upvotes: 0

Views: 72

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

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.

Upvotes: 1

Related Questions