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. 

*)