Skip to content

Instantly share code, notes, and snippets.

@Rotsor
Rotsor / strange-monad.agda
Created July 9, 2019 22:36
A weird tree monad proposed on reddit
-- a proof of monad laws for a strange monad defined in:
-- https://www.reddit.com/r/haskell/comments/cb1j40/is_there_a_valid_monad_instance_for_binary_trees/etcqsts/
data TREE (a : Set) : Set where
Leaf : a → TREE a
Tree : a → TREE a → TREE a → TREE a
distribute : ∀ {a} → (TREE a) -> (TREE a) -> (TREE a) -> TREE a
distribute l r (Leaf a) = Tree a l r
distribute l r (Tree a cl cr) = Tree a (distribute l r cl) (distribute l r cr)
@Rotsor
Rotsor / fulcrum.lean
Last active May 15, 2018 20:04
Fulcrum in lean
-- Solution for the "Fulcrum" problem from "The Great Theorem Prover Showdown"
-- (https://www.hillelwayne.com/post/theorem-prover-showdown/)
--
-- I am novice with Lean so the verbosity is almost certainly my
-- fault and not that of Lean.
import system.io
universes u v w
-----------------------------------------
module problem3 where
-- see:
-- https://www.reddit.com/r/DailyProver/comments/6d4oct/finite_cancellative_semigroups/
-- https://coq-math-problems.github.io/Problem3/
open import Relation.Binary.PropositionalEquality
open import Data.Product
Injective : {A B : Set} → (f : A → B) → Set
module problem2 where
-- see https://np.reddit.com/r/DailyProver/comments/6brksy/infinite_valleys_and_the_limited_principle_of/
open import Data.Nat as Nat
import Data.Nat.Properties as NatProp
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
module problem1 where
-- solution to https://coq-math-problems.github.io/Problem1/
--
-- sadly mine is the longest one
-- see https://www.reddit.com/r/Coq/comments/6amhkb/starting_a_problemoftheweek_blog_for_coq/
open import Data.Nat
import Data.Nat.Properties as NatProp
open import Data.Sum
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
import Data.List
import Control.Monad
import Data.Function
import Numeric
formatFloatN floatNum numOfDecimals = showFFloat (Just numOfDecimals) floatNum ""
space = 10