3値論理

clojure.contrib.typesの使い方がいまいち分からない。
もうちょっと賢いマッチングしてくれないのかな。

(use '[clojure.contrib.types])

(defn not-3 [x]
  (match [x]
         [:yes] :no
         [:no] :yes
         [:maybe] :maybe))

(defn and-3 [x y]
  (match [x y]
         [:yes :yes] :yes
         [:yes :no] :no
         [:yes :maybe] :maybe
         [:no :yes] :no
         [:no :no] :no
         [:no :maybe] :no
         [:maybe :yes] :maybe
         [:maybe :no] :no
         [:maybe :maybe] :maybe))

(defn or-3 [x y]
  (match [x y]
         [:yes :yes] :yes
         [:yes :no] :yes
         [:yes :maybe] :yes
         [:no :yes] :yes
         [:no :no] :no
         [:no :maybe] :maybe
         [:maybe :yes] :yes
         [:maybe :no] :maybe
         [:maybe :maybe] :maybe))

なんでこんなものを書いたのかというと、
第4回FormalMethods勉強会のCoq編で、
3値論理の交換則と分配則を証明したから。

Inductive truth : Set :=
| Yes
| No
| Maybe.

Definition not_t (t: truth) : truth :=
match t with
| Yes => No
| No => Yes
| Maybe => Maybe
end.

Definition and_t (t1 t2: truth): truth :=
match t1,t2 with
| Yes, Yes => Yes
| No,_ => No
| _,No => No
| _,_ => Maybe
end.

Definition or_t (t1 t2:truth): truth :=
match t1,t2 with
| _,Yes => Yes
| Yes,_ => Yes
| _,Maybe => Maybe
| Maybe,_ => Maybe
| _,_ => No
end.

Eval compute in (or_t Yes Yes).
Eval compute in (and_t Yes Maybe).

Theorem and_t_commutative : forall t1 t2:truth, and_t t1 t2 = and_t t2 t1.
intros.
induction t1;
induction t2;
reflexivity.
Qed.
Print and_t_commutative.

Theorem or_t_commutative : forall t1 t2:truth, or_t t1 t2 = or_t t2 t1.
intros.
induction t1;
induction t2;
reflexivity.
Qed.
Print or_t_commutative.

Theorem and_t_or_t_distributive : 
  forall t1 t2 t3: truth,
    and_t t1 (or_t t2 t3) = or_t (and_t t1 t2) (and_t t1 t3).
intros.
induction t1; induction t2; induction t3; reflexivity.
Qed.
Print and_t_or_t_distributive.

男気のある証明（力業で全件検証）に、参加者一同、感動したのでした。