# [Agda] lib solve f(x) = a

Serge D. Mechveliani mechvel at botik.ru
Thu Jan 24 12:20:27 CET 2013

```On Thu, Jan 24, 2013 at 11:40:45AM +0100, Twan van Laarhoven wrote:
> 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.

Sorry, it was
noSolution : ((x : A) -> \neg (f x \~~ a)) -> DecSolution f b

I think, this means that there are no solutions. Right?

> I would use

(I change some math symbols)

>
>     open import Data.Product      -- for \exists
>     open import Relation.Nullary  -- for Dec
>
>     Solution : {A B : Set} -> (f : A -> B) -> B -> Set
>     Solution f b = \exists (\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 (\exists (\a -> f a ~~ b))
>

This latter line looks the best -- if only  \exists  means the needed
constructive thing (I need to look into  \exists).

Thank you.

------
Sergei
```