[Agda] proof by patterns

[Andreas Abel]

Why don't you simply match on argument "ft" of function "f" ?

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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/