flickyfrans

import Data.Array
import Data.Array.ST
import Control.Monad
import Control.Monad.ST
import Data.Maybe
import Data.Functor
import Control.Monad.Trans.State

f <.> g = liftM f . g

flickyfrans

-- This is related to http://stackoverflow.com/questions/27029564/how-do-i-build-a-list-with-a-dependently-typed-length/

{-# LANGUAGE GADTs, KindSignatures, DataKinds, PolyKinds, RankNTypes, TypeOperators #-}

import Data.Either
import Data.Functor
import Control.Monad

data Nat = Z | S Nat

flickyfrans

-- This is related to http://stackoverflow.com/questions/24475546/non-tedious-ast-transformation-proofs-in-agda/

open import Level
open import Function
open import Relation.Nullary.Core
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Bool
open import Data.Product hiding (map)

flickyfrans

{-# OPTIONS --no-positivity-check #-}

open import Level as Le
open import Function
open import Data.Maybe renaming (map to _<$>_)

infixl 4 _<*>_
_<*>_ : ∀ {α β} {A : Set α} {B : Set β} -> Maybe (A -> B) -> Maybe A -> Maybe B
just f <*> just x = just (f x)
_      <*> _      = nothing

flickyfrans

open import Level as Le
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Product hiding (map)
open import Data.Nat as N hiding (_⊔_)
open import Data.Vec

N-ary-level-Vec' : ∀ {n} -> Vec Level n -> Level -> Level
N-ary-level-Vec' = flip $ foldr _ Le._⊔_

flickyfrans

-- This is related to http://stackoverflow.com/questions/26615082/how-does-one-prove-a-type-of-the-form-a-b-in-agda

open import Function
open import Relation.Binary.PropositionalEquality

data Int : Set where
  Z : Int
  S : Int -> Int
  P : Int -> Int

flickyfrans

-- totally isomorphic to [], even in a strict monad
-- no redundant (<= 0) checks in the `drop' function
-- the `zipWith' function is still O(n^2)

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE BangPatterns #-}

import Data.List
import Control.Applicative
import Control.Monad

flickyfrans

Require Import Arith omega.Omega Lists.List.
Import ListNotations.

Fixpoint ble_nat (n m : nat) : bool :=
 match n with
 | 0    => true
 | S n' =>
    match m with
    | 0    => false
    | S m' => ble_nat n' m'

flickyfrans

(** * Hoare2: Hoare Logic, Part II *)

Require Export Hoare.


(* ####################################################### *)
(** * Decorated Programs *)

(** The beauty of Hoare Logic is that it is _compositional_ --
    the structure of proofs exactly follows the structure of programs.

flickyfrans

-- This is inspired by https://github.com/luqui/experiments/blob/master/Fin-inj.agda

open import Function
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality using (refl ; _≅_ ; _≇_ )
open import Data.Empty
open import Data.Nat
open import Data.Fin as F hiding (_+_)