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