coq練習問題(4)

coq4.v

Require Import ssreflect.

Module Odd.

Inductive odd : nat -> Prop :=
  | odd_1 : odd 1
  | odd_SS : forall n, odd n -> odd (S (S n)).
Inductive even : nat -> Prop :=
  | even_0 : even 0
  | even_SS : forall n, even n -> even (S (S n)).
Theorem even_odd n : even n -> odd (S n).
Proof.
  intro en.
  elim en.
  + apply odd_1.
  + move => m em osm.
    apply odd_SS.
    assumption.
Qed.

Theorem odd_even n : odd n -> even (S n).
Proof.
  intro en.
  elim en.
  + apply /even_SS /even_0.
  + move => m em osm.
    apply even_SS.
    assumption.
Qed.

Lemma SS_odd n : odd (S (S n)) -> odd n.
Proof.
  move => odd2.
  
Qed.
Theorem even_not_odd n : even n -> ~odd n.
Proof.
  elim.
  + move H : 0 => z odz.
    case: odz H.
    - done.
    - move => n0 oddn0.
      move => abs.
      done.
  + move => x evx noddx odd2.
    apply noddx.
    apply SS_odd.
    
  
Qed.
End Odd.