gistfile1.txt

Inductive odd : nat -> Prop :=
  | odd_1 : odd 1
  | odd_S n : even (n ) -> odd (n+1)
  with even : nat -> Prop :=
  | even_S n : odd n -> even (n+1).

Fixpoint oddmembers (l : natlist) : natlist :=
  match l with
  | nil => []
  | O :: t => oddmembers(t)
  | S n :: t => match S n with
    | odd => S  n :: oddmembers(t)
    end
  end.


Example test_oddmembers: oddmembers [0,1,0,2,3,0,0] = [1,3].
Proof. intros. simpl.