[Agda] Not Unfolding Local Defs

[G. Allais]

Hi Harley,

One think you can do is use records rather than local definitions.
This will force you to use the copattern / projection but will
also prevent reduction from happening.

This approach is reminiscent of "Types as Programming Problems"
used in a systematic manner in Epigram to document the meaning of
the goals and the values obtained by induction. E.g. if you were
to implement addition on natural numbers, you'd define:

=================================================================
record PLUS (m n : ℕ) : Set where
   field unfold : ℕ

plus : (m n : ℕ) -> PLUS m n
plus = ?
=================================================================

A goal of type `PLUS m n` is a lot clearer than simply `ℕ` even
though the two are isomorphic. And if you try to use an induction
principle rather than defining the function by pattern matching,
then the induction hypothesis is helpfully labeled and you don't
have to guess which `ℕ` represents what.

Anyway, here is a quick example with lifting a relation in a
pointwise manner to vectors. If you try to comment out the
recursive call "pointwiseEq as", you'll see that the goal is
clean because I have refined the goal by using a combinator
which expects its second argument to be packaged in a Pointwise
record.

This does force you to do a bit of extra work but it's also a good
way to highlight the structure of the problem which is always helpful
for the reader.

=================================================================
module TypesAsProblems where

open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Relation.Binary.PropositionalEquality


record Pointwise
   {A B : Set} (R : A → B → Set)
   {n : ℕ} (as : Vec A n) (bs : Vec B n) : Set where
   field unfold : (k : Fin n) → R (lookup k as) (lookup k bs)
open Pointwise

pointwise-base : {A B : Set} {R : A → B → Set} → Pointwise R [] []
unfold pointwise-base ()

pointwise-extend : {A B : Set} {R : A → B → Set}
   {a : A} {b : B} → R a b →
   {n : ℕ} {as : Vec A n} {bs : Vec B n} → Pointwise R as bs →
   Pointwise R (a ∷ as) (b ∷ bs)
unfold (pointwise-extend r rs) zero    = r
unfold (pointwise-extend r rs) (suc k) = unfold rs k

open Pointwise

pointwiseEq : {A : Set} {n : ℕ} (as : Vec A n) → Pointwise _≡_ as as
pointwiseEq []       = pointwise-base
pointwiseEq (a ∷ as) = pointwise-extend refl (pointwiseEq as)
=================================================================

Cheers,


On 10/05/16 19:26, Harley Eades III wrote:
> Hi, everyone.
>
> I am using a ton of records in my formalization, and at the top of
> each module I give several convince definitions for the projections
> of my records to make types easier to read.
>
> For example, see the top of this file:
>
> https://github.com/heades/dialectica-spaces/blob/Lambek/NCDialSets.agda
>
> A typical example is the following:
>
> _≤M_ : M → M → Set
> _≤M_ = (rel (poset (oncMonoid bp-pf)))
>
> This definition makes reading types a lot easier, but this definition is unfolded
> in goals, which makes the goal very hard to read.  Multiply this with a number
> of definitions like this, and we get goals that are close to impossible to read.
>
> So I spend a lot of time trying to parse a goal myself to be able to do the proof.
>
> Is there a way to tell Agda not to unfold these definitions in goals?
>
> Thanks,
> Harley
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>