auto/default proof search

TenStrings.idr

module TenStrings

import Decidable.Order

%default total

-----------------------------------------------
-- Copied from tpsinnem/libs-misc
-----------------------------------------------

decType : {a:Type} -> Dec a -> Type
decType {a} _ = a


data BadDecYes : Type -> Type where
  badDecYes  : {A:Type} -> (A)        -> BadDecYes A

data BadDecNo : Type -> Type where
  badDecNo   : {A:Type} -> (A -> _|_) -> BadDecNo A


decYesType : {A:Type} -> Dec A -> Type
decYesType {A} (Yes _)  = A
decYesType {A} (No _)   = BadDecNo A

decNoType : {A:Type} -> Dec A -> Type
decNoType {A} (Yes _)   = BadDecYes A
decNoType {A} (No _)    = A -> _|_


decYes : {A:Type} -> (dec : Dec A) -> decYesType dec
decYes (Yes a) = a
decYes (No a)  = badDecNo a

decNo : {A:Type} -> (dec : Dec A) -> decNoType dec
decNo (Yes a)  = badDecYes a
decNo (No a)   = a

syntax "{{" [proofname] ":" "yes" [dec] "}}" "->" [ret]
  = { default (decYes dec) proofname : decType dec } -> ret

syntax "{{" [proofname] ":" "no" [dec] "}}" "->" [ret]
  = { default (decNo dec) proofname : decType dec -> _|_ } -> ret




---

vec : x -> Vect n x
vec {n = Z}   _ = []
vec {n = S n} x = x :: vec x

unshift : (m : Nat) -> (n : Nat) -> NatLTE (S m) (S n) -> NatLTE m n
unshift m m     nEqn         = nEqn
unshift Z (S _) _            = zeroAlwaysSmaller
unshift _ Z     (nLTESm prf) = FalseElim (zeroNeverGreater prf)
unshift m (S n) (nLTESm prf) = nLTESm (unshift m n prf)


minusSuccLeftSucc : (x : Nat) -> (y : Nat) -> (p : x `NatLTE` y) -> S (y - x) = S y - x
minusSuccLeftSucc x     x     nEqn       = ?minusSuccLeftSuccEq
minusSuccLeftSucc Z     (S _) (nLTESm _) = refl
minusSuccLeftSucc (S x) (S y) prf        = let ih = minusSuccLeftSucc x y (unshift x y prf)
                                           in rewrite ih in refl

plusXYminX : (x : Nat) -> (y : Nat) -> (p : x `NatLTE` y) -> x + (y - x) = y
plusXYminX Z     y     p    = rewrite minusZeroRight y in refl
plusXYminX (S x) Z     nEqn impossible
plusXYminX (S x) (S y) p    = let ih = plusXYminX x y (unshift x y p)
                              in rewrite ih in refl

vec10foo : {m : Nat} -> {{ prf : yes (Decidable.Order.lte m 10) }} -> Vect m String -> Vect 10 String
vec10foo {m} v1 ?= v1 ++ vec {n = 10 - m} "foo"

example1 : Vect 10 String
example1 = vec10foo {m = 2} ["bar" , "baz"]

TenStrings.vec10foo_lemma_1 = proof
  intros
  rewrite plusXYminX m 10 proofname
  trivial

TenStrings.minusSuccLeftSuccEq = proof
  intros
  rewrite minusZeroN x
  rewrite minusOneSuccN x
  trivial