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.