[Agda] Not Unfolding Local Defs

[Harley Eades III]

Hi, Guillaume.

Thanks for this explanation.  It did work for types such as my 
example, but it isn’t clear how to use it for local definitions of
terms used in types.  So for example:

So something like this:

 _⊗M_ : M → M → M
  _⊗M_ = mul (oncMonoid bp-pf)

Can the same trick be applied?

Best,
Harley

> On May 11, 2016, at 5:33 AM, G. Allais <guillaume.allais at ens-lyon.org> wrote:
> 
> 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
>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda