From db6bf44902379a04a67cd14085fb7080a62f2416 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 11 Mar 2016 09:43:29 +0100 Subject: [PATCH] Choice principle for finite types. --- theories/finite.v | 50 ++++++++++++++++++++++++++++++++++++++++++++++- theories/vector.v | 17 +--------------- 2 files changed, 50 insertions(+), 17 deletions(-) diff --git a/theories/finite.v b/theories/finite.v index c56dfcf..fd15244 100644 --- a/theories/finite.v +++ b/theories/finite.v @@ -1,6 +1,6 @@ (* Copyright (c) 2012-2015, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) -From stdpp Require Export countable list. +From stdpp Require Export countable vector. Class Finite A `{∀ x y : A, Decision (x = y)} := { enum : list A; @@ -61,6 +61,39 @@ Proof. exists y. by rewrite !Nat2Pos.id by done. Qed. +Definition encode_fin `{Finite A} (x : A) : fin (card A) := + Fin.of_nat_lt (encode_lt_card x). +Program Definition decode_fin `{Finite A} (i : fin (card A)) : A := + match Some_dec (decode_nat i) return _ with + | inleft (exist x _) => x | inright _ => _ + end. +Next Obligation. + intros A ?? i ?; exfalso. + destruct (encode_decode A i); naive_solver auto using fin_to_nat_lt. +Qed. +Lemma decode_encode_fin `{Finite A} (x : A) : decode_fin (encode_fin x) = x. +Proof. + unfold decode_fin, encode_fin. destruct (Some_dec _) as [[x' Hx]|Hx]. + { by rewrite fin_to_of_nat, decode_encode_nat in Hx; simplify_eq. } + exfalso; by rewrite ->fin_to_of_nat, decode_encode_nat in Hx. +Qed. + +Lemma fin_choice {n} {B : fin n → Type} (P : ∀ i, B i → Prop) : + (∀ i, ∃ y, P i y) → ∃ f, ∀ i, P i (f i). +Proof. + induction n as [|n IH]; intros Hex. + { exists (fin_0_inv _); intros i; inv_fin i. } + destruct (IH _ _ (λ i, Hex (FS i))) as [f Hf], (Hex 0%fin) as [y Hy]. + exists (fin_S_inv _ y f); intros i; by inv_fin i. +Qed. +Lemma finite_choice `{Finite A} {B : A → Type} (P : ∀ x, B x → Prop) : + (∀ x, ∃ y, P x y) → ∃ f, ∀ x, P x (f x). +Proof. + intros Hex. destruct (fin_choice _ (λ i, Hex (decode_fin i))) as [f ?]. + exists (λ x, eq_rect _ _ (f(encode_fin x)) _ (decode_encode_fin x)); intros x. + destruct (decode_encode_fin x); simpl; auto. +Qed. + Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P. Proof. intros ? x. destruct finA as [[|??] ??]; simplify_eq. @@ -297,3 +330,18 @@ Proof. induction (enum A) as [|x xs IH]; intros l; simpl; auto. by rewrite app_length, fmap_length, IH. Qed. + +Fixpoint fin_enum (n : nat) : list (fin n) := + match n with 0 => [] | S n => 0%fin :: FS <\$> fin_enum n end. +Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}. +Next Obligation. + intros n. induction n; simpl; constructor. + - rewrite elem_of_list_fmap. by intros (?&?&?). + - by apply (NoDup_fmap _). +Qed. +Next Obligation. + intros n i. induction i as [|n i IH]; simpl; + rewrite elem_of_cons, ?elem_of_list_fmap; eauto. +Qed. +Lemma fin_card n : card (fin n) = n. +Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed. diff --git a/theories/vector.v b/theories/vector.v index e1b00a7..d2e6beb 100644 --- a/theories/vector.v +++ b/theories/vector.v @@ -5,7 +5,7 @@ definitions from the standard library, but renames or changes their notations, so that it becomes more consistent with the naming conventions in this development. *) -From stdpp Require Import list finite. +From stdpp Require Export list. Open Scope vector_scope. (** * The fin type *) @@ -82,21 +82,6 @@ Proof. revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia. Qed. -Fixpoint fin_enum (n : nat) : list (fin n) := - match n with 0 => [] | S n => 0%fin :: FS <\$> fin_enum n end. -Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}. -Next Obligation. - intros n. induction n; simpl; constructor. - - rewrite elem_of_list_fmap. by intros (?&?&?). - - by apply (NoDup_fmap _). -Qed. -Next Obligation. - intros n i. induction i as [|n i IH]; simpl; - rewrite elem_of_cons, ?elem_of_list_fmap; eauto. -Qed. -Lemma fin_card n : card (fin n) = n. -Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed. - (** * Vectors *) (** The type [vec n] represents lists of consisting of exactly [n] elements. Whereas the standard library declares exactly the same notations for vectors as -- GitLab