Поиск списка по List.filter - PullRequest
Новая
       9

Поиск списка по List.filter

0 голосов
/ 02 марта 2019

В моей программе я использую List.filter для поиска в списке для поиска определенных элементов.Я докажу, что если List.filter найдет какие-то элементы в списке, то, добавив другой список, мы все равно получим те элементы, которые были в первом списке до добавления.Я немного застрял в доказательстве filterKeepSameElementsAfterAppending.Чтобы сделать мою программу короче, я изменил данные своей программы на customType и mydata. 

 Require Import  List Nat.
 Inductive customType : Type :=
  |Const1:  nat -> customType
  |Const2: list nat -> customType.

Inductive mydata : Set :=
   |Set1: customType * customType ->mydata
   |Set2: customType ->mydata.

   Fixpoint custome_Equal (c1 c2:customType) :bool:=
        match c1 with
            |Const1 nt => match c2 with 
                       |Const1 mt =>  eqb nt  mt
                       |Const2 (hm::lmt) => eqb nt hm
                      | _ => false
                                     end
           |Const2 (hn::lnt) => match c2 with                                                                            
                           |Const1 mt => eqb  hn  mt
                           |Const2 (hm:: lmt) => eqb hn  hm
                           | _ => false
                                     end
           | _ => false
          end.

 Fixpoint Search (l: mydata) (t:customType):  bool :=
    match l with
       |Set1 (a1, a2) =>  if (custome_Equal a2 t)  then  true else false
       | _=>false
    end.

Lemma filterKeepSameElementsAfterAppending(l1 l2: list mydata)(x:mydata)(ta:customType):
In x (filter (fun n => Search n ta) (l1)) -> In x (filter (fun n  => Search n ta) (l2++ l1)).
Proof.
intro.

1 Ответ

0 голосов
/ 02 марта 2019

Лемма filter_cat должна вдохновлять вас: 

filter_cat
   forall (T : Type) (a : pred T) (s1 s2 : seq T),
   [seq x <- s1 ++ s2 | a x] = [seq x <- s1 | a x] ++ [seq x <- s2 | a x]

вместе с mem_cat должны делать то, что вы хотите: 

mem_cat
   forall (T : eqType) (x : T) (s1 s2 : seq T),
   (x \in s1 ++ s2) = (x \in s1) || (x \in s2)

Полный код: 

From mathcomp Require Import all_ssreflect.

Lemma mem_filter_cat (T : eqType) p (l1 l2 : seq T) x :
  x \in filter p l1 -> x \in filter p (l1 ++ l2).
Proof. by rewrite filter_cat mem_cat => ->. Qed.
...