[Agda] proof by patterns

[Sergei Meshveliani]

People,
I have the following difficulties with a proof by patterns: 

-------------------------------------------------------------------------
open import Function using (case_of_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Empty           using (⊥-elim; ⊥)
open import Data.Nat             using (ℕ; _*_; _<_; _>_; _≯_)
open import Data.Product         using (_×_; _,_; ∃₂)
open import Data.List            using (List; []; _∷_; length; foldr)
open import Data.List.All as All using ()

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

-- This is about  decomposition of a natural into a product.

IsComposed : ℕ → Set
IsComposed n =  ∃₂ \ l m →  l > 1  ×  m > 1  ×  n ≡ l * m

Π : List ℕ → ℕ
Π = foldr _*_ 1

record Ft (a : ℕ) : Set where    -- something like a factorization
  field                          -- structure (contrived)
    factors : List ℕ
    all>1   : All.All (_>_ 1) factors
    eq      : a ≡ Π factors


f : (a : ℕ) → (ft : Ft a) → (length (Ft.factors ft)) > 1 → IsComposed a
--
-- decompose  a  to  d * d'   by using the factorization structure

f a ft ∣fs∣>1  with  Ft.factors ft    

... | d ∷ d' ∷ [] =  composed-a  
                     where                             
                     fs = Ft.factors ft 

                     e0 :  a ≡ Π fs            
                     e0 =  Ft.eq ft          
                                                                                
                     e :  a ≡ Π (d ∷ d' ∷ [])   
                     e =  Ft.eq ft    
              
                     -- postulate
                     composed-a : isComposed a
                     ...
... | _ =  ...
--------------------------------------------------------------

I hoped for the field  eq  to provide a proof for  
                                          a ≡ Π (d ∷ d' ∷ []) 
in the first branch.
And then, one could derive the decomposition  a ≡ d * d'. 
The line  "e : ..."  starts to check this approach.

1.
But  "e = ..."  is not type-checked. As it often occurs, Agda does not
see that  eq  holds for  d ∷ d' ∷ [],  despite that this pattern is a
special case of  Ft.factors.
Such is a strange nature of patters in Agda. It is difficult to get used
to it.

Can this `with' or `case' be fixed in this example?


2.
After I have given up with  case/with,  I find that this approach works:

------------------------------------------------------------------
f a ft ∣fs∣>1 =  g (Ft.factors ft) (Ft.all>1 ft) (Ft.eq ft)

  -- extract all the fields and put their values to one signature
  -- simultaneously

  where
  g : (fs : List ℕ) → All.All (_>_ 1) fs → a ≡ Π fs → IsComposed a

  g (d ∷ d' ∷ []) all>1 a=product =  composed-a
    where
    e :  a ≡ d * (d' * 1)
    e =  a=product            -- this works

    composed-a : IsComposed a
    ...
------------------------------------------------------------------


But for a record of 10 dependent fields, the signature for  g  may
occur too large and complex.

What is a regular way out?
Is it trying to refine the approach of  `g'  in each particular case?

Thank you in advance for explanation,

------
Sergei