Muad`Dib

Some sums

2010-03-29T10:36:00.000-07:00

1 − 1 + 1 − 1 + ... = 1/2

1 + 1 + 1 + 1 + ... = -1/2

1 + 2 + 3 + 4 + ... = -1/12

1 + 2 + 4 + 8 + ... = -1

1 − 2 + 4 − 8 + ... = 1/3

1 * 2 * 3 * 4 * ... = sqrt(2*pi)

2 * 3 * 5 * 7 * ... = 4*pi^2

Why is the derivative of a type a zipper

2010-03-16T12:52:00.000-07:00

Why is the derivative of a regular type its type of one-hole contexts?

Let us define a function that counts the elements of a type, |()| = 1, |Void| = 0, |Either x y| = |x|+|y|, |(x,y)|=|x|*|y|, |List A| = 0 + |A| + |A|^2 + |A|^3 + ... (because lists can be [], [a], [a,b], and so on)

In general the 'size' of any type can be written as a power series (like an infinite polynomial), now for the type |k|*|x|^3, if we punch a hole in it, we get |k|*|x|^2 but we could have picked one of 3 different places to put it so we need to say which one, this gives 3*|k|*|x|^2, and this should be done to every term of a power series.

Since the derivative of a type = the derivative of its powerseries* this explains why we can 'differentiate' a type and get a zipper. (At least it sort of makes sense).

(* why is this true?)

Algebra System

2010-03-07T16:33:00.000-08:00

I have made a start on this already, al-jabr. Really what I am doing here is just getting my toes wet - What I want to do is:

Algebra hierarchy -- build up monoids, groups, fields etc and develop the basic theory of these structures also give concrete implementations of things like integers, reals (isomorphisms with efficient representations would be nice too!)

Algebraic algorithms -- produce algorithms that can be used to help me do mathematics (e.g. factoring, transformations, solving classes of equations)

Wiki -- Dependently typed programming in the large has already been done, they came up with FTA and FTC -- this is a constructive proof that it works!

There are some projects already working on this kind of thing, http://c-corn.cs.ru.nl/, http://github.com/Eelis/new-alg-hierarchy, http://www.lix.polytechnique.fr/coq/contribs/Algebra.html, http://hlombardi.free.fr/liens/constr.html, http://www.lix.polytechnique.fr/~assia/rech-eng.html, help make this list bigger!.

Ignoring these would be so dammed stupid I am not even going to think about it, but I want to point out that unless we make the most use of these projects as is possible then anything we create will be an anti-social library that nobody can use except me -- that is not desirable.

I think the only way to get this done is by collaborating with other people in a formally checked wiki (http://www.vdash.org/, http://code.google.com/p/hol-online/, http://prover.cs.ru.nl/login.php, http://www.cs.ru.nl/~herman/afstud.html, more?). These projects are all 'beta' that don't let everyone get involved so that's not very useful. Lets write it in Ur perhaps, using Coq as a subprocess. The directory structure of the Coq libraries would reflect that of the wiki. Edits will be accepted if they are checked and correct. I think once you have a spinal chord implemented, people will be able to add on parts quite easily.

I see no reason why someone with a bit of time wouldn't pick up Disquisitiones Arithmeticae or whatever and fold it into the wiki. With a bit of work getting everything set up correctly I think we could make a useful (basic) algebra system.

LU Decomposition in Prolog

2010-02-08T09:04:00.000-08:00

:- use_module(library(clpr)).

// various obvious bits of matrix machinary.

lu_decompose(M, L*U) :-
dimensions(M,N*N),
dimensions(L,N*N),
dimensions(U,N*N),
lower(L),
upper(U),
matrix_multiply(L,U,M).

ZFC's probably inconsistent

2009-12-24T16:47:00.000-08:00

Now stop worrying and enjoy your life.

Nice books

2009-11-29T18:44:00.000-08:00

Cantors Diagonalization Proof in Coq

2009-10-27T11:42:00.000-07:00


Axiom b : (nat -> nat) -> nat.
Axiom b' : nat -> (nat -> nat).

Axiom bijection : forall f, b' (b f) = f.
Axiom bijection' : forall x, b (b' x) = x.

Definition Stream A := nat -> A.
Definition Map {A B} (f : A -> B) : Stream A -> Stream B :=
  fun sa =>
    fun i =>
      f (sa i).

Definition l : Stream (nat -> nat) -> Stream nat :=
  Map b.
Definition l' : Stream nat -> Stream (nat -> nat) :=
  Map b'.

Definition isnt x :=
  match x with
    | O => S O
    | S _ => O
  end.

Theorem isn't_isnt {x} : isnt x <> x.
  destruct x; discriminate.
Qed.

Definition Diagonal {A} (s : Stream (Stream A)) : Stream A:=
  fun i => s i i.

Definition Diagonalization (sequences : Stream (nat -> nat)) : Stream nat :=
  Map isnt (Diagonal sequences).

Theorem isn't_in {sequences} : forall i, Diagonalization sequences <> sequences i.
intros; intro.
pose (f_equal (fun f => f i) H) as H'.
unfold Diagonalization in H'.
unfold Diagonal in H'.
unfold Map in H'.
revert H'.
apply isn't_isnt.
Qed.

Definition pink_elephant : Stream nat := fun i => i.

Definition sequence_enumeration : Stream (nat -> nat) := l' pink_elephant.

Theorem every_sequence : forall s, exists i, s = sequence_enumeration i.
intro s; exists (b s).
unfold sequence_enumeration.
unfold pink_elephant.
unfold l'.
unfold Map.
rewrite bijection.
reflexivity.
Qed.

Theorem Cantor : False.
destruct (every_sequence (Diagonalization sequence_enumeration)) as [i iPrf].
pose (@isn't_in sequence_enumeration i).
contradiction.
Qed.

Short Note on Semantics

2009-10-24T19:04:00.000-07:00

With all curious derivations that come from the forests of To Mock a Mockingbird, and in the intrests of deepening understanding of type theory (in particular CIC) we considered axiomatizing the SK calculus in Coq.

Module Type SK.
  (* axiomatization of the theory *)
  Parameter SK : Set.

  Parameter app : SK -> SK -> SK.
  Infix "*" := app.
  
  Parameter S : SK.
  Parameter K : SK.
  
  Axiom S_prop : forall a b c, S * a * b * c = (a * c) * (b * c).
  Axiom K_prop : forall a b, K * a * b = a.
End SK.

It is not defined as an inductive type (as you might usually do) because there is no normal form for SK that we can compute terms into inside Coq (we would have to equate diverging terms with an "omega" symbol for a start, which is well known to be a partial operation). It would be possible to use a non-normal forma and quotient it out with a special (undecidable) equivalence relation, but we do not this.. Instead the axioms of the theory are given, One immediately notices that there is a trivial model of these axioms:

Module SK_trivial_model : SK.
  (* one model (giving non-contradiction of the theory) *)
  Definition SK := unit.
  
  Definition app := fun (_ _ : unit) => tt.
  Infix "*" := app.
  
  Definition S := tt.
  Definition K := tt.
  
  Theorem S_prop : forall a b c, S * a * b * c = (a * c) * (b * c).
    reflexivity.
  Qed.
  
  Theorem K_prop : forall a b, K * a * b = a.
    destruct a; reflexivity.
  Qed.
End SK_trivial_model.

(This implementation mostly serves to show the syntax and so on of how to construct a model of a theory inside Coq).

Anyway, we eliminate trivial models by saying that S <> K.

  Axiom SK_prop : S <> K.

We could now develop the theory of combinator calculus, prove things like S <> I and so forth.

Module SK_theory <: SK.
  Include Type SK.
  
  (* Development of the theory of SK calculus, valid for all models *)
  
  Ltac sk := repeat (rewrite S_prop || rewrite K_prop).
  
  Definition I := S * K * S.
  Theorem I_prop : forall x, I * x = x.
    intros; unfold I; sk; reflexivity.
  Qed.
  Ltac ski := repeat (sk || rewrite I_prop).
  
  Theorem IK : I <> K.
    Definition F x y b := b * K * I * x * y.
    
    intro Eq; generalize (f_equal (F K S) Eq); unfold F; ski.
    apply SK_prop.
  Qed.
  
  Definition U := S * I * I.
  Theorem U_prop : forall x, U * x = x * x.
    intros; unfold U; ski; reflexivity.
  Qed.
  
  Ltac skiu := repeat (ski; rewrite U_prop).
End SK_theory.

As fun as that would be, I don't believe you could ever reach a contradiction by assuming the SK theory. Yet no model exists inside Coq!

This is a rather confusing and troubling state, but Russell O'Connor mentioned to me the possibility of giving an interpretation of CIC into a theory that has a Halting-Oracle and that solves it! This is surely a valid interpretation of CIC, it's just got this SK theory added in with the usual stuff - the halting oracle would be used to normalize SK terms and prove satisfy our theory. So despite the non-existence of a model of SK inside Coq: It appears we can reason about the SK calculus directly. (Rather than a halting oracle you might have considered a special equivalence relation being interpreted for the congruence of SK objects but lets pretend Coq has Axiom K so that need not be considered).

This is all very interesting to me because it seems to suggest mathematics existing outside of the formal theory we work in or study. Something I never believed in - It's not completely clear if this is profound or if I am just going soft.

Do you live in UK?

2009-08-25T13:07:00.000-07:00

http://www.pirateparty.org.uk/

Strongly Specified Parser Combinators

2009-04-26T10:11:00.000-07:00

Following the approach Wouter Swierstra used for Hoare State Monad, we define a Parser monad with pre and post conditions that express soundness (but not completeness) of the parser.

The computational aspect of it is the same old parser monad, type Parser s a = [s] -> [(s, [a])], which takes a list of tokens [s] to a (possibly empty) list (here is where backtracking/nondeterminism comes into it) of parses paired with the rest of the text. It's a monad and also a monad plus.

On the specification end, we can put a precondition on the input string (for example, you might say the input length is <= some value, for ensuring termination of a recursive parser) and also a post condition comparing the input with the parsed value and the remaining output.


  Definition Pre := list s -> Prop.
  Definition Post (t : Set) := list s -> t -> list s -> Prop.
  
  Program Definition Parser (pre : Pre) (t : Set) (post : Post t) : Set :=
      forall i : { t : list s | pre t }, list ({ (x, r) : t * list s | post i x r }).

in Haskell we might define:

m >>= f = \i -> concatMap (uncurry f) (m i)

And in Coq, using Program we have roughly the same thing. Except that one has to apply a 'noncomputational_map' to fudge the proofs paired up with the list elements.


  Program Definition Bind (a b : Set) P1 P2 Q1 Q2
    (m : Parser P1 a Q1)
    (f : (forall x : a, Parser (P2 x) b (Q2 x))) :
    Parser (fun i => P1 i /\ forall x o, Q1 i x o -> P2 x o)
           b
           (fun i x' o' => exists x o, Q1 i x o /\ Q2 x o x' o') :=
    fun i => @flat_map ({ (x, o) : a * list s | Q1 i x o }) _
      (fun xo => match xo with (x,o) => noncomputational_map _ _ _ _ (f x o) end)
      (m i).

Seeing as noncomputational map doesn't do anything, we prove a theorem expressing that as justification for extracting it out as the identity function (rather it being equivalent to map id traversing the whole list).


  Theorem noncomputational_map_identity :
    forall l,
      map (@proj1_sig _ _) l = map (@proj1_sig _ _) (noncomputational_map l).
  
  Extract Inlined Constant noncomputational_map => "id".

Another nice parser combinator is the fixed point of a parser:


  Program Definition Fix t {P Q} :
    (forall i : { t : list s | P t },
      Parser (fun i' => length i' < length i /\ P i') t Q ->
      list ({ (x, o) : t * list s | Q i x o })) ->
    Parser P t Q :=
    fun Rec =>
      well_founded_induction
        (well_founded_ltof ({ i : list s | P i }) (fun i => length i))
        (fun i => list ({ (x, o) : t * list s | Q i x o }))
        (fun x Rec' => Rec x (fun i => Rec' i _)).

It packages up well founded recursion on the size of the input string, so that any non-left recursive parsers should be easily defined.

Enough of the heavy machinary! A simple example of putting thing into work now:

 <par> ::= <epsilon> | '(' <par> ')' <par>

To parse this we define a type of tokens and abstract syntax of parsing derivations - then relate them with a function:


  Inductive token := open | close.
  Inductive par := epsilon : par | wrappend : par -> par -> par.

  Fixpoint print (p : par) : list token :=
    match p with
      | epsilon => nil
      | wrappend m n => (open::nil) ++ print m ++ (close::nil) ++ print n
    end.

Now Program lets us define the par parser as the fixed point of the sum of epsilon and wrapped recursions:


  Program Definition par_parser : Parser token (fun _ => True) par (fun x p y => x = print p ++ y /\ length y <= length x) :=
    Fix token par (fun i parRec =>
      Plus _ _ (fun i' => i = i') _
        (fudge_pre_and_post_conditions _ _ _
          (Return epsilon))
        (fudge_pre_and_post_conditions _ _ _
          (Symbol token eq_token_dec open >>= fun _ =>
           parRec >>= fun m =>
           Symbol token eq_token_dec close >>= fun _ =>
           parRec >>= fun n =>
           Return (wrappend m n)))
      i).

Here are the actual scripts http://github.com/odge/parseq/tree/master

Type Checker

2009-03-27T06:23:00.000-07:00

prototype


import Control.Monad
import Control.Monad.Error
import Control.Monad.Identity
import Data.Maybe
import Data.Char
import Text.ParserCombinators.ReadP

-- Proof irrelevance is implemented by:
--
--   erase(Gamma) |- phi : P
--   ----------------------- Prf
--   Gamma |- []phi : Prf(P)
--
--   []phi =def []psi : Prf(_)
--
-- Allow eliminations like P(x) -> Prf(x = y) -> P(y)
-- along the same schema as Coqs Prop sort, this gives us Axiom K.

-- * I am not a number: I am a free variable
-- * Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory
-- * Intensionality, extensionality, and proof irrelevance in modal type theory

-- Syntax

type Ref = Int
newtype Scope a = Scope a
 deriving Show

data Name
 = Local Ref
 | Global String
   deriving (Eq, Show)

data T
 = Type
 | Pi T (Scope T)
 | Prf T
 | Lam T (Scope T)
 | Square T
 | App T T
 | Def String
 | Bound Ref
 | Free Name
   deriving Show

abstract x expr = Scope (rip 0 expr) where
 rip i Type = Type
 rip i (Pi tau (Scope sigma)) = Pi (rip i tau) (Scope (rip (i+1) sigma))
 rip i (Prf p) = Prf (rip i p)
 rip i (Lam tau (Scope sigma)) = Lam (rip i tau) (Scope (rip (i+1) sigma))
 rip i (Square s) = Square (rip i s)
 rip i (App m n) = App (rip i m) (rip i n)
 rip i (Def d) = Def d
 rip i (Bound j) = Bound j
 rip i (Free j)
  | x == j = Bound i
  | otherwise = Free j

instantiate y (Scope expr) = shove 0 expr where
 shove i Type = Type
 shove i (Pi tau (Scope sigma)) = Pi (shove i tau) (Scope (shove (i+1) sigma))
 shove i (Prf p) = Prf (shove i p)
 shove i (Lam tau (Scope sigma)) = Lam (shove i tau) (Scope (shove (i+1) sigma))
 shove i (Square s) = Square (shove i s)
 shove i (App m n) = App (shove i m) (shove i n)
 shove i (Def d) = Def d
 shove i (Bound j)
  | i == j = y
  | otherwise = Bound j
 shove i (Free j) = Free j

-- Parsing

-- *
-- /\(x:T),x
-- Prf(P)
-- \(x:T),x
-- []P
-- T T
-- x

parseTerm = readP_to_S pTerm

pTerm = pPi +++ pLam +++
 do a <- skipSpaces >> pSimpleUnit ; as <- many (skipSpaces >> pUnit) ; skipSpaces ; return (foldl1 App (a:as))
pUnit = pType +++ pPi +++ pPrf +++ pLam +++ pSquare +++ pFree +++ parens pTerm
pSimpleUnit = pType +++ pPrf +++ pSquare +++ pFree +++ parens pTerm

pType = do string "*" ; return Type
pPi = do string "/\\" ; (x, t) <- binder ; string "," ; b <- pTerm ; return (Pi t (abstract x b))
pPrf = do string "Prf" ; m <- parens pTerm ; return (Prf m)
pLam = do string "\\" ; (x, t) <- binder ; string "," ; b <- pTerm ; return (Lam t (abstract x b))
pSquare = do string "[]" ; m <- pTerm ; return (Square m)
pFree = do a <- name ; guard (a /= "Prf") ; return (Free (Global a))

name = munch1 isAlpha
binder = b +++ parens b where
 b = do a <- name ; string ":" ; x <- pTerm ; return (Global a,x)
parens p = do string "(" ; r <- p ; string ")" ; return r

-- bug 1:       (\x:*,\y:*,x y)
--   parses as: (\x:*,(\y:*,(x y)))
--          or: (\x:*,(\y:*,x) y)
--          or: ((\x:*,\y:*,x) y)
-- fix: introduced 'simple' units and changed pTerm
--      from being applications of [unit unit ...] to [simpleUnit unit ...]

-- Typing

data V
 = VType
 | VPi V (V -> V)
 | VPrf V
 | VLam (V -> V)
 | VSquare V
 | VNeutral N
data N
 = NApp N V
 | NFree Name

VLam f % x = f x
VNeutral n % x = VNeutral (NApp n x)
_ % _ = error "Malformed application"

eval delta xi Type = VType
eval delta xi (Pi tau (Scope sigma)) = VPi (eval delta xi tau) (\x -> eval (x:delta) xi sigma)
eval delta xi (Prf p) = VPrf (eval delta xi p)
eval delta xi (Lam _ (Scope f)) = VLam (\x -> eval (x:delta) xi f)
eval delta xi (Square s) = VSquare (eval delta xi s)
eval delta xi (App m n) = eval delta xi m % eval delta xi n
eval delta xi (Def d) = fromJust (lookup d xi)
eval delta xi (Bound i) = delta !! i
eval delta xi (Free j) = VNeutral (NFree j)

quote q VType = Type
quote q (VPi tau sigmaF) = Pi (quote q tau) (abstract (Local q) (quote (q+1) (sigmaF (VNeutral (NFree (Local q))))))
quote q (VPrf p) = Prf (quote q p)
quote q (VLam f) = Lam Type (abstract (Local q) (quote (q+1) (f (VNeutral (NFree (Local q))))))
quote q (VSquare s) = Square (quote q s)
quote q (VNeutral n) = nquote q n
nquote q (NApp n v) = App (nquote q n) (quote q v)
nquote q (NFree j) = Free j

abstractV i VType _ = VType
abstractV i (VPi tau sigmaF) o = VPi (abstractV i tau o) (\e -> abstractV i (sigmaF e) o)
abstractV i (VPrf p) x = VPrf (abstractV i p x)
abstractV i (VLam sigmaF) o = VLam (\e -> abstractV i (sigmaF e) o)
abstractV i (VSquare s) x = VSquare (abstractV i s x)
abstractV i (VNeutral n) x = abstractN i n x
abstractN i (NApp n m) x = abstractN i n x % abstractV i m x
abstractN i (NFree j) x
 | i == j = x
 | otherwise = VNeutral (NFree j)

type Infer = ErrorT String Identity
runInfer :: Infer o -> Either String o
runInfer m = runIdentity (runErrorT m)

conv q gamma VType VType = True
conv q gamma (VPi tau sigmaF) (VPi tau' sigmaF') =
 conv q gamma tau tau' && conv (q+1) ((Local q, tau):gamma) (sigmaF x) (sigmaF' x) where
  x = VNeutral (NFree (Local q))
conv q gamma (VPrf p) (VPrf p') = conv q gamma p p'
conv q gamma (VNeutral n) (VNeutral m) = maybe False (const True) (convN q gamma n m)
conv q gamma _ _ = False
convV q gamma f g (VPi tau sigmaF) = convV (q+1) ((Local q, tau):gamma) (f % x) (g % x) (sigmaF x)
 where x = VNeutral (NFree (Local q))
convV q gamma _ _ (VPrf _) = True
convV q gamma (VNeutral n) (VNeutral m) _ = maybe False (const True) (convN q gamma n m)
convV q gamma t s VType = conv q gamma t s
convN q gamma (NFree i) (NFree j)
 | i == j = lookup i gamma
convN q gamma (NApp f x) (NApp g y) = do
 VPi tau sigmaF <- convN q gamma f g
 case convV q gamma x y tau of
  True -> Just (sigmaF x)
  False -> Nothing
convN q gamma n m = do
 case (convN q gamma n n, convN q gamma m m) of
  (Just (VPrf p), Just (VPrf p')) | conv q gamma (VPrf p) (VPrf p') -> Just (VPrf p)
  _ -> Nothing

erase = map (\(q,tau) -> (q,eraseV tau))
eraseV (VPrf p) = eraseV p
eraseV sigma = sigma

infer :: Ref -> [(Name, V)] -> [(String, V)] -> T -> Infer V
infer q gamma xi Type = return VType
infer q gamma xi (Pi tau scopeSigma) = do
 VType <- infer q gamma xi tau
 VType <- infer (q+1) ((Local q, VType):gamma) xi (instantiate (Free (Local q)) scopeSigma)
 return VType
infer q gamma xi (Prf p) = do
 VType <- infer q gamma xi p
 return VType
infer q gamma xi (Lam tau scopeM) = do
 VType <- infer q gamma xi tau
 tau' <- return $ eval [] xi tau
 sigmaF <- infer (q+1) ((Local q, tau'):gamma) xi (instantiate (Free (Local q)) scopeM)
 pi <- return $ VPi tau' (abstractV (Local q) sigmaF)
 return pi
infer q gamma xi (Square s) = do
 p <- infer q (erase gamma) xi s -- How do local definitions relate to erasure?
 return (VPrf p)
infer q gamma xi (App m n) = do
 pi <- infer q gamma xi m
 case pi of
  VPi sigma tauF -> do
   sigma' <- infer q gamma xi n
   case conv q gamma sigma sigma' of
    True -> return (tauF (eval [] xi n))
    False -> throwError (unlines [ "Type error in application: "
                                 , " expected: " ++ show (quote q sigma)
                                 , " received: " ++ show (quote q sigma')
                                 ])
  _ -> throwError "Nonfunctional application"
infer q gamma xi (Def d) = do
 infer q gamma xi (Free (Global d))
infer q gamma xi (Bound _) = do
 throwError "Encountered a bound variable"
infer q gamma xi (Free j) = do
 case lookup j gamma of
  Just tau -> return tau
  Nothing -> case j of
   Local _ -> throwError "Free local variable"
   Global j -> throwError ("Free global variable: " ++ j)

inferType gamma xi t = case runInfer (infer q gamma xi t) of
  Left err -> Left err
  Right tau -> Right (quote q tau)
 where q = length gamma + 1

checkType gamma xi t tau = case runInfer (infer q gamma xi t) of
  Left err -> Left err
  Right tau' -> Right (conv q gamma tau tau')
 where q = length gamma + 1

unstickDefinitions xi Type = Type
unstickDefinitions xi (Pi t (Scope b)) = Pi (unstickDefinitions xi t) (Scope (unstickDefinitions xi b))
unstickDefinitions xi (Prf p) = Prf (unstickDefinitions xi p)
unstickDefinitions xi (Lam t (Scope b)) = Lam (unstickDefinitions xi t) (Scope (unstickDefinitions xi b))
unstickDefinitions xi (Square p) = Square (unstickDefinitions xi p)
unstickDefinitions xi (App m n) = App (unstickDefinitions xi m) (unstickDefinitions xi n)
unstickDefinitions xi (Def d) = Def d
unstickDefinitions xi (Bound j) = Bound j
unstickDefinitions xi (Free (Local j)) = Free (Local j)
unstickDefinitions xi (Free (Global g)) =
 case lookup g xi of 
  Nothing -> Free (Global g)
  Just _ -> Def g
-- TODO: that was silly, find a sensible fold for T

-- User interfacing

repl gamma xi = do
 putStr "> "
 line <- getLine
 case parseTerm line of
  [] -> putStrLn "No parse"
  [(t,"")] -> case inferType gamma xi (unstickDefinitions xi t) of
                Left err -> putStrLn err
                Right ty -> print ty
  [(_,stuff)] -> putStrLn ("extra stuff at end of line: " ++ stuff)
  ambiguous -> putStrLn ("ambiguous parse: " ++ show (length ambiguous) ++ " alternatives")
 repl gamma xi

-- Examples/Toys

-- nat : *; Z : nat; S : nat -> nat
nat =
 [ (Global "nat", VType)
 , (Global "Z", zType)
 , (Global "S", sType)
 , (Global "natElim", natElimType)
 ]
natDefs =
 [ ("natElim", natElimV)
 ]
zType = VNeutral (NFree (Global "nat"))
sType = VPi (VNeutral (NFree (Global "nat"))) (\_ -> VNeutral (NFree (Global "nat")))
natElimType = VPi (VPi (VNeutral (nfree "nat")) (\_ -> VType)) (\p ->               -- forall P : nat -> Type,
               VPi (p % (VNeutral (nfree "Z"))) (\_ ->                               -- P 0 ->
                VPi (VPi (VNeutral (nfree "nat")) (\n ->                              -- (forall n : nat,
                         VPi (p % n) (\_ -> (p % (VNeutral (nfree "S") % n))))) (\_ -> -- P n -> P (S n)) ->
                 VPi (VNeutral (nfree "nat")) (\n -> p % n))))                          -- forall n : nat, P n
 where nfree = NFree . Global
natElimV = VLam (\motive -> VLam (\zero -> VLam (\succ -> VLam (\n -> natElim motive zero succ n))))
natElim motive zero succ (VNeutral (NFree (Global "Z"))) = zero
natElim motive zero succ (VNeutral (NApp (NFree (Global "S")) m)) = succ % m % natElim motive zero succ m
natElim motive zero succ stuck = VNeutral (NFree (Global "natElim")) % motive % zero % succ % stuck

-- add : Pi (Free (Global "nat")) (Scope (Pi (Free (Global "nat")) (Scope (Free (Global "nat")))))
--  := (\(x:nat),\(y:nat),natElim (\(n:nat),nat) x (\(T:nat),S) y)
add =
 [ (Global "add", addType)
 ]
addDefs =
 [ ("add", addValue)
 ]
addType = VPi (VNeutral (NFree (Global "nat"))) (\_ -> 
           VPi (VNeutral (NFree (Global "nat"))) (\_ -> 
            VNeutral (NFree (Global "nat"))))
addValue = VLam (\x -> VLam (\y ->
  natElimV % (VLam (\_ -> VNeutral (NFree (Global "nat")))) % y % (VLam (\_ -> VNeutral (NFree (Global "S")))) % x))

-- eq : /\T:*, T -> T -> *; refl : /\T:*,/\t:T, eq T t t
eq =
 [ (Global "eq", VPi VType (\t -> VPi t (\_ -> VPi t (\_ -> VType))))
 , (Global "refl", reflType)
 , (Global "eqElim", eqElimType)
 , (Global "eqPrfElim", eqPrfElimType) -- eq has only one constructor so allow Proof eliminations
 ]
eqDefs =
 [ ("eqElim", eqElimV)
 , ("eqPrfElim", eqElimV)
 ]
reflType = VPi VType (\t -> VPi t (\t' -> VNeutral (NFree (Global "eq")) % t % t' % t'))
eqElimType = VPi VType (\a -> VPi a (\x -> VPi (VPi a (\_ -> VType)) (\p -> -- forall (A : Type) (x : A) (P : A -> Type),
              VPi (p % x) (\_ -> VPi a (\y -> -- P x -> forall y : A,
               VPi (VNeutral (NFree (Global "eq")) % a % x % y) (\_ -> p % y)))))) -- x = y -> P y
eqPrfElimType = VPi VType (\a -> VPi a (\x -> VPi (VPi a (\_ -> VType)) (\p -> -- forall (A : Type) (x : A) (P : A -> Type),
                 VPi (p % x) (\_ -> VPi a (\y -> -- P x -> forall y : A,
                  VPi (VPrf (VNeutral (NFree (Global "eq")) % a % x % y)) (\_ -> p % y)))))) -- Prf(x = y) -> P y
eqElimV = VLam (\a -> VLam (\x -> VLam (\motive -> VLam (\pX -> VLam (\y -> VLam (\eqPrf -> eqElim pX eqPrf))))))
eqElim pX (VNeutral (NApp (NFree (Global "refl")) _)) = pX
eqElim _ _ = error "not implemented"

-- Example session:
--
-- Main> repl (nat ++ add ++ eq) (natDefs ++ addDefs ++ eqDefs)
--
-- -- join for the Prf monad:
--
-- > \P:*,\phi:Prf(Prf(P)),[]phi
-- Pi Type (Scope (Pi (Prf (Prf (Bound 0))) (Scope (Prf (Bound 1)))))
--
-- -- proof of eq symmetry:
--
-- > (\T:*,\a:T,\b:T,\e:eq T a b,eqElim T a (\x:T,eq T x a) (refl T a) b e)
-- Pi Type (Scope (Pi (Bound 0) (Scope (Pi (Bound 1) (Scope (Pi (App (App (App (Free (Global "eq")) (Bound 2)) (Bound 1)) (Bound 0)) (Scope (App (App (App (Free (Global "eq")) (Bound 3)) (Bound 1)) (Bound 2)))))))))
--
-- -- that is: /\T:*,/\a:T,/\b:T,/\(a = b),b = a
--
-- proof of f_equal, x = y -> f x = f y
--
-- > (\x:nat,\y:nat,\f:(/\n:nat,nat),\e:eq nat x y,eqElim nat x (\y:nat,eq nat (f x) (f y)) (refl nat (f x)) y e)
-- Pi (Free (Global "nat")) (Scope (
--  Pi (Free (Global "nat")) (Scope (
--   Pi (Pi (Free (Global "nat")) (Scope (Free (Global "nat")))) (Scope (
--    Pi (App (App (App (Free (Global "eq")) (Free (Global "nat"))) (Bound 2)) (Bound 1)) (Scope (
--     App (App (App (Free (Global "eq")) (Free (Global "nat"))) (App (Bound 1) (Bound 3))) (App (Bound 1) (Bound 2))))))))))
--
-- Induction proof that: n + 0 = n
--
-- > (natElim (\n:nat,eq nat (add n Z) n) (refl nat Z) (\n:nat,\e:eq nat (add n Z) n,(\x:nat,\y:nat,\f:(/\n:nat,nat),\e:eq nat x y,eqElim nat x (\y:nat,eq nat (f x) (f y)) (refl nat (f x)) y e) (add n Z) n S e))
-- Pi (Free (Global "nat")) (Scope (
--  App (App (App (Free (Global "eq")) (Free (Global "nat")))
--      (App (App (App (App (Free (Global "natElim"))
--        (Lam Type (Scope (Free (Global "nat")))))
--        (Free (Global "Z")))
--        (Lam Type (Scope (Free (Global "S")))))
--        (Bound 0)))
--      (Bound 0)))

How to halve a number

2009-03-01T05:00:00.000-08:00


(*
 * How to halve a number
 * ---------------------
 *)

(* (* just so we start on the same page, what is a number? *)
 *
 * Inductive nat : Set :=
 * | O : nat
 * | S : nat -> nat.
 *)

Module Type Halver.
  
  Parameter half : nat -> nat.
  
  Axiom e1 : half 0 = 0.
  Axiom e2 : half 1 = 0.
  Axiom e3 : forall n, half (S (S n)) = S (half n).

  (* An equational specification is given as a module
   * so now it is possible it give various implementations
   *)

End Halver.

Module By_Default : Halver.
  
  Fixpoint half (n : nat) : nat :=
    match n with
      | O => O
      | S O => O
      | S (S n) => S (half n)
    end.
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.

  (* This is the sort of thing one would normally start with,
   * pattern match on a term and use recursive calls on a
   * structurally smaller term, the idea of 'structurally smaller'
   * is part of the type rules actually and it is the transitive
   * closure of   (1) p_i < C p_1 p_2 ... p_n
   *        and   (2) f x < f
   * rule (1) and (2) say that a term in smaller than any
   * construction built from it, a construction being something
   * literally built from constructor or a function
   *)

End By_Default.

Module By_Divine_Inspiration : Halver.
  
  (* Definition half n :=
   *    fst (nat_rect (fun _ => (nat * nat)%type)
   *      (O, O)
   *      (fun n Pn => let (p,q) := Pn in (q, S p))
   *      n).
   * (* it seems impossible to prove this one correct *)
   *)
  
  Definition half n :=
    fst (nat_rect (fun _ => (nat * nat)%type)
      (O, O)
      (fun n Pn => (snd Pn, S (fst Pn)))
      n).
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.

End By_Divine_Inspiration.

Module By_Devising_Data : Halver.
  
  (* This way seems like a 'view' in the sense of Wadler,
   * The structure of the data make the program definition
   * straight-forward.
   *)
  
  Inductive nat' : Set :=
  | Zero : nat'
  | One : nat'
  | SuccSucc : nat' -> nat'.
  
  Definition zero := Zero.
  Fixpoint succ (n : nat') :=
    match n with
      | Zero => One
      | One => SuccSucc Zero
      | SuccSucc n => SuccSucc (succ n)
    end.
  
  Fixpoint nat_to_nat' (n : nat) : nat' :=
    match n with
      | O => zero
      | S n => succ (nat_to_nat' n)
    end.
  
  Fixpoint half' (n : nat') : nat :=
    match n with
      | Zero => O
      | One => O
      | SuccSucc n => S (half' n)
    end.
  
  Definition half n := half' (nat_to_nat' n).
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  
  Lemma succ_succs n : succ (succ n) = SuccSucc n.
    induction n; simpl; try reflexivity.
    rewrite IHn; reflexivity.
  Qed.
  
  Theorem e3 n : half (S (S n)) = S (half n).
    intro n.
    unfold half.
    simpl.
    rewrite succ_succs.
    reflexivity.
  Qed.

End By_Devising_Data.

Module By_Mutual_Induction : Halver.
  
  Inductive Even : nat -> Set :=
  | EvenO : Even O
  | EvenS n : Odd n -> Even (S n)
  with      Odd : nat -> Set :=
  | OddS n : Even n -> Odd (S n).
  
  Fixpoint even_or_odd n : Even n + Odd n :=
    match n as n return Even n + Odd n with
      | O => inl _ EvenO
      | S n =>
        match even_or_odd n with
          | inl even => inr _ (OddS _ even)
          | inr odd => inl _ (EvenS _ odd)
        end
    end.
  
  Fixpoint halfE n (e : Even n) : nat :=
    match e with
      | EvenO => O
      | EvenS n odd => S (halfO n odd)
    end
  with     halfO n (o : Odd n) : nat :=
    match o with
      | OddS n even => halfE n even
    end.
  
  Definition half (n : nat) : nat :=
    match even_or_odd n with
      | inl even => halfE n even
      | inr odd => halfO n odd
    end.
  
  (* Proving this program correct is quite a lot
   * of work compared to the previous implementations,
   * these tricky inversion lemmas which would be trivial
   * to prove using pattern matching at least show some
   * techniques.
   *)
  
  Lemma unique_lemma_1 (e : Even 0) : e = EvenO.
    intro e.
    refine (
      match e as e' in Even Zero return
        match Zero return Even Zero -> Prop with
          | O => fun e'' : Even 0 => e'' = EvenO
          | S _ => fun _ => True
        end e'
        with
        | EvenO => refl_equal _
        | EvenS _ _ => I
      end
    ).
  Qed.
  
  Lemma unique_lemma_2 n (e : Even (S n)) : { o' : _ | e = EvenS n o' }.
    intros n e.
    refine (
      match e as e' in Even SuccN return
        match SuccN return Even SuccN -> Set with
          | O => fun _ => True
          | S n => fun e' : Even (S n) =>
            { o' : _ | e' = EvenS n o' }
        end e'
        with
        | EvenO => I
        | EvenS n' o' => exist _ o' (refl_equal _)
      end
    ).
  Qed.
  
  Lemma unique_lemma_3 n (o : Odd (S n)) : { e' : _ | o = OddS n e' }.
    intros n o.
    refine (
      match o as o' in Odd SuccN return
        match SuccN return Odd SuccN -> Set with
          | O => fun _ => True
          | S n => fun o' : Odd (S n) =>
            { e' : _ | o' = OddS n e' }
        end o'
        with
        | OddS n' e' => exist _ e' (refl_equal _)
      end
    ).
  Qed.
  
  (* There is only one way to prove a number is Even
   * and similarly to prove it's Odd
   *)
  
  Theorem unique_classificationE n (e e' : Even n) : e = e'
  with    unique_classificationO n (o o' : Odd n) : o = o'.
    induction n; intros.
    
    rewrite unique_lemma_1 with e.
    rewrite unique_lemma_1 with e'.
    reflexivity.
    
    destruct (unique_lemma_2 _ e) as [o eq].
    destruct (unique_lemma_2 _ e') as [o' eq'].
    rewrite eq; rewrite eq'.
    rewrite (unique_classificationO n o o').
    reflexivity.
    
    destruct n.
    intro H; inversion H.
    intros.
    destruct (unique_lemma_3 _ o) as [e eq].
    destruct (unique_lemma_3 _ o') as [e' eq'].
    rewrite eq; rewrite eq'.
    rewrite (unique_classificationE n e e').
    reflexivity.
  Qed.
  
  Lemma halfE_SS n e e' : halfE (S (S n)) e' = S (halfE n e)
  with  halfO_SS n o o' : halfO (S (S n)) o' = S (halfO n o).
  intros.
  destruct (unique_lemma_2 _ e') as [o eq].
  destruct (unique_lemma_3 _ o) as [e'' eq'].
  subst.
  simpl.
  assert (e = e'') as E by apply unique_classificationE.
  rewrite E; reflexivity.
  
  intros.
  destruct (unique_lemma_3 _ o') as [e eq].
  destruct (unique_lemma_2 _ e) as [o'' eq'].
  subst.
  simpl.
  assert (o = o'') as O by apply unique_classificationO.
  rewrite O; reflexivity.
  Qed.
  
  Definition which P Q : P + Q -> bool :=
    fun choice =>
      match choice with
        | inl _ => true
        | inr _ => false
      end.
  Lemma even_or_odd_SS n : which _ _ (even_or_odd (S (S n))) = which _ _ (even_or_odd n).
    induction n.
    reflexivity.
    simpl in *.
    destruct (even_or_odd n).
    reflexivity.
    reflexivity.
  Qed.
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Theorem e3 n : half (S (S n)) = S (half n).
    intro n.
    unfold half.
    generalize (even_or_odd_SS n).
    destruct (even_or_odd n); destruct (even_or_odd (S (S n)));
      simpl; intro hyp; try discriminate hyp.
    apply halfE_SS.
    apply halfO_SS.
  Qed.

End By_Mutual_Induction.

Module By_Well_Founded_Induction : Halver.
  
  Section Well_Founded_Relations.
    
    Variable A : Type.
    Variable R : A -> A -> Prop.
    
    Inductive Acc (x : A) : Prop :=
    | below : (forall y : A, R y x -> Acc y) -> Acc x.
    
    (* x must be a parameter (instead of Acc : A -> Prop) for
     * Set/Type elimination, but why?
     *)
    
    Definition Well_Founded := forall x : A, Acc x.
    
    Inductive Transitive_Closure : A -> A -> Prop :=
    | step x y : R x y -> Transitive_Closure x y
    | transitivity x y z : R x y -> Transitive_Closure y z -> Transitive_Closure x z.
    
    Definition Well_Founded_Induction
      (W : Well_Founded)
      (P : A -> Type)
      (rec : forall x, (forall y, R y x -> P y) -> P x)
      : forall a, P a :=
        fun a => Acc_rect P (fun x _ hyp => rec x hyp) a (W a).
  
  End Well_Founded_Relations.
  
  Section Transitive_Relation.
    
    Variable A : Type.
    Variable R : A -> A -> Prop.
    
    Theorem Transitive_Closure_Well_Founded :
      Well_Founded A R -> Well_Founded A (Transitive_Closure A R).
    Proof.
      unfold Well_Founded; intros R_Acc x.
      
      induction (R_Acc x) as [x R_ind T_ind].
      
      apply below; intros y Trans.
      
      induction Trans.
      
      apply T_ind; assumption.
      
      pose (IHTrans R_ind T_ind) as IH; inversion IH as [H']; subst.
      apply H'.
      apply step.
      assumption.
    Defined.
  
  End Transitive_Relation.
  
  Section Nat_Structural_Measure.
    
    (* Looking at the definition of nat: *)
    
    (*
     * Inductive nat : Set :=
     * | O : nat
     * | S : nat -> nat.
     *)
    
    (* shows there is one (simple) recursive field *)
    
    Inductive nat_step : nat -> nat -> Prop :=
    | nat_step_a : forall x, nat_step x (S x).
    
    (* the nat_step relation expresses this recursion
     * every inductive type admits a step relation
     * (indexed inductives define indexed relations,
     * but maybe wrappig them in sigT would be better?)
     *)
    
    Theorem nat_step_Well_Founded : Well_Founded nat nat_step.
      
      unfold Well_Founded.
      
      induction x;
        apply below; intros y Ry.
      
      inversion Ry.
      
      inversion Ry.
      subst.
      assumption.
    
    Defined.
    
    (* Could one generically define all Φ_step relations,
     * and give a generic proof that they are all Well_Founded?
     *)
    
    (* The transitive closure of the step relation corresponds to
     * the usual idea of lt/(<) on nat:
     *)
    
    Definition nat_struct := Transitive_Closure nat nat_step.
    Definition nat_struct_Well_Founded :=
      Transitive_Closure_Well_Founded nat nat_step nat_step_Well_Founded.
    
    (* In general terms it is a typed version of the 'structurally smaller'
     * relation in the metatheory which lets definitions like the one in
     * By_Default be accepted
     *)
  
  End Nat_Structural_Measure.
  
  (* Now the equations we want to satisy are: *)
  
  (*
   * half O := O
   * half (S O) := O
   * half (S (S n)) := S (half n)
   *)
  
  (* so in terms of (toned down) eliminators that is:
   * 
   * half n := nat_case n
   *            O
   *            (fun n' Pn' =>
   *              nat_case n'
   *               O
   *               (fun n'' Pn'' =>
   *                 S (half n''))).
   * 
   * clearly that definition is not acceptable with
   *  no termination argument what-so-ever! so to
   *  rectify that, we can let P express that this
   *  number is smaller than n, and use well founded
   *  induction on the size measure.
   *)
  
  Lemma SSsmaller m : nat_struct m (S (S m)).
    intro m.
    apply transitivity with (S m).
    constructor.
    apply step.
    constructor.
  Defined.
  
  Definition half := Well_Founded_Induction nat nat_struct nat_struct_Well_Founded
    (fun _ => nat)
    (nat_rec (fun x => (forall y : nat, nat_struct y x -> nat) -> nat)
      (fun rec => O)
      (fun n Pn rec =>
        nat_rec (fun x => (forall y : nat, nat_struct y (S x) -> nat) -> nat)
        (fun rec => O)
        (fun m Pm rec => S (rec m (SSsmaller m)))
        n
        rec)).
  
  (*
   * The definition may look a bit complicated but I think this could
   *  be computed automatically from the equational specification,
   *  the method seems like a good way to compile dependent pattern matching
   *  into a basic type theory though, so that we don't have to use something
   *  like a 'match' construct.
   *)
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.
  
  (*
   * It's not luck (at least I think it's not, and I really hope so)
   *  that the recursive equality is provable by reflexivity, but it
   *  does require the SSsmaller proof term to be canonical (made up
   *  of constructors), since every proof that a term is structurally 
   *  smaller than another can be a canonical proof that poses no
   *  problem. I don't yet know how it will interact with dependent
   *  pattern match specialization though. (I can't think of any
   *  functions over inductive families that aren't 'step' recursive
   *  though, does anyone know of some examples?)
   *)

End By_Well_Founded_Induction.

Universes for discrimination proofs

2009-02-18T15:37:00.001-08:00

I can't decide if this is trivial or not. What does this construction mean/say?


module Universe where

data N0 : Set where

data Bool : Set where
 True : Bool
 False : Bool

data Direction : Set where
 Left : Direction
 Right : Direction

data Eq (T : Set) : T -> T -> Set where
 refl : (t : T) -> Eq T t t

-- Eq Set Bool Direction -> N0
--  is not provable
--  (techincally I would have to define Eq in Set1 but we can pretend universe polymorphism)

mutual
 data U : Set where
  n0 : U
  bool : U
  direction : U
  eq : (A : U) -> T A -> T A -> U
  pi : (A : U) -> (B : T A -> U) -> U
 
 T : U -> Set
 T n0 = N0
 T bool = Bool
 T direction = Direction
 T (eq A x y) = Eq (T A) x y
 T (pi A B) = (a : T A) -> T (B a)

mutual
 data U1 : Set where
  n0' : U1
  bool' : U1
  direction' : U1
  eq' : (A : U1) -> T1 A -> T1 A -> U1
  pi' : (A : U1) -> (B : T1 A -> U1) -> U1
  u' : U1
  lift : U -> U1
 
 T1 : U1 -> Set
 T1 n0' = N0
 T1 bool' = Bool
 T1 direction' = Direction
 T1 (eq' A x y) = Eq (T1 A) x y
 T1 (pi' A B) = (a : T1 A) -> T1 (B a)
 T1 u' = U
 T1 (lift A) = T A

T' : U -> Set
T' n0 = T n0
T' bool = T bool
T' direction = T n0
T' (eq A x y) = T n0
T' (pi A B) = T n0

rew : forall {A B : U} -> Eq U A B -> T' A -> T' B
rew (refl _) prf = prf

discr : Eq U bool direction -> N0
discr prf = rew prf True

corr : T1 (pi' (eq' u' bool direction) \_ -> n0')
corr = discr

Agda Supports Eta - Cont is a monad

2009-02-15T07:23:00.000-08:00

Since Agda 2 now supports eta in the definitional equality, here is a celebratory proof that Cont is a monad!


module eta where

data _==_ {T : Set} : T -> T -> Set where refl : (x : T) -> x == x

cont : Set -> Set -> Set
cont a r = (a -> r) -> r

return : forall {a r} -> a -> cont a r
return a f = f a

_>>=_ : forall {a b r} -> cont a r -> (a -> cont b r) -> cont b r
m >>= k = \c -> m (\a -> k a c)

cont-left-identity : forall {a b r} -> (o : a) -> (f : a -> cont b r) ->
 (return o >>= f) == f o
cont-left-identity o f = refl (f o)

cont-right-identity : forall {a r} -> (n : cont a r) ->
 (n >>= return) == n
cont-right-identity n = refl n

cont-associativity : forall {a b c r} -> (n : cont a r) -> (f : a -> cont b r) -> (g : b -> cont c r) ->
 ((n >>= f) >>= g) == (n >>= (\x -> (f x) >>= g))
cont-associativity n f g = refl ((n >>= f) >>= g)

Inventing a concrete syntax

2009-02-07T10:31:00.000-08:00

ind F : ★.

ind T : ★;
I : T.

ind Bool : ★;
true : Bool;
false : Bool.

ind N : ★;
O : N;
S : N → N.

ind Ord : ★
OO : Ord;
OS : Ord → Ord;
OL : (N → Ord) → Ord.

ind Fin : N → ★;
fz : (n:N)Fin (S n);
fs : (n:N)Fin n → Fin (S n).

ind Eq (A:★)(x:A):A → ★;
refl : Eq A x x.

ind JMEq (A:★)(x:A):(B:★)B → ★;
JMrefl : JMEq A x A x.

ind So : Bool → ★;
oh : So true.

ind Ex (T:★)(P:T → ★):★;
witness : (t : T)Prf(P t) → Ex T P.

ind Acc (A:★)(R:A → A → ★):A → ★;
below : ((y:A)R y x → Acc A R y) → Acc A R x.

ind W (A:★)(B:A → ★):★;
sup : (a:A)(f:B a → W A B)W A B.

CPS transformation using delimited continuations

2009-02-01T01:05:00.001-08:00


;; Idea: Use reified continuations to implement a CPS converter
;;
;; in the expression: (+ (* x x) (* y y))
;; the continuation of (* x x) is (lambda (x-squared) (+ x-squared (* y y)))
;;
;; similiarly,
;;
;; in the expression: (list '+ (list '* 'x 'x) (list '* 'y 'y))
;; the continuation of (list '* 'x 'x) is (lambda (x-squared) (list '+ x-squared (list '* 'y 'y)))

(require scheme/control) ;; shift/reset delimited continuations

;; > (reset (list '+ (shift k (list '* 'x 'x))     (list '* 'y 'y)))
;; (* x x)
;; > (reset (list '+ (shift k (k '?))              (list '* 'y 'y)))
;; (+ ? (* y y))
;; > (reset (list '+ (shift k (k (list '* 'x 'x))) (list '* 'y 'y)))
;; (+ (* x x) (* y y))
;; > (reset (list '+ (shift k `(let ((x-squared ,(list '* 'x 'x))) ,(k 'x-squared))) (list '* 'y 'y)))
;; (let ((x-squared (* x x))) (+ x-squared (* y y)))


;; CPS applications should throw the result value into a continuation
;; so (f x y z) turns into (f x y z (lambda (result) (continuation result)))

(define (apply# f . args) (shift k (let ((g (gensym "g"))) (reset `(,f ,@args (lambda (,g) ,(k g)))))))

;; Some examples of apply# in action:
;;
;; > `(k ,(apply# 'f--> 'x 'y 'z))
;; (f--> x y z (lambda (g349) (k g349)))
;; > (apply# 'f--> (apply# '+--> 2 3) 'y 'z)
;; (+--> 2 3 (lambda (g345) (f--> g345 y z (lambda (g346) g346))))
;; > (apply# 'f--> (apply# '+--> 2 3) (apply# '*--> 'x 'y) 'z)
;; (+--> 2 3 (lambda (g415) (*--> x y (lambda (g416) (f--> g415 g416 z (lambda (g417) g417))))))

;; What about syntax like IF? clearly apply# would be wrong (due to evaluation order) so define new syntax!
(define-syntax if#
  (syntax-rules ()
    ((if# <cond> <then> <else>) (shift k `(if ,<cond> ,(reset (k <then>)) ,(reset (k <else>)))))))

;; Examples:
;;
;; > (if# (apply# 'zero?--> 'n) ''yes ''no)
;; (zero?--> n (lambda (g374) (if g374 'yes 'no)))
;; > `(display ,(if# (apply# 'zero?--> 'n) ''yes ''no))
;; (zero?--> n (lambda (g850) (if g850 (display 'yes) (display 'no))))

(define-syntax define#
  (syntax-rules ()
    ((define# (name/args ...) body) `(define (name/args ... k-->) ,(reset `(k--> ,body))))))

;; That's enough now to CPS convert entire procedures:

;; > (define# (fact-iter--> n acc)
;;     (if# (apply# 'zero?--> 'n)
;;          'acc
;;          (apply# 'fact-iter--> (apply# '---> 'n 1) (apply# '*--> 'acc 'n))))
(define (fact-iter--> n acc k-->)
  (zero?--> n (lambda (g875)
   (if g875
       (k--> acc)
       (---> n 1 (lambda (g876)
        (*--> acc n (lambda (g877)
         (fact-iter--> g876 g877 (lambda (g878) (k--> g878)))))))))))

;; Test it! (this CPS format is a subset of Scheme)
(define (zero?--> n k) (k (zero? n)))
(define (*--> x y k) (k (* x y)))
(define (---> x y k) (k (- x y)))
;; > (fact-iter--> 7 1 display)
;; 5040


;; Now a function to CPS convert based on all this is trivial, it's just a fold
;; that replaces if with if#, define with define# and applications with apply#!

(define (if#-thunked cond then-thunk else-thunk) (if# cond (then-thunk) (else-thunk)))
(define (define#-thunked name/args body-thunk)
  (let ((k--> (gensym "k-->"))) `(define (,@name/args ,k-->) ,(reset `(,k--> ,(body-thunk))))))
(define (cps term)
  (if (pair? term)
      (case (car term)
        ((quote) `',term)
        ((if) (if#-thunked (cps (cadr term)) (lambda () (cps (caddr term))) (lambda () (cps (cadddr term)))))
        ((define) (define#-thunked (cadr term) (lambda () (cps (caddr term)))))
        (else (apply apply# (map cps term))))
      term))

;; > (cps '(define (fact-iter-2 n acc) (if (zero? n) acc (fact-iter-2 (- n 1) (* n acc)))))
(define (fact-iter-2--> n acc k-->)
  (zero?--> n (lambda (g443)
   (if g443
       (k--> acc)
       (---> n 1 (lambda (g444)
        (*--> n acc (lambda (g445)
         (fact-iter-2--> g444 g445 (lambda (g446)
          (k--> g446)))))))))))
;; > (fact-iter-2--> 8 1 display)
;; 40320

alternative beta-eta equality test

2009-01-21T05:22:00.000-08:00


import Prelude hiding (lookup,($))
import Control.Monad

type Ref = Integer

data V
 = Neutral N
 | Lam (V -> V)
 | Pi V (V -> V)
 | Set
 | Type

data N
 = App N V
 | Var Ref

Neutral n $ x = Neutral (App n x)
Lam f $ x = f x

lookup ((i, tau) : gamma) j
 | i == j = Just tau
 | otherwise = lookup gamma j
lookup [] _ = Nothing

eq gamma i f g (Pi tau sigmaF) = eq ((i, tau) : gamma) (i+1) (f $ x) (g $ x) (sigmaF x) where x = Neutral (Var i)
eq gamma i (Neutral n) (Neutral m) Set = maybe False (const True) (eqN gamma i n m)
eq gamma i s t Type = eqT gamma i s t

eqT gamma i (Pi s tF) (Pi u vF) = eqT gamma i s u && eqT ((i, s) : gamma) (i+1) (tF x) (vF x) where x = Neutral (Var i)
eqT gamma i Set Set = True

eqN gamma i (App n x) (App m y) = do
 Pi tau sigmaF <- eqN gamma i n m
 guard (eq gamma i x y tau)
 return (sigmaF x)
eqN gamma _ (Var i) (Var j)
 | i == j = lookup gamma i
 | otherwise = Nothing

-- test = eq [] 0
--   (Lam (\x -> x))
--   (Lam (\f -> Lam (\x -> f $ x)))
--   (Pi (Pi Set (\_ -> Set)) (\_ -> (Pi Set (\_ -> Set))))

-- > test
-- True

Data.Dynamic without typeclasses or unsafeCoerce

2009-01-12T01:08:00.000-08:00


{-# LANGUAGE RankNTypes, GADTs #-}

data DYN t where
 BOOL :: DYN Bool
 INT :: DYN Integer
 (:->:) :: DYN a -> DYN b -> DYN (a -> b)

data DYNAMIC where UnDYNAMIC :: DYN t -> t -> DYNAMIC
data Equal a b where REFL :: Equal x x

mkDyn :: DYN t -> t -> DYNAMIC
mkDyn code obj = UnDYNAMIC code obj

decide :: DYN t -> DYN u -> Maybe (Equal t u)
decide BOOL BOOL = Just REFL
decide INT INT = Just REFL
decide (u :->: v) (p :->: q) = do REFL <- decide u p; REFL <- decide v q; return REFL
decide _ _ = Nothing

unbox :: DYNAMIC -> DYN t -> Maybe t
unbox (UnDYNAMIC t e) u = do REFL <- decide t u; return e

list = [ mkDyn BOOL True, mkDyn INT 34, mkDyn (BOOL :->: INT) (\x -> if x then 32 else 56) ]

-- > unbox (list !! 0) BOOL
-- Just True
-- > unbox (list !! 1) BOOL
-- Nothing
-- > unbox (list !! 2) BOOL
-- Nothing
--
-- > unbox (list !! 0) INT
-- Nothing
-- > unbox (list !! 1) INT
-- Just 34
-- > unbox (list !! 2) INT
-- Nothing
--
-- > fmap ($ True) (unbox (list !! 2) (BOOL:->:INT))
-- Just 32
-- > fmap ($ False) (unbox (list !! 2) (BOOL:->:INT))
-- Just 56
-- > fmap ($ True) (unbox (list !! 1) (BOOL:->:INT))
-- Nothing

More GADT nonsense

2009-01-06T03:14:00.001-08:00


{-# LANGUAGE GADTs #-}

data CON f a fa k z where
 CTR :: c -> CON f a c z z
 VAR :: CON f a (a -> r) k z -> CON f a r (a -> k) z
 REC :: CON f a (f a -> r) k z -> CON f a r (f a -> k) z

infixr :+:
data SUM f a ka z where
 ZRO :: SUM f a (f a -> z) z
 (:+:) :: CON f a (f a) k z -> SUM f a ka z -> SUM f a (k -> ka) z


size :: kase -> SUM f a kase Integer -> f a -> Integer
size kase code = size' kase code kase code
size' :: kase -> SUM f a kase Integer -> ka -> SUM f a ka Integer -> f a -> Integer
size' kase code ka ZRO = ka
size' kase code ka (t :+: ts) = size' kase code (ka (sizeCON kase code 0 t)) ts
sizeCON :: kase -> SUM f a kase Integer -> Integer -> CON f a i0 k Integer -> k
sizeCON kase code k (CTR _) = 0 + k
sizeCON kase code k (VAR r) = \_ -> sizeCON kase code (1 + k) r
sizeCON kase code k (REC r) = \x -> sizeCON kase code (size kase code x + k) r


dfs :: kase -> SUM f a kase [a] -> f a -> [a]
dfs kase code = dfs' kase code kase code
dfs' :: kase -> SUM f a kase [a] -> ka -> SUM f a ka [a] -> f a -> [a]
dfs' kase code ka ZRO = ka
dfs' kase code ka (t :+: ts) = dfs' kase code (ka (dfsCON kase code [] t)) ts
dfsCON :: kase -> SUM f a kase [a] -> [a] -> CON f a i0 k [a] -> k
dfsCON kase code k (CTR _) = k
dfsCON kase code k (VAR r) = \a -> dfsCON kase code (a : k) r
dfsCON kase code k (REC r) = \x -> dfsCON kase code (dfs kase code x ++ k) r


data Both a = a :&: a
(&) = VAR (VAR (CTR (:&:)))
both = (&) :+: ZRO
bothCase (&) (x :&: y) = x & y
bothCaseR (&) (x :&: y) = y & x

data List a = Nil | Cons a (List a)
nil = CTR (Nil)
cons = REC (VAR (CTR (Cons)))
list = nil :+: cons :+: ZRO
listCase nil cons Nil = nil
listCase nil cons (Cons x xs) = cons x xs
listCaseR nil cons Nil = nil
listCaseR nil cons (Cons x xs) = cons xs x

data Tree a = Leaf a | Branch (Tree a) (Tree a)
leaf = VAR (CTR (Leaf))
branch = REC (REC (CTR Branch))
tree = leaf :+: branch :+: ZRO
treeCase leaf branch (Leaf a) = leaf a
treeCase leaf branch (Branch l r) = branch l r
treeCaseR leaf branch (Leaf a) = leaf a
treeCaseR leaf branch (Branch l r) = branch r l

-- > size bothCaseR both (True :&: False)
-- 2
-- > size listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))
-- 3
-- > size treeCaseR tree (Branch (Leaf ()) (Branch (Branch (Leaf ()) (Leaf ())) (Leaf ())))
-- 4
-- > dfs listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))
-- "xyz"
-- > dfs treeCaseR tree (Branch (Leaf 4) (Branch (Branch (Leaf 3) (Leaf 5)) (Leaf 7)))
-- [4,3,5,7]

beta eta equality for STLC by NbE

2009-01-04T07:00:00.000-08:00


{-# LANGUAGE NoMonomorphismRestriction #-}

import Prelude hiding (($))
import Control.Monad

type Ref = Int
newtype Scope a = Scope a deriving (Eq, Show)
data T = O | T :->: T deriving (Eq, Show)
data S = Var Ref | Lam T (Scope S) | App S S
       | Quote Ref deriving (Eq, Show)

abstract i t = Scope (extract 0 t) where
 extract r (Var j) = Var j
 extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b))
 extract r (App m n) = App (extract r m) (extract r n)
 extract r (Quote j)
  | j == i = Var r
  | otherwise = Quote j

gamma |- Var i = Just (gamma !! i)
gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)
gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return v

data V = VLam (V -> V)
       | VNeutral N
data N = NApp N V
       | NQuote Ref

VLam f $ x = f x
VNeutral n $ x = VNeutral (NApp n x)

eval delta (Var j) = delta !! j
eval delta (Lam _ (Scope b)) = VLam (\x -> eval (x:delta) b)
eval delta (App m n) = eval delta m $ eval delta n

------------------- OLD
-- r :: T -> V -> V
-- r O e = e
-- r (tau :->: sigma) f = VLam (\x -> r sigma (f $ (r tau x)))

------------------- NEW
r :: T -> V -> V
r O e = e
r (tau :->: sigma) f = f $ VLam (\f -> r sigma (VLam (\x -> f $ (r tau x))))



q i (VLam f) = Lam O (abstract i (q (i+1) (f (VNeutral (NQuote i)))))
q i (VNeutral n) = nq i n

nq i (NApp m n) = App (nq i m) (q i n)
nq i (NQuote j) = Quote j

nf tm = fmap (q 0 . flip r (eval [] tm)) ([] |- tm)

identity = Lam (O :->: O) (Scope (Var 0))
dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0)))))


{- OLDER
{-# LANGUAGE NoMonomorphismRestriction #-}

import Control.Monad

type Ref = Int
newtype Scope a = Scope a deriving (Eq, Show)
data T = O | T :->: T deriving (Eq, Show)
data S = Var Ref | Lam T (Scope S) | App S S
       | Quote Ref deriving (Eq, Show)

gamma |- Var i = Just (gamma !! i)
gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)
gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return v

data V = VLam T (V -> V) | VNeutral N
       | VQuote Ref
data N = NVar V | NApp N V
       | NQuote Ref

lift i (Var j)
 | j < i = Var j
 | otherwise = Var (j+1)
lift i (Lam t (Scope b)) = Lam t (Scope (lift (i+1) b))
lift i (App m n) = App (lift i m) (lift i n)

abstract i t = Scope (extract 0 t) where
 extract r (Var j) = Var j
 extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b))
 extract r (App m n) = App (extract r m) (extract r n)
 extract r (Quote j)
  | j == i = Var r
  | otherwise = Quote j

eta u t = Lam u (Scope (App (lift 0 t) (Var 0)))

etaReify (u :->: v) (Lam t (Scope b)) delta gamma = VLam u (\x -> etaReify v b (x:delta) (u:gamma))
etaReify (u :->: v) t delta gamma = etaReify (u :->: v) (eta u t) delta gamma
etaReify O t delta gamma = betaEtaReify O t delta gamma

betaEtaReify _   (Var i) delta gamma = delta !! i
betaEtaReify tau (Lam t (Scope b)) delta gamma = etaReify tau (Lam t (Scope b)) delta gamma
betaEtaReify tau (App m n) delta gamma = app (betaEtaReify (sigma :->: tau) m delta gamma) (etaReify sigma n delta gamma)
 where sigma = case gamma |- n of Nothing -> error "Type error" ; Just sigma -> sigma
       app (VLam _ f) x = f x
       app (VNeutral n) x = VNeutral (NApp n x)
       app (VQuote j) x = VNeutral (NApp (NQuote j) x)

quote i (VLam t f) = Lam t (abstract i (quote (i+1) (f (VQuote i))))
quote i (VNeutral n) = nquote i n
quote i (VQuote j) = Quote j

nquote i (NVar v) = quote i v
nquote i (NApp n v) = App (nquote i n) (quote i v)
nquote i (NQuote j) = Quote j

betaEtaNF p = do
 t <- [] |- p
 return (quote 0 (etaReify t p [] []))

betaEtaEqual p q = do
 t <- [] |- p ; t' <- [] |- q ; guard (t == t')
 return (quote 0 (etaReify t p [] []) == quote 0 (etaReify t q [] []))

identity = Lam (O :->: O) (Scope (Var 0))
dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0)))))

-- > betaEtaEqual identity dollar
-- Just True
-}

Other Peoples Thoughts

2008-12-26T14:40:00.000-08:00

"i kinda like haskell and erlang but i don't think they make it any easier to do anything. by the time you learn how to do the one liners, time has passed and you've become a professor of computer science, and your applications no longer matter."

"wow lisp occured in 1958"

"Yeah, but Haskell does such nice things for you. Like pattern matching? Very mathematical feel"

regarding C: "damn it.I m doing something so simple and its takes time.its like traveling from the UK to France via China"

Common Subexpression Elimination

2008-12-21T10:07:00.001-08:00


;; My example of when mutation is a useful tool that simplifies things.

(define (identity i) i)
(define (concat xs) (apply append xs))
(define (concat-map f x) (concat (map f x)))
(define (sort by xs)
  (define (insert by x xs)
    (if (null? xs)
        (list x)
        (if (< (by x) (by (car xs)))
            (cons x xs)
            (cons (car xs) (insert by x (cdr xs))))))
  (if (null? xs) '()
      (insert by (car xs) (sort by (cdr xs)))))

;; <variadic-tree> ::= <leaf> | (<variadic-tree> ...)
;; <leaf> is any non-list datum

(define (leaf? datum) (not (list? datum)))

(define (variadic-tree leaf nodes)
  (lambda (tree)
    (if (leaf? tree)
        (leaf tree)
        (apply nodes (map (variadic-tree leaf nodes) tree)))))

(define copy-tree (variadic-tree identity list))

(define exp-1
  (copy-tree
   '(+ (* (- x-1 x-2) (- x-1 x-2))
       (* (- y-1 y-2) (- y-1 y-2))
       (* (- z-1 z-2) (- z-1 z-2)))))

(define (splat tree)
  (if (leaf? tree)
      '()
      (cons tree (concat-map splat tree))))

(define (subexpressions tree) (sort length (cdr (splat tree))))

(define (eliminate exp sub sym)
  (cond ((null? exp) exp)
        ((leaf? exp) exp)
        ((cond ((equal? sub (car exp)) (set-car! exp sym))
               (else (eliminate (car exp) sub sym)))
         (eliminate (cdr exp) sub sym)
         exp)))

(define gensym
  (let ((n 0))
    (lambda ()
      (set! n (+ n 1))
      (string->symbol (string-append "g" (number->string n))))))

(define (eliminate-subexpressions env exp subs)
  (cond ((null? subs) `(let ,(reverse env) ,exp))
        (else
         (let* ((g (gensym))
                (sub (car subs))
                (exp-2 (eliminate exp sub g)))
           (eliminate-subexpressions (cons (list g sub) env) exp-2 (subexpressions exp-2))))))

;; (eliminate-subexpressions '() exp-1 (subexpressions exp-1))
;; =>
;; (let ((g1 (- z-1 z-2))
;;       (g2 (* g1 g1))
;;       (g3 (- y-1 y-2))
;;       (g4 (* g3 g3))
;;       (g5 (- x-1 x-2))
;;       (g6 (* g5 g5)))
;;   (+ g6 g4 g2))

Virgin Killer

2008-12-08T04:08:00.000-08:00

http://www.theregister.co.uk/2008/12/07/brit_isps_censor_wikipedia/

http://iwfwebfilter.thus.net/error/blocked.html

You are currently unable to edit pages on Wikipedia.

You can still read pages, but cannot edit, change, or create them.

Editing from 193.195.3.41 (your account, IP address, or IP address range) has been disabled by Lucasbfr for the following reason(s):

193.195.3.41 <-- This is the IP of the filter which I view wikipedia through.

I am not able to edit wikipedia because one of the million people viewing it through the same ip filter as me vandalised as article and was banned. I found out this censorship was the reason. Maybe if you want to help abused children you could find a way that doesn't mean sitting in a comfy chair fiddling with 1's and 0's and patting yourself on the back.

Statement by "IWF":

"IWF statement regarding Wikipedia URL
IWF is the UK’s internet ‘Hotline’ for the public and IT professionals to report potentially illegal online content within our remit. We work in partnership with the online industry, law enforcement, government, the education sector, charities, international partners and the public to minimise the availability of this content, specifically, child sexual abuse content hosted anywhere in the world and criminally obscene and incitement to racial hatred content hosted in the UK. We are an independent self-regulatory body, funded by the EU and the wider online industry, including internet service providers, mobile operators and manufacturers, content service providers, filtering companies, search providers, trade associations and the financial sector as well as other organisations that support us for corporate social responsibility reasons.

We help internet service providers and hosting companies to combat abuse of their networks through our national ‘notice and take-down’ service which alerts them to potentially illegal content within our remit on their systems and we provide unique data to law enforcement partners in the UK and abroad to assist investigations into the distributers of potentially illegal online content. As sexually abusive images of children are primarily hosted abroad, we facilitate the industry-led initiative to protect users from inadvertent exposure to this content by blocking access to it through our provision of a dynamic list of child sexual abuse URLs.

A Wikipedia web page, was reported through the IWF’s online reporting mechanism in December 2008. As with all child sexual abuse reports received by our Hotline analysts, the image was assessed according to the UK Sentencing Guidelines Council (page 109). The content was considered to be a potentially illegal indecent image of a child under the age of 18, but hosted outside the UK. The IWF does not issue takedown notices to ISPs or hosting companies outside the UK, but we did advise one of our partner Hotlines abroad and our law enforcement partner agency of our assessment. The specific URL (individual webpage) was then added to the list provided to ISPs and other companies in the online sector to protect their customers from inadvertent exposure to a potentially illegal indecent image of a child."

I had not realized that wikipedia (The free encylcopedia) is a hive of child sexual abuse and a den for pedophiles.

to IWF: Wikipedia is a website for people that are like to read and learn things, studying, or writing. You are not helping the world or sexually abused children by censoring it. Realize you have become robots and by following your protocols you're actually worsening the planet for everyone.

This is how all Authoritarian/Stalinist governments work.
First they choose to censor something that most people would find reasonable to censor, such as the image of a naked child.
Before you know it, all wikipedia pages relating to opposition politicians and opposition parties will also be unavailable.
I see IWF are 'supported' by both the Home Office and the Dept of Business, Enterprise and Regulatory Reform, enough said !

For people like Berlusconi the world will always be open and free. He can get on a jet and talk to his friends in Australia in person. For the rest of us, the internet will be what Berlusconi and his ilk allow us to have and see. And yes this is a small step, but there have been hundreds of little steps that add up.

Axiom Free NoConfusion in Coq

2008-12-02T04:00:00.000-08:00


Require Import Cast.
Require Import Fin.

Ltac prove_noConfusion :=
  intros;
    match goal with Eql : ?x = _ |- _ =>
      elim Eql; elim x; simpl; tauto end.

(*
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
*)

Definition NoConfusion_nat (P : Type) (x y : nat) : Type :=
  match x, y with
    | O, O => P -> P
    | O, S y => P
    | S x, O => P
    | S x, S y => (x = y -> P) -> P
  end.

Definition noConfusion_nat (P : Type) (x y : nat) :
  x = y -> NoConfusion_nat P x y.
prove_noConfusion.
Defined.

Definition eq_nat_dec : forall x y : nat, {x = y} + {x <> y}.
decide equality.
Defined.

Definition eq_nat_dec' : forall x y : nat, x = y \/ x <> y.
decide equality.
Defined.

(*
Inductive Fin : nat -> Set :=
| fz : forall n, Fin (S n)
| fs : forall n, Fin n -> Fin (S n).
*)

Notation FinINeq f g := (INeq nat Fin _ f _ g).

Definition NoConfusion_Fin (P : Type) (i : nat) (x y : Fin i) : Type :=
  match x, y with
    | fz _, fz _ => P -> P
    | fz _, fs _ _ => P
    | fs _ _, fz _=> P
    | fs x_i x, fs y_i y => (FinINeq x y -> P) -> P
  end.

Definition noConfusion_Fin (P : Type) (i : nat) (x y : Fin i) :
  x = y -> NoConfusion_Fin P i x y.
prove_noConfusion.
Defined.

Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)
  : fz = fs f -> P
  := fun Eq =>
    noConfusion_Fin P (S n) (fz) (fs f) Eq.

Definition fs_inj {n} {f f' : Fin n}
  : fs f = fs f' -> f = f'
  := fun Eq =>
    noConfusion_Fin (f = f') _ _ _ Eq (INeq_eq nat Fin eq_nat_dec _ _ _).

Inductive type : Set :=
| Nat : type
| Arrow : type -> type -> type.

Definition eq_type_dec (s t : type) : { s = t } + { s <> t }.
decide equality.
Defined.

Section equand.

Variable vars : nat.

Inductive equand : type -> Set :=
| Zero : equand Nat
| Succ : equand (Arrow Nat Nat)
| VAR (V : Fin vars) : equand Nat
| APP {A B} : equand (Arrow A B) -> equand A -> equand B.

Notation equandINeq f g := (INeq type equand _ f _ g).

Definition NoConfusion_equand (P : Type) (i : type) (x y : equand i) : Type :=
  match x, y with
    | Zero, Zero => P -> P
    | Succ, Succ => P -> P
    | VAR f, VAR f' => (f = f' -> P) -> P
    | APP xi xj xf xo, APP yi yj yf yo =>
      (equandINeq xf yf -> equandINeq xo yo -> P) -> P
    | _, _ => P
  end.

Definition noConfusion_equand (P : Type) (i : type) (x y : equand i) : x = y -> NoConfusion_equand P i x y.
prove_noConfusion.
Defined.

Definition Zero_One_clash (P : Type) (i : type)
  : Zero = APP Succ Zero -> P
  := fun Eq =>
    noConfusion_equand P Nat Zero (APP Succ Zero) Eq.

Definition APP_f_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)
  : @APP u v F O = @APP u v F' O' -> F = F'
  := fun Eq =>
    noConfusion_equand (F = F') _ _ _ Eq
    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ FEq).

Definition APP_o_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)
  : @APP u v F O = @APP u v F' O' -> O = O'
  := fun Eq =>
    noConfusion_equand (O = O') _ _ _ Eq
    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ OEq).

Definition eq_equand_dec : forall (t : type)(u v : equand t), {u = v} + {u <> v}.
apply INeq_dec_dec.
apply eq_type_dec.

refine (fix eq_equand_dec (i : type) (I : equand i)
                          (i' : type) (I' : equand i') {struct I} :
                          {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'} := _).
refine (match I as I in equand i, I' as I' in equand i'
        return {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'}
        with
          | Zero, Zero => _
          | Zero, Succ => _
          | Zero, VAR _ => _
          | Zero, APP _ _ _ _ => _
          | Succ, Zero => _
          | Succ, Succ => _
          | Succ, VAR _ => _
          | Succ, APP _ _ _ _ => _
          | VAR _, Zero => _
          | VAR _, Succ => _
          | VAR _, VAR _ => _
          | VAR _, APP _ _ _ _ => _
          | APP _ _ _ _, Zero => _
          | APP _ _ _ _, Succ => _
          | APP _ _ _ _, VAR _ => _
          | APP _ _ _ _, APP _ _ _ _ => _
        end);

try solve [ discriminate
          | left; reflexivity
          | right; intro Q; inversion Q
          | destruct B; right; intro Q; inversion Q; discriminate
          ].

destruct (fin_eq_dec V V0); subst.
left; reflexivity.
right; intro Q; inversion Q; contradiction.

destruct (eq_type_dec B B0);
(destruct (eq_equand_dec _ e0 _ e2) as [Q|N];[inversion Q|idtac]);
(destruct (eq_equand_dec _ e _ e1) as [Q'|N'];[inversion Q'|idtac]);
  subst;

try solve [ left;
  rewrite Q; try apply eq_type_dec;
  rewrite Q'; try apply eq_type_dec;
    reflexivity ];

right; intro NQ;
  try inversion NQ;
  try inversion Q;
  try inversion Q';
  try contradiction;
  try subst;
  try pose (APP_f_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ));
  try pose (APP_o_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ)).

apply N'; rewrite e3; reflexivity.
apply N; rewrite e4; reflexivity.
apply N; rewrite e4; reflexivity.
Defined.

Eval compute in (eq_equand_dec _
  (APP Succ (APP Succ Zero))
  (APP Succ (APP Succ Zero))
).

End equand.

Print Assumptions eq_equand_dec.


(*
 *  = left (APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero) -> False)
 *      (refl_equal (APP Succ (APP Succ Zero)))
 *  : {APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero)} +
 *    {APP Succ (APP Succ Zero) <> APP Succ (APP Succ Zero)}
 *
 * Computed fully, no JMeq_eq axiom stopping reduction
 *
 *)

Require Import Coven.
Require Import Arith.
Require Import Omega.
Print le.

Lemma le_irrelevent : forall n m (H1 H2:le n m), H1=H2.
refine (fix le_irrelevent n m (H1 H2:le n m) {struct H1} : H1=H2 := _).
apply INeq_eq; auto with arith.

refine (
  match H1 as H1' in _ <= m', H2 as H2' in _ <= m''
  return m = m' ->
         m = m'' ->
         INeq nat (le n) m H1 m' H1' ->
         INeq nat (le n) m H2 m'' H2' ->
         INeq nat (le n) m H1 m H2
  with
    | le_n, le_n => fun m'eq m''eq H1eq H2eq => _
    | le_n, le_S p_m p_le => fun m'eq m''eq H1eq H2eq => !
    | le_S p_m p_le, le_n => fun m'eq m''eq H1eq H2eq => !
    | le_S p_m p_le, le_S p_m' p_le' => fun m'eq m''eq H1eq H2eq => _
  end
  (refl_equal _)
  (refl_equal _)
  (INeq_refl _ _ _ _)
  (INeq_refl _ _ _ _)
); subst; subst.

rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).
rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).
reflexivity.

omega.

omega.

injection m''eq; intro; subst.
rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).
rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).
rewrite (le_irrelevent _ _ p_le p_le').
reflexivity.
Qed.

Print Assumptions le_irrelevent.
(** Closed under the global context **)

Dependently typed Data.Dynamic

2008-12-02T03:58:00.001-08:00


Require Import Eqdep_dec_defined.

Section Cast.
  
  Variable U:Type.
  Variable F : U -> Type.
  
  Variable eq_dec : forall x y:U, {x = y} + {x <> y}.
  
  Definition eq_decide : forall x y:U, x = y \/ x <> y.
  intros x y; destruct (eq_dec x y); [ left | right ]; assumption.
  Defined.
  
  Definition cast (i j : U) : F j -> option (F i) :=
    fun J =>
      match eq_dec j i with
        | left Eql => match Eql in _ = i return option (F i) with
                        | refl_equal => Some J
                      end
        | right _ => None
      end.
  
  Theorem cast_reflexivity (i : U) (I : F i) : cast i i I = Some I.
    unfold cast; intro i; destruct (eq_dec i i);
      [ subst | absurd (i = i); tauto ].
    rewrite (eq_proofs_unicity eq_decide e (refl_equal i)).
    reflexivity.
  Defined.
  
  Definition cast_injective (i : U) (I I' : F i) :
    cast i i I = cast i i I' -> I = I'.
  intros i I I'; repeat rewrite cast_reflexivity.
  intro SomeEq; injection SomeEq; tauto.
  Defined.
  
  Inductive INeq (i : U)(I : F i) : forall (j : U)(J : F j), Prop :=
  | INeq_refl : INeq i I i I.
  Implicit Arguments INeq [i j].
  
  Hint Resolve INeq_refl.
  
  Definition INeq_eq (i : U)(I I' : F i) : INeq I I' -> I = I'.
  intros i I I' inEq; apply cast_injective.
  change ((fun i' I' => cast i i I = cast i i' I') i I').
  elim inEq; reflexivity.
  Defined.
  Implicit Arguments INeq_eq [i I I'].
  
  Lemma INeq_ind_r :
    forall (i:U) (I J:F i) (P:F i -> Prop), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Lemma INeq_rec_r :
    forall (i:U) (I J:F i) (P:F i -> Set), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Lemma INeq_rect_r :
    forall (i:U) (I J:F i) (P:F i -> Type), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Definition INeq_dec_dec :
    (forall (i:U)(I:F i) (j:U)(J:F j), {INeq I J} + {~INeq I J}) ->
    (forall (i:U)(I J:F i), {I = J} + {I <> J}).
  intros ineq_dec i I J; destruct (ineq_dec i I i J); [ left | right ].
  apply INeq_eq; assumption.
  contradict n; subst; reflexivity.
  Defined.
  
End Cast.

Decidable Equality and Type Equality

2008-11-30T05:16:00.001-08:00


Require Import Eqdep_dec_defined.
(** Same as Eqdep_dec but s/Qed/Defined/ **)

Theorem dep_destruct :
  forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),
    (forall x' (v' : T' x') (Heq : x' = x),
      P (match Heq in (_ = x) return (T' x) with
           | refl_equal => v'
         end)) ->
      P v.
  intros T T' x v P I; apply (I _ v (refl_equal _)).
Defined.
(** Stolen from http://www.cs.harvard.edu/~adamc/cpdt/ **)

Inductive type : Set :=
| Nat : type
| Arrow : type -> type -> type.

Definition eq_type_dec' (s t : type) : s = t \/ s <> t.
decide equality.
Defined.

Inductive equand : type -> Set :=
| Zero : equand Nat
| Succ : equand (Arrow Nat Nat).

Definition eq_equand_dec {T} (x y : equand T) : {x = y} + {x <> y}.
intro.
destruct x;
  intro y; apply (dep_destruct type equand _ y);
    intros T y' Teq; destruct y';
      discriminate ||
        rewrite <- (eq_proofs_unicity eq_type_dec' (refl_equal _) Teq).
left; reflexivity.
left; reflexivity.
Defined.

Calculating Journeys

2008-11-30T00:13:00.000-08:00

-- WARNING: contains recursive programming


-- For example data, pick some imaginary flight network:

data Node = Paris | London | Shanghai | NewYork | Tokyo deriving (Eq, Show)

flights Paris = [London]
flights London = [Paris,Shanghai,NewYork]
flights Shanghai = [Tokyo,NewYork]
flights NewYork = [London]
flights Tokyo = [Paris,London,Shanghai]


-- and a convenient data representation of the transitive closure

data Graph a = {- DeadEnd | -} a :-->: [Graph a] deriving Show

transitiveClosure location = location :-->: map transitiveClosure (flights location)

{-- define the truncation of any cyclical journeys

finite visited DeadEnd = DeadEnd
finite visited (location :-->: destinations)
 | already visited location = DeadEnd
 |         otherwise        = location :-->: map (finite (location : visited)) destinations

already = flip elem
-}

{-- remove any 'DeadEnd's left over

simplify DeadEnd = DeadEnd
simplify (location :-->: destinations) = location :-->: purge (map simplify destinations)

purge = foldr cons []
 where cons DeadEnd ys = ys
       cons x       ys = x : ys
-}

-- holidays = simplify . finite [] . transitiveClosure

-- but fusing the truncation and simplification into one allows the 'DeadEnd' construtor to be erased!

simplifyFinite visited (location :-->: destinations) =
 location :-->: filter (not . already visited) (map (simplifyFinite (location : visited)) destinations)

already visited (location :-->: _) = elem location visited

holidays = simplifyFinite [] . transitiveClosure


-- > holidays Paris
-- Paris :-->: [London :-->: [Shanghai :-->: [Tokyo :-->: [],
--                                            NewYork :-->: []],
--                            NewYork :-->: []]]
-- > holidays London 
-- London :-->: [Paris :-->: [],
--               Shanghai :-->: [Tokyo :-->: [Paris :-->: []],
--                               NewYork :-->: []],
--               NewYork :-->: []]

my thought process for breadth first numbering

2008-11-22T13:49:00.000-08:00


data Tree a = Leaf a | Branch a (Tree a) (Tree a) deriving Show

i 0 = Leaf 0
i n = Branch 0 (i (n-1)) (i (n-1))


identity (Leaf i) = Leaf i
identity (Branch i left right) = Branch i (identity left) (identity right)


depth current (Leaf _) = Leaf current
depth current (Branch _ left right) = Branch current (depth (current + 1) left) (depth (current + 1) right)


depth' current (Leaf i) = Leaf i
depth' current (Branch i left right) = Branch i left' right'
 where left' = depth' (current + 1) left
       right' = depth' (current + 1) right


depth'' current target (Leaf i) = Leaf (if current == target then i+1 else i)
depth'' current target (Branch i left right) = Branch (if current == target then i+1 else i) left' right'
 where left' = depth'' (current + 1) target left
       right' = depth'' (current + 1) target right


depth''' current target delta (Leaf i) = Leaf (if current == target then i+delta else i) `with` (if current == target then delta+1 else delta)
depth''' current target delta (Branch i left right) = Branch (if current == target then i+delta else i) left' right' `with` delta''
 where (left',delta') = depth''' (current + 1) target (if current == target then delta+1 else delta) left
       (right',delta'') = depth''' (current + 1) target delta' right

with = (,)


unfold step current = case step current of Nothing -> current ; Just next -> unfold step next


breadth tree = case unfold step (0,0,tree) of (_,_,tree) -> tree
 where step (depth, delta, tree) = case depth''' 0 depth delta tree of
         (tree, delta') -> if delta == delta' then Nothing else Just (depth + 1, delta', tree)

-- > breadth (i 3)
-- Branch 0 (Branch 1 (Branch 3 (Leaf 7)
--                              (Leaf 8))
--                    (Branch 4 (Leaf 9)
--                              (Leaf 10)))
--          (Branch 2 (Branch 5 (Leaf 11)
--                              (Leaf 12))
--                    (Branch 6 (Leaf 13)
--                              (Leaf 14)))

Type Error

2008-11-20T12:41:00.001-08:00

Error:
In environment
ty : type
m : term ty
eq_term_dec :
forall (m' : {m' : term ty | size m' < size m}) (n : term ty),
{`m' = n} + {`m' <> n}
n : term ty
eq_term_dec0 :
forall (ty : type) (m n : term ty),
{[m : (term ty)]= [n : (term ty)]} + {m =/= n}
ty0 : type
m0 : term ty0
n0 : term ty0
uTy : type
vTy : type
u : term (uTy --> vTy)
v : term uTy
uTy' : type
vTy' : type
u' : term (uTy' --> vTy')
v' : term uTy'
vTyEq : vTy = vTy'
filtered_var := eq_type_dec uTy uTy' : {uTy = uTy'} + {uTy <> uTy'}
uTyEq : uTy = uTy'
Heq_anonymous : in_left = filtered_var
u0 : term (uTy --> vTy)
v0 : term uTy
u'0 : term (uTy --> vTy)
v'0 : term uTy
filtered_var0 := eq_term_dec0 (uTy --> vTy) u0 u'0 :
{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}
filtered_var1 := eq_term_dec0 uTy v0 v'0 :
{[v0 : (term uTy)]= [v'0 : (term uTy)]} + {v0 =/= v'0}
branch_0 :=
fun (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)])
  (Heq_anonymous0 : in_left = filtered_var0)
  (Heq_anonymous1 : in_left = filtered_var1) => in_left :
forall
  (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
in_left = filtered_var0 ->
in_left = filtered_var1 ->
{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +
{app u0 v0 =/= app u'0 v'0}
branch_1 :=
fun
  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +
               {u0 =/= u'0})
  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
                {u'0 =/= filtered_var0})
  (H : forall
         (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0
                       : (term (uTy --> vTy))])
         (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
       ~ (in_left = wildcard' /\ in_left = wildcard'0))
  (Heq_anonymous0 : wildcard' = filtered_var0)
  (Heq_anonymous1 : wildcard'0 = filtered_var1) => in_right :
forall
  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +
               {u0 =/= u'0})
  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
                {u'0 =/= filtered_var0}),
(forall
   (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
   (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
 ~ (in_left = wildcard' /\ in_left = wildcard'0)) ->
wildcard' = filtered_var0 ->
wildcard'0 = filtered_var1 ->
{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +
{app u0 v0 =/= app u'0 v'0}
Anonymous : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]
wildcard' := in_left :
{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}
Anonymous0 : u'0 =/= wildcard'
wildcard'0 := in_right :
{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}
The term "wildcard'0" has type
 "{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}"
 while it is expected to have type
 "{[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
  {u'0 =/= filtered_var0}".

Variadic via GADT

2008-11-15T08:00:00.001-08:00


data Pill a where
 Stop :: Pill Integer
 O :: Pill (Pill a -> a)

collect :: Integer -> Pill a -> a
collect i Stop = i
collect i O = collect (i+1)

start = collect 0

-- > start Stop
-- 0
-- > start O Stop
-- 1
-- > start O O Stop
-- 2
-- > start O O O Stop
-- 3
-- > start O O O O Stop
-- 4
-- > start O O O O O Stop
-- 5

Somewhat Pointfree Haskell Huffman Tree

2008-11-09T05:18:00.000-08:00

{-# LANGUAGE NoMonomorphismRestriction #-}

import Prelude hiding (Either(..))
import Data.List

import Data.Maybe
import Data.Ord
import Control.Monad.Reader

lookdown :: (Eq b) => [(a, b)] -> b -> Maybe a

lookdown pairs i = lookup i (map swap pairs)

onFst f (x,y) = (f x, y)

swap (x,y) = (y,x)
f & g = \x -> (f x, g x)

infix 4 &

-------

data Huff a = Leaf a | Branch (Huff a) (Huff a) deriving Show

-- -- Example tree:
-- let t =
--   (Branch (Leaf T)
--           (Branch (Leaf F)
--                   (Leaf T)))


foldHuff leaf branch = φ
 where φ (Leaf o) = leaf o
       φ (Branch left right) = branch (φ left) (φ right)

-- foldHuff (!) (*) t =
--   (* (! T)
--      (* (! F)
--         (! T)))

instance Functor Huff where fmap f = foldHuff (Leaf . f) Branch

depthFirstTraversal = foldHuff return (++)

-- foldHuff (!) (*) t =
--   (return T) ++

--       (return F) ++
--       (return T)
-- = [T,F,T]

member e = foldHuff (== e) (||)


data Direction = Left | Right deriving Show

type Path = [Direction]

branch join left right = \φleft φright -> join (left φleft) (right φright)

label = foldHuff (Leaf . (,) []) -- you are here
                 (branch Branch (fmap (onFst (Left:))) -- first on your left
                                (fmap (onFst (Right:))))

type Freq a = (Integer, Huff a)

frequencies = map (length & Leaf . head) . sortBy (comparing length) . group . sort

joinTrees ((p1,t1) : (p2,t2) : freqs) = joinTrees (insertBy (comparing fst) (p1 + p2,Branch t1 t2) freqs)
joinTrees [(_,tree)] = tree

huffmanTree = joinTrees . frequencies

codeTable = depthFirstTraversal . label . huffmanTree

encode codeTable = catMaybes . map (lookdown codeTable)

huffmanCode = concat . join (encode . codeTable)

traverse (Leaf o) path = Just (o, path)
traverse (Branch l r) (Left:path) = traverse l path
traverse (Branch l r) (Right:path) = traverse r path
traverse _ [] = Nothing

huffmanDecode = unfoldr . traverse


-- forall text, length text > 1 ->
correct text = huffmanDecode (huffmanTree text) (huffmanCode text) == text

-- checking how many bits saved on an 8 bit encoded string
savings text = length text * 8 - length (huffmanCode text)


-- > huffmanTree "quick brown fox jumped over the lazy dog"
-- Branch (Branch (Branch (Branch (Branch (Leaf 'i') (Leaf 'j')) (Branch (Leaf 'g') (Leaf 'h'))) (Branch (Branch (Leaf 'm') (Leaf 'n')) (Branch (Leaf 'k') (Leaf 'l')))) (Branch (Branch (Leaf 'd') (Leaf 'r')) (Branch (Branch (Leaf 'c') (Leaf 'f')) (Branch (Leaf 'a') (Leaf 'b'))))) (Branch (Branch (Leaf 'o') (Branch (Leaf 'u') (Leaf 'e'))) (Branch (Leaf ' ') (Branch (Branch (Branch (Leaf 't') (Leaf 'v')) (Branch (Leaf 'p') (Leaf 'q'))) (Branch (Branch (Leaf 'y') (Leaf 'z')) (Branch (Leaf 'w') (Leaf 'x'))))))

-- > correct "quick brown fox jumped over the lazy dog"
-- True

-- > savings  "quick brown fox jumped over the lazy dog"
-- 143

Coq Extension

2008-10-31T11:24:00.000-07:00


(*
NoConfusion_Foo (P : Type) [indices] (u v : Foo [indices]) :=
 match u, v with
 | Foo x y z, Foo x y z => (x == x' -> y == y' -> z == z' -> P) -> P
 | ...
 | Chalk*, Cheese* => P
 end
*)

(*
noConfusion_Foo (P : Type) [indices] (u v : Foo [indices]) : u == v -> NoConfusion_foo P [indices] u v.
*)

open Univ
open Inductive
open Util
open Coqlib

let ith_univ i = make_univ (make_dirpath [id_of_string"implicit"], i)
let implicit_type i = mkSort (Type (ith_univ i))
let raw_type i = RSort (dummy_loc, RType (Some (ith_univ i)))

let coq_heq_ref = lazy (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq")

let construct_no_conf_body env ind mind =
  let ctr_types = arities_of_constructors ind mind in
  let n_ctr_types = Array.length ctr_types in
  let n_indices = length (snd mind).mind_arity_ctxt in
  let indices =
    let rec names i = if i > n_indices then [] else RVar (dummy_loc, id_of_string ("e"^string_of_int i)) :: names (i+1) in names 1 in
  let abstract_indices x =
    let rec abs i =
      if i > n_indices
       then x
       else RLambda (dummy_loc, Name (id_of_string ("e"^string_of_int i)), Explicit, RHole (dummy_loc, BinderType Anonymous), abs (i+1)) in
    abs 1 in
  Pretyping.Default.understand Evd.empty env
   (RLambda (dummy_loc, Name (id_of_string "P"), Explicit, raw_type 1,
   abstract_indices
   (RLambda (dummy_loc, Name (id_of_string "u"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
   (RLambda (dummy_loc, Name (id_of_string "v"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     RCases (dummy_loc, MatchStyle, None,
       [(RVar (dummy_loc, (id_of_string "u")), (Anonymous, None));(RVar (dummy_loc, (id_of_string "v")), (Anonymous, None))],
       (Array.to_list (Array.mapi (fun i ty_i ->
         let ctr = (ind, i+1) in
         let ctr_args = constructor_nrealhyps env ctr in
         let rec spread n i = if i = 0 then [] else (PatVar (dummy_loc, Name (id_of_string (n^string_of_int i)))) :: spread n (i-1) in
         let left_patterns = List.rev (spread "i" ctr_args) in
         let right_patterns = List.rev (spread "j" ctr_args) in
         let rec assume_eqs n x = if n > ctr_args
                                   then x
                                   else RProd (dummy_loc, Anonymous, Explicit,
                                        RApp (dummy_loc, RRef (dummy_loc, Lazy.force coq_heq_ref),
                                          [RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string ("i"^string_of_int n));
                                           RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string ("j"^string_of_int n))]),
                                        assume_eqs (n+1) x) in
         (dummy_loc, [id_of_string "foo";id_of_string "bar"],
                     [PatCstr (dummy_loc, ctr, left_patterns, Anonymous);PatCstr (dummy_loc, ctr, right_patterns, Anonymous)],
                     RProd (dummy_loc, Anonymous, Explicit,
                       assume_eqs 1 (RVar (dummy_loc, id_of_string "P")), RVar (dummy_loc, id_of_string "P")))) ctr_types) @
        if n_ctr_types = 1
         then []
         else [(dummy_loc, [id_of_string "foo";id_of_string "bar"],
                           [PatVar (dummy_loc, Anonymous);PatVar (dummy_loc, Anonymous)],
                           RVar (dummy_loc, id_of_string "P"))]))))))))

let construct_no_conf_declaration env ind mind =
 DefinitionEntry
  { const_entry_body = construct_no_conf_body env ind mind;
    const_entry_type = None;
    const_entry_opaque = false;
    const_entry_boxed = false }, IsDefinition Definition

let construct_little_no_conf env ind mind little_no_conf no_conf =
  let n_indices = length (snd mind).mind_arity_ctxt in
  let indices =
    let rec names i = if i > n_indices then [] else RVar (dummy_loc, id_of_string ("e"^string_of_int i)) :: names (i+1) in names 1 in
  let abstract_indices x =
    let rec abs i =
      if i > n_indices
       then x
       else RProd (dummy_loc, Name (id_of_string ("e"^string_of_int i)), Explicit, RHole (dummy_loc, BinderType Anonymous), abs (i+1)) in
    abs 1 in
  let little_no_conf_type = Pretyping.Default.understand Evd.empty env 
     (RProd (dummy_loc, Name (id_of_string "P"), Explicit, raw_type 1,
      abstract_indices
     (RProd (dummy_loc, Name (id_of_string "u"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     (RProd (dummy_loc, Name (id_of_string "v"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     (RProd (dummy_loc, Name (id_of_string "eql"), Explicit,
                          RApp (dummy_loc, RRef (dummy_loc, Lazy.force coq_heq_ref),
                           [RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string "u");
                            RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string "v")]),
       RApp (dummy_loc, RRef (dummy_loc, no_conf),
        ([RVar (dummy_loc, id_of_string "P")] @
         indices @
         [RVar (dummy_loc, id_of_string "u");
          RVar (dummy_loc, id_of_string "v")])))))))))) in
  try
    let _ =
    Pfedit.start_proof little_no_conf (Global, DefinitionBody Definition)
      (named_context_val env)
      little_no_conf_type
      (fun _ _ -> ());
    Pfedit.by (tclTHENSEQ
      [intros;
       simplest_elim (mkVar (id_of_string "eql"));
       simplest_elim (mkVar (id_of_string "u"));
       simpl_in_concl;
       Tauto.tauto]) in
    let _,(const,_,_) = Pfedit.cook_proof (fun _ -> ()) in
     Pfedit.delete_current_proof ();
     DefinitionEntry const, IsDefinition Definition
  with e ->
    Pfedit.delete_current_proof ();
    msg (str "Could not prove noConfusion, this is a serious (unexpected) problem!");
    raise e

let no_confusion i =
  check_required_library ["Coq";"Logic";"JMeq"];
  let env = Global.env () in
  let istr = string_of_id i in
  try
    match Nametab.locate (qualid_of_string istr) with
    | IndRef ind ->
       let mind = lookup_mind_specif env ind in
            let no_conf = add_prefix "NoConfusion_" i in
            let little_no_conf = add_prefix "noConfusion_" i in
            (* msg (print_constr (construct_no_conf_body env ind mind)); TODO: Print a better message *)
            let _ = Declare.declare_constant no_conf (construct_no_conf_declaration env ind mind) in
            let no_conf_ty = Nametab.locate (qualid_of_string ("NoConfusion_"^istr)) in
            let env = Global.env () in
            Declare.declare_constant little_no_conf (construct_little_no_conf env ind mind little_no_conf no_conf_ty);
            ()
    | _ -> msg (str (istr^" is not an inductive."))
  with Not_found -> msg (str ("Inductive "^istr^" not found in global environment."))
 

VERNAC COMMAND EXTEND Derive_NoConfusion
| [ "Derive" "NoConfusion" ident(i) ] -> [ no_confusion i ]
END

2008-10-27T15:16:00.001-07:00


% Unprogramming a permutation machine

stack([],[],[]) --> [].
stack([push|Instrs],[I|IS],SS) --> stack(Instrs,IS,[I|SS]).
stack([pop|Instrs],IS,[S|SS]) --> [S], stack(Instrs,IS,SS).

% ?- phrase(stack(Instructions, [1,2,3,4,5], []), [1,2,4,3,5], []).
% Instructions = [push, pop, push, pop, push, push, pop, pop, push, pop] .

Implementing tactics in Coq

2008-10-12T14:47:00.000-07:00


Require Import List.

Section propr.
  Variable Sym : Set.
  Variable lookup : Sym -> Prop.
  Variable eq_Sym_dec : forall s s' : Sym, {s = s'} + {s <> s'}.
  
  Inductive prop : Set :=
  | var : Sym -> prop
  | imp : prop -> prop -> prop.
  
  Fixpoint interpret (p : prop) : Prop :=
    match p with
      | var i => lookup i
      | imp p q => interpret p -> interpret q
    end.
  
  Fixpoint assume (context : list Sym) :=
    match context with
      | nil => True
      | i :: is => lookup i /\ assume is
    end.
  
  Fixpoint contextLookup (i : Sym) (context : list Sym) :=
    match context as context' return option (assume context' -> interpret (var i)) with
      | nil => None
      | j::js =>
        match eq_Sym_dec i j with
          | left eql =>
            match eql with
              | refl_equal =>
                Some (fun hypotheses =>
                  match hypotheses with
                    | conj J _ => J
                  end)
            end
          | right _ =>
            match contextLookup i js with
              | Some Prf =>
                Some (fun hypotheses =>
                  match hypotheses with
                    | conj _ Js => Prf Js
                  end)
              | None => None
            end
        end
    end.
  
  Fixpoint proveable' (p : prop) (context : list Sym) : option (assume context -> interpret p) :=
    match p as p' return option (assume context -> interpret p') with
      | var i => contextLookup i context
      | imp (var i) q =>
        match proveable' q (i :: context) with
          | Some Hypo'X => Some (fun Hyp o => Hypo'X (conj o Hyp))
          | None => None
        end
      | imp _ x => None
    end.
  
  Definition some X (x : option X) :=
    match x with
      | Some _ => True
      | None => False
    end.
  Implicit Arguments some [X].
  
  Theorem proveable'_proveable p : some (proveable' p nil) -> interpret p.
    intro p; destruct (proveable' p nil); [ exact i | simpl; tauto ].
  Qed.

End propr.


Require Import Arith.

Theorem test (X Y Z W : Prop) : X -> Y -> Z -> X -> Y -> Z.
intros X Y Z W.
exact
  (proveable'_proveable
    nat
    (fun i =>
      match i with
        | 0 => X
        | 1 => Y
        | 2 => Z
        | 3 => W
        | _ => False
      end)
    eq_nat_dec
    (imp _ (var _ 0)
      (imp _ (var _ 1)
        (imp _ (var _ 2)
          (imp _ (var _ 0)
            (imp _ (var _ 1) (var _ 2))))))
  I).
Qed.

Print test.
(**************

test = 
fun X Y Z W : Prop =>
proveable'_proveable nat
  (fun i : nat =>
   match i with
   | 0 => X
   | 1 => Y
   | 2 => Z
   | 3 => W
   | S (S (S (S _))) => False
   end) eq_nat_dec
  (imp nat (var nat 0)
     (imp nat (var nat 1)
        (imp nat (var nat 2)
           (imp nat (var nat 0) (imp nat (var nat 1) (var nat 2)))))) I
     : forall X Y Z : Prop, Prop -> X -> Y -> Z -> X -> Y -> Z

 ***************)

eq_fin_dec via NoConfusion

2008-10-11T11:57:00.000-07:00


Require Import JMeq.
Infix "==" := JMeq (at level 30).
Notation "X =/= Y" := (X == Y -> False) (at level 30).

Inductive Fin : nat -> Set :=
| fz n : Fin (S n)
| fs n : Fin n -> Fin (S n).

Fixpoint Fin_NoConfusion (P : Type) (n : nat) (f f' : Fin n) {struct f} :=
  match f, f' with
    | fz _, fz _ => P -> P
    | fs _ f, fs _ f' => (f == f' -> P) -> P
    | _, _ => P
  end.

Definition Fin_noConfusion P n (f f' : Fin n) : f == f' -> Fin_NoConfusion P n f f'.
intros P n f f' Eq.
elim Eq.
elim f;
  simpl; intros; tauto.
Defined.

Definition fs_injective (P : Type) (n : nat) (f f' : Fin n)
  : (f == f' -> P) -> (fs n f == fs n f' -> P)
  := fun m Eq =>
    Fin_noConfusion P (S n) (fs n f) (fs n f') Eq m.

Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)
  : fz n == fs n f -> P
  := fun Eq =>
    Fin_noConfusion P (S n) (fz n) (fs n f) Eq.

Definition eq_fin_dec n : forall f f' : Fin n, {f == f'} + {f =/= f'}.
refine (fix eq_fin_dec n (f f' : Fin n) {struct f'} : {f == f'} + {f =/= f'} :=
  match f in Fin n, f' in Fin n' return n = n' -> {f == f'} + {f =/= f'} with
    | fz _, fz _ => _
    | fs _ _, fz _ => _
    | fz _, fs _ _ => _
    | fs _ _, fs _ _ => _
  end (refl_equal _));
intro Eq; injection Eq; clear Eq; intro Eq.

left; rewrite Eq; reflexivity.

right; rewrite Eq; intro; exact (fz_fs_clash False _ _ H).

right; rewrite <- Eq; intro; exact (fz_fs_clash False _ _ (sym_JMeq H)).

clear f f' n; subst n0.
destruct (eq_fin_dec n1 f0 f1).
left; elim j; reflexivity.
right; intro; apply f; exact (fs_injective _ _ _ _ (fun Eq => Eq) H).
Defined.

A different approach

2008-10-10T15:08:00.001-07:00

Just typing out stuff from http://www.cs.nott.ac.uk/~pwm/ .


module Universe where

open import Data.Nat

data SPT : ℕ -> Set1 where
 vz : {n : ℕ} -> SPT (suc n)
 vs : {n : ℕ} -> SPT n -> SPT (suc n)
 _[_] : {n : ℕ} -> SPT (suc n) -> SPT n -> SPT n
 “0” : {n : ℕ} -> SPT n
 “1” : {n : ℕ} -> SPT n
 _“+”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“×”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“->”_ : {n : ℕ} -> (K : Set) -> SPT n -> SPT n
 “μ”_ : {n : ℕ} -> SPT (suc n) -> SPT n

data Tel : ℕ -> (ℕ -> Set1) -> Set2 where
 ε : (F : ℕ -> Set1) -> Tel zero F
 _^_ : {F : ℕ -> Set1} -> {n : ℕ} -> F n -> Tel n F -> Tel (suc n) F

data ⟦_⟧_ : {n : ℕ} -> SPT n -> Tel n SPT -> Set2 where
 top : {n : ℕ} -> {T' : Tel n SPT} -> {T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vz ⟧ (T ^ T')
 pop : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vs T ⟧ (S ^ T')
 def : {n : ℕ} -> {T' : Tel n SPT} -> {A : SPT n} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ (A ^ T') -> ⟦  F [ A ]  ⟧ T'
 void : {n : ℕ} -> {T' : Tel n SPT} ->
   ⟦ “1” ⟧ T'
 inl : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ S “+” T ⟧ T'
 inr : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ S “+” T ⟧ T'
 pair : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ S “×” T ⟧ T'
 funk : {n : ℕ} -> {T' : Tel n SPT} -> {K : Set} -> {T : SPT n} ->
  (f : K -> ⟦ T ⟧ T') -> ⟦ (K “->” T) ⟧ T'
 miso : {n : ℕ} -> {T' : Tel n SPT} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ ((“μ” F) ^ T') -> ⟦ (“μ” F) ⟧ T'



“Nat” : {n : ℕ} -> SPT n
“Nat” = “μ” (“1” “+” vz)

“zero” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T'
“zero” = miso (inl (void))

“succ” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“succ” x = miso (inr (top x))


data “Nat”-View : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> Set2 where
 isZero : {n : ℕ} -> {T' : Tel n SPT} -> “Nat”-View {n} {T'} “zero”
 isSucc : {n : ℕ} -> {T' : Tel n SPT} -> (x : ⟦ “Nat” ⟧ T') -> “Nat”-View {n} {T'} (“succ” x)

viewNat : {n : ℕ} -> {T' : Tel n SPT} -> (n : ⟦ “Nat” ⟧ T') -> “Nat”-View n
viewNat {n} {T'} (miso Q) = aux1 Q
 where aux3 : (r : ⟦ vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inr r))
       aux3 (top x) = isSucc x
       aux2 : (l : ⟦ “1” ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inl l))
       aux2 void = isZero
       aux1 : (u : ⟦ “1” “+” vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso u)
       aux1 (inl U) = aux2 U
       aux1 (inr V) = aux3 V

“add” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“add” x y with viewNat x
“add” (miso (inl (void))) y | isZero = y
“add” (miso (inr (top x))) y | isSucc .x = “succ” (“add” x y)


test = “add” {zero} {ε SPT}
         (“succ” (“succ” (“succ” “zero”)))
         (“succ” (“succ” “zero”))

{- =
miso
(inr
 (top
  (miso
   (inr
    (top
     (miso
      (inr
       (top
        (miso (inr (top (miso (inr (top (miso (inl void)))))))))))))))) -}

Emulate Agda style pattern matching in Coq using ideas frow Eliminating Dependent Pattern Matching..


Require Import JMeq.
Infix "==" := JMeq (at level 31).
Notation "[ x : X ]  == [ y : Y ]" := (@JMeq X x Y y) (at level 30).
Notation "X =/= Y" := (JMeq _ X _ Y -> False) (at level 30).


Derive NoConfusion nat.
Definition noConfusion_nat (P : Type) (u v : nat) : JMeq u v -> NoConfusion_nat P u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.


Inductive SPT : nat -> Type :=
| vz {n} : SPT (S n)
| vs {n} : SPT n -> SPT (S n)
| of {n} : SPT (S n) -> SPT n -> SPT n
| q_zero_q {n} : SPT n
| q_one_q {n} : SPT n
| q_sum_q {n} : SPT n -> SPT n -> SPT n
| q_mul_q {n} : SPT n -> SPT n -> SPT n
| q_arrow_q {n} : Type -> SPT n -> SPT n
| q_mu_q {n} : SPT (S n) -> SPT n.
Derive NoConfusion SPT.
Definition noConfusion_SPT (P : Type) (e1 : nat) (u v : SPT e1) : JMeq u v -> NoConfusion_SPT P e1 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Inductive Tel : nat -> (nat -> Type) -> Type :=
| eps : forall {F}, Tel 0 F
| telCons : forall {F} {n}, Tel n F -> F n -> Tel (S n) F.
Infix ";" := telCons (at level 27, left associativity).
Derive NoConfusion Tel.
Definition noConfusion_Tel (P : Type) (e1 : nat) (e2 : nat -> Type) (u v : Tel e1 e2) : JMeq u v -> NoConfusion_Tel P e1 e2 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Reserved Notation "⟦  type ⟧ scope" (at level 30, no associativity).
Inductive Interpretation : forall n, SPT n -> Tel n SPT -> Type :=
| top {n} {T' : Tel n SPT} {T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vz ⟧ (T';T)
| pop {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vs T ⟧ (T';S)
| def {n} {T' : Tel n SPT} {A : SPT n} {F : SPT (S n)}
  : ⟦ F ⟧ (T'; A) -> ⟦ of F A ⟧ T'
| void {n} {T' : Tel n SPT}
  : ⟦ q_one_q ⟧ T'
| inl {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| inr {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| pair {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ q_mul_q S T ⟧ T'
| funk {n} {T' : Tel n SPT} {K : Type} {T : SPT n}
  : (K -> ⟦ T ⟧ T') -> ⟦ q_arrow_q K T ⟧ T'
| miso {n} {T' : Tel n SPT} {F : SPT (S n)}
  : ⟦ F ⟧ (T';q_mu_q F) -> ⟦ q_mu_q F ⟧ T'
where "⟦  type ⟧ scope" := (Interpretation _ type scope).
Derive NoConfusion Interpretation.
Definition noConfusion_Interpretation (P : Type) (e1 : nat) (e2 : SPT e1) (e3 : Tel e1 SPT) (u v : ⟦e2 ⟧ e3) : JMeq u v -> NoConfusion_Interpretation P e1 e2 e3 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Definition mu_injective (P : Type) (e1 : nat) (u v : SPT (S e1))
  : (e1 == e1 -> u == v -> P) -> (q_mu_q u == q_mu_q v -> P)
  := fun m Eq =>
    noConfusion_SPT P _ (q_mu_q u) (q_mu_q v) Eq m.

Definition mu_vz_clash (P : Type) (n : nat) (F : SPT (S (S n)))
  : q_mu_q F == vz -> P
  := fun Eq =>
    noConfusion_SPT P (S n) (q_mu_q F) vz Eq.



Definition q_Nat_q {n} : SPT n := q_mu_q (q_sum_q q_one_q vz).
Definition q_O_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' := miso (inl void).
Definition q_S_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> ⟦ q_Nat_q ⟧ T' := fun x => miso (inr (top x)).

Inductive q_Nat_q'View {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> Type :=
| isO : q_Nat_q'View q_O_q
| isS : forall x : ⟦ q_Nat_q ⟧ T', q_Nat_q'View (q_S_q x).



Ltac dpm_lift := repeat match goal with H : _ |- _ => intro Eq; revert H; revert Eq end.
Ltac dpm_prepare :=
  match goal with
    | |- @JMeq _ ?x _ ?x -> _ => intros _; dpm_prepare
    | |- @JMeq _ _ _ _ -> _ => dpm_lift
    | _ => intro; dpm_prepare
  end.

Ltac dpm_subst := intro Eql;
  match type of Eql with @JMeq _ ?x _ ?y =>
    (rewrite Eql; clear x Eql) || (rewrite <- Eql; clear y Eql)
  end.

Ltac dpm_confusion := intro Eql;
  match goal with |- ?P =>
    apply (noConfusion_nat P _ _ Eql)||
    apply (noConfusion_SPT P _ _ _ Eql)||
    apply (noConfusion_Tel P _ _ _ _ Eql)||
    apply (noConfusion_Interpretation P _ _ _ _ _ Eql)
  end.

Ltac dpm_specialize := repeat (dpm_prepare; (dpm_subst||dpm_confusion)).



Definition view'q_Nat_q
  (n : nat) (Ts : Tel n SPT) (x : ⟦ q_Nat_q ⟧ Ts) : (@q_Nat_q'View n Ts x).
intros.

refine
  (Interpretation_rect
    (fun n' S' Ts' x' =>
      n == n' -> @q_Nat_q n == S' -> Ts == Ts' -> x == x' ->
      q_Nat_q'View x)
    _ _ _ _ _ _ _ _ _
               n               q_Nat_q                Ts             x
    (JMeq_refl n) (JMeq_refl (@q_Nat_q n)) (JMeq_refl Ts) (JMeq_refl x));
unfold q_Nat_q in *;
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i' =>
      S n0 == n0' -> q_sum_q q_one_q vz == S' -> T'; q_mu_q (q_sum_q q_one_q vz) == Ts' -> i == i' ->
      q_Nat_q'View (miso i))
    _ _ _ _ _ _ _ _ _
    (S n0) (q_sum_q q_one_q vz) (T'; q_mu_q (q_sum_q q_one_q vz)) i
    (JMeq_refl (S n0)) (JMeq_refl (q_sum_q q_one_q vz)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i));
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> q_one_q == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inl i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) q_one_q (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl (q_one_q)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize.

exact isO.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> vz == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inr i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) vz (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl vz) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize;
intros _.

exact (isS i).

Defined.

Semigroup/Group proof

2008-10-06T11:05:00.001-07:00


Definition associativity (T : Set) (o : T -> T -> T) :=
  forall x y z, (o (o x y) z) = (o x (o y z)).

Record Semigroup : Type := makeSemigroup {
  T : Set;
  o : T -> T -> T;
  assoc : associativity T o
}.

Record Group : Type := makeGroup {
  T' : Set;
  o' : T' -> T' -> T';
  assoc' : associativity T' o';
  I : T';
  unit' : forall u : T', exists v, o' u v = I
}.

(* Any semigroup S with a right unit, and right inverse forall a in
   S is a group *)

Theorem ex10
  (S : Semigroup)
  (right_unit : T S)
  (right_unit_meaning : forall a, (o S) a right_unit = a)
  (right_inverse : forall a, exists b, (o S) a b = right_unit)
: (* --------------------------------------------------------- *)
  exists I : T S,
    forall u : T S, exists v, (o S) u v = I.

intros.
exists right_unit.

intro.

destruct (right_inverse u).
exists x.

assumption.
Qed.