Contents

# Target

Try to develop function which binarize image with Proof Driven Development.# Coq

# Target

Try to develop function which binarize image with Proof Driven Development.# Coq

Define binarization function with Coq.I think following things are needed for proofing.Require Import List. Require Import Arith. Fixpoint binarize (l : list nat)(th : nat) : list nat := match l with | nil =&amp;gt; nil | x::xs =&amp;gt; if leb th x then 255 :: (binarize xs th) else 0 :: (binarize xs th) end.

- Same element number with the list and the list after applying function.
- The list which is applied the function has only 2 type value 0 or 255.

Define binarization function with Coq.

Require Import List. Require Import Arith. Fixpoint binarize (l : list nat)(th : nat) : list nat := match l with | nil => nil | x::xs => if leb th x then 255 :: (binarize xs th) else 0 :: (binarize xs th) end.I think following things are needed for proofing.

- Same element number with the list and the list after applying function.
- The list which is applied the function has only 2 type value 0 or 255.