[Agda] lib solve f(x) = a

[Twan van Laarhoven]

On 24/01/13 11:32, Serge D. Mechveliani wrote:
> People,
> I need the signature for decidable solution for  f x = b,
>
>             solve : ... (f : A -> B) -> (b : B) -> DecSolution f b
>
> (some details skipped)
> -- any solution, with a proof, or a proof for the solution absence.
>
>    record Solution ... (f : A -> B) (b : B)  : Set _  where
>                                     field
>                                       solution : A
>                                       proof    : (f solution) \~~ b
>    data DecSolution ... f b : Set _
>         where
>         solved     : Solution f b                -> DecSolution f b
>         noSolution : (x : A) -> \neg (f x \~~ a) -> DecSolution f b

That noSolution constructor just says that a given x is not a solution, it 
doesn't say that there are no solutions. I would use

     open import Data.Product      -- for ∃
     open import Relation.Nullary  -- for Dec

     Solution : {A B : Set} -> (f : A -> B) -> B -> Set
     Solution f b = ∃ (\a -> f a ≡ b)

     DecSolution : {A B : Set} -> (f : A -> B) -> B -> Set
     DecSolution f b = Dec (Solution f b)

Or without the synonyms,

     solve : ... (f : A -> B) -> (b : B) -> Dec (∃ (\a -> f a ≡ b))


Twan