AndrasKovacs’s gists

AndrasKovacs / Pigeon.v

Created July 18, 2015 21:32

Pigeonhole principle in Coq

	Section Pigeon.
	Require Import List.
	Require Import Arith.
	Variable A : Type.

	Definition Unique : list A -> Prop :=
	list_rect _ True (fun x xs hyp => ~(In x xs) /\ hyp).

	Definition Sub (xs ys : list A) : Prop := forall {x}, In x xs -> In x ys.

AndrasKovacs / FinSigma.agda

Created July 17, 2015 18:29

Finite sums of finite types are finite (ugly proof!)


	open import Data.Nat
	open import Data.Fin hiding (_+_)
	open import Function
	open import Relation.Binary.PropositionalEquality
	open import Data.Product renaming (map to pmap)
	open import Data.Vec renaming (map to vmap) hiding ([_])
	open import Data.Unit
	open import Data.Sum renaming (map to smap)
	open import Level renaming (zero to lzero; suc to lsuc)

AndrasKovacs / Inord.idr

Created June 7, 2015 10:31

The (positions of elements in a binary tree) and (the positions in its inorder traversal) are isomorphic.


	import Data.List
	%default total

	data Tree : Type -> Type where
	Tip : Tree a
	Node : (x : a) -> (l : Tree a) -> (r : Tree a) -> Tree a
	%name Tree t, u

	data InTree : a -> Tree a -> Type where

AndrasKovacs / PreIn.agda

Created June 7, 2015 10:00

Binary trees are unambiguously identified by their preorder and inorder traversals.


	module _ (A : Set) where

	open import Data.Empty
	open import Data.List hiding ([_])
	open import Data.Nat
	open import Data.Product renaming (map to productMap)
	open import Data.Sum renaming (map to sumMap)
	open import Data.Unit
	open import Function

AndrasKovacs / BoundDependentLC.hs

Last active November 29, 2020 05:36

Minimal (Type : Type) dependent LC with the Bound library

	{-# LANGUAGE LambdaCase, DeriveFunctor #-}

	import Prelude hiding (pi)
	import Control.Applicative
	import Control.Monad
	import Prelude.Extras
	import Bound

	data Term a
	= Var a

AndrasKovacs / Inject1.hs

Last active August 29, 2015 14:20

Unabiguously injecting functors with an inner type index into open sums.

	{-# LANGUAGE
	DataKinds, PolyKinds, TypeFamilies, MultiParamTypeClasses,
	RankNTypes, FlexibleInstances, UndecidableInstances,
	TypeOperators, ConstraintKinds, FlexibleContexts,
	DeriveFunctor, ScopedTypeVariables #-}

	import Data.Proxy
	import Control.Monad.Free

	data Pos = Here \| GoLeft Pos \| GoRight Pos

AndrasKovacs / ZipFolds.agda

Created April 30, 2015 16:46

Zipping with foldr in linear time.

	open import Data.Nat
	open import Data.List hiding (foldr)
	open import Function
	open import Data.Empty
	open import Relation.Binary.PropositionalEquality
	open import Data.Product

	foldr :
	{A : Set}
	(B : List A → Set)

AndrasKovacs / lzw.hs

Created March 14, 2015 17:55

LZW

	import Data.Maybe
	import Data.Char
	import Data.List

	dictionary :: [String]
	dictionary = [[chr x] \| x <- [0..127]]

	encode :: String -> [Int]
	encode [] = []
	encode (x:xs) = go dictionary [x] xs where

AndrasKovacs / GameSearch.hs

Created March 5, 2015 14:15

game tree search notes

	{-# LANGUAGE
	LambdaCase, NoMonomorphismRestriction,
	RankNTypes, ScopedTypeVariables,
	TupleSections, GADTs, FlexibleContexts,
	ViewPatterns, GeneralizedNewtypeDeriving #-}

	import Data.List
	import Data.List.Split
	import Data.Ord
	import Control.Lens

AndrasKovacs / PredSystemF.agda

Last active June 16, 2017 08:36

Another shot at System F with predicative instantiation. This time it's over a small closed universe and it's vastly simpler to implement. Inspired by Conor McBride's "Outrageous but Meaningful Coincidences".


	open import Function
	open import Data.Nat
	open import Data.Fin
	open import Data.Empty
	open import Data.Unit
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary
	open import Data.Product
	open import Data.Vec hiding (_∈_; module _∈_)

András Kovács AndrasKovacs