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