[Agda] `with' in standard functions

[Sergei Meshveliani]

On Mon, 2017-09-25 at 14:32 +0200, Sandro Stucki wrote:
> 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.
> 
> [..]


Thanks to Sandro!

You see, I often occur unlucky when apply `inspect'.


> ----
> 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
>