Доказательство свойства на множествах - PullRequest
Новая
       4

Доказательство свойства на множествах

0 голосов
/ 21 сентября 2018

Как опыт программирования Coq и следуя моему вопросу в здесь , я хотел бы знать, есть ли другое доказательство, возможно, более короткое и без использования леммы subset_listpair_consver , для доказательства леммы subset_listpair_consFalse .Я доказал это, но это долго и использует лемму subset_listpair_consve. 

Require Import List.
Require Import Bool.

Definition entity := nat.
Definition entityID := nat.
Definition listPair : Set :=
  list (entity * entityID).

   (* check if e is in list l*)
Fixpoint in_listpair e (l : listPair) :=
  match l with
  | nil          => false
  | (x, y) :: l' => Nat.eqb e x || in_listpair e l'
  end.

 (* check if list l1 is in list l2:i.e., 11 entities are in l2*)
Fixpoint subset_listpair (l1 l2 : listPair) :=
  match l1 with
  | nil => true
  | (x1, _) :: l1 => in_listpair x1 l2 && subset_listpair l1 l2
  end.




Lemma subset_listpair_consver l1 l2 l3 e :
 in_listpair e l2 = true->
 in_listpair e l3 = false ->
   subset_listpair l1 l2 = true ->
   subset_listpair l1 l3 = false.
Proof.
Admitted.



Lemma subset_listpair_consFalse l1 l2 l3 :
  subset_listpair l1 l2 = true ->
  subset_listpair l1 l3 = false -> subset_listpair l2 l3=false .
Proof.
induction l1.
induction l3.
destruct l2.
simpl. intros.
inversion H0.
intros. destruct p. simpl in *.  reflexivity.
simpl in *. intros. intuition. inversion H0. 
intros. rewrite IHl1. reflexivity.
simpl in H0.
destruct a. simpl in H.
rewrite andb_true_iff in H.
rewrite andb_false_iff in H0.
elim H. intros. assumption.
simpl in H0.
destruct a. simpl in H.
rewrite andb_true_iff in H.
rewrite andb_false_iff in H0.
elim H. intros.
elim H0. intros.
pose proof ( subset_listpair_consver  ) as H10.
assert ( subset_listpair l1 l3 = false) as H11.
rewrite H10 with (l2:=l2) (e:=e).
reflexivity. assumption. assumption. assumption. assumption.
intro.
assumption.
Qed.

1 Ответ

0 голосов
/ 22 сентября 2018

Вот одно из возможных решений.Я не пошел ни на доказательство без леммы, ни на самое короткое доказательство.Вместо этого я попытался разбить все на куски размером с кусочек, которыми (относительно) легко манипулировать.

Во-первых, вот вспомогательная лемма, отсутствующая в стандартной библиотеке.Он просто устанавливает закон противопоставления в классической логике (у нас здесь есть разрешимые предложения, так что это своего рода классика). 

From Coq Require Import Arith Bool List.

Lemma contra b1 b2 :
  (b2 = false -> b1 = false) <-> (b1 = true -> b2 = true).
Proof. destruct b1, b2; intuition. Qed.

Теперь нам понадобится следующее простое свойство: 

Lemma in_subset_listpair {p l1 l2} :
  in_listpair p l1 = true ->
  subset_listpair l1 l2 = true ->
  in_listpair p l2 = true.
Proof.
  induction l1 as [| [x1 y1] l1 IH]; simpl; [easy|].
  rewrite orb_true_iff, andb_true_iff. intros [->%Nat.eqb_eq|] []; trivial.
  now apply IH.
Qed.

Далее мы докажем, что subset является транзитивным: 

Lemma subset_listpair_transitive l2 l1 l3 :
  subset_listpair l1 l2 = true ->
  subset_listpair l2 l3 = true ->
  subset_listpair l1 l3 = true .
Proof.
  induction l1 as [| [x1 y1] l1 IH]; simpl; trivial.
  intros [I1 S1]%andb_prop S2. rewrite (IH S1 S2), andb_true_r.
  now apply (in_subset_listpair I1).
Qed.

А теперь целевая лемма, которая в основном является контрапозитивным утверждением свойства транзитивности: 

Lemma subset_listpair_consFalse l1 l2 l3 :
  subset_listpair l1 l2 = true ->
  subset_listpair l1 l3 = false ->
  subset_listpair l2 l3 = false .
Proof.
  intros S12; rewrite contra.
  now apply subset_listpair_transitive.
Qed.
...