This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* -*- 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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. *) | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(*** | |
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). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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. |
NewerOlder