diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrfun.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 0ce3752a51..b8affba541 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -56,6 +56,10 @@ Require Import ssreflect. Structure inference, as in the implementation of the mxdirect predicate in matrix.v. + - The empty type: + void == a notation for the Empty_set type of the standard library. + of_void T == the canonical injection void -> T. + - Sigma types: tag w == the i of w : {i : I & T i}. tagged w == the T i component of w : {i : I & T i}. @@ -166,7 +170,7 @@ Require Import ssreflect. right_loop inv op <-> op, inv obey the inverse loop right axiom: (x op y) op (inv y) = x for all x, y. rev_right_loop inv op <-> op, inv obey the inverse loop reverse right - axiom: (x op y) op (inv y) = x for all x, y. + axiom: (x op (inv y)) op y = x for all x, y. Note that familiar "cancellation" identities like x + y - y = x or x - y + y = x are respectively instances of right_loop and rev_right_loop The corresponding lemmas will use the K and NK/VK suffixes, respectively. @@ -483,6 +487,12 @@ Arguments idfun {T} x /. Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2. +(** The empty type. **) + +Notation void := Empty_set. + +Definition of_void T (x : void) : T := match x with end. + (** Strong sigma types. **) Section Tag. @@ -642,6 +652,9 @@ End Injections. Lemma Some_inj {T : nonPropType} : injective (@Some T). Proof. by move=> x y []. Qed. +Lemma of_voidK T : pcancel (of_void T) [fun _ => None]. +Proof. by case. Qed. + (** cancellation lemmas for dependent type casts. **) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). Proof. by case: y /. Qed. |