Logic_five_not_even.v

Definition five_not_even' : ~ ev 5 :=
  fun (Hev5 : ev 5) =>
    (fun (P : nat -> Prop)                                       (* evの帰納法の原理*)
         (f : P 0)
         (f0 : forall n : nat, ev n -> P n -> P (S (S n))) =>
            fix F (n : nat) (e : ev n) {struct e} : P n :=       (* eについて減少 *)
              match e in (ev n0) return (P n0) with
              | ev_0 => f
              | ev_SS n1 ev1 => f0 n1 ev1 (F n1 ev1)
              end)
    (fun n : nat => ev (S n) -> False)
    (fun ev1 : ev 1 =>                                           (* 基底 *)
      (fun H : 1 = 1 -> False => H eq_refl)
      match ev1 in (ev n0) return (n0 = 1 -> False) with
      | ev_0 =>
          fun H1 : 0 = 1 =>
            eq_ind 0 (fun n1 : nat => match n1 with
                                     | 0 => True
                                     | S _ => False
                                     end) I 1 H1
      | ev_SS n2 Hev2 =>
          fun H2 : S (S n2) = 1 =>
            eq_ind (S (S n2)) (fun n3 : nat => match n3 with
                                               | 0 => False
                                               | 1 => False
                                               | S (S _) => True
                                               end) I 1 H2
      end
    )
    (fun (n : nat) (e : ev n) (IHev : ev (S n) -> False) =>      (* 帰納 *)
       fun evn : ev (S (S (S n))) =>
         (fun H : S (S (S n)) = S (S (S n)) -> False => H eq_refl)
         match evn in (ev n0) return (n0 = S (S (S n)) -> False) with
         | ev_0 =>
             fun H1 : 0 = S (S (S n)) =>
               eq_ind 0 (fun n1 : nat => match n1 with
                                         | 0 => True
                                         | S _ => False
                                         end) I (S (S (S n))) H1
         | ev_SS n2 Hev2 =>
             fun H2 : S (S n2) = S (S (S n)) =>
               (fun H3 : n2 = S n => (* 帰納法の仮定と一致のためコンストラクタを削る *)
                  eq_ind 
                  (S n)                                          (* x : A *)
                  (fun n3 : nat => ev n3 -> False)               (* P : A -> Prop *)
                  (fun H4 : ev (S n) => IHev H4)                 (* f : P x *)
                  n2                                             (* y : A *)
                  (eq_sym H3) (* H3とはx, yの順が逆だから*)      (* e : x = y *)
               )
               (f_equal (fun e : nat => match e : nat with
                                        | 0 => n2
                                        | 1 => n2
                                        | S (S n4) => n4
                                        end) H2) (* コンストラクタ削るのに使う *)
               Hev2
         end
    )
    4 (ev_SS 2 (ev_SS 0 ev_0)) Hev5.