fin.v 4.24 KB
 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 ``````(** This file collects general purpose definitions and theorems on the fin type (bounded naturals). It uses the 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 Export base tactics. Set Default Proof Using "Type". (** * The fin type *) (** The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We define a scope [fin], in which we declare notations for small literals of the [fin] type. Whereas the standard library starts counting at [1], we start counting at [0]. This way, the embedding [fin_to_nat] preserves [0], and allows us to define [fin_to_nat] as a coercion without introducing notational ambiguity. *) Notation fin := Fin.t. Notation FS := Fin.FS. Delimit Scope fin_scope with fin. `````` Robbert Krebbers committed Sep 08, 2017 19 ``````Arguments Fin.FS _ _%fin : assert. `````` 20 21 22 23 24 25 26 27 28 `````` Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope. Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope. Notation "4" := (FS 3) : fin_scope. Notation "5" := (FS 4) : fin_scope. Notation "6" := (FS 5) : fin_scope. Notation "7" := (FS 6) : fin_scope. Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope. Notation "10" := (FS 9) : fin_scope. Fixpoint fin_to_nat {n} (i : fin n) : nat := `````` Ralf Jung committed Oct 28, 2017 29 `````` match i with 0%fin => 0 | FS i => S (fin_to_nat i) end. `````` 30 31 ``````Coercion fin_to_nat : fin >-> nat. `````` Robbert Krebbers committed Mar 05, 2020 32 ``````Notation nat_to_fin := Fin.of_nat_lt. `````` 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 ``````Notation fin_rect2 := Fin.rect2. Instance fin_dec {n} : EqDecision (fin n). Proof. refine (fin_rect2 (λ n (i j : fin n), { i = j } + { i ≠ j }) (λ _, left _) (λ _ _, right _) (λ _ _, right _) (λ _ _ _ H, cast_if H)); abstract (f_equal; by auto using Fin.FS_inj). Defined. (** The inversion principle [fin_S_inv] is more convenient than its variant [Fin.caseS] in the standard library, as we keep the parameter [n] fixed. In the tactic [inv_fin i] to perform dependent case analysis on [i], we therefore do not have to generalize over the index [n] and all assumptions depending on it. Notice that contrary to [dependent destruction], which uses the [JMeq_eq] axiom, the tactic [inv_fin] produces axiom free proofs.*) Notation fin_0_inv := Fin.case0. Definition fin_S_inv {n} (P : fin (S n) → Type) (H0 : P 0%fin) (HS : ∀ i, P (FS i)) (i : fin (S n)) : P i. Proof. revert P H0 HS. `````` Ralf Jung committed Oct 28, 2017 58 `````` refine match i with 0%fin => λ _ H0 _, H0 | FS i => λ _ _ HS, HS i end. `````` 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 ``````Defined. Ltac inv_fin i := let T := type of i in match eval hnf in T with | fin ?n => match eval hnf in n with | 0 => revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end | S ?n => revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end end end. Instance FS_inj: Inj (=) (=) (@FS n). Proof. intros n i j. apply Fin.FS_inj. Qed. Instance fin_to_nat_inj : Inj (=) (=) (@fin_to_nat n). Proof. intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia. Qed. Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n. Proof. induction i; simpl; lia. Qed. `````` Robbert Krebbers committed Mar 05, 2020 82 ``````Lemma fin_to_nat_to_fin n m (H : n < m) : fin_to_nat (nat_to_fin H) = n. `````` 83 84 85 ``````Proof. revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia. Qed. `````` Robbert Krebbers committed Mar 05, 2020 86 87 ``````Lemma nat_to_fin_to_nat {n} (i : fin n) H : @nat_to_fin (fin_to_nat i) n H = i. Proof. apply (inj fin_to_nat), fin_to_nat_to_fin. Qed. `````` 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 `````` Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type) (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1)) (H2 : ∀ i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i := match n1 with | 0 => λ P H1 H2 i, H2 i | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_plus_inv _ (λ i, H1 (FS i)) H2) end. Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) → Type) (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n1) : fin_plus_inv P H1 H2 (Fin.L n2 i) = H1 i. Proof. revert P H1 H2 i. induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto. intros i. apply (IH (λ i, P (FS i))). Qed. Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2) → Type) (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n2) : fin_plus_inv P H1 H2 (Fin.R n1 i) = H2 i. Proof. revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto. apply (IH (λ i, P (FS i))). Qed.``````