(*======================================================================================
  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.
*)