Sergei Meshveliani | 19 Oct 18:06 2014
Picon

explicit irrelevance question

Dear Agda developers,

can you, please tell whether the below statement  g=f-if
must have a proof in Agda ?
If yes, then what can be a proof ?

(I am stuck with both explicit irrelevance and a dot-annotated
irrelevance). 

Thanks,

------
Sergei

--------------------------------------------------------------
open import Level            using (_⊔_)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary  using (module IsEquivalence;
                                    module DecSetoid; DecSetoid)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty using (⊥-elim)

module _ {α α=} (A : DecSetoid α α=) (0# : DecSetoid.Carrier A)
  where
  open DecSetoid A using (_≈_; _≟_; isEquivalence)
                                    renaming (Carrier to C)
  open IsEquivalence isEquivalence renaming (refl to ≈refl)

  record Foo : Set (α ⊔ α=)
(Continue reading)

Helmut Grohne | 15 Oct 13:15 2014
Picon

Internal error at src/full/Agda/TypeChecking/Substitute.hs:144

Dear Agda developers,

While refactoring some Agda code I ran into the following error message:

| Checking Error (../full/path/to/Error.agda).
| An internal error has occurred. Please report this as a bug.
| Location of the error: src/full/Agda/TypeChecking/Substitute.hs:144

This is produced using Agda 2.4.2 as obtained using cabal on a Linux
amd64 system with GHC 7.6.3.

I went ahead and tried to find a reproducer with less than 1000 lines.
After feeding Agda 30000 samples, I came up with the following 7 lines:

data A (B : Set) : Set where
module C where
  record D : Set where
module E (F : Set) (G : A F) where
  open C public using (module D)
module H (I : Set) (J : A I) where
  open E I J using ()

Is this also reproducible on the development version of Agda?

Helmut
Andrew Harris | 14 Oct 04:13 2014
Picon

simple question

Hello,

   I'm trying to follow along in the very good paper "Dependent Types At Work" written by Ana Bove and Peter Dybjer.  I'm stuck at trying to prove "eq-succ", which is one of the exercises in Section 4.4.  The closest I can make it is the following:

{- proof of eq-succ -}
eq-succ : {n m : Nat} → n == m → succ n == succ m
eq-succ (refl m) = natrec {(\k → (k + m) == (plus k m))} (refl m) (\i h → ((succ i) + m) == (plus (succ i) m)) m

But this does not typecheck, I get the error:

Set !=< (succ i + m) == plus (succ i) m of type Set₁
when checking that the expression (succ i + m) == plus (succ i) m
has type (succ i + m) == plus (succ i) m

I'm stuck -- I don't quite understand what I'm supposed to create an element of Set_1 that has a signature of (succ i + m) == plus (succ i) m, (if that's what I'm supposed to do).  Any hints would be appreciated!

-andrew
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Pepijn Kokke | 12 Oct 13:28 2014
Picon

Expanding literate Agda

Dear all,

I've implemented a pre-processor to "unlit" various styles of literate code, i.e. LaTeX-style, bird tags, Markdown-style code blocks, etcetera. I'm currently trying to integrate it into Agda. There are currently two proposals for how to do this.

The first is the following:

Try to infer the literate format from the file, making it explicit with Agda command-line arguments if necessary. 
 
This would mean that, for instance, if the "unlit" program would encounter a "\begin{code}" tag, it would assume the literate Agda file was was written in LaTeX style, if it encountered a "```" fence it would assume Markdown, etcetera... 
(I would personally prefer that a bird tag would also indicate Markdown, because the two formats integrate so well and are already used in this manner in the Haskell community.)
 
The advantages of this approach is that it can easily be integrated into the current Agda, and all literate files would have the .lagda extension.
 
In the case where it is desirable to mix formats in a strange way (i.e. mix bird tags and LaTeX or even LaTeX blocks and Markdown blocks) command-line arguments could be passed to Agda explicitly stating the literate style---though I'm guessing this would never be necessary.

The second proposal is the following:

Each style of literate Agda would have its own extension. For instance: LaTeX-style would ".agda.tex", Markdown would use ".agda.md" and Bird-style would use ".agda.txt". 
 
The advantages of this approach is that there is no inference needed, as the format will be unambiguously specified in the extension. 
 
The problem with this approach is that it will require modifications to many parts of the Agda ecosystem. For instance, the code that resolves module names to files would have to change to also take ".agda.tex" and such into consideration. The same modifications would probably have to be made for the Emacs (and other) editing mode. This would constitute many (trivial) changes across the Agda codebase. 

I'd like to hear your thoughts on these different approaches, or---if you have proposals of dealing with this in a different manner---how you would solve this problem.

Regards,
Pepijn
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
José Pedro Magalhães | 10 Oct 14:58 2014
Picon
Picon

Mathematics of Program Construction (MPC 2015): first call for papers

Apologies for multiple copies.

FIRST CALL FOR PAPERS

12th International Conference on Mathematics of Program Construction (MPC 2015)
Königswinter, Germany, 29 June - 1 July 2015


BACKGROUND

The MPC conferences aim to promote the development of mathematical principles
and techniques that are demonstrably practical and effective in the process of
constructing computer programs, broadly interpreted.

The 2015 MPC conference will be held in Königswinter, Germany, from 29th June to
1st July 2015. The previous conferences were held in Twente, The Netherlands
(1989), Oxford, UK (1992), Kloster Irsee, Germany (1995), Marstrand, Sweden
(1998), Ponte de Lima, Portugal (2000), Dagstuhl, Germany (2002), Stirling, UK
(2004, colocated with AMAST), Kuressaare, Estonia (2006, colocated with AMAST),
Marseille, France (2008), Québec City, Canada (2010, colocated with AMAST), and
Madrid, Spain (2012).


TOPICS

Papers are solicited on mathematical methods and tools put to use in program
construction. Topics of interest range from algorithmics to support for program
construction in programming languages and systems. The notion of "program" is
broad, from algorithms to hardware. Some typical areas are type systems, program
analysis and transformation, programming-language semantics, security, and
program logics. Theoretical contributions are welcome, provided that their
relevance to program construction is clear. Reports on applications are welcome,
provided that their mathematical basis is evident.

We also encourage the submission of "pearls": elegant, instructive, and fun
essays on the mathematics of program construction.


IMPORTANT DATES

   * Submission of abstracts:      26 January 2015
   * Submission of full papers:     2 February 2015
   * Notification to authors:      16 March 2015
   * Final version:                13 April 2015


SUBMISSION

Submission is in two stages. Abstracts (plain text, 10 to 20 lines) must be
submitted by 26 January 2015. Full papers (pdf) adhering to the LaTeX llncs
style must be submitted by 2 February 2015. There is no official page limit, but
authors should strive for brevity. The web-based system EasyChair will be used

Papers must report previously unpublished work, and must not be submitted
concurrently to a journal or to another conference with refereed proceedings.
Accepted papers must be presented at the conference by one of the authors.
Please feel free to write to mpc2015-bC77Qfv0vuxrovVCs/uTlw@public.gmane.org with any questions
about academic matters.

The proceedings of MPC 2015 will be published in Springer-Verlag's Lecture Notes
in Computer Science series, as have all the previous editions. Authors of
accepted papers will be expected to transfer copyright to Springer for this
purpose. After the conference, authors of the best papers will be invited to
submit revised versions to a special issue of the Elsevier journal Science of
Computer Programming.


PROGRAMME COMMITTEE

Ralf Hinze                University of Oxford, UK (chair)

Eerke Boiten              University of Kent, UK
Jules Desharnais          Université Laval, Canada
Lindsay Groves            Victoria University of Wellington, New Zealand
Zhenjiang Hu              National Institute of Informatics, Japan
Graham Hutton             University of Nottingham, UK
Johan Jeuring             Utrecht University and Open University, The Netherlands
Jay McCarthy              Vassar College, US
Bernhard Möller           Universität Augsburg, Germany
Shin-Cheng Mu             Academia Sinica, Taiwan
Dave Naumann              Stevens Institute of Technology, US
Pablo Nogueira            Universidad Politécnica de Madrid, Spain
Ulf Norell                University of Gothenburg, Sweden
Bruno C. d. S. Oliveira   The University of Hong Kong, Hong Kong
José Nuno Oliveira        Universidade do Minho, Portugal
Alberto Pardo             Universidad de la República, Uruguay
Christine Paulin-Mohring  INRIA-Université Paris-Sud, France
Tom Schrijvers  KU Leuven, Belgium
Emil Sekerinski           McMaster University, Canada
Tim Sheard                Portland State University, US
Anya Tafliovich           University of Toronto Scarborough, Canada
Tarmo Uustalu             Institute of Cybernetics, Estonia
Janis Voigtländer         Universität Bonn, Germany


VENUE

The conference will take place in Königswinter, Maritim Hotel, where
accommodation has been reserved. Königswinter is situated on the right bank of
the river Rhine, opposite Germany's former capital Bonn, at the foot of the
Siebengebirge.


LOCAL ORGANIZERS

Ralf Hinze                      University of Oxford, UK (co-chair)
Janis Voigtländer               Universität Bonn, Germany (co-chair)
José Pedro Magalhães            University of Oxford, UK
Nicolas Wu                      University of Oxford, UK

For queries about local matters, please write to jv-jNDFPZUTrfTJi8DqpkIagcUtbM6s6Vk+@public.gmane.org.

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Dmytro Starosud | 11 Oct 21:50 2014
Picon

(Stronger) double negation of law of excluded middle

Hello everyone

Could you have a look at my problem below?
I am trying to prove something that looks like just better double negation of law of excluded middle:

¬¬lem : ¬ ¬ ((A : Set) → A ⊎ ¬ A)
¬¬lem = _

Which I cannot prove, whereas following one is pretty easy to prove:

¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))

Is it actually possible to prove the first one in constructive logic (in particular in Agda)?

Thanks in advance for your help!

Best regards,
Dmytro

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani | 10 Oct 17:44 2014
Picon

map⊆

People,
I program mapping the _⊆_ relation on lists:

  ...

  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → {xs ys : List C} →
                                          xs ⊆ ys → map f xs ⊆' map f ys

  map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs =
       let
         (x , x∈≡xs , fx≈z) = counter-map f xs z z∈f-xs
         x∈xs    = ∈≡→∈ x∈≡xs
         x∈ys    = xs⊆ys x∈xs
         fx∈f-ys = map∈ f fCong x∈ys
       in
       cong₁∈' fx≈z fx∈f-ys

Here _≈_ and _≈'_ are of the two corresponding setoids.
This implementation uses 

 map∈ : (f : C → C')  → (f Preserves _≈_ ⟶ _≈'_) → {x : C} →
        {xs : List C} → x ∈ xs                   → f x ∈' map f xs 
 ,
 counter-map : (f : C → C') → (xs : List C) → (y : C') → y ∈' map f xs →
                                               ∃ \x → x ∈≡ xs × f x ≈' y
 ,
 cong₁∈' : {zs : List C'} → (\x → x ∈' zs) Respects _≈'_

-- which I implement in their turn.

And I wonder of whether all this is inventing a bicycle.
Can  map⊆  be expressed in a simpler way?
What Standard library has for all this?

Thanks,

------
Sergei
Andrea Vezzosi | 10 Oct 17:11 2014
Picon

Re: Restrictions on 'with' introductions?

If you want to understand "with" better you can look at the "More in
depth" part of this:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.With-expression

I find that with enough type dependencies the "with" construct only
makes sense if you think of its desugaring into an helper function. It
should also clarify the meaning of the "w" variables in the error
messages.

Cheers,
Andrea

On Tue, Oct 7, 2014 at 2:31 AM, Dan Krejsa <dan.krejsa@...> wrote:
> Hi,
>
> I'm trying to work through a self-imposed exercise in Agda, proving
> that a functional insertion sort algorithm on lists is correct (i.e., it
> produces
> an ordered list that is in fact a permutation of the original list).
> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit
> is proving something of a pain to me.  In particular, I'm developing all the
> permutation infrastructure myself...)
>
> In any case, I notice that I'm structuring a lot of the more difficult
> proofs / functions as a long chain of 'with' patterns  (here's a short one):
>
> some_func : type
> some_func  args  with term1 | term 2
> ... | term1-deconstructed | term2-deconstructed  with f x y
> ... | fxy  with term4
> ... | term4 = ?
>
> However, sometimes when I try to add a well-typed term to
> the values scrutinized via the 'with' , Agda complains of some type
> error 'when checking that the type <some long type> of the generated with
> function is well-formed'.
>
> For instance, maybe the above example works fine, but if I also try to
> get Agda to remember that fxy = f x y using inspect-on-steroids,
>
> some_func : type
> some_func  args  with term1 | term 2
> ... | term1-deconstructed | term2-deconstructed  with f x y | inspect (f x)
> y
> ... | fxy | [ fxydef ] with term4
> ... | term4 = ?
>
> then I get a type error about the generated with-function.  (That's just an
> example, other sorts of as-far-as-I-can-see good terms sometimes also cause
> similar problems.)
>
> So, I don't really understand what the 'with function' is, and what are the
> restrictions on the terms that one can scrutinize using 'with'.
>
> Or, if this is just a shortcoming/bug in current Agda, what would be a
> workaround for such a case?
>
> Thanks,
>
> - Dan
>
> P.S. I could post my file, but it's pretty hairy still. (I could try to find
> a small or minimal test case if this is not already a known problem.)
>
> That reminds me: is there a good forum for asking for help improving
> practical Agda proving style & skills?  I'm not in school and am learning
> mostly on my own out of personal interest.  I'm hoping to improve my nose
> for 'code smells' in Agda, things like the 'green slime' mentioned in a
> recent Connor McBride paper ;-)
>
>
>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>
Nils Anders Danielsson | 10 Oct 17:00 2014
Picon
Picon

Re: Restrictions on 'with' introductions?

On 2014-10-07 02:31, Dan Krejsa wrote:
> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit
> is proving something of a pain to me.  In particular, I'm developing all the
> permutation infrastructure myself...)

Proofs of this kind are hopefully easy (but perhaps boring) if you use
the technique that I describe in "Bag Equivalence via a Proof-Relevant
Membership Relation":

   http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence.html

For instance, here's how one can implement tree sort, and prove that the
output is a permutation of the input:

   http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence/Tree-sort.Partial.html

The following code by Bob Atkey uses a different approach, embedding
linear logic inside Agda to give you the permutation property "for
free":

   https://github.com/bobatkey/sorting-types/blob/master/agda/Linear.agda

--

-- 
/NAD
David Van Horn | 10 Oct 00:23 2014

ICFP 2015 Call for Workshop and Co-located Event Proposals

         CALL FOR WORKSHOP AND CO-LOCATED EVENT PROPOSALS
                            ICFP 2015
 20th ACM SIGPLAN International Conference on Functional Programming
                   August 30 - September 5, 2015
                        Vancouver, Canada
               http://icfpconference.org/icfp2015/

The 120th ACM SIGPLAN International Conference on Functional
Programming will be held in Vancouver, British Columbia, Canada on
August 30-September 5, 2015.  ICFP provides a forum for researchers
and developers to hear about the latest work on the design,
implementations, principles, and uses of functional programming.

Proposals are invited for workshops (and other co-located events, such
as tutorials) to be affiliated with ICFP 2015 and sponsored by
SIGPLAN. These events should be less formal and more focused than ICFP
itself, include sessions that enable interaction among the attendees,
and foster the exchange of new ideas. The preference is for one-day
events, but other schedules can also be considered.

The workshops are scheduled to occur on August 30 (the day
before ICFP) and September 3-5 (the three days after ICFP).

----------------------------------------------------------------------

Submission details
 Deadline for submission:     November 16, 2014
 Notification of acceptance:  December 15, 2014

Prospective organizers of workshops or other co-located events are
invited to submit a completed workshop proposal form in plain text
format to the ICFP 2015 workshop co-chairs (Tom Schrijvers and Nicolas
Wu), via email to icfp2015-workshops@... by November 16,
2014. (For proposals of co-located events other than workshops, please
fill in the workshop proposal form and just leave blank any sections
that do not apply.) Please note that this is a firm deadline.

Organizers will be notified if their event proposal is accepted by
December 15, 2014, and if successful, depending on the event, they
will be asked to produce a final report after the event has taken
place that is suitable for publication in SIGPLAN Notices.

The proposal form is available at:

http://www.icfpconference.org/icfp2015/icfp15-workshops-form.txt

Further information about SIGPLAN sponsorship is available at:

"http://www.sigplan.org/Resources/Guidelines/Workshops

----------------------------------------------------------------------

Selection committee

The proposals will be evaluated by a committee comprising the
following members of the ICFP 2015 organizing committee, together with
the members of the SIGPLAN executive committee.

 Workshop Co-Chair: Tom Schrijvers                         (KU Leuven)
 Workshop Co-Chair: Nicolas Wu                  (University of Oxford)
 General Chair:     Kathleen Fisher                 (Tufts University)
 Program Chair:     John Reppy                 (University of Chicago)

----------------------------------------------------------------------

Further information

Any queries should be addressed to the workshop co-chairs (Tom
Schrijvers and Nicolas Wu), via email to
icfp2015-workshops@...
Andreas Abel | 9 Oct 20:22 2014
Picon

Re: Restrictions on 'with' introductions?

Dan this may well be a bug in Agda.  This might be a related issue:

   https://code.google.com/p/agda/issues/detail?id=745

If you have test case that exhibits the problem, please add it to the 
issue tracker.

Cheers,
Andreas

On 07.10.2014 02:31, Dan Krejsa wrote:
> Hi,
>
> I'm trying to work through a self-imposed exercise in Agda, proving
> that a functional insertion sort algorithm on lists is correct (i.e., it
> produces
> an ordered list that is in fact a permutation of the original list).
> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit
> is proving something of a pain to me.  In particular, I'm developing all the
> permutation infrastructure myself...)
>
> In any case, I notice that I'm structuring a lot of the more difficult
> proofs / functions as a long chain of 'with' patterns  (here's a short one):
>
> some_func : type
> some_func  args  with term1 | term 2
> ... | term1-deconstructed | term2-deconstructed  with f x y
> ... | fxy  with term4
> ... | term4 = ?
>
> However, sometimes when I try to add a well-typed term to
> the values scrutinized via the 'with' , Agda complains of some type
> error 'when checking that the type <some long type> of the generated
> with function is well-formed'.
>
> For instance, maybe the above example works fine, but if I also try to
> get Agda to remember that fxy = f x y using inspect-on-steroids,
>
> some_func : type
> some_func  args  with term1 | term 2
> ... | term1-deconstructed | term2-deconstructed  with f x y | inspect (f
> x) y
> ... | fxy | [ fxydef ] with term4
> ... | term4 = ?
>
> then I get a type error about the generated with-function.  (That's just
> an example, other sorts of as-far-as-I-can-see good terms sometimes also
> cause similar problems.)
>
> So, I don't really understand what the 'with function' is, and what are
> the restrictions on the terms that one can scrutinize using 'with'.
>
> Or, if this is just a shortcoming/bug in current Agda, what would be a
> workaround for such a case?
>
> Thanks,
>
> - Dan
>
> P.S. I could post my file, but it's pretty hairy still. (I could try to
> find a small or minimal test case if this is not already a known problem.)
>
> That reminds me: is there a good forum for asking for help improving
> practical Agda proving style & skills?  I'm not in school and am
> learning mostly on my own out of personal interest.  I'm hoping to
> improve my nose for 'code smells' in Agda, things like the 'green slime'
> mentioned in a recent Connor McBride paper ;-)
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>

--

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

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

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/

Gmane