2. Falso

Coq Anarchy Proof

Anarchy Proof 二題目です．矛盾からはなんでも証明できるというやつです．

矛盾に対応する False は，何も規則がひとつもない inductive type として定義されています．なので，H: False という仮定があれば，inversion H するだけでなんでも証明できてしまいます．

これと同じ事をする tactic として exfalso (=elimtype False) があります．exfalso をすると，goal が False になります．なので今回は，exfalso をしてから Falso を適用するだけで証明できます．と思ったんですが， 残念ながら Anarchy Proof の Coq のバージョンが古いようで exfalso はないみたいです．というわけで今回の解答は下の通り．

Require Import Definitions.

Theorem Fermat's_Last_Theorem:
  forall (a b c n: nat), n > 2 -> pow a n + pow b n = pow c n ->
  a = 0 /\ b = 0 /\ c = 0.
Proof.
  elimtype False.
  exact Falso.
Qed.