Пересечение списков с использованием List.filter - PullRequest
Новая
       6

Пересечение списков с использованием List.filter

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

Следуя моему вопросу здесь , я доказываю, что пересечение двух списков не пусто, добавляя еще один список в каждый из списков, но пересечение будет не пустым.Интересно, как мне доказать лемму filterKeepIntersection.Я пытаюсь решить ее с помощью тактики filter_cat из библиотеки seq, но, похоже, недостаточно доказать эту лемму. 

 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.

Fixpoint search2 (c1 c2:mydata) :bool:=
         match c1,c2  with
       |Set1 (a1, a2) ,Set1(a3,a4)=>  if (custome_Equal a2 a4)  then  true else false
       | _,_=>false
    end.


Lemma filterKeepIntersection(l1 l2 l3 l4: list mydata):
(List.filter (fun n => List.existsb (search2 n) l2) l1) <> nil->
(List.filter (fun n => List.existsb (search2 n) (l3++l2)) (l4++l1))<>nil.
Proof.

1 Ответ

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

Небольшая переформулировка вашего внутреннего предиката с точки зрения predI плюс использование filter_predI делает доказательство немедленным, но может просто использовать mem_filter напрямую.

...