1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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
58
59
60
61
62
|
From mathcomp Require Import ssreflect.
From Corelib Require Export ssrfun.
From mathcomp Require Export ssrnotations.
#[export] Set Warnings "-overwriting-delimiting-key".
(* remove above line when requiring Rocq >= 9.0 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(******************)
(* v9.1 additions *)
(******************)
#[export] Set Warnings "-hiding-delimiting-key".
Delimit Scope function_scope with FUN.
Declare Scope fun_scope.
Close Scope fun_scope.
Definition injective2 (rT aT1 aT2 : Type) (f : aT1 -> aT2 -> rT) :=
forall (x1 x2 : aT1) (y1 y2 : aT2), f x1 y1 = f x2 y2 -> (x1 = x2) * (y1 = y2).
Arguments injective2 [rT aT1 aT2] f.
Lemma inj_omap {aT rT : Type} (f : aT -> rT) :
injective f -> injective (omap f).
Proof. by move=> injf [?|] [?|] //= [/injf->]. Qed.
Lemma omap_id {T : Type} (x : option T) : omap id x = x.
Proof. by case: x. Qed.
Lemma eq_omap {aT rT : Type} (f g : aT -> rT) : f =1 g -> omap f =1 omap g.
Proof. by move=> Ef [?|] //=; rewrite Ef. Qed.
Lemma omapK {aT rT : Type} (f : aT -> rT) (g : rT -> aT) :
cancel f g -> cancel (omap f) (omap g).
Proof. by move=> fK [?|] //=; rewrite fK. Qed.
Definition idempotent_op (S : Type) (op : S -> S -> S) := forall x, op x x = x.
#[deprecated(since="mathcomp 2.3.0", note="use `idempotent_op` instead")]
Notation idempotent:= idempotent_op (only parsing).
Definition idempotent_fun (U : Type) (f : U -> U) := f \o f =1 f.
Lemma inr_inj {A B} : injective (@inr A B). Proof. by move=> ? ? []. Qed.
Lemma inl_inj {A B} : injective (@inl A B). Proof. by move=> ? ? []. Qed.
(**********************)
(* not yet backported *)
(**********************)
Lemma taggedK {I : Type} (T_ : I -> Type) (s : {i : I & T_ i}) :
Tagged T_ (tagged s) = s.
Proof. by case: s. Qed.
Definition swap_pair {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1).
(* Note that this lemma coudn't be an instance of the [involutive] predicate. *)
Lemma swap_pairK {T1 T2 : Type} : @cancel _ (T1 * T2) swap_pair swap_pair.
Proof. by case. Qed.
|
