BC1e: Logika boolowska

Zadania z funkcji boolowskich, sprawdzające radzenie sobie w pracy z enumeracjami, definiowaniem funkcji przez dopasowanie do wzorca i dowodzeniem przez rozbicie na przypadki.
Chciałem, żeby nazwy twierdzeń odpowiadały tym z biblioteki standardowej, ale na razie nie mam siły tego ujednolicić.

Section boolean_functions.

Variables b b1 b2 b3 : bool.

Definicje

Zdefiniuj następujące funkcje boolowskie:


Notation "b1 && b2" := (andb b1 b2).
Notation "b1 || b2" := (orb b1 b2).

Twierdzenia

Udowodnij, że zdefiniowane przez ciebie funkcje mają spodziewane właściwości.


Właściwości negacji


Lemma negb_inv : negb (negb b) = b.

Lemma negb_ineq : negb b <> b.

Eliminacja


Lemma andb_elim_l : b1 && b2 = true -> b1 = true.

Lemma andb_elim_r : b1 && b2 = true -> b2 = true.

Lemma andb_elim : b1 && b2 = true -> b1 = true /\ b2 = true.

Lemma orb_elim : b1 || b2 = true -> b1 = true \/ b2 = true.

Elementy neutralne


Lemma andb_true_neutral_l : true && b = b.

Lemma andb_true_neutral_r : b && true = b.

Lemma orb_false_neutral_l : false || b = b.

Lemma orb_false_neutral_r : b || false = b.

Anihilacja


Lemma andb_false_l : false && b = false.

Lemma andb_false_r : b && false = false.

Lemma orb_true_l : true || b = true.

Lemma orb_true_r : b || true = true.

Łączność


Lemma andb_assoc : b1 && (b2 && b3) = (b1 && b2) && b3.

Lemma orb_assoc : b1 || (b2 || b3) = (b1 || b2) || b3.

Przemienność


Lemma andb_comm : b1 && b2 = b2 && b1.

Lemma orb_comm : b1 || b2 = b2 || b1.

Rozdzielność


Lemma andb_dist_orb :
  b1 && (b2 || b3) = (b1 && b2) || (b1 && b3).

Lemma orb_dist_andb :
  b1 || (b2 && b3) = (b1 || b2) && (b1 || b3).

Wyłączony środek i niesprzeczność


Lemma andb_negb : b && negb b = false.

Lemma orb_negb : b || negb b = true.

Prawa de Morgana


Lemma negb_andb : negb (b1 && b2) = negb b1 || negb b2.

Lemma negb_orb : negb (b1 || b2) = negb b1 && negb b2.

eqb, xorb, norb, nandb


Lemma eqb_spec : eqb b1 b2 = true -> b1 = b2.

Lemma eqb_spec' : eqb b1 b2 = false -> b1 <> b2.

Lemma xorb_spec :
  xorb b1 b2 = negb (eqb b1 b2).

Lemma xorb_spec' :
  xorb b1 b2 = true -> b1 <> b2.

Lemma norb_spec :
  norb b1 b2 = negb (b1 || b2).

Lemma nandb_spec :
  nandb b1 b2 = negb (b1 && b2).

Różne


Lemma andb_eq_orb :
  b1 && b2 = b1 || b2 -> b1 = b2.

Lemma all3_spec :
  (b1 && b2) || (negb b1 || negb b2) = true.

Lemma noncontradiction_bool :
  negb (eqb b (negb b)) = true.

Lemma excluded_middle_bool :
  b || negb b = true.

End boolean_functions.

Zadania

majority

Zdefiniuj funkcję majority, która bierze 3 wartości boolowskie i zwraca wartość boolowską. Jeśli co najmniej dwa z trzech argumentów to true, to wynikiem funkcji jest true. W przeciwnym wypadku wynikiem jest false.
Użyj wyłącznie dopasowania do wzorca - nie używaj żadnych zdefiniowanych wcześniej funkcji.
Następnie udowodnij kilka właściwości funkcji majority.

Definition majority (a b c : bool) : bool :=
match a, b, c with
| true , true , true => true
| x , false, true => x
| true , y , false => y
| false, true , z => z
| false, false, false => false
end.

Lemma majority_spec :
  forall a b c : bool,
    majority a b c = andb (orb a b) (andb (orb b c) (orb c a)).

Lemma majority_spec' :
  forall a b c : bool,
    majority a b c = orb (andb a b) (orb (andb b c) (andb c a)).

Lemma negb_majority :
  forall a b c : bool,
    negb (majority a b c) = majority (negb a) (negb b) (negb c).

Lemma majority_orb :
  forall a1 a2 b c : bool,
    majority (orb a1 a2) b c = orb (majority a1 b c) (majority a2 b c).

Lemma majority_andb :
  forall a1 a2 b c : bool,
    majority (andb a1 a2) b c = andb (majority a1 b c) (majority a2 b c).

Lemma majority_permute :
  forall a b c : bool,
    majority a b c = majority b c a.

Lemma majority_swap :
  forall a b c : bool,
    majority a b c = majority b a c.

Logika ternarna

Wymyśl logikę trójwartościową. W tym celu: