fixedpoint.jp

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.