diff options
Diffstat (limited to 'plugins/ssr/ssrfun.v')
| -rw-r--r-- | plugins/ssr/ssrfun.v | 487 |
1 files changed, 248 insertions, 239 deletions
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index ac2c7824..4810c6e1 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -10,207 +10,210 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + Require Import ssreflect. -(******************************************************************************) -(* This file contains the basic definitions and notations for working with *) -(* functions. The definitions provide for: *) -(* *) -(* - Pair projections: *) -(* p.1 == first element of a pair *) -(* p.2 == second element of a pair *) -(* These notations also apply to p : P /\ Q, via an and >-> pair coercion. *) -(* *) -(* - Simplifying functions, beta-reduced by /= and simpl: *) -(* [fun : T => E] == constant function from type T that returns E *) -(* [fun x => E] == unary function *) -(* [fun x : T => E] == unary function with explicit domain type *) -(* [fun x y => E] == binary function *) -(* [fun x y : T => E] == binary function with common domain type *) -(* [fun (x : T) y => E] \ *) -(* [fun (x : xT) (y : yT) => E] | == binary function with (some) explicit, *) -(* [fun x (y : T) => E] / independent domain types for each argument *) -(* *) -(* - Partial functions using option type: *) -(* oapp f d ox == if ox is Some x returns f x, d otherwise *) -(* odflt d ox == if ox is Some x returns x, d otherwise *) -(* obind f ox == if ox is Some x returns f x, None otherwise *) -(* omap f ox == if ox is Some x returns Some (f x), None otherwise *) -(* *) -(* - Singleton types: *) -(* all_equal_to x0 == x0 is the only value in its type, so any such value *) -(* can be rewritten to x0. *) -(* *) -(* - A generic wrapper type: *) -(* wrapped T == the inductive type with values Wrap x for x : T. *) -(* unwrap w == the projection of w : wrapped T on T. *) -(* wrap x == the canonical injection of x : T into wrapped T; it is *) -(* equivalent to Wrap x, but is declared as a (default) *) -(* Canonical Structure, which lets the Coq HO unification *) -(* automatically expand x into unwrap (wrap x). The delta *) -(* reduction of wrap x to Wrap can be exploited to *) -(* introduce controlled nondeterminism in Canonical *) -(* Structure inference, as in the implementation of *) -(* the mxdirect predicate in matrix.v. *) -(* *) -(* - Sigma types: *) -(* tag w == the i of w : {i : I & T i}. *) -(* tagged w == the T i component of w : {i : I & T i}. *) -(* Tagged T x == the {i : I & T i} with component x : T i. *) -(* tag2 w == the i of w : {i : I & T i & U i}. *) -(* tagged2 w == the T i component of w : {i : I & T i & U i}. *) -(* tagged2' w == the U i component of w : {i : I & T i & U i}. *) -(* Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. *) -(* sval u == the x of u : {x : T | P x}. *) -(* s2val u == the x of u : {x : T | P x & Q x}. *) -(* The properties of sval u, s2val u are given by lemmas svalP, s2valP, and *) -(* s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. *) -(* A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 *) -(* and pair, e.g., *) -(* have /all_sig[f fP] (x : T): {y : U | P y} by ... *) -(* yields an f : T -> U such that fP : forall x, P (f x). *) -(* - Identity functions: *) -(* id == NOTATION for the explicit identity function fun x => x. *) -(* @id T == notation for the explicit identity at type T. *) -(* idfun == an expression with a head constant, convertible to id; *) -(* idfun x simplifies to x. *) -(* @idfun T == the expression above, specialized to type T. *) -(* phant_id x y == the function type phantom _ x -> phantom _ y. *) -(* *** In addition to their casual use in functional programming, identity *) -(* functions are often used to trigger static unification as part of the *) -(* construction of dependent Records and Structures. For example, if we need *) -(* a structure sT over a type T, we take as arguments T, sT, and a "dummy" *) -(* function T -> sort sT: *) -(* Definition foo T sT & T -> sort sT := ... *) -(* We can avoid specifying sT directly by calling foo (@id T), or specify *) -(* the call completely while still ensuring the consistency of T and sT, by *) -(* calling @foo T sT idfun. The phant_id type allows us to extend this trick *) -(* to non-Type canonical projections. It also allows us to sidestep *) -(* dependent type constraints when building explicit records, e.g., given *) -(* Record r := R {x; y : T(x)}. *) -(* if we need to build an r from a given y0 while inferring some x0, such *) -(* that y0 : T(x0), we pose *) -(* Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. *) -(* Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking *) -(* the dependent type constraint y0 : T(x0). *) -(* *) -(* - Extensional equality for functions and relations (i.e. functions of two *) -(* arguments): *) -(* f1 =1 f2 == f1 x is equal to f2 x for all x. *) -(* f1 =1 f2 :> A == ... and f2 is explicitly typed. *) -(* f1 =2 f2 == f1 x y is equal to f2 x y for all x y. *) -(* f1 =2 f2 :> A == ... and f2 is explicitly typed. *) -(* *) -(* - Composition for total and partial functions: *) -(* f^~ y == function f with second argument specialised to y, *) -(* i.e., fun x => f x y *) -(* CAVEAT: conditional (non-maximal) implicit arguments *) -(* of f are NOT inserted in this context *) -(* @^~ x == application at x, i.e., fun f => f x *) -(* [eta f] == the explicit eta-expansion of f, i.e., fun x => f x *) -(* CAVEAT: conditional (non-maximal) implicit arguments *) -(* of f are NOT inserted in this context. *) -(* fun=> v := the constant function fun _ => v. *) -(* f1 \o f2 == composition of f1 and f2. *) -(* Note: (f1 \o f2) x simplifies to f1 (f2 x). *) -(* f1 \; f2 == categorical composition of f1 and f2. This expands to *) -(* to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x). *) -(* pcomp f1 f2 == composition of partial functions f1 and f2. *) -(* *) -(* *) -(* - Properties of functions: *) -(* injective f <-> f is injective. *) -(* cancel f g <-> g is a left inverse of f / f is a right inverse of g. *) -(* pcancel f g <-> g is a left inverse of f where g is partial. *) -(* ocancel f g <-> g is a left inverse of f where f is partial. *) -(* bijective f <-> f is bijective (has a left and right inverse). *) -(* involutive f <-> f is involutive. *) -(* *) -(* - Properties for operations. *) -(* left_id e op <-> e is a left identity for op (e op x = x). *) -(* right_id e op <-> e is a right identity for op (x op e = x). *) -(* left_inverse e inv op <-> inv is a left inverse for op wrt identity e, *) -(* i.e., (inv x) op x = e. *) -(* right_inverse e inv op <-> inv is a right inverse for op wrt identity e *) -(* i.e., x op (i x) = e. *) -(* self_inverse e op <-> each x is its own op-inverse (x op x = e). *) -(* idempotent op <-> op is idempotent for op (x op x = x). *) -(* associative op <-> op is associative, i.e., *) -(* x op (y op z) = (x op y) op z. *) -(* commutative op <-> op is commutative (x op y = y op x). *) -(* left_commutative op <-> op is left commutative, i.e., *) -(* x op (y op z) = y op (x op z). *) -(* right_commutative op <-> op is right commutative, i.e., *) -(* (x op y) op z = (x op z) op y. *) -(* left_zero z op <-> z is a left zero for op (z op x = z). *) -(* right_zero z op <-> z is a right zero for op (x op z = z). *) -(* left_distributive op1 op2 <-> op1 distributes over op2 to the left: *) -(* (x op2 y) op1 z = (x op1 z) op2 (y op1 z). *) -(* right_distributive op1 op2 <-> op distributes over add to the right: *) -(* x op1 (y op2 z) = (x op1 z) op2 (x op1 z). *) -(* interchange op1 op2 <-> op1 and op2 satisfy an interchange law: *) -(* (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). *) -(* Note that interchange op op is a commutativity property. *) -(* left_injective op <-> op is injective in its left argument: *) -(* x op y = z op y -> x = z. *) -(* right_injective op <-> op is injective in its right argument: *) -(* x op y = x op z -> y = z. *) -(* left_loop inv op <-> op, inv obey the inverse loop left axiom: *) -(* (inv x) op (x op y) = y for all x, y, i.e., *) -(* op (inv x) is always a left inverse of op x *) -(* rev_left_loop inv op <-> op, inv obey the inverse loop reverse left *) -(* axiom: x op ((inv x) op y) = y, for all x, y. *) -(* 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. *) -(* 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. *) -(* *) -(* - Morphisms for functions and relations: *) -(* {morph f : x / a >-> r} <-> f is a morphism with respect to functions *) -(* (fun x => a) and (fun x => r); if r == R[x], *) -(* this states that f a = R[f x] for all x. *) -(* {morph f : x / a} <-> f is a morphism with respect to the *) -(* function expression (fun x => a). This is *) -(* shorthand for {morph f : x / a >-> a}; note *) -(* that the two instances of a are often *) -(* interpreted at different types. *) -(* {morph f : x y / a >-> r} <-> f is a morphism with respect to functions *) -(* (fun x y => a) and (fun x y => r). *) -(* {morph f : x y / a} <-> f is a morphism with respect to the *) -(* function expression (fun x y => a). *) -(* {homo f : x / a >-> r} <-> f is a homomorphism with respect to the *) -(* predicates (fun x => a) and (fun x => r); *) -(* if r == R[x], this states that a -> R[f x] *) -(* for all x. *) -(* {homo f : x / a} <-> f is a homomorphism with respect to the *) -(* predicate expression (fun x => a). *) -(* {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the *) -(* relations (fun x y => a) and (fun x y => r). *) -(* {homo f : x y / a} <-> f is a homomorphism with respect to the *) -(* relation expression (fun x y => a). *) -(* {mono f : x / a >-> r} <-> f is monotone with respect to projectors *) -(* (fun x => a) and (fun x => r); if r == R[x], *) -(* this states that R[f x] = a for all x. *) -(* {mono f : x / a} <-> f is monotone with respect to the projector *) -(* expression (fun x => a). *) -(* {mono f : x y / a >-> r} <-> f is monotone with respect to relators *) -(* (fun x y => a) and (fun x y => r). *) -(* {mono f : x y / a} <-> f is monotone with respect to the relator *) -(* expression (fun x y => a). *) -(* *) -(* The file also contains some basic lemmas for the above concepts. *) -(* Lemmas relative to cancellation laws use some abbreviated suffixes: *) -(* K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). *) -(* LR - a lemma moving an operation from the left hand side of a relation to *) -(* the right hand side, like canLR: cancel g f -> x = g y -> f x = y. *) -(* RL - a lemma moving an operation from the right to the left, e.g., canRL. *) -(* Beware that the LR and RL orientations refer to an "apply" (back chaining) *) -(* usage; when using the same lemmas with "have" or "move" (forward chaining) *) -(* the directions will be reversed!. *) -(******************************************************************************) + +(** + This file contains the basic definitions and notations for working with + functions. The definitions provide for: + + - Pair projections: + p.1 == first element of a pair + p.2 == second element of a pair + These notations also apply to p : P /\ Q, via an and >-> pair coercion. + + - Simplifying functions, beta-reduced by /= and simpl: + #[#fun : T => E#]# == constant function from type T that returns E + #[#fun x => E#]# == unary function + #[#fun x : T => E#]# == unary function with explicit domain type + #[#fun x y => E#]# == binary function + #[#fun x y : T => E#]# == binary function with common domain type + #[#fun (x : T) y => E#]# \ + #[#fun (x : xT) (y : yT) => E#]# | == binary function with (some) explicit, + #[#fun x (y : T) => E#]# / independent domain types for each argument + + - Partial functions using option type: + oapp f d ox == if ox is Some x returns f x, d otherwise + odflt d ox == if ox is Some x returns x, d otherwise + obind f ox == if ox is Some x returns f x, None otherwise + omap f ox == if ox is Some x returns Some (f x), None otherwise + + - Singleton types: + all_equal_to x0 == x0 is the only value in its type, so any such value + can be rewritten to x0. + + - A generic wrapper type: + wrapped T == the inductive type with values Wrap x for x : T. + unwrap w == the projection of w : wrapped T on T. + wrap x == the canonical injection of x : T into wrapped T; it is + equivalent to Wrap x, but is declared as a (default) + Canonical Structure, which lets the Coq HO unification + automatically expand x into unwrap (wrap x). The delta + reduction of wrap x to Wrap can be exploited to + introduce controlled nondeterminism in Canonical + Structure inference, as in the implementation of + the mxdirect predicate in matrix.v. + + - Sigma types: + tag w == the i of w : {i : I & T i}. + tagged w == the T i component of w : {i : I & T i}. + Tagged T x == the {i : I & T i} with component x : T i. + tag2 w == the i of w : {i : I & T i & U i}. + tagged2 w == the T i component of w : {i : I & T i & U i}. + tagged2' w == the U i component of w : {i : I & T i & U i}. + Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. + sval u == the x of u : {x : T | P x}. + s2val u == the x of u : {x : T | P x & Q x}. + The properties of sval u, s2val u are given by lemmas svalP, s2valP, and + s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. + A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 + and pair, e.g., + have /all_sig#[#f fP#]# (x : T): {y : U | P y} by ... + yields an f : T -> U such that fP : forall x, P (f x). + - Identity functions: + id == NOTATION for the explicit identity function fun x => x. + @id T == notation for the explicit identity at type T. + idfun == an expression with a head constant, convertible to id; + idfun x simplifies to x. + @idfun T == the expression above, specialized to type T. + phant_id x y == the function type phantom _ x -> phantom _ y. + *** In addition to their casual use in functional programming, identity + functions are often used to trigger static unification as part of the + construction of dependent Records and Structures. For example, if we need + a structure sT over a type T, we take as arguments T, sT, and a "dummy" + function T -> sort sT: + Definition foo T sT & T -> sort sT := ... + We can avoid specifying sT directly by calling foo (@id T), or specify + the call completely while still ensuring the consistency of T and sT, by + calling @foo T sT idfun. The phant_id type allows us to extend this trick + to non-Type canonical projections. It also allows us to sidestep + dependent type constraints when building explicit records, e.g., given + Record r := R {x; y : T(x)}. + if we need to build an r from a given y0 while inferring some x0, such + that y0 : T(x0), we pose + Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. + Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking + the dependent type constraint y0 : T(x0). + + - Extensional equality for functions and relations (i.e. functions of two + arguments): + f1 =1 f2 == f1 x is equal to f2 x for all x. + f1 =1 f2 :> A == ... and f2 is explicitly typed. + f1 =2 f2 == f1 x y is equal to f2 x y for all x y. + f1 =2 f2 :> A == ... and f2 is explicitly typed. + + - Composition for total and partial functions: + f^~ y == function f with second argument specialised to y, + i.e., fun x => f x y + CAVEAT: conditional (non-maximal) implicit arguments + of f are NOT inserted in this context + @^~ x == application at x, i.e., fun f => f x + #[#eta f#]# == the explicit eta-expansion of f, i.e., fun x => f x + CAVEAT: conditional (non-maximal) implicit arguments + of f are NOT inserted in this context. + fun=> v := the constant function fun _ => v. + f1 \o f2 == composition of f1 and f2. + Note: (f1 \o f2) x simplifies to f1 (f2 x). + f1 \; f2 == categorical composition of f1 and f2. This expands to + to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x). + pcomp f1 f2 == composition of partial functions f1 and f2. + + + - Properties of functions: + injective f <-> f is injective. + cancel f g <-> g is a left inverse of f / f is a right inverse of g. + pcancel f g <-> g is a left inverse of f where g is partial. + ocancel f g <-> g is a left inverse of f where f is partial. + bijective f <-> f is bijective (has a left and right inverse). + involutive f <-> f is involutive. + + - Properties for operations. + left_id e op <-> e is a left identity for op (e op x = x). + right_id e op <-> e is a right identity for op (x op e = x). + left_inverse e inv op <-> inv is a left inverse for op wrt identity e, + i.e., (inv x) op x = e. + right_inverse e inv op <-> inv is a right inverse for op wrt identity e + i.e., x op (i x) = e. + self_inverse e op <-> each x is its own op-inverse (x op x = e). + idempotent op <-> op is idempotent for op (x op x = x). + associative op <-> op is associative, i.e., + x op (y op z) = (x op y) op z. + commutative op <-> op is commutative (x op y = y op x). + left_commutative op <-> op is left commutative, i.e., + x op (y op z) = y op (x op z). + right_commutative op <-> op is right commutative, i.e., + (x op y) op z = (x op z) op y. + left_zero z op <-> z is a left zero for op (z op x = z). + right_zero z op <-> z is a right zero for op (x op z = z). + left_distributive op1 op2 <-> op1 distributes over op2 to the left: + (x op2 y) op1 z = (x op1 z) op2 (y op1 z). + right_distributive op1 op2 <-> op distributes over add to the right: + x op1 (y op2 z) = (x op1 z) op2 (x op1 z). + interchange op1 op2 <-> op1 and op2 satisfy an interchange law: + (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). + Note that interchange op op is a commutativity property. + left_injective op <-> op is injective in its left argument: + x op y = z op y -> x = z. + right_injective op <-> op is injective in its right argument: + x op y = x op z -> y = z. + left_loop inv op <-> op, inv obey the inverse loop left axiom: + (inv x) op (x op y) = y for all x, y, i.e., + op (inv x) is always a left inverse of op x + rev_left_loop inv op <-> op, inv obey the inverse loop reverse left + axiom: x op ((inv x) op y) = y, for all x, y. + 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. + 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. + + - Morphisms for functions and relations: + {morph f : x / a >-> r} <-> f is a morphism with respect to functions + (fun x => a) and (fun x => r); if r == R#[#x#]#, + this states that f a = R#[#f x#]# for all x. + {morph f : x / a} <-> f is a morphism with respect to the + function expression (fun x => a). This is + shorthand for {morph f : x / a >-> a}; note + that the two instances of a are often + interpreted at different types. + {morph f : x y / a >-> r} <-> f is a morphism with respect to functions + (fun x y => a) and (fun x y => r). + {morph f : x y / a} <-> f is a morphism with respect to the + function expression (fun x y => a). + {homo f : x / a >-> r} <-> f is a homomorphism with respect to the + predicates (fun x => a) and (fun x => r); + if r == R#[#x#]#, this states that a -> R#[#f x#]# + for all x. + {homo f : x / a} <-> f is a homomorphism with respect to the + predicate expression (fun x => a). + {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the + relations (fun x y => a) and (fun x y => r). + {homo f : x y / a} <-> f is a homomorphism with respect to the + relation expression (fun x y => a). + {mono f : x / a >-> r} <-> f is monotone with respect to projectors + (fun x => a) and (fun x => r); if r == R#[#x#]#, + this states that R#[#f x#]# = a for all x. + {mono f : x / a} <-> f is monotone with respect to the projector + expression (fun x => a). + {mono f : x y / a >-> r} <-> f is monotone with respect to relators + (fun x y => a) and (fun x y => r). + {mono f : x y / a} <-> f is monotone with respect to the relator + expression (fun x y => a). + + The file also contains some basic lemmas for the above concepts. + Lemmas relative to cancellation laws use some abbreviated suffixes: + K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). + LR - a lemma moving an operation from the left hand side of a relation to + the right hand side, like canLR: cancel g f -> x = g y -> f x = y. + RL - a lemma moving an operation from the right to the left, e.g., canRL. + Beware that the LR and RL orientations refer to an "apply" (back chaining) + usage; when using the same lemmas with "have" or "move" (forward chaining) + the directions will be reversed!. **) + Set Implicit Arguments. Unset Strict Implicit. @@ -219,7 +222,7 @@ Unset Printing Implicit Defensive. Delimit Scope fun_scope with FUN. Open Scope fun_scope. -(* Notations for argument transpose *) +(** Notations for argument transpose **) Notation "f ^~ y" := (fun x => f x y) (at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope. Notation "@^~ x" := (fun f => f x) @@ -228,7 +231,7 @@ Notation "@^~ x" := (fun f => f x) Delimit Scope pair_scope with PAIR. Open Scope pair_scope. -(* Notations for pair/conjunction projections *) +(** Notations for pair/conjunction projections **) Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1") : pair_scope. Notation "p .2" := (snd p) @@ -239,8 +242,9 @@ Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ). Definition all_pair I T U (w : forall i : I, T i * U i) := (fun i => (w i).1, fun i => (w i).2). -(* Complements on the option type constructor, used below to *) -(* encode partial functions. *) +(** + Complements on the option type constructor, used below to + encode partial functions. **) Module Option. @@ -260,7 +264,7 @@ Notation obind := Option.bind. Notation omap := Option.map. Notation some := (@Some _) (only parsing). -(* Shorthand for some basic equality lemmas. *) +(** Shorthand for some basic equality lemmas. **) Notation erefl := refl_equal. Notation ecast i T e x := (let: erefl in _ = i := e return T in x). @@ -269,31 +273,32 @@ Definition nesym := sym_not_eq. Definition etrans := trans_eq. Definition congr1 := f_equal. Definition congr2 := f_equal2. -(* Force at least one implicit when used as a view. *) +(** Force at least one implicit when used as a view. **) Prenex Implicits esym nesym. -(* A predicate for singleton types. *) +(** A predicate for singleton types. **) Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0. Lemma unitE : all_equal_to tt. Proof. by case. Qed. -(* A generic wrapper type *) +(** A generic wrapper type **) Structure wrapped T := Wrap {unwrap : T}. Canonical wrap T x := @Wrap T x. Prenex Implicits unwrap wrap Wrap. -(* Syntax for defining auxiliary recursive function. *) -(* Usage: *) -(* Section FooDefinition. *) -(* Variables (g1 : T1) (g2 : T2). (globals) *) -(* Fixoint foo_auxiliary (a3 : T3) ... := *) -(* body, using [rec e3, ...] for recursive calls *) -(* where "[ 'rec' a3 , a4 , ... ]" := foo_auxiliary. *) -(* Definition foo x y .. := [rec e1, ...]. *) -(* + proofs about foo *) -(* End FooDefinition. *) +(** + Syntax for defining auxiliary recursive function. + Usage: + Section FooDefinition. + Variables (g1 : T1) (g2 : T2). (globals) + Fixoint foo_auxiliary (a3 : T3) ... := + body, using #[#rec e3, ... #]# for recursive calls + where " #[# 'rec' a3 , a4 , ... #]#" := foo_auxiliary. + Definition foo x y .. := #[#rec e1, ... #]#. + + proofs about foo + End FooDefinition. **) Reserved Notation "[ 'rec' a0 ]" (at level 0, format "[ 'rec' a0 ]"). @@ -319,14 +324,15 @@ Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]" (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"). -(* Definitions and notation for explicit functions with simplification, *) -(* i.e., which simpl and /= beta expand (this is complementary to nosimpl). *) +(** + Definitions and notation for explicit functions with simplification, + i.e., which simpl and /= beta expand (this is complementary to nosimpl). **) Section SimplFun. Variables aT rT : Type. -CoInductive simpl_fun := SimplFun of aT -> rT. +Variant simpl_fun := SimplFun of aT -> rT. Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. @@ -362,11 +368,12 @@ Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" := (fun x : xT => [fun y : yT => E]) (at level 0, x ident, y ident, only parsing) : fun_scope. -(* For delta functions in eqtype.v. *) +(** For delta functions in eqtype.v. **) Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z]. -(* Extensional equality, for unary and binary functions, including syntactic *) -(* sugar. *) +(** + Extensional equality, for unary and binary functions, including syntactic + sugar. **) Section ExtensionalEquality. @@ -439,7 +446,7 @@ Notation "@ 'idfun' T " := (@id_head T explicit_id_key) Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2. -(* Strong sigma types. *) +(** Strong sigma types. **) Section Tag. @@ -473,9 +480,9 @@ Lemma all_tag2 I T U V : {f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}. Proof. by case/all_tag=> f /all_pair[]; exists f. Qed. -(* Refinement types. *) +(** Refinement types. **) -(* Prenex Implicits and renaming. *) +(** Prenex Implicits and renaming. **) Notation sval := (@proj1_sig _ _). Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'"). @@ -514,16 +521,16 @@ Section Morphism. Variables (aT rT sT : Type) (f : aT -> rT). -(* Morphism property for unary and binary functions *) +(** Morphism property for unary and binary functions **) Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x). Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y). -(* Homomorphism property for unary and binary relations *) +(** Homomorphism property for unary and binary relations **) Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x). Definition homomorphism_2 (aR rR : _ -> _ -> Prop) := forall x y, aR x y -> rR (f x) (f y). -(* Stability property for unary and binary relations *) +(** Stability property for unary and binary relations **) Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x. Definition monomorphism_2 (aR rR : _ -> _ -> sT) := forall x y, rR (f x) (f y) = aR x y. @@ -600,16 +607,18 @@ Notation "{ 'mono' f : x y /~ a }" := (at level 0, f at level 99, x ident, y ident, format "{ 'mono' f : x y /~ a }") : type_scope. -(* In an intuitionistic setting, we have two degrees of injectivity. The *) -(* weaker one gives only simplification, and the strong one provides a left *) -(* inverse (we show in `fintype' that they coincide for finite types). *) -(* We also define an intermediate version where the left inverse is only a *) -(* partial function. *) +(** + In an intuitionistic setting, we have two degrees of injectivity. The + weaker one gives only simplification, and the strong one provides a left + inverse (we show in `fintype' that they coincide for finite types). + We also define an intermediate version where the left inverse is only a + partial function. **) Section Injections. -(* rT must come first so we can use @ to mitigate the Coq 1st order *) -(* unification bug (e..g., Coq can't infer rT from a "cancel" lemma). *) +(** + rT must come first so we can use @ to mitigate the Coq 1st order + unification bug (e..g., Coq can't infer rT from a "cancel" lemma). **) Variables (rT aT : Type) (f : aT -> rT). Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2. @@ -639,10 +648,10 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. -(* Force implicits to use as a view. *) +(** Force implicits to use as a view. **) Prenex Implicits Some_inj. -(* cancellation lemmas for dependent type casts. *) +(** 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. @@ -684,7 +693,7 @@ Section Bijections. Variables (A B : Type) (f : B -> A). -CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f. +Variant bijective : Prop := Bijective g of cancel f g & cancel g f. Hypothesis bijf : bijective. |