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

mbrcknl

{-# LANGUAGE ScopedTypeVariables #-}

-- | Solve the r-peg Towers of Hanoi puzzle, using the Frame-Stewart algorithm.

module Hanoi where

import Prelude
  ( Bool(..), Int, Integer, Integral, Eq(..), Ord(..), Ordering(..)
  , error, fst, length, map, otherwise, snd, (+), (++), (-), (*), ($)
  , minimum, head, last

mbrcknl

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March 2015

open import Agda.Primitive using (_⊔_)

postulate
  String : Set

{-# BUILTIN STRING String #-}

mbrcknl

Definition red_split_a {red: red_type} {e: aexp} (ret: red_cexp red a e): red_aexp red e :=
  match ret in red_cexp _ t e return
        (match t return exp_type t -> Type with
           | a => fun e' => red_aexp red e'
           | b => fun _  => unit
         end e)
  with
    | RCNum       n     => RANum   n
    | RCPlus  _ _ a1 a2 => RAPlus  a1 a2
    | RCMinus _ _ a1 a2 => RAMinus a1 a2