Проверьте непересекающиеся списки в coq - PullRequest
Новая
       17

Проверьте непересекающиеся списки в coq

0 голосов
/ 06 июля 2019 
    I have a different groups of natural numbers(sn1 ,sn2…   snn).

Я передаю / передаю эту группу функции, которая преобразует эту группу в Список. Я хочу доказать, что эти списки не пересекаются. Я определил теоремы о непересекающемся списке. Но у меня есть проблема в доказательстве леммы. , 1. Достаточно ли базовых теорем о непересекающихся списках для доказательства требуемой леммы? 2. Я должен добавить некоторые основные теоремы о непересекающихся множествах? 

Lemma mutualexc: forall (sn1 sn2 bmax snmax:nat), 
  let g1 := group sn1 bmax snmax in 
  let g2 := group sn2 bmax snmax in 
  let list1 := f (fst(g1)) (snd(g1))  ((snd(g1)) - (fst(g1))) in
  let list2 := f (fst(g2)) (snd(g2))  ((snd(g2)) - (fst(g2))) in
  sn1 <> sn2 -> disjoint list1 list2. 



intros. induction list1 as [|t l1] .
 apply disjoint_nil_l. apply disjoint_cons_l.
 unfold disjoint . 
unfold disjoint.`
...