[Agda] lib solve f(x) = a

[Serge D. Mechveliani]

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