opam

-opam-version: "1.2"
-name: "coq-stdpp"
-maintainer: "Ralf Jung <jung@mpi-sws.org>"
-homepage: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp"
-authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
-bug-reports: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues"
-license: "BSD"
-dev-repo: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git"
-build: [make "-j%{jobs}%"]
-install: [make "install"]
-remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
-depends: [
-  "coq" { (>= "8.6" & < "8.8~") | (= "dev") }
-]

stdpp/binders.v

+(** This file implements a type [binder] with elements [BAnon] for the
+anonymous binder, and [BNamed] for named binders. This type is isomorphic to
+[option string], but we use a special type so that we can define [BNamed] as
+a coercion.
+
+This library is used in various Iris developments, like heap-lang, LambdaRust,
+Iron, Fairis. *)
+From stdpp Require Export strings.
+From stdpp Require Import sets countable finite fin_maps.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
+
+Declare Scope binder_scope.
+Delimit Scope binder_scope with binder.
+
+Inductive binder := BAnon | BNamed :> string → binder.
+Bind Scope binder_scope with binder.
+Notation "<>" := BAnon : binder_scope.
+
+(** [binder_list] matches [option_list]. *)
+Definition binder_list (b : binder) : list string :=
+  match b with
+  | BAnon => []
+  | BNamed s => [s]
+  end.
+
+Global Instance binder_dec_eq : EqDecision binder.
+Proof. solve_decision. Defined.
+Global Instance binder_inhabited : Inhabited binder := populate BAnon.
+Global Instance binder_countable : Countable binder.
+Proof.
+ refine (inj_countable'
+   (λ b, match b with BAnon => None | BNamed s => Some s end)
+   (λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
+Qed.
+
+(** The functions [cons_binder b ss] and [app_binder bs ss] are typically used
+to collect the free variables of an expression. Here [ss] is the current list of
+free variables, and [b], respectively [bs], are the binders that are being
+added. *)
+Definition cons_binder (b : binder) (ss : list string) : list string :=
+  match b with BAnon => ss | BNamed s => s :: ss end.
+Infix ":b:" := cons_binder (at level 60, right associativity).
+Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
+  match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
+Infix "+b+" := app_binder (at level 60, right associativity).
+
+Global Instance set_unfold_cons_binder s b ss P :
+  SetUnfoldElemOf s ss P → SetUnfoldElemOf s (b :b: ss) (BNamed s = b ∨ P).
+Proof.
+  constructor. rewrite <-(set_unfold (s ∈ ss) P).
+  destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
+Qed.
+Global Instance set_unfold_app_binder s bs ss P Q :
+  SetUnfoldElemOf (BNamed s) bs P → SetUnfoldElemOf s ss Q →
+  SetUnfoldElemOf s (bs +b+ ss) (P ∨ Q).
+Proof.
+  intros HinP HinQ.
+  constructor. rewrite <-(set_unfold (s ∈ ss) Q), <-(set_unfold (BNamed s ∈ bs) P).
+  clear HinP HinQ.
+  induction bs; set_solver.
+Qed.
+
+Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
+Proof. induction ss1; by f_equal/=. Qed.
+
+Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
+Proof. induction bs; by f_equal/=. Qed.
+
+Global Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
+Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
+
+Global Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
+Proof.
+  assert (∀ bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
+  { intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
+  induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
+    first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
+Qed.
+
+Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
+  match b with BAnon => m | BNamed s => delete s m end.
+Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
+  match b with BAnon => m | BNamed s => <[s:=x]> m end.
+Global Instance: Params (@binder_insert) 4 := {}.
+
+Section binder_delete_insert.
+  Context `{FinMap string M}.
+
+  Global Instance binder_insert_proper `{Equiv A} b :
+    Proper ((≡) ==> (≡) ==> (≡@{M A})) (binder_insert b).
+  Proof. destruct b; solve_proper. Qed.
+
+  Lemma binder_delete_empty {A} b : binder_delete b ∅ =@{M A} ∅.
+  Proof. destruct b; simpl; eauto using delete_empty. Qed.
+
+  Lemma lookup_binder_delete_None {A} (m : M A) b s :
+    binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.
+  Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
+  Lemma binder_insert_fmap {A B} (f : A → B) (x : A) b (m : M A) :
+    f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
+  Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
+
+  Lemma binder_delete_insert {A} b s x (m : M A) :
+    b ≠ BNamed s → binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
+  Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
+  Lemma binder_delete_delete {A} b s (m : M A) :
+    binder_delete b (delete s m) = delete s (binder_delete b m).
+  Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
+End binder_delete_insert.

stdpp/boolset.v

+(** This file implements boolsets as functions into Prop. *)
+From stdpp Require Export prelude.
+From stdpp Require Import options.
+
+Record boolset (A : Type) : Type := BoolSet { boolset_car : A → bool }.
+Global Arguments BoolSet {_} _ : assert.
+Global Arguments boolset_car {_} _ _ : assert.
+
+Global Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
+Global Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
+Global Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
+  BoolSet (λ y, bool_decide (y = x)).
+Global Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
+Global Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
+Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
+Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
+Global Instance boolset_cprod {A B} :
+  CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
+
+Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
+Proof.
+  split; [split; [split| |]|].
+  - by intros x ?.
+  - by intros x y; rewrite <-(bool_decide_spec (x = y)).
+  - split; [apply orb_prop_elim | apply orb_prop_intro].
+  - split; [apply andb_prop_elim | apply andb_prop_intro].
+  - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
+    destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
+  - done.
+Qed.
+Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
+Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
+
+Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
+  x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof. apply andb_True. Qed.
+
+Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
+  SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
+  SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
+Proof.
+  intros ??; constructor.
+  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
+    (set_unfold_elem_of x.2 X2 Q).
+Qed.
+
+Global Typeclasses Opaque boolset_elem_of.
+Global Opaque boolset_empty boolset_singleton boolset_union
+  boolset_intersection boolset_difference boolset_cprod.

stdpp/coGset.v

+(** This file implements the type [coGset A] of finite/cofinite sets
+of elements of any countable type [A].
+
+Note that [coGset positive] cannot represent all elements of [coPset]
+(e.g., [coPset_suffixes], [coPset_l], and [coPset_r] construct
+infinite sets that cannot be represented). *)
+From stdpp Require Export sets countable.
+From stdpp Require Import decidable finite gmap coPset.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
+
+Inductive coGset `{Countable A} :=
+  | FinGSet (X : gset A)
+  | CoFinGset (X : gset A).
+Global Arguments coGset _ {_ _} : assert.
+
+Global Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
+Proof. solve_decision. Defined.
+Global Instance coGset_countable `{Countable A} : Countable (coGset A).
+Proof.
+  apply (inj_countable'
+    (λ X, match X with FinGSet X => inl X | CoFinGset X => inr X end)
+    (λ s, match s with inl X => FinGSet X | inr X => CoFinGset X end)).
+  by intros [].
+Qed.
+
+Section coGset.
+  Context `{Countable A}.
+
+  Global Instance coGset_elem_of : ElemOf A (coGset A) := λ x X,
+    match X with FinGSet X => x ∈ X | CoFinGset X => x ∉ X end.
+  Global Instance coGset_empty : Empty (coGset A) := FinGSet ∅.
+  Global Instance coGset_top : Top (coGset A) := CoFinGset ∅.
+  Global Instance coGset_singleton : Singleton A (coGset A) := λ x,
+    FinGSet {[x]}.
+  Global Instance coGset_union : Union (coGset A) := λ X Y,
+    match X, Y with
+    | FinGSet X, FinGSet Y => FinGSet (X ∪ Y)
+    | CoFinGset X, CoFinGset Y => CoFinGset (X ∩ Y)
+    | FinGSet X, CoFinGset Y => CoFinGset (Y ∖ X)
+    | CoFinGset X, FinGSet Y => CoFinGset (X ∖ Y)
+    end.
+  Global Instance coGset_intersection : Intersection (coGset A) := λ X Y,
+    match X, Y with
+    | FinGSet X, FinGSet Y => FinGSet (X ∩ Y)
+    | CoFinGset X, CoFinGset Y => CoFinGset (X ∪ Y)
+    | FinGSet X, CoFinGset Y => FinGSet (X ∖ Y)
+    | CoFinGset X, FinGSet Y => FinGSet (Y ∖ X)
+    end.
+  Global Instance coGset_difference : Difference (coGset A) := λ X Y,
+    match X, Y with
+    | FinGSet X, FinGSet Y => FinGSet (X ∖ Y)
+    | CoFinGset X, CoFinGset Y => FinGSet (Y ∖ X)
+    | FinGSet X, CoFinGset Y => FinGSet (X ∩ Y)
+    | CoFinGset X, FinGSet Y => CoFinGset (X ∪ Y)
+    end.
+
+  Global Instance coGset_set : TopSet A (coGset A).
+  Proof.
+    split; [split; [split| |]|].
+    - by intros ??.
+    - intros x y. unfold elem_of, coGset_elem_of; simpl.
+      by rewrite elem_of_singleton.
+    - intros [X|X] [Y|Y] x; unfold elem_of, coGset_elem_of, coGset_union; simpl.
+      + set_solver.
+      + by rewrite not_elem_of_difference, (comm (∨)).
+      + by rewrite not_elem_of_difference.
+      + by rewrite not_elem_of_intersection.
+    - intros [] [];
+      unfold elem_of, coGset_elem_of, coGset_intersection; set_solver.
+    - intros [X|X] [Y|Y] x;
+      unfold elem_of, coGset_elem_of, coGset_difference; simpl.
+      + set_solver.
+      + rewrite elem_of_intersection. destruct (decide (x ∈ Y)); tauto.
+      + set_solver.
+      + rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto.
+    - done.
+  Qed.
+End coGset.
+
+Global Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
+  λ x X,
+  match X with
+  | FinGSet X => decide_rel elem_of x X
+  | CoFinGset X => not_dec (decide_rel elem_of x X)
+  end.
+
+Section infinite.
+  Context `{Countable A, Infinite A}.
+
+  Global Instance coGset_leibniz : LeibnizEquiv (coGset A).
+  Proof.
+    intros [X|X] [Y|Y]; rewrite set_equiv;
+    unfold elem_of, coGset_elem_of; simpl; intros HXY.
+    - f_equal. by apply leibniz_equiv.
+    - by destruct (exist_fresh (X ∪ Y)) as [? [? ?%HXY]%not_elem_of_union].
+    - by destruct (exist_fresh (X ∪ Y)) as [? [?%HXY ?]%not_elem_of_union].
+    - f_equal. apply leibniz_equiv; intros x. by apply not_elem_of_iff.
+  Qed.
+
+  Global Instance coGset_equiv_dec : RelDecision (≡@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz).
+  Defined.
+
+  Global Instance coGset_disjoint_dec : RelDecision (##@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
+      abstract (by rewrite disjoint_intersection_L).
+  Defined.
+
+  Global Instance coGset_subseteq_dec : RelDecision (⊆@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X ∪ Y = Y)));
+      abstract (by rewrite subseteq_union_L).
+  Defined.
+
+  Definition coGset_finite (X : coGset A) : bool :=
+    match X with FinGSet _ => true | CoFinGset _ => false end.
+  Lemma coGset_finite_spec X : set_finite X ↔ coGset_finite X.
+  Proof.
+    destruct X as [X|X];
+    unfold set_finite, elem_of at 1, coGset_elem_of; simpl.
+    - split; [done|intros _]. exists (elements X). set_solver.
+    - split; [intros [Y HXY]%(pred_finite_set(C:=gset A))|done].
+      by destruct (exist_fresh (X ∪ Y)) as [? [?%HXY ?]%not_elem_of_union].
+  Qed.
+  Global Instance coGset_finite_dec (X : coGset A) : Decision (set_finite X).
+  Proof.
+    refine (cast_if (decide (coGset_finite X)));
+      abstract (by rewrite coGset_finite_spec).
+  Defined.
+End infinite.
+
+(** * Pick elements from infinite sets *)
+Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
+  fresh (match X with FinGSet _ => ∅ | CoFinGset X => X end).
+
+Lemma coGpick_elem_of `{Countable A, Infinite A} (X : coGset A) :
+  ¬set_finite X → coGpick X ∈ X.
+Proof.
+  unfold coGpick.
+  destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
+  by intros _; apply is_fresh.
+Qed.
+
+(** * Conversion to and from gset *)
+Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
+  match X with FinGSet X => X | CoFinGset _ => ∅ end.
+Definition gset_to_coGset `{Countable A} : gset A → coGset A := FinGSet.
+
+Section to_gset.
+  Context `{Countable A}.
+
+  Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
+  Proof. done. Qed.
+
+  Context `{Infinite A}.
+
+  Lemma elem_of_coGset_to_gset (X : coGset A) x :
+    set_finite X → x ∈ coGset_to_gset X ↔ x ∈ X.
+  Proof. rewrite coGset_finite_spec. by destruct X. Qed.
+  Lemma gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
+  Proof. by rewrite coGset_finite_spec. Qed.
+End to_gset.
+
+(** * Conversion to coPset *)
+Definition coGset_to_coPset (X : coGset positive) : coPset :=
+  match X with
+  | FinGSet X => gset_to_coPset X
+  | CoFinGset X => ⊤ ∖ gset_to_coPset X
+  end.
+Lemma elem_of_coGset_to_coPset X x : x ∈ coGset_to_coPset X ↔ x ∈ X.
+Proof.
+  destruct X as [X|X]; simpl.
+  - by rewrite elem_of_gset_to_coPset.
+  - by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)).
+Qed.
+
+(** * Inefficient conversion to arbitrary sets with a top element *)
+(** This shows that, when [A] is countable, [coGset A] is initial
+among sets with [∪], [∩], [∖], [∅], [{[_]}], and [⊤]. *)
+Definition coGset_to_top_set `{Countable A, Empty C, Singleton A C, Union C,
+    Top C, Difference C} (X : coGset A) : C :=
+  match X with
+  | FinGSet X => list_to_set (elements X)
+  | CoFinGset X => ⊤ ∖ list_to_set (elements X)
+  end.
+Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
+  x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
+Proof. destruct X; set_solver. Qed.
+
+Global Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
+Global Typeclasses Opaque coGset_union coGset_intersection coGset_difference.

stdpp/dune

+(include_subdirs qualified)
+(coq.theory
+ (name stdpp)
+ (package coq-stdpp))

theories/fin.v → stdpp/fin.v

-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 (** 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".
+From stdpp Require Import options.
 
 (** * The fin type *)
 (** The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We
@@ -17,24 +15,24 @@ ambiguity. *)
 Notation fin := Fin.t.
 Notation FS := Fin.FS.
 
+Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
-Arguments Fin.FS _ _%fin : assert.
+Bind Scope fin_scope with fin.
+Global Arguments Fin.FS _ _%fin : assert.
 
-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.
+(** Allow any non-negative number literal to be parsed as a [fin]. For example
+[42%fin : fin 64], or [42%fin : fin _], or [42%fin : fin (43 + _)]. *)
+Number Notation fin Nat.of_num_uint Nat.to_num_uint (via nat
+  mapping [[Fin.F1] => O, [Fin.FS] => S]) : fin_scope.
 
 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).
+Global Instance fin_dec {n} : EqDecision (fin n).
 Proof.
  refine (fin_rect2
   (λ n (i j : fin n), { i = j } + { i ≠ j })
@@ -66,48 +64,50 @@ Ltac inv_fin i :=
   | fin ?n =>
     match eval hnf in n with
     | 0 =>
-      revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
+      generalize 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
+      generalize 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).
+Global Instance FS_inj {n} : Inj (=) (=) (@FS n).
+Proof. intros i j. apply Fin.FS_inj. Qed.
+Global Instance fin_to_nat_inj {n} : Inj (=) (=) (@fin_to_nat n).
 Proof.
-  intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
+  intros 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.
-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)
+Fixpoint fin_add_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)
+  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_add_inv _ (λ i, H1 (FS i)) H2)
   end.
 
-Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) → Type)
+Lemma fin_add_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.
+  fin_add_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)
+Lemma fin_add_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.
+  fin_add_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))).

theories/functions.v → stdpp/functions.v

-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 From stdpp Require Export base tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Section definitions.
   Context {A T : Type} `{EqDecision A}.