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

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

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

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

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

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

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

Keybase proof

I hereby claim:

• I am mbrcknl on github.
• I am mbrcknl (https://keybase.io/mbrcknl) on keybase.
• I have a public key whose fingerprint is 37B9 11E4 FB0C 3331 D832 1E56 3F92 8682 66EE 73F0

To claim this, I am signing this object:

mbrcknl

data bool : Set where
  tt : bool
  ff : bool

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n

mbrcknl

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
succ m + n = succ (m + n)

_×_ : ℕ → ℕ → ℕ
zero × n = zero