0 | ||| The content of this module is based on the paper
  1 | ||| Applications of Applicative Proof Search
  2 | ||| by Liam O'Connor
  3 | ||| https://doi.org/10.1145/2976022.2976030
  4 |
  5 | module Search.Properties
  6 |
  7 | import Data.Fuel
  8 | import Data.List.Lazy
  9 | import Data.List.Lazy.Quantifiers
 10 | import Data.Nat
 11 | import Data.So
 12 |
 13 | import public Data.Stream
 14 | import public Data.Colist
 15 | import public Data.Colist1
 16 |
 17 | import public Search.Negation
 18 | import public Search.HDecidable
 19 | import public Search.Generator
 20 |
 21 | import Decidable.Equality
 22 |
 23 | %default total
 24 |
 25 | ------------------------------------------------------------------------
 26 | -- Type
 27 |
 28 | ||| Take the product of a list of types
 29 | public export
 30 | Product : List Type -> Type
 31 | Product = foldr Pair ()
 32 |
 33 | ||| A property amenable to testing
 34 | ||| @cs is the list of generators we need (inferrable)
 35 | ||| @a  is the type we hope is inhabited
 36 | ||| NB: the longer the list of generators, the bigger the search space!
 37 | public export
 38 | record Prop (cs : List Type) (a : Type) where
 39 |   constructor MkProp
 40 |   ||| The function trying to find an `a` provided generators for `cs`.
 41 |   ||| Made total by consuming some fuel along the way.
 42 |   runProp : Colist1 (Product cs) -> Fuel -> HDec a
 43 |
 44 | ------------------------------------------------------------------------
 45 | -- Prop-like structure
 46 |
 47 | ||| A type constructor satisfying the AProp interface is morally a Prop
 48 | ||| It may not make use of all of the powers granted by Prop, hence the
 49 | ||| associated `Constraints` list of types.
 50 | public export
 51 | interface AProp (0 t : Type -> Type) where
 52 |   0 Constraints : List Type
 53 |   toProp : t a -> Prop Constraints a
 54 |
 55 | ||| Props are trivially AProp
 56 | public export
 57 | AProp (Prop cs) where
 58 |   Constraints = cs
 59 |   toProp = id
 60 |
 61 | ||| Half deciders are AProps that do not need any constraints to be satisfied
 62 | public export
 63 | AProp HDec where
 64 |   Constraints = []
 65 |   toProp = MkProp . const . const
 66 |
 67 | ||| Deciders are AProps that do not need any constraints to be satisfied
 68 | public export
 69 | AProp Dec where
 70 |   Constraints = []
 71 |   toProp = MkProp . (const . const . toHDec)
 72 |
 73 | ||| We can run an AProp to try to generate a value of type a
 74 | public export
 75 | check : (gen : Generator (Product cs)) => (f : Fuel) -> (p : Prop cs a) ->
 76 |         {auto pr : So (isTrue (runProp p (generate @{gen}) f))} -> a
 77 | check @{gen} f p @{pr} = evidence (runProp p (generate @{gen}) f) pr
 78 |
 79 | ||| Provided that we know how to generate candidates of type `a`, we can look
 80 | ||| for a witness satisfying a given predicate over `a`.
 81 | public export
 82 | exists : {0 p : a -> Type} -> (aPropt : AProp t) =>
 83 |          ((x : a) -> t (p x)) ->
 84 |          Prop (a :: Constraints @{aPropt}) (DPair a p)
 85 | exists test = MkProp $ \ acs, fuel =>
 86 |   let candidates : LazyList a = take fuel (map fst acs) in
 87 |   let cs = map snd acs in
 88 |   let find = any candidates (\ x => runProp (toProp (test x)) cs fuel) in
 89 |   map toDPair find
 90 |
 91 | ------------------------------------------------------------------------
 92 | -- Examples
 93 |
 94 | namespace GT11
 95 |
 96 |   example : Prop ? (DPair Nat (\ i => Not (i `LTE` 10)))
 97 |   example = exists (\ i => not (isLTE 11 i))
 98 |
 99 |   lemma : DPair Nat (\ i => Not (i `LTE` 10))
100 |   lemma = check (limit 1000) example
101 |
102 | namespace Pythagoras
103 |
104 |   formula : Type
105 |   formula = DPair Nat $ \ m =>
106 |             DPair Nat $ \ n =>
107 |             DPair Nat $ \ p =>
108 |             (0 `LT` m, 0 `LT` n, 0 `LT` p
109 |             , (m * m + n * n) === (p * p))
110 |
111 |   search : Prop ? Pythagoras.formula
112 |   search = exists $ \ m =>
113 |            exists $ \ n =>
114 |            exists $ \ p =>
115 |            (isLT 0 m && isLT 0 n && isLT 0 p
116 |            && decEq (m * m + n * n) (p * p))
117 |
118 |   -- This one is quite a bit slower so it's better to run
119 |   -- the compiled version instead
120 |   lemma : HDec Pythagoras.formula
121 |   lemma = runProp search generate (limit 10)
122 |