GallagherCommaJack

au FileType haskell nmap <F5> :!runhaskell %<cr>
au FileType haskell nmap <F6> :!ghci %<cr>
au FileType haskell nmap <F7> :!ghc --make %<cr>

GallagherCommaJack

data MIU = M | I | U deriving (Show, Read, Eq)
type STR = [MIU]

rep2 = concat . (replicate 2)

start = [M,I]

r1 :: STR -> STR
r1 ms = ms ++ [U]

GallagherCommaJack

import System.Cmd (system)
import System.Environment (getArgs)
import System.FilePath (takeExtension)
import Control.Exception (IOException, bracket, handle)
import System.IO (IOMode(..), hClose, hFileSize, openFile)
import GHC.IO.Exception (ExitCode(..))

gccCom :: String -> [String] -> IO ExitCode
gccCom filepath args = system $ "gcc " ++ filepath ++ unwords args

GallagherCommaJack

--Helper and Main
isPalindrome :: Eq a => [a] -> Bool
isPalindrome xs = reverse xs == xs

main = print num4 >> print num4'

--Naive Solution (still finishes in .122 seconds with -O2)
threeDigNums :: [Int]
threeDigNums = [1000,999..100]

GallagherCommaJack

This is a hybrid markdown and Literate Haskell document.  It's a blog post that I converted to pure html and posted <a href="http://blog.gallabytes.com/2014/03/isomorphism-equality-pq-and-other-ways.html">here</a>

So we'll first take as an axiom that math is based on axioms.  So far so good?
Well, an important thing to note with this is that it's really easy for axioms to have different significance - it all comes down to what metaphor you use in your brain to describe the axiomset

For example, <a href="http://blog.gallabytes.com/2014/03/miu-haskellized.html">MIU</a> seems wholly abstract, but it turned out to be isomorphic to some operations on the integers modulo 3.  And that isomorphism allowed some things to be made clear about it that weren't otherwise.

In Chapter 2, Hofstadter defines some axioms that he calls the "PQ system".  These axioms are:
<ol>
<li> The only valid characters are -, P, and Q</li>

GallagherCommaJack

#!/bin/zsh
# This is a script to take literate haskell code with markdown syntax throughout and turn it into pure HTML
# Just put it in your path and run blcm
hscolour -html -lit $1 > "$2" # colorizes the document, -html specifies the format, -lit says this is literate code
if [ "$3" = "-s" ] # Same as the -s argument to pandoc
then
    pandoc -f markdown -t html "$2" > "$2.html" -Ss # Pandoc is a wonderful thing
else
    pandoc -f markdown -t html "$2" > "$2.html" -S
fi

GallagherCommaJack

module Lob where

open import Data.Product
open import Function

_←→_ : Set → Set → Set
A ←→ B = (A → B) × (B → A)

postulate -- provability axioms
  □ : Set → Set

GallagherCommaJack

has_type(G,abs(V,E),arr(T1,T2)) :- has_type([[V,T1]|G],E,T2).
has_type(G,let(I,V,E),T2) :- has_type(G,V,T1), has_type([[I,T1]|G],E,T2).
has_type(G,app(E1,E2),T2) :- has_type(G,E1,arr(T1,T2)), has_type(G,E2,T1).
has_type(G,if(C,V1,V2),T) :- has_type(C,bool), has_type(G,V1,T), has_type(G,V2,T).
has_type(G,I,T) :- atom(I), append(_,[[I,T]|_],G).
has_type([],X,bool) :- X = true ; X = false.
has_type(Tm,Ty) :- has_type([],Tm,Ty).

subst(I,V,I,V).
subst(I,V,app(T1,T2),app(T12,T22)) :- subst(I,V,T1,T12), subst(I,V,T2,T22).

GallagherCommaJack

Theorem contr_pos_eq_classic :
  (forall P Q, (~ Q -> ~ P) -> P -> Q) ->
  forall P, ~~ P -> P.
Proof. intros H P nnP. apply H with (Q := P) in nnP; intuition. Qed.

GallagherCommaJack

Ltac eq_ids :=
  repeat progress match goal with
                      [i1 : id, i2 : id |- _] => extend (eq_id_dec i1 i2)
                  end.

Lemma subst_aexp_equiv : forall i a1 a2 st,
      aeval st (subst_aexp i a2 a1) = aeval (update st i (aeval st a2)) a1.
Proof. induction a1; simpl; auto; unfold update; eq_ids; crush. Qed.

Hint Rewrite aeval_weakening subst_aexp_equiv.