Подмножества списка нац в Coq

Я определил рекурсивную функцию для всех подмножеств nat_list в Coq, какПодмножества списка нац в Coq

Fixpoint subsets (a: list nat) : (list (list nat)) := 
match a with 
    |[] => [[]] 
    |h::t => subsets t ++ map (app [h]) (subsets t) 
end.

Я пытаюсь доказать, что

forall (a:list nat), In [] (subsets a).

Я пытался индукцию по а. Базовый корпус был прямым. Однако в индукционном случае я попытался использовать встроенную теорему in_app_or.

Unable to unify "In ?M1396 ?M1394 \/ In ?M1396 ?M1395" with 
"(fix In (a : list nat) (l : list (list nat)) {struct l} : Prop := 

match l with 
| [] => False 
| b :: m => b = a \/ In a m  
end)               
[] (subsets t ++ map (fun m : list nat => h :: m) (subsets t))".

Как доказать такую теорему или решить такую проблему?

источник

2016-12-03 Dhananjay Raju

Примечания о вашем наименовании ваша функция не возвращает «подмножество» в смысле списка списков, не имеющих тех же свойств, что и набор списков. В частности, сделайте списки '[a; b] 'и' [b; a] 'представляют один и тот же набор? Думаю об этом! – ejgallego

Для чего это стоит, в этом случае «индукция l; просто, интуиция» также является веским доказательством. –

Проблема in_app_or в том, что это имеет следующий вид:

forall (A : Type) (l m : list A) (a : A), 
    In a (l ++ m) -> In a l \/ In a m

и применение чешуй к цели работ «назад»: Coq соответствует последовательное B импликации A -> B с целью, и если они могут быть объединены, вы остаетесь с новой целью: вам нужно доказать (более сильное) утверждение A. А в вашем случае A и B находятся в неправильном порядке (местами), так что вам нужно применить in_or_app вместо:

in_or_app : forall (A : Type) (l m : list A) (a : A), 
    In a l \/ In a m -> In a (l ++ m)

Это, как ваша цель может быть доказано с помощью in_or_app:

Goal forall (a:list nat), In [] (subsets a). 
    intros. 
    induction a; simpl; auto. 
    apply in_or_app; auto. 
Qed.

источник

2016-12-03 12:34:23

ответ

Смежные вопросы