AndrasKovacs’s gists

AndrasKovacs / IxFix.hs

Last active December 2, 2022 06:15

Example for recursion schemes for mutually recursive data

	{-# LANGUAGE
	UndecidableInstances, RankNTypes, TypeOperators, TypeFamilies,
	StandaloneDeriving, DataKinds, PolyKinds, DeriveFunctor, DeriveFoldable,
	DeriveTraversable, LambdaCase, PatternSynonyms, TemplateHaskell #-}

	import Control.Monad
	import Control.Applicative
	import Data.Singletons.TH

AndrasKovacs / FinSigma2.agda

Last active September 15, 2015 12:35

Alternative take on "finite sums of finite types are finite". This is much clearer and uses sensible lemmas (although it's not more succinct).


	open import Data.List renaming (map to lmap) hiding ([_])
	open import Relation.Binary.PropositionalEquality hiding ([_])
	open import Relation.Nullary
	open import Data.Empty
	open import Data.Product renaming (map to pmap)
	open import Data.Unit hiding (_≤_)
	open import Function
	open import Level renaming (suc to lsuc; zero to lzero)
	open import Data.Sum renaming (map to smap)

AndrasKovacs / Fin-neq-Nat.agda

Last active September 13, 2015 19:59

Nat is not equal to "Fin n" for any n.

	open import Data.Fin hiding (_<_; _≤_)
	open import Data.Nat
	open import Function
	open import Data.Product renaming (map to pmap)
	open import Data.List renaming (map to lmap)
	open import Relation.Binary.PropositionalEquality
	open import Data.Empty
	open import Relation.Nullary
	open import Relation.Binary
	open import Data.Sum renaming (map to smap)

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)

András Kovács AndrasKovacs