[Agda] signature for `with' branch

[Sergei Meshveliani]

On Tue, 2017-02-28 at 11:26 +0100, Nils Anders Danielsson wrote:
> On 2017-02-27 21:38, Sergei Meshveliani wrote:
> > when I expect that there the result for  (add a (x ∷ xs))  must be
> > a ∷ x ∷ xs.
> 
> The term "add a (x ∷ xs)" reduces to "aux (a ≟ 0) (x ∷ xs)", which is
> stuck, because "a ≟ 0" does not reduce to WHNF.
> 
> [..]


I knew that it is not reduced. But how to make it reduced there without
using `with' or `case' ?

Generally, the matter is that I do not discover any regular and uniform
way to set Agda proofs for simple statements when a proof is based on
considering cases.   
I always know a simple naive proof, but often fail to convert it to an
Agda proof, because some terms do not want to reduce along the branches.
Mostly, "with | inspect" works, but not always.  

I attach the code again, because it has missed the mail list.

Thanks,

------
Sergei
-------------- next part --------------
open import Relation.Nullary using (yes; no; ¬_; Dec)
open import Relation.Binary  using (DecSetoid; DecTotalOrder; Tri; 
                                                       StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Empty    using (⊥-elim)
open import Data.List     using (List; []; _∷_; map)
open import Data.List.All using (All) renaming ([] to []a; _∷_ to _∷a_)
open import Data.Nat      using (ℕ; suc; _+_; _<_; _>_)
open import Data.Nat.Properties using (≤-decTotalOrder; strictTotalOrder) 

decSetoid = DecTotalOrder.Eq.decSetoid ≤-decTotalOrder
open DecSetoid        decSetoid        using (_≟_)
open StrictTotalOrder strictTotalOrder using (compare) 
open Tri

postulate anything : ∀ {a} {A : Set a} → A 


add : ℕ → List ℕ → List ℕ 
add a xs =  aux (a ≟ 0) xs 
  where
  aux : Dec (a ≡ 0) → List ℕ → List ℕ   
  aux (yes _)  xs       =  xs
  aux (no _)   []       =  a ∷ []
  aux (no a≢0) (x ∷ xs) =  aux0 (compare a x) 
                           where
                           aux0 : Tri (a < x) (a ≡ x) (a > x) → List ℕ 
                           aux0 (tri> _ _ _) =  a ∷ x ∷ xs 
                           aux0 (tri≈ _ _ _) =  (a + x) ∷ xs
                           aux0 (tri< _ _ _) =  x ∷ (aux (no a≢0) xs)


lemma :  ∀ a xs → a ≢ 0 → All (_≢ 0) xs → All (_≢ 0) (add a xs) 

lemma _ []       _   _             =  anything
lemma a (x ∷ xs) a≢0 (x≢0 ∷a xs≢0) =  aux (a ≟ 0)
  where
  aux :  Dec (a ≡ 0) → All (_≢ 0) (add a (x ∷ xs)) 

  aux (yes a≡0) = ⊥-elim (a≢0 a≡0)
  aux (no a≢0)  = aux0 (compare a x) 
      where
      aux0 :  Tri (a < x) (a ≡ x) (a > x) → All (_≢ 0) (add a (x ∷ xs)) 
      aux0 (tri> _ _ _) = 
                          -- add a (x ∷ xs) --> a ∷ x ∷ xs,
                          -- so that   (a≢0 ∷a x≢0 ∷a xs≢0)  is a proof
                   aux1 (a ≟ 0)
                   where
                   aux1 : Dec (a ≡ 0) → All (_≢ 0) (add a (x ∷ xs)) 
                   aux1 (no _)    = a≢0 ∷a x≢0 ∷a xs≢0
                   aux1 (yes a≡0) = ⊥-elim (a≢0 a≡0)

      aux0 (tri≈ _ _ _) = anything   
      aux0 (tri< _ _ _) = anything