effectfully | 2 Sep 14:41 2015

Lambda terms as a natural transformation.

Hi. I tried to rewrite the code from the "Relative monads formalized"
paper ([1]) using in the category of contexts order preserving
embeddings ([2]) as morphisms instead of functions, but then I
realized that substitution is a functor from ConCat to Fam Ty as well
as renaming:

    ren : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> σ ∈ Γ -> σ ∈ Δ
    sub : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ ⊢ σ -> Δ ⊢ σ

    Ren : Functor ConCat (Fam Ty)
    Sub : Functor ConCat (Fam Ty)

Terms then form a natural transformation between these functors:

    Term : NaturalTransformation Ren Sub
    Term = record
      { η          = var
      ; naturality = λ v -> refl

This is completely trivial. Is this well-known?

The code (with a bit different names) can be found at [3].

[1] http://cs.ioc.ee/~james/papers/AssistedMonads2.pdf
[2] http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=91
[3] https://github.com/effectfully/Categories/blob/master/NaturalTransformation/Lambda.agda
Chantal Keller | 31 Aug 20:53 2015

Post-doctoral position in interactive theorem proving at the University of Iowa

Post-doctoral position in interactive theorem proving
Computational Logic Center
Department of Computer Science
The University of Iowa

Applications are invited for a post-doctoral research position in the 
Computational Logic Center at the University of Iowa in the area of 
interactive theorem proving and verification.

The position is funded by DARPA through the HACMS program. The work will 
be done in collaboration with researchers at New York University, the 
Université Paris Sud and Princeton University. The main goal of the 
project is to increase the level of automation in the Coq proof 
assistant by soundly integrating SMT solvers into it. Our immediate 
emphasis is on supporting software verification efforts by other 
research groups currently funded by HAMCS. However, we expect that the 
results of the integration will benefit Coq users in general.

The ideal candidate will have a Ph.D. in Computer Science, general 
knowledge of formal methods, and expertise in interactive theorem 
proving in higher-order logics, with substantial experience in using 
Coq, Isabelle, or similar tools. Candidates should demonstrate strong 
programming and formal modeling skills. Previous experience in writing 
Coq tactics and plug-ins is a considerable plus. Familiarity with SMT is 
welcome but not required.

The position is a full time appointment that runs initially through 
August 2016 and could be renewed for another year subject to 
(Continue reading)

Andreas Abel | 31 Aug 10:30 2015

FLOPS 2016 last cfp (deadline 21st Sep)

Dear colleagues, please consider contributing to FLOPS 2016! --Andreas

FLOPS 2016: 13th International Symposium on Functional and Logic Programming
March 3-6, 2016, Kochi, Japan

Final Call For Papers 

New: revised submission deadlines (Sep 21 for abstracts, Sep 25 for papers)

Writing down detailed computational steps is not the only way of
programming. The alternative, being used increasingly in practice, is
to start by writing down the desired properties of the result. The
computational steps are then (semi-)automatically derived from these
higher-level specifications. Examples of this declarative style
include functional and logic programming, program transformation and
re-writing, and extracting programs from proofs of their correctness.

FLOPS aims to bring together practitioners, researchers and
implementors of the declarative programming, to discuss mutually
interesting results and common problems: theoretical advances, their
implementations in language systems and tools, and applications of
these systems in practice. The scope includes all aspects of the
design, semantics, theory, applications, implementations, and teaching
of declarative programming.  FLOPS specifically aims to
promote cross-fertilization between theory and practice and among
different styles of declarative programming.


(Continue reading)

Martin Stone Davis | 27 Aug 05:11 2015

Perplexed in a proof

The full code is pasted here: http://lpaste.net/139721

{- This uses Agda and agda-stdlib -}

{- In the below, lemJoinˡ⁺IsCorrect, I am trying to prove that if a key is in the left-hand tree given to Data.AVL.Indexed.joinˡ⁺ then it will still be present in the joined tree. Unforunately, I have only been successful in about half of the cases. Would someone be so kind as to clue me in as to what might be going wrong? -}

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module Enagda03
  {k v ℓ}
  {Key : Set k} (Value : Key → Set v)
  {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _<_) where

open import Data.Product
open import Level using (_⊔_)
open import Data.AVL Value isStrictTotalOrder using (KV; module Extended-key; module Height-invariants; module Indexed)
open Extended-key
open Height-invariants
open Indexed

open IsStrictTotalOrder isStrictTotalOrder

data _∈_ {lb ub} (key : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
  here : ∀ {hˡ hʳ h v}
    {lk : Tree lb [ key ] hˡ}
    {ku : Tree [ key ]  ub hʳ}
    {bal : hˡ ∼ hʳ ⊔ h} →
    key ∈ node (key , v) lk ku bal
  left : ∀ {hˡ hʳ h k′} {v′ : Value k′}
    {lk′ : Tree lb [ k′ ] hˡ}
    {k′u : Tree [ k′ ] ub hʳ}
    {bal : hˡ ∼ hʳ ⊔ h} →
    key ∈ lk′ →
    key ∈ node (k′ , v′) lk′ k′u bal
  right : ∀ {hˡ hʳ h k′} {v′ : Value k′}
    {lk′ : Tree lb [ k′ ] hˡ}
    {k′u : Tree [ k′ ] ub hʳ}
    {bal : hˡ ∼ hʳ ⊔ h} →
    key ∈ k′u →
    key ∈ node (k′ , v′) lk′ k′u bal

open import Data.Nat.Base

lemJoinˡ⁺IsCorrect : ∀ { l r hˡ hʳ h }
    { k′ : Key }
    { v′ : Value k′ }
    ( tˡ⁺ : ∃ λ i → Tree l [ k′ ] ( i ⊕ hˡ ) )
    ( tʳ : Tree [ k′ ] r hʳ )
    ( bal : hˡ ∼ hʳ ⊔ h )
    { key : Key }
    ( k∈tˡ : key ∈ proj₂ tˡ⁺ ) →
    key ∈ proj₂ ( joinˡ⁺ ( k′ , v′ ) tˡ⁺ tʳ bal )
lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- here = left here
lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( left k∈tˡ ) = left ( left k∈tˡ )
lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( right here ) = here
lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( right ( left k∈tʳˡ ) ) = left ( right k∈tʳˡ )
lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( right ( right k∈tʳʳ ) ) = right ( left k∈tʳʳ )
{- This is the first case that doesn't work. -}
lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- here = {!here!}
   If I fill-out the term as follows

      lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- here = here

   then I get the following error:

      suc (_h_217 Value isStrictTotalOrder .k .lk .ku .tʳ)
      proj₁ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku &sim;-) .tʳ &sim;-) ⊕ (1 + suc .hʳ)
      of type ℕ
      when checking that the expression here has type
      proj₁ .k ∈ proj₂ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku &sim;-) .tʳ &sim;-)

   Thinking it would help, I tried to get around the above error by specifying the implicit variable h:

      lemJoinˡ⁺IsCorrect { hʳ = hʳ } ( 1# , node _ _ _ ∼- ) _ ∼- here = here { h = suc hʳ }

   But that just results in a different error:

      suc (suc hʳ) !=
      proj₁ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku &sim;-) .tʳ &sim;-) ⊕ (1 + suc hʳ)
      of type ℕ
      when checking that the expression here {h = suc hʳ} has type
      proj₁ .k ∈ proj₂ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku &sim;-) .tʳ &sim;-)

   Notice that, from the definition of joinˡ⁺, the first and second lines in the above-reported error are actually equivalent. So, what's going on? Is it not "eta reducing"? And how would I get it to reduce?
lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- ( left k∈tˡˡ ) = {!left k∈tˡˡ!}
lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- ( right k∈tˡʳ ) = {!right ( left ( k∈tˡʳ ) )!}
lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼0 ) _ ∼- here = {!here!}
lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼0 ) _ ∼- ( left k∈tˡˡ ) = {!left k∈tˡˡ!}
lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼0 ) _ ∼- ( right k∈tˡʳ ) = {!right ( left ( k∈tˡʳ ) )!}
lemJoinˡ⁺IsCorrect ( 1# , _ ) _ ∼0 k∈tˡ = {!left k∈tˡ!}
lemJoinˡ⁺IsCorrect ( 1# , _ ) _ ∼+ k∈tˡ = {!left k∈tˡ!}
lemJoinˡ⁺IsCorrect ( 0# , _ ) _ _ k∈tˡ = left k∈tˡ

Martin Stone Davis

1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578
Electronic Mail: martin.stone.davis-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org
Agda mailing list
mechvel | 25 Aug 21:48 2015

simple with->case fail

I have

  f :  ∀ x → ¬ AnyRepeats (gfilter toSubsetIf (x ∷ []))
  f x  with member? x
  ...  | yes _ = noRepetition[x]
  ...  | no _  = noRepetition[]

which is type checked in  Agda
But its `case' version

  f x = case member? x of \ { (yes _) → noRepetition[x]
                            ; (no _)  → noRepetition[] }

leads to the report

   _x_170 x ∷ [] != [] of type List subC
   when checking that the expression noRepetition[] has type
   (AnyRepeats (_x_170 x ∷ []) → ⊥)

Is the first version  noRepetition[]  has the needed type,
and in the second has not.

May this be all right for the type checker?


Manuel Hermenegildo | 21 Aug 06:20 2015

CFP: 25th International Conference on Compiler Construction (CC)

[ Please forward. Apologies for any duplicates. ] 

                           CALL FOR PAPERS

   25th International Conference on Compiler Construction (CC 2016)

                  March 17-18 2016, Barcelona, Spain
            Co-located with CGO, HPCA, PPoPP, and EuroLLVM

Important dates

  Abstracts due:         13 November 2015 
  Papers due:            20 November 2015 
  Author notification:   27 January  2016
  Conference:            17-18 March 2016


The  International   Conference  on  Compiler  Construction   (CC)  is
interested in work  on processing programs in the  most general sense:
analyzing, transforming or executing input that describes how a system
operates,  including traditional  compiler construction  as a  special

Original contributions are solicited on the topics of interest which
include, but are not limited to:

- Compilation   and  interpretation   techniques,  including   program
  representation,  analysis, and  transformation; code  generation and
- Run-time techniques, including  memory management, virtual machines,
  and dynamic and just-in-time compilation;
- Programming   tools,   including  refactoring   editors,   checkers,
  verifiers, compilers, debuggers, and profilers;
- Techniques  for   specific  domains,   such  as   secure,  parallel,
  distributed, embedded or mobile environments;
- Design  and   implementation  of   novel  language   constructs  and
  programming models.

CC 2016 is the 25th edition  of the conference.  It will be co-located
with CGO, HPCA, PPoPP, and EuroLLVM on March 17-18 2016, in Barcelona,


Papers   should  be   submitted   electronically   via  EasyChair   at
https://easychair.org/conferences/?conf=cc2016.    Papers    must   be
written in English and be submitted  in pdf in ACM SIGPLAN proceedings
format  (http://www.sigplan.org/Resources/Author/).   The  proceedings
will  be  published in  the  ACM  Digital  Library  and will  be  made
available freely for the period around the conference.

Both regular  papers (up to  11 pages)  and tool papers  (up to 2  + 3
pages), are invited.   In tool papers the first part  (2 pages) should
describe the tool and the second (3 pages) explain the contents of the
demo that will be presented with examples and screenshots.

Submissions  must  adhere  strictly  to  the  page  limits,  including
bibliography, figures,  or appendices.   Submissions that  are clearly
too long  may be  rejected immediately.  Additional  material intended
for reviewers but not for publication in the final version ( listings,
data, proofs) may be included  in a clearly marked appendix. Submitted
papers  must  be unpublished  and  not  be submitted  for  publication
elsewhere.  A  condition of submission  is that, if the  submission is
accepted,  one of  the  authors  attends the  conference  to give  the


General Chair
  Ayal Zaks
  Intel and Technion, Israel

Program Committee Chair 
  Manuel Hermenegildo
  IMDEA SW Institute and Technical U. of Madrid, Spain

Program Committee
  Raj Barik, Intel Labs, Santa Clara, CA
  Uday Bondhugula, IIS Bangalore
  Maria Garzaran, U. of Illinois UC and Intel
  Laurie Hendren, McGill U.
  Manuel Hermenegildo, IMDEA and T.U. Madrid
  Xavier Leroy, INRIA
  Ondrej Lhotak, U of Waterloo
  Francesco Logozzo, Facebook
  Antoine Miné, Ecole Normale Supérieure, Paris
  Jose Morales, IMDEA SW
  Diego Novillo, Google
  Dorit Nuzman, Intel Haifa
  Jens Palsberg, UCLA
  Xipeng Shen, North Carolina State University
  Walid Taha, Rice U.
  Zheng Wang, Lancaster U.

Steering Committee
  Koen De Bosschere, Ghent U.
  Björn Franke, U. of Edinburgh
  Michael O'Boyle, U. of Edinburgh
  Albert Cohen, INRIA

Web site


Ryan Wright | 17 Aug 20:11 2015

Internship Opportunity at Galois: Winter/Sprint 2016

Galois has some exciting opportunities for interns in software research and engineering for the Winter/Spring of 2016. Most of our projects use Haskell to some extent, so this is a great chance to get experience applying functional programming to important real-world problems.

Please pass along this posting to anyone you think might be interested--even if they don't yet know Haskell!

Thank you,
Ryan Wright

# Galois Software Engineering/Research Intern #

Galois is currently seeking software engineering and research interns for Winter/Spring 2016 at all educational levels. We are committed to matching interns with exciting and engaging engineering work that fits their particular interests, creating lasting value for interns, Galois, and our community. A Galois internship is a chance to tackle cutting-edge, meaningful problems in a uniquely collaborative environment with world-leading researchers.

Roles may include technology research and development, requirements gathering, implementation, testing, formal verification, and infrastructure development. Past interns have integrated formal methods tools into larger projects, built comprehensive validation suites, synthesized high-performance cryptographic algorithms, written autopilots for quad-copters, designed the syntax and semantics of scripting languages, and researched type system extensions for academic publication.

We deeply believe in providing comprehensive support and mentorship to all of our employees, particularly interns. We provide our employees with a steward who regularly checks in to ensure that they feel welcome and safe in the Galois community while gaining real value from their experiences.

## Important Dates ##

Applications due: October 1st, 2015
Internship period (flexible): January through April, 2016

## About Galois ##

Our mission is to create trustworthiness in critical systems. We’re in the business of taking blue-sky ideas and turning them into real-world technology solutions. We’ve been developing real-world systems for over ten years using functional programming, language design, and formal methods.

Galois values diversity. We believe that differing viewpoints and experiences are essential to the process of innovation. We look broadly, including outside of established communities, to deliver innovation.

## How to Prepare ##

An internship is an opportunity for learning and growth as an engineer. To make the most of the opportunity, we ask that candidates have experience reading, writing, and maintaining code in a realistic project. Many university courses involve multi-week collaborative projects that provide this type of experience.

Most of our projects use the Haskell programming language and the git version control system. These tools aren’t often taught in computer science classes, but there are many free resources available that we recommend for learning:

- [Learn You a Haskell] for Great Good! [1] by Miran Lipovača
- [Real World Haskell] [2] by Bryan O’Sullivan, Don Stewart, and John Goerzen
- [tryGit] [3] by Code School
- [Pro Git] [4] by Scott Chacon

## Qualifications ##

The ability to be geographically located in Portland during the internship
Experience reading, writing, and maintaining code in a project as described above
Proficiency in software development practices such as design, documentation, testing, and the use of version control
Well-developed verbal and written communication skills; comfort in a collaborative team environment
The following skills are not required, but may be relevant to a particular project.

- Proficiency in Haskell or other programming languages with rich type systems (eg., OCaml, Standard ML, Scala)
- Experience using C and assembly languages for low-level systems programming
- Development experience in high assurance systems or security software
- Specific experience in an area of Galois’ expertise, such as:
  - Assured information sharing
  - Software modeling and formal verification
  - Cyber-physical systems and control systems
  - Operating systems, virtualization and secure platforms
  - Networking and mobile technology
  - Cyber defense systems
  - Scientific computing
  - Program analysis and software evaluation
  - Web security

## Logistics ##

The length and start date of the internship are negotiable: starting any time from the new year through next spring is acceptable, but an intern must be at Galois for at least three continuous months. The internship is paid competitively, and interns are responsible for living arrangements (although we can certainly help you find arrangements). Galois is located in the heart of downtown Portland with multiple public transportation options available and world-class bicycle infrastructure.

## Application Details ##

We’re looking for people who can invent, learn, think, and inspire. We reward creativity and thrive on collaboration. If you are interested, please send your cover letter and resume to us via http://galois-inc.hiringthing.com.
Agda mailing list
Jesper Cockx | 16 Aug 13:33 2015

Reminder: AIM XXII is in one month!

Dear all,

This is a gentle reminder that the twenty-second Agda Implementor's Meeting will be held in Leuven 16-22 September, which is in one month. If you want to attend, please fill out this form before 4 September: http://goo.gl/forms/5wav2d9C6q (soft deadline). More information can be found at http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXII.

Kind regards,

Agda mailing list
Sergei Meshveliani | 15 Aug 20:46 2015

type check cost for `open'


I have a problem of the  type check cost for the `open' declaration.

The project consists of about 20 files:

  Foo1.agda ... Foo18, OverIntegralRing-0.agda, OverIntegralRing-1.agda.

It is for               Agda
The machine is of       16 Gb RAM,  3 GHz.
Type checking is under  -M13G -H13G

(-A1G does not effect essentially).

The first 19 files are type-checked in 1-2 hours,
and I take this as "Anyway, it is done. let us type-check the next and

OverIntegralRing-0.agdai  has  12 Mb size.
Other .agdai files have         4 Mb on average.

There arises a question of type-checking  OverIntegralRing-1.agda.
This file is as follows:

************************************** OverIntegralRing-1.agda **
open import Level using ...
open import Relation.Binary using ...
open import Data.Nat using (ℕ; suc)

-- of DoCon-A --
open import Structures0 using (module Magma; module UpMagma)
open import Structures3 using (module IntegralRing; UpIntegralRing; 
                                                module UpIntegralRing) 
open import Factorization.FtMonoid using 
                                   (module OfCancellativeCommMonoid)
import OverIntegralRing-0   --

module OverIntegralRing-1 {α α=} (upIR : UpIntegralRing α α=)
                   (_∣?_ : let Mg = UpIntegralRing.*magma upIR
                           in  Decidable₂ $ Magma._∣_ Mg 
  open UpIntegralRing upIR using (...)
                renaming (Carrier to C; *upCommutativeMonoid to *upCMon)
  open IsEquivalence isEquivalence using () 
                  renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)
  open EqR setoid renaming (_≈⟨_⟩_ to _≈[_]_)
  open UpMagma *upMagma using (_∣_; _∤_; ∣cong₁; ∣cong₂; ∤cong₁)
                                                renaming (_~asd_ to _~_)
  open UpMonoid *upMonoid using (_^_; ^1=id; ∣trans)
  open CommutativeSemigroup *commutativeSemigroup using (bothFactors∣)
  open MonoidLemmata *upMonoid     using (^cong₁; x∣x; x^2≈xx)
  open RingLemmata   upRing        using (0*; ∣nonzero→≉0)
  open Ring1Lemmata  upRingWithOne using (∣1→≉0; 0^suc) 

{- -- expensive 
  open OverIntegralRing-0 upIR _∣?_ using                       
       (_∣'?_; *cancel-nz; *cMon-NZ; *upCMon-NZ; IsPrime; prime→≉0; 
        Factorization; IsPrime-nz→IsPrime; IsPrime→IsPrime-nz)

And that is all:  
only open several modules imported from previous files.

1. It is type-checked in  41 sec,  with  .agdai  of ~ 900 Kb
   (the smallest .agdai).

2. Uncomment the last `open'.
Then  30 min  is not enough to type-check. Many Gb are allocated.

Giving  14 Gb  leads to swapping, this slows down the process greatly
(I expect that on a 32 Gb machine and under -M24G it will type-check in 
1 minute).

I need to program several functions in this environment.
But this very environment fails to type check on a 16 Gb machine.

The are two functions set under  NO_TERMINATION_CHECK
-- this pragma will be removed after certain `panic' is fixed in Agda.
Probably, this pragma does not increase the type check cost
(can it?).

Is something wrong in the Agda implementation approach?
(a real sharing, the normal form interpreter ... I do not know).


Martin Stone Davis | 15 Aug 05:10 2015

A sticky refusal

NB Crossposted to http://stackoverflow.com/q/32021121/1312174.

This question is about

* how to help Agda get unstuck when solving unification problems, and
* how to convince Agda to solve a "heterogeneous constraint" (whatever that means)

The complete code for my question can be found [here](http://lpaste.net/138853). I'll lay out my code and eventually get to the question. My project concerns proving things in Data.AVL, so I start with some boilerplate for that:

    open import Data.Product
    open import Level
    open import Relation.Binary
    open import Relation.Binary.PropositionalEquality as P using (_≡_)

    module Data.AVL.Properties-Refuse
      {k v ℓ}
      {Key : Set k} (Value : Key → Set v)
      {_<_ : Rel Key ℓ}
      (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _<_) where

      open import Data.AVL Value isStrictTotalOrder using (KV; module Extended-key; module Height-invariants; module Indexed)
      import Data.AVL Value isStrictTotalOrder as AVL
      open Extended-key                      
      open Height-invariants                 
      open Indexed                           

      open IsStrictTotalOrder isStrictTotalOrder

I then borrow [an idea from Vitus](http://stackoverflow.com/a/21083647/1312174) to represent membership:

      data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
        here : ∀ {hˡ hʳ} V
          {l : Tree lb [ K ] hˡ}
          {r : Tree [ K ] ub hʳ}
          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
          K ∈ node (K , V) l r (proj₂ b)
        left : ∀ {hˡ hʳ K′} {V : Value K′}
          {l : Tree lb [ K′ ] hˡ}
          {r : Tree [ K′ ] ub hʳ}
          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
          K < K′ →
          K ∈ l →
          K ∈ node (K′ , V) l r (proj₂ b)
        right : ∀ {hˡ hʳ K′} {V : Value K′}
          {l : Tree lb [ K′ ] hˡ}
          {r : Tree [ K′ ] ub hʳ}
          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
          K′ < K →
          K ∈ r →
          K ∈ node (K′ , V) l r (proj₂ b)

I then declare a function (whose meaning is irrelevant -- this is a contrived and simple version of a more meaningful function not shown here):

      refuse1 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
      refuse1 = {!!}

So far, so good. Now, I case split on the default variables:

      refuse2 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
      refuse2 t k₁ k∈t = {!!}

And now I split on `t`:

      refuse3 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
      refuse3 (leaf l<u) k₁ k∈t = {!!}
      refuse3 (node k₁ t t₁ bal) k₂ k∈t = {!!}

And now on `bal`:

      refuse4 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
      refuse4 (leaf l<u) k₁ k∈t = {!!}
      refuse4 (node k₁ t t₁ ∼+) k₂ k∈t = {!!}
      refuse4 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
      refuse4 (node k₁ t t₁ &sim;-) k₂ k∈t = {!!}

The first error comes when I try to case split on `k∈t` of the equation including `(node ... ∼+)`:

      refuse5 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
      refuse5 (leaf l<u) k₁ k∈t = {!!}
      refuse5 (node k₁ t t₁ ∼+) k₂ k∈t = {!k∈t!}
      {- ERROR
        I'm not sure if there should be a case for the constructor here,
        because I get stuck when trying to solve the following unification
        problems (inferred index ≟ expected index):
          {_} ≟ {_}
          node (k₅ , V) l r (proj₂ b) ≟ node k₄
                                        t₂ t₃ ∼+
        when checking that the expression ? has type Set
      refuse5 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
      refuse5 (node k₁ t t₁ &sim;-) k₂ k∈t = {!!}

Agda tells me it gets stuck doing the unification, but it's not clear to me why or how to help. In [a response to a similar question](http://stackoverflow.com/q/30951993/1312174), Ulf suggested first case-splitting on another variable. So, now working by hand, I focus on case-splitting the `∼+` line from `refuse5` and include many of the implicit variables:

      open import Data.Nat.Base as ℕ

      refuse6 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
      refuse6 {h = ℕ.suc .hˡ}
              (node (k , V) lk ku (∼+ {n = hˡ}))
              (here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku} {b = (ℕ.suc .hˡ , ∼+ {n = .hˡ})}) = {!!}
      {- ERROR
        Refuse to solve heterogeneous constraint proj₂ b :
        n ∼ hʳ ⊔ proj₁ b =?=
        ∼+ : n ∼ ℕ.suc n ⊔ ℕ.suc n
        when checking that the pattern
        here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}
          {b = ℕ.suc .hˡ , ∼+ {n = .hˡ}}
        has type
        k₂ ∈ node (k₁ , V) lk ku ∼+
      refuse6 _ _ _ = ?

Oops. Now Agda goes from complaining that it's stuck to downright refusing to solve. What's going on here? Is it possible to specify the lhs of the equations with at least as much detail as in refuse5 **and also** case split on `k∈t`? If so, how?
Martin Stone Davis

1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578
Electronic Mail: martin.stone.davis <at> gmail.com
Agda mailing list
effectfully | 13 Aug 23:52 2015

The proving cycle.

Hi. That's how I define a recursive function in Agda:

1) f : {A} -> B -> C -> D
    f y z = {!!}

2) Split on `y' or `z'. At this stage Agda often changes code
formatting and makes e.g.

    f : {A} -> B -> C -> D
    f {x} y z = {!!}


    f : {A} -> B -> C -> D
    f {x = x} y z = {!!}

I revert these changes.

3) Look at the context and the type of a term. Very often the context
and the term are not normalized, and I need to do this manually. Terms
usually contain implicit arguments, so C-c C-n doesn't work, and I
have to bind these implicits, again manually.

4) Remove stuff like (λ {.x} {.y} → ...).

5) When everything become explicit, I type C-c C-n and sometimes get
(_42 a dh dfh f sd). Agda doesn't display implicits in terms (as to
ShowImplicit: [1]), so it's sometimes impossible to meaningfully
normalize a term without additionally instantiating some implicits,
which can be non-trivial.

6) C-c C-r time. Agda again ignores my formatting, so I copy an
expression, refine the hole, delete the mess that Agda made from my
code (it sometimes even doesn't typecheck, especially when sections
are involved: Agda outputs something like (λ .section₀ → .section₀ +
m)) and paste the untouched expression.

When terms are large the whole process may take up to 20 minutes or
even more. Then I prove the theorem in 2 minutes.

Am I doing something wrong?

Here are some proposals:

1) The ability to normalize the type of a term in a context. The
ability to see the normalized type of a term in a hole (i.e. something
similar to C-c C-d or C-c C-., but with full normalization). The
ability to normalize a whole context.

2) Refine doesn't change formatting.

3) Something like C-c C-i makes an implicit explicit. I.e. C-c C-i i makes

i : I
x : A


.i : I
x : A

and inserts a lambda in the appropriate place.

4) More control on how things are evaluated. I rarely want `map' to be
unfolded into `replicate' and `_⊛_', but I always want `const', `_∘_',
`uncurry' and other combinators to be unfolded fully (which can
probably be a good heuristic on its own).

5) It would be nice, if it would be possible to declare fixities for
arguments. Maybe something like (infixl 6 _+_ : ℕ -> ℕ -> ℕ).

I realize that most of these proposals are fairly complex, but I hope
it's not just me being silly and there are other people that have
problems with using Agda, when complicated terms are involved. I'd
also appreciate if someone told me how to make the process of writing
code in Agda more straightforward.

Thanks for the attention.

[1] http://lpaste.net/138758