Merge branch 'robbert/nat_to_fin' into 'master'

Rename `fin_of_nat` → `nat_to_fin` to follow the conventions.

See merge request iris/stdpp!120

CHANGELOG.md

@@ -16,6 +16,9 @@ API-breaking change is listed.
 - Add `set_solver` support for `dom`.
 - Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
   `list_to_vec_to_list` for the converse.
+- Rename `fin_of_nat` into `nat_to_fin`, `fin_to_of_nat` into
+  `fin_to_nat_to_fin`, and `fin_of_to_nat` into `nat_to_fin_to_nat`, to follow
+  the conventions.
 - Add `Countable` instance for `vec`.
 - Introduce `destruct_or{?,!}` to repeatedly destruct disjunctions in
   assumptions. The tactic can also be provided an explicit assumption name;

theories/fin.v

@@ -31,7 +31,7 @@ Fixpoint fin_to_nat {n} (i : fin n) : nat :=
   match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
 Coercion fin_to_nat : fin >-> nat.
 
-Notation fin_of_nat := Fin.of_nat_lt.
+Notation nat_to_fin := Fin.of_nat_lt.
 Notation fin_rect2 := Fin.rect2.
 
 Instance fin_dec {n} : EqDecision (fin n).
@@ -81,12 +81,12 @@ Qed.
 
 Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
 Proof. induction i; simpl; lia. Qed.
-Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (fin_of_nat H) = n.
+Lemma fin_to_nat_to_fin n m (H : n < m) : fin_to_nat (nat_to_fin H) = n.
 Proof.
   revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
 Qed.
-Lemma fin_of_to_nat {n} (i : fin n) H : @fin_of_nat (fin_to_nat i) n H = i.
-Proof. apply (inj fin_to_nat), fin_to_of_nat. Qed.
+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.
 
 Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
     (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1))

theories/finite.v

@@ -82,8 +82,8 @@ 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.
+  { by rewrite fin_to_nat_to_fin, decode_encode_nat in Hx; simplify_eq. }
+  exfalso; by rewrite ->fin_to_nat_to_fin, decode_encode_nat in Hx.
 Qed.
 
 Lemma fin_choice {n} {B : fin n → Type} (P : ∀ i, B i → Prop) :

theories/vector.v

@@ -181,20 +181,20 @@ Proof.
   induction v as [|? ? v IH]; inv_fin i. simpl; split; congruence. done.
 Qed.
 Lemma vlookup_lookup' {A n} (v : vec A n) (i : nat) x :
-  (∃ H : i < n, v !!! (fin_of_nat H) = x) ↔ (v : list A) !! i = Some x.
+  (∃ H : i < n, v !!! nat_to_fin H = x) ↔ (v : list A) !! i = Some x.
 Proof.
   split.
-  - intros [Hlt ?]. rewrite <-(fin_to_of_nat i n Hlt). by apply vlookup_lookup.
+  - intros [Hlt ?]. rewrite <-(fin_to_nat_to_fin i n Hlt). by apply vlookup_lookup.
   - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix).
     rewrite vec_to_list_length in Hlt. exists Hlt.
-    apply vlookup_lookup. by rewrite fin_to_of_nat.
+    apply vlookup_lookup. by rewrite fin_to_nat_to_fin.
 Qed.
 Lemma elem_of_vlookup {A n} (v : vec A n) x :
   x ∈ vec_to_list v ↔ ∃ i, v !!! i = x.
 Proof.
   rewrite elem_of_list_lookup. setoid_rewrite <-vlookup_lookup'.
   split; [by intros (?&?&?); eauto|]. intros [i Hx].
-  exists i, (fin_to_nat_lt _). by rewrite fin_of_to_nat.
+  exists i, (fin_to_nat_lt _). by rewrite nat_to_fin_to_nat.
 Qed.
 
 Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) :