aspiwack

(** A "function" of the form [forall x, exists y, R x y] can be mapped
over a list [l], and produces [exists l', Forall2 R l l'], where
[Forall2 R l l'] means that [l] and [l'] have the same length and
elements at corresponding positions are related by [R].
We basically use the fact that the propositional truncation (written
[[A]] in this file) is a monad, and lists are traversable
(see http://hackage.haskell.org/package/base-4.7.0.0/docs/Data-Traversable.html )
*)
 
Require Import Coq.Lists.List.

aspiwack

(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)

Require Coq.Lists.List.

Definition IList (A:Set) : Set :=
  forall R:Set, (A->R->R) -> R -> R
.

Definition empty {A:Set} : IList A :=
  fun R c e => e

aspiwack

(** Infinite stacks with fast lookups. *)
 
(** Using co-inductive tries over binary positive integers, it is
remarkably easy to write infinite stack operations. While
maintaining an access in log(n) to the n-th element of the
stack. Of course [push] and [pull] are not constant time. I'm not
sure what the exact (amortised) complexity is. But both operation
are fairly elegant, and both their definitions and proof of
correctness are remarkably short and easy. *)
 

aspiwack

(** In this file we go a little further and follow the derivation
    proposed by Jeremy Gibbons (
    http://patternsinfp.wordpress.com/2011/05/05/horners-rule/ ).  It
    uses the definitions in Scan.v. The problem is to compute the
    maximum sum of consecutive elements in a list [l]. It happens that
    there is a linear time solution for that problem. Again, we start
    with a simple executable specification, and using appropriate
    rewriting steps, we find the linear time solution. *)

Require Import Prelim List NList Scan.

aspiwack

Definition compose {A B C:Type} (f:A->B) (g:B->C) : A->C := fun x => g (f x).
Arguments compose {A B C} f g x /.
Notation "g ∘ f" := (compose f g) (at level 3, left associativity).

Definition id {A:Type} : A -> A := fun x => x.
Arguments id {A} x /.


(** The impredicative encoding of functions. There is a bit of
    cheating as it is not actually an impredicative

aspiwack

type void = { ex_falso : 'a.'a }

module Eq = struct

  (** Leibniz equality. *)
  type (_,_) t = Refl : ('a,'a) t

  (** Variant of equality with a dummy case used to prove disequalities. *)
  type (_,_) u = Refl' : ('a,'a) u | Dummy : void -> ('a,'b) u

aspiwack

(***

    Impredicative Pearl.

    The file below demonstrates that it cannot be shown, in a
    predicative theory, that the functors between fixed categories
    together with natural transformations form a category. This, in
    turn, implies that one cannot prove that the categories with
    functors and natural transformations form a bicategory (unless we
    give up on the idea that the homs of bicategories are categories).

aspiwack

(* Must be ran with -impredicative-set *)

(* This files briefly demonstrates that the impredicative encoding of
   inductive fixed point (μα.F α is encoded as ∀α.(F α→α)→α) can also
   be used for mutual inductive types. The inductive definition is
   represented as a binary eliminator E α β, (α and β being
   placeholder for the respective types), the first type is then
   ∀αβ.E α β→α, the second one ∀αβ.E α β→β.

   In the non-mutual case, an eliminator is simply F α→α. However, in

aspiwack

-- Multi-prompted shift/reset in metalua
-- after Roshan James & Amr Sabry @ http://parametricity.net/dropbox/yield.subc.pdf
-- indepth comments and explanation are to be found in the paper.
-- The addition of multi-prompt is mine (Arnaud Spiwack) and documented in the
-- only function I had to change significantly from the single-prompted one
-- (namely runco). The rest is just carrying the prompt around.
-- The implementation is ok as long as continuations are not used twice.
-- To be work properly in all generality, the coroutine.clone primitive
-- must be implemented. There exists a patch against Lua 5.1 to that effect.
-- Hopefully it'll make it into the distribution soon.