fixedpoint.jp - 「ライオンとユニコーン」のパズルをCoqで解く




「ライオンとユニコーン」のパズルをCoqで解く

「ライオンとユニコーン」と呼ばれるパズルは以下のようなものです:

Lion lies on Monday, Tuesday and Wednesday. Unicorn lies on Thursday, Friday and Saturday. Both tell truth on other days. Both say yesterday was one of their lying days. Prove that today is Thursday.

(TPTP Problem File: PUZ005-1.p から引用)

この答えを Coq で証明するにはさまざまな形の公理化が考えられますが、以下のものは証明に排中律を使わずに済むものです(Coq 8.4pl4で確認):

lion_and_unicorn.v
Module LionAndUnicorn.

Inductive animal : Set :=
| lion : animal
| unicorn : animal.

Inductive day_of_week : Set :=
| monday : day_of_week
| tuesday : day_of_week
| wednesday : day_of_week
| thursday : day_of_week
| friday : day_of_week
| saturday : day_of_week
| sunday: day_of_week.

Definition yesterday (D : day_of_week) : day_of_week :=
  match D with
    | monday => sunday
    | tuesday => monday
    | wednesday => tuesday
    | thursday => wednesday
    | friday => thursday
    | saturday => friday
    | sunday => saturday
  end.

Definition lying_day (A : animal) (D : day_of_week) : Prop :=
  match A with
    | lion => match D with
                | monday => True
                | tuesday => True
                | wednesday => True
                | thursday => False
                | friday => False
                | saturday => False
                | sunday => False
              end
    | unicorn => match D with
                | monday => False
                | tuesday => False
                | wednesday => False
                | thursday => True
                | friday => True
                | saturday => True
                | sunday => False
                 end
  end.

Parameter says_it_is_a_lying_day : animal -> day_of_week -> Prop.

Parameter today : day_of_week.

Axiom tell_lie_on_lying_day:
  forall A : animal,
    lying_day A today -> forall D : day_of_week, (says_it_is_a_lying_day A D -> ~ lying_day A D).

Axiom tell_truth_on_non_lying_day:
  forall A : animal,
    ~ lying_day A today -> forall D : day_of_week, (says_it_is_a_lying_day A D -> lying_day A D).

Lemma lion_tells_lie_today:
  lying_day lion today -> forall D : day_of_week, (says_it_is_a_lying_day lion D -> ~ lying_day lion D).
Proof.
  apply tell_lie_on_lying_day.
Qed.

Lemma lion_tells_truth_today:
  ~ lying_day lion today -> forall D : day_of_week, (says_it_is_a_lying_day lion D -> lying_day lion D).
Proof.
  apply tell_truth_on_non_lying_day.
Qed.

Lemma unicorn_tells_truth_today:
  ~ lying_day unicorn today -> forall D : day_of_week, (says_it_is_a_lying_day unicorn D -> lying_day unicorn D).
Proof.
  apply tell_truth_on_non_lying_day.
Qed.

Lemma l_tuesday:
  says_it_is_a_lying_day lion (yesterday today) -> today <> tuesday.
Proof.
  intro H.
  intro G.
  assert (lying_day lion today) as F.
  rewrite G.
  simpl.
  tauto.
  assert (monday = (yesterday today)) as E.
  rewrite G.
  reflexivity.
  rewrite <- E in H.
  assert (~ lying_day lion monday) as D.
  apply lion_tells_lie_today.
  exact F.
  exact H.
  apply D.
  simpl.
  tauto.
Qed.

Lemma l_wednesday:
  says_it_is_a_lying_day lion (yesterday today) -> today <> wednesday.
Proof.
  intro H.
  intro G.
  assert (lying_day lion today) as F.
  rewrite G.
  simpl.
  tauto.
  assert (tuesday = (yesterday today)) as E.
  rewrite G.
  reflexivity.
  rewrite <- E in H.
  assert (~ lying_day lion tuesday) as D.
  apply lion_tells_lie_today.
  exact F.
  exact H.
  apply D.
  simpl.
  tauto.
Qed.

Lemma l_friday:
  says_it_is_a_lying_day lion (yesterday today) -> today <> friday.
Proof.
  intro H.
  intro G.
  assert (~ lying_day lion today) as F.
  rewrite G.
  simpl.
  tauto.
  assert (thursday = (yesterday today)) as E.
  rewrite G.
  reflexivity.
  rewrite <- E in H.
  assert (lying_day lion thursday) as D.
  apply lion_tells_truth_today.
  exact F.
  exact H.
  apply D.
Qed.

Lemma l_saturday:
  says_it_is_a_lying_day lion (yesterday today) -> today <> saturday.
Proof.
  intro H.
  intro G.
  assert (~ lying_day lion today) as F.
  rewrite G.
  simpl.
  tauto.
  assert (friday = (yesterday today)) as E.
  rewrite G.
  reflexivity.
  rewrite <- E in H.
  assert (lying_day lion friday) as D.
  apply lion_tells_truth_today.
  exact F.
  exact H.
  apply D.
Qed.

Lemma l_sunday:
  says_it_is_a_lying_day lion (yesterday today) -> today <> sunday.
Proof.
  intro H.
  intro G.
  assert (~ lying_day lion today) as F.
  rewrite G.
  simpl.
  tauto.
  assert (saturday = (yesterday today)) as E.
  rewrite G.
  reflexivity.
  rewrite <- E in H.
  assert (lying_day lion saturday) as D.
  apply lion_tells_truth_today.
  exact F.
  exact H.
  apply D.
Qed.

Lemma u_monday:
  says_it_is_a_lying_day unicorn (yesterday today) -> today <> monday.
Proof.
  intro H.
  intro G.
  assert (~ lying_day unicorn today) as F.
  rewrite G.
  simpl.
  tauto.
  assert (sunday = (yesterday today)) as E.
  rewrite G.
  reflexivity.
  rewrite <- E in H.
  assert (lying_day unicorn sunday) as D.
  apply unicorn_tells_truth_today.
  exact F.
  exact H.
  apply D.
Qed.

Theorem it_is_thursday_if_both_say_yesterday_was_one_of_their_lying_days:
  (forall A : animal, says_it_is_a_lying_day A (yesterday today)) -> today = thursday.
Proof.
  intro H.
  assert (says_it_is_a_lying_day lion (yesterday today)) as H0.
  apply H.
  assert (says_it_is_a_lying_day unicorn (yesterday today)) as H1.
  apply H.
  cut (today <> sunday).
  cut (today <> saturday).
  cut (today <> friday).
  cut (today <> wednesday).
  cut (today <> tuesday).
  cut (today <> monday).

  case today.
  (* monday *)
  intro G0.
  exfalso.
  apply G0.
  reflexivity.
  (* tuesday *)
  intro G0.
  intro G1.
  exfalso.
  apply G1.
  reflexivity.
  (* wednesday *)
  intro G0.
  intro G1.
  intro G2.
  exfalso.
  apply G2.
  reflexivity.
  (* thursday *)
  intros.
  reflexivity.
  (* friday *)
  intro G0.
  intro G1.
  intro G2.
  intro G3.
  exfalso.
  apply G3.
  reflexivity.
  (* saturday *)
  intro G0.
  intro G1.
  intro G2.
  intro G3.
  intro G4.
  exfalso.
  apply G4.
  reflexivity.
  (* sunday *)
  intro G0.
  intro G1.
  intro G2.
  intro G3.
  intro G4.
  intro G5.
  exfalso.
  apply G5.
  reflexivity.

  apply u_monday.
  exact H1.
  apply l_tuesday.
  exact H0.
  apply l_wednesday.
  exact H0.
  apply l_friday.
  exact H0.
  apply l_saturday.
  exact H0.
  apply l_sunday.
  exact H0.
Qed.

End LionAndUnicorn.

© 2006-2015 fixedpoint.jp