Логика: все определения и теорема All_In - PullRequest
Новая
       15

Логика: все определения и теорема All_In

0 голосов
/ 26 апреля 2019

Вот задача:

Вдохновляясь из [In], напишите рекурсивную функцию [All], утверждающую, что некоторое свойство [P] содержит все элементы списка [l].Чтобы убедиться, что ваше определение верно, докажите лемму [All_In] ниже.(Конечно, ваше определение должно , а не просто переформулировать левую часть [All_In].)

In было определено так: 

Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | [] => False
  | x' :: l' => x' = x \/ In x l'
  end.

Сначала я определил All аналогичным образом: 

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  match l with
  | [] => False
  | x' :: l' => P x' /\ All P l'
  end.

Но потом я подумал, что это неверно, потому что False в конце соединения всегда будет давать False.

Нам нужно игнорировать последний элемент nil списка, если он не пустой (это не работает, просто идея): 

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  match l with
  | [] => False
  | x' :: l' => P x' /\ if l' = [] then True else All P l'
  end.

Ошибка, которую я не знаю, как решить:

Ошибка: термин "l '= []" имеет тип "Prop", который не является (ко) индуктивным.

Затем я возвращаюсь к первомуcase: 

  | x' :: l' => P x' /\ All P l'

и попытайтесь доказать теорему All_In: 

Lemma All_In :
  forall T (P : T -> Prop) (l : list T),
    (forall x, In x l -> P x) <->
    All P l.
Proof.
  intros T P l. split.
  - (* Left to right *)
    intros H. induction l as [| h t IHl].
    + simpl. simpl in H.

Теперь мы застряли: 

T : Type
P : T -> Prop
H : forall x : T, False -> P x
============================
False

Поскольку в выводе есть False, нов этой посылке нет ложной гипотезы, и все утверждение является ложью.

  1. Как правильно определить все?
  2. Что не так с моим доказательством?

1 Ответ

2 голосов
/ 27 апреля 2019

All должно занять [] до True. Это в основном из-за бессмысленной правды , но вы можете видеть, как это не вызывало проблем.

Отсутствие All P [] истинности также делает вашу лемму ложной. Для всех x, In x [] ложно. Но ложь подразумевает все, включая P x, поэтому у нас есть forall x, In x [] -> P x. Но если All P [] ложно, то эти два утверждения не могут быть эквивалентными.

...