Rotsor

{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
import Data.List
import Control.Monad
import Data.Function
import Numeric 

formatFloatN floatNum numOfDecimals = showFFloat (Just numOfDecimals) floatNum ""

space = 10

Rotsor

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

Rotsor

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

Rotsor

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

Rotsor

-- 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

-----------------------------------------

Rotsor

-- 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)