[Agda] proof by patterns

[Sergei Meshveliani]

On Sat, 2014-02-22 at 15:04 +0100, Andreas Abel wrote:
> Why don't you simply match on argument "ft" of function "f" ?

Thank you.
Indeed, adding  "constructor ftCons"  and matching

  f a (ftCons (d ∷ d' ∷ []) all>1 a=d*d') ∣fs∣>1 =  composed-a
                                                    where ...
does work.
But in other examples, matched are some record members, not necessarily
field values.  
I do not know, I shall see the further practice.

------
Sergei




> On 21.02.2014 19:05, Sergei Meshveliani wrote:
> > 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
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
>