[Agda] `with' in standard functions

[Sandro Stucki]

Hi Sergei,

Here's a solution that uses a with clause in the proof (similar to
that in the definition of `fromBits`) and the `inspect` idiom to keep
track of the result of the with clause. There's also a helper lemma to
dispatch some absurd cases. It's not very elegant, and I'm not sure it
will scale to bigger examples, but I hope it's useful to you anyway.

----
open import Data.Bin
open import Data.Digit
open import Data.Fin renaming (suc to 1+_)
open import Data.List
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Relation.Nullary.Negation

-- A helper: lists of bits ending in `1b` do not convert to `0#`.
fromBits-bs++1≠0 : ∀ bs → fromBits (bs ∷ʳ 1b) ≢ 0#
fromBits-bs++1≠0 []                ()
fromBits-bs++1≠0 (b          ∷ bs) _
  with fromBits (bs ∷ʳ 1b) | inspect fromBits (bs ∷ʳ 1b)
fromBits-bs++1≠0 (zero       ∷ bs) _  | 0#     | [ eq ] = fromBits-bs++1≠0 bs eq
fromBits-bs++1≠0 (1+ zero    ∷ bs) () | 0#     | [ _ ]
fromBits-bs++1≠0 (1+ (1+ ()) ∷ bs) _  | 0#     | _
fromBits-bs++1≠0 (b ∷ bs)          () | bs′ 1# | [ _ ]

fromBits-bs++1 :  fromBits ∘ (_∷ʳ 1b) ≗ _1#
fromBits-bs++1 []                = refl
fromBits-bs++1 (b          ∷ bs)
  with fromBits (bs ∷ʳ 1b) | inspect fromBits (bs ∷ʳ 1b)
fromBits-bs++1 (b          ∷ bs) | bs′ 1# | [ eq ] =
  helper (begin
    bs′ 1#                            ≡⟨ sym eq ⟩
    fromBits (bs ++ (1+ zero) ∷ [])   ≡⟨ fromBits-bs++1 bs ⟩
    bs 1#                             ∎)
  where
    -- Combines injectivity of `_1#` with `cong (_#1 ∘ (b ∷_))`.
    helper : ∀ {b bs₁ bs₂} → bs₁ 1# ≡ bs₂ 1# → (b ∷ bs₁) 1# ≡ (b ∷ bs₂) 1#
    helper refl = refl
fromBits-bs++1 (zero       ∷ bs) | 0#     | [ eq ] =
  contradiction eq ((fromBits-bs++1≠0 bs))
fromBits-bs++1 (1+ zero    ∷ bs) | 0#     | [ eq ] =
  contradiction eq ((fromBits-bs++1≠0 bs))
fromBits-bs++1 (1+ (1+ ()) ∷ bs) | 0#     | _
----

Cheers
/Sandro


On Sun, Sep 24, 2017 at 1:46 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> People,
>
> There is a certain problem with user proofs for Standard library
> functions that use `with' or `case_of_'.
> If a function is written without `with' (`with' replaced with calling an
> auxiliary function  aux, and this  aux  is exported from the module),
> then it is much easier to compose various new proofs about it.
>
> But the user cannot change implementation for a standard function.
>
> For example,  Data.Bin  implements
>
> -------------------------
> fromBits : List Bit → Bin
> fromBits []        = 0#
> fromBits (b  ∷ bs) with fromBits bs
> fromBits (b  ∷ bs) | bs′ 1# = (b ∷ bs′) 1#
> fromBits (0b ∷ bs) | 0#     = 0#
> fromBits (1b ∷ bs) | 0#     = [] 1#
> fromBits (⊥b ∷ bs) | _
> -------------------------
>
> I need to prove
>
>           fromBits-bs++1 :  fromBits ∘ (_∷ʳ 1b) ≗ _1#
>
> And find it difficult.
> Then I get free of `with', and a proof becomes plain and easy to
> compose:
>
> --------------------------------------------------
> fromBits-aux : Bit → List Bit → Bin → Bin    -- needs to be exported
>
> fromBits-aux b  bs (bs' 1#) = (b ∷ bs') 1#
> fromBits-aux 0b bs 0#       = 0#
> fromBits-aux 1b bs 0#       = [] 1#
> fromBits-aux ⊥b bs _
>
> fromBits' : List Bit → Bin
> fromBits' []       = 0#
> fromBits' (b ∷ bs) = fromBits-aux b bs (fromBits' bs)
>
>
> fromBits-bs++1 :  fromBits' ∘ (_∷ʳ 1b) ≗ _1#
> fromBits-bs++1 []       =  refl
> fromBits-bs++1 (b ∷ bs) =
>   begin
>     fromBits' (b ∷ (bs ∷ʳ 1b))                        ≡⟨ refl ⟩
>     fromBits-aux b (bs ∷ʳ 1b) (fromBits' (bs ∷ʳ 1b))
>                                     ≡⟨ cong (fromBits-aux b (bs ∷ʳ 1b))
>                                             (fromBits-bs++1 bs)
>                                      ⟩
>     fromBits-aux b (bs ∷ʳ 1b) (bs 1#)                 ≡⟨ refl ⟩
>     (b ∷ bs) 1#
>   ∎
> ---------------------------------------------------
>
> Please, what is a way out?
>
> Thanks,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda