Ltac 仮定をおく := intros.
Ltac 仮定を使う := assumption.
Ltac 条件文を使う H1 H2 := apply H1 in H2.
Ltac 場合分けをする H := destruct H.
Ltac 連言を分解 H := destruct H.
Ltac 矛盾 := contradiction.


Section Puzzle.

Variables 太郎は犯人である
          次郎は犯人である
          花子は犯人である
          : Prop.

(* 一つ目のパズルを解く：
   三つの証言を仮定して，そこから「太郎は犯人である」を導く *)
Theorem puzzle1 : (太郎は犯人である \/ 次郎は犯人である) ->
  (次郎は犯人である -> 花子は犯人である) ->
  ~ 花子は犯人である ->
  太郎は犯人である.
Proof.
  仮定をおく.  (* 三つの証言を仮定する *)
  場合分けをする H.  (* 太郎が犯人である場合 or 次郎が犯人である場合 *)
  仮定を使う.
  条件文を使う H0 H.  (* A -> B と A から B を導く *)
  矛盾.  (* 次郎が犯人である場合はありえない *)
Qed.

(* Coqを用いて書いた証明はプログラムにもなっている *)
Print puzzle1.

(* 二つ目のパズルを解く：
   三つの証言を仮定して，そこから矛盾 False を導く
   ここは参考程度に眺めてもらえばOK
   デフォルトでは以下のように英単語のコマンドを用いる
   このようなコマンドは「タクティク」と呼ばれる *)
Theorem puzzle2 : (次郎は犯人である /\ ~ 太郎は犯人である) ->
  ~ (次郎は犯人である /\ 花子は犯人である) ->
  (~ 花子は犯人である -> 太郎は犯人である) ->
  False.
Proof.
  intros.
  destruct H.
  assert (~ 花子は犯人である).
  intro.
  apply H0.
  split; assumption.
  apply H1 in H3.
  contradiction.
Qed.
  
Print puzzle2.

End Puzzle.


Section Exercises.

Variables 雨が降る
          地面が濡れる
          運動会が中止になる
          お弁当が売れ残る
          : Prop.

(* 次の三つの仮定

   雨が降る -> 地面が濡れる
   地面が濡れる -> 運動会が中止になる
   運動会が中止になる -> お弁当が売れ残る

   から

   雨が降る -> お弁当が売れ残る

   を導いてみよう *)
Theorem claim1 : (雨が降る -> 地面が濡れる) ->
  (地面が濡れる -> 運動会が中止になる) ->
  (運動会が中止になる -> お弁当が売れ残る) ->
  (雨が降る -> お弁当が売れ残る).
Proof.
  仮定をおく.
  条件文を使う H H2.
Admitted.

Variables バスに乗る
          電車に乗る
          試験に遅刻する
          : Prop.

(* 次の三つの仮定

   バスに乗る -> 試験に遅刻する
   電車に乗る -> 試験に遅刻する
   バスに乗る \/ 電車に乗る

   から

   試験に遅刻する

   を導いてみよう *)
Theorem claim2 : (バスに乗る -> 試験に遅刻する) ->
  (電車に乗る -> 試験に遅刻する) ->
  バスに乗る \/ 電車に乗る ->
  試験に遅刻する.
Proof.
  仮定をおく.
Admitted.

End Exercises.