mbrcknl

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Definition rev_spec (X: Type) (rev: list X -> list X) :=
  (forall x, rev [x] = [x]) /\ (forall xs ys, rev (xs ++ ys) = rev ys ++ rev xs).

Lemma app_eq_nil: forall (X: Type) (xs ys: list X), xs ++ ys = xs -> ys = [].
  induction xs; simpl; inversion 1; auto.

mbrcknl

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Fixpoint reverse (X: Type) (xs: list X): list X :=
  match xs with
    | [] => []
    | x :: xs' => reverse xs' ++ [x]
  end.

mbrcknl

Lemma list_narrow_ind:
  forall
    (X: Type)
    (P: list X -> Prop)
    (H: P [])
    (J: forall x, P [x])
    (K: forall x ys z, P ys -> P (x :: ys ++ [z]))
    (l: list X),
    P l.
Proof.

mbrcknl

Lemma list_len_odd_even_ind:
  forall
    (X: Type)
    (P: list X -> Prop)
    (H: forall xs, length xs = 0 -> P xs)
    (J: forall xs, length xs = 1 -> P xs)
    (K: forall xs n, length xs = n -> P xs -> forall ys, length ys = S (S n) -> P ys)
    (l: list X),
    P l.
Proof.

mbrcknl

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  induction l as [|[x y] ps];
  try (simpl; destruct (split ps));
  inversion 1;
  try (simpl; apply f_equal; apply IHps);
  reflexivity.
Qed.

mbrcknl

Fixpoint split
           {X Y : Type} (l : list (X*Y))
           : (list X) * (list Y) :=
  match l with
    | nil => (nil, nil)
    | (x,y) :: t =>
      let (r,s) := split t in
      (x :: r, y :: s)
  end.

mbrcknl

{-# LANGUAGE RankNTypes #-}

import Control.Lens.Lens (Lens,lens)

type Quotient s t a = forall b. Lens s t a b

quotient :: (s -> a) -> (s -> t) -> Quotient s t a
quotient sa st = lens sa (const . st)

mbrcknl

{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

-- Richard Bird, Thinking Functionally with Haskell.
-- Chapter 2, Exercise E:

mbrcknl

{-# LANGUAGE Rank2Types #-}

type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t)

type Ref s t a b = s -> Rep a b t
data Rep a b t = Rep a (b -> t)

instance Functor (Rep a b) where
  fmap f (Rep a g) = Rep a (f . g)

mbrcknl

Difference Lists

Proposed BFPG lightning talk. 25 slides, 5 minutes, 12 seconds per slide. No problem!

September 2014

1

Motivation: we want to write something as clear as this, but this is O(n^2).