Доказательство свойства отношения Подмножество в списке пар - PullRequest
Новая
       10

Доказательство свойства отношения Подмножество в списке пар

0 голосов
/ 06 сентября 2018

Я доказываю простое математическое свойство для подмножеств, например: A подмножество B; о том, что добавление члена в набор B не может повлиять на это отношение. В программе A и B - список пар. entity_IN_listPair проверяет, есть ли конкретная пара в списке пар, а listPairEqual проверяет равенство двух списков пар. Я немного застрял, как действовать в доказательстве леммы 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.

1 Ответ

0 голосов
/ 06 сентября 2018

Вот оно.(Я позволил себе немного реорганизовать ваш код.) 

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.
...