every-bit-counts (empty) → 0.1
raw patch · 25 files changed
+4436/−0 lines, 25 filesdep +basedep +haskell98setup-changed
Dependencies added: base, haskell98
Files
- BadGames.hs +37/−0
- BasicGames.hs +128/−0
- BasicGames.v +741/−0
- Combinators.v +360/−0
- FilterGames.hs +138/−0
- Games.hs +81/−0
- Games.v +665/−0
- Huffman.hs +76/−0
- Iso.hs +127/−0
- Iso.v +414/−0
- LICENSE +30/−0
- Main.hs +18/−0
- NatGames.hs +57/−0
- PBasicGames.hs +291/−0
- PGames.hs +162/−0
- PSTLC.hs +152/−0
- PTLC.hs +247/−0
- PolyLet.hs +253/−0
- README +24/−0
- STLC.hs +149/−0
- SetGames.hs +124/−0
- Setup.hs +2/−0
- UTLC.hs +37/−0
- colist.v +43/−0
- every-bit-counts.cabal +80/−0
+ BadGames.hs view
@@ -0,0 +1,37 @@+{-# options_ghc -XEmptyDataDecls -XOverlappingInstances -XScopedTypeVariables #-} +module BadGames where + +import Data.Maybe +import Iso +import Games +import BasicGames + +-- /badBoolGame/ +-- precondition: t is uninhabited +voidGame :: Game t +voidGame = Split (splitIso (const True)) voidGame voidGame + +badBoolGame :: Game Bool +badBoolGame = Split (splitIso id) + (Split (splitIso id) (constGame True) voidGame) + (Split (splitIso id) voidGame (constGame False)) +-- /End/ + +-- /badNatGame/ +badNatGame :: Game Nat +badNatGame = Split parityIso badNatGame badNatGame +-- /End/ + +{- +badBoolGame2 :: Game Bool +badBoolGame2 = Split (splitIso id) + (Split (Iso (\x -> if x then Left () else Right ()) (const True)) unitGame unitGame) + (Split (Iso (\x -> if x then Left () else Right ()) (const False)) unitGame unitGame) +-} + +badBoolGame3 :: Game Bool +badBoolGame3 = Split boolIso + (Split (Iso (const (Left ())) (const ())) unitGame unitGame) + (Split (Iso (const (Right())) (const ())) unitGame unitGame) + +
+ BasicGames.hs view
@@ -0,0 +1,128 @@+{-# options_ghc -XEmptyDataDecls #-} +module BasicGames where + +import Data.Maybe +import Iso +import Games +import List + +-- /unitGame/ +unitGame :: Game () +unitGame = Single (Iso id id) +-- /End/ + +-- /boolGame/ +boolGame :: Game Bool +boolGame = Split boolIso unitGame unitGame +-- /End/ + +-- /constGame/ +constGame :: t -> Game t +-- forall (k:t), Game { x | x=k } +constGame k = Single (singleIso k) +-- /End/ + +-- /geNatGame/ +geNatGame :: Nat -> Game Nat +-- forall k:nat, Game { x | x >= k } +geNatGame k = Split (splitIso ((==) k)) + (Single (singleIso k)) + (geNatGame (k+1)) +-- /End/ + +-- /unaryNatGame/ +unaryNatGame :: Game Nat +unaryNatGame = Split succIso unitGame unaryNatGame +-- /End/ + +-- /encUnaryNat/ +encUnaryNat x = case x of 0 -> I : [] + n+1 -> O : encUnaryNat n +-- /End/ + +-- /rangeGame/ +rangeGame :: Nat -> Nat -> Game Nat +-- forall m n : nat, Game { x | m <= x && x <= n } +rangeGame m n | m == n = Single (singleIso m) +rangeGame m n = Split (splitIso (\x -> x > mid)) + (rangeGame (mid+1) n) + (rangeGame m mid) + where mid = (m + n) `div` 2 +-- /End/ + +-- /binNatGame/ +binNatGame :: Game Nat +binNatGame = Split succIso unitGame + (Split parityIso binNatGame binNatGame) +-- /End/ + +-- Flip the meaning of the bits +flipGame :: Game a -> Game a +flipGame (Split iso g1 g2) = Split (iso `seqI` swapSumI) (flipGame g2) (flipGame g1) +flipGame g = g + +-- A game for sums +-- /sumGame/ +sumGame :: Game t -> Game s -> Game (Either t s) +sumGame = Split idI +-- /End/ + + +-- A game for products, based on appending +-- /prodGame/ +prodGame :: Game t -> Game s -> Game (t,s) +prodGame (Single iso) g2 = + g2 +> prodI iso idI `seqI` prodLUnitI +prodGame (Split iso g1a g1b) g2 = + Split (prodI iso idI `seqI` prodLSumI) + (prodGame g1a g2) + (prodGame g1b g2) +-- /End/ + + +-- A game for products, based on interleaving +-- /ilGame/ +ilGame :: Game t -> Game s -> Game (t,s) +ilGame (Single iso) g2 = + g2 +> prodI iso idI `seqI` prodLUnitI +ilGame (Split iso g1a g1b) g2 = + Split (swapProdI `seqI` prodI idI iso `seqI` prodRSumI) + (ilGame g2 g1a) + (ilGame g2 g1b) +-- /End/ + + +-- Dependent composition +-- /depGame/ +depGame :: Game t -> (t -> Game s) -> Game (t,s) +-- Game t -> (forall x:t, Game(s x)) -> Game {x:t & s x} +depGame (Single iso) f = + f (from iso ()) +> prodI iso idI `seqI` prodLUnitI +depGame (Split iso g1a g1b) f + = Split (prodI iso idI `seqI` prodLSumI) + (depGame g1a (f . from iso . Left)) + (depGame g1b (f . from iso . Right)) +-- /End/ + + +-- A game for lists, using sum-of-products +-- /listGame/ +listGame :: Game t -> Game [t] +listGame g = + Split listIso unitGame (prodGame g (listGame g)) +-- /End/ + +nonemptyIso = Iso (\(x:xs) -> (x,xs)) (\(x,xs) -> x:xs) + +-- /vecGame/ +vecGame :: Game t -> Nat -> Game [t] +-- Game t -> forall n:nat, Game t^n +-- /End/ +vecGame g 0 = constGame [] +vecGame g (n+1) = prodGame g (vecGame g n) +> nonemptyIso + +-- /listGameAux/ +listGame' :: Game t -> Game [t] +listGame' g = depGame binNatGame (vecGame g) + +> depListIso +-- /End/
+ BasicGames.v view
@@ -0,0 +1,741 @@+(*====================================================================================== + Games for basic types, and type constructors + ======================================================================================*) +Require Import List. + +Set Implicit Arguments. +Unset Strict Implicit. +Set Printing Implicit Defensive. +Set Transparent Obligations. + +Require Import colist. +Require Import Iso. +Require Import Games. + +(*====================================================================================== + The unit game + ======================================================================================*) +Definition unitGame : Game unit := Single (idI unit). + +Lemma unitGameIsTotal : TotalGame unitGame. apply singletonGameIsTotal. Qed. +Lemma unitGameIsProper : ProperGame unitGame. apply singletonGameIsProper. Qed. +Lemma unitGameIsProductive : ProductiveGame unitGame. apply (TotalAndProperImpliesProductive unitGameIsTotal unitGameIsProper). Qed. + +(*====================================================================================== + The void game + ======================================================================================*) +Program CoFixpoint voidGame : Game Void := + Split (Iso (fun x => inr _ x) (fun x => match x with inl x => x | inr x => x end) (Void_rect _) _) voidGame voidGame. +Next Obligation. +destruct y. destruct v. reflexivity. +Defined. + +(* Vacuously true! *) +Lemma voidGameIsTotal : TotalGame voidGame. +unfold TotalGame. intros. destruct x. +Qed. + +CoFixpoint boolGame : Game bool := + Split boolIso unitGame unitGame. + +Definition rightVoidIso : ISO unit (Void + unit). +refine (Iso (fun x => inr _ tt) (fun x => tt) _ _). +destruct x. auto. +destruct y. inversion v. destruct u. auto. +Defined. + +Definition leftVoidIso : ISO unit (unit + Void). +refine (Iso (fun x => inl _ tt) (fun x => tt) _ _). +destruct x. auto. +destruct y. destruct u. auto. inversion v. +Defined. + +CoFixpoint badBoolGame : Game bool := Split boolIso (Split leftVoidIso unitGame voidGame) (Split rightVoidIso voidGame unitGame). + +Definition constGame t (x:t) := Single (singleIso x). + +(*====================================================================================== + Given games for a and b, construct a game for a+b + ======================================================================================*) +(*=sumGame *) +Definition sumGame a b : + Game a -> Game b -> Game (a+b) := Split (idI _). +(*=End *) + +Lemma sumGamePreservesTotality a b (g1 : Game a) (g2 : Game b) : TotalGame g1 -> TotalGame g2 -> TotalGame (sumGame g1 g2). +Proof. +intros a b g1 g2 T1 T2. apply (splitPreservesTotality _ T1 T2). +Qed. + +Lemma sumGamePreservesProper a b (g1 : Game a) (g2 : Game b) : ProperGame g1 -> ProperGame g2 -> ProperGame (sumGame g1 g2). +Proof. +intros a b g1 g2 P1 P2. apply (splitPreservesProper P1 P2). +Qed. + +(* +Definition NonProperGame t (g : Game t) := sumGame VoidGame g. +Check NonProperGame. +Program CoFixpoint NonProperGame t : Game t := + Split (@Build_Iso t (t+Void) (fun x => inl x) (fun x => match x with inl x => x | _ => ! end) _ _) (NonProperGame t) VoidGame. +Next Obligation. +destruct x. specialize (H t0). apply H. reflexivity. destruct v. Defined. +Next Obligation. +destruct y. reflexivity. destruct v. Defined. +*) + +(*====================================================================================== + Given a game for a and an isomorphism between a and b, construct a game for a+b + ======================================================================================*) +(*=coerceGame *) +Definition coerceGame a b (g : Game a) + (iso : ISO b a) : Game b := + match g with + | Single i => Single (seqI iso i) + | Split _ _ i g1 g2 => Split (seqI iso i) g1 g2 + end. +Notation "g '+>' i" := (coerceGame g i) (at level 40). +(*=End *) + + +Lemma coerceGamePreservesProper a b (iso : ISO b a) (g : Game a) : ProperGame g -> ProperGame (g +> iso). +Proof. +intros a b iso g P. +destruct g. simpl. apply singletonGameIsProper. +simpl. destruct (ProperOfSplit P) as [P1 P2]. apply splitPreservesProper. apply P1. apply P2. +Qed. + +Require Import Program.Equality. +Lemma coerceGamePreservesTotality a b (iso : ISO b a) g : TotalGame g -> TotalGame (g +> iso). +Proof. +intros a b iso g P. unfold TotalGame in *. unfold coerceGame. +intros. destruct g. +(* Single *) +rewrite (uniqueSingleton (seqI iso i)). apply HasFinPathSing. +(* Split *) +specialize (P (iso x)). rewrite <- (mapinv iso x). +dependent destruction P. +admit. (* +(* Left *) +assert (SS : inv iso (iso x) = inv (seqI iso i) (inl _ x1)). simpl. congruence. rewrite SS. apply HasFinPathLeft. apply P. *) +admit. (* +(* Right *) +assert (SS : inv iso (iso x) = inv (seqI iso i) (inr _ x2)). simpl. congruence. rewrite SS. apply HasFinPathRight. apply P. *) +Qed. + + +(*====================================================================================== + Flip the meaning of the bits + ======================================================================================*) +CoFixpoint flipGame a (g : Game a) : Game a := + match g with + | Split _ _ iso g1 g2 => Split (seqI iso (swapSumI _ _)) (flipGame g2) (flipGame g1) + | _ => g + end. + +(*====================================================================================== + Given games for a and b, construct a game for a*b, first playing the game for a + then playing the game for b at the leaves. The resulting encoding appends codes for the + two games. + ======================================================================================*) +(*=prodGame *) +CoFixpoint prodGame a b (g1 : Game a) (g2 : Game b) + : Game (a*b) := + match g1 with + | Single iso => + g2 +> seqI (prodR _ iso) (prodLUnitI _) + | Split _ _ iso g1a g1b => + Split (seqI (prodR _ iso) (prodLSumI _ _ _)) + (prodGame g1a g2) (prodGame g1b g2) + end. +(*=End *) + + +(*Definition coerceSingle a B (x:a) (g : Game (B x)) : Game {x:a & B x}. +intros. +refine (coerceGame g _). +refine (Iso (fun z => match z with existT x0 Bx0 => Bx0 end) (fun Bx0 => existT _ x Bx0) _ _). +*) + +(* +Program CoFixpoint depProdGame a B (g1 : Game a) : (forall (x:a), Game (B x)) -> Game {x:a & B x } := + match g1 with + | Single iso => fun (g2 : forall (x:a), Game (B x)) => g2 (inv iso tt) +> _ (* seqI (depProdI iso _) (depProdLUnitI _) *) + | Split aa ab iso g1a g1b => fun g2 => Split _ (* (seqI (depProdI (idI _) iso) _ (*(depProdLSumI _ _ _) *)) *) + (depProdGame g1a (fun x => g2 (inv iso (inl _ x)))) + (depProdGame g1b (fun x => g2 (inv iso (inr _ x)))) + end. +Next Obligation. +assert (H1 := uniqueSingleton iso). +refine (Iso (fun z => match z with existT x Bx => _ end) (fun z => existT _ z _) _ _). +apply depProdI. +refine (Iso (fun _ => tt) (fun _ => existT _ (inv iso tt) _) _ _). +intros [x Bx]. assert (H1 := uniqueSingleton iso x). unfold getSingleton in H1. +subst. +assert (H2 := uniqueSingleton iso' Bx). unfold getSingleton in H2. subst. auto. +intros y. destruct y. reflexivity. +Defined. +Next Obligation. +*) + + +Lemma prod_Single a b (iso : ISO a unit) (g2 : Game b) : prodGame (Single iso) g2 = g2 +> seqI (prodR _ iso) (prodLUnitI _). +Proof. intros. apply (trans_equal (decomp_game_thm _)). destruct g2; auto. +Qed. + +Lemma prod_Split a a1 a2 b (iso : ISO a (a1+a2)) g1a g1b (g2 : Game b) : prodGame (Split iso g1a g1b) g2 = Split (seqI (prodR _ iso) (prodLSumI _ _ _)) (prodGame g1a g2) (prodGame g1b g2). +Proof. intros. apply (trans_equal (decomp_game_thm _)). destruct g2; auto. +Qed. + +Lemma prodPreservesTotality a b (g1 : Game a) (g2 : Game b) : TotalGame g1 -> TotalGame g2 -> TotalGame (prodGame g1 g2). +intros a b g1 g2 T1 T2. +intros [x1 x2]. +assert (T1' := T1 x1). +induction T1'. +(* HasFinPathSing *) +rewrite prod_Single. apply coerceGamePreservesTotality. assumption. +(* HasFinPathLeft *) +rewrite prod_Split. +destruct (TotalOfSplit T1) as [T1a _]. +assert (R : (inv (seqI (prodR b iso) (prodLSumI a b0 b)) (inl _ (x1, x2))) = (inv iso (inl _ x1), x2)) by auto. +rewrite <- R. +apply HasFinPathLeft. +auto. +(* HasFinPathRight *) +rewrite prod_Split. +destruct (TotalOfSplit T1) as [_ T1b]. +assert (R : (inv (seqI (prodR b iso) (prodLSumI a b0 b)) (inr _ (x0, x2))) = (inv iso (inr _ x0), x2)) by auto. +rewrite <- R. +apply HasFinPathRight. +auto. +Qed. + +Lemma ProperImpliesInhabited a (g : Game a) : ProperGame g -> Inhabited a. +intros. unfold ProperGame, Everywhere in H. apply (H a g (InsideSame _)). +Qed. + +(* +Lemma coerceSplitInversion : forall t a b (g : Game t) (g1 : Game a) (g2 : Game b) (iso' : ISO _ _) (iso : ISO _ _), + coerceGame iso g = Split iso' g1 g2 -> + g = Split (seqIso (invIso iso) iso') g1 g2. +intros. destruct g. auto. +*) + +(* +Lemma prodPreservesProper a b (g1 : Game a) (g2 : Game b) : ProperGame g1 -> ProperGame g2 -> ProperGame (prod g1 g2). +Proof. +intros a b ga gb Pa Pb. +unfold ProperGame, Everywhere. +intros t g IN. +dependent induction IN. + destruct (ProperImpliesInhabited Pa) as [xa _]. + destruct (ProperImpliesInhabited Pb) as [xb _]. + exists (xa,xb). trivial. + destruct ga. + rewrite prod_Single in H. dependent destruction H. destruct gb. simpl in H. inversion H. simpl in H. dependent destruction H. +destruct (ProperOfSplit Pb). +apply IHIN. +*) + +CoFixpoint ilGame a b (g1 : Game a) (g2 : Game b) : Game (a*b) := + match g1 with + | Single iso => g2 +> seqI (prodR _ iso) (prodLUnitI _) + | Split _ _ iso g1a g1b => + Split (seqI (swapProdI _ _) (seqI (prodL _ iso) (prodRSumI _ _ _))) (ilGame g2 g1a) (ilGame g2 g1b) + end. + + +Lemma interleave_Single a b (iso : ISO a unit) (g2 : Game b) : ilGame (Single iso) g2 = g2 +> seqI (prodR _ iso) (prodLUnitI _). +Proof. intros. apply (trans_equal (decomp_game_thm _)). destruct g2; auto. +Qed. + +Lemma interleave_Split a a1 a2 b (iso : ISO a (a1+a2)) g1a g1b (g2 : Game b) : ilGame (Split iso g1a g1b) g2 = Split (seqI (swapProdI _ _) (seqI (prodL _ iso) (prodRSumI _ _ _))) + (ilGame g2 g1a) (ilGame g2 g1b). +Proof. intros. apply (trans_equal (decomp_game_thm _)). destruct g2; auto. +Qed. + +Definition splitIso t (p : t -> bool) : ISO t ({ x | p x = true } + { x | p x = false }). Admitted. +Check neq. +Require Import EqNat. +Check eq_nat. nat_eq. +Program CoFixpoint geNatGame k : Game { x | x>=k } := Split (splitIso (fun k1 => (Single _) (geNatGame (S k)). +induction k. refine (Split _ (Single _) _). + +(* +Lemma interleavePreservesTotality a b (g1 : Game a) (g2 : Game b) : TotalGame g1 -> TotalGame g2 -> forall x1 x2, HasFinPath (interleave g1 g2) (x1,x2) /\ HasFinPath (interleave g2 g1) (x2,x1). +intros a b g1 g2 T1 T2. +intros x1 x2. +assert (T1' := T1 x1). +induction T1'. +(* HasFinPathSing *) +split. +rewrite interleave_Single. apply coerceGamePreservesTotality. assumption. +rewrite interleave_SingleR. apply coerceGamePreservesTotality. assumption. +(* HasFinPathLeft *) +rewrite interleave_Split. +destruct (TotalSplit T1) as [T1a _]. + +assert (R : (seqIso (swap t b) (seqIso (prodL b iso) (prodSumR b a b0)) (inl _ (x1, x2))) = (inv iso (inl _ x1), x2)) by auto. +rewrite <- R. +apply HasFinPathLeft. +auto. +(* HasFinPathRight *) +rewrite prod_Split. +destruct (TotalSplit T1) as [_ T1b]. +assert (R : (inv (seqIso (prodR b iso) (ProdSumL a b0 b)) (inr _ (x0, x2))) = (inv iso (inr _ x0), x2)) by auto. +rewrite <- R. +apply HasFinPathRight. +auto. +Qed. + +*) + +(* +Lemma interleavePreservesTotality a (g1 : Game a) : TotalGame g1 -> forall b (g2 : Game b), TotalGame g2 -> TotalGame (interleave g1 g2) /\ TotalGame (interleave g2 g1). +intros a g1 T1. +unfold TotalGame in T1. +intros b g2 T2. +split. +intros [x1 x2]. +generalize x1 x2. +specialize (T1 x1). +induction T1. +(* HasFinPathSing *) +intros. rewrite interleave_Single. apply coerceGamePreservesTotality. assumption. +(* HasFinPathLeft *) +intros. rewrite interleave_Split. apply splitPreservesTotality. unfold TotalGame. intros [y1 y2]. apply IHT1. intros [z1 z2]. apply IHT1. apply HasFinPathLeft. simpl. +*) + + +(*Program CoFixpoint balanceGame t (g : Game t) : Game t := + match g with + | Split a b iso1 (Split c d iso2 g1 g2) g3 => + @Split t c (d+b) _ (balanceGame g1) (@Split _ d b _ (balanceGame g2) (balanceGame g3)) + | _ => g + end. +Next Obligation. +assert (ISO (c + (d + b)) ((c + d) + b)). +apply assocChoice. +assert (ISO (a + b) (c + d + b)). +apply sum. apply iso2. apply idIso. +apply (seqIso iso1). apply (seqIso X0 (invIso X)). +Defined. +Next Obligation. apply idIso. Defined. +*) + +Inductive HasFinPathDec : forall t, Game t -> t -> Prop := + | HasFinPathDecSing : forall t (iso : ISO t unit) , HasFinPathDec (Single iso) (getSingleton iso) + | HasFinPathDecLeft : forall (t a b : Type) (g1 : Game a) (g2 : Game b) (iso : ISO t _) x1, + HasFinPathDec g1 x1 -> + HasFinPathDec (Split iso g1 g2) (inv iso (inl _ x1)) + | HasFinPathDecRight : forall (t a b : Type) (g1 : Game a) (g2 : Game b) (iso : ISO t _) x2, + HasFinPathDec g2 x2 -> + HasFinPathDec (Split iso g1 g2) (inv iso (inr _ x2)). + +(*====================================================================================== + Unary representation of nats + ======================================================================================*) +Definition singleIso t (k:t) : ISO { x | x=k } unit. +intros t k. +refine (Iso (fun _ => tt) (fun _ => exist _ k eq_refl) _ _). + +intros. destruct x as [x H]. subst. auto. +destruct y. auto. +Defined. + +(*Require Import EqNat. +Definition irrelIso t (P Q : t -> Prop) : + (forall x, P x <-> Q x) -> { x | P x } = { x | Q x}. +Proof. +intros t P Q H. +Check UIP. +refine (Iso (fun s:{x | P x} => exist Q (proj1_sig s) (proj1 (H (proj1_sig s)) (proj2_sig s)) : {x | Q x}) _ _ _). intros. destruct x. simpl. rewrite H in e. (fun p => exist _ (projT1 p) (projT2 p)) _ _ _). +CoFixpoint geNatGame k : Game { x | x >= k } := + Split (splitIso (beq_nat k)) + (Single (singleIso k)) + (geNatGame (k+1)). +*) + +CoFixpoint unaryNatGame : Game nat := Split succIso unitGame unaryNatGame. + +Fixpoint encUnNat n := + match n with + | O => true::nil + | S n => false::encUnNat n + end. + +Lemma encUnNatEquiv : forall n, encProduces unaryNatGame n (encUnNat n). +Proof. +induction n; simpl; unfold encProduces. +rewrite (decomp_colist_thm _). simpl. apply FinCoListCons. +rewrite (decomp_colist_thm _). apply FinCoListNil. + +rewrite (decomp_colist_thm _). +simpl. apply FinCoListCons. auto. +Qed. + +(*====================================================================================== + Log representation of nats + ======================================================================================*) +CoFixpoint binNatGame : Game nat := + Split succIso unitGame (Split parityIso binNatGame binNatGame). + +CoFixpoint badLogNatGame : Game nat := + Split parityIso binNatGame binNatGame. + +(*====================================================================================== + Diff functions used for representations of sets and multisets + ======================================================================================*) +Fixpoint diff' t (d : t -> t -> t) b xs := + match xs with + nil => nil + | x::xs => d b x :: diff' d x xs + end. + +Definition diff t (d : t -> t -> t) xs := + match xs with + | nil => nil + | x::xs => x :: diff' d x xs + end. + +Fixpoint undiff' t (a : t -> t -> t) b xs := + match xs with + nil => nil + | x::xs => a b x :: undiff' a (a b x) xs + end. + +Definition undiff t (a : t -> t -> t) xs := + match xs with + | nil => nil + | x::xs => x :: undiff' a x xs + end. + +Definition exL := diff (fun x => fun y => minus y x) (2::4::5::nil). + +Require Import Sorting. + +Lemma undiff'Le : forall xs x, lelistA le x (undiff' plus x xs). +Proof. +induction xs; intros. +apply nil_leA. +apply cons_leA. intuition. +Qed. + +Lemma undiff'Sorted : forall xs x, sort le (undiff' plus x xs). +Proof. +induction xs; intros. +apply nil_sort. +apply cons_sort. auto. fold undiff'. +apply undiff'Le. +Qed. + +Lemma undiffSorted : forall xs, sort le (undiff plus xs). +Proof. +destruct xs. apply nil_sort. apply cons_sort. apply undiff'Sorted. apply undiff'Le. +Qed. + +Lemma undiffDiff' : forall xs x, diff' (fun x y : nat => y - x) x (undiff' plus x xs) = xs. +Proof. +induction xs. +auto. +intros. +simpl. +rewrite IHxs. rewrite Minus.minus_plus. reflexivity. +Qed. + +Lemma undiffDiff : forall xs, diff (fun x y : nat => y - x) (undiff plus xs) = xs. +Proof. +destruct xs. auto. simpl. rewrite undiffDiff'. reflexivity. +Qed. + +Lemma diffUndiff' : forall xs x, sort le (x::xs) -> undiff' plus x (diff' (fun x y => y - x) x xs) = xs. +Proof. +induction xs. auto. +intros. +inversion H. subst. specialize (IHxs _ H2). +simpl. inversion H3. rewrite <- (Minus.le_plus_minus _ _ H1). rewrite IHxs. reflexivity. +Qed. + +Lemma diffUndiff : forall xs, sort le xs -> undiff plus (diff (fun x y => y - x) xs) = xs. +Proof. +destruct xs; auto. +intros. simpl. rewrite (diffUndiff' H). reflexivity. +Qed. + +Definition multisetIso : ISO (list nat) { x:list nat & sort le x } := + @subsetIso _ _ _ _ undiffSorted _ undiffDiff diffUndiff. + +(*====================================================================================== + Finite lists + ======================================================================================*) +(*Program Fixpoint finListGame (t : Type) (g : Game t) (n : nat) : Game {l : list t | length l = n } := + match n with + | 0 => Single (Iso (fun _ => tt) (fun _ => existT _ nil _) _ _) + | S n0 => prodGame g (finListGame g n0) +> (Iso _ _ _ _) + end. +Next Obligation. destruct x; dependent destruction H; auto. Defined. +Next Obligation. destruct y. reflexivity. Defined. +Next Obligation. dependent destruction H. inversion H. destruct H. refine (existT _ (t0::s) _). auto. Defined. +Next Obligation. destruct X. discriminate H. dependent destruction H. refine (t0, _). refine (existT _ X _). reflexivity. Defined. +Next Obligation. dependent destruction Heq_n. dependent destruction H. auto. Defined. +Next Obligation. dependent destruction Heq_n. destruct y. discriminate H. dependent destruction H. auto. Defined. +*) + +(*====================================================================================== + N-ary products + ======================================================================================*) +Require Import NaryFunctions. +Fixpoint naryGame t (g : Game t) (n : nat ) : Game (t ^ n) := + match n with + | O => unitGame + | S n => prodGame g (naryGame g n) + end. + +Lemma nprod_to_list_dom t n : forall (x:t^n), length (nprod_to_list t n x) = n. +Proof. +induction n. +auto. simpl. intros. destruct x. simpl. rewrite IHn. reflexivity. +Qed. + +Fixpoint list_to_nprod t (x:list t) : t ^ length x := + match x with + | nil => tt + | x::xs => (x, list_to_nprod xs) + end. + +Definition list_to_nprod_aux t n (x:list t) (P : length x = n) : t ^ n. +intros. rewrite <- P. exact (list_to_nprod x). +Defined. + +Definition finListIso t n : ISO (t ^ n) {l:list t & length l = n}. +intros t n. +refine (@subsetIso (t^n) (list t) (fun x => length x = n) (nprod_to_list _ _) (@nprod_to_list_dom _ _) (@list_to_nprod_aux _ _) _ _). + +induction n. simpl. intros. destruct x. unfold list_to_nprod_aux. simpl. admit. +simpl. intros [x xs]. admit. + +induction n. intros. simpl. destruct y. reflexivity. simpl in p. inversion p. +intros. simpl. destruct y. inversion p. dependent destruction p. simpl in *. specialize (IHn y (refl_equal _)). simpl in IHn. rewrite IHn. reflexivity. +Defined. + + +(* +(* The unary encoding of nat asks non trivial questions *) +Lemma ntp_unNatGame : CNonTrivialPart unNatGame. +Proof. cofix H. +rewrite decomp_game_thm. simpl. +apply CNTPPart. apply CNTPSing. apply H. +eapply ex_intro. exact tt. auto. +eapply ex_intro. apply 0. auto. +Qed. +*) + +(* The unary encoding of nat is complete *) +(* +Lemma co_unNatGame : CComplete unNatGame. +Proof. cofix H. +rewrite decomp_game_thm. simpl. +eapply CompletePart. +Focus 6. exists 0. auto. Unfocus. +Focus 5. eapply ex_intro. exists 0. reflexivity. auto. Unfocus. +Focus 4. intro n. +induction n. +rewrite decomp_game_thm with (g := unNatGame). simpl. +set (emb1 :=fun x : SingT 0 => `x). +replace 0 with (emb1 (exist _ 0 (refl_equal _))). +simpl. admit. + +eapply HasFinPathLeft. +apply HasFinPathSing. compute. reflexivity. +admit. +admit. +rewrite decomp_game_thm with (g := unNatGame). simpl. +set (emb2 := fun x => S x). +replace (S n) with (emb2 n). +apply HasFinPathRight. apply IHn. +auto. Unfocus. +apply CompleteSing. apply H. +intros. simpl. compute. compute. +destruct x. destruct x. dependent destruction e. +apply HasFinPathSing. discriminate e. +Qed. +*) + + +(***************************************************************************** + * Range natural number game * + *****************************************************************************) + +(* Another model of integers based on range: [k1,k2] *) + +Definition Range k1 k2 := {n : nat | k1 <= n <= k2 }. +Notation "'[' a '...' b ']'" := (Range a b) (at level 90). + +Require Import Le. +Require Import Compare_dec. +Require Import Plus. + +Definition ask_dich: forall k1 k2 (prf : k1 < k2), Range k1 k2 -> Range k1 (div2 (k1+k2)) + Range (1+div2 (k1+k2)) k2. +intros k1 k2. intro prf. intro x. +destruct x. destruct (le_le_S_dec x (div2 (k1 + k2))). + left. exists x. split. destruct a. assumption. assumption. + right. exists x. split. assumption. destruct a. assumption. +Defined. + +Lemma div2_succ : forall k, div2 k <= div2 (k+1). +Proof. +intro k. apply ind_0_1_SS with (n := k). +compute. auto. +compute. auto. +intros. + assert (n + 1 = S n). rewrite plus_comm. auto. rewrite H0 in *. clear H0. + assert (S (S n) + 1 = S (S (S n))). rewrite plus_comm. auto. rewrite H0. clear H0. + simpl. simpl in H. destruct n. compute. auto. apply le_n_S. auto. +Qed. + +Lemma div2_monotone : forall k1 k2, k1 <= k2 -> div2 k1 <= div2 k2. +intros k1 k2 geq. +assert (exists m, k2 = k1 + m). induction k2. exists 0. inversion geq. auto. +Require Import Omega. +assert (k1 = S k2 \/ k1 <= k2) by omega. +destruct H. subst k1. exists 0. auto. +destruct (IHk2 H). exists (S x). omega. +destruct H. subst k2. +induction x. assert (k1 + 0 = k1) by auto. rewrite H. auto. +assert (k1 + S x = S (k1 + x)) by auto. rewrite H in *. clear H. +eapply le_trans. apply IHx. omega. +assert (S (k1 + x) = (k1 + x) + 1) by omega. rewrite H. +apply div2_succ. +Qed. + +Lemma div2_zero_k: forall k, 0 < k -> S (div2 k) <= k. +intro k. apply ind_0_1_SS with (n := k). +intros. compute. auto. +intros. compute. auto. +intros. simpl. +apply le_n_S. apply le_n_S. +destruct n. compute. auto. +assert (div2 (S n) < S n). apply lt_div2. auto with arith. +auto with arith. +Qed. + +Lemma div2_range : forall k1 k2, k1 < k2 -> S (div2 (k1 + k2)) <= k2. +intros k1. induction k1. intros k2. +assert (0 + k2 = k2) by auto. rewrite H. +clear H. intros. apply div2_zero_k. assumption. +intros. +assert (exists l2, k2 = S l2). destruct k2. inversion H. exists k2. reflexivity. +destruct H0. subst k2. +assert (S k1 + S x = S (S (k1 + x))) by omega. rewrite H0. clear H0. simpl. +apply le_n_S. apply IHk1. auto with arith. +Qed. + +Program Definition ask_emb1 k1 k2 (prf : k1 <= k2) (x : Range k1 (div2 (k1+k2))) : Range k1 k2 := x. +Next Obligation. + destruct x. simpl. destruct a. split. assumption. + assert (div2 (k1 + k2) <= div2 (k2 + k2)). + apply div2_monotone. + apply plus_le_compat_r. apply prf. + assert (k2 + k2 = 2*k2) by omega. rewrite H2 in H1. + rewrite div2_double in H1. eapply le_trans. apply H0. apply H1. +Qed. + +(* +Program Definition ask_emb2 k1 k2 (prf : k1 <= k2) (x : Range (S (div2 (k1+k2))) k2) : Range k1 k2 := x. +Next Obligation. + destruct x. simpl. destruct a. split. + destruct (le_le_S_eq _ _ H). + Focus 2. + subst x. + assert (k1 + k2 <= 2*k2). omega. + assert (k1 <= div2 (2*k1)). rewrite div2_double. auto. + assert (div2 (2*k1) <= div2 (k1 + k2)). apply div2_monotone. omega. + omega. + Unfocus. + assert (k1 = div2 (2*k1)). rewrite div2_double. reflexivity. + assert (div2 (2*k1) <= div2 (k1 + k2)). apply div2_monotone. omega. + omega. assumption. +Qed. + +Lemma proof_irrelevant_existential: forall (t:Type) P (x : t) prf1 prf2, exist P x prf1 = exist P x prf2. +Proof. +intros. assert (prf1 = prf2). apply proof_irrelevance. subst prf1. reflexivity. +Qed. + + +Definition mkNatRangeGame: forall (k1 : nat) (k2 : nat), + (k1 <= k2) -> Game (Range k1 k2). +Proof. cofix mkIntLogModel. +intros k1 k2 prf. +destruct (eq_nat_dec k1 k2). + (* k1 = k2 *) + subst k1. apply Single. admit. (*exists k2. split. omega. omega. + unfold Sing. intros. destruct x. destruct y. + assert (x = k2). destruct a. apply le_antisym. omega. omega. subst x. + assert (x0= k2). destruct a0. apply le_antisym. omega. omega. subst x0. + assert (a = a0). apply proof_irrelevance. subst a. reflexivity.*) + (* k1 <> k2 *) + assert (k1 < k2) as ineq by omega. + eapply Split with (iso := Build_Iso @ask_dich k1 k2 ineq) + (emb1 := @ask_emb1 k1 k2 prf) + (emb2 := @ask_emb2 k1 k2 prf). + Focus 2. apply mkIntLogModel. + assert (div2 (2*k1) <= div2 (k1 + k2)). apply div2_monotone. omega. + rewrite div2_double in H. assumption. Unfocus. + Focus 2. apply mkIntLogModel. clear prf. clear n. + apply div2_range. assumption. Unfocus. + + unfold SEmbed. intros. destruct x. + split. intros. split. intros. + unfold ask_dich in H. + destruct (le_le_S_dec x (div2 (k1 + k2))). revert H. case a. + intros. inversion H. unfold ask_emb1. simpl. + apply proof_irrelevant_existential. + inversion H. + intros. unfold ask_dich. + destruct (le_le_S_dec x (div2 (k1+k2))). + compute in H. revert H. dependent destruction a. + intros. dependent destruction x1. case a. intros. + erewrite proof_irrelevant_existential. reflexivity. + destruct x1. + assert False as Absurd. + compute in H. inversion H. subst x0. omega. + destruct Absurd. + intros. split. intros. + destruct x2. revert H. case a. + intros. simpl in H. + destruct (le_le_S_dec x (div2 (k1 + k2))). intros. + inversion H. inversion H. subst x. unfold ask_emb2. simpl. + apply proof_irrelevant_existential. + intros. + destruct x2. unfold ask_emb2 in H. simpl in H. inversion H. subst x0. + unfold ask_dich. destruct (le_le_S_dec x (div2 (k1 +k2))). + assert False as Absurd. clear H. omega. destruct Absurd. + erewrite proof_irrelevant_existential. reflexivity. +Defined. + +Program Definition natRangeGame : Game { n : nat | 0 <= n <= 255} := mkNatRangeGame _. +Next Obligation. +omega. +Defined. +*) + +(*====================================================================================== + Weak filtering + ======================================================================================*) +(* +Program CoFixpoint filterGame (t : Type) (P : t -> bool) (m : Game t) : Game { x : t | P x = true } := + match m with + | Single iso => match (P (inv iso tt)) with + | true => Single _ + | false => coerceGame _ voidGame + end + | Split _ _ iso g1 g2 => + let P1 := fun x => P (inv iso (inl x)) in + let P2 := fun x => P (inv iso (inr x)) in @Split _ _ _ (filterGame P1 g1) (filterGame P2 g2) +(* let emb1' (x : {z : t11 | P (emb1 z) = true}) : {z : t | P z = true} := emb1 x in *) +(* let emb2' (x : {z : t12 | P (emb2 z) = true}) : {z : t | P z = true} := emb2 x in *) +(* (@Partition {z : t | P z = true} {z : t11 | P (emb1 z) = true } *) +(* {z : t12 | P (emb2 z) = true } (restrict_splice sprf) emb1' emb2' _ (mkRestrictedWeak (fun z => P (emb1 z)) m11) *) +(* (mkRestrictedWeak (fun z => P (emb2 z)) m12)) *) + end. +*)
+ Combinators.v view
@@ -0,0 +1,360 @@+Require Import List. +Require Import Bool. +Require Import Arith. +Require Import Le. +Require Import Max. +Require Import Compare_dec. +(*Require Import EqNat.*) +Require Import Streams. +Require Import List. + +Require Import Program.Equality. +Require Import Eqdep_dec. + + +Require Import Iso. +Require Import Games. +(*Require Import Simple.*) + +Set Implicit Arguments. +Unset Strict Implicit. +Set Printing Implicit Defensive. +Set Transparent Obligations. + +(*Definition depIso t (A:t->Type) : Iso (forall s:t, A s) ({x:t & A x}). +intros t A. +refine (@Build_Iso (forall s:t, A s) ({x:t & A x}) (fun (x:forall s:t, A s) => existT _ _ _). +*) + +(* +Program Definition surjDepProdGame (t : Type) (A : t -> Type) (mkGame : forall s : t, Game (A s)) (g : Game t) : option (Game { x : t & A x }) := + match g with + | Singleton iso (* x sing *) => + let x := inv iso tt in + match mkGame x with + | Singleton iso' => None + | Split t1 t2 iso (*ask emb1 emb2 sprf *) g1 g2 => + let ask' (z : { x : t & A x }) : t1 + t2 := match z with existT _ ax => iso ax end in + let emb1' (z : t1) : { x : t & A x } := existT _ x (inv iso (inl _ z)) in + let emb2' (z : t2) : { x : t & A x } := existT _ x (inv iso (inr _ z)) in + Some (Split (@Build_Iso {x:t & A x} (t1+t2) ask' (fun z => match z with inl z => emb1' z | inr z => emb2' z end) _ _) g1 g2) + end + | Split _ _ _ _ _ => None + end. +Next Obligation. rewrite (uniqueSingleton iso z). auto. Defined. +Next Obligation. admit. Defined. Next Obligation. admit. Defined. +Print surjDepProdGame. Print surjDepProdGame_obligation_1. +*) + +Definition unitIsoDep (t : Type) (iso : ISO t unit) (A : t -> Type) (mkIso : forall s : t, ISO (A s) unit) : ISO { x : t & A x } unit. +intros t iso A mkIso. +refine (@Build_ISO {x:t&A x} unit (fun _ => tt) (fun _ => existT (fun x:t => A x) (inv iso tt) (inv (mkIso (inv iso tt)) tt)) _ _). +intros [x X]. assert (EQ := uniqueSingleton iso x). subst. assert (EQ := uniqueSingleton (mkIso (inv iso tt)) X). subst. auto. +intros y. destruct y. reflexivity. +Defined. + +Program CoFixpoint surjDepProdGame (t : Type) (A : t -> Type) (mkGame : forall s : t, Game (A s)) (g : Game t) : Game { x : t & A x } := + match g with + | Singleton iso => + match mkGame (inv iso tt) with + | Singleton iso' => Singleton (@Build_ISO {x:t&A x} unit (fun _ => tt) (fun _ => existT (fun x:t => A x) (inv iso tt) (inv iso' tt)) _ _) + | Split t1 t2 iso' g1 g2 => + let ask' (z : { x : t & A x }) : t1 + t2 := match z with existT _ ax => iso' ax end in + let emb1' (z : t1) : { x : t & A x } := existT _ (inv iso tt) (inv iso' (inl _ z)) in + let emb2' (z : t2) : { x : t & A x } := existT _ (inv iso tt) (inv iso' (inr _ z)) in + Split (@Build_ISO {x:t & A x} (t1+t2) ask' (fun z => match z with inl z => emb1' z | inr z => emb2' z end) _ _) g1 g2 + end + | Split t1 t2 iso g1 g2 => + let ask' (z : {x : t & A x}) : {x : t1 & A (inv iso (inl _ x)) } + + {x : t2 & A (inv iso (inr _ x)) } := + match z with + existT x ax => match iso x with + | inl x1 => inl _ (existT _ x1 ax) + | inr x2 => inr _ (existT _ x2 ax) + end + end in + let emb1' (z : {x : t1 & A (inv iso (inl _ x))}) : { x : t & A x } := match z with existT x1 ax => existT _ (inv iso (inl _ x1)) ax end in + let emb2' (z : {x : t2 & A (inv iso (inr _ x)) }) : { x : t & A x } := match z with existT x2 ax => existT _ (inv iso (inr _ x2)) ax end in + Split (@Build_ISO _ _ ask' (fun z => match z with inl z => emb1' z | inr z => emb2' z end) _ _) + (@surjDepProdGame t1 (fun x => A (inv iso (inl _ x))) (fun s : t1 => mkGame (inv iso (inl _ s))) g1) + (@surjDepProdGame t2 (fun x => A (inv iso (inr _ x))) (fun s : t2 => mkGame (inv iso (inr _ s))) g2) + end. +Next Obligation. +assert (EQ := uniqueSingleton iso x). subst. +assert (EQ := uniqueSingleton iso' X). subst. auto. +Defined. +Next Obligation. +destruct y. reflexivity. +Defined. +Next Obligation. +apply (uniqueSingleton iso z). +Defined. +Next Obligation. +assert (EQ := uniqueSingleton iso x). subst. +unfold getSingleton in EQ. +case_eq (mkGame (inv iso tt)). intros. inversion Heq_anonymous. rewrite H in H1. inversion H1. +intros. inversion Heq_anonymous. rewrite H in H1. dependent destruction H1. inversion H1. Heq_anonymous. rewrite H in Heq_anonymous. +destruct (mkGame (inv iso tt)). subst. +assert (EQ := uniqueSingleton (mkGame x)). iso' X). rewrite EQ in X. subst. +(* +intro s. dependent destruction s. +assert (x = x0). apply sing. subst x. split. intros. split. intros. +rewrite <- eq_rect_eq in H. destruct (sprf a). destruct (H0 x1). rewrite (H2 H). reflexivity. +intros. dependent destruction H. rewrite <- eq_rect_eq. +destruct (sprf (emb1 x1)). destruct (H x1). apply H2. reflexivity. +intro x2. rewrite <- eq_rect_eq. split. intros. destruct (sprf a). destruct (H1 x2). rewrite (H2 H). reflexivity. +intros. dependent destruction H. destruct (sprf (emb2 x2)). destruct (H0 x2). apply H2. reflexivity. +Defined. Next Obligation. +*) +destruct (mkGame (inv iso tt)). symmetry. destruct (H x1). apply H1. symmetry. assumption. +Defined. Next Obligation. +destruct (sprf z). symmetry. destruct (H0 x2). apply H1. symmetry. assumption. +Defined. Next Obligation. split. +intro x1. destruct x1. destruct x. split. intros. revert H. +(* Dependent rewriter will not cooperate otherwise! *) +generalize (@surjDepProdGame_obligation_4 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x : t => A x) x a0) x a0 (@refl_equal (@sigT t (fun x : t => A x)) (@existT t (fun x : t => A x) x a0))). +generalize (@surjDepProdGame_obligation_5 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x1 : t => A x1) x a0) x a0 (@refl_equal (@sigT t (fun x1 : t => A x1)) (@existT t (fun x1 : t => A x1) x a0))). +intros e e0. destruct (ask x). +intros. inversion H. simpl. simpl in H. subst t0. +assert (x = emb1 x0). apply e0. reflexivity. subst x. rewrite <- eq_rect_eq. reflexivity. +intros. inversion H. +intros. +dependent destruction H. compute. case(sprf (emb1 x0)). intros. compute. destruct (ask (emb1 x0)). +destruct (i t0). assert (t0 = x0). apply (sembed_inj_left sprf). apply H. reflexivity. +subst t0. case (i x0). compute. intro e. intro e0. compute. +generalize (e refl). intros. dependent destruction e1. reflexivity. +destruct (i x0). assert (inr t0 = inl x0). apply H0. reflexivity. discriminate. +intro x2. destruct x. destruct x2. +(* Dependent rewriter will not cooperate otherwise! *) +generalize (@surjDepProdGame_obligation_4 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x2 : t => A x2) x a) x a (@refl_equal (@sigT t (fun x2 : t => A x2)) (@existT t (fun x2 : t => A x2) x a))). +generalize (@surjDepProdGame_obligation_5 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x1 : t => A x1) x a) x a (@refl_equal (@sigT t (fun x1 : t => A x1)) (@existT t (fun x1 : t => A x1) x a))). +intros e e0. destruct (ask x). split. intros. inversion H. intros. +dependent destruction H. assert (emb1 t0 = emb2 x0). symmetry. apply e0. reflexivity. +assert False. destruct (sembed_disj sprf H). destruct H0. +split. intros. inversion H. simpl. subst t0. inversion H. +assert (x = emb2 x0). apply e. reflexivity. subst x. rewrite <- eq_rect_eq. reflexivity. +intros. dependent destruction H. assert (x0 = t0). +apply (sembed_inj_right sprf (e t0 (refl_equal _))). subst x0. +rewrite <- eq_rect_eq. reflexivity. +Qed. + +Definition depProdModel (t : Type) (g : Game t) (A : t -> Type) (mkGame : forall s : t, Game (A s)) : Game { x : t & A x }. +intros t g A mkGame. +destruct g. +(* g = Singleton *) + destruct (mkGame (inv i tt)). + (* mkGame _ = Singleton *) + refine (Singleton _). +(* assert ({x:t & A x}). + refine (existT _ (inv i tt) (inv _ tt)). exact (inv i0 tt). *) + refine (@Build_Iso _ _ (fun _ => tt) (fun _ => existT _ (inv i tt) (inv _ tt)) _ _). + intros. rewrite <- (mapinv i x). invmap i tt). auto. + Focus 2. + destruct y. trivial. + Focus 3. + Defined. auto. +i0). existT _ (inv i tt) (inv i0 tt)). +set (ask' := fun (z : { x : t & A x }) : t1 + t2 := match z with existT _ ax => ask ax). + let emb1' (z : t1) : { x : t & A x } := existT _ x (emb1 z) in + let emb2' (z : t2) : { x : t & A x } := existT _ x (emb2 z) in + +admit. +(*refine (Singleton _). +refine (@Build_Iso _ _ (fun _ => tt) (fun z => existT (fun z => A z) (inv i tt) _) _ _). +intros. destruct x. assert (inv i () = x). rewrite <- (invmap i). simpl. auto. rewrite <- (mapinv i). simpl. auto. +*) +refine (Split _ _ _). +refine (@Build_Iso ({ x : t & A x}) (({x:t1 & A (inv i (inl _ x))}) + ({x:t2 & A (inv i (inr _ x))}))%type + (fun z:{x:t & A x} => match i (projT1 z) with inl y => inl _ (existT _ y _) | inr y => inr _ (existT _ y _) end) _ _). +admit. +auto. + +intros. destruct x. +Check existT. +Check (invmap i). +unfold Iso in i. +Check (i). eadmit. +Program CoFixpoint depProdModel (t : Type) (g : Game t) (A : t -> Type) (mkGame : forall s : t, Game (A s)) : Game { x : t & A x }. + + := + match g with + | Singleton iso => coerceGame _ (mkGame (getSingleton iso)) + | Split t11 t12 iso m11 m12 => Split _ (*(SeqIso (ProdRIso t iso) (ProdSumL t11 t12 t)) *) (depProdModel m11 _) (depProdModel m12 _) + end. + +Lemma prodModelPreservesProper : forall t1 t2 (m1 : Game t1) (m2 : Game t2), ProperGame m1 -> ProperGame m2 -> ProperGame (prodModel m1 m2). +Proof. +intros t1 t2 m1 m2 P1 P2. unfold ProperGame in *. unfold prodModel. +unfold Everywhere. intros. +assert (EH1 := EverywhereHere P1). +assert (EH2 := EverywhereHere P2). +destruct EH1 as [x1 _]. destruct EH2 as [x2 _]. +dependent destruction H. +(**) +exists (x1,x2). trivial. +(**) +destruct m1. + rewrite decomp_game_thm in H0. simpl in H0. + destruct m2. + simpl in H0. inversion H0. + simpl in H0. dependent destruction H0. unfold Everywhere in P2. apply (P2 _ n). apply InsideLeft. assumption. +rewrite decomp_game_thm in H0. simpl in H0. + destruct m2. + simpl in H0. dependent destruction H0. admit. + dependent destruction H0. admit. +(**) +destruct m1. + rewrite decomp_game_thm in H0. simpl in H0. + destruct m2. + simpl in H0. inversion H0. + simpl in H0. dependent destruction H0. apply (P2 _ n). apply InsideRight. assumption. +rewrite decomp_game_thm in H0. simpl in H0. + destruct m2. + dependent destruction H0. fold prodModel in H. assert (EH := EverywhereHere P1). simpl in EH. simpl in EH. apply P2. simpl in H. apply (P1 _ n). apply InsideLeft. apply H. +destruct m2. +simpl in H0. +destruct m2. +assert (EH1 := EverywhereHere EP1). simpl in EH1. +inversion H0. dependent destruction H0. simpl in H0. inversion H0. dependent destruction H2. unfold Everywhere in P. apply (P _ n). apply InsideLeft. assumption. +destruct g. inversion H0. dependent destruction H0. unfold Everywhere in P. apply (P _ n). apply InsideRight. assumption. + + +(* +Lemma prodModelPreservesTotality : forall t1 t2 (m1 : Game t1) (m2 : Game t2), TotalGame m1 -> TotalGame m2 -> TotalGame (prodModel m1 m2). +Proof. +intros t1 t2 m1 m2 T1 T2. +unfold prodModel. +unfold TotalGame. +intros [x1 x2]. rewrite (decomp_game_thm _). destruct m1. simpl. admit. +simpl. +destruct m2. simpl. +simpl. +rewrite (decomp_game_thm _). fold IdGame. destruct m2. simpl. unfold coerceGame. simpl. +*) + +(* Strong dependent products: they assume that it is always possible to accept a mkGame function + ************************************************************************************************************************************) +Program CoFixpoint surjDepProdGame (t : Type) (A : t -> Type) (mkGame : forall s : t, Game (A s)) (g : Game t) : Game { x : t & A x } := + match g with + | Singleton x sing => + match mkGame x with + | Singleton ax axsing => Singleton (existT _ x ax) _ + | Split t1 t2 ask emb1 emb2 sprf g1 g2 => + let ask' (z : { x : t & A x }) : t1 + t2 := match z with existT _ ax => ask ax end in + let emb1' (z : t1) : { x : t & A x } := existT _ x (emb1 z) in + let emb2' (z : t2) : { x : t & A x } := existT _ x (emb2 z) in + Split (_ : SEmbed ask' emb1' emb2') g1 g2 + end + | Split t1 t2 ask emb1 emb2 sprf g1 g2 => + let ask' (z : {x : t & A x}) : {x : t1 & A (emb1 x) } + + {x : t2 & A (emb2 x) } := + match z with + existT x ax => match ask x with + | inl x1 => inl (existT _ x1 ax) + | inr x2 => inr (existT _ x2 ax) + end + end in + let emb1' (z : {x : t1 & A (emb1 x)}) : { x : t & A x } := + match z with + existT x1 ax => existT _ (emb1 x1) ax + end in + let emb2' (z : {x : t2 & A (emb2 x) }) : { x : t & A x } := + match z with existT x2 ax => existT _ (emb2 x2) ax end in + Split (_ : SEmbed ask' emb1' emb2') (@surjDepProdGame t1 (fun x => A (emb1 x)) (fun s : t1 => mkGame (emb1 s)) g1) + (@surjDepProdGame t2 (fun x => A (emb2 x)) (fun s : t2 => mkGame (emb2 s)) g2) + end. +Next Obligation. +unfold Sing. intros x1 x2. destruct x1. dependent destruction x2. +assert (x0 = x1). apply sing. subst x0. assert (x = x1). apply sing. subst x. +assert (a0 = a). apply axsing. subst a0. reflexivity. +Defined. Next Obligation. +intro s. dependent destruction s. +assert (x = x0). apply sing. subst x. split. intros. split. intros. +rewrite <- eq_rect_eq in H. destruct (sprf a). destruct (H0 x1). rewrite (H2 H). reflexivity. +intros. dependent destruction H. rewrite <- eq_rect_eq. +destruct (sprf (emb1 x1)). destruct (H x1). apply H2. reflexivity. +intro x2. rewrite <- eq_rect_eq. split. intros. destruct (sprf a). destruct (H1 x2). rewrite (H2 H). reflexivity. +intros. dependent destruction H. destruct (sprf (emb2 x2)). destruct (H0 x2). apply H2. reflexivity. +Defined. Next Obligation. +destruct (sprf z). symmetry. destruct (H x1). apply H1. symmetry. assumption. +Defined. Next Obligation. +destruct (sprf z). symmetry. destruct (H0 x2). apply H1. symmetry. assumption. +Defined. Next Obligation. split. +intro x1. destruct x1. destruct x. split. intros. revert H. +(* Dependent rewriter will not cooperate otherwise! *) +generalize (@surjDepProdGame_obligation_4 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x : t => A x) x a0) x a0 (@refl_equal (@sigT t (fun x : t => A x)) (@existT t (fun x : t => A x) x a0))). +generalize (@surjDepProdGame_obligation_5 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x1 : t => A x1) x a0) x a0 (@refl_equal (@sigT t (fun x1 : t => A x1)) (@existT t (fun x1 : t => A x1) x a0))). +intros e e0. destruct (ask x). +intros. inversion H. simpl. simpl in H. subst t0. +assert (x = emb1 x0). apply e0. reflexivity. subst x. rewrite <- eq_rect_eq. reflexivity. +intros. inversion H. +intros. +dependent destruction H. compute. case(sprf (emb1 x0)). intros. compute. destruct (ask (emb1 x0)). +destruct (i t0). assert (t0 = x0). apply (sembed_inj_left sprf). apply H. reflexivity. +subst t0. case (i x0). compute. intro e. intro e0. compute. +generalize (e refl). intros. dependent destruction e1. reflexivity. +destruct (i x0). assert (inr t0 = inl x0). apply H0. reflexivity. discriminate. +intro x2. destruct x. destruct x2. +(* Dependent rewriter will not cooperate otherwise! *) +generalize (@surjDepProdGame_obligation_4 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x2 : t => A x2) x a) x a (@refl_equal (@sigT t (fun x2 : t => A x2)) (@existT t (fun x2 : t => A x2) x a))). +generalize (@surjDepProdGame_obligation_5 t A mkGame g t1 t2 ask emb1 + emb2 sprf g1 g2 Heq_g (@existT t (fun x1 : t => A x1) x a) x a (@refl_equal (@sigT t (fun x1 : t => A x1)) (@existT t (fun x1 : t => A x1) x a))). +intros e e0. destruct (ask x). split. intros. inversion H. intros. +dependent destruction H. assert (emb1 t0 = emb2 x0). symmetry. apply e0. reflexivity. +assert False. destruct (sembed_disj sprf H). destruct H0. +split. intros. inversion H. simpl. subst t0. inversion H. +assert (x = emb2 x0). apply e. reflexivity. subst x. rewrite <- eq_rect_eq. reflexivity. +intros. dependent destruction H. assert (x0 = t0). +apply (sembed_inj_right sprf (e t0 (refl_equal _))). subst x0. +rewrite <- eq_rect_eq. reflexivity. +Qed. + + +(**************************************************************************************************** + * + * Recursive types cooking recipe: + * Typically a recursive type game is a partition of all of its constructors and for + * each game we have a call to prodGame between the function itself (a recursive call) + * and the payload (if any). For example, for trees it should be something like: + * treeGame := Split Singleton (prodGame payLoadGame treeGame) + * + * Of course, Coq is not clever enough to understand the well-formedness of such corecursive + * definitions, so our choice for encoding recursive datatypes is by creating inductive objects + * depending on *some* metric on the datatype (such as the depth) we are encoding and then use + * dependent products. + ****************************************************************************************************) + +Program Fixpoint finListGame (t : Type) (g : Game t) (n : nat) : Game {l : list t | length l = n } := + match n with + | 0 => Singleton nil _ + | S n0 => @coerceGame _ _ _ _ _ (prodGame g (finListGame g n0)) + end. +Next Obligation. +intros. unfold Sing. intros. destruct x. destruct y. +destruct x. destruct x0. apply proof_irrelevant_existential. +inversion e0. inversion e. +Defined. Next Obligation. +exists (t0::s). simpl. reflexivity. +Defined. Next Obligation. +destruct X. inversion H. simpl in H. split. apply t0. +exists X. auto. +Defined. Next Obligation. +split. inversion Heq_n. destruct n. inversion H. inversion H. +unfold Iso. intros. destruct x. destruct x. inversion e. simpl in e. inversion e. simpl. +subst n0. subst n. rewrite <- eq_rect_eq. apply proof_irrelevant_existential. +intro y. destruct y. dependent destruction Heq_n. dependent destruction s. +dependent destruction e. simpl. erewrite proof_irrelevant_existential. reflexivity. +Qed. + + + + + +
+ FilterGames.hs view
@@ -0,0 +1,138 @@+{-# OPTIONS_GHC -fglasgow-exts #-} +module FilterGames where + +import Iso +import Games +import BasicGames + +import Data.Maybe + +-- /voidGame/ +voidGame :: Game t -- Precondition: t is uninhabited +voidGame = Split (Iso ask bld) voidGame voidGame + where ask = Right + bld (Left x) = x + bld (Right x) = x +-- /End/ + + +-- /filterGame/ +filterGame :: (t -> Bool) -> Game t -> Game t +-- forall (p : t -> Bool), Game t -> Game { x | p x } +filterGame p g@(Single (Iso _ bld)) = + if p (bld ()) then g else voidGame +filterGame p (Split (Iso ask bld) g1 g2) + = Split (Iso ask bld) (filterGame (p . bld . Left) g1) + (filterGame (p . bld . Right) g2) +-- /End/ + +-- /filterGameOpt/ +-- (f : t -> Bool) -> Game t -> Maybe (Game {x:t | f t}) +filterGameOpt :: (t -> Bool) -> Game t -> Maybe (Game t) +filterGameOpt f (Single iso) + | f (from iso ()) = Just $ Single iso + | otherwise = Nothing +filterGameOpt f (Split (Iso ask bld) g1 g2) + = case filterGameOpt (f . bld . Left) g1 of + Nothing -> + case filterGameOpt (f . bld . Right) g2 of + Nothing -> Nothing + Just g2' -> Just (g2' +> iso2) + Just g1' -> + case filterGameOpt (f . bld . Right) g2 of + Nothing -> Just (g1' +> iso1) + Just g2' -> Just $ Split (Iso ask bld) g1' g2' + where iso1 = Iso (\x -> case ask x of Left x1 -> x1) + (bld . Left) + iso2 = Iso (\x -> case ask x of Right x2 -> x2) + (bld . Right) +-- /End/ + +-- /filterFinGame/ +filterFinGame :: (t -> Bool) -> Game t -> Maybe (Game t) +-- forall (p : t -> Bool), Game t -> option (Game { x | p x }) +filterFinGame p g@(Single (Iso _ bld)) = + if p (bld ()) then Just g else Nothing +filterFinGame p (Split iso@(Iso ask bld) g1 g2) + = case (filterFinGame (p . bld . Left) g1, + filterFinGame (p . bld . Right) g2) of + (Nothing, Nothing) -> Nothing + (Just g1', Nothing) -> Just $ g1' +> iso1 + (Nothing, Just g2') -> Just $ g2' +> iso2 + (Just g1', Just g2') -> Just $ Split iso g1' g2' + where fromLeft (Left x) = x + fromRight (Right x) = x + iso1 = Iso (fromLeft . ask) (bld . Left ) + iso2 = Iso (fromRight . ask) (bld . Right) +-- /End/ + +{- Games for infinitely inhabited (after filtering) data types -} + +pre_filterGame_inf :: Eq t => Game t -> (t -> Bool) -> Game t +pre_filterGame_inf stack f + = case unfoldUntil stack of + (x,rest) | f x -> + let iso = Iso ask (either id id) + ask z = if x == z then Left z else Right z + sing_iso = Iso (\_ -> ()) (\_ -> x) + in Split iso (Single sing_iso) (pre_filterGame_inf rest f) + | otherwise -> pre_filterGame_inf rest f + +filterInfGame :: forall t. Eq t => (t -> Bool) -> Game t -> Game t +filterInfGame f g = pre_filterGame_inf (mkStack g) f + where mkStack g = Split (iso :: ISO t (Either t t)) g (Single undefined) -- terminator node + iso = Iso Left (either id id) + +-- -- unfoldUntil (stack :: Game t) returns an element z and +-- -- Game {x : t | x <> z } +-- -- We *know* it will terminate because there are infinitely many +-- -- elements inhabiting the datatype +unfoldUntil :: Game t -> (t, Game t) +unfoldUntil stack = case find stack of + Left (x,rest) -> (x,rest) + Right unfolded -> unfoldUntil unfolded + +-- One step unfolding of a list-like game +unfoldOne :: forall t. Game t -> Game t +unfoldOne (Single undef) = Single undef -- Terminator +unfoldOne (Split iso (Single siso) rest) + = Split iso (Single siso) (unfoldOne rest) +unfoldOne (Split iso (Split iso' g1 g2) rest) + = shufflePartition (Split iso (Split iso' g1 g2) (unfoldOne rest)) + +find :: forall t. Game t -> Either (t,Game t) (Game t) +find (Single undef) = Right (Single undef) -- Terminator: not found +find (Split (iso :: ISO t (Either t1 t2)) (Single siso) rest) + = let x = from iso $ Left (from siso ()) + unfolded = unfoldOne rest +> ciso + ciso :: ISO t t2 + ciso = Iso (\x -> case to iso x of Right x2 -> x2) (from iso . Right) + in Left (x,unfolded) +find (Split siso (Split siso' g1 g2) rest) + = case find rest of + Left (x, unfolded) -> Left (from siso (Right x), shufflePartition (Split siso (Split siso' g1 g2) unfolded)) + Right unfolded -> Right (shufflePartition (Split siso (Split siso' g1 g2) unfolded)) + +shufflePartition :: forall t. Game t -> Game t +shufflePartition (Split (siso :: ISO t (Either t1 trest)) + (Split (siso' :: ISO t1 (Either t11 t12)) g1 g2) rest) + = Split siso1 g1 (Split siso2 g2 rest) + where siso2 = idI + siso1 = Iso ask bld + + ask :: t -> Either t11 (Either t12 trest) + ask x = case to siso x of + Left x1 -> case to siso' x1 of + Left x11 -> Left x11 + Right x12 -> Right (Left x12) + Right xrest -> Right (Right xrest) + + bld (Left x11) = from siso $ Left (from siso' (Left x11)) + bld (Right (Left x12)) = from siso $ Left (from siso' (Right x12)) + bld (Right (Right xrest)) = from siso $ Right xrest + +mkOddNatGame = filterInfGame odd unaryNatGame +test_odd0 bitstream = dec mkOddNatGame bitstream +test_odd1 num = enc mkOddNatGame num + +
+ Games.hs view
@@ -0,0 +1,81 @@+{-# options_ghc -XGADTs -XScopedTypeVariables -XKindSignatures #-} +module Games where + +import Random +import Iso + +-- A game for type t, Game t, is a potentially infinite decision tree +-- with extra information about how to ask questions in the branches, +-- and elements of the datatype in the leaves. + +-- /Game/ +data Game :: * -> * where + Single :: ISO t () -> Game t + Split :: ISO t (Either t1 t2) -> + Game t1 -> Game t2 -> Game t +-- /End/ + +-- /Bit/ +data Bit = O | I +-- /End/ + deriving Show + +showBits [] = "" +showBits (b:bs) = show b ++ showBits bs + +-- /dec/ +dec :: Game t -> [Bit] -> (t, [Bit]) +dec (Single (Iso _ bld)) str = (bld (), str) +dec (Split _ _ _) [] = error "Input too short" +dec (Split (Iso _ bld) g1 g2) (I : xs) + = let (x1, rest) = dec g1 xs + in (bld (Left x1), rest) +dec (Split (Iso _ bld) g1 g2) (O : xs) + = let (x2, rest) = dec g2 xs + in (bld (Right x2), rest) +-- /End/ + +-- /decOpt/ +decOpt :: Game t -> [Bit] -> Maybe (t, [Bit]) +decOpt (Single (Iso _ bld)) str = Just (bld (), str) +decOpt (Split _ _ _) [] = Nothing +decOpt (Split (Iso _ bld) g1 g2) (I:xs) + = do (x1, rest) <- decOpt g1 xs + return (bld (Left x1), rest) +decOpt (Split (Iso _ bld) g1 g2) (O:xs) + = do (x2, rest) <- decOpt g2 xs + return (bld (Right x2), rest) +-- /End/ + + +-- /decRand/ +decRandAux :: RandomGen g => g -> Game t -> t +decRandAux r (Single (Iso _ bld)) = bld () +decRandAux r (Split (Iso _ bld) g1 g2) = + let (b::Int,r') = random r + in if even b then bld (Left (decRandAux r' g1)) + else bld (Right (decRandAux r' g2)) +decRand :: Int -> Game t -> t +decRand i g = decRandAux (mkStdGen i) g +-- /decRand/ + +-- Coerce a game, via an isomorphism +-- /coerceGame/ +(+>) :: Game t -> ISO s t -> Game s +(Single j) +> i = Single (i `seqI` j) +(Split j g1 g2) +> i = Split (i `seqI` j) g1 g2 +-- /End/ + +infixl 4 +> + +-- /enc/ +enc :: Game t -> t -> [Bit] +enc (Single _) x = [] +enc (Split (Iso ask _) g1 g2) x + = case ask x of Left x1 -> I : enc g1 x1 + Right x2 -> O : enc g2 x2 +-- /End/ + + +testGame :: Game t -> t -> (t,[Bit]) +testGame g x = dec g (enc g x)
+ Games.v view
@@ -0,0 +1,665 @@+Require Import List. + +Set Implicit Arguments. +Unset Strict Implicit. +Set Printing Implicit Defensive. +Set Transparent Obligations. + +Require Import colist. +Require Import Iso. + +(* Empty sets *) +Definition Empty (t : Type) : Prop := t -> False. +Definition Inhabited (t : Type) : Prop := exists x : t, True. + +(*====================================================================================== + A Game for a type t is a (potentially infinite) decision tree + in which each node partitions by an isomorphism t ~= a+b, and each leaf represents + a singleton "answer" by an isomorphism t ~= unit + + Note that we are not yet imposing a "strict" partitioning, i.e. it + might be that a or b is empty. + ======================================================================================*) +(*=Game *) +CoInductive Game t := + | Single : ISO t unit -> Game t + | Split : forall a b, ISO t (a + b) -> + Game a -> Game b -> Game t. +(*=End *) + +(*====================================================================================== + Given a game g for a type t, we can decode a list of bools by interpreting the bools as + "answers" in the game, using the inverse map of the isomorphism to construct a value. + ======================================================================================*) +(*=dec *) +Fixpoint dec t (g: Game t) (str:list bool) + : option (t*list bool) := + match g with + | Single iso => Some (inv iso tt, str) + | Split _ _ iso g1 g2 => + match str with + | true :: xs => + match dec g1 xs with + None => None + | Some (x,str') => + Some (inv iso (inl _ x),str') end + | false :: xs => + match dec g2 xs with + None => None + | Some (x,str') => + Some (inv iso (inr _ x),str') end + | nil => None + end + end. +(*=End *) + +Lemma decSingle : forall t xs (iso : ISO t unit), dec (Single iso) xs = Some (getSingleton iso,xs). +Proof. intros. destruct xs; auto. +Qed. + +Lemma decSplit : forall ta ta1 ta2 iso g1 g2 (x : list bool), + dec (@Split ta ta1 ta2 iso g1 g2) x + = + match x with + | true :: xs => match dec g1 xs with None => None | Some (x,str') => Some (inv iso (inl _ x), str') end + | false :: xs => match dec g2 xs with None => None | Some (x,str') => Some (inv iso (inr _ x), str') end + | nil => None + end. +Proof. intros. destruct x. auto. destruct b. auto. auto. +Qed. + +(*====================================================================================== + Given a game g for a type t, we can encode a value of type t by playing the game, using + the forward map of the isomorphism to ask questions of the value. + + The encoder is not guaranteed to terminate. + For example when the ask question splits the two sets in + - the full set (bit 0) + - and the empty set (bit 1) + and repeating the same question infinitely, then the + encoder is only going to give a stream 000... back. + ======================================================================================*) +(*=enc *) +CoFixpoint enc t (g : Game t) : t -> colist bool := + match g with + | Single _ => fun x => cnil _ + | Split _ _ iso g1 g2 => + fun x => match iso x with + | inl x1 => ccons true (enc g1 x1) + | inr x2 => ccons false (enc g2 x2) + end + end. +(*=End *) + +Lemma encSingle : forall t (iso:ISO t unit) y, enc (Single iso) y = cnil bool. +Proof. intros. rewrite (decomp_colist_thm (enc (Single iso) y)). compute. reflexivity. +Qed. + +Lemma encSplit : forall ta ta1 ta2 iso g1 g2 (x : ta), + enc (@Split ta ta1 ta2 iso g1 g2) x + = + match iso x with + | inl x1 => ccons true (enc g1 x1) + | inr x2 => ccons false (enc g2 x2) + end. +Proof. intros. rewrite (@decomp_colist_thm _ (enc (Split iso g1 g2) x)). +simpl. destruct (iso x); reflexivity. +Qed. + +(*=encDefs *) +Definition encProduces t (g : Game t) x str := + FinCoList (enc g x) str. +Definition encTerminates t (g : Game t) x := + exists str, encProduces g x str. +Definition encTotal t (g : Game t) := + forall x, encTerminates g x. +(*=End *) + + +(*====================================================================================== + We can prove the prefix property of enc for finite prefixes, using only + injectivity of the map of the isomorphism. + ======================================================================================*) +Require Import Program.Equality. +(* +(*=encFinPrefix *) +Lemma encFinPrefix t (g : Game t) : forall v w, FinPrefix (enc g v) (enc g w) -> v=w. +(*=End *) +Proof. intros t g v w PRE. +dependent induction PRE. destruct g. rewrite (uniqueSingleton i). rewrite <- (uniqueSingleton i v). reflexivity. +rewrite encSplit in *. destruct (i v); congruence. + +destruct g. rewrite encSingle in *. congruence. +rewrite encSplit in *. + +case_eq (i v). intros v' EQv. rewrite EQv in *. +(* i v = inl _ *) + case_eq (i w). + (* i w = inl _ *) + intros w' EQw. rewrite EQw in *. + specialize (@IHPRE a g1 v' w'). assert (SS : x = true /\ xs = enc g1 v'). split; congruence. destruct SS. subst. + assert (SS : ys = enc g1 w'). congruence. subst. + specialize (IHPRE (refl_equal _) (refl_equal _)). rewrite IHPRE in *. rewrite <- EQw in EQv. apply (isoInj EQv). + (* i w = inr _ *) + intros w' EQw. rewrite EQw in *. congruence. +(* i v = inr _ *) +intros v' EQv. rewrite EQv in *. + case_eq (i w). + (* i w = inl _ *) + intros w' EQw. rewrite EQw in *. assert (SS : x = false /\ xs = enc g2 v'). split; congruence. destruct SS. congruence. + (* i w = inr _ *) + intros w' EQw. rewrite EQw in *. + specialize (@IHPRE _ g2 v' w'). + assert (SS : x = false /\ xs = enc g2 v'). split; congruence. destruct SS. subst. + assert (SS : ys = enc g2 w'). congruence. subst. specialize (IHPRE (refl_equal _) (refl_equal _)). + subst. rewrite <- EQw in EQv. + apply (isoInj EQv). +Qed. +*) + +(* The obvious corollary to the above is injectivity of enc. To do this properly we + should define Prefix coinductively so that it includes equality even on infinite lists. + Here we prove injectivity for the finite case. *) +(* +Lemma encPrefix t (g : Game t) : forall v w, Prefix (enc g v) (enc g w) -> v=w. +Proof. intros t g v w PRE. +dependent destruction PRE. +destruct g. rewrite (uniqueSingleton i). rewrite <- (uniqueSingleton i _). reflexivity. +rewrite encSplit in H. destruct (i v); auto. discriminate H. discriminate H. + +destruct g. rewrite encSingle in H. discriminate H. +rewrite encSplit in H. rewrite encSplit in H0. + +case_eq (i v). intros v' EQv. rewrite EQv in H. +(* i v = inl _ *) + case_eq (i w). + (* i w = inl _ *) + intros w' EQw. rewrite EQw in H0. + specialize (@IHPRE a g1 v' w'). + inversion H. subst. inversion H0. subst. specialize (IHPRE (refl_equal _) (refl_equal _)). + subst. rewrite <- EQw in EQv. + apply (isoInj EQv). + (* i w = inr _ *) + intros w' EQw. rewrite EQw in H0. inversion H. inversion H0. rewrite H4 in H2. discriminate H2. +(* i v = inr _ *) +intros v' EQv. rewrite EQv in H. + case_eq (i w). + (* i w = inl _ *) + intros w' EQw. rewrite EQw in H0. inversion H. inversion H0. subst. discriminate H4. + (* i w = inr _ *) + intros w' EQw. rewrite EQw in H0. + specialize (@IHPRE _ g2 v' w'). + inversion H. subst. inversion H0. subst. specialize (IHPRE (refl_equal _) (refl_equal _)). + subst. rewrite <- EQw in EQv. + apply (isoInj EQv). +Qed. +*) + +(*====================================================================================== + The basic correctness property: if encoding a value x results in a + finite list str, then decoding of str++xs produces the value x and + residual xs. + ======================================================================================*) +(*=encDec *) +Lemma encDec : forall (str xs : list bool) t (g : Game t) x, + encProduces g x str -> dec g (str ++ xs) = Some (x, xs). +(*=End *) +Proof. +unfold encProduces. +induction str. +(* str := nil *) +intros. simpl. +destruct g. +(* g := Single _ *) rewrite decSingle. rewrite <- (uniqueSingleton i x). reflexivity. +(* g := Split _ *) +rewrite encSplit in H. destruct (i x). rewrite decSplit. +inversion H. +inversion H. +(* str := a::str *) +intros. inversion H. subst. simpl. +destruct g. +(* g := Single _ *) rewrite encSingle in H0. inversion H0. +(* g := Split _ _ *) +destruct a. +(* a := true *) +rewrite encSplit in H0. case_eq (i x). +intros z EQ. rewrite EQ in H0. inversion H0. subst. rewrite (IHstr _ _ _ _ H2). rewrite <- EQ. rewrite mapinv. reflexivity. +intros z EQ. rewrite EQ in H0. inversion H0. +(* a := false *) +rewrite encSplit in H0. case_eq (i x). +intros z EQ. rewrite EQ in H0. inversion H0. +intros z EQ. rewrite EQ in H0. inversion H0. subst. rewrite (IHstr _ _ _ _ H2). rewrite <- EQ. rewrite mapinv. reflexivity. +Qed. + +Definition DecSomeImpliesEnc t (g : Game t) (str : list bool) := + forall x (rest : list bool), dec g str = Some (x, rest) -> + exists x_str, encProduces g x x_str /\ x_str ++ rest = str. + +(*====================================================================================== + If decoding succeeds, then it round-trips. + ======================================================================================*) +Lemma decEncSuccess : forall (str : list bool) t (g : Game t), + DecSomeImpliesEnc g str. +Proof. +induction str. +(* str := nil *) +intros. unfold DecSomeImpliesEnc. intros. +exists (@nil bool). +destruct g. +(* g := Single _ *) +rewrite decSingle in *. inversion H. subst. split. unfold encProduces. rewrite encSingle. apply FinCoListNil. auto. +(* g := Split _ *) +rewrite decSplit in H. discriminate H. +(* str := cons _ _ *) +intros. unfold DecSomeImpliesEnc. intros. +destruct g. +(* g := Single _ *) +rewrite decSingle in H. inversion H. subst. unfold encProduces. rewrite encSingle. exists (nil : list bool). +split. apply FinCoListNil. unfold app. reflexivity. +(* g :- Split _ *) +rewrite decSplit in H. +unfold encProduces. rewrite encSplit. destruct a. +(* a = true *) +unfold DecSomeImpliesEnc in IHstr. +case_eq (dec g1 str). intros [x1 str'] EQ. rewrite EQ in H. specialize (IHstr _ _ _ _ EQ). +inversion H. subst. rewrite invmap. destruct IHstr as [str' [H1 H2]]. exists (true::str'). +split. apply FinCoListCons. auto. simpl. rewrite H2. auto. +intros EQ. rewrite EQ in H. inversion H. +(* a = false *) +unfold DecSomeImpliesEnc in IHstr. +case_eq (dec g2 str). intros [x2 str'] EQ. rewrite EQ in H. specialize (IHstr _ _ _ _ EQ). +inversion H. subst. rewrite invmap. destruct IHstr as [str' [H1 H2]]. exists (false::str'). +split. apply FinCoListCons. auto. simpl. rewrite H2. auto. +intros EQ. rewrite EQ in H. inversion H. +Qed. + + +(*====================================================================================== + Does there exist a path from the current node to a leaf? The + second parameter is the value at the leaf, embedded through the + path to a value at t. + ======================================================================================*) +(*=HasFinPath *) +Inductive HasFinPath : forall t, Game t -> t -> Prop := + | HasFinPathSing : forall t (iso : ISO t unit) , + HasFinPath (Single iso) (inv iso tt) + | HasFinPathLeft : forall (t a b : Type) + (g1 : Game a) (g2 : Game b) + (iso : ISO t _) x1, + HasFinPath g1 x1 -> + HasFinPath (Split iso g1 g2) + (inv iso (inl _ x1)) + | HasFinPathRight : forall (t a b : Type) + (g1 : Game a) (g2 : Game b) + (iso : ISO t _) x2, + HasFinPath g2 x2 -> + HasFinPath (Split iso g1 g2) + (inv iso (inr _ x2)). +(*=End *) + +Lemma HasFinPathInversion : forall t (g:Game t) (x:t), HasFinPath g x -> + (exists iso : ISO t unit, g = Single iso /\ x = getSingleton iso) \/ + (exists a, exists b, exists g1 : Game a, exists g2 : Game b, exists iso : ISO t _, + g = Split iso g1 g2 /\ + ((exists y, HasFinPath g1 y /\ x = inv iso (inl _ y)) \/ + (exists y, HasFinPath g2 y /\ x = inv iso (inr _ y)))). +Proof. +intros. +destruct H. + left. exists iso. auto. + right. + exists a. exists b. exists g1. exists g2. exists iso. split. reflexivity. + left. exists x1. auto. + right. + exists a. exists b. exists g1. exists g2. exists iso. split. reflexivity. + right. exists x2. auto. +Qed. + +(* We seem to need dependent destruction for Split _ _ _ = Split _ _ _ *) +Require Import Program.Equality. +Lemma HasFinPathSplit : forall t a b (g1:Game a) (g2:Game b) iso (x:t), HasFinPath (Split iso g1 g2) x -> + (exists y, HasFinPath g1 y /\ x = inv iso (inl _ y)) \/ + (exists y, HasFinPath g2 y /\ x = inv iso (inr _ y)). +Proof. +intros. +assert (H' := HasFinPathInversion H). +destruct H'. destruct H0. destruct H0. inversion H0. +destruct H0 as [t3 [t4 [g3 [g4 [iso0 [P HH]]]]]]. +destruct HH. + left. destruct H0. dependent destruction P. exists x0. auto. + right. destruct H0. dependent destruction P. exists x0. auto. +Qed. + +(*====================================================================================== + Inside n m: is node n inside tree m + ======================================================================================*) +Inductive Inside tb (g:Game tb) : forall ta, Game ta -> Prop := + | InsideSame : Inside g g + | InsideLeft : forall (ta ta1 ta2 : Type) g1 g2 (iso : ISO ta (ta1+ta2)), + Inside g g1 -> + Inside g (Split iso g1 g2) + | InsideRight : forall (ta ta1 ta2 : Type) g1 g2 (iso : ISO ta (ta1+ta2)), + Inside g g2 -> + Inside g (Split iso g1 g2). + +(* Transitivity of Inside *) +Lemma inside_trans : forall a (g1 : Game a) b (g2 : Game b) c (g3 : Game c), + Inside g2 g3 -> Inside g1 g2 -> Inside g1 g3. +intros a g1 b g2 c g3 ins2. generalize a g1. +induction ins2. + intros. apply H. + intros. apply InsideLeft. apply IHins2. apply H. + intros. apply InsideRight. apply IHins2. apply H. +Qed. + +(*====================================================================================== + Quantification over all subtrees is expressed using Inside + ======================================================================================*) +Definition GameProp := forall s, Game s -> Prop. +Definition Everywhere (P : GameProp) t (g : Game t) := forall s (n:Game s), Inside n g -> P s n. + +Lemma EverywhereSplit P t a b (g1 : Game a) (g2 : Game b) (iso : ISO t (a+b)) + : Everywhere P (Split iso g1 g2) -> Everywhere P g1 /\ Everywhere P g2. +Proof. intros. unfold Everywhere in *. split. intros. apply H. apply InsideLeft. assumption. +intros. apply H. apply InsideRight. assumption. +Qed. + +Lemma EverywhereHere t (g : Game t) P : Everywhere P g -> P _ g. +Proof. intros. unfold Everywhere in H. apply H. apply InsideSame. +Qed. + +(*====================================================================================== + A game is Productive if every subtree contains a finite path to a leaf. + This gives the 'every bit counts' property. + + The VoidGame and NonProperGame (see Simple.v) are not Productive. + ======================================================================================*) +Definition ProductiveGame := Everywhere (fun s (n:Game s) => exists x, HasFinPath n x). + +Lemma productive_ne : forall t (g : Game t), ProductiveGame g -> Inhabited t. +Proof. +intros. unfold ProductiveGame in H. +assert (exists z, HasFinPath g z). apply H. apply InsideSame. clear H. +induction H0. unfold Inhabited. exists x. auto. +Qed. + +Lemma EncTerminatesFinPathAux : forall str t (g : Game t) x, encProduces g x str -> HasFinPath g x. +induction str. +(* str = nil *) +intros. inversion H. +destruct g. rewrite (uniqueSingleton i). apply HasFinPathSing. rewrite encSplit in H1. destruct (i x); inversion H1. +(* str = cons _ _ *) +intros. +unfold encProduces in *. +destruct g. +(* g = Single _ *) +rewrite encSingle in H. inversion H. +(* g = Split _ *) +rewrite encSplit in *. +case_eq (i x). + intros x' EQ. rewrite EQ in *. rewrite <- (mapinv i). rewrite EQ. apply HasFinPathLeft. + apply IHstr. inversion H. auto. + + intros x' EQ. rewrite EQ in *. rewrite <- (mapinv i). rewrite EQ. apply HasFinPathRight. + apply IHstr. inversion H. auto. +Qed. + +(*====================================================================================== + Encoder terminates on x if and only if there is a finite path to x + ======================================================================================*) +Theorem EncTerminatesFinPath t (g : Game t) : forall x, encTerminates g x <-> HasFinPath g x. +Proof. +intros t g x. +split. +(* If encoder terminates then there is a finite path *) +intros TERM. +unfold encTerminates in TERM. +destruct TERM as [str H]. +apply (EncTerminatesFinPathAux H). +(* If there is a finite path then encoder terminates *) +intros IFpath. +induction IFpath. + exists (nil : list bool). unfold encProduces. rewrite encSingle. apply FinCoListNil. + destruct IHIFpath. + exists (true::x). unfold encProduces. rewrite encSplit. + cut (iso (inv iso (inl _ x1)) = inl _ x1). intros. rewrite H0. apply FinCoListCons. destruct H0. apply H. + apply invmap. + + destruct IHIFpath. + exists (false::x). unfold encProduces. rewrite encSplit. + cut (iso (inv iso (inr _ x2)) = inr _ x2). intros. rewrite H0. apply FinCoListCons. destruct H0. apply H. + apply invmap. +Qed. + +Lemma elem_from_model: forall t (g : Game t), ProductiveGame g -> exists x, encTerminates g x. +Proof. +intros. unfold ProductiveGame in *. edestruct H. apply InsideSame. assert (T := proj2 (EncTerminatesFinPath g x)). exists x. auto. +Qed. + +Definition DecNoneImpliesEnc t (g : Game t) (str : list bool) := + ProductiveGame g -> dec g str = None -> + exists rest, exists x, FinCoList (enc g x) (str ++ rest). + + +(* Productive games satisfy one more property *) +Lemma decEncFail : forall (str : list bool) t (g : Game t), DecNoneImpliesEnc g str. +Proof. +induction str. +(* str := nil *) +intros. unfold DecNoneImpliesEnc. intros. simpl. assert (H' := elem_from_model H). unfold encTerminates in H'. destruct H' as [x [str H']]. exists str. exists x. auto. +(* str := cons _ _ *) +intros. unfold DecNoneImpliesEnc. intros. +destruct g. +(* g := Single _ *) +rewrite decSingle in H0. inversion H0. +(* g := Split _ *) +rewrite decSplit in H0. +destruct (EverywhereSplit H) as [Hl Hr]. +destruct a. +(* a := true *) +assert (DecNoneImpliesEnc g1 str). apply IHstr. +unfold DecNoneImpliesEnc in H1. specialize (H1 Hl). +case_eq (dec g1 str). +intros [x1 str'] EQ. +rewrite EQ in H0. inversion H0. intros EQ. specialize (H1 EQ). destruct H1 as [rest [x H2]]. exists rest. +exists (inv i (inl _ x)). rewrite encSplit. rewrite invmap. apply FinCoListCons. apply H2. +(* a := false *) +assert (DecNoneImpliesEnc g2 str). apply IHstr. +unfold DecNoneImpliesEnc in H1. specialize (H1 Hr). +case_eq (dec g2 str). +intros [x2 str'] EQ. +rewrite EQ in H0. inversion H0. intros EQ. specialize (H1 EQ). destruct H1 as [rest [x H2]]. exists rest. +exists (inv i (inr _ x)). rewrite encSplit. rewrite invmap. apply FinCoListCons. apply H2. +Qed. + +(*====================================================================================== + A game g for type t is Total if every element of t is reachable by some finite path. + + Unlike Productivity, this guarantees termination of the encoder. + ======================================================================================*) +(*=TotalGame *) +Definition TotalGame t (g : Game t) := forall x, HasFinPath g x. +(*=End *) +(* The encoder is total if and only if the game is total *) +(*=Totality *) +Theorem Totality : forall t (g : Game t), TotalGame g <-> encTotal g. +(*=End *) +Proof. +intros t g. +split. +(* If game is total then encoding is total *) +intros Hc x. +unfold TotalGame in Hc. +apply (proj2 (EncTerminatesFinPath g _)). auto. +(* If encoding is total then game is total *) +intros TERM. +unfold TotalGame. +intros x. +destruct (TERM x) as [str H]. clear TERM. +apply (proj1 (EncTerminatesFinPath g _)). unfold encTerminates. exists str. auto. +Qed. + +Definition decomp_game t (g : Game t) : Game t := + match g with + | Single iso => Single iso + | Split _ _ iso g1 g2 => Split iso g1 g2 + end. + +Theorem decomp_game_thm : forall t (g : Game t), g = decomp_game g. +Proof. intros; case g; auto. Qed. + +Lemma singletonGameIsTotal : forall t (iso : ISO t unit), TotalGame (Single iso). +Proof. intros. unfold TotalGame. intros. rewrite (uniqueSingleton iso x). apply HasFinPathSing. Defined. + +Lemma splitPreservesTotality t a b (iso : ISO t (a+b)) g1 g2 : TotalGame g1 -> TotalGame g2 -> TotalGame (Split iso g1 g2). +Proof. +intros t a b iso g1 g2 T1 T2. +unfold TotalGame in *. +intros x. intros. case_eq (iso x). + intros x1 EQ. replace x with (inv iso (inl _ x1)). apply (HasFinPathLeft). auto. rewrite <- EQ. rewrite mapinv. trivial. + intros x2 EQ. replace x with (inv iso (inr _ x2)). apply (HasFinPathRight). auto. rewrite <- EQ. rewrite mapinv. trivial. +Qed. + +Lemma TotalOfSplit t a b (iso : ISO t (a+b)) g1 g2 : TotalGame (Split iso g1 g2) -> TotalGame g1 /\ TotalGame g2. +intros. unfold TotalGame. split. +intros. assert (H' := HasFinPathSplit (H (inv iso (inl _ x)))). destruct H'. +destruct H0 as [y [H1 H2]]. assert (H3 := invInj H2). inversion H3. auto. +destruct H0 as [y [H1 H2]]. assert (H3 := invInj H2). inversion H3. auto. +intros. assert (H' := HasFinPathSplit (H (inv iso (inr _ x)))). destruct H'. +destruct H0 as [y [H1 H2]]. assert (H3 := invInj H2). inversion H3. auto. +destruct H0 as [y [H1 H2]]. assert (H3 := invInj H2). inversion H3. auto. +Qed. + + + +(*====================================================================================== + A weaker notation of productivity: all subtree types are inhabited. + ======================================================================================*) +Definition ProperGame := Everywhere (fun t _ => Inhabited t). + +Lemma singletonGameIsProper : forall t (iso : ISO t unit), ProperGame (Single iso). +Proof. +intros. unfold ProperGame. unfold Everywhere. intros. inversion H. subst. exists (getSingleton iso). trivial. +Qed. + +Lemma splitPreservesProper t a b (iso : ISO t (a+b)) g1 g2 : ProperGame g1 -> ProperGame g2 -> ProperGame (Split iso g1 g2). +Proof. +intros t a b iso g1 g2 P1 P2. +unfold ProperGame in *. + +unfold Everywhere. intros. +dependent destruction H. +assert (P1a := EverywhereHere P1). simpl in P1a. +unfold Inhabited in *. destruct P1a. exists (inv iso (inl _ x)). trivial. + +apply (P1 _ _ H). apply (P2 _ _ H). +Qed. + + +Lemma ProperOfSplit t a b (iso : ISO t (a+b)) g1 g2 : ProperGame (Split iso g1 g2) -> ProperGame g1 /\ ProperGame g2. +Proof. +intros. apply (EverywhereSplit H). +Qed. + + +(* Productivity implies proper *) +Lemma ProductiveImpliesProper : forall t (g : Game t), ProductiveGame g -> ProperGame g. +Proof. +intros. unfold ProperGame. unfold Everywhere. intros s n IN. +induction IN. +destruct n. exists (getSingleton i). trivial. +unfold ProductiveGame in H. unfold Everywhere in H. +assert (Inside n1 (Split i n1 n2)). apply InsideLeft. apply InsideSame. +specialize (H _ n1 H0). destruct H as [x1 _]. exists (inv i (inl _ x1)). trivial. +destruct (EverywhereSplit H) as [H1 H2]. apply (IHIN H1). +destruct (EverywhereSplit H) as [H1 H2]. apply (IHIN H2). +Qed. + +(* The converse property: + * non_trivial_prod : forall t (g : Game t), ProperGame g -> ProductiveGame g. + * is False even for Adequate games. Think of a game of dichotomy on the rationals + * in [1,2]. Then there are always questions we can ask but all these questions will + * never reach a leaf (a rational). + ***********************************************************************************) + +(* If a game is total and completely inhabited, then it's productive *) +Lemma TotalAndProperImpliesProductive : forall t (g : Game t), TotalGame g -> ProperGame g -> ProductiveGame g. +Proof. +intros t g TOTAL NONTRIV. +unfold TotalGame in TOTAL. +unfold ProductiveGame. intros. +unfold Everywhere. intros s n IN. +induction IN. +unfold ProperGame in NONTRIV. unfold Everywhere in NONTRIV. +specialize (NONTRIV s n (InsideSame n)). destruct NONTRIV. exists x. auto. + +apply IHIN. +intros. specialize (TOTAL (inv iso (inl _ x))). destruct (HasFinPathSplit TOTAL). + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. +apply (EverywhereSplit NONTRIV). + +apply IHIN. +intros. specialize (TOTAL (inv iso (inr _ x))). destruct (HasFinPathSplit TOTAL). + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. +apply (EverywhereSplit NONTRIV). +Qed. + +Lemma TotalAndProperImpliesEverywhereTotal : forall t (g : Game t), TotalGame g -> ProperGame g -> Everywhere TotalGame g. +Proof. +intros t g TOTAL NONTRIV. +unfold TotalGame in TOTAL. +unfold TotalGame. +unfold Everywhere. intros s n IN. +induction IN. +unfold ProperGame in NONTRIV. unfold Everywhere in NONTRIV. +specialize (NONTRIV s n (InsideSame n)). auto. + +apply IHIN. +intros. specialize (TOTAL (inv iso (inl _ x))). destruct (HasFinPathSplit TOTAL). + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. +apply (EverywhereSplit NONTRIV). + +apply IHIN. +intros. specialize (TOTAL (inv iso (inr _ x))). destruct (HasFinPathSplit TOTAL). + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. + destruct H as [y [H EQ]]. assert (EQ' := invInj EQ). congruence. +apply (EverywhereSplit NONTRIV). +Qed. + +(* The converse property is false, see note [INCOMPLETENESS] below *) + +(*====================================================================================== + Equality to level n; return None if not done, Some true if equal, Some false if unequal + ======================================================================================*) +Fixpoint eq t (g : Game t) (x y : t) (n:nat) := + match n with + | O => None + | S n' => + match g with + | Single _ => Some true + | Split _ _ iso g1 g2 => + match iso x, iso y with + | inl x1, inl x2 => eq g1 x1 x2 n' + | inr x1, inr x2 => eq g2 x1 x2 n' + | _, _ => Some false + end + end + end. + + + +(* Question: If the game is Productive (and Adequate), is the encoder + * guaranteed to terminate? [INCOMPLETENESS] Answer: + * Not necessarily. Imagine the type (option Nat). Imagine the sequence of + * questions: (are you Some 0 or the rest) + * (are you Some 1 or the rest) + * (are you Some 2 or the rest) ... + * At each level we do split the input space correctly so this sequence of + * questions is Adequate. And it is Productive as from every point in the + * game there exists a finite path to an element. But we will never terminate + * if we run on (None). [DIMITRIS: Check and Prove] + ******************************************************************************) +
+ Huffman.hs view
@@ -0,0 +1,76 @@+module Huffman where + + +import System( getArgs ) + +import Data.Char +import Iso +import Games +import BasicGames + +type Set a = [a] + +-- A simple priority queue, with integers corresponding +-- to frequencies; element with smallest frequency first +type PQ a = [(Int,a)] + +-- Add a *new* item to a priority queue +addItem :: Int -> a -> PQ a -> PQ a +addItem n x [] = [(n,x)] +addItem n x q@((n1,x1):qrest) + | n < n1 = (n,x) : q + | otherwise = (n1,x1) : addItem n x qrest + +-- Update the frequency of an existing item in a priority queue +updPQ :: Eq a => PQ a -> a -> PQ a +updPQ ((n,x):rest) y + | y == x = addItem (n+1) x rest + | otherwise = (n,x) : updPQ rest y + + +-- A game for Huffman +huff :: Eq a => PQ (Set a, Game a) -> Game a +huff [(_,(_,g))] = g +huff ((w1,(s1,g1)):(w2,(s2,g2)):wgs) + = huff $ addItem (w1+w2) (s1++s2, Split (splitIso (\n -> elem n s1)) g1 g2) wgs + +huffGame :: Eq a => PQ a -> Game a +huffGame pq = huff $ map (\(i,x) -> (i,([x], constGame x))) pq + +charHuffGame :: Game Char +charHuffGame = huffGame $ uniform ascii_chars + +ascii_chars = map chr [32..126] +uniform = map (\x -> (1,x)) + + +-- Static precomputed Huffman game +sHuffGame :: PQ Char -> Game [Char] +sHuffGame pq = listGame $ huffGame pq + +-- Dynamic Huffman game +dHuffGame :: PQ Char -> Game [Char] +dHuffGame pq = Split listIso unitGame $ + depGame (huffGame pq) (dHuffGame . updPQ pq) + + + +-- Let's save some more bits +vecHuffGame :: Nat -> PQ Char -> Game [Char] +vecHuffGame 0 pq = constGame [] +vecHuffGame (n+1) pq = depGame (huffGame pq) (vecHuffGame n . updPQ pq) +> nonemptyIso + + +lengthHuffGame :: PQ Char -> Game (Nat,[Char]) +lengthHuffGame pq = depGame binNatGame (\n -> vecHuffGame n pq) + +dHuffGame' pq = lengthHuffGame pq +> Iso h j + where h :: [t] -> (Nat,[t]) + h lst = (length lst, lst) + j :: (Nat,[t]) -> [t] + -- Precondition: n = length lst + j (n,lst) = lst + + +prodPQ :: PQ a -> PQ b -> PQ (a,b) +prodPQ p q = [ (m*n,(a,b)) | (m,a) <- p, (n,b) <- q ]
+ Iso.hs view
@@ -0,0 +1,127 @@+module Iso where + +-- An isomorphism +-- /Iso/ +-- (Iso to from) must satisfy +-- left inverse: from . to = id +-- right inverse: to . from = id +data ISO t s = Iso { to :: t -> s, from :: s -> t } +-- /End/ + +-- /Nat/ +type Nat = Int +-- /End/ + +-- Basic set-theoretic isos -------------------------------- + +-- /singleIso/ +singleIso :: a -> ISO a () +-- forall x:a, ISO {z | z = x} unit +singleIso x = Iso (const ()) (const x) +-- /End/ + +-- /splitIso/ +splitIso :: (a -> Bool) -> ISO a (Either a a) +-- forall p:a->bool, ISO a ({x|p x = true}+{x|p x = false}) +splitIso p = Iso ask bld + where ask x = if p x then Left x else Right x + bld x = case x of Left y -> y; Right y -> y +-- /End/ + +-- Some isomorphisms on concrete types --------------------- +-- /boolIso/ +boolIso :: ISO Bool (Either () ()) +boolIso = Iso ask bld where ask True = Left () + ask False = Right () + bld (Left ()) = True + bld (Right ()) = False +-- /End/ + +-- /succIso/ +succIso :: ISO Nat (Either () Nat) +succIso = Iso ask bld where ask 0 = Left () + ask (n+1) = Right n + bld (Left ()) = 0 + bld (Right n) = n+1 +-- /End/ + +-- /parityIso/ +parityIso :: ISO Nat (Either Nat Nat) +parityIso = Iso + (\n -> if even n then Left(n `div` 2) + else Right(n `div` 2)) + (\x -> case x of Left m -> m*2; Right m -> m*2+1) +-- /End/ + +-- /listIso/ +listIso :: ISO [t] (Either () (t,[t])) +listIso = Iso ask bld where ask [] = Left () + ask (x:xs) = Right (x,xs) + bld (Left ()) = [] + bld (Right (x,xs)) = x:xs +-- /End/ + +-- /depListIso/ +depListIso :: ISO [t] (Nat,[t]) +-- ISO (list t) { n:nat & t^n } +depListIso = Iso ask bld where ask xs = (length xs, xs) + bld (n,xs) = xs +-- /End/ + +-- Isomorphism combinators --------------------------------- +-- /AllIso/ +idI :: ISO a a +seqI :: ISO a b -> ISO b c -> ISO a c +sumI :: ISO a b -> ISO c d + -> ISO (Either a c) (Either b d) +prodI :: ISO a b -> ISO c d -> ISO (a,c) (b,d) +invI :: ISO a b -> ISO b a +swapProdI :: ISO (a,b) (b,a) +swapSumI :: ISO (Either a b) (Either b a) +assocProdI :: ISO (a,(b,c)) ((a,b),c) +assocSumI :: ISO (Either a (Either b c)) + (Either (Either a b) c) +prodLUnitI :: ISO ((),a) a +prodRUnitI :: ISO (a,()) a +prodRSumI :: ISO (a,Either b c) (Either (a,b) (a,c)) +prodLSumI :: ISO (Either b c, a) (Either (b,a) (c,a)) +-- /End/ + +idI = Iso id id +seqI (Iso i1 j1) (Iso i2 j2) = Iso (i2.i1) (j1.j2) +sumI (Iso i1 j1) (Iso i2 j2) + = Iso (either (Left . i1) (Right . i2)) + (either (Left . j1) (Right . j2)) +prodI (Iso i1 j1) (Iso i2 j2) + = Iso (\(x,y) -> (i1 x, i2 y)) + (\(x,y) -> (j1 x, j2 y)) +invI (Iso i j) = Iso j i + + +swapProdI = Iso sw sw + where sw (x,y) = (y,x) + +swapSumI = Iso sw sw + where sw = either Right Left + +assocProdI = Iso (\(x,(y,z)) -> ((x,y),z)) (\((x,y),z) -> (x,(y,z))) +assocSumI = Iso (\s -> case s of Left x -> Left (Left x); Right yz -> case yz of Left y -> Left (Right y); Right z -> Right z) + (\s -> case s of Left xy -> (case xy of Left x -> Left x; Right y -> Right (Left y)) ; Right z -> Right (Right z)) + +prodLUnitI = Iso snd (\x -> ((),x)) +prodRUnitI = Iso fst (\x -> (x,())) + + +prodRSumI = Iso f t + where f (x,Left z) = Left (x,z) + f (x,Right z) = Right (x,z) + t (Left (y,z)) = (y, Left z) + t (Right (y,z)) = (y, Right z) + +prodLSumI = Iso f t + where f (Left z, x) = Left (z,x) + f (Right z, x) = Right (z,x) + t (Left (y,z)) = (Left y, z) + t (Right (y,z)) = (Right y, z) + +
+ Iso.v view
@@ -0,0 +1,414 @@+Set Implicit Arguments. +Unset Strict Implicit. +Set Printing Implicit Defensive. +Set Transparent Obligations. + +Inductive Void := . + +(* An isomorphism between types whose maps are explicit functions *) +(*=Iso *) +Record ISO a b := Iso { + map :> a -> b; + inv : b -> a; + mapinv : forall x, inv (map x) = x; + invmap : forall y, map (inv y) = y }. +(*=End *) + +Implicit Arguments Iso [a b]. + +(* The inversion map of an isomorphism is injective *) +Lemma invInj : forall a b (iso : ISO a b) x y, inv iso x = inv iso y -> x = y. +Proof. +intros. +rewrite <- (invmap iso). rewrite <- H. rewrite invmap. reflexivity. +Qed. + +(* The map of an isomorphism is injective *) +Lemma isoInj : forall a b (iso : ISO a b) x y, iso x = iso y -> x = y. +Proof. +intros. +rewrite <- (mapinv iso). rewrite <- H. rewrite mapinv. reflexivity. +Qed. + +(* Identity isomorphism (reflexivity) *) +Definition idI t : ISO t t. +intros t. +refine (Iso (@id t) (@id t) _ _). +auto. auto. +Defined. + +(* Invert an isomorphism (symmetry) *) +Definition invI a b : ISO a b -> ISO b a. +intros a b iso. +refine (Iso (inv iso) (map iso) _ _). +intros. rewrite invmap. reflexivity. +intros. rewrite mapinv. reflexivity. +Defined. + +(* Compose two isomorphisms (transitivity) *) +Definition seqI a b c : ISO a b -> ISO b c -> ISO a c. +intros a b c i1 i2. +refine (Iso (fun x => i2 (i1 x)) (fun x => inv i1 (inv i2 x)) _ _). +intros. rewrite 2 mapinv. reflexivity. +intros. rewrite 2 invmap. reflexivity. +Defined. + +(* Sum *) +Definition sumI a b c d : ISO a b -> ISO c d -> ISO (a+c) (b+d). +intros a b c d i1 i2. +refine (Iso (fun x => match x with inl y => inl _ (i1 y) | inr z => inr _ (i2 z) end) + (fun x => match x with inl y => inl _ (inv i1 y) | inr z => inr _ (inv i2 z) end) _ _). +intros x. destruct x; rewrite mapinv; reflexivity. +intros x. destruct x; rewrite invmap; reflexivity. +Defined. + +(* Product is a congruence *) +Definition prodI a b c d : ISO a b -> ISO c d -> ISO (a*c) (b*d). +intros a b c d i1 i2. +refine (Iso (fun x => (i1 (fst x), i2 (snd x))) (fun y => (inv i1 (fst y), inv i2 (snd y))) _ _). +intros p. simpl. rewrite 2 mapinv. destruct p; reflexivity. +intros p. simpl. rewrite 2 invmap. destruct p; reflexivity. +Defined. + +(* Dependent pair is a congruence *) +Definition depProdI a b C D : ISO a b -> (forall (x:a) (y:b), ISO (C x) (D y)) -> ISO {x:a & C x} {y:b & D y}. +intros a b C D i1 i2. +refine (Iso (fun z => match z with existT x Cx => existT (fun x => D x) (i1 x) ((i2 x (i1 x)) _) end) + (fun z => match z with existT y Dy => existT (fun x => C x) (inv i1 y) (inv (i2 (inv i1 y) y) Dy) end) _ _). +intros [x Cx]. rewrite 2 mapinv. reflexivity. +intros [y Dy]. rewrite 2 invmap. reflexivity. +Defined. + +(* Void is isomorphic to empty dependent pair *) +Definition voidI t : ISO Void { x:t | False }. +intros t. +refine (Iso (fun (H:Void) => match H with end) (fun (p:{x:t | False}) => let (_,f) := p in match f with end) _ _). +intros. destruct x. +intros. destruct y. destruct f. +Defined. + + +(* Swap isomorphism (commutativity of product) *) +Definition swapProdI a b : ISO (a*b) (b*a). +intros a b. +refine (Iso (fun x => (snd x, fst x)) (fun x => (snd x, fst x)) _ _). +intros. destruct x; auto. +intros. destruct y; auto. +Defined. + +(* Swap choice isomorphism (commutativity of sum) *) +Definition swapSumI a b : ISO (a+b) (b+a). +intros a b. +refine (Iso (fun x => match x with inl x => inr _ x | inr x => inl _ x end) (fun x => match x with inl x => inr _ x | inr x => inl _ x end) _ _). +intros. destruct x; auto. destruct y; auto. +Defined. + +Definition assocSumI a b c : ISO (a+(b+c)) ((a+b)+c). +intros a b c. +refine (Iso (fun x => match x with inl x => inl _ (inl _ x) | inr x => match x with inl y => inl _ (inr _ y) | inr y => inr _ y end end) + (fun x => match x with inl x => match x with inl y => inl _ y | inr y => inr _ (inl _ y) end | inr y => inr _ (inr _ y) end) _ _). +intros. destruct x; auto. destruct s; auto. destruct y; auto. destruct s; auto. +Defined. + +Definition assocSwapSumI a b c : ISO (a+(b+c)) ((b+a)+c). +intros a b c. +refine (Iso (fun x:a+(b+c) => match x with inl x => inl _ (inr _ x) | inr x => match x with inl y => inl _ (inl _ y) | inr y => inr _ y end end) + (fun x:(b+a)+c => match x with inl x => match x with inl y => inr _ (inl _ y) | inr y => inl _ y end | inr y => inr _ (inr _ y) end) _ _). +intros. destruct x; auto. destruct s; auto. destruct y; auto. destruct s; auto. +Defined. + +Definition prodRSumI a b c : ISO (a*(b+c)) (a*b + a*c). +intros a b c. +refine (Iso + (fun x => match snd x with inl y => inl _ (fst x, y) | inr z => inr _ (fst x, z) end) + (fun x => match x with inl y => (fst y, inl _ (snd y)) | inr z => (fst z, inr _ (snd z)) end) _ _). +intros [x y]. simpl. destruct y; auto. +intros y. destruct y. destruct p. auto. destruct p. auto. +Defined. + +Definition depProdRSumI a B C : (ISO { x:a & B x + C x } ({ x:a & B x } + { x:a & C x }))%type. +intros a B C. +refine (Iso + (fun x => match projT2 x with inl y => inl _ (existT (fun z => B z) (projT1 x) y) | inr z => inr _ (existT (fun z => C z) (projT1 x) z) end) + (fun x => match x with inl y => existT _ (projT1 y) (inl _ (projT2 y)) | inr z => existT _ (projT1 z) (inr _ (projT2 z)) end) _ _). +intros [x y]. simpl. destruct y; auto. +intros y. destruct y. destruct s. auto. destruct s. auto. +Defined. + + +Definition prodLSumI a b c : ISO ((a+b)*c) (a*c + b*c). +intros a b c. +refine (Iso + (fun x => match fst x with inl y => inl _ (y, snd x) | inr z => inr _ (z, snd x) end) + (fun x => match x with inl y => (inl _ (fst y), snd y) | inr z => (inr _ (fst z), snd z) end) _ _). +intros [x y]. simpl. destruct x; auto. +intros y. destruct y; destruct p; auto. +Defined. + +Definition prodR a b c : ISO a b -> ISO (a*c) (b*c) := fun i => prodI i (idI _). +Definition prodL a b c : ISO a b -> ISO (c*a) (c*b) := prodI (idI _). + +Definition prodRUnitI t : ISO (t*unit) t. +intros t. +refine (Iso (fun x => fst x) (fun x => (x,tt)) _ _). +intros. destruct x. simpl. destruct u. reflexivity. +intros. auto. +Defined. + +Definition prodLUnitI t : ISO (unit*t) t. +intros t. +refine (Iso (fun x => snd x) (fun x => (tt,x)) _ _). +intros. destruct x. simpl. destruct u. reflexivity. +intros. auto. +Defined. + +Definition depProdLUnitI T : ISO { x:unit & T x } (T tt). +intros T. +refine (Iso (fun x => match x with existT tt Tx => Tx end) (fun x => existT _ tt x) _ _). +intros [x Tx]. destruct x. reflexivity. intros. reflexivity. +Defined. + +Definition getSingleton t (iso : ISO t unit) : t := inv iso tt. +Lemma uniqueSingleton t (iso : ISO t unit) : forall (x:t), x = getSingleton iso. +Proof. intros. unfold getSingleton. +assert (iso x = iso (inv iso tt)). +generalize (iso x). destruct u. rewrite invmap. reflexivity. +assert (inv iso (iso x) = inv iso (iso (inv iso tt))). +rewrite <- H. reflexivity. rewrite invmap in H0. rewrite mapinv in H0. assumption. +Qed. + +(*--------------------------------------------------------------------------------- + Now for some concrete isomorphisms + ---------------------------------------------------------------------------------*) + +(* Bool is isomorphic to sum of units *) +Definition boolIso : ISO bool (unit + unit). +refine (Iso (fun x:bool => if x then inl _ tt else inr _ tt) (fun x => match x with inl _ => true | inr _ => false end) _ _). +destruct x; auto. +destruct y; destruct u; auto. +Defined. + +Require Import Div2. +Require Import Even. + +Fixpoint isEven (n : nat) := + match n with + | O => true + | S n' => isOdd n' + end +with isOdd (n : nat) := + match n with + | O => false + | S n' => isEven n' + end. + +Require Import Bool. +Lemma isEvenOdd : forall n, isEven n = negb (isOdd n). +Proof. +induction n. auto. simpl. rewrite IHn. rewrite Bool.negb_involutive. reflexivity. +Qed. + +Corollary isEvenOddAux : forall n, isOdd n = negb (isEven n). +intros. +rewrite isEvenOdd. rewrite Bool.negb_involutive. reflexivity. +Qed. + +Lemma EvenOddDec : forall n, (isEven n = true <-> even n) /\ (isOdd n = true <-> odd n). +Proof. +induction n. split. + split. intros _. apply even_O. + intros _. auto. + split. intros H. simpl in H. discriminate H. intros H. inversion H. + +split. +destruct IHn as [[H1 H2] [H3 H4]]. +split. intuition. +simpl. intros H5. inversion H5. auto. +split. +destruct IHn as [[H1 H2] [H3 H4]]. +simpl. intros H. apply odd_S. auto. +intros H. inversion H. firstorder. +Qed. + +Lemma isEvenDouble : forall n, isEven (double n) = true. +Proof. induction n; auto. simpl. replace (n + S n) with (S (n+n)); auto. +Qed. +Lemma isOddDouble : forall n, isOdd (double n) = false. +Proof. induction n; auto. simpl. replace (n + S n) with (S (n+n)); auto. +Qed. + + +Definition succIso : ISO nat (unit + nat). +refine (Iso + (fun x => match x with O => inl _ tt | S y => inr _ y end) + (fun x => match x with inl tt => 0 | inr y => S y end) + _ _). +induction x; auto. +intros. destruct y. destruct u. reflexivity. reflexivity. +Defined. + + +(*====================================================================================== + Isomorphism between N and N+N, based on parity + ======================================================================================*) +Definition parityIso : ISO nat (nat + nat). +refine (Iso + (fun x => let y := div2 x in if isEven x then inl _ y else inr _ y) (fun x => match x with inl x => double x | inr x => S (double x) end) _ _). +(* First axiom *) +intros. case_eq (isEven x). intros H. +assert (even x). assert (EOD := EvenOddDec). firstorder. +assert (H1 := proj1 (proj1 (even_odd_double x)) H0). auto. +intros. +rewrite isEvenOdd in H. assert (H' := Bool.negb_sym _ _ (sym_equal H)). simpl in H'. +assert (odd x). assert (EOD := EvenOddDec). firstorder. +assert (H1 := proj1 (proj2 (even_odd_double x)) H0). auto. +(* Second axiom *) +intros. destruct y. simpl. rewrite isEvenDouble. assert (double n = 2*n). simpl. unfold double. auto. rewrite H. rewrite div2_double. reflexivity. +simpl isEven. +assert (double n = 2*n). simpl. unfold double. auto. rewrite H. rewrite div2_double_plus_one. +replace (2*n) with (double n). rewrite isOddDouble. trivial. +Defined. + + +Require Import List. +(*====================================================================================== + Representation of lists + ======================================================================================*) +Definition listIso t : ISO (list t) (unit + t * list t). +intros t. +refine (Iso (fun xs => match xs with nil => inl _ tt | x::xs => inr _ (x,xs) end) + (fun z => match z with inl tt => nil | inr (x,xs) => x::xs end) _ _). +intros. destruct x; auto. +intros. destruct y. destruct u. auto. destruct p. auto. +Defined. + +Require Import NaryFunctions. +Require Import List. + +Fixpoint list_to_nprodsum t (x:list t) : { n:nat & t^n } := + match x with + | nil => existT (fun n => t^n) 0 tt + | x::xs => + let r := list_to_nprodsum xs in + existT (fun n => t^n) (S (projT1 r)) (x,projT2 r) + end. + +Definition depListIso t : ISO (list t) {n:nat & t^n}. +Proof. intros t. +refine (Iso (@list_to_nprodsum t) (fun (p:{n:nat & t^n}) => nprod_to_list _ (projT1 p) (projT2 p)) _ _). + +intros. simpl. induction x. auto. simpl. rewrite IHx. auto. + +intros. simpl. destruct y as [n p]. induction n. destruct p. auto. destruct p as [y ys]. fold nprod in ys. simpl in IHn. +simpl. specialize (IHn ys). rewrite IHn. auto. +Defined. + + +(*====================================================================================== + Set-theoretic splitting + ======================================================================================*) +Definition boolSplitIsoMap t (p:t->bool) (x:t) : {y | p y = true} + {y | p y = false}. +intros t p x. +case_eq (p x). +intros H. +left. exists x. assumption. +right. exists x. assumption. +Defined. + +Print boolSplitIsoMap. +Definition boolSplitIsoInv t (p:t->bool) (s:{y | p y = true} + {y | p y = false}) : t. +intros t p s. +destruct s; exact (projT1 s). +Defined. +Print boolSplitIsoInv. + +Require Import ProofIrrelevance. +Definition splitIso t (p : t -> bool) : ISO t ({y | p y = true } + {y | p y = false}). +intros t p. +refine (Iso (boolSplitIsoMap p) (@boolSplitIsoInv t p) _ _). +intros x. admit. +destruct y. simpl. destruct s. simpl. admit. +admit. +Defined. + +Definition singleIso t (k:t) : ISO { x | x=k } unit. +intros t k. +refine (Iso (fun _ => tt) (fun _ => exist _ k (refl_equal k)) _ _). +admit. (* +intros [x EQ]. Set Printing All. Show . assert (SEC := @subset_eq_compat). apply (subset_eq_compat t (fun x0 => x0=k) k x (refl_equal k) EQ). assert (EQ = refl_equal k). Heq EQ. inversion EQ. Require Import Program.Tactics. dependent destruction EQ. trivial. *) +destruct y. trivial. +Defined. + + +(* Construct an isomorphism between a type X and a subset of a type Y defined by P : Y -> Prop *) +Require Import ProofIrrelevance. +Definition subsetIso + X (* The source *) + Y (P:Y -> Prop) (* The target, with domain *) + (i:X -> Y) (* The map from source to target *) + (iP : forall x:X, P (i x)) (* The map lands in the domain of the target *) + (j : forall y:Y, P y -> X) (* The map from target to source *) + (ij : forall x, j (i x) (iP x) = x) (* Round-tripping from source works *) + (ji : forall y:Y, forall (p:P y), i (j y p) = y) (* Round-tripping from target works *) + : ISO X {y:Y & P y}. +intros. +refine (Iso (fun x => existT _ (i x) _) (fun z:{y:Y & P y} => j (projT1 z) (projT2 z)) _ _). + +simpl. auto. + +destruct y. simpl. apply subsetT_eq_compat. auto. +Defined. + + +(*Definition isLeft a b (x:a+b) := match x with inl _ => True | _ => False end. +Definition isRight a b (x:a+b) := match x with inr _ => True | _ => False end. + +(* Or maybe: *) +Definition makeSubset a (pred : a -> bool) : a -> {y:a & pred y = true } + {y:a & pred y = false}. +intros a pred y. +case_eq (pred y). +intros EQ. +exact (inl _ (existT _ y EQ)). +intros EQ. +exact (inr _ (existT _ y EQ)). +Defined. + + +Print makeSubset. + +(* +Definition MakeSubset a (pred : a -> bool) (x : a) := +(if pred x as b return {y : a & pred y = true} + {y : a & pred y = false} + then +(* fun EQ : pred y = true => *) + inl _ (existT (fun y0 : a => pred y0 = true) x (@refl_equal _ (pred x))) + else +(* fun EQ : pred y = false => *) + inr {y0 : a & pred y0 = true} + (existT (fun y0 : a => pred y0 = false) x (*EQ*))) + (*(refl_equal (pred y))*). + +*) + +(* +Add LoadPath "C:\coq\heq-0.9\src". + +Require Import Heq. +*) +Definition boolSplitIso a (pred : a -> bool) : ISO a ({y:a & pred y = true } + {y:a & pred y = false}). +intros. +refine (@Iso _ _ (makeSubset pred) (fun z => match z with inl y => projT1 y | inr y => projT1 y end) _ _). +intros x. admit. +destruct y. unfold makeSubset. + destruct s. simpl. generalize (refl_equal (pred x)). rewrite e. + destruct s. unfold makeSubset. simpl. assert ( +( fun EQ : false = false => + inr {y : a & pred y = true} ({{fun y : a => pred y = false # x, EQ}})) + (refl_equal (false)) = + inr {y : a & pred y = true} ({{fun y : a => pred y = false # x, e}}) +). + +admit. +Defined. + +*)
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c)2010, Dimitrios Vytiniotis and Andrew Kennedy++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Dimitrios Vytiniotis and Andrew Kennedy nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Main.hs view
@@ -0,0 +1,18 @@+module Main where + +import System +import Games +import Huffman +import Data.List +import Data.Char + +-- Silly experiment +main :: IO () +main = do { (fn:_) <- getArgs + ; contents <- readFile fn + ; let minc = minimumBy compare contents + maxc = maximumBy compare contents + chars = map (\c -> (1,chr c)) [(ord minc)..(ord maxc)] + ; let bitstring = enc (dHuffGame' chars) contents + ; putStrLn $ "Bytes needed: " ++ (show $ (length bitstring) `div` 8) + }
+ NatGames.hs view
@@ -0,0 +1,57 @@+{-# options_ghc -XEmptyDataDecls -XOverlappingInstances -XScopedTypeVariables #-} +module NatGames where + +import Data.Maybe +import Iso +import Games +import BasicGames + +-- positive integers +type Pos = Int + +-- /Elias/ +power2 0 = 1 +power2 (n+1) = 2 * power2 n + +log2 1 = 0 +log2 n = 1 + log2 (n `div` 2) + +-- binaryIso :: ISO Pos (n:Nat, [0,2^n-1]) +binaryIso :: ISO Pos (Nat,Pos) +binaryIso = Iso (\p -> (log2 p, p)) snd + +-- Parameterized on a game for encoding the number of bits +eliasGame :: Game Nat -> Game Pos +eliasGame natGame = depGame natGame (\n -> let m = power2 n in rangeGame m (2*m - 1)) +> binaryIso + +-- The Elias gamma game for positive integers: +-- First encode the number of bits - 1 in unary, then the binary rep of the number, without the leading one +gammaGame = eliasGame unaryNatGame + +isOneIso :: ISO Pos (Either () Pos) +isOneIso = Iso ask bld + where ask 1 = Left () + ask n = Right n + bld (Left ()) = 1 + bld (Right n) = n + +-- The Elias omega game: +-- Recursively apply the game to the number of bits +omegaGame = Split isOneIso unitGame (eliasGame omegaGame) +-- /End/ + +primes = sieve [2..] + where + sieve (p:xs) = p : sieve [x | x<-xs, x `mod` p /= 0] + + +factIso :: [Int] -> ISO Int (Either Int Int) +factIso (p:ps) = + Iso (\n -> let (d,r) = divMod n p in if r==0 then Left d else Right n) + (\z -> case z of Left d -> d*p; Right n -> n) + +factPosGame ps = Split isOneIso unitGame (factPosNotOneGame ps) +factPosNotOneGame (p:ps) = Split (factIso (p:ps)) (factPosGame (p:ps)) (factPosNotOneGame ps) + +factGame :: Game Pos +factGame = factPosGame primes
+ PBasicGames.hs view
@@ -0,0 +1,291 @@+{-# options_ghc -XEmptyDataDecls -XOverlappingInstances -XScopedTypeVariables -XGADTs #-} +module PBasicGames where + +import Data.Maybe +import Iso +import PGames +import List + +type Nat = Int + +-- Game for () + +-- /boolGame/ +unitGame :: Game () +unitGame = Single (Iso (\() -> ()) (\() -> ())) + +boolIso :: ISO Bool (Either () ()) +boolIso = + Iso (\b -> if b then Left() else Right()) + (\x -> case x of Left() -> True; Right() -> False) + +boolGame :: Game Bool +boolGame = split boolIso unitGame unitGame +-- /End/ + + +-- /constGame/ +constGame :: t -> Game t +constGame k = Single (Iso (const ()) (const k)) +-- /End/ + + +-- Games for natural numbers +parityIso :: ISO Int (Either Int Int) +parityIso = Iso + (\n -> if even n then Left (n `div` 2) else Right (n `div` 2)) + (\x -> case x of Left m -> m*2; Right m -> m*2+1) + + +-- /geNatGame/ +-- geNatGame k returns a game for { n:Nat | n >= k } +geNatGame :: Nat -> Game Nat +geNatGame k = split iso (constGame k) (geNatGame (k+1)) + where iso :: ISO Nat (Either Nat Nat) + iso = Iso ask bld + -- Precondition of ask x: x >= k + ask x = if x == k then Left x else Right x + bld (Left x) = x + bld (Right x) = x +-- /End/ + +-- /unaryNatGame/ +succIso :: ISO Nat (Either () Nat) +succIso = Iso ask bld + where ask 0 = Left () + ask (n+1) = Right n + bld (Left ()) = 0 + bld (Right n) = n+1 + +unaryNatGame :: Game Nat +unaryNatGame = split succIso unitGame unaryNatGame +-- /End/ + +-- /encUnaryNat/ +encUnaryNat x = case x of 0 -> 1 : [] + n+1 -> 0 : encUnaryNat n +-- /End/ + + +-- /binNatGame/ +binNatGame :: Game Nat +binNatGame = split succIso unitGame divG + where divG = split (Iso ask bld) binNatGame binNatGame + ask n | even n = Left (n `div` 2) + | otherwise = Right (n `div` 2) + bld (Left m) = 2*m + bld (Right m) = 2*m+1 +-- /End/ + +-- /natGameFunny/ +natGameFunny :: Game Nat +natGameFunny = split (Iso ask bld) (constGame 0) gfunny + where ask n = if n == 0 then Left n else Right n -- Are you 0 or not? + bld (Left n) = n + bld (Right n) = n + + gfunny = split evi binNatGame (split pred_evi binNatGame voidNatGame) + evi = Iso (\n -> if even n then Left (n `div` 2) else Right n) -- Are you even or not? + (either (\n->2*n) id) + pred_evi = Iso (\(n+1) -> if even n then Left (n `div` 2) else Right (n+1)) -- Is your predecessor odd or not? + (either (\n->2*n+1) id) + + voidNatGame :: Game Nat + -- In reality: Game { x: Nat | x > 0 /\ x odd /\ x-1 odd } + voidNatGame = split voidi voidNatGame voidNatGame + -- Empty set is disjoint with any set so voidi *is* an isomorphism + voidi = Iso (\x -> Right x) bld +-- /End/ + +binNatGameFunny :: Game Nat +binNatGameFunny = split (Iso ask bld) zOneG divG + where zOneG = split (Iso askz bldz) (constGame 0) + (constGame 1) + askz 0 = Left 0 + askz 1 = Right 1 + bldz (Right 1) = 1 + bldz (Left 0) = 0 + -- the rest as in binNatGame +-- /End/ + ask 0 = Left 0 + ask (n+1) = Right n + bld (Left 0) = 0 + bld (Right n) = n+1 + + divG = split iso binNatGame binNatGame + iso = Iso ask' bld' + ask' n = if even n then Left (n `div` 2) + else Right (n `div` 2) + bld' (Left m) = 2*m + bld' (Right m) = 2*m+1 + + + +-- Flip the meaning of the bits +{- +flipGame :: Game a -> Game a +flipGame (Split iso f1 g1 f0 g0) = Split (iso `seqI` swapSumI) f0 (flipGame g0) f1 (flipGame g1) +flipGame g = g +-} + +-- A game for sums +-- /sumGame/ +sumGame :: Game t -> Game s -> Game (Either t s) +sumGame = split idI +-- /End/ + + +-- A game for products, based on appending +-- /prodGame/ +data ProdGamesResult s t where + PGR :: ISO (s,t) s' -> GamesOver s' -> ProdGamesResult s t + +prodGame :: forall t s. Game t -> Game s -> Game (t,s) +prodGame (Single iso) g = g +> iso' + where iso' :: ISO (t,s) s -- assuming ISO t () + iso' = prodI iso idI `seqI` prodLUnitI +prodGame (Split (Iso i j) gs) g = + case prodGames gs of + PGR (Iso i' j') gs' -> + Split (Iso (\(x,y) -> i' (i x, y)) (\z -> let (x,y) = j' z in (j x,y))) gs' + where + prodGames :: forall sum. GamesOver sum -> ProdGamesResult sum s + prodGames gs = + case gs of + NilGames -> PGR (Iso (\_ -> error "should not happen") (\_ -> error "should not happen")) NilGames + ConsGames w ga gsa -> + case prodGames gsa of + PGR (Iso i j) gs'' -> PGR (Iso (\(x,y) -> case x of Left xl -> Left (xl,y); Right xr -> Right (i (xr,y))) + (\x -> case x of Left (y,z) -> (Left y,z); Right z -> let (z1,z2) = j z in (Right z1,z2))) (ConsGames w (prodGame ga g) gs'') + + +-- /End/ + +-- A game for products, based on interleaving +-- /ilGame/ + {- +ilGame :: forall t s. Game t -> Game s -> Game (t,s) +ilGame (Single iso) g2 = g2 +> iso' + where iso' :: ISO (t,s) s -- assuming ISO t () + iso' = prodI iso idI `seqI` prodLUnitI +ilGame (Split (iso :: ISO t (Either ta tb)) f1a g1a f1b g1b) g2 + = Split iso' f1a (ilGame g2 g1a) f1b (ilGame g2 g1b) + where iso' :: ISO (t,s) (Either (s,ta) (s,tb)) + iso' = swapProdI `seqI` prodI idI iso + `seqI` prodRSumI +-} +-- /End/ + + +-- /depGame/ + +depGame :: forall t s. Game t -> (t -> Game s) -> Game (t,s) +depGame (Single iso) f = f (from iso ()) +> iso' + where iso' = prodI iso idI `seqI` prodLUnitI +depGame (Split (Iso i j) gs) f = + case depGames gs (f . j) of + PGR (Iso i' j') gs' -> Split (Iso (\(x,y) -> i' (i x, y)) (\z -> let (x,y) = j' z in (j x,y))) gs' + where + depGames :: forall sum. GamesOver sum -> (sum -> Game s) -> ProdGamesResult sum s + depGames gs f = + case gs of + NilGames -> PGR (Iso (\_ -> error "should not happen") (\_ -> error "should not happen")) NilGames + ConsGames w ga gsa -> + case depGames gsa (f . Right) of + PGR (Iso i'' j'') gs'' -> + PGR (Iso (\(x,y) -> case x of Left xl -> Left (xl,y); Right xr -> Right (i'' (xr,y))) + (\x -> case x of Left (y,z) -> (Left y,z); Right z -> let (z1,z2) = j'' z in (Right z1,z2))) + (ConsGames w (depGame ga (f . Left)) gs'') + +-- /End/ + + + + + +getRight (Right x) = x +getLeft (Left x) = x + + +nonemptyIso = Iso (\(x:xs) -> (x,xs)) (\(x,xs) -> x:xs) + + + +-- /vecGame/ +vecGame :: Game t -> Nat -> Game [t] +-- /End/ +vecGame g 0 = constGame [] +vecGame g (n+1) = prodGame g (vecGame g n) +> nonemptyIso + +-- /lengthListGame/ +lengthListGame :: Game t -> Game (Nat,[t]) +lengthListGame g = depGame binNatGame (vecGame g) + +listGame' :: forall t. Game t -> Game [t] +listGame' g = lengthListGame g +> Iso h j + where h :: [t] -> (Nat,[t]) + h lst = (length lst, lst) + j :: (Nat,[t]) -> [t] + -- Precondition: n = length lst + j (n,lst) = lst +-- /End/ + + + +-- A game for lists, using sum-of-products +-- /listGame/ +listIso :: ISO [t] (Either () (t,[t])) +listIso = Iso ask bld + where ask [] = Left () + ask (x:xs) = Right (x,xs) + bld (Left ()) = [] + bld (Right (x,xs)) = x:xs + +listGame :: Game t -> Game [t] +listGame g = + split listIso unitGame (prodGame g (listGame g)) + +-- Parameterized on how much more likely a Cons is than a Nil +biasedListGame :: Int -> Game t -> Game [t] +biasedListGame n g = + split2 listIso 1 unitGame n (prodGame g (biasedListGame n g)) +-- /End/ + + +-- /rangeGame/ +-- Precondition for rangeGame k1 k2: k1 <= k2 +rangeGame :: Nat -> Nat -> Game Nat +rangeGame k1 k2 | k1 == k2 = constGame k1 +rangeGame k1 k2 = split (Iso ask bld) g1 g2 + where g1 = rangeGame (m+1) k2 + g2 = rangeGame k1 m + ask x = if x > m then Left x else Right x + bld (Left x) = x + bld (Right x) = x + m = (k1 + k2) `div` 2 +-- /End/ + + +data Tree = Leaf | Node Tree Tree deriving Show + +tiso = Iso ask bld + where ask (Leaf) = Left () + ask (Node t1 t2) = Right (t1,t2) + bld (Left ()) = Leaf + bld (Right (t1,t2)) = Node t1 t2 + +treeGame1 = split tiso (Single idI) (prodGame treeGame1 treeGame1) + +{-treeGame2 = split tiso (Single idI) (ilGame treeGame2 treeGame2)-} + +ones :: [Bit] +ones = 1:ones + +biasedBool = split2 boolIso 3 unitGame 1 unitGame +biasedBoolTriple = prodGame biasedBool (prodGame biasedBool biasedBool) + + +data Three = A | B | C +threeGame = split3 (flat3 (Iso (\x -> case x of A -> Left (); B -> Right (Left ()); C -> Right (Right ())) + (\x -> case x of Left () -> A; Right (Left ()) -> B; Right (Right ()) -> C))) + 1 unitGame 1 unitGame 1 unitGame
+ PGames.hs view
@@ -0,0 +1,162 @@+{-# options_ghc -XGADTs -XKindSignatures -XFlexibleInstances -XOverlappingInstances -XScopedTypeVariables -XEmptyDataDecls #-} +module PGames where + +import Random +import Iso +import Debug.Trace + +-- A game for type t, Game t, is a potentially infinite decision tree +-- with extra information about how to ask questions in the branches, +-- and elements of the datatype in the leaves. +-- We now include probabilities in the branches + +-- /Game/ +-- More general would be n-ary nodes, subsuming Split and Single +-- Easier in Coq, where we can define +-- Split : forall (a : list {t:Type & nat * Game t}), ISO t (SumOver a) -> Type +data Void + +data GamesOver :: * -> * where + NilGames :: GamesOver Void + ConsGames :: Int -> Game t -> GamesOver s -> GamesOver (Either t s) + +data Game :: * -> * where + Single :: ISO t () -> Game t + Split :: ISO t s -> GamesOver s -> Game t + +totalWeight :: GamesOver s -> Int +totalWeight NilGames = 0 +totalWeight (ConsGames w _ go) = w + totalWeight go + +split3 :: ISO t (Either t1 (Either t2 (Either t3 Void))) -> Int -> Game t1 -> Int -> Game t2 -> Int -> Game t3 -> Game t +split3 i w1 g1 w2 g2 w3 g3 = Split i (ConsGames w1 g1 $ ConsGames w2 g2 $ ConsGames w3 g3 $ NilGames) + +flat2 :: ISO t (Either t1 t2) -> ISO t (Either t1 (Either t2 Void)) +flat2 (Iso i j) = Iso (\x -> case i x of Left y -> Left y; Right z -> Right (Left z)) + (\x -> case x of Left y -> j (Left y); Right (Left z) -> j (Right z)) + +flat3 :: ISO t (Either t1 (Either t2 t3)) -> ISO t (Either t1 (Either t2 (Either t3 Void))) +flat3 (Iso i j) = Iso (\x -> case i x of Left y -> Left y; Right (Left z) -> Right (Left z); Right (Right z) -> Right (Right (Left z))) + (\x -> case x of Left y -> j (Left y); Right (Left z) -> j (Right (Left z)); Right (Right (Left z)) -> j (Right (Right z))) + +split2 :: ISO t (Either t1 t2) -> Int -> Game t1 -> Int -> Game t2 -> Game t +split2 i w1 g1 w2 g2 = Split (flat2 i) (ConsGames w1 g1 $ ConsGames w2 g2 $ NilGames) + +split :: ISO t (Either t1 t2) -> Game t1 -> Game t2 -> Game t +split i g1 g2 = split2 i 1 g1 1 g2 +-- /End/ + +-- Coerce a game, via an isomorphism +-- /coerceGame/ +(+>) :: Game t -> ISO s t -> Game s +(Single j) +> i = Single (i `seqI` j) +(Split j gs) +> i = Split (i `seqI` j) gs +-- /End/ + +infixl 4 +> + +-- /Bit/ +type Bit = Int -- 0 or 1 +-- /End/ + +type MInterval = (Int,Int,Int) + +-- Interval is specified by lower and upper bounds +type Interval = (Int,Int) + +-- Expanded interval +type EInterval = (Int,Interval) + +w1, w2, w3, w4 :: Int +w1 = 08192 --- 2^13 = w4/4 +w2 = 16384 --- 2^14 = w4/2 +w3 = 24576 --- 3*2^13 = 3*w4/4 +w4 = 32768 --- 2^15 = w4 + +e :: Int +e = 15 + +unit :: Interval +unit = (0,w4) + +narrow :: Interval -> MInterval -> Interval +narrow (l,r) (p,q,d) = (l + (w*p) `div` d, l + (w*q) `div` d) + where w = r-l + +nextBits :: EInterval -> Maybe ([Bit],EInterval) +nextBits (n,(l,r)) + | r <= w2 = Just (bits n 0,(0,(2*l,2*r))) + | w2 <= l = Just (bits n 1,(0,(2*l-w4,2*r-w4))) + | otherwise = Nothing + +enarrow :: EInterval -> MInterval -> EInterval +enarrow ei int2 = (n,narrow int1 int2) + where (n,int1) = expand ei + +expand :: EInterval -> EInterval +expand (n,(l,r)) + | w1 <= l && r <= w3 = expand (n+1,(2*l - w2,2*r - w2)) + | otherwise = (n,(l,r)) + +bits :: Int -> Bit -> [Bit] +bits n b = b:replicate n (1-b) + +stream :: EInterval -> [MInterval] -> [Bit] +stream z xs = case nextBits z of + Just(y,z') -> y ++ stream z' xs + Nothing -> case xs of + [] -> [] + x:xs -> stream (enarrow z x) xs + +arithEncAux :: EInterval -> Game t -> t -> [Bit] +arithEncAux ei g x = stream ei (encodeSyms g x) + +encodeSyms :: Game t -> t -> [MInterval] +encodeSyms (Single _) x = [] +encodeSyms (Split (Iso ask _) gs) x = encodeSym 0 gs (ask x) + where encodeSym :: Int -> GamesOver t -> t -> [MInterval] + encodeSym n (ConsGames w g gs) x = + case x of + Left y -> (n,n+w,total) : encodeSyms g y + Right z -> encodeSym (n+w) gs z + total = totalWeight gs + +enc :: Game t -> t -> [Bit] +enc = arithEncAux (0,unit) + +decode :: EInterval -> [Bit] -> Game t -> t +decode ei bs g = destream ei (c,ds) g + where c = foldl (\x b -> 2*x + b) 0 cs + (cs,ds) = splitAt e (bs ++ 1:replicate (e-1) 0) + +ominus :: (Int,[Bit]) -> [Bit] -> (Int,[Bit]) +ominus (c,ds) bs = foldl op (c,ds) bs + where op (c,ds) b = (2*c - w4*b + head ds,tail ds) + +fscale :: (Int,(Int,[Bit])) -> Int +fscale (n,(x,ds)) = foldl step x (take n ds) + where step x b = 2*x + b - w2 + +destream :: EInterval -> (Int, [Bit]) -> Game t -> t +destream ei w g = case nextBits ei of + Just (y,ei') -> destream ei' (ominus w y) g + Nothing -> + case g of + Single (Iso _ bld) -> bld () + Split (Iso _ bld) gs ->decodeSym bld gs 0 + where + (n,(l,r)) = expand ei + k = fscale (n,w) + t = ((k-l+1)*d - 1) `div` (r-l) + d = totalWeight gs + + decodeSym :: (s -> t) -> GamesOver s -> Int -> t + decodeSym bld (ConsGames weight g gs) n = + if n' > t then bld (Left (destream (enarrow ei (n,n',d)) w g)) + else decodeSym (bld . Right) gs n' + where n' = n+weight + +dec g bs = decode (0,unit) bs g + +testGame :: Game t -> t -> t +testGame g = dec g . enc g
+ PSTLC.hs view
@@ -0,0 +1,152 @@+{-# OPTIONS_GHC -fglasgow-exts #-} +module PSTLC where + +import Iso +import PGames +import PBasicGames + +import Data.Maybe +import FilterGames + +-- Simple types +-- /TyExp/ +data Ty = TyNat | TyArr Ty Ty deriving (Eq, Show) +data Exp = Var Nat | Lam Ty Exp | App Exp Exp +-- /End/ + deriving (Eq,Show) + +-- Game for types +-- /tyG/ +tyGame :: Game Ty +tyGame = Split (Iso ask bld) + (constGame TyNat) (prodGame tyGame tyGame) + where ask TyNat = Left TyNat + ask (TyArr t1 t2) = Right (t1,t2) + bld (Left TyNat) = TyNat + bld (Right (t1,t2)) = TyArr t1 t2 +-- /End/ + + +-- Environment is just a list of types +-- Precondition: expression well typed in environment +-- /typeOf/ +type Env = [Ty] +typeOf :: Env -> Exp -> Ty +typeOf env (Var i) = env !! i +typeOf env (App e _) = let TyArr _ t = typeOf env e in t +typeOf env (Lam t e) = TyArr t (typeOf (t:env) e) +-- /End/ + +-- Matching +-- /Pat/ +data Pat = Any | PArr Ty Pat +matches :: Pat -> Ty -> Bool +matches Any _ = True +matches (PArr t p) (TyArr t1 t2) = t1==t && matches p t2 +matches _ _ = False +-- /End/ + +{- Let the Games begin! + ~~~~~~~~~~~~~~~~~~~~ -} + + + +-- Game for matching variables +-- /mkVarGame/ +varGame :: (Ty -> Bool) -> Env -> Maybe (Game Nat) +varGame f [] = Nothing +varGame f (t:env) = case varGame f env of + Nothing -> if f t then Just (constGame 0) else Nothing + Just g -> if f t then Just (Split succIso unitGame g) + else Just (g +> Iso pred succ) +-- /End/ + +progGame :: Game Exp +progGame = expGame [] Any + +-- Returns an expression with a type that that matches match +-- Satisfies the "all bits count" property +-- /expGame/ +-- (env : Env) -> (p : Pat) -> +-- Game {e | exists t, env |- e : t && matches p t} +expGame :: Env -> Pat -> Game Exp +expGame env p + = case varGame (matches p) env of + Nothing -> appLamG + Just varG -> Split varI varG appLamG + where appLamG = Split appLamI appG (lamG p) + appG = depGame (expGame env Any) $ \e -> + expGame env (PArr (typeOf env e) p) + lamG (PArr t p) = prodGame (constGame t) $ + expGame (t:env) p + lamG Any = depGame tyGame $ \t -> + expGame (t:env) Any + +varI = Iso ask bld where ask (Var x) = Left x + ask e = Right e + bld (Left x) = Var x + bld (Right e) = e +appLamI = Iso ask bld + where ask (App e1 e2) = Left (e2,e1) + ask (Lam t e) = Right (t,e) + bld (Left (e2,e1)) = App e1 e2 + bld (Right (t,e)) = Lam t e + +-- /End/ + + +-- Returns a game for terms in a *given* environment and *given* type. +-- /expGameCheck/ +-- (env:Env) -> (t:Ty) -> Game {e | env |- e : t} +expGameCheck :: Env -> Ty -> Game Exp +expGameCheck env t + = case varGame (== t) env of + Nothing -> appLamG t + Just varG -> Split varI varG (appLamG t) + where appLamG TyNat + = appG +> Iso (\(App e1 e2)->(e2,e1)) + (\(e2,e1)->App e1 e2) + appLamG (TyArr t1 t2) + = let ask (App e1 e2) = Left (e2,e1) + ask (Lam t e) = Right e + bld (Left (e2,e1)) = App e1 e2 + bld (Right e) = Lam t1 e + in Split (Iso ask bld) appG (lamG t1 t2) + appG = depGame (expGame env Any) $ \e -> + expGameCheck env (TyArr (typeOf env e) t) + lamG t1 t2 = expGameCheck (t1:env) t2 + +-- /End/ + +-- -- A strong model for terms (will be strong only if there are infinite inhabitants) +-- -- [Satisfies the all bits count property] +-- /expGameCheckProper/ +expGameCheckProper env t + = filterGame_inf (\_ -> True) (expGameCheck env t) +-- /End/ + + +-- /allTerms/ +all01 = [1] : map (0:) all01 +-- Games for the empty environment and type Nat -> Nat +allNat2Nat = map (fst . dec game) all01 + where game = expGameCheckProper [] (TyArr TyNat TyNat) +-- /End/ + +-- decRandomTm i = run decClosedTm (mkRandom i) + +listsOfLength :: Int -> [[Bit]] +listsOfLength 0 = [[]] +listsOfLength (n+1) = map (0:) (listsOfLength n) ++ map (1:) (listsOfLength n) + +allLists n = listsOfLength n ++ allLists (n+1) + +enumerateTms (x:l) = + case decOpt (expGame [] Any) x of + Just (e,[]) -> e : enumerateTms l + _ -> enumerateTms l + +allTms = enumerateTms (allLists 0) + + +ex = Lam TyNat (Lam TyNat (Var 1))
+ PTLC.hs view
@@ -0,0 +1,247 @@+{-# OPTIONS_GHC -fglasgow-exts #-} +module PTLC where + +import Iso +import Games +import BasicGames + +import Data.Maybe +import FilterGames + +-- /TyExp/ +data Ty = TyVar Nat | TyArr Ty Ty | TyProd Ty Ty | TyAll Nat Ty deriving (Eq, Show) +data Exp = Var Nat [Ty] | Lam Ty Exp | App Exp Exp | TLam Int Exp +-- /End/ + deriving (Eq,Show) + +instantiate :: Nat -> [Ty] -> Ty -> Ty +instantiate n tys (TyVar i) = if i >= n && i < n + length tys then tys !! (i-n) else TyVar (i - length tys) +instantiate n tys (TyArr t1 t2) = TyArr (instantiate n tys t1) (instantiate n tys t2) +instantiate n tys (TyProd t1 t2) = TyProd (instantiate n tys t1) (instantiate n tys t2) +instantiate n tys (TyAll m t) = TyAll m (instantiate (n+m+1) t) + +--instantiateSch :: TySch -> [Ty] -> Ty +--instantiateSch (TySch _ ty) tys = instantiate tys ty + +type Subst = [Maybe Ty] +subst :: Nat -> Subst -> Ty -> Ty +subst n [] ty = ty +subst n (Just ty:s) (TyVar 0) = TyVar 0 +subst (Nothing:s) (TyVar i) = TyVar i +subst (_:s) (TyVar (i+1)) = subst s (TyVar i) +subst n s (TyArr t1 t2) = TyArr (subst n s t1) (subst n s t2) +subst n s (TyProd t1 t2) = TyProd (subst n s t1) (subst n s t2) +subst n s (TyAll m t) = TyAll m (subst (n+m+1) s t) + +merge [] [] = [] +merge (Nothing:s1) (Nothing:s2) = Nothing:merge s1 s2 +merge (_:s1) (Just ty:s2) = Just ty:merge s1 s2 +merge (Just ty:s1) (_:s2) = Just ty:merge s1 s2 + +singleton ntyvars i ty = copies i Nothing ++ [Just ty] ++ replicate (ntyvars-i-1) Nothing + +-- Attempt to match the first n type variables in the second type against the first +matchTy :: Ty -> Subst -> Ty -> Maybe Subst +matchTy ty s (TyVar i) = + if i<length s + then case s!!i of Nothing -> Just (merge (singleton (length s) i ty) s) ; Just ty' -> if ty==ty' then Just s else Nothing + else if ty == TyVar (i-length s) then Just s else Nothing +matchTy (TyArr ty1a ty1b) s (TyArr ty2a ty2b) = + case matchTy ty1a s ty2a of + Nothing -> Nothing + Just s' -> matchTy ty1b s' ty2b +matchTy (TyProd ty1a ty1b) s (TyProd ty2a ty2b) = + case matchTy ty1a s ty2a of + Nothing -> Nothing + Just s' -> matchTy ty1b s' ty2b +matchTy _ _ _ = Nothing + +matchSch :: Ty -> TySch -> Maybe Subst +matchSch ty (TySch n ty') = matchTy ty (copies n Nothing) ty' + +intTy = TyVar 0 +boolTy = TyVar 1 + +showNiceTy :: [String] -> Ty -> String +showNiceTy names (TyVar i) = names !! i +showNiceTy names (TyArr ty1 ty2) = "(" ++ showNiceTy names ty1 ++ "->" ++ showNiceTy names ty2 ++ ")" +showNiceTy names (TyProd ty1 ty2) = "(" ++ showNiceTy names ty1 ++ "*" ++ showNiceTy names ty2 ++ ")" + +var n = Var n [] + +iAtBool = Lam boolTy (var 0) +iAtBoolToBool = Lam (TyArr boolTy boolTy) (var 0) +iAtInt = Lam intTy (var 0) +kAtBool = Lam boolTy (Lam boolTy (var 1)) +kAtInt = Lam intTy (Lam intTy (var 1)) +ii = App iAtBoolToBool iAtBool +twiceTm = Lam (TyArr intTy intTy) (Lam intTy (App (var 1) (App (var 1) (var 0)))) + +type Env = (Int, [TySch]) + +-- Types for fst, snd, pair, zero, succ +exEnv :: Env +exEnv = (2, [TySch 2 (TyArr (TyProd (TyVar 0) (TyVar 1)) (TyVar 0)), + TySch 2 (TyArr (TyProd (TyVar 0) (TyVar 1)) (TyVar 1)), + TySch 2 (TyArr (TyVar 0) (TyArr (TyVar 1) (TyProd (TyVar 0) (TyVar 1)))), + TySch 0 intTy, + TySch 0 (TyArr intTy intTy), + TySch 1 (TyArr (TyArr (TyVar 0) (TyVar 0)) (TyArr (TyVar 0) (TyVar 0))) + ]) + +typeOf :: Env -> Exp -> Ty +typeOf (_,env) (Var i tys) = instantiateSch (env !! i) tys +typeOf env (App e1 e2) = case typeOf env e1 of TyArr t1 t2 -> t2 +typeOf (n,env) (Lam t e) = TyArr t (typeOf (n, TySch 0 t:env) e) +typeOf (n,env) (TLam m e) = TyAll m (typeOf (n+m+1, env) e) + +showTys names [] = "" +showTys names [ty] = showNiceTy names ty +showTys names (ty:tys) = showNiceTy names ty ++ "," ++ showTys names tys + +niceName names = let name = [toEnum (length names + fromEnum 'a')] in (name, name:names) + +niceNames 0 names = names +niceNames (n+1) names = let (_,names') = niceName names in niceNames n names' + +showNice :: Env -> [String] -> [String] -> Exp -> String +showNice (env @ (ntyvars,tyenv)) names tynames t = + case t of + Var i [] -> names !! i + Var i tys -> names !! i ++ "{" ++ showTys tynames tys ++ "}" + App t1 t2 -> showNice env names tynames t1 ++ " " ++ showNice env names tynames t2 + Lam ty t -> let (name,names') = niceName names in "(\\" ++ name ++ ":" ++ showNiceTy tynames ty ++ "." ++ showNice (ntyvars, TySch 0 ty : tyenv) names' tynames t ++ ")" + Let n t1 t2 -> + let tynames' = niceNames n tynames in + let (name,names') = niceName names in + "let(" ++ show n ++ ")" ++ name ++ " = " ++ showNice (n+ntyvars,tyenv) names tynames' t1 ++ " in " ++ showNice (ntyvars,TySch n (typeOf (n+ntyvars,tyenv) t1) : tyenv) names' tynames t2 + +showClosed t = showNice exEnv ["fst", "snd", "pair", "zero", "succ", "twice"] ["Int", "Bool"] t + +ex1 = + Let 1 + (Lam (TyArr (TyVar 0) (TyVar 0)) + (Lam (TyVar 0) + (App (Var 1 []) (App (Var 1 []) (Var 0 []))))) + (App (Var 0 [intTy]) (Var 5 [])) + +-- Match a type scheme against a pattern +data Pat = Any | PArr Ty Pat +matchMatch :: Pat -> Subst -> Ty -> Maybe Subst +matchMatch m s ty = + case (m, ty) of + (Any, _) -> Just s + (PArr ty1 m', TyArr ty2 ty2') -> + case matchTy ty1 s ty2 of + Nothing -> Nothing + Just s' -> matchMatch m' s' ty2' + _ -> Nothing + + +matches :: Pat -> TySch -> Maybe Subst +matches p (TySch n t) = matchMatch p (copies n Nothing) t + +-- Game for types +-- /tyG/ +tyGame :: Nat -> Game Ty +tyGame 0 = (prodGame (tyGame 0) (tyGame 0)) +> Iso (\(TyArr t1 t2) -> (t1,t2)) (\(t1,t2) -> TyArr t1 t2) +tyGame ntyvars = Split (Iso ask bld) + (rangeGame 0 (ntyvars-1)) (prodGame (tyGame ntyvars) (tyGame ntyvars)) + where ask (TyVar i) = Left i + ask (TyArr t1 t2) = Right (t1,t2) + bld (Left i) = TyVar i + bld (Right (t1,t2)) = TyArr t1 t2 +-- /End/ + + +{- Let the Games begin! + ~~~~~~~~~~~~~~~~~~~~ -} + +-- Given a template for a list of a's that fills in some of the elements, create +-- a game that fills out the missing elements +partialVecGame :: [Maybe a] -> Game a -> Game [a] +partialVecGame [] g = constGame [] +partialVecGame (x:xs) g = prodGame (maybe g constGame x) (partialVecGame xs g) +> nonemptyIso + +instGame :: Int -> Subst -> Game [Ty] +instGame ntyvars s = partialVecGame s (tyGame ntyvars) + +-- Game for matching variables +-- /mkVarGame/ +varGame :: (TySch -> Maybe Subst) -> Env -> Maybe (Game (Nat,[Ty])) +varGame f (_,[]) = Nothing +varGame f (ntyvars,t:env) = + case varGame f (ntyvars,env) of + Nothing -> + case f t of + Nothing -> Nothing + Just s -> Just (prodGame (constGame 0) (instGame ntyvars s)) + Just g -> + case f t of + Nothing -> Just (g +> Iso (\(n,i) -> (pred n,i)) (\(n,i) -> (succ n,i))) + Just s -> Just (Split (Iso ask bld) (instGame ntyvars s) g) + where ask (0,i) = Left i + ask (n+1,i) = Right (n,i) + bld (Left i) = (0,i) + bld (Right (n,i)) = (n+1,i) +-- /End/ + +progGame :: Game Exp +progGame = expGame exEnv Any + +posGame :: Game Nat +posGame = unaryNatGame +> Iso pred succ + +-- Returns an expression with a type that that matches match +-- Satisfies the "all bits count" property +-- /expGame/ +-- (env : Env) -> (p : Pat) -> +-- Game {e | exists t, env |- e : t && matches p t} +expGame :: Env -> Pat -> Game Exp +expGame (env@(ntyvars,tyschs)) p = + case varGame (matches p) env of + Nothing -> nonVarG + Just varG -> Split varI varG nonVarG + where nonVarG = Split nonVarI letG appLamG + appLamG = Split appLamI appG (lamG p) + tlamG = + depGame posGame $ \nbound -> + expGame (nbound+ntyvars,tyschs) Any + expGame (ntyvars, TySch nbound (typeOf (nbound+ntyvars,tyschs) e1) : tyschs) p + + appG = depGame (expGame env Any) $ \e -> + expGame env (PArr (typeOf env e) p) + lamG (PArr t p) = prodGame (constGame t) $ + expGame (ntyvars,TySch 0 t:tyschs) p + lamG Any = depGame (tyGame ntyvars) $ \t -> + expGame (ntyvars,TySch 0 t:tyschs) Any + +varI = Iso ask bld where ask (Var x inst) = Left (x,inst) + ask e = Right e + bld (Left (x,inst)) = Var x inst + bld (Right e) = e + +nonVarI = Iso ask bld + where ask (Let n e1 e2) = Left (n, (e1,e2)) + ask e = Right e + bld (Left (n, (e1,e2))) = Let n e1 e2 + bld (Right e) = e + +appLamI = Iso ask bld + where ask (App e1 e2) = Left (e2,e1) + ask (Lam t e) = Right (t,e) + bld (Left (e2,e1)) = App e1 e2 + bld (Right (t,e)) = Lam t e + +listsOfLength :: Int -> [[Bit]] +listsOfLength 0 = [[]] +listsOfLength (n+1) = map (0:) (listsOfLength n) ++ map (1:) (listsOfLength n) + +allLists n = listsOfLength n ++ allLists (n+1) + +enumerateTms (x:l) = + case decOpt progGame x of + Just (e,[]) -> e : enumerateTms l + _ -> enumerateTms l + +allTms = enumerateTms (allLists 0)
+ PolyLet.hs view
@@ -0,0 +1,253 @@+{-# OPTIONS_GHC -fglasgow-exts #-} +module PolyLet where + +import Iso +import Games +import BasicGames + +import Data.Maybe +import FilterGames + +-- Simple types +-- /TyExp/ +data Ty = TyVar Nat | TyArr Ty Ty | TyProd Ty Ty deriving (Eq, Show) +data Exp = Var Nat [Ty] | Lam Ty Exp | App Exp Exp | Let Int Exp Exp +-- /End/ + deriving (Eq,Show) + +-- Type schemes, with number of bound vars first +data TySch = TySch Int Ty deriving Eq + +instance Show TySch where + show (TySch 0 ty) = show ty + show (TySch n ty) = "(forall " ++ show n ++ ")" ++ show ty + +instantiate :: [Ty] -> Ty -> Ty +instantiate tys (TyVar i) = if i < length tys then tys !! i else TyVar (i - length tys) +instantiate tys (TyArr t1 t2) = TyArr (instantiate tys t1) (instantiate tys t2) +instantiate tys (TyProd t1 t2) = TyProd (instantiate tys t1) (instantiate tys t2) + +instantiateSch :: TySch -> [Ty] -> Ty +instantiateSch (TySch _ ty) tys = instantiate tys ty + +type Subst = [Maybe Ty] +subst :: Subst -> Ty -> Ty +subst [] ty = ty +subst (Just ty:s) (TyVar 0) = TyVar 0 +subst (Nothing:s) (TyVar i) = TyVar i +subst (_:s) (TyVar (i+1)) = subst s (TyVar i) +subst s (TyArr t1 t2) = TyArr (subst s t1) (subst s t2) +subst s (TyProd t1 t2) = TyProd (subst s t1) (subst s t2) + +merge [] [] = [] +merge (Nothing:s1) (Nothing:s2) = Nothing:merge s1 s2 +merge (_:s1) (Just ty:s2) = Just ty:merge s1 s2 +merge (Just ty:s1) (_:s2) = Just ty:merge s1 s2 + +singleton ntyvars i ty = replicate i Nothing ++ [Just ty] ++ replicate (ntyvars-i-1) Nothing + +-- Attempt to match the first n type variables in the second type against the first +matchTy :: Ty -> Subst -> Ty -> Maybe Subst +matchTy ty s (TyVar i) = + if i<length s + then case s!!i of Nothing -> Just (merge (singleton (length s) i ty) s) ; Just ty' -> if ty==ty' then Just s else Nothing + else if ty == TyVar (i-length s) then Just s else Nothing +matchTy (TyArr ty1a ty1b) s (TyArr ty2a ty2b) = + case matchTy ty1a s ty2a of + Nothing -> Nothing + Just s' -> matchTy ty1b s' ty2b +matchTy (TyProd ty1a ty1b) s (TyProd ty2a ty2b) = + case matchTy ty1a s ty2a of + Nothing -> Nothing + Just s' -> matchTy ty1b s' ty2b +matchTy _ _ _ = Nothing + +matchSch :: Ty -> TySch -> Maybe Subst +matchSch ty (TySch n ty') = matchTy ty (replicate n Nothing) ty' + +intTy = TyVar 0 +boolTy = TyVar 1 + +showNiceTy :: [String] -> Ty -> String +showNiceTy names (TyVar i) = names !! i +showNiceTy names (TyArr ty1 ty2) = "(" ++ showNiceTy names ty1 ++ "->" ++ showNiceTy names ty2 ++ ")" +showNiceTy names (TyProd ty1 ty2) = "(" ++ showNiceTy names ty1 ++ "*" ++ showNiceTy names ty2 ++ ")" + +var n = Var n [] + +iAtBool = Lam boolTy (var 0) +iAtBoolToBool = Lam (TyArr boolTy boolTy) (var 0) +iAtInt = Lam intTy (var 0) +kAtBool = Lam boolTy (Lam boolTy (var 1)) +kAtInt = Lam intTy (Lam intTy (var 1)) +ii = App iAtBoolToBool iAtBool +twiceTm = Lam (TyArr intTy intTy) (Lam intTy (App (var 1) (App (var 1) (var 0)))) + +type Env = (Int, [TySch]) + +-- Types for fst, snd, pair, zero, succ +exEnv :: Env +exEnv = (2, [TySch 2 (TyArr (TyProd (TyVar 0) (TyVar 1)) (TyVar 0)), + TySch 2 (TyArr (TyProd (TyVar 0) (TyVar 1)) (TyVar 1)), + TySch 2 (TyArr (TyVar 0) (TyArr (TyVar 1) (TyProd (TyVar 0) (TyVar 1)))), + TySch 0 intTy, + TySch 0 (TyArr intTy intTy), + TySch 1 (TyArr (TyArr (TyVar 0) (TyVar 0)) (TyArr (TyVar 0) (TyVar 0))) + ]) + +typeOf :: Env -> Exp -> Ty +typeOf (_,env) (Var i tys) = instantiateSch (env !! i) tys +typeOf env (App e1 e2) = case typeOf env e1 of TyArr t1 t2 -> t2 +typeOf (n,env) (Lam t e) = TyArr t (typeOf (n, TySch 0 t:env) e) +typeOf (n,env) (Let m e1 e2) = typeOf (m, TySch m (typeOf (m+n,env) e1) : env) e2 + +showTys names [] = "" +showTys names [ty] = showNiceTy names ty +showTys names (ty:tys) = showNiceTy names ty ++ "," ++ showTys names tys + +niceName names = let name = [toEnum (length names + fromEnum 'a')] in (name, name:names) + +niceNames 0 names = names +niceNames (n+1) names = let (_,names') = niceName names in niceNames n names' + +showNice :: Env -> [String] -> [String] -> Exp -> String +showNice (env @ (ntyvars,tyenv)) names tynames t = + case t of + Var i [] -> names !! i + Var i tys -> names !! i ++ "{" ++ showTys tynames tys ++ "}" + App t1 t2 -> showNice env names tynames t1 ++ " " ++ showNice env names tynames t2 + Lam ty t -> let (name,names') = niceName names in "(\\" ++ name ++ ":" ++ showNiceTy tynames ty ++ "." ++ showNice (ntyvars, TySch 0 ty : tyenv) names' tynames t ++ ")" + Let n t1 t2 -> + let tynames' = niceNames n tynames in + let (name,names') = niceName names in + "let(" ++ show n ++ ")" ++ name ++ " = " ++ showNice (n+ntyvars,tyenv) names tynames' t1 ++ " in " ++ showNice (ntyvars,TySch n (typeOf (n+ntyvars,tyenv) t1) : tyenv) names' tynames t2 + +showClosed t = showNice exEnv ["fst", "snd", "pair", "zero", "succ", "twice"] ["Int", "Bool"] t + +ex1 = + Let 1 + (Lam (TyArr (TyVar 0) (TyVar 0)) + (Lam (TyVar 0) + (App (Var 1 []) (App (Var 1 []) (Var 0 []))))) + (App (Var 0 [intTy]) (Var 5 [])) + +-- Match a type scheme against a pattern +data Pat = Any | PArr Ty Pat +matchMatch :: Pat -> Subst -> Ty -> Maybe Subst +matchMatch m s ty = + case (m, ty) of + (Any, _) -> Just s + (PArr ty1 m', TyArr ty2 ty2') -> + case matchTy ty1 s ty2 of + Nothing -> Nothing + Just s' -> matchMatch m' s' ty2' + _ -> Nothing + + +matches :: Pat -> TySch -> Maybe Subst +matches p (TySch n t) = matchMatch p (replicate n Nothing) t + +-- Game for types +-- /tyG/ +tyGame :: Nat -> Game Ty +tyGame 0 = (prodGame (tyGame 0) (tyGame 0)) +> Iso (\(TyArr t1 t2) -> (t1,t2)) (\(t1,t2) -> TyArr t1 t2) +tyGame ntyvars = Split (Iso ask bld) + (rangeGame 0 (ntyvars-1)) (prodGame (tyGame ntyvars) (tyGame ntyvars)) + where ask (TyVar i) = Left i + ask (TyArr t1 t2) = Right (t1,t2) + bld (Left i) = TyVar i + bld (Right (t1,t2)) = TyArr t1 t2 +-- /End/ + + +{- Let the Games begin! + ~~~~~~~~~~~~~~~~~~~~ -} + +-- Given a template for a list of a's that fills in some of the elements, create +-- a game that fills out the missing elements +partialVecGame :: [Maybe a] -> Game a -> Game [a] +partialVecGame [] g = constGame [] +partialVecGame (x:xs) g = prodGame (maybe g constGame x) (partialVecGame xs g) +> nonemptyIso + +instGame :: Int -> Subst -> Game [Ty] +instGame ntyvars s = partialVecGame s (tyGame ntyvars) + +-- Game for matching variables +-- /mkVarGame/ +varGame :: (TySch -> Maybe Subst) -> Env -> Maybe (Game (Nat,[Ty])) +varGame f (_,[]) = Nothing +varGame f (ntyvars,t:env) = + case varGame f (ntyvars,env) of + Nothing -> + case f t of + Nothing -> Nothing + Just s -> Just (prodGame (constGame 0) (instGame ntyvars s)) + Just g -> + case f t of + Nothing -> Just (g +> Iso (\(n,i) -> (pred n,i)) (\(n,i) -> (succ n,i))) + Just s -> Just (Split (Iso ask bld) (instGame ntyvars s) g) + where ask (0,i) = Left i + ask (n+1,i) = Right (n,i) + bld (Left i) = (0,i) + bld (Right (n,i)) = (n+1,i) +-- /End/ + +progGame :: Game Exp +progGame = expGame exEnv Any + +posGame :: Game Nat +posGame = unaryNatGame +> Iso pred succ + +-- Returns an expression with a type that that matches match +-- Satisfies the "all bits count" property +-- /expGame/ +-- (env : Env) -> (p : Pat) -> +-- Game {e | exists t, env |- e : t && matches p t} +expGame :: Env -> Pat -> Game Exp +expGame (env@(ntyvars,tyschs)) p = + case varGame (matches p) env of + Nothing -> nonVarG + Just varG -> Split varI varG nonVarG + where nonVarG = Split nonVarI letG appLamG + appLamG = Split appLamI appG (lamG p) + letG = + depGame posGame $ \nbound -> + depGame (expGame (nbound+ntyvars,tyschs) Any) $ \e1 -> + expGame (ntyvars, TySch nbound (typeOf (nbound+ntyvars,tyschs) e1) : tyschs) p + + appG = depGame (expGame env Any) $ \e -> + expGame env (PArr (typeOf env e) p) + lamG (PArr t p) = prodGame (constGame t) $ + expGame (ntyvars,TySch 0 t:tyschs) p + lamG Any = depGame (tyGame ntyvars) $ \t -> + expGame (ntyvars,TySch 0 t:tyschs) Any + +varI = Iso ask bld where ask (Var x inst) = Left (x,inst) + ask e = Right e + bld (Left (x,inst)) = Var x inst + bld (Right e) = e + +nonVarI = Iso ask bld + where ask (Let n e1 e2) = Left (n, (e1,e2)) + ask e = Right e + bld (Left (n, (e1,e2))) = Let n e1 e2 + bld (Right e) = e + +appLamI = Iso ask bld + where ask (App e1 e2) = Left (e2,e1) + ask (Lam t e) = Right (t,e) + bld (Left (e2,e1)) = App e1 e2 + bld (Right (t,e)) = Lam t e + +listsOfLength :: Int -> [[Bit]] +listsOfLength 0 = [[]] +listsOfLength (n+1) = map (0:) (listsOfLength n) ++ map (1:) (listsOfLength n) + +allLists n = listsOfLength n ++ allLists (n+1) + +enumerateTms (x:l) = + case decOpt progGame x of + Just (e,[]) -> e : enumerateTms l + _ -> enumerateTms l + +allTms = enumerateTms (allLists 0)
+ README view
@@ -0,0 +1,24 @@+List of files in this directory +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Games.hs, Games.v + Definition of games, encoder and decoder, proofs of game properties. + +BasicGames.hs + Combinator libraries and examples. + +Iso.hs, Iso.v + Isomorphism library. + +SetGames.hs, NatGames.hs + Encodings of sets and natural numbers + +FilterGames.hs + Filtering games + +UTLC.hs, STLC.hs + Games for untyped and typed lambda-calculi + +Huffman.hs + Huffman codes, static and adaptive dictionaries. +
+ STLC.hs view
@@ -0,0 +1,149 @@+module STLC where + +import Iso +import Games +import BasicGames + +import Data.Maybe +import FilterGames + +-- Simple types +-- /TyExp/ +data Ty = TyNat | TyArr Ty Ty deriving (Eq, Show) +data Exp = Var Nat | Lam Ty Exp | App Exp Exp +-- /End/ + deriving (Eq,Show) + +-- Game for types +-- /tyG/ +tyG :: Game Ty +tyG = Split (Iso ask bld) unitGame (prodGame tyG tyG) + where ask TyNat = Left () + ask (TyArr t1 t2) = Right (t1,t2) + bld (Left ()) = TyNat + bld (Right (t1,t2)) = TyArr t1 t2 +-- /End/ + + +-- Environment is just a list of types +-- Precondition: expression well typed in environment +-- /typeOf/ +type Env = [Ty] +typeOf :: Env -> Exp -> Ty +typeOf env (Var i) = env !! i +typeOf env (App e _) = let TyArr _ t = typeOf env e in t +typeOf env (Lam t e) = TyArr t (typeOf (t:env) e) +-- /End/ + +-- Matching +-- /Pat/ +data Pat = Any | PArr Ty Pat +matches :: Pat -> Ty -> Bool +matches Any _ = True +matches (PArr t p) (TyArr t1 t2) = t1==t && matches p t2 +matches _ _ = False +-- /End/ + +{- Let the Games begin! + ~~~~~~~~~~~~~~~~~~~~ -} + + + +-- Game for matching variables +-- /mkVarGame/ +varGame :: (Ty -> Bool) -> Env -> Maybe (Game Nat) +varGame f [] = Nothing +varGame f (t:env) = case varGame f env of + Nothing -> if f t then Just (constGame 0) else Nothing + Just g -> if f t then Just (Split succIso unitGame g) + else Just (g +> Iso pred succ) +-- /End/ + +-- Returns an expression with a type that that matches match +-- Satisfies the "all bits count" property +-- /expGame/ +expGame :: Env -> Pat -> Game Exp +-- forall (env:Env) (p:Pat), +-- Game { e | exists t, env |- e : t && matches p t = true } +expGame env p + = case varGame (matches p) env of + Nothing -> appLamG + Just varG -> Split varI varG appLamG + where appLamG = Split appLamI appG (lamG p) + appG = depGame (expGame env Any) $ \e -> + expGame env (PArr (typeOf env e) p) + lamG (PArr t p) = prodGame (constGame t) $ + expGame (t:env) p + lamG Any = depGame tyG $ \t -> + expGame (t:env) Any + +varI = Iso ask bld where ask (Var x) = Left x + ask e = Right e + bld (Left x) = Var x + bld (Right e) = e +appLamI = Iso ask bld + where ask (App e1 e2) = Left (e2,e1) + ask (Lam t e) = Right (t,e) + bld (Left (e2,e1)) = App e1 e2 + bld (Right (t,e)) = Lam t e + +-- /End/ + +progGame :: Game Exp +progGame = expGame [] Any + +-- Returns a game for terms in a *given* environment and *given* type. +-- /expGameCheck/ +-- forall (env:Env) (t:Ty), Game { e | env |- e : t } +expGameCheck :: Env -> Ty -> Game Exp +expGameCheck env t + = case varGame (== t) env of + Nothing -> appLamG t + Just varG -> Split varI varG (appLamG t) + where appLamG TyNat + = appG +> Iso (\(App e1 e2)->(e2,e1)) + (\(e2,e1)->App e1 e2) + appLamG (TyArr t1 t2) + = let ask (App e1 e2) = Left (e2,e1) + ask (Lam t e) = Right e + bld (Left (e2,e1)) = App e1 e2 + bld (Right e) = Lam t1 e + in Split (Iso ask bld) appG (lamG t1 t2) + appG = depGame (expGame env Any) $ \e -> + expGameCheck env (TyArr (typeOf env e) t) + lamG t1 t2 = expGameCheck (t1:env) t2 + +-- /End/ + +-- -- A strong model for terms (will be strong only if there are infinite inhabitants) +-- -- [Satisfies the all bits count property] +-- /expGameCheckProper/ +expGameCheckProper env t + = filterInfGame (\_ -> True) (expGameCheck env t) +-- /End/ + + +-- /allTerms/ +all01 = [O] : map (O:) all01 +-- Games for the empty environment and type Nat -> Nat +allNat2Nat = map (fst . dec game) all01 + where game = expGameCheckProper [] (TyArr TyNat TyNat) +-- /End/ + +-- decRandomTm i = run decClosedTm (mkRandom i) + +listsOfLength :: Int -> [[Bit]] +listsOfLength 0 = [[]] +listsOfLength (n+1) = map (O:) (listsOfLength n) ++ map (I:) (listsOfLength n) + +allLists n = listsOfLength n ++ allLists (n+1) + +enumerateTms (x:l) = + case decOpt (expGame [] Any) x of + Just (e,[]) -> e : enumerateTms l + _ -> enumerateTms l + +allTms = enumerateTms (allLists 0) + + +ex = Lam TyNat (Lam TyNat (Var 1))
+ SetGames.hs view
@@ -0,0 +1,124 @@+{-# options_ghc -XEmptyDataDecls -XOverlappingInstances -XScopedTypeVariables #-} +module SetGames where + +import Data.Maybe +import Iso +import Games +import BasicGames +import List + +getRight (Right x) = x +getLeft (Left x) = x +nonemptyIso = Iso (\(x:xs) -> (x,xs)) (\(x,xs) -> x:xs) + +-- Diff functions used for representations of sets and multisets +-- /diff/ +diff minus [] = [] +diff minus (x:xs) = x : diff' x xs + where diff' base [] = [] + diff' base (x:xs) = minus x base : diff' x xs + +undiff plus [] = [] +undiff plus (x:xs) = x : undiff' x xs + where undiff' base [] = [] + undiff' base (x:xs) = base' : undiff' base' xs + where base' = plus base x +-- /End/ + + +-- Makes use of isomorphism between [Nat] and { xs:[Nat] | sorted xs } +-- /natMultisetGame/ +natMultisetGame :: Game Nat -> Game [Nat] +natMultisetGame g = + listGame g +> Iso (diff (-) . sort) (undiff (+)) +-- /End/ + +-- Makes use of isomorphism between [Nat] and { xs:[Nat] | sorted xs && distinct xs } +-- /natSetGame/ +natSetGame :: Game Nat -> Game [Nat] +natSetGame g = + listGame g +> Iso (diff (\ x y -> x-y-1) . sort) + (undiff (\ x y -> x+y+1)) +-- /End/ + +-- Comparison of two elements based on their games +-- /compareByGame/ +compareByGame :: Game a -> (a -> a -> Ordering) +compareByGame (Single _) x y = EQ +compareByGame (Split (Iso ask bld) g1 g2) x y = + case (ask x, ask y) of + (Left x1 , Left y1) -> compareByGame g1 x1 y1 + (Right x2, Right y2) -> compareByGame g2 x2 y2 + (Left x1, Right y2) -> LT + (Right x2, Left y1) -> GT +sortByGame :: Game a -> [a] -> [a] +sortByGame g = sortBy (compareByGame g) +-- /End/ + +-- Remove an element from a game, returning Nothing if the game was a singleton +removeEQ :: Game a -> a -> Maybe (Game a) +removeEQ (Single _) x = Nothing +removeEQ (Split (Iso ask bld) g1 g2) x = + case ask x of + Left x1 -> + Just $ case removeEQ g1 x1 of + Nothing -> g2 +> rightI + Just g1' -> Split (Iso ask bld) g1' g2 + Right x2 -> + Just $ case removeEQ g2 x2 of + Nothing -> g1 +> leftI + Just g2' -> Split (Iso ask bld) g1 g2' + where rightI = Iso (getRight . ask) + (bld . Right) + leftI = Iso (getLeft . ask) + (bld . Left) + + + +-- Remove every element less than or equal to an element according to +-- the ordering induced by the game, returning Nothing if no elements would remain +-- /removeLE/ +removeLE :: Game a -> a -> Maybe (Game a) +removeLE (Single _) x = Nothing +removeLE (Split (Iso ask bld) g1 g2) x = + case ask x of + Left x1 -> + Just $ case removeLE g1 x1 of + Nothing -> g2 +> rightI + Just g1' -> Split (Iso ask bld) g1' g2 + Right x2 -> case removeLE g2 x2 of + Nothing -> Nothing + Just g2' -> Just (g2' +> rightI) + where rightI = Iso (getRight . ask) + (bld . Right) +-- /End/ + +-- /removeLT/ +-- Remove every element less than an element according to +-- the ordering induced by the game +-- Don't think this one works!!! +removeLT :: Game a -> a -> Game a +removeLT (Single iso) x = Single iso +removeLT (Split (Iso ask bld) g1 g2) x = + case ask x of + Left x1 -> Split (Iso ask bld) (removeLT g1 x1) g2 + Right x2 -> g2 +> Iso (getRight . ask) (bld . Right) +-- /End/ + +-- /setGame/ +setGame :: Game a -> Game [a] +setGame g = setGame' g +> Iso (sortByGame g) id + where setGame' g = Split listIso unitGame $ + depGame g $ \x -> + case removeLE g x of + Just g' -> setGame' g' + Nothing -> constGame [] +-- /End/ + +-- /multisetGame/ +multisetGame :: Game a -> Game [a] +multisetGame g = multisetGame' g +> Iso (sortByGame g) id + where multisetGame' g = Split listIso unitGame + (depGame g (\x -> multisetGame' (removeLT g x))) +-- /End/ +
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ UTLC.hs view
@@ -0,0 +1,37 @@+module UTLC where + +import Iso +import Games +import BasicGames + +-- /Exp/ +data Exp = Var Nat | Lam Exp | App Exp Exp +-- /End/ + deriving Show + + + +-- /expGame/ +expGame :: Nat -> Game Exp +expGame 0 = appLamG 0 +expGame n = + Split (Iso ask bld) (rangeGame 0 (n-1)) (appLamG n) + where ask (Var i) = Left i + ask e = Right e + bld (Left i) = Var i + bld (Right e) = e +-- /End/ + +-- /appLamGame/ +appLamG n = + Split (Iso ask bld) (prodGame (expGame n) (expGame n)) + (expGame (n+1)) + where ask (App e1 e2) = Left (e1,e2) + ask (Lam e) = Right e + bld (Left (e1,e2)) = App e1 e2 + bld (Right e) = Lam e +-- /End/ + +exI = Lam (Var 0) +exK = Lam (Lam (Var 1)) +ex = App exI exK
+ colist.v view
@@ -0,0 +1,43 @@+Set Implicit Arguments. +Unset Strict Implicit. +Set Printing Implicit Defensive. +Require Import List. + +Section colistDef. + +Variable t : Type. + +(* A small custom stream datatype for infinite *and* finite streams *) +CoInductive colist := + | cnil : colist + | ccons: t -> colist -> colist. + +Definition decomp_colist lst := + match lst with + | cnil => cnil | ccons x lst => ccons x lst + end. + +Theorem decomp_colist_thm : forall (l : colist), l = decomp_colist l. +Proof. intros. case l; auto. Qed. + +Inductive FinCoList : colist -> list t -> Prop := + | FinCoListNil : FinCoList cnil nil + | FinCoListCons : forall (x : t) (clst : colist) (lst : list t), + FinCoList clst lst -> FinCoList (ccons x clst) (x :: lst). + +Inductive FinPrefix : colist -> colist -> Prop := + | FinPrefixNil : forall xs, FinPrefix cnil xs + | FinPrefixCons : forall x xs ys, FinPrefix xs ys -> FinPrefix (ccons x xs) (ccons x ys). + +CoInductive Prefix : colist -> colist -> Prop := + | PrefixNil : forall xs, Prefix cnil xs + | PrefixCons : forall x xs ys, Prefix xs ys -> Prefix (ccons x xs) (ccons x ys). + +Fixpoint ctake n (x:colist) := + match n with 0 => nil | S n => + match x with ccons h tl => h :: ctake n tl | cnil => nil end end. + +End colistDef. + + +
+ every-bit-counts.cabal view
@@ -0,0 +1,80 @@+-- every-bit-counts.cabal auto-generated by cabal init. For additional+-- options, see+-- http://www.haskell.org/cabal/release/cabal-latest/doc/users-guide/authors.html#pkg-descr.+-- The name of the package.+Name: every-bit-counts++-- The package version. See the Haskell package versioning policy+-- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for+-- standards guiding when and how versions should be incremented.+Version: 0.1++-- A short (one-line) description of the package.+Synopsis: A functional pearl on encoding and decoding using question-and-answer strategies++Description:+ A functional pearl on encoding and decoding using question-and-answer strategies++-- A longer description of the package.+-- Description: ++-- URL for the project homepage or repository.+Homepage: http://research.microsoft.com/en-us/people/dimitris/pearl.pdf++-- The license under which the package is released.+License: BSD3++-- The file containing the license text.+License-file: LICENSE++-- The package author(s).+Author: Dimitrios Vytiniotis and Andrew Kennedy++-- An email address to which users can send suggestions, bug reports,+-- and patches.+Maintainer: dons@galois.com++-- A copyright notice.+-- Copyright: ++Category: Data++Build-type: Simple++-- Extra files to be distributed with the package, such as examples or+-- a README.+-- Extra-source-files: ++-- Constraint on the version of Cabal needed to build this package.+Cabal-version: >=1.2+++Library+ -- Modules exported by the library.+ Exposed-modules: + BadGames, + BasicGames, + FilterGames, + Games, + Huffman, + Iso, +-- Main, + SetGames, + NatGames, + STLC, + UTLC,+ PGames+-- PBasicGames, +-- PolyLet, +-- PSTLC, +-- PTLC, ++-- Packages needed in order to build this package.+ Build-depends: haskell98, base >= 3 && < 5++-- Modules not exported by this package.+-- Other-modules: ++-- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source.+-- Build-tools: +