[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
More information about the Agda
mailing list