Timings for Fin.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import Spaces.Nat.Core.
Require Import Equiv.PathSplit.
(** By setting this, using [simple_induction] instead of [induction], and specifying universe variables in a couple of places, we can avoid all universe variables in this file. Several results are confirmed to use no universe variables with an @{} annotation. *)
Local Set Universe Minimization ToSet.
Local Open Scope path_scope.
Local Open Scope nat_scope.
(** * Finite sets *)
(** ** Canonical finite sets *)
(** A *finite set* is a type that is merely equivalent to the canonical finite set determined by some natural number. There are many equivalent ways to define the canonical finite sets, such as [{ k : nat & k < n}]; we instead choose a recursive one. *)
Fixpoint Fin (n : nat) : Type0
:= match n with
| 0 => Empty
| S n => Fin n + Unit
end.
Fixpoint fin_to_nat {n} : Fin n -> nat
:= match n with
| 0 => Empty_rec
| S n' =>
fun k =>
match k with
| inl k' => fin_to_nat k'
| inr tt => n'
end
end.
Global Instance decidable_fin (n : nat)
: Decidable (Fin n).
destruct n as [|n]; try exact _.
Global Instance decidablepaths_fin@{} (n : nat)
: DecidablePaths (Fin n).
simple_induction n n IHn; simpl; exact _.
Global Instance contr_fin1 : Contr (Fin 1).
refine (contr_equiv' Unit (sum_empty_l Unit)^-1).
Definition fin_empty (n : nat) (f : Fin n -> Empty) : n = 0.
destruct n; [ reflexivity | ].
(** The zeroth element of a non-empty finite set is the left most element. It also happens to be the biggest by termsize. *)
Fixpoint fin_zero {n : nat} : Fin n.+1 :=
match n with
| O => inr tt
| S _ => inl fin_zero
end.
(** Where `fin_zero` computes the first element of Fin (S n), `fin_last` computes the last. *)
Definition fin_last {n : nat} : Fin (S n) := inr tt.
(** Injection Fin n -> Fin n.+1 mapping the kth element to the kth element. *)
Definition fin_incl {n : nat} (k : Fin n) : Fin (S n) := inl k.
(** There is an injection from Fin n -> Fin n.+1 that maps the kth element to the (k+1)th element. *)
Fixpoint fsucc {n : nat} : Fin n -> Fin n.+1 :=
match n with
| O => Empty_rec
| S n' =>
fun i : Fin (S n') =>
match i with
| inl i' => inl (fsucc i')
| inr tt => inr tt
end
end.
(** This injection is an injection/embedding *)
Lemma isembedding_fsucc@{} {n : nat} : IsEmbedding (@fsucc n).
apply isembedding_isinj_hset.
simple_induction n n IHn.
destruct u, u0; reflexivity.
Lemma path_fin_fsucc_incl {n : nat} : forall k : Fin n, fsucc (fin_incl k) = fin_incl (fsucc k).
Definition path_nat_fin_incl {n : nat} (k : Fin n)
: fin_to_nat (fin_incl k) = fin_to_nat k
:= 1.
Lemma path_nat_fsucc@{} {n : nat} : forall k : Fin n, fin_to_nat (fsucc k) = S (fin_to_nat k).
simple_induction n n IHn.
rewrite path_fin_fsucc_incl, path_nat_fin_incl.
Lemma path_nat_fin_zero@{} {n} : fin_to_nat (@fin_zero n) = 0.
simple_induction n n IHn.
Definition path_nat_fin_last {n} : fin_to_nat (@fin_last n) = n
:= 1.
(** ** Transposition equivalences *)
(** To prove some basic facts about canonical finite sets, we need some standard automorphisms of them. Here we define some transpositions and prove that they in fact do the desired things. *)
(** *** Swap the last two elements. *)
Definition fin_transpose_last_two (n : nat)
: Fin n.+2 <~> Fin n.+2
:= ((equiv_sum_assoc _ _ _)^-1)
oE (1 +E (equiv_sum_symm _ _))
oE (equiv_sum_assoc _ _ _).
Arguments fin_transpose_last_two : simpl nomatch.
Definition fin_transpose_last_two_last (n : nat)
: fin_transpose_last_two n (inr tt) = (inl (inr tt))
:= 1.
Definition fin_transpose_last_two_nextlast (n : nat)
: fin_transpose_last_two n (inl (inr tt)) = (inr tt)
:= 1.
Definition fin_transpose_last_two_rest (n : nat) (k : Fin n)
: fin_transpose_last_two n (inl (inl k)) = (inl (inl k))
:= 1.
(** *** Swap the last element with [k]. *)
Fixpoint fin_transpose_last_with (n : nat) (k : Fin n.+1)
: Fin n.+1 <~> Fin n.+1.
refine ((fin_transpose_last_two n)
oE _
oE (fin_transpose_last_two n)).
refine ((fin_transpose_last_with n (inl k)) +E 1).
apply fin_transpose_last_two.
Arguments fin_transpose_last_with : simpl nomatch.
Definition fin_transpose_last_with_last@{} (n : nat) (k : Fin n.+1)
: fin_transpose_last_with n k (inr tt) = k.
simple_induction n n IHn; intro k; simpl.
rewrite IHn; reflexivity.
apply ap, ap, path_contr.
(** We have to destruct [n] since fixpoints don't reduce unless their argument is a constructor. *)
all:apply ap, path_contr.
Definition fin_transpose_last_with_with@{} (n : nat) (k : Fin n.+1)
: fin_transpose_last_with n k k = inr tt.
simple_induction n n IHn; intro k; simpl.
destruct k as [|k]; simpl.
rewrite IHn; reflexivity.
all:apply ap, path_contr.
Definition fin_transpose_last_with_rest@{} (n : nat)
(k : Fin n.+1) (l : Fin n)
(notk : k <> inl l)
: fin_transpose_last_with n k (inl l) = (inl l).
simple_induction n n IHn; intros k l notk; simpl.
destruct k as [k|]; simpl.
destruct l as [l|]; simpl.
exact (fun p => notk (ap inl p)).
destruct l as [l|]; simpl.
elim (notk (ap inl (ap inr (path_unit _ _)))).
Definition fin_transpose_last_with_last_other (n : nat) (k : Fin n.+1)
: fin_transpose_last_with n (inr tt) k = k.
Definition fin_transpose_last_with_invol (n : nat) (k : Fin n.+1)
: fin_transpose_last_with n k o fin_transpose_last_with n k == idmap.
destruct (dec_paths k l) as [p|p].
rewrite fin_transpose_last_with_with.
apply fin_transpose_last_with_last.
rewrite fin_transpose_last_with_rest;
try apply fin_transpose_last_with_rest;
exact (fun q => p (path_sum_inl _ q)).
rewrite fin_transpose_last_with_last_other.
apply fin_transpose_last_with_last_other.
rewrite fin_transpose_last_with_last.
apply fin_transpose_last_with_with.
(** ** Equivalences between canonical finite sets *)
(** To give an equivalence [Fin n.+1 <~> Fin m.+1] is equivalent to giving an element of [Fin m.+1] (the image of the last element) together with an equivalence [Fin n <~> Fin m]. More specifically, any such equivalence can be decomposed uniquely as a last-element transposition followed by an equivalence fixing the last element. *)
(** Here is the uncurried map that constructs an equivalence [Fin n.+1 <~> Fin m.+1]. *)
Definition fin_equiv (n m : nat)
(k : Fin m.+1) (e : Fin n <~> Fin m)
: Fin n.+1 <~> Fin m.+1
:= (fin_transpose_last_with m k) oE (e +E 1).
(** Here is the curried version that we will prove to be an equivalence. *)
Definition fin_equiv' (n m : nat)
: ((Fin m.+1) * (Fin n <~> Fin m)) -> (Fin n.+1 <~> Fin m.+1)
:= fun ke => fin_equiv n m (fst ke) (snd ke).
(** We construct its inverse and the two homotopies first as versions using homotopies without funext (similar to [ExtendableAlong]), then apply funext at the end. *)
Definition fin_equiv_hfiber@{} (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
: { kf : (Fin m.+1) * (Fin n <~> Fin m) & fin_equiv' n m kf == e }.
refine (equiv_sigma_prod _ _).
recall (e (inr tt)) as y eqn:p.
assert (p' := (moveL_equiv_V _ _ p)^).
simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set}
(fin_transpose_last_with m (inl y) oE e)
_ _ ; _).
assert (q : inl y <> e (inl a))
by exact (fun z => inl_ne_inr _ _ (equiv_inj e (z^ @ p^))).
set (z := e (inl a)) in *.
rewrite fin_transpose_last_with_rest;
try exact tt; try assumption.
rewrite fin_transpose_last_with_last; exact tt.
rewrite fin_transpose_last_with_with; exact tt.
unfold fst, snd; ev_equiv.
destruct x as [x|[]]; simpl.
rewrite unfunctor_sum_l_beta.
apply fin_transpose_last_with_invol.
refine (fin_transpose_last_with_last _ _ @ p^).
simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set} e _ _ ; _).
destruct (is_inl_or_is_inr (e (inl a))) as [l|r].
assert (q := inr_un_inr (e (inl a)) r).
apply moveR_equiv_V in q.
assert (s := q^ @ ap (e^-1 o inr) (path_unit _ _) @ p').
intros []; exact (p^ # tt).
unfold fst, snd; ev_equiv.
rewrite fin_transpose_last_with_last_other.
apply unfunctor_sum_l_beta.
rewrite fin_transpose_last_with_last.
Definition fin_equiv_inv (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
: (Fin m.+1) * (Fin n <~> Fin m)
:= (fin_equiv_hfiber n m e).1.
Definition fin_equiv_issect (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
: fin_equiv' n m (fin_equiv_inv n m e) == e
:= (fin_equiv_hfiber n m e).2.
Definition fin_equiv_inj_fst (n m : nat)
(k l : Fin m.+1) (e f : Fin n <~> Fin m)
: (fin_equiv n m k e == fin_equiv n m l f) -> (k = l).
refine (_ @ p (inr tt) @ _); simpl;
rewrite fin_transpose_last_with_last; reflexivity.
Definition fin_equiv_inj_snd (n m : nat)
(k l : Fin m.+1) (e f : Fin n <~> Fin m)
: (fin_equiv n m k e == fin_equiv n m l f) -> (e == f).
assert (q := p (inr tt)); simpl in q.
rewrite !fin_transpose_last_with_last in q.
rewrite <- q in p; clear q l.
exact (path_sum_inl _
(equiv_inj (fin_transpose_last_with m k) (p (inl x)))).
(** Now it's time for funext. *)
Global Instance isequiv_fin_equiv `{Funext} (n m : nat)
: IsEquiv (fin_equiv' n m).
refine (isequiv_pathsplit 0 _); split.
intros e; exists (fin_equiv_inv n m e).
apply path_equiv, path_arrow, fin_equiv_issect.
intros [k e] [l f]; simpl.
refine (_ , fun _ _ => tt).
intros p; refine (_ ; path_ishprop _ _).
apply (ap equiv_fun) in p.
refine (fin_equiv_inj_fst n m k l e f p).
apply path_equiv, path_arrow.
refine (fin_equiv_inj_snd n m k l e f p).
Definition equiv_fin_equiv `{Funext} (n m : nat)
: ((Fin m.+1) * (Fin n <~> Fin m)) <~> (Fin n.+1 <~> Fin m.+1)
:= Build_Equiv _ _ (fin_equiv' n m) _.
(** In particular, this implies that if two canonical finite sets are equivalent, then their cardinalities are equal. *)
Definition nat_eq_fin_equiv (n m : nat)
: (Fin n <~> Fin m) -> (n = m).
revert m; simple_induction n n IHn; intro m; simple_induction m m IHm; intros e.
exact (snd (fin_equiv_inv n m e)).
(** ** Initial segments of [nat] *)
Definition nat_fin (n : nat) (k : Fin n) : nat.
simple_induction n n nf; intro k.
Definition nat_fin_inl (n : nat) (k : Fin n)
: nat_fin n.+1 (inl k) = nat_fin n k
:= 1.
Definition nat_fin_compl (n : nat) (k : Fin n) : nat.
simple_induction n n nfc; intro k.
Definition nat_fin_compl_compl n k
: (nat_fin n k + nat_fin_compl n k).+1 = n.
simple_induction n n IHn; intro k.
destruct k as [k|?]; simpl.
rewrite nat_add_comm in IHn.
rewrite nat_add_comm; reflexivity.
(** [fsucc_mod] is the successor function mod n *)
Definition fsucc_mod@{} {n : nat} : Fin n -> Fin n.
(** fsucc allows us to convert a natural number into an element of a finite set. This can be thought of as the modulo map. *)
Fixpoint fin_nat {n : nat} (m : nat) : Fin n.+1
:= match m with
| 0 => fin_zero
| S m => fsucc_mod (fin_nat m)
end.
(** The 1-dimensional version of Sperner's lemma says that given any finite sequence of decidable hProps, where the sequence starts with true and ends with false, we can find a point in the sequence where the sequence changes from true to false. This is like a discrete intermediate value theorem. *)
Fixpoint sperners_lemma_1d {n} :
forall (f : Fin (n.+2) -> Type)
{dprop : forall i, Decidable (f i)}
(left_true : f fin_zero)
(right_false : ~ f fin_last),
{k : Fin n.+1 & f (fin_incl k) /\ ~ f (fsucc k)}.
destruct (dec (f (fin_incl fin_last))) as [prev_true|prev_false].
destruct (sperners_lemma_1d _ (f o fin_incl) _ left_true prev_false) as [k' [fleft fright]].