Getting past a `with` block in an Idris proof

ProofWith.idr

module ProofWith

--------------------------------------------------------------------------------
-- Some lemmas used in the proofs below.  I've proposed these for inclusion in
-- the prelude, with cases like this in mind.
--
-- Together, these prove that we can predict the shape of the output of `decEq`
-- if we can either demonstrate propositional equality of its arguments, or
-- show that such equality is ridiculous.

||| `decEq` applied to identical arguments produces a `Yes` result.
decEq_refl : (DecEq t) => (x : t) -> decEq x x = Yes Refl
decEq_refl x with (decEq x x)
  decEq_refl x | Yes Refl = Refl
  decEq_refl x | No contra = absurd (contra Refl)

||| If two values are known *not* to be identical, `decEq` says `No`.
decEq_not : (DecEq t) => (x, y : t) -> Not (x = y) -> (c ** decEq x y = No c)
decEq_not x y xny with (decEq x y)
  decEq_not x x xny | Yes Refl = absurd (xny Refl)
  decEq_not x y xny | No contra = (contra ** Refl)


--------------------------------------------------------------------------------
-- A motivating example.  This is an Idris gloss of the data structure used at
-- the end of the Lists chapter of Software Foundations.  It's a simple
-- dictionary, little more than an association list.

||| A dictionary mapping values of type `k` to values of type `v`.
data Dictionary : (k, v : Type) -> Type where
  ||| The empty dictionary.
  Empty : Dictionary k v
  ||| A dictionary record conses a key-value pair onto another dictionary.
  Record : (key : k) -> (val : v) -> (rest : Dictionary k v) -> Dictionary k v

||| Inserts a key-value mapping into a dictionary.
insert : k -> v -> Dictionary k v -> Dictionary k v
insert = Record


--------------------------------------------------------------------------------
-- Dictionary proofs using a helper function.  This is one of two ways I've
-- tried to write these proofs.  In the end, it was far more obvious how to work
-- with this form of `find` (below), particularly incrementally -- but the
-- version using the `with` block winds up being simpler once you wrap your
-- head around it.

namespace HelperFn
  mutual
    ||| Looks up a value corresponding to `key` in a dictionary.  The first
    ||| such mapping will be chosen.  If no such mapping is present, returns
    ||| `Nothing`.
    find : (DecEq k) => (key : k) -> Dictionary k v -> Maybe v
    find key Empty = Nothing
    find key (Record x val rest) = findHelp key x val rest (decEq key x)

    ||| Helper function for `find`.  Mostly responsible for case analysis on
    ||| the `Dec` parameter.
    findHelp : (DecEq k) => (tgtKey, nxtKey : k) -> (val : v) ->
               (rest : Dictionary k v) -> Dec (tgtKey = nxtKey) -> Maybe v
    findHelp tgtKey tgtKey val  _   (Yes Refl) = Just val
    findHelp tgtKey   _     _  rest (No  _   ) = find tgtKey rest

  ||| The first interesting property: that `find` finds the record added by
  ||| `insert`.  I've written this in a verbose style for didactic reasons,
  ||| largely to highlight the mechanics of the call to `replace` since
  ||| `rewrite` failed.
  find_insert_id : (DecEq k) =>
                   (key : k) -> (val : v) -> (d : Dictionary k v) ->
                   find key (insert key val d) = Just val
  find_insert_id key val d =
    let ins = insert key val d  -- shorthand used below
        s1 : (find key ins = find key ins)
           = Refl
        s2 : (find key ins = find key (Record key val d))
           = s1  -- by the definition of insert
        s3 : (find key ins = findHelp key key val d (decEq key key))
           = s2  -- by case analysis in find
        s4 : (find key ins = findHelp key key val d (Yes Refl))
           -- We have to significantly assist this rewrite from `decEq k k` to
           -- `Yes Refl`, for reasons I don't understand.  Fortunately we can
           -- do it, because we can name the helper.
           = replace {P=\t => find key ins = findHelp key key val d t}
                     (decEq_refl key)
                     s3
        -- With the rewrite complete, evaluating `findHelp` finishes the job.
        qed : (find key (insert key val d) = Just val) = s4
      in qed

  ||| The second interesting property: that `find` will *not* locate a record
  ||| inserted with a different key.
  find_insert_neq : (DecEq k) =>
                    (d : Dictionary k v) ->
                    (k1, k2 : k) ->
                    (val : v) ->
                    Not (k1 = k2) ->
                    find k1 d = find k1 (insert k2 val d)
  find_insert_neq d k1 k2 val prf =
    let (_ ** lemma) = decEq_not k1 k2 prf
    in rewrite lemma  -- discharge the decEq obligation in findHelp
    in Refl  -- now it becomes easy


--------------------------------------------------------------------------------
-- Dictionary proofs using a `with` block.  The functions and proofs are
-- doing the same thing as the examples I gave above, only the methods are
-- different.  These proofs were harder to construct interactively, because
-- hitting a `with` (or a `case`) produces goal output that is hard to read and
-- impossible (AFAIK) to use with `replace`.  However, in the end, that proved
-- to be surmountable.

namespace WithBlock
  %hide find  -- from HelperFn above; odd that this is necessary, but hey.

  ||| Looks up a value corresponding to `key` in a dictionary.  This version
  ||| is far simpler than the helper function variant.
  find : (DecEq k) => (key : k) -> Dictionary k v -> Maybe v
  find key Empty = Nothing
  find key (Record key2 val rest) with (decEq key key2)
    find key (Record key val rest) | Yes Refl = Just val
    find key (Record key2 val rest) | No _ = find key rest

  ||| The property stated above, for the new implementation.  When proving this
  ||| interactively the goal winds up looking like this:
  |||  with block in ProofWith.WithBlock.find k
  |||                                         v
  |||                                         key
  |||                                         key
  |||                                         (decEq key key)
  |||                                         val
  |||                                         d
  |||                                         constrarg =
  |||                                         Just val
  ||| Ew.
  |||
  ||| The key is to notice that `decEq key key` has not been destructed,
  ||| preventing further case analysis and leaving the `with` block as an
  ||| obstacle.  We can destruct it using the lemma defined at the top of
  ||| this file.
  |||
  ||| By adding `rewrite decEq_refl key in ?hole` we get the far more tractable
  ||| goal:
  |||    Just val = Just val
  ||| which we can discharge by `Refl`.
  find_insert_id : (DecEq k) =>
                   (key : k) -> (val : v) -> (d : Dictionary k v) ->
                   find key (insert key val d) = Just val
  find_insert_id key val d = rewrite decEq_refl key in Refl
 
  ||| Same approach for the opposing property, with similar results.  The proof
  ||| is slightly hairier since I used a sigma type for the `decEq_not` lemma.
  find_insert_neq : (DecEq k) =>
                    (d : Dictionary k v) ->
                    (k1, k2 : k) ->
                    (val : v) ->
                    Not (k1 = k2) ->
                    find k1 d = find k1 (insert k2 val d)
  find_insert_neq d k1 k2 val prf =
    let (_ ** lemma) = decEq_not k1 k2 prf
    in rewrite lemma
    in Refl