diff --git a/config/tests.config b/config/tests.config index a5762df7d9..889b4ce7a4 100644 --- a/config/tests.config +++ b/config/tests.config @@ -14,4 +14,5 @@ exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomple okdirs = examples/MEE-CBC [test-unit] -okdirs = tests tests/exception +okdirs = tests tests/exception tests/notations +kodirs = tests/notations-ko diff --git a/doc/index.rst b/doc/index.rst index 8b6c7d9b2f..560348597b 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -5,3 +5,4 @@ EasyCrypt reference manual :maxdepth: 2 tactics + notation diff --git a/doc/notation.rst b/doc/notation.rst new file mode 100644 index 0000000000..87340f91fe --- /dev/null +++ b/doc/notation.rst @@ -0,0 +1,425 @@ +======================================================================== +Notations +======================================================================== + +Notations are user-declared surface-syntax forms for formulas. A +declaration binds a name prefixed by ``#`` to a template of literal +punctuation and slots; uses of the notation at the call site are parsed +against the template and expanded to an underlying body at type-checking +time. Notations live in the same namespace as operators and +abbreviations: they follow ``import``/``export``/``clone`` rules, they +can be declared ``local`` inside a ``section``, and the pretty-printer +automatically renders expanded bodies back to template syntax whenever +possible. + +------------------------------------------------------------------------ +Anatomy of a declaration +------------------------------------------------------------------------ + +.. admonition:: Syntax + + | ``local``? ``notation`` ``#``\ *name* + | *tyvars*? + | *binder-slots*? + | *form-slots*\ * + | *template* + | (``:`` *codom*)? + | ``=`` *body* ``.`` + + where a form slot is either ``(`` *name* ``:`` *ty* ``)`` or + ``(`` *name* ``:`` *deps* ``==>`` *ty* ``)``, optionally extended + with a default ``(`` *name* ``:`` *ty* ``=`` *default* ``)``; and + a template item is a STRING punctuation, a slot name, or an + optional group ``(`` *template-item*\ * ``)?``. + +Every piece except the name, template, and body is optional. The +declaration mirrors an operator declaration with an extra *template* +section that describes the surface syntax. + +Example:: + + notation #pair (a : int) (b : int) " [" a ", " b "] " = (a, b). + + lemma L (x y : int) : #pair [x, y] = (x, y). + proof. by trivial. qed. + +------------------------------------------------------------------------ +Template literals and punctuations +------------------------------------------------------------------------ + +A template is a sequence that alternates **STRING literals** and **slot +references**. The first element of the template must be a STRING. + +Each STRING must lex to exactly one of six punctuation tokens: + + ``[`` ``]`` ``:`` ``|`` ``,`` ``;`` + +Additional whitespace *inside* the string is ignored by the input +matcher but preserved verbatim by the pretty-printer. For example, +``" [ "`` and ``"["`` both match a single ``[`` at the call site, but +the former pretty-prints with spaces on both sides. + +A STRING that lexes to zero tokens, two or more tokens, or an +unsupported symbol is rejected at declaration time:: + + notation #bad " @" a " @ " = a. + (* rejected: notation punctuation `" @"' must lex to one of: [ ] : | , ; *) + +------------------------------------------------------------------------ +Slots +------------------------------------------------------------------------ + +A slot is a bare lowercase identifier inside the template. Each slot +must be declared earlier in the notation as either a **form slot** or a +**binder slot**. + +Form slots + Declared with ``( name : ty )`` in the usual function-argument style. + At the call site the slot consumes a formula; at typing time the + formula is checked against ``ty``. + +Binder slots + Declared inside ``#< ... >`` before the form-slot block, for example + ``#< i : int >`` or ``#< i : int, j : int >``. A binder slot reads + an *identifier* at the call site. The chosen identifier becomes a + locally-bound name visible to any form slot that depends on it. + Writing ``_`` as the binder name at the call site introduces a + fresh anonymous binder — useful when no dependent form slot + actually uses it:: + + lemma L (xs : int list) : #mapI [_ : 3 : 42] = [42; 42; 42]. + +Per-slot binder dependencies + A form slot can declare that it depends on binder slots via + ``==>``:: + + notation #mapI #< i : int > (n : int) (f : i ==> int) + " [" i " : " n " : " f "] " = + map f (iota_ 0 n). + + At typing, ``f`` has type ``int -> int`` (curried over the binders + it declares). At the call site the user writes the body of the + lambda in terms of the chosen binder name, and the expansion wraps + it automatically:: + + lemma M : #mapI [k : 4 : k + 1] = map (fun k => k + 1) (iota_ 0 4). + proof. by trivial. qed. + +**Template order is free.** A form slot may reference a binder that +appears anywhere in the template, including *after* the form slot. At +expansion time binder slots are bound in a first pass and form slots in +a second, so a comprehension-style template like ``"[" f " | " x " : " +s "]"`` works even though ``f`` (which depends on ``x``) is printed +before ``x``. + +**Slot kind is inferred from the declaration, not the template.** A +template reference like ``i`` means "ident slot" iff ``i`` is in the +``#< ... >`` group; otherwise it means "form slot". + +------------------------------------------------------------------------ +Type parameters +------------------------------------------------------------------------ + +Notations may be polymorphic. Type parameters are declared in the same +``['a 'b]`` syntax used by operators, appearing before the slot lists:: + + notation #ppair ['a 'b] (a : 'a) (b : 'b) " [" a ", " b "] " = (a, b). + + lemma L (x : int) (y : bool) : #ppair [x, y] = (x, y). + proof. by trivial. qed. + +Type parameters are freshened at every call site, so independent uses +do not leak type equalities. + +------------------------------------------------------------------------ +Optional template groups +------------------------------------------------------------------------ + +A sub-sequence of template items can be wrapped in ``( ... )?`` to +mark it optional. The group must start with a punctuation literal +(its trigger) and can contain further form slots. Any form slot that +appears only inside an optional group must declare a default via +``(x : ty = default)`` at the slot declaration:: + + notation #big ['a] #< i : 'a > + (r : 'a list) + (P : i ==> bool = predT) + (F : i ==> t) + "[" i " : " r ("| " P)? "] " F = + big P F r. + +At a call site the dispatcher peeks one token at the group's trigger +position: present → parse the group, absent → the slots inside get +their declared defaults:: + + #big [ i : xs | 0 <= i ] (F i) (* P = fun i => 0 <= i *) + #big [ i : xs ] (F i) (* P = predT *) + +Groups are mutually independent — each is triggered by its own +punctuation character and can appear or not regardless of sibling +groups. + +Constraints at declaration time: + +- the group must be non-empty and start with a punctuation literal; +- only form slots may be inside a group (ident/binder slots must + always be present); +- a ``(x : ty = default)`` default may be attached only to a slot + that appears solely inside optional groups; if the same slot also + appears at a mandatory position, no default is needed (or + allowed); +- every form slot that appears only inside optional groups must + declare a default. + +------------------------------------------------------------------------ +Qualified and projected uses +------------------------------------------------------------------------ + +Notations participate in qualified operator lookup, so ``Mod.#foo`` +is accepted wherever the module path makes the notation visible:: + + clone Bigop as BRA with type t <- real, ... + ... + lemma L s : BRA.#big [ x : s ] (f x) = 0%r. + +Projection after a notation call works at the simple-formula level:: + + notation #pair ['a 'b] (a : 'a) (b : 'b) " [" a ", " b "] " = (a, b). + + lemma L (x y : int) : #pair [x, y].`1 = x. + +------------------------------------------------------------------------ +Slot holes and pattern uses +------------------------------------------------------------------------ + +Inside contexts that accept ``_`` patterns (``pose X := ...``, +``rewrite [PATTERN](...)`` and similar), slot arguments may be ``_``: + +- A bare ``_`` as the *entire* slot body creates a meta-variable of + the slot's full curried type — so ``#big [ i : _ | _ ] _`` matches + any ``big P F s`` in the same way ``big _ _ _`` does. +- A ``_`` inside a compound slot body (e.g. ``f _ i``) stands for a + sub-term meta-variable. + +Typical use:: + + (* positional pattern, equivalent to `pose c := big _ _ _' *) + pose c := #big [ i : _ | _ ] _. + + (* targeted rewrite *) + rewrite [#bigi [ i : _, (max _ _) | _ ] _] big_range0r. + +Outside pattern-accepting contexts ``_`` is rejected at typing time +as usual. + +------------------------------------------------------------------------ +Semantics +------------------------------------------------------------------------ + +A notation is compiled to a regular operator of kind ``OB_nott`` that +records the template alongside the typed body. At a call site +``#name [ ... ]``: + +1. The parser looks up the template for ``#name`` and consumes tokens + according to its items, collecting the slot arguments. Form-slot + contents are parsed as **formulas**, so they may contain memory + references, ``Pr[...]`` expressions, and any other formula-level + construct — not just expressions. +2. The resulting ``PFntt`` node is type-checked. For each form slot + with binder dependencies, the argument is type-checked in an + environment extended with the user-chosen binder idents, then + wrapped in ``fun`` over those idents. Eta-reduction is applied + when the slot body is ``f b_1 ... b_n`` with trailing args exactly + matching the binders, so ``F i`` stores as ``F`` (and ``(P \o h) i`` + as ``P \o h``) while ``mem s i`` keeps its lambda wrap. For each + ident slot, a fresh local is created with the user-chosen name. + The body is then obtained by substituting all slot idents with + their resolved values and alpha-renaming each bound binder to the + user-chosen name. + +Because expansion happens at typing, slot-level errors attribute to the +user's source and not to the declaration's body. + +Form slots outside a closing fence parse at **simple-formula** level so +that outer binary operators are not absorbed. Consequently an +application like ``F i`` at a trailing slot position must be +parenthesised:: + + #big [ i : s ] (F i) = 0%r (* correct *) + #big [ i : s ] F i = 0%r (* rejected *) + +Form slots that are fenced by a following punctuation token parse at +full formula level. + +------------------------------------------------------------------------ +Locality +------------------------------------------------------------------------ + +A declaration may be prefixed with ``local`` inside a ``section``; the +notation is then discharged when the section closes:: + + section. + local notation #tmp (a : int) " [" a "] " = a + 1. + lemma inside : #tmp [3] = 4. + proof. by trivial. qed. + end section. + (* #tmp is no longer visible here. *) + +Outside a section, ``local notation`` is rejected, as for other +operators. + +------------------------------------------------------------------------ +Pretty-printing +------------------------------------------------------------------------ + +The pretty-printer reverse-matches the body of each registered notation +against each formula it prints. When a formula matches the body of a +notation, the printer renders it using the template, honouring +whitespace from the declaration's STRING literals:: + + notation #pair (a : int) (b : int) " [" a ", " b "] " = (a, b). + + lemma L (x y : int) : #pair [x, y] = (x, y). + + print L. + (* lemma L: forall (x y : int), #pair [x, y] = #pair [x, y] . *) + +For notations with binder slots, the printer unwraps the matched +lambdas to recover the user's chosen binder names. + +------------------------------------------------------------------------ +Examples +------------------------------------------------------------------------ + +A polymorphic pair:: + + notation #pair ['a 'b] (a : 'a) (b : 'b) " [" a ", " b "] " = (a, b). + + lemma L (x : int) (y : bool) : #pair [x, y] = (x, y). + proof. by trivial. qed. + +A polymorphic map notation with an explicit lambda:: + + notation #pmap ['a 'b] (f : 'a -> 'b) (xs : 'a list) + " [" f " : " xs "] " = + map f xs. + + lemma L : #pmap [(fun x => x + 1) : [1; 2; 3]] = [2; 3; 4]. + proof. by trivial. qed. + +A binder-slot map notation where the user-chosen name scopes into the +body form:: + + notation #mapI #< i : int > (n : int) (f : i ==> int) + " [" i " : " n " : " f "] " = + map f (iota_ 0 n). + + lemma L : #mapI [k : 4 : k + 1] = map (fun k => k + 1) (iota_ 0 4). + proof. by trivial. qed. + +A notation with an optional predicate group (default ``predT``):: + + notation #filter ['a] #< i : 'a > + (xs : 'a list) + (P : i ==> bool = predT) + "[" i " : " xs ("| " P)? "]" = + filter P xs. + + lemma with_P (xs : int list) : + #filter [ i : xs | 0 <= i ] = filter (fun i => 0 <= i) xs. + proof. by trivial. qed. + + lemma without_P (xs : int list) : + #filter [ i : xs ] = filter predT xs. + proof. by trivial. qed. + +A notation inside a section:: + + section. + + notation #gpair (a : int) (b : int) " [" a ", " b "] " = (a, b). + local notation #lpair (a : int) (b : int) " [" a ", " b "] " = (a, b). + + lemma t_g : #gpair [1, 2] = (1, 2). + proof. by trivial. qed. + + lemma t_l : #lpair [1, 2] = (1, 2). + proof. by trivial. qed. + + end section. + + lemma after : #gpair [3, 4] = (3, 4). + proof. by trivial. qed. + +------------------------------------------------------------------------ +Error catalogue +------------------------------------------------------------------------ + +The following errors may appear at notation-declaration or call time. + +``notation punctuation `"x"' must lex to one of: [ ] : | , ;`` + A template STRING could not be lexed to exactly one of the six + accepted punctuation tokens. + +``template references unknown slot: `x'`` + The template refers to a slot name that is not declared as either a + binder slot (``#< ... >``) or a form slot (``( ... )``). + +``parse error: unknown notation `#name'`` + The call site used a notation name that is not in scope. The + notation may not be ``import``-ed, may be ``local`` and out of + scope, or simply not declared. + +``parse error: in notation `#name': expected `:'`` + The call site did not match the template at the indicated punct. + Check that the call reproduces the declaration template verbatim. + +``parse error: in notation `#name': expected identifier for binder slot `i'`` + A binder slot consumes an identifier at the call site; another + token was supplied. A bare ``_`` is accepted here and yields a + fresh anonymous binder name. + +``notation's optional group must be non-empty and start with a punctuation`` + A ``( ... )?`` group was declared without leading punctuation + (e.g. a slot first) or was empty. + +``slot `x' can only have a default if it appears solely inside an optional group`` + ``(x : ty = default)`` was used for a slot that also occurs at a + mandatory template position, where it cannot be absent. + +``slot `x' must declare a default because it only appears inside optional groups`` + A form slot that lives exclusively inside optional groups must + have a default value, so that a well-defined value is bound when + the group is omitted. + +------------------------------------------------------------------------ +Limitations +------------------------------------------------------------------------ + +- The punctuation palette is fixed to the six tokens listed above. + Arbitrary keywords or operator symbols are not accepted because the + lexer tokenizes ahead of the notation-aware parser. + +- Templates cannot describe iteration (e.g. ``item*`` or + ``item, ...``). Optional groups (``( ... )?``) are supported but + repetition is not. Each declaration has a fixed maximum arity. + +- Explicit type-instantiation on a notation call site + (``#foo<:'a * 'b> [...]``) is not accepted. Type arguments must be + inferred from the slot contents; when inference is insufficient, + annotate one of the slot arguments or the enclosing binding. + +- Notation lookup is not overloading-aware: when two clones of the + same underlying theory are imported (e.g. ``BBOr`` and ``BRA`` both + providing ``#big``), the unqualified ``#big`` resolves to a single + candidate by name only, unlike the raw operator ``big`` which is + disambiguated by type. Use a qualified form + (``StdBigop.Bigbool.BBOr.#big``) to select the intended + instantiation. + +- Within a single theory file loaded via ``require``, a notation + declared on line *N* is visible from line *N + 1* onward. In + interactive mode the visibility is immediate. + +- A ``local notation`` must appear inside a ``section``, as for other + ``local`` operators. diff --git a/src/dune b/src/dune index 487e9cfcf5..1f9e599d52 100644 --- a/src/dune +++ b/src/dune @@ -31,4 +31,4 @@ (menhir (modules ecParser) (explain true) - (flags --table --unused-token COMMENT)) + (flags --table --unused-token COMMENT --inspection)) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 2b08923ea9..4dd20f7ce3 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -572,12 +572,24 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) = let i_pragma = Pragma.get () in try_finally (fun () -> - let commands = EcIo.parseall (EcIo.from_file filename) in - let commands = - List.fold_left - (fun scope g -> process_internal subld scope g.gl_action) - iscope commands in - commands) + let reader = EcIo.from_file filename in + let rec loop scope = + let notations = EcEnv.Op.lookup_template (EcScope.env scope) in + match EcLocation.unloc (EcIo.parse ~notations reader) with + | EcParsetree.P_Prog (commands, terminate) -> + let scope = + List.fold_left + (fun scope g -> process_internal subld scope g.gl_action) + scope commands in + if terminate then scope else loop scope + | EcParsetree.P_DocComment _ -> + loop scope + | EcParsetree.P_Undo _ | EcParsetree.P_Exit -> + assert false + in + try_finally + (fun () -> loop iscope) + (fun () -> EcIo.finalize reader)) (fun () -> Pragma.set i_pragma) in diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 2dbd8b27c6..322557b153 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -110,11 +110,37 @@ and opbranch = { opb_sub : opbranches; } +and nt_punct_kind = + [ `LBRACKET | `RBRACKET | `COLON | `PIPE | `COMMA | `SEMICOLON ] + +and nt_punct = { + np_kind : nt_punct_kind; (* lexed token to match at use sites *) + np_display : string; (* verbatim source, for pretty-printing *) +} + +and nt_slot_kind = + | NTS_Form of EcSymbols.symbol list (* binder slots this form depends on, in order *) + | NTS_Ident + +and nt_template_item = + | NTI_Punct of nt_punct + | NTI_Slot of EcSymbols.symbol * nt_slot_kind + | NTI_Optional of nt_template_item list (* first item must be NTI_Punct *) + +and nt_template = { + nt_items : nt_template_item list; + nt_defaults : expr EcIdent.Mid.t; + (* Default value for each slot that only appears inside optional + template groups. Keys are ont_args idents; absent slots → no + default (must appear outside all optional groups). *) +} + and notation = { - ont_args : (EcIdent.t * EcTypes.ty) list; - ont_resty : EcTypes.ty; - ont_body : expr; - ont_ponly : bool; + ont_args : (EcIdent.t * EcTypes.ty) list; + ont_resty : EcTypes.ty; + ont_body : expr; + ont_ponly : bool; + ont_template : nt_template option; } and prind = { @@ -234,10 +260,30 @@ let mk_exception (exn_loca : locality) (exn_dom : ty list) : exception_ = let mk_abbrev ?(ponly = false) tparams xs (codom, body) lc = let kind = { - ont_args = xs; - ont_resty = codom; - ont_body = body; - ont_ponly = ponly; + ont_args = xs; + ont_resty = codom; + ont_body = body; + ont_ponly = ponly; + ont_template = None; + } in + + gen_op ~opaque:optransparent tparams + (EcTypes.toarrow (List.map snd xs) codom) (OB_nott kind) lc + +let mk_notation + (tparams : ty_params) + (xs : (EcIdent.t * EcTypes.ty) list) + ((codom, body) : EcTypes.ty * EcTypes.expr) + (template : nt_template) + (lc : locality) + : operator += + let kind = { + ont_args = xs; + ont_resty = codom; + ont_body = body; + ont_ponly = false; + ont_template = Some template; } in gen_op ~opaque:optransparent tparams diff --git a/src/ecDecl.mli b/src/ecDecl.mli index db24d1950b..cbd2b4425b 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -90,11 +90,34 @@ and opbranch = { opb_sub : opbranches; } +and nt_punct_kind = + [ `LBRACKET | `RBRACKET | `COLON | `PIPE | `COMMA | `SEMICOLON ] + +and nt_punct = { + np_kind : nt_punct_kind; + np_display : string; +} + +and nt_slot_kind = + | NTS_Form of symbol list + | NTS_Ident + +and nt_template_item = + | NTI_Punct of nt_punct + | NTI_Slot of symbol * nt_slot_kind + | NTI_Optional of nt_template_item list + +and nt_template = { + nt_items : nt_template_item list; + nt_defaults : expr EcIdent.Mid.t; +} + and notation = { - ont_args : (EcIdent.t * EcTypes.ty) list; - ont_resty : EcTypes.ty; - ont_body : expr; - ont_ponly : bool; + ont_args : (EcIdent.t * EcTypes.ty) list; + ont_resty : EcTypes.ty; + ont_body : expr; + ont_ponly : bool; + ont_template : nt_template option; } and prind = { @@ -140,6 +163,10 @@ val mk_abbrev : ?ponly:bool -> ty_params -> (EcIdent.ident * ty) list -> ty * expr -> locality -> operator +val mk_notation : + ty_params -> (EcIdent.ident * ty) list + -> ty * expr -> nt_template -> locality -> operator + val operator_as_ctor : operator -> EcPath.path * int val operator_as_rcrd : operator -> EcPath.path val operator_as_proj : operator -> EcPath.path * int * int diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 8a449a7797..8b2be9a4b9 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -2673,6 +2673,14 @@ module Op = struct env_ntbase = update_ntbase (root env) (name, op) env.env_ntbase; env_item = mkitem ~import (Th_operator (name, op)) :: env.env_item; } + let lookup_template (env : env) (qs : qsymbol) + : EcDecl.nt_template_item list option + = + match lookup_opt qs env with + | Some (_, { op_kind = EcDecl.OB_nott { ont_template = Some t; _ }; _ }) -> + Some t.EcDecl.nt_items + | _ -> None + let rebind name op env = MC.bind_operator name op env @@ -3000,7 +3008,6 @@ module Theory = struct in bind_base_th for1 - (* ------------------------------------------------------------------ *) let bind_rd_th = let for1 _path db = function | Th_reduction rules -> diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 04354a391d..ab567450d7 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -344,6 +344,8 @@ module Op : sig val get_notations : head:path option -> env -> (path * notation) list + val lookup_template : env -> qsymbol -> EcDecl.nt_template_item list option + val iter : ?name:qsymbol -> (path -> t -> unit) -> env -> unit val all : ?check:(path -> t -> bool) -> ?name:qsymbol -> env -> (path * t) list end diff --git a/src/ecHiNotations.ml b/src/ecHiNotations.ml index 3d742857c5..d37fef1fb8 100644 --- a/src/ecHiNotations.ml +++ b/src/ecHiNotations.ml @@ -16,6 +16,14 @@ type nterror = | NTE_DupIdent | NTE_UnknownBinder of symbol | NTE_AbbrevIsVar +| NTE_UnknownSlot of symbol +| NTE_DuplicateSlot of symbol +| NTE_TemplateEmpty +| NTE_BadPunct of string +| NTE_OptionalEmpty +| NTE_OptionalMustStartWithPunct +| NTE_DefaultOnNonOptional of symbol +| NTE_MissingDefault of symbol exception NotationError of EcLocation.t * EcEnv.env * nterror @@ -28,44 +36,274 @@ let trans_abbrev_opts (opts : abrvopts) = false opts (* -------------------------------------------------------------------- *) -let trans_notation_r (env : env) (nt : pnotation located) = - let nt = nt.pl_desc and gloc = nt.pl_loc in - let ue = TT.transtyvars env (gloc, nt.nt_tv) in +(* Pipeline stages used by [trans_notation_r]. Kept internal; the + public API is [trans_notation]/[trans_abbrev]. *) +module Internal = struct + +type binder_slots = { + bs_entries : (symbol * (EcIdent.t * ty)) list; + (* (name, ident, type) in declaration order *) + bs_map : (EcIdent.t * ty) Msym.t; + (* name -> (ident, type) for downstream slot lookups *) +} + +type form_slots = { + fs_args : (EcIdent.t * ty) list; + (* ident + curried type, in declaration order *) + fs_map : (EcIdent.t * ty) Msym.t; + (* name -> (ident, curried type) *) + fs_deps : symbol list Msym.t; + (* slot name -> binder-dep names, in order *) + fs_defaults : pformula Msym.t; + (* slot name -> raw default formula (validated at stage 4, + typechecked at stage 5) *) +} - (* Translate bound idents and their types *) - let bd = List.mapi (fun i (x, pty) -> +type template_info = { + ti_items : EcDecl.nt_template_item list; + (* compiled template items; the full [nt_template] record is built + later by combining these with the typechecked defaults *) + ti_seen : bool Msym.t; + (* slot name -> true if its single occurrence is at a mandatory + position, false if only inside an optional group *) +} + +(* Stage 1: compile binder slots (`#< i : ty, j : ty >`). Each slot + becomes a fresh ident paired with its translated type. Rejects + duplicate binder names with [NTE_DupIdent]. *) +let compile_binder_slots + (env : env) + (ue : EcUnify.unienv) + (gloc : EcLocation.t) + (nt_bd : (psymbol * pty) list) + : binder_slots += + let bd = List.map (fun (x, pty) -> let id = EcIdent.create (unloc x) in let ty = TT.transty TT.tp_relax env ue pty in - (unloc x, (i, (id, ty)))) nt.nt_bd in + (unloc x, (id, ty))) nt_bd in if not (List.is_unique ~eq:(fun (x, _) (y, _) -> sym_equal x y) bd) then nterror gloc env NTE_DupIdent; - let bd = Msym.of_list bd in + { bs_entries = bd; bs_map = Msym.of_list bd; } + +(* -------------------------------------------------------------------- *) +(* Stage 2: compile form slots. Each declared `(f : b1, ..., bn ==> ty)` + yields a fresh ident whose type is the curried + `bty_1 -> ... -> bty_n -> ty`, so the body treats the slot as a + function. Also collects the per-slot binder-dep list (stored on the + template) and the raw default formulas — those are validated in + stage 4 and typechecked in stage 5. Rejects duplicate slot names + with [NTE_DupIdent] and unknown binder deps with + [NTE_UnknownBinder]. *) +let compile_form_slots + (env : env) + (ue : EcUnify.unienv) + (gloc : EcLocation.t) + (bd_map : (EcIdent.t * ty) Msym.t) + (nt_args : (psymbol * (psymbol list * pty option) * pformula option) list) + : form_slots += + let abd, args_raw = List.split (List.map (fun (x, (xbd, ty), _dflt) -> + let dty = fun () -> mk_loc (loc x) PTunivar in + let raw = ([mk_loc (loc x) (Some x)], ofdfl dty ty) in + (xbd, raw)) + nt_args) in + + let args_plain = snd (TT.trans_binding env ue args_raw) in + + let args = + List.map2 (fun xbd (aid, aty) -> + let bd_tys = + List.map (fun b -> + match Msym.find_opt (unloc b) bd_map with + | Some (_, t) -> t + | None -> nterror (loc b) env (NTE_UnknownBinder (unloc b))) xbd in + (aid, toarrow bd_tys aty)) abd args_plain in + + if not (List.is_unique ~eq:sym_equal + (List.map (fun (id, _) -> EcIdent.name id) args)) then + nterror gloc env NTE_DupIdent; + + let fs_map = + List.fold_left (fun m (id, ty) -> Msym.add (EcIdent.name id) (id, ty) m) + Msym.empty args in + + let fs_deps = + List.fold_left2 (fun m (x, _, _) xbd -> + Msym.add (unloc x) (List.map unloc xbd) m) + Msym.empty nt_args abd in + + let fs_defaults = + List.fold_left (fun m (x, _, d) -> + match d with + | None -> m + | Some f -> Msym.add (unloc x) f m) + Msym.empty nt_args in + + { fs_args = args; fs_map; fs_deps; fs_defaults; } + +(* -------------------------------------------------------------------- *) +(* Stage 3: compile the surface template. Produces the stored + [nt_template] AND a map [seen] from each referenced slot name to a + bool — [true] if the (single) occurrence is at a mandatory position, + [false] if it is inside an optional group. Each slot may appear at + most once (enforced by [NTE_DuplicateSlot]), so a plain map suffices. + The map drives the default-validation in stage 4. *) +let compile_template + (env : env) + (gloc : EcLocation.t) + (bd_map : (EcIdent.t * ty) Msym.t) + (args_map : (EcIdent.t * ty) Msym.t) + (slot_deps : symbol list Msym.t) + (nt_template : pnt_template) + : template_info += + if List.is_empty nt_template then + nterror gloc env NTE_TemplateEmpty; + + let compile_punct loc str : EcDecl.nt_punct = + let kind = + match EcIo.lex_only_token str with + | Some EcParser.LBRACKET -> `LBRACKET + | Some EcParser.RBRACKET -> `RBRACKET + | Some EcParser.COLON -> `COLON + | Some EcParser.PIPE -> `PIPE + | Some EcParser.COMMA -> `COMMA + | Some EcParser.SEMICOLON -> `SEMICOLON + | _ -> nterror loc env (NTE_BadPunct str) in + { EcDecl.np_kind = kind; np_display = str; } + in + + let rec compile_item ~in_optional seen item = + match item with + | PNTI_Punct p -> + (seen, EcDecl.NTI_Punct (compile_punct (loc p) (unloc p))) - let getident x = - try Msym.find (unloc x) bd - with Not_found -> nterror (loc x) env (NTE_UnknownBinder (unloc x)) + | PNTI_Slot s -> + let name = unloc s in + if Msym.mem name seen then + nterror (loc s) env (NTE_DuplicateSlot name); + let seen = Msym.add name (not in_optional) seen in + if Msym.mem name bd_map then + (seen, EcDecl.NTI_Slot (name, EcDecl.NTS_Ident)) + else if Msym.mem name args_map then + let deps = Msym.find name slot_deps in + (seen, EcDecl.NTI_Slot (name, EcDecl.NTS_Form deps)) + else + nterror (loc s) env (NTE_UnknownSlot name) + + | PNTI_Optional items -> + if List.is_empty items then + nterror gloc env NTE_OptionalEmpty; + (match List.hd items with + | PNTI_Punct _ -> () + | _ -> nterror gloc env NTE_OptionalMustStartWithPunct); + let (seen, compiled) = + List.fold_left (fun (seen, acc) it -> + let (seen, it) = compile_item ~in_optional:true seen it in + (seen, it :: acc)) + (seen, []) items in + (seen, EcDecl.NTI_Optional (List.rev compiled)) in + let ti_seen, template_rev = + List.fold_left (fun (seen, acc) it -> + let (seen, it) = compile_item ~in_optional:false seen it in + (seen, it :: acc)) + (Msym.empty, []) nt_template in + { ti_items = List.rev template_rev; ti_seen; } + +(* -------------------------------------------------------------------- *) +(* Stage 4: validate the default/optional-slot invariants. A slot with + [seen name = false] (only inside an optional group) MUST have a + default — the expansion needs a value when the group is omitted. A + slot with a declared default MUST have [seen name = false] — + otherwise the mandatory occurrence always supplies a value and the + default is unreachable. *) +let check_defaults + (env : env) + (gloc : EcLocation.t) + (slot_dflt_raw : pformula Msym.t) + (seen : bool Msym.t) + : unit += + Msym.iter (fun slot_name _ -> + match Msym.find_opt slot_name seen with + | Some false -> () + | _ -> nterror gloc env (NTE_DefaultOnNonOptional slot_name)) + slot_dflt_raw; + Msym.iter (fun slot_name is_mandatory -> + if not is_mandatory && not (Msym.mem slot_name slot_dflt_raw) then + nterror gloc env (NTE_MissingDefault slot_name)) + seen + +(* -------------------------------------------------------------------- *) +(* Stage 5: typecheck each declared default at the slot's curried + type in the body environment [benv], so the default may reference + any binder or slot the body can reference. *) +let typecheck_defaults + (ue : EcUnify.unienv) + (benv : env) + (args : (EcIdent.t * ty) list) + (slot_dflt_raw : pformula Msym.t) + : expr EcIdent.Mid.t += + let args_by_name = + List.fold_left (fun m (id, ty) -> + Msym.add (EcIdent.name id) (id, ty) m) + Msym.empty args in + Msym.fold (fun slot_name dflt_pf acc -> + let (slot_id, slot_ty) = Msym.find slot_name args_by_name in + let pe = mk_loc (loc dflt_pf) (Expr dflt_pf) in + let dflt_e = TT.transexpcast benv `InOp ue slot_ty pe in + EcIdent.Mid.add slot_id dflt_e acc) + slot_dflt_raw EcIdent.Mid.empty + +end - (* Translate formal arguments and theiry types *) - let abd, xs = List.split (List.map (fun (x, (xbd, ty)) -> - let dty = fun () -> mk_loc (loc x) (PTunivar) in - let arg = ([mk_loc (loc x) (Some x)], ofdfl dty ty) in - (List.map getident xbd, arg)) nt.nt_args) in +(* -------------------------------------------------------------------- *) +let trans_notation_r (env : env) (nt : pnotation located) = + let nt = nt.pl_desc and gloc = nt.pl_loc in + let ue = TT.transtyvars env (gloc, nt.nt_tv) in + + let bs = Internal.compile_binder_slots env ue gloc nt.nt_bd in + let fs = Internal.compile_form_slots env ue gloc bs.bs_map nt.nt_args in - let xs = List.map2 (fun xty (aid, aty) -> - (aid, toarrow (List.map (snd -| snd) xty) aty)) - abd (snd (TT.trans_binding env ue xs)) in + (* Body env: binder idents + form-slot idents (with curried types). *) + let all_locals = List.map snd bs.bs_entries @ fs.fs_args in + let benv = EcEnv.Var.bind_locals all_locals env in + let codom = TT.transty TT.tp_relax env ue nt.nt_codom in + let body_pe = mk_loc (loc nt.nt_body) (Expr nt.nt_body) in + let body = TT.transexpcast benv `InOp ue codom body_pe in - let benv = EcEnv.Var.bind_locals xs env in - let codom = TT.transty TT.tp_relax env ue nt.nt_codom in - let body = TT.transexpcast benv `InOp ue codom nt.nt_body in + let ti = + Internal.compile_template env gloc bs.bs_map fs.fs_map fs.fs_deps + nt.nt_template in + + Internal.check_defaults env gloc fs.fs_defaults ti.ti_seen; + + let defaults = Internal.typecheck_defaults ue benv fs.fs_args fs.fs_defaults in if not (EcUnify.UniEnv.closed ue) then nterror gloc env NTE_TyNotClosed; - ignore body; () + let ts = Tuni.subst (EcUnify.UniEnv.close ue) in + let es = e_subst ts in + let body = es body in + let codom = ty_subst ts codom in + let all_xs = List.map (snd_map (ty_subst ts)) all_locals in + let defaults = EcIdent.Mid.map es defaults in + + let template : EcDecl.nt_template = { + nt_items = ti.ti_items; + nt_defaults = defaults; + } in + let tparams = EcUnify.UniEnv.tparams ue in + let op = EcDecl.mk_notation tparams all_xs (codom, body) + template (nt.nt_local :> locality) in + + (unloc nt.nt_name, op) (* -------------------------------------------------------------------- *) let trans_notation (env : EcEnv.env) (nt : pnotation located) = diff --git a/src/ecHiNotations.mli b/src/ecHiNotations.mli index 54dd54543e..32872cf0dd 100644 --- a/src/ecHiNotations.mli +++ b/src/ecHiNotations.mli @@ -12,11 +12,19 @@ type nterror = | NTE_DupIdent | NTE_UnknownBinder of symbol | NTE_AbbrevIsVar +| NTE_UnknownSlot of symbol +| NTE_DuplicateSlot of symbol +| NTE_TemplateEmpty +| NTE_BadPunct of string +| NTE_OptionalEmpty +| NTE_OptionalMustStartWithPunct +| NTE_DefaultOnNonOptional of symbol +| NTE_MissingDefault of symbol exception NotationError of EcLocation.t * EcEnv.env * nterror val nterror : EcLocation.t -> env -> nterror -> 'a (* -------------------------------------------------------------------- *) -val trans_notation : env -> pnotation located -> unit -val trans_abbrev : env -> pabbrev located -> symbol * operator +val trans_notation : env -> pnotation located -> symbol * operator +val trans_abbrev : env -> pabbrev located -> symbol * operator diff --git a/src/ecIo.ml b/src/ecIo.ml index 016545d85c..e8ed8d1f8a 100644 --- a/src/ecIo.ml +++ b/src/ecIo.ml @@ -1,6 +1,7 @@ (* -------------------------------------------------------------------- *) open EcUtils +module A = EcParsetree module P = EcParser module L = Lexing module I = EcParser.MenhirInterpreter @@ -32,23 +33,31 @@ let isuniop_fun () : unit parser_t = MenhirLib.Convert.Simplified.traditional2revised EcParser.is_uniop (* -------------------------------------------------------------------- *) +type lctoken = EcParser.token * L.position * L.position + type ecreader_r = { - (*---*) ecr_lexbuf : Lexing.lexbuf; - (*---*) ecr_source : Buffer.t; - mutable ecr_atstart : bool; - mutable ecr_trim : int; - mutable ecr_tokens : EcParser.token list; + (*---*) ecr_lexbuf : Lexing.lexbuf; + (*---*) ecr_source : Buffer.t; + mutable ecr_atstart : bool; + mutable ecr_trim : int; + mutable ecr_tokens : lctoken list; + mutable ecr_lkahead : lctoken option; + mutable ecr_is_nt_name : string -> bool; + mutable ecr_prev_token : EcParser.token option; } type ecreader = ecreader_r Disposable.t (* -------------------------------------------------------------------- *) let ecreader_of_lexbuf (buffer : Buffer.t) (lexbuf : L.lexbuf) : ecreader_r = - { ecr_lexbuf = lexbuf; - ecr_source = buffer; - ecr_atstart = true; - ecr_trim = 0; - ecr_tokens = []; } + { ecr_lexbuf = lexbuf; + ecr_source = buffer; + ecr_atstart = true; + ecr_trim = 0; + ecr_tokens = []; + ecr_lkahead = None; + ecr_is_nt_name = (fun _ -> false); + ecr_prev_token = None; } (* -------------------------------------------------------------------- *) let lexbuf (reader : ecreader) = @@ -108,42 +117,60 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) = ecreader.ecr_trim <- ecreader.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum; while List.is_empty (ecreader.ecr_tokens) do - match EcLexer.main lexbuf with + let tokens = EcLexer.main lexbuf in + let lstart = Lexing.lexeme_start_p lexbuf in + let lend = Lexing.lexeme_end_p lexbuf in + let locate (tks : P.token list) : lctoken list = + List.map (fun tk -> (tk, lstart, lend)) tks in + match tokens with | [COMMENT] -> if ecreader.ecr_atstart then ecreader.ecr_trim <- (Lexing.lexeme_end_p ecreader.ecr_lexbuf).pos_cnum - | [DOCCOMMENT _] as tokens -> + | [DOCCOMMENT _] -> if ecreader.ecr_atstart then - ecreader.ecr_tokens <- tokens + ecreader.ecr_tokens <- locate tokens | tokens -> - ecreader.ecr_tokens <- tokens + ecreader.ecr_tokens <- locate tokens done; let token, queue = List.destruct ecreader.ecr_tokens in let token, prequeue = match checkpoint, token with - | Some checkpoint, P.DECIMAL (pre, (_, post)) -> - if I.acceptable checkpoint token lexbuf.lex_curr_p then + | Some checkpoint, ((P.DECIMAL (pre, (_, post))) as tk, lstart, lend) -> + if I.acceptable checkpoint tk lexbuf.lex_curr_p then token, [] else - List.destruct P.[UINT pre; DOT; UINT post] + let tokens = P.[UINT pre; DOT; UINT post] in + let tokens = List.map (fun tk -> (tk, lstart, lend)) tokens in + List.destruct tokens + | Some checkpoint, (P.NIDENT n, lstart, lend) + when ecreader.ecr_prev_token <> Some P.DOT + && not (ecreader.ecr_is_nt_name n) + && I.acceptable checkpoint P.SHARP lexbuf.lex_curr_p -> + let suffix = String.sub n 1 (String.length n - 1) in + let tokens = P.[SHARP; LIDENT suffix] in + let tokens = List.map (fun tk -> (tk, lstart, lend)) tokens in + List.destruct tokens | _ -> token, [] in ecreader.ecr_tokens <- prequeue @ queue; - if isfinal token then + let raw = proj3_1 token in + if isfinal raw then ecreader.ecr_atstart <- true else ecreader.ecr_atstart <- ecreader.ecr_atstart && ( - match token with + match raw with | P.DOCCOMMENT _ | P.COMMENT -> true | _ -> false ); - (token, Lexing.lexeme_start_p lexbuf, Lexing.lexeme_end_p lexbuf) + ecreader.ecr_lkahead <- Some token; + ecreader.ecr_prev_token <- Some raw; + token (* -------------------------------------------------------------------- *) let drain (ecreader : ecreader) = @@ -155,43 +182,307 @@ let drain (ecreader : ecreader) = | _ | exception EcLexer.LexicalError _ -> drain () in if not ecreader.ecr_atstart then - drain () + drain (); + ecreader.ecr_lkahead <- None + +(* -------------------------------------------------------------------- *) +(* Notation parse-time dispatcher. Reads a `#name [...]` call site by + driving the menhir parser's [N_nttstart] reduction: collects the + notation name, consumes template punctuation, reads identifier slots + and recursively-parsed form slots, then synthesizes the + [NTTINSTANCE] token the grammar expects. *) +module Notations = struct + +type t = EcSymbols.qsymbol -> EcDecl.nt_template_item list option + +let empty : t = fun _ -> None (* -------------------------------------------------------------------- *) -let parse (ecreader : ecreader) : EcParsetree.prog = +(* Low-level lookahead/error helpers, used only by the dispatcher. *) + +let pushback_lookahead (ecreader : ecreader_r) : unit = + ecreader.ecr_tokens <- Option.to_list ecreader.ecr_lkahead @ ecreader.ecr_tokens; + ecreader.ecr_lkahead <- None + +let show_qsymbol ((ns, x) : EcSymbols.qsymbol) : string = + String.concat "." (ns @ [x]) + +let punct_kind_name : EcDecl.nt_punct_kind -> string = function + | `LBRACKET -> "`['" + | `RBRACKET -> "`]'" + | `COLON -> "`:'" + | `PIPE -> "`|'" + | `COMMA -> "`,'" + | `SEMICOLON -> "`;'" + +let parse_error_loc (loc : EcLocation.t) (msg : string) : 'a = + raise (EcParsetree.ParseError (loc, Some msg)) + +let cur_loc (ecreader : ecreader_r) : EcLocation.t = + let lexbuf = ecreader.ecr_lexbuf in + EcLocation.make lexbuf.L.lex_start_p lexbuf.L.lex_curr_p + +(* -------------------------------------------------------------------- *) +(* Consume the next token and require it to be the punct [p]. Returns + the end position (for instance-span tracking). Raises a located + ParseError on mismatch. *) +let eat + ~(notation : string) + (ecreader : ecreader_r) + (p : EcDecl.nt_punct) + : L.position += + pushback_lookahead ecreader; + let (tk, startp, endp) = lexer ecreader in + let ok = + match tk, p.EcDecl.np_kind with + | EcParser.LBRACKET , `LBRACKET + | EcParser.RBRACKET , `RBRACKET + | EcParser.COLON , `COLON + | EcParser.PIPE , `PIPE + | EcParser.COMMA , `COMMA + | EcParser.SEMICOLON, `SEMICOLON -> true + | _ -> false + in + if ok then begin + ecreader.ecr_lkahead <- None; + endp + end else + parse_error_loc (EcLocation.make startp endp) + (Printf.sprintf "in notation `%s': expected %s" notation + (punct_kind_name p.EcDecl.np_kind)) + +(* Reads an lident (or `_` for a fresh anonymous name) for a binder + slot. Returns (arg, end_pos). *) +let read_ident_slot + ~(notation : string) + ~(slot : string) + (ecreader : ecreader_r) + : A.pformula option * L.position += + pushback_lookahead ecreader; + match lexer ecreader with + | (EcParser.LIDENT x, lstart, lend) -> + ecreader.ecr_lkahead <- None; + let loc = EcLocation.make lstart lend in + let sym = EcLocation.mk_loc loc ([], x) in + Some (EcLocation.mk_loc loc (A.PFident (sym, None))), lend + | (EcParser.UNDERSCORE, lstart, lend) -> + ecreader.ecr_lkahead <- None; + let loc = EcLocation.make lstart lend in + let name = Printf.sprintf "_%s" slot in + let sym = EcLocation.mk_loc loc ([], name) in + Some (EcLocation.mk_loc loc (A.PFident (sym, None))), lend + | (_, lstart, lend) -> + parse_error_loc (EcLocation.make lstart lend) + (Printf.sprintf + "in notation `%s': expected identifier for binder slot `%s'" + notation slot) + +(* Peek the next non-consumed token without consuming it. Returns the + punctuation kind if the next token is one of the six template + puncts, [None] otherwise. Used by [collect_instance] to decide + whether an optional group's trigger fires. *) +let peek_punct (ecreader : ecreader_r) : EcDecl.nt_punct_kind option = + pushback_lookahead ecreader; + let (tk, _, _) as lc = lexer ecreader in + ecreader.ecr_lkahead <- Some lc; + match tk with + | EcParser.LBRACKET -> Some `LBRACKET + | EcParser.RBRACKET -> Some `RBRACKET + | EcParser.COLON -> Some `COLON + | EcParser.PIPE -> Some `PIPE + | EcParser.COMMA -> Some `COMMA + | EcParser.SEMICOLON -> Some `SEMICOLON + | _ -> None + +(* Mark every slot inside a non-triggered optional group as absent, so + the typechecker substitutes the stored default for each. [acc] is + the running list of [(slot_name, arg_opt)] entries in REVERSE order + (the [collect_instance] caller reverses it at the end). *) +let rec mark_absent + (acc : (EcSymbols.symbol * A.pformula option) list) + (items : EcDecl.nt_template_item list) + : (EcSymbols.symbol * A.pformula option) list += + match items with + | [] -> acc + | EcDecl.NTI_Slot (s, _) :: tl -> mark_absent ((s, None) :: acc) tl + | EcDecl.NTI_Punct _ :: tl -> mark_absent acc tl + | EcDecl.NTI_Optional sub :: tl -> mark_absent (mark_absent acc sub) tl + +(* -------------------------------------------------------------------- *) +(* Collect the notation name and slot args, then synthesize the + NTTINSTANCE token payload with the real source span. Returns the + updated menhir env. *) +let collect_instance + (ecreader : ecreader_r) + (notations : t) + (parse_form_slot : + level:[`Form | `SForm] -> ecreader_r -> A.pformula) + (env : 'a I.env) + (production : I.production) + : 'a I.env += + let env = I.force_reduction production env in + let name, name_loc, startp = + let Element (s, ntt, startp, _endp) = Option.get (I.top env) in + match I.incoming_symbol s with + | N (N_nttstart) -> + (EcLocation.unloc ntt, EcLocation.loc ntt, startp) + | _ -> assert false in + let name_str = show_qsymbol name in + let template = + match notations name with + | None -> + parse_error_loc name_loc + (Printf.sprintf "unknown notation `%s'" name_str) + | Some t -> t in + + (* Walk template items consuming input. [present] accumulates + (slot_name, arg_opt) entries in REVERSE order. *) + let endp = ref startp in + let rec step present = function + | [] -> present + + | EcDecl.NTI_Slot (slot, EcDecl.NTS_Ident) :: rest -> + let arg, e = read_ident_slot ~notation:name_str ~slot ecreader in + endp := e; + step ((slot, arg) :: present) rest + + | EcDecl.NTI_Slot (slot, EcDecl.NTS_Form _) :: rest -> + (* A form slot is "fenced" at form-level iff the next thing that + might appear is a PUNCT (either immediately or as the trigger + of an optional group). Otherwise it's trailing; parse at + sform-level so it doesn't absorb outer operators. *) + let level = + match rest with + | EcDecl.NTI_Punct _ :: _ -> `Form + | EcDecl.NTI_Optional (EcDecl.NTI_Punct _ :: _) :: _ -> `Form + | _ -> `SForm in + let f = parse_form_slot ~level ecreader in + step ((slot, Some f) :: present) rest + + | EcDecl.NTI_Punct tk :: rest -> + endp := eat ~notation:name_str ecreader tk; + step present rest + + | EcDecl.NTI_Optional items :: rest -> + let trigger = + match items with + | EcDecl.NTI_Punct t :: _ -> t.EcDecl.np_kind + | _ -> assert false in + match peek_punct ecreader with + | Some k when k = trigger -> + (* Splice the group's items into the continuation so trailing + form slots inside the group see the outer [rest] as their + fence. *) + step present (items @ rest) + | _ -> + step (mark_absent present items) rest in + let args = List.rev (step [] template) in + + pushback_lookahead ecreader; + I.feed (T T_NTTINSTANCE) startp args !endp env + +(* Parse a quoted form appearing inside a notation slot; delimited by + the `form error` production so parsing accepts once the next token + doesn't continue the form. Nested notations resolve recursively. + + [level] selects the precedence bracket at which the slot's form is + parsed: [`Form] lets the form greedily slurp low-precedence operators + (equality, chained orderings) up to the next token that the form + grammar can't extend with; [`SForm] stops at sform boundaries so + operators like [=] are left to the outer context. Use [`Form] for + slots fenced by a following punct, [`SForm] for trailing slots. *) +let rec parse_quoted_formula + ~(level : [`Form | `SForm]) + (ecreader : ecreader_r) + (notations : t) + : A.pformula += + let rec go (checkpoint : A.pformula I.checkpoint) : A.pformula = + match checkpoint with + | Accepted pst -> pst + + | I.Rejected -> + parse_error_loc (cur_loc ecreader) + "parse error in notation slot" + + | InputNeeded _ -> + go (I.offer checkpoint (lexer ~checkpoint ecreader)) + + | HandlingError _ | Shifting _ -> + go (I.resume checkpoint) + + | AboutToReduce (env, production) -> + match I.lhs production with + | X (N N_nttstart) -> + let env = + collect_instance ecreader notations + (fun ~level:inner r -> + parse_quoted_formula ~level:inner r notations) + env production in + go (I.offer (I.input_needed env) (lexer ecreader)) + | _ -> + go (I.resume checkpoint) + in + pushback_lookahead ecreader; + let start = + match level with + | `Form -> EcParser.Incremental.ntt_form + | `SForm -> EcParser.Incremental.ntt_sform in + go (start ecreader.ecr_lexbuf.lex_curr_p) + +end + +(* -------------------------------------------------------------------- *) +let parse ?(notations : Notations.t = Notations.empty) (ecreader : ecreader) = let ecreader = Disposable.get ecreader in + ecreader.ecr_is_nt_name <- + (fun n -> Option.is_some (notations ([], n))); - let rec parse (checkpoint : EcParsetree.prog I.checkpoint) : EcParsetree.prog = + let rec parse (checkpoint : A.prog I.checkpoint) : EcParsetree.prog = match checkpoint with | Accepted pst -> pst + | Rejected -> + raise (EcParsetree.ParseError (Notations.cur_loc ecreader, None)) + | InputNeeded _ -> parse (I.offer checkpoint (lexer ~checkpoint ecreader)) - | Shifting _ | AboutToReduce _ | HandlingError _ -> + | HandlingError _ | Shifting _ -> parse (I.resume checkpoint) - | Rejected -> - raise EcParser.Error + | AboutToReduce (env, production) -> + match I.lhs production with + | X (N N_nttstart) -> + let env = + Notations.collect_instance ecreader notations + (fun ~level r -> Notations.parse_quoted_formula ~level r notations) + env production in + parse (I.offer (I.input_needed env) (lexer ecreader)) + | _ -> parse (I.resume checkpoint) in parse (EcParser.Incremental.prog ecreader.ecr_lexbuf.lex_curr_p) (* -------------------------------------------------------------------- *) -let xparse (ecreader : ecreader) : string * EcParsetree.prog = +let xparse ?notations (ecreader : ecreader) : string * EcParsetree.prog = let ecr = Disposable.get ecreader in let p1 = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum in - let cd = parse ecreader in + let cd = parse ?notations ecreader in let p2 = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum in let p1 = max p1 ecr.ecr_trim in (Buffer.sub ecr.ecr_source p1 (p2 - p1), cd) (* -------------------------------------------------------------------- *) -let parseall (ecreader : ecreader) = +let parseall ?notations (ecreader : ecreader) = let rec aux acc = - match EcLocation.unloc (parse ecreader) with + match EcLocation.unloc (parse ?notations ecreader) with | EcParsetree.P_Prog (commands, terminate) -> let acc = List.rev_append commands acc in if terminate then List.rev acc else aux acc @@ -208,6 +499,26 @@ let lex_single_token (name : string) = | token :: _ -> Some token | _ | exception EcLexer.LexicalError _ -> None +(* Lex the entire string and require it to produce exactly one token (with + only whitespace around it). Returns [None] if the string contains more + than one token, a lexical error, or nothing. Trailing EOF is tolerated. *) +let lex_only_token (name : string) : EcParser.token option = + let is_trailing_noise = function + | EcParser.EOF + | EcParser.COMMENT -> true + | _ -> false in + let lexbuf = Lexing.from_string name in + match EcLexer.main lexbuf with + | exception EcLexer.LexicalError _ -> None + | [] -> None + | token :: rest -> + if not (List.is_empty rest) then None + else + match EcLexer.main lexbuf with + | exception EcLexer.LexicalError _ -> None + | toks when List.for_all is_trailing_noise toks -> Some token + | _ -> None + (* -------------------------------------------------------------------- *) let is_sym_ident x = match lex_single_token x with diff --git a/src/ecIo.mli b/src/ecIo.mli index 42d28ba740..73fe016e5e 100644 --- a/src/ecIo.mli +++ b/src/ecIo.mli @@ -6,16 +6,27 @@ val from_channel : ?close:bool -> name:string -> in_channel -> ecreader val from_file : string -> ecreader val from_string : string -> ecreader +(* -------------------------------------------------------------------- *) +module Notations : sig + (* Callback driving template lookup at parse time. Receives the full + qualified symbol of the notation reference (e.g. `["Dst"], "#foo"`) + and returns the template items if one is registered. *) + type t = EcSymbols.qsymbol -> EcDecl.nt_template_item list option + + val empty : t +end + (* -------------------------------------------------------------------- *) val finalize : ecreader -> unit -val xparse : ecreader -> string * EcParsetree.prog -val parse : ecreader -> EcParsetree.prog -val parseall : ecreader -> EcParsetree.global list +val xparse : ?notations:Notations.t -> ecreader -> string * EcParsetree.prog +val parse : ?notations:Notations.t -> ecreader -> EcParsetree.prog +val parseall : ?notations:Notations.t -> ecreader -> EcParsetree.global list val drain : ecreader -> unit val lexbuf : ecreader -> Lexing.lexbuf (* -------------------------------------------------------------------- *) val lex_single_token : string -> EcParser.token option +val lex_only_token : string -> EcParser.token option val is_sym_ident : string -> bool val is_op_ident : string -> bool val is_mem_ident : string -> bool diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 704b0e9764..fd2001b632 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -345,6 +345,7 @@ let lident = (lower ichar*) | ('_' ichar+) let uident = upper ichar* let tident = '\'' lident let mident = '&' (lident | uint) +let nident = '#' lident let opchar = ['=' '<' '>' '+' '-' '*' '/' '\\' '%' '&' '^' '|' ':' '#' '$'] @@ -364,6 +365,12 @@ rule main = parse | uident as id { try [Hashtbl.find keywords id] with Not_found -> [UIDENT id] } | tident { [TIDENT (Lexing.lexeme lexbuf)] } | mident { [MIDENT (Lexing.lexeme lexbuf)] } + | nident as n { + let suffix = String.sub n 1 (String.length n - 1) in + match Hashtbl.find_opt keywords suffix with + | Some kw -> [SHARP; kw] + | None -> [NIDENT n] + } | uint { [UINT (BI.of_string (Lexing.lexeme lexbuf))] } | uxint { [UINT (BI.of_string (Lexing.lexeme lexbuf))] } diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 29a4617cb0..ccac53c6dd 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -1144,6 +1144,13 @@ let f_match_core opts hyps (ue, ev) f1 f2 = failure (); doit env (subst, mxs) f1' f2' in + let try_etared () = + let f1' = EcReduction.eta_norm f1 in + let f2' = EcReduction.eta_norm f2 in + if f1 == (*phy*) f1' && f2 == (*phy*) f2' then + failure (); + doit env (subst, mxs) f1' f2' in + let try_horder () = if not opts.fm_horder then failure (); @@ -1193,7 +1200,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 = List.find_map_opt (fun doit -> try Some (doit ()) with MatchFailure -> None) - [try_betared; try_horder; try_delta; default] + [try_betared; try_etared; try_horder; try_delta; default] |> oget ~exn:MatchFailure and doit_args env ilc fs1 fs2 = diff --git a/src/ecParser.mly b/src/ecParser.mly index 65cd97b95f..5b165952ec 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -141,35 +141,9 @@ (Some "cannot mark with 'declare' this kind of objects ") (* ------------------------------------------------------------------ *) - type prover = - [ `Exclude | `Include | `Only] * psymbol - - type pi = [ - | `DBHINT of pdbhint - | `INT of int - | `PROVER of prover list - ] - - type smt = [ - | `ALL - | `ITERATE - | `QUORUM of int - | `MAXLEMMAS of int option - | `MAXPROVERS of int - | `PROVER of prover list - | `TIMEOUT of int - | `UNWANTEDLEMMAS of EcParsetree.pdbhint - | `WANTEDLEMMAS of EcParsetree.pdbhint - | `VERBOSE of int option - | `VERSION of [ `Full | `Lazy ] - | `DUMPIN of string located - | `SELECTED - | `DEBUG - ] - module SMT : sig - val mk_pi_option : psymbol -> pi option -> smt - val mk_smt_option : smt list -> pprover_infos + val mk_pi_option : psymbol -> psmt_prover_info option -> psmt + val mk_smt_option : psmt list -> pprover_infos val simple_smt_option : pprover_infos end = struct let option_matching tomatch = @@ -243,7 +217,7 @@ let msg = Printf.sprintf "`%s`: no option expected" (unloc s) in parse_error s.pl_loc (Some msg) - let mk_pi_option (s : psymbol) (o : pi option) : smt = + let mk_pi_option (s : psymbol) (o : psmt_prover_info option) : psmt = let s = option_matching s in match unloc s with @@ -263,7 +237,7 @@ | "debug" -> get_as_none s o; (`DEBUG) | _ -> assert false - let mk_smt_option (os : smt list) = + let mk_smt_option (os : psmt list) = let mprovers = ref None in let timeout = ref None in let pnames = ref None in @@ -357,6 +331,7 @@ %token UIDENT %token TIDENT %token MIDENT +%token NIDENT %token PUNIOP %token PBINOP %token PNUMOP @@ -373,7 +348,6 @@ %token<[`Raw|`Eq]> RING %token<[`Raw|`Eq]> FIELD - %token ABORT %token ABBREV %token ABSTRACT @@ -604,11 +578,14 @@ %token WLOG %token WP %token ZETA + %token NOP LOP1 ROP1 LOP2 ROP2 LOP3 ROP3 LOP4 ROP4 NUMOP %token LTCOLON DASHLT GT LT GE LE LTSTARGT LTLTSTARGT LTSTARGTGT %token FINAL %token DOCCOMMENT +%token <(EcSymbols.symbol * EcParsetree.pformula option) list> NTTINSTANCE + %nonassoc prec_below_comma %nonassoc COMMA ELSE @@ -643,14 +620,16 @@ %nonassoc prec_tactic -%type global -%type prog +%type global +%type prog +%type ntt_form +%type ntt_sform %type is_uniop %type is_binop %type is_numop -%start prog global is_uniop is_binop is_numop +%start prog global ntt_form ntt_sform is_uniop is_binop is_numop %% (* -------------------------------------------------------------------- *) @@ -691,10 +670,16 @@ _lident: %inline _mident: | x=MIDENT { x } +%inline _nident: +| x=NIDENT { x } + +%inline nqident: x=genqident(_nident) { x } + %inline lident: x=loc(_lident) { x } %inline uident: x=loc(_uident) { x } %inline tident: x=loc(_tident) { x } %inline mident: x=loc(_mident) { x } +%inline nident: x=loc(_nident) { x } %inline _ident: | x=_lident { x } @@ -1138,6 +1123,9 @@ sform_u(P): { let id = PFident(mk_loc op.pl_loc EcCoreLib.s_dinter, ti) in PFapp(mk_loc op.pl_loc id, [e1; e2]) } +| name=nttstart args=NTTINSTANCE + { PFntt { pnt_name = name; pnt_args = args } } + match_body(P): | bs=plist0(p=mcptn(sbinop) IMPL bf=form_r(P) { (p, bf) }, PIPE) { bs } @@ -1919,25 +1907,44 @@ nt_argty: nt_arg1: | x=ident - { (x, ([], None)) } + { (x, ([], None), None) } | LPAREN x=ident COLON ty=nt_argty RPAREN - { (x, snd_map some ty) } + { (x, snd_map some ty, None) } + +| LPAREN x=ident COLON ty=nt_argty EQ dflt=form RPAREN + { (x, snd_map some ty, Some dflt) } nt_bindings: | DASHLT bd=plist0(nt_binding1, COMMA) GT { bd } +nt_template_item: +| s=loc(STRING) { PNTI_Punct s } +| x=ident { PNTI_Slot x } +| LPAREN items=nt_template_item+ RPAREN QUESTION + { PNTI_Optional items } + +nt_template: +| first=loc(STRING) rest=nt_template_item* + { PNTI_Punct first :: rest } + notation: -| locality=loc(locality) NOTATION x=loc(NOP) tv=tyvars_decl? bd=nt_bindings? - args=nt_arg1* codom=prefix(COLON, loc(type_exp))? EQ body=expr - { { nt_name = x; - nt_tv = tv; - nt_bd = odfl [] bd; - nt_args = args; - nt_codom = ofdfl (fun () -> mk_loc (loc body) PTunivar) codom; - nt_body = body; - nt_local = locality_as_local locality; } } +| locality=loc(locality) NOTATION name=nident + tv=tyvars_decl? + bd=nt_bindings? + args=nt_arg1* + tpl=nt_template + codom=prefix(COLON, loc(type_exp))? + EQ body=form + { { nt_name = name; + nt_tv = tv; + nt_bd = odfl [] bd; + nt_args = args; + nt_template = tpl; + nt_codom = ofdfl (fun () -> mk_loc (loc body) PTunivar) codom; + nt_body = body; + nt_local = locality_as_local locality; } } abrvopt: | b=boption(MINUS) x=ident { @@ -1968,6 +1975,15 @@ abbreviation: mempred_binding: | TICKBRACE u=uident+ RBRACE { PT_MemPred u } +nttstart: (* DO NOT MAKE THIS INLINE *) +| nqident { $1 } + +ntt_form: (* DO NOT MAKE THIS INLINE *) +| form_h error { $1 } + +ntt_sform: (* DO NOT MAKE THIS INLINE *) +| sform_h error { $1 } + (* -------------------------------------------------------------------- *) (* Global entries *) diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index fa83d6e698..9f98eb7cc6 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -252,6 +252,8 @@ and pformula_r = | PFprob of psymbol option * pgamepath * (pformula list) * pmemory * pformula | PFBDhoareF of psymbol option * pformula * pgamepath * pformula * phoarecmp * pformula + | PFntt of pntt_instance + and pmemtype_el = ([`Single|`Tuple] * (psymbol list)) located * pty and pmemtype = pmemtype_el list @@ -293,6 +295,14 @@ and pmodule_type_restr = { pmty_pq : pqsymbol; pmty_mem : pmod_restr option; } +(* [pnt_args] is a list of (slot name, argument) pairs. The argument is + [None] when an optional template group did not trigger and the + typechecker should substitute the slot's default. *) +and pntt_instance = { + pnt_name : pqsymbol; + pnt_args : (EcSymbols.symbol * pformula option) list; +} + (* -------------------------------------------------------------------- *) (* qident optionally taken in a (implicit) module parameters. *) and qident_inparam = { inp_in_params : bool; @@ -505,14 +515,31 @@ type ppredicate = { } (* -------------------------------------------------------------------- *) +(* A template punctuation is a quoted STRING at declaration-time. Its *) +(* content must lex to exactly one of the six accepted punctuations, but *) +(* the enclosing whitespace is preserved for pretty-printing. *) +(* *) +(* An optional group [PNTI_Optional items] is a sequence of template *) +(* items that may be absent at a call site; its first item must be a *) +(* PUNCT (the trigger). At parse time a single-token peek decides *) +(* whether to consume the group. Slots referenced only inside optional *) +(* groups may declare a default value (see [nt_args]). *) +type pnt_template_item = + | PNTI_Punct of string located + | PNTI_Slot of psymbol + | PNTI_Optional of pnt_template_item list + +type pnt_template = pnt_template_item list + type pnotation = { - nt_name : psymbol; - nt_tv : ptyvardecls option; - nt_bd : (psymbol * pty) list; - nt_args : (psymbol * (psymbol list * pty option)) list; - nt_codom : pty; - nt_body : pexpr; - nt_local : is_local; + nt_name : psymbol; (* #name with location *) + nt_tv : ptyvardecls option; + nt_bd : (psymbol * pty) list; + nt_args : (psymbol * (psymbol list * pty option) * pformula option) list; + nt_template : pnt_template; + nt_codom : pty; + nt_body : pformula; + nt_local : is_local; } (* -------------------------------------------------------------------- *) @@ -861,6 +888,7 @@ and pcfold = (* -------------------------------------------------------------------- *) type include_exclude = [ `Include | `Exclude ] + type pdbmap1 = { pht_flag : include_exclude; pht_kind : [ `Theory | `Lemma ]; @@ -869,6 +897,32 @@ type pdbmap1 = { and pdbhint = pdbmap1 list +type psmtprover = + [include_exclude | `Only] * psymbol + +type psmt_prover_info = [ +| `DBHINT of pdbhint +| `INT of int +| `PROVER of psmtprover list +] + +type psmt = [ + | `ALL + | `ITERATE + | `QUORUM of int + | `MAXLEMMAS of int option + | `MAXPROVERS of int + | `PROVER of psmtprover list + | `TIMEOUT of int + | `UNWANTEDLEMMAS of pdbhint + | `WANTEDLEMMAS of pdbhint + | `VERBOSE of int option + | `VERSION of [ `Full | `Lazy ] + | `DUMPIN of string located + | `SELECTED + | `DEBUG +] + (* -------------------------------------------------------------------- *) type pprover_list = { pp_use_only : string located list; diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index b5f4e20300..9ac78f3c3d 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -1565,6 +1565,45 @@ let lower_left (ppe : PPEnv.t) (t_ty : form -> EcTypes.ty) (f : form) (opprec : | _ -> None in l_l f opprec +(* -------------------------------------------------------------------- *) +(* Count operator applications in a formula. Used as a "specificity" + metric for [match_pp_notations]: a notation body with more [Fop] + nodes has more structural constraints and therefore matches fewer + forms, so it is a more precise fit when several notations cover + the same form. *) +let rec count_ops (f : form) : int = + match f.f_node with + | Fop _ -> 1 + | Fapp (h, a) -> + List.fold_left (fun acc g -> acc + count_ops g) (count_ops h) a + | Fquant (_, _, b) -> count_ops b + | Ftuple fs -> List.fold_left (fun acc g -> acc + count_ops g) 0 fs + | Fif (c, t, e) -> count_ops c + count_ops t + count_ops e + | Flet (_, a, b) -> count_ops a + count_ops b + | Fproj (a, _) -> count_ops a + | Fmatch (f, bs, _) -> + List.fold_left (fun acc g -> acc + count_ops g) (count_ops f) bs + | _ -> 0 + +(* -------------------------------------------------------------------- *) +(* Sort key picking the most specific notation match among successes. + Primary: [-body_ops] so more structural constraints win (e.g. + `#big` body `big predT F r` beats `#bigP` body `big P F r` when + `P = predT`). Secondary: fewer [ont_args] (more baked-in structure, + fewer metavars). *) +let notation_specificity + (((_, (_, nt)), _, _, _, _) : + (EcPath.path * (EcDecl.ty_params * EcDecl.notation)) + * EcUnify.unienv + * EcMatching.mevmap + * EcTypes.ty EcIdent.Mid.t + * form list) + : int * int += + let body_ops = count_ops (EcCoreFol.form_of_expr nt.ont_body) in + let nargs = List.length nt.ont_args in + (- body_ops, nargs) + (* -------------------------------------------------------------------- *) let rec pp_lvalue (ppe : PPEnv.t) fmt lv = match lv with @@ -1791,6 +1830,62 @@ and try_pp_lossless in maybe_paren outer prio pp fmt (); true +and resolve_binder_slots_from_forms + (nt : EcDecl.notation) + (ev : EcMatching.mevmap) + : EcMatching.mevmap += + let find_pos (name : EcSymbols.symbol) (xs : EcSymbols.symbol list) = + let rec aux i = function + | [] -> None + | x :: _ when EcSymbols.sym_equal x name -> Some i + | _ :: rest -> aux (i + 1) rest + in aux 0 xs in + + let try_recover_from_form template slot_meta iname ity ev = + let try_one item = + match item with + | EcDecl.NTI_Slot (fname, EcDecl.NTS_Form deps) -> + (match find_pos iname deps with + | None -> None + | Some pos -> + let (fid, _) = EcSymbols.Msym.find fname slot_meta in + (match EcMatching.MEV.get fid `Form ev with + | Some (`Set (`Form fv)) -> + (try + let bd, _body = + EcCoreFol.destr_lambda ~bound:(pos + 1) fv in + (match List.nth_opt bd pos with + | Some (b_id, _gty) -> Some (EcCoreFol.f_local b_id ity) + | None -> None) + with EcCoreFol.DestrError _ -> None) + | _ -> None)) + | _ -> None + in + List.opick try_one template + in + + match nt.ont_template with + | None -> ev + | Some template -> + let items = template.EcDecl.nt_items in + let slot_meta = + List.fold_left (fun m (id, ty) -> + EcSymbols.Msym.add (EcIdent.name id) (id, ty) m) + EcSymbols.Msym.empty nt.ont_args in + List.fold_left (fun ev item -> + match item with + | EcDecl.NTI_Slot (iname, EcDecl.NTS_Ident) -> + let (iid, ity) = EcSymbols.Msym.find iname slot_meta in + if EcMatching.MEV.isset iid `Form ev then ev + else begin + match try_recover_from_form items slot_meta iname ity ev with + | Some v -> EcMatching.MEV.set iid (`Form v) ev + | None -> ev + end + | _ -> ev + ) ev items + and match_pp_notations ?(filter : (_ -> bool) = predT) (ppe : PPEnv.t) @@ -1825,6 +1920,8 @@ and match_pp_notations EcMatching.f_match_core fmnotation hy (ue, ev) bd f in + let ev = resolve_binder_slots_from_forms nt ev in + if not (EcMatching.can_concretize ev ue) then raise EcMatching.MatchFailure; @@ -1845,8 +1942,110 @@ and match_pp_notations in let nts = EcEnv.Op.get_notations ~head ppe.PPEnv.ppe_env in - - List.find_map_opt try_notation nts + let successes = List.filter_map try_notation nts in + let sorted = + List.stable_sort (fun a b -> + compare (notation_specificity a) (notation_specificity b)) + successes in + List.ohead sorted + +and pp_nt_punct (fmt : Format.formatter) (p : EcDecl.nt_punct) : unit = + Format.pp_print_string fmt p.EcDecl.np_display + +and pp_nt_template_slot + (ppe : PPEnv.t) + (fmt : Format.formatter) + (slot_args : form EcSymbols.Msym.t) + (arg : form) + (kind : EcDecl.nt_slot_kind) + : unit += + match kind with + | EcDecl.NTS_Ident -> + (match arg.f_node with + | Flocal id -> + Format.fprintf fmt "%a" (pp_local ppe) id + | _ -> + (* Non-local arg in an ident slot — shouldn't happen for well-formed + notation applications; fall back to generic form printing. *) + pp_form ppe fmt arg) + + | EcDecl.NTS_Form [] -> + pp_form ppe fmt arg + + | EcDecl.NTS_Form deps -> + let dep_count = List.length deps in + let bd, body = + EcCoreFol.decompose_lambda ~bound:dep_count arg in + if List.length bd = dep_count then + (* The matched arg is a lambda of the right arity; peel those + binders and print the body in their scope. *) + let ids = List.map fst bd in + let ppe = PPEnv.add_locals ppe ids in + pp_form ppe fmt body + else + (* The matched arg is not (fully) a lambda — eta-expand by + applying it to the user-chosen binder idents. *) + let dep_refs = + List.map (fun dep -> EcSymbols.Msym.find dep slot_args) deps in + let rec strip n t = + if n = 0 then t + else match t.EcAst.ty_node with + | EcAst.Tfun (_, t') -> strip (n - 1) t' + | _ -> t in + let applied = + EcCoreFol.f_app arg dep_refs (strip dep_count arg.f_ty) in + pp_form ppe fmt applied + +and try_pp_template + (ppe : PPEnv.t) + (fmt : Format.formatter) + (name : string) + (nt : EcDecl.notation) + (ov : ty Mid.t) + (args : form list) + : bool += + match nt.ont_template with + | None -> false + | Some template -> + (* Map slot name -> (arg, decl-time ident) via ont_args order. *) + let slot_info = + List.fold_left2 (fun m (id, _) a -> + EcSymbols.Msym.add (EcIdent.name id) (id, a) m) + EcSymbols.Msym.empty nt.ont_args args in + let slot_args = EcSymbols.Msym.map snd slot_info in + (* Is an optional group all-default? Walk its slots and compare each + matched form against its stored default (after substituting the + opened type variables of this call site). *) + let rec all_defaulted items = + List.for_all (function + | EcDecl.NTI_Punct _ -> true + | EcDecl.NTI_Optional subs -> all_defaulted subs + + | EcDecl.NTI_Slot (sname, _) -> + match EcSymbols.Msym.find_opt sname slot_info with + | None -> false + | Some (slot_id, arg) -> + (match EcIdent.Mid.find_opt slot_id template.EcDecl.nt_defaults with + | None -> false + | Some dflt -> + let dflt_f = + Fsubst.f_subst_tvar ~freshen:true ov + (EcCoreFol.form_of_expr dflt) in + EcCoreFol.f_equal arg dflt_f)) items in + Format.fprintf fmt "%s " name; + let rec render items = + List.iter (function + | EcDecl.NTI_Punct p -> pp_nt_punct fmt p + | EcDecl.NTI_Slot (sname, kind) -> + let arg = EcSymbols.Msym.find sname slot_args in + pp_nt_template_slot ppe fmt slot_args arg kind + | EcDecl.NTI_Optional subs -> + if not (all_defaulted subs) then render subs + ) items + in render template.EcDecl.nt_items; + true and try_pp_notations (ppe : PPEnv.t) @@ -1866,8 +2065,15 @@ and try_pp_notations let args = let subst = EcMatching.MEV.assubst ue ev ppe.ppe_env in List.map (Fsubst.f_subst subst) args in - let f = f_app (f_op p tv rty) (args @ eargs) f.f_ty in - pp_form_core_r ppe outer fmt f; true + (* If the matched notation has a template and there are no extra args, + print with the template layout. *) + if eargs = [] && Option.is_some nt.ont_template then begin + let name = EcPath.basename p in + let _ = try_pp_template ppe fmt name nt ov args in true + end else begin + let f = f_app (f_op p tv rty) (args @ eargs) f.f_ty in + pp_form_core_r ppe outer fmt f; true + end and pp_poe (ppe : PPEnv.t) (fmt : Format.formatter) (poe : form Mop.t) = let pp_branch fmt (e, f) = diff --git a/src/ecReduction.mli b/src/ecReduction.mli index ceb057d245..e3b9f5b872 100644 --- a/src/ecReduction.mli +++ b/src/ecReduction.mli @@ -59,6 +59,9 @@ end (* -------------------------------------------------------------------- *) val can_eta : ident -> form * form list -> bool +(* -------------------------------------------------------------------- *) +val eta_norm : form -> form + (* -------------------------------------------------------------------- *) type reduction_info = { beta : bool; diff --git a/src/ecScope.ml b/src/ecScope.ml index d0125b46fc..b183895fbd 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1711,7 +1711,8 @@ module Notations = struct module TT = EcTyping let add (scope : scope) (nt : pnotation located) = - EcHiNotations.trans_notation (env scope) nt; scope + let op = EcHiNotations.trans_notation (env scope) nt in + Op.bind scope op let add_abbrev (scope : scope) (ab : pabbrev located) = let op = EcHiNotations.trans_abbrev (env scope) ab in diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 107aba6e06..96d8857d87 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -889,10 +889,22 @@ let rec subst_op_kind (s : subst) (kind : operator_kind) = and subst_notation (s : subst) (nott : notation) = let s, xs = fresh_elocals s nott.ont_args in - { ont_args = xs; - ont_resty = subst_ty s nott.ont_resty; - ont_body = subst_expr s nott.ont_body; - ont_ponly = nott.ont_ponly; } + (* Rekey each template's defaults via the old→new ident mapping + established by fresh_elocals, and substitute expressions. *) + let template = + Option.map (fun (t : nt_template) -> + let nt_defaults = + List.fold_left2 (fun acc (old_id, _) (new_id, _) -> + match EcIdent.Mid.find_opt old_id t.nt_defaults with + | Some e -> EcIdent.Mid.add new_id (subst_expr s e) acc + | None -> acc) + EcIdent.Mid.empty nott.ont_args xs in + { nt_items = t.nt_items; nt_defaults; }) nott.ont_template in + { ont_args = xs; + ont_resty = subst_ty s nott.ont_resty; + ont_body = subst_expr s nott.ont_body; + ont_ponly = nott.ont_ponly; + ont_template = template; } and subst_op_body (s : subst) (bd : opbody) = match bd with diff --git a/src/ecTerminal.ml b/src/ecTerminal.ml index c5f85bc814..21b7c3351e 100644 --- a/src/ecTerminal.ml +++ b/src/ecTerminal.ml @@ -70,7 +70,9 @@ object(self) end; Format.printf "[%d|%s]>\n%!" (EcCommands.uuid ()) (EcCommands.mode ()); - EcIo.xparse iparser + let notations = + EcEnv.Op.lookup_template (EcScope.env (EcCommands.current ())) in + EcIo.xparse ~notations iparser method notice ~(immediate:bool) (lvl : loglevel) (msg : string) = match immediate with @@ -116,7 +118,9 @@ object method next = Format.printf "[%d|%s]>\n%!" (EcCommands.uuid ()) (EcCommands.mode ()); EcIo.drain iparser; - EcIo.xparse iparser + let notations = + EcEnv.Op.lookup_template (EcScope.env (EcCommands.current ())) in + EcIo.xparse ~notations iparser method notice ~(immediate:bool) (_ : loglevel) (msg : string) = ignore immediate; @@ -272,7 +276,9 @@ class from_channel method interactive = false method next = - let aout = EcIo.xparse iparser in + let notations = + EcEnv.Op.lookup_template (EcScope.env (EcCommands.current ())) in + let aout = EcIo.xparse ~notations iparser in loc <- (snd aout).LC.pl_loc; self#_update_progress; aout diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 3a4c27a778..5d0c3144a1 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -1751,7 +1751,8 @@ let top_is_mem_binding pf = match pf with | PFeqveq _ | PFeqf _ | PFlsless _ - | PFscope _ -> false + | PFscope _ + | PFntt _ -> false let f_or_mod_ident_loc : f_or_mod_ident -> EcLocation.t = function @@ -1865,6 +1866,73 @@ let trans_restr_oracle_calls env env_in (params : Sm.t) = function * 'forall (A <: T) (B <: S {some restriction)), ...' * Here, the parameter of the functor [S] are not binded in [env], but must be * binded in [env_in]. *) + +(* -------------------------------------------------------------------- *) +(* Eta-reduce the body of a notation form-slot argument over its + declared binders. Called after typechecking a slot body that was + written in the user's source as `f b_1 ... b_n` (or similar). + + If the body ends with exactly [dep_binders] applied in order to a + head [f], and collapsing is safe, return [f] applied to the "kept" + prefix (or just [f] if the body was pure eta-expansion). Otherwise + wrap the body in a lambda over [dep_binders]. + + Reduction fires when: + - the trailing args of the body are exactly [dep_binders], as + [Flocal]s with the expected types (order matters); + - the head and the kept prefix don't capture any binder in + [dep_binders] (standard eta-safety check); + - AND either (a) there are already "kept" args, so the user wrote + something like `(P \o h) i` — the outer application makes it + clear a non-trivial function is being composed — or (b) the + head is a local variable (the common `F i` case). + + Case (b) catches the common idiom but deliberately leaves + `fun i => i%r` (op applied only to the binder) wrapped, because + downstream stdlib proofs match on the lambda form. See + [doc/notation.rst] and the matching heuristic in [ecMatching.ml] + (which complements this via `try_etared`) for the full story. *) +let eta_reduce_slot_arg + ~(dep_binders : (EcIdent.t * ty) list) + ~(slot_ty : ty) + (arg_f : EcFol.form) + : EcFol.form += + let wrap_lambda () = + EcCoreFol.f_lambda + (List.map (fun (x, t) -> (x, EcAst.GTty t)) dep_binders) + arg_f in + let n = List.length dep_binders in + match arg_f.EcAst.f_node with + | EcAst.Fapp (f, args) when List.length args >= n -> + let k = List.length args - n in + let kept, tail = List.split_at k args in + let binders_ok = + List.for_all2 (fun (bid, bty) a -> + match a.EcAst.f_node with + | EcAst.Flocal aid -> + EcIdent.id_equal aid bid + && EcTypes.ty_equal a.EcAst.f_ty bty + | _ -> false) dep_binders tail in + let no_capture () = + let fvs = List.fold_left (fun acc e -> + EcIdent.fv_union acc e.EcAst.f_fv) + f.EcAst.f_fv kept in + List.for_all (fun (bid, _) -> + not (EcIdent.Mid.mem bid fvs)) dep_binders in + let head_ok = + (not (List.is_empty kept)) + || (match f.EcAst.f_node with + | EcAst.Flocal _ -> true + | _ -> false) in + if binders_ok && no_capture () && head_ok then + EcCoreFol.f_app f kept slot_ty + else + wrap_lambda () + + | _ -> wrap_lambda () + +(* -------------------------------------------------------------------- *) let rec trans_restr_fun env env_in (params : Sm.t) (r_el : pmod_restr_el) = let name = unloc r_el.pmre_name in let r_orcls = trans_restr_oracle_calls env env_in params r_el.pmre_orcls in @@ -2931,6 +2999,177 @@ and trans_gbinding env ue decl = and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let state = PFS.create () in + (* Expand a [PFntt] call site. Looks up the notation operator, opens + its type parameters, then walks [pnt_args] (in dispatcher-emitted + order) binding each slot to its typechecked formula argument or + stored default. The body is substituted in at the end. Slot args + are typechecked via [trans_form_or_pattern] so that [Pr[...]], + memory refs, and other formula-level constructs are accepted. *) + let expand_notation + (env : EcEnv.env) + (pf : pformula) + (pnt_name : pqsymbol) + (pnt_args : (EcSymbols.symbol * pformula option) list) + : EcFol.form + = + let qname = EcLocation.unloc pnt_name in + let op = + match EcEnv.Op.lookup_opt qname env with + | None -> + tyerror pnt_name.pl_loc env + (UnknownVarOrOp (qname, [])) + | Some (_, op) -> op in + let ont = + match op.op_kind with + | OB_nott ({ ont_template = Some _; _ } as n) -> n + | _ -> + tyerror pnt_name.pl_loc env + (UnknownVarOrOp (qname, [])) in + let template = Option.get ont.ont_template in + + (* Collect slot kinds from the template, walking through optional + groups. *) + let rec collect_kinds acc = function + | [] -> acc + | EcDecl.NTI_Slot (n, k) :: tl -> + collect_kinds (EcSymbols.Msym.add n k acc) tl + | EcDecl.NTI_Punct _ :: tl -> collect_kinds acc tl + | EcDecl.NTI_Optional sub :: tl -> + collect_kinds (collect_kinds acc sub) tl in + let slot_kinds = collect_kinds EcSymbols.Msym.empty template.EcDecl.nt_items in + + (* Open the operator's type parameters. *) + let ov = EcUnify.UniEnv.opentvi ue op.op_tparams None in + let tsub_ty = Tvar.subst ov in + let slot_meta = + List.fold_left (fun m (id, ty) -> + EcSymbols.Msym.add (EcIdent.name id) (id, tsub_ty ty) m) + EcSymbols.Msym.empty ont.ont_args in + + (* Formula-level substitution carrying the type-variable + instantiation. Notations share the [OB_nott] body representation + with abbreviations but expand at formula level just like + abbreviation calls. *) + let tsub_f = EcCoreSubst.f_subst_init ~tv:ov () in + + (* Classify each dispatcher-emitted arg by its slot kind, then + partition idents from forms so each binding pass walks only its + own slots. Binding idents first lets form slots reference any + binder regardless of template order. *) + let module M = struct + type slot_info = { + kind : EcDecl.nt_slot_kind; + name : EcSymbols.symbol; + id : EcIdent.t; + ty : ty; + arg_opt : pformula option; + } + end in + let classified : M.slot_info list = + List.map (fun (slot_name, arg_opt) -> + let kind = + try EcSymbols.Msym.find slot_name slot_kinds + with Not_found -> + tyerror pf.pl_loc env (UnknownVarOrOp (([], slot_name), [])) in + let (slot_id, slot_ty) = + try EcSymbols.Msym.find slot_name slot_meta + with Not_found -> assert false in + M.{ kind; name = slot_name; id = slot_id; ty = slot_ty; arg_opt; }) + pnt_args in + let idents, forms = + List.partition (fun (c : M.slot_info) -> c.kind = EcDecl.NTS_Ident) + classified in + + (* Pass 1: assign a fresh ident to each user-chosen binder name. + The fold wires two outputs: a substitution [s] that renames the + slot-ident to the fresh one, and a map [ub] used by pass 2 to + put the same binders in scope when typechecking form slots. *) + let assign_ident (si : M.slot_info) : EcIdent.t = + match si.arg_opt with + | Some arg -> + let new_name = + match EcLocation.unloc arg with + | PFident ({ pl_desc = ([], n); _ }, None) -> n + | _ -> + tyerror arg.pl_loc env + (UnknownVarOrOp (([], si.name), [])) in + EcIdent.create new_name + + | None -> + (* Ident slots can't be absent: they have no default and there's + no sensible identifier to synthesise. The declaration-time + validation disallows ident slots inside optional groups, so + this is an invariant violation. *) + tyerror pf.pl_loc env (UnknownVarOrOp (([], si.name), [])) + in + let (s, ub) = + List.fold_left (fun (s, ub) (si : M.slot_info) -> + let new_id = assign_ident si in + ( EcCoreSubst.Fsubst.f_bind_local s si.id + (EcCoreFol.f_local new_id si.ty) + , EcSymbols.Msym.add si.name (new_id, si.ty) ub)) + (tsub_f, EcSymbols.Msym.empty) idents in + + (* Pass 2: build the bound formula for each form slot — from the + user-supplied argument, or from the stored default — and extend + the substitution. [ub] is fixed from pass 1. *) + let build_form (si : M.slot_info) : EcFol.form = + let deps = + match si.kind with + | EcDecl.NTS_Form d -> d + | EcDecl.NTS_Ident -> assert false in + match si.arg_opt with + | Some arg -> + let rec strip n t = + if n = 0 then t + else match t.EcAst.ty_node with + | EcAst.Tfun (_, t') -> strip (n - 1) t' + | _ -> assert false in + let plain_ty = strip (List.length deps) si.ty in + let dep_binders = + List.map (fun bname -> + try EcSymbols.Msym.find bname ub + with Not_found -> assert false) deps in + let local_env = EcEnv.Var.bind_locals dep_binders env in + (* Special-case `_` as the entire slot body: create a single + meta-var of the slot's FULL curried type (not the stripped + body type). Makes `pose c := #big [ i : _ | _ ] _` behave + like `pose c := big _ _ _`: each `_` matches the whole + function, not just its scalar body. *) + let is_bare_hole = + match EcLocation.unloc arg with + | PFhole -> Option.is_some ps + | _ -> false in + if is_bare_hole then + let ps = Option.get ps in + let x = EcIdent.create (Printf.sprintf "?%d" (EcUid.unique ())) in + ps := EcIdent.Mid.add x si.ty !ps; + EcCoreFol.f_local x si.ty + else + (* Type the slot arg with the same pattern map the outer + caller uses, so `_` in a slot works when the notation + instance appears inside a rewrite/pose pattern. *) + let arg_f = + trans_form_or_pattern local_env `Form + ?mv ?ps ue arg (Some plain_ty) in + eta_reduce_slot_arg ~dep_binders ~slot_ty:si.ty arg_f + + | None -> + (* Absent form slot → bind the typechecked default, with type + vars substituted from the current [ov]. *) + let dflt = + try EcIdent.Mid.find si.id template.EcDecl.nt_defaults + with Not_found -> assert false in + EcCoreSubst.Fsubst.f_subst tsub_f (EcCoreFol.form_of_expr dflt) + in + let subst = + List.fold_left (fun s (si : M.slot_info) -> + EcCoreSubst.Fsubst.f_bind_local s si.id (build_form si)) + s forms in + + let body_f = EcCoreFol.form_of_expr ont.ont_body in + EcCoreSubst.Fsubst.f_subst subst body_f in + let rec transf_r_tyinfo opsc env ?tt f = let transf env ?tt f = transf_r opsc env ?tt f in @@ -3604,6 +3843,9 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty; f_eagerF {ml;mr;inv=pre'} s1 fpath1 fpath2 s2 {ml;mr;inv=post'} + | PFntt { pnt_name; pnt_args } -> + expand_notation env f pnt_name pnt_args + and transf_r opsc env ?tt pf = let f = transf_r_tyinfo opsc env ?tt pf in let () = oiter (fun tt -> unify_or_fail env ue pf.pl_loc ~expct:tt f.f_ty) tt in diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml index 65a874e64c..70bfcfc033 100644 --- a/src/ecUserMessages.ml +++ b/src/ecUserMessages.ml @@ -738,6 +738,22 @@ end = struct msg "unknown binder: `%s'" x | NTE_AbbrevIsVar -> msg "abbrev. body cannot reduce to a variable" + | NTE_UnknownSlot x -> + msg "template references unknown slot: `%s'" x + | NTE_DuplicateSlot x -> + msg "template references slot `%s' more than once" x + | NTE_TemplateEmpty -> + msg "notation template is empty" + | NTE_BadPunct s -> + msg "notation punctuation `%S' must lex to one of: [ ] : | , ;" s + | NTE_OptionalEmpty -> + msg "optional template group `( ... )?' is empty" + | NTE_OptionalMustStartWithPunct -> + msg "optional template group `( ... )?' must start with a punctuation literal" + | NTE_DefaultOnNonOptional s -> + msg "slot `%s' has a default but is referenced outside an optional group" s + | NTE_MissingDefault s -> + msg "slot `%s' appears only inside optional groups and must declare a default via `= ...'" s end (* -------------------------------------------------------------------- *) diff --git a/src/ecUtils.ml b/src/ecUtils.ml index 0cd31828dd..686b94e549 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -1,5 +1,7 @@ (* -------------------------------------------------------------------- *) module Enum = BatEnum +module GSet = BatSet +module GMap = BatMap (* -------------------------------------------------------------------- *) exception Unexpected diff --git a/src/ecUtils.mli b/src/ecUtils.mli index 3141d814b6..f268302975 100644 --- a/src/ecUtils.mli +++ b/src/ecUtils.mli @@ -1,5 +1,7 @@ (* -------------------------------------------------------------------- *) module Enum = BatEnum +module GSet = BatSet +module GMap = BatMap (* -------------------------------------------------------------------- *) exception Unexpected diff --git a/tests/notations-ko/dup_slot.ec b/tests/notations-ko/dup_slot.ec new file mode 100644 index 0000000000..5357dcaabf --- /dev/null +++ b/tests/notations-ko/dup_slot.ec @@ -0,0 +1,4 @@ +require import AllCore. + +(* Rejected: the template references slot `a' twice. *) +notation #bad (a : int) "[" a ", " a "] " = a. diff --git a/tests/notations/WithNotation.ec b/tests/notations/WithNotation.ec new file mode 100644 index 0000000000..c9b3f79150 --- /dev/null +++ b/tests/notations/WithNotation.ec @@ -0,0 +1,6 @@ +require import AllCore. + +notation #pair (a : int) (b : int) "[" a ", " b "] " = (a, b). + +lemma same_file : #pair [1, 2] = (1, 2). +proof. by trivial. qed. diff --git a/tests/notations/abstract.ec b/tests/notations/abstract.ec new file mode 100644 index 0000000000..17ae9c5926 --- /dev/null +++ b/tests/notations/abstract.ec @@ -0,0 +1,17 @@ +require import AllCore. + +(* Abstract theory parameterized by `t`, declaring a notation that uses it. *) +abstract theory AbsT. + type t. + + notation #pairT (a : t) (b : t) "[" a ", " b "] " = (a, b). +end AbsT. + +(* Clone with t := int. *) +clone AbsT as IntT with + type t <- int. + +import IntT. + +lemma check : #pairT [1, 2] = (1, 2). +proof. by trivial. qed. diff --git a/tests/notations/binders.ec b/tests/notations/binders.ec new file mode 100644 index 0000000000..f20c5408eb --- /dev/null +++ b/tests/notations/binders.ec @@ -0,0 +1,35 @@ +require import AllCore List. + +(* Binder slot `i` declared via `#<...>`; form slot `f` has `i` as a *) +(* binder dep, so inside the body `f` appears as a function; at the *) +(* call site `f` is written as an open form over the user-chosen name. *) +notation #mapI #< i : int > (n : int) (f : i ==> int) + "[" i " : " n " : " f "] " = + map f (iota_ 0 n). + +(* Expansion equals the fully-expanded form with the user-chosen binder. *) +lemma t1 : #mapI [i : 3 : i * 10] = map (fun i => i * 10) (iota_ 0 3). +proof. by trivial. qed. + +lemma t2 : #mapI [k : 4 : k + 1] = map (fun k => k + 1) (iota_ 0 4). +proof. by trivial. qed. + +(* Two binder slots with two form-slot deps. *) +notation #matI #< i : int, j : int > (n : int) (m : int) (f : i, j ==> int) + "[" i ", " j " : " n " : " m " : " f "] " = + map (fun i => map (fun j => f i j) (iota_ 0 m)) (iota_ 0 n). + +lemma t3 : + #matI [a, b : 2 : 2 : a * 10 + b] + = map (fun a => map (fun b => a * 10 + b) (iota_ 0 2)) (iota_ 0 2). +proof. by trivial. qed. + +(* Comprehension-style: the form slot `f` appears BEFORE the binder `x` in the + template; binding is two-pass so dep idents are available regardless of + template order. *) +notation #mapC #< x : int > (f : x ==> int) (s : int list) + "[" f " | " x " : " s "] " = + map f s. + +lemma t4 : #mapC [x + 1 | x : [1; 2; 3]] = [2; 3; 4]. +proof. by trivial. qed. diff --git a/tests/notations/clone.ec b/tests/notations/clone.ec new file mode 100644 index 0000000000..bcf2083ba9 --- /dev/null +++ b/tests/notations/clone.ec @@ -0,0 +1,16 @@ +require import AllCore. + +(* Theory with a notation. *) +theory Src. + notation #twice (a : int) "[" a "] " = a + a. + + lemma inside : #twice [3] = 6. + proof. by trivial. qed. +end Src. + +(* Clone brings the notation into the new namespace. *) +clone Src as Dst. +import Dst. + +lemma cross_clone : #twice [7] = 14. +proof. by trivial. qed. diff --git a/tests/notations/clone_op.ec b/tests/notations/clone_op.ec new file mode 100644 index 0000000000..e72123f62a --- /dev/null +++ b/tests/notations/clone_op.ec @@ -0,0 +1,26 @@ +require import AllCore. + +(* Abstract theory where the notation body references an abstract op. *) +abstract theory Src. + type t. + op combine : t -> t -> t. + + notation #c (a : t) (b : t) "[" a ", " b "] " = combine a b. + + lemma combine_self (x : t) : #c [x, x] = combine x x. + proof. by trivial. qed. +end Src. + +(* Clone with concrete op substitution: combine <- Int.(+). *) +clone Src as SumT with + type t <- int, + op combine <- Int.(+). + +import SumT. + +(* After substitution, #c should expand to `+`. *) +lemma sum_c (a b : int) : #c [a, b] = a + b. +proof. by trivial. qed. + +lemma sum_commute (x y : int) : #c [x, y] = x + y. +proof. by trivial. qed. diff --git a/tests/notations/closures.ec b/tests/notations/closures.ec new file mode 100644 index 0000000000..34a5cc47d5 --- /dev/null +++ b/tests/notations/closures.ec @@ -0,0 +1,14 @@ +require import AllCore List. + +(* A notation whose form slots are function-typed — user supplies lambdas. *) +notation #map (f : int -> int) (xs : int list) "[" f " : " xs "] " = + map f xs. + +lemma t1 : #map [(fun x => x + 1) : [1; 2; 3]] = [2; 3; 4]. +proof. by trivial. qed. + +(* Nested notation use — the inner #map expands first. *) +lemma t2 (xs : int list) : + #map [(fun x => x * 2) : #map [(fun x => x + 1) : xs]] + = map (fun x => x * 2) (map (fun x => x + 1) xs). +proof. by trivial. qed. diff --git a/tests/notations/deep.ec b/tests/notations/deep.ec new file mode 100644 index 0000000000..56b7e49592 --- /dev/null +++ b/tests/notations/deep.ec @@ -0,0 +1,46 @@ +require import AllCore List. + +notation #pair ['a 'b] (a : 'a) (b : 'b) "[" a ", " b "] " = (a, b). + +(* Three levels deep, mixing template punct and form-slot content. *) +lemma deep3 (x y z w : int) : + #pair [#pair [x, y], #pair [z, w]] = ((x, y), (z, w)). +proof. by trivial. qed. + +lemma deep4 (x y z w v : int) : + #pair [#pair [x, #pair [y, z]], #pair [w, v]] = ((x, (y, z)), (w, v)). +proof. by trivial. qed. + +(* Multi-binder notation where a single form slot depends on both binders. *) +notation #ij #< i : int, j : int > (f : i, j ==> int) + "[" i ", " j " : " f "] " = + f 10 20. + +lemma ij_call : #ij [a, b : a * b + 1] = 201. +proof. by trivial. qed. + +lemma ij_call_eq : #ij [i, j : i + j] = (fun (i j : int) => i + j) 10 20. +proof. by trivial. qed. + +(* Three binders, three different form slots depending on subsets of them. *) +notation #rank #< i : int, j : int, k : int > + (fij : i, j ==> int) + (fjk : j, k ==> int) + (fik : i, k ==> int) + "[" i ", " j ", " k " : " fij " | " fjk " | " fik "] " = + fij 1 2 + fjk 2 3 + fik 1 3. + +lemma rank_check : + #rank [a, b, c : a + b | b * c | a - c] = (1 + 2) + (2 * 3) + (1 - 3). +proof. by trivial. qed. + +(* Deep nesting + binder slot. The inner #pair provides the value for the *) +(* form slot; the tuple result matches a polymorphic `'a = int * int`. *) +notation #mapI ['a] #< i : int > (n : int) (f : i ==> 'a) + "[" i " : " n " : " f "] " = + map f (iota_ 0 n). + +lemma nested_binder (n : int) : + #mapI [i : n : #pair [i, i + 1]] + = map (fun i => (i, i + 1)) (iota_ 0 n). +proof. by trivial. qed. diff --git a/tests/notations/forms.ec b/tests/notations/forms.ec new file mode 100644 index 0000000000..22d6b92a48 --- /dev/null +++ b/tests/notations/forms.ec @@ -0,0 +1,18 @@ +require import AllCore. + +(* Form-slot notation: #cond [c : t | f] expands to if c then t else f. *) +notation #cond (c : bool) (t : int) (f : int) "[" c " : " t " | " f "] " = + if c then t else f. + +lemma t1 : #cond [true : 1 | 2] = 1. +proof. by trivial. qed. + +lemma t2 (x y : int) : #cond [x < y : x | y] = if x < y then x else y. +proof. by trivial. qed. + +(* Multiple notations in one file; later notation uses earlier-bound ops. *) +notation #max (a : int) (b : int) "[" a ", " b "] " = + if a < b then b else a. + +lemma t3 (x y : int) : #max [x, y] = if x < y then y else x. +proof. by trivial. qed. diff --git a/tests/notations/locality.ec b/tests/notations/locality.ec new file mode 100644 index 0000000000..9ed1755f19 --- /dev/null +++ b/tests/notations/locality.ec @@ -0,0 +1,14 @@ +require import AllCore. + +(* Global notation: visible after import. *) +theory T1. + notation #pairT1 (a : int) (b : int) "[" a ", " b "] " = (a, b). + + lemma inside_T1 : #pairT1 [1, 2] = (1, 2). + proof. by trivial. qed. +end T1. + +import T1. + +lemma outside_T1_sees_global : #pairT1 [3, 4] = (3, 4). +proof. by trivial. qed. diff --git a/tests/notations/optional.ec b/tests/notations/optional.ec new file mode 100644 index 0000000000..d9e08c54a0 --- /dev/null +++ b/tests/notations/optional.ec @@ -0,0 +1,36 @@ +require import AllCore List. + +(* A notation with one optional group containing one form slot that has *) +(* a default. The call site may omit the ` | P` suffix. *) +notation #filter ['a] #< i : 'a > + (xs : 'a list) + (P : i ==> bool = predT) + "[" i " : " xs ("| " P)? "]" = + filter P xs. + +(* With the optional group: P is user-supplied. *) +lemma with_P (xs : int list) : + #filter [ i : xs | 0 <= i ] = filter (fun i => 0 <= i) xs. +proof. by trivial. qed. + +(* Without the optional group: P defaults to predT. *) +lemma without_P (xs : int list) : + #filter [ i : xs ] = filter predT xs. +proof. by trivial. qed. + +(* Two independent optional groups in one notation (different puncts). *) +notation #take2 (xs : int list) (lo : int = 0) (hi : int = 1000) + "[" xs ("| " lo)? ("; " hi)? "]" = + take (hi - lo) (drop lo xs). + +lemma no_opt (xs : int list) : + #take2 [ xs ] = take (1000 - 0) (drop 0 xs). +proof. by trivial. qed. + +lemma both_opt (xs : int list) : + #take2 [ xs | 5 ; 20 ] = take (20 - 5) (drop 5 xs). +proof. by trivial. qed. + +lemma only_second (xs : int list) : + #take2 [ xs ; 7 ] = take (7 - 0) (drop 0 xs). +proof. by trivial. qed. diff --git a/tests/notations/phl.ec b/tests/notations/phl.ec new file mode 100644 index 0000000000..5b4e5ad5f5 --- /dev/null +++ b/tests/notations/phl.ec @@ -0,0 +1,25 @@ +require import AllCore. + +notation #pair (a : int) (b : int) "[" a ", " b "] " = (a, b). + +module M = { + proc f (x : int, y : int) : int * int = { + return (x + 1, y + 1); + } +}. + +(* Notation inside a Hoare post — `res` is the procedure's return value. *) +lemma hoare_ok (a b : int) : + hoare [M.f : x = a /\ y = b ==> res = #pair [a + 1, b + 1]]. +proof. + proc. + by trivial. +qed. + +(* Probabilistic: same notation in a phoare post. *) +lemma phoare_ok (a b : int) : + phoare [M.f : x = a /\ y = b ==> res = #pair [a + 1, b + 1]] = 1%r. +proof. + proc. + by trivial. +qed. diff --git a/tests/notations/polymorphic.ec b/tests/notations/polymorphic.ec new file mode 100644 index 0000000000..be23cfeb42 --- /dev/null +++ b/tests/notations/polymorphic.ec @@ -0,0 +1,29 @@ +require import AllCore List. + +(* Polymorphic pair with two independent type parameters. *) +notation #ppair ['a 'b] (a : 'a) (b : 'b) "[" a ", " b "] " = (a, b). + +lemma t1 : #ppair [1, true] = (1, true). +proof. by trivial. qed. + +lemma t2 (x : int) (y : bool) : #ppair [x, y] = (x, y). +proof. by trivial. qed. + +(* Polymorphic list-mapper — 'a and 'b are independent. *) +notation #pmap ['a 'b] (f : 'a -> 'b) (xs : 'a list) "[" f " : " xs "] " = + map f xs. + +lemma t3 : #pmap [(fun x => x + 1) : [1; 2; 3]] = [2; 3; 4]. +proof. by trivial. qed. + +lemma t4 : #pmap [(fun (x : int) => (x, x)) : [1; 2]] = [(1, 1); (2, 2)]. +proof. by trivial. qed. + +(* Polymorphic with binder slot. *) +notation #piota ['a] #< i : int > (n : int) (f : i ==> 'a) + "[" i " : " n " : " f "] " = + map f (iota_ 0 n). + +lemma t5 (n : int) : + #piota [i : n : i + 10] = map (fun i => i + 10) (iota_ 0 n). +proof. by trivial. qed. diff --git a/tests/notations/projection.ec b/tests/notations/projection.ec new file mode 100644 index 0000000000..2f852ef206 --- /dev/null +++ b/tests/notations/projection.ec @@ -0,0 +1,15 @@ +require import AllCore. + +notation #pair ['a 'b] (a : 'a) (b : 'b) "[" a ", " b "] " = (a, b). + +(* Tuple projection after a notation call. *) +lemma proj_1 (x y : int) : #pair [x, y].`1 = x. +proof. by trivial. qed. + +lemma proj_2 (x y : int) : #pair [x, y].`2 = y. +proof. by trivial. qed. + +(* Projection inside a larger expression. *) +lemma compose (x : int) : + #pair [x, x + 1].`1 + #pair [x, x + 1].`2 = 2 * x + 1. +proof. by smt(). qed. diff --git a/tests/notations/qualified.ec b/tests/notations/qualified.ec new file mode 100644 index 0000000000..21cf17e33b --- /dev/null +++ b/tests/notations/qualified.ec @@ -0,0 +1,27 @@ +require import AllCore. + +theory Src. + notation #pair (a : int) (b : int) "[" a ", " b "] " = (a, b). +end Src. + +clone Src as Dst. + +(* Qualified call without `import`. *) +lemma qualified_call (x y : int) : Dst.#pair [x, y] = (x, y). +proof. by trivial. qed. + +(* Deeper qualifier. *) +theory Outer. + theory Inner. + notation #twice (a : int) "[" a "] " = a + a. + end Inner. +end Outer. + +lemma deep_qualified (x : int) : Outer.Inner.#twice [x] = x + x. +proof. by trivial. qed. + +(* Bare call after explicit import still works. *) +import Src. + +lemma bare_after_import (x y : int) : #pair [x, y] = (x, y). +proof. by trivial. qed. diff --git a/tests/notations/require_site.ec b/tests/notations/require_site.ec new file mode 100644 index 0000000000..8a406f569d --- /dev/null +++ b/tests/notations/require_site.ec @@ -0,0 +1,5 @@ +require import AllCore. +require import WithNotation. + +lemma cross_file : #pair [3, 4] = (3, 4). +proof. by trivial. qed. diff --git a/tests/notations/roundtrip.ec b/tests/notations/roundtrip.ec new file mode 100644 index 0000000000..b0cb670013 --- /dev/null +++ b/tests/notations/roundtrip.ec @@ -0,0 +1,25 @@ +require import AllCore List. + +(* Form-slot only *) +notation #pair (a : int) (b : int) "[" a ", " b "] " = (a, b). + +(* Binder slot with form-slot dependent on it *) +notation #mapI #< i : int > (n : int) (f : i ==> int) + "[" i " : " n " : " f "] " = + map f (iota_ 0 n). + +lemma L (x y : int) : + #pair [x, y] = (x, y). +proof. by trivial. qed. + +(* The printer must render `(x, y)` back as `#pair [x, y]`. *) +expect "lemma L: forall (x y : int), #pair [x, y] = #pair [x, y] ." + by print axiom L. + +(* Binder slot round-trip through printer — the RHS is the body expansion *) +lemma M : #mapI [k : 4 : k + 1] = map (fun k => k + 1) (iota_ 0 4). +proof. by trivial. qed. + +(* The printer must recover the user-chosen binder name `k` on both sides. *) +expect "lemma M: #mapI [k : 4 : k + 1] = #mapI [k : 4 : k + 1] ." + by print axiom M. diff --git a/tests/notations/section.ec b/tests/notations/section.ec new file mode 100644 index 0000000000..0e83dc81eb --- /dev/null +++ b/tests/notations/section.ec @@ -0,0 +1,20 @@ +require import AllCore. + +(* Notations inside a section, including a local one. *) +section. + + notation #gpair (a : int) (b : int) "[" a ", " b "] " = (a, b). + + local notation #lpair (a : int) (b : int) "[" a ", " b "] " = (a, b). + + lemma t_g : #gpair [1, 2] = (1, 2). + proof. by trivial. qed. + + lemma t_l : #lpair [1, 2] = (1, 2). + proof. by trivial. qed. + +end section. + +(* After the section closes, the global notation survives. *) +lemma after : #gpair [3, 4] = (3, 4). +proof. by trivial. qed. diff --git a/tests/notations/simple.ec b/tests/notations/simple.ec new file mode 100644 index 0000000000..353e8a63fc --- /dev/null +++ b/tests/notations/simple.ec @@ -0,0 +1,7 @@ +require import AllCore. + +(* Minimal notation: #pair [a, b] expands to (a, b). *) +notation #pair (a : int) (b : int) "[" a ", " b "] " = (a, b). + +lemma test1 : #pair [3, 4] = (3, 4). +proof. by trivial. qed. diff --git a/tests/notations/unfold.ec b/tests/notations/unfold.ec new file mode 100644 index 0000000000..c9cd71b44c --- /dev/null +++ b/tests/notations/unfold.ec @@ -0,0 +1,20 @@ +require import AllCore List. + +(* Unfolding a notation via `rewrite` — since notations are real operators *) +(* of kind `OB_nott`, the usual delta-rewrite machinery should unfold them. *) + +notation #pair (a : int) (b : int) "[" a ", " b "] " = (a, b). + +lemma pair_fst (x y : int) : fst (#pair [x, y]) = x. +proof. by trivial. qed. + +(* Explicit delta unfold via `rewrite /#pair`. *) +lemma explicit_unfold (x y : int) : #pair [x, y] = (x, y). +proof. by rewrite /#pair. qed. + +(* Unfold under a binder. *) +notation #bump (a : int) "[" a "] " = a + 1. + +lemma unfold_under_binder : + map (fun x => #bump [x]) [1; 2; 3] = [2; 3; 4]. +proof. by trivial. qed. diff --git a/theories/algebra/Bigalg.ec b/theories/algebra/Bigalg.ec index a56bc14135..8cf586b450 100644 --- a/theories/algebra/Bigalg.ec +++ b/theories/algebra/Bigalg.ec @@ -23,38 +23,42 @@ realize Support.Axioms.addmC. by apply/addrC. qed. realize Support.Axioms.add0m. by apply/add0r. qed. (* -------------------------------------------------------------------- *) -lemma sumrD P F1 F2 (r : 'a list): - (big P F1 r) + (big P F2 r) = big P (fun x => F1 x + F2 x) r. +lemma sumrD P (F1 F2 : 'a -> t) (r : 'a list): + (#big [ x : r | P x ] (F1 x)) + (#big [ x : r | P x ] (F2 x)) + = #big [ x : r | P x ] (F1 x + F2 x). proof. by rewrite big_split. qed. (* -------------------------------------------------------------------- *) -lemma sumrN P F (r : 'a list): - - (big P F r) = (big P (fun x => -(F x)) r). +lemma sumrN P (F : 'a -> t) (r : 'a list): + - (#big [ x : r | P x ] (F x)) = (#big [ x : r | P x ] (-(F x))). proof. by apply/(big_endo oppr0 opprD). qed. (* -------------------------------------------------------------------- *) -lemma sumrB P F1 F2 (r : 'a list): - (big P F1 r) - (big P F2 r) = big P (fun x => F1 x - F2 x) r. +lemma sumrB P (F1 F2 : 'a -> t) (r : 'a list): + (#big [ x : r | P x ] (F1 x)) - (#big [ x : r | P x ] (F2 x)) + = #big [ x : r | P x ] (F1 x - F2 x). proof. by rewrite sumrN sumrD; apply/eq_bigr => /=. qed. (* -------------------------------------------------------------------- *) lemma sumr_const (P : 'a -> bool) x s: - big P (fun _ => x) s = intmul x (count P s). + #big [ i : s | P i ] x = intmul x (count P s). proof. by rewrite big_const intmulpE 1:count_ge0 // -ZM.AddMonoid.iteropE. qed. -lemma sumri_const k (n m:int) : n <= m => bigi predT (fun _ => k) n m = intmul k (m - n). +lemma sumri_const k (n m:int) : n <= m => + #bigi [ _ : n, m ] k = intmul k (m - n). proof. by move=> h; rewrite sumr_const count_predT size_range /#. qed. (* -------------------------------------------------------------------- *) -lemma sumr_undup ['a] (P : 'a -> bool) F s : - big P F s = big P (fun a => intmul (F a) (count (pred1 a) s)) (undup s). +lemma sumr_undup ['a] (P : 'a -> bool) (F : 'a -> t) s : + #big [ a : s | P a ] (F a) + = #big [ a : (undup s) | P a ] (intmul (F a) (count (pred1 a) s)). proof. rewrite big_undup; apply/eq_bigr=> x _ /=. by rewrite intmulpE ?count_ge0 ZM.AddMonoid.iteropE. qed. lemma telescoping_sum (F: int -> t) (m n:int) : m <= n => - F m - F n = bigi predT (fun i => F i - F (i+1)) m n. + F m - F n = #bigi [ i : m, n ] (F i - F (i+1)). proof. move=> /IntOrder.ler_eqVlt [<<- | hmn]. + by rewrite big_geq 1:// subrr. @@ -69,7 +73,7 @@ by rewrite /(\o) /= -(@range_addl m n 1) (@addrC _ (F n)) subr_add2r. qed. lemma telescoping_sum_down (F: int -> t) (m n:int) : m <= n => - F n - F m = bigi predT (fun i => F (i+1) - F i) m n. + F n - F m = #bigi [ i : m, n ] (F (i+1) - F i). proof. move=> hmn; have /= := telescoping_sum (fun i => -F i) _ _ hmn. by rewrite opprK addrC => ->; apply eq_big => //= i _; rewrite opprK addrC. @@ -98,39 +102,37 @@ realize ZM.addrC. by apply/addrC. qed. realize ZM.add0r. by apply/add0r. qed. realize ZM.addNr. by apply/addNr. qed. -lemma sumr_1 (P : 'a -> bool) s: - big P (fun i => oner) s = CR.ofint (count P s). +lemma sumr_1 ['a] (P : 'a -> bool) s: + #big [ i : s | P i ] oner = CR.ofint (count P s). proof. by apply/sumr_const. qed. -lemma mulr_suml (P : 'a -> bool) F s x : - (big P F s) * x = big P (fun i => F i * x) s. +lemma mulr_suml (P : 'a -> bool) (F : 'a -> t) s x : + (#big [ i : s | P i ] (F i)) * x = #big [ i : s | P i ] (F i * x). proof. by rewrite big_distrl //; (apply/mul0r || apply/mulrDl). qed. -lemma mulr_sumr (P : 'a -> bool) F s x : - x * (big P F s) = big P (fun i => x * F i) s. +lemma mulr_sumr (P : 'a -> bool) (F : 'a -> t) s x : + x * (#big [ i : s | P i ] (F i)) = #big [ i : s | P i ] (x * F i). proof. by rewrite big_distrr //; (apply/mulr0 || apply/mulrDr). qed. -lemma divr_suml (P : 'a -> bool) F s x : - (big P F s) / x = big P (fun i => F i / x) s. +lemma divr_suml (P : 'a -> bool) (F : 'a -> t) s x : + (#big [ i : s | P i ] (F i)) / x = #big [ i : s | P i ] (F i / x). proof. by rewrite mulr_suml; apply/eq_bigr. qed. -lemma sum_pair_dep ['a 'b] u v J : uniq J => - big predT (fun (ij : 'a * 'b) => (u ij.`1 * v ij.`1 ij.`2)%CR) J - = big predT - (fun i => u i * big predT - (fun ij : _ * _ => v ij.`1 ij.`2) - (filter (fun ij : _ * _ => ij.`1 = i) J)) - (undup (unzip1 J)). +lemma sum_pair_dep ['a 'b] (u : 'a -> t) (v : 'a -> 'b -> t) (J : ('a * 'b) list) : + uniq J => + #big [ ij : J ] ((u ij.`1 * v ij.`1 ij.`2)%CR) + = #big [ i : (undup (unzip1 J)) ] + (u i * #big [ ij : (filter (fun ij : _ * _ => ij.`1 = i) J) ] (v ij.`1 ij.`2)). proof. move=> uqJ; rewrite big_pair // &(eq_bigr) => /= a _. by rewrite mulr_sumr !big_filter &(eq_bigr) => -[a' b] /= ->>. qed. -lemma sum_pair ['a 'b] u v J : uniq J => - big predT (fun (ij : 'a * 'b) => (u ij.`1 * v ij.`2)%CR) J - = big predT - (fun i => u i * big predT v (unzip2 (filter (fun ij : _ * _ => ij.`1 = i) J))) - (undup (unzip1 J)). +lemma sum_pair ['a 'b] (u : 'a -> t) (v : 'b -> t) (J : ('a * 'b) list) : + uniq J => + #big [ ij : J ] ((u ij.`1 * v ij.`2)%CR) + = #big [ i : (undup (unzip1 J)) ] + (u i * #big [ j : (unzip2 (filter (fun ij : _ * _ => ij.`1 = i) J)) ] (v j)). proof. move=> uqJ; rewrite (@sum_pair_dep u (fun _ => v)) // &(eq_bigr) /=. by move=> a _ /=; congr; rewrite big_map predT_comp /(\o). @@ -153,8 +155,8 @@ end BMul. (* -------------------------------------------------------------------- *) lemma mulr_big (P Q : 'a -> bool) (f g : 'a -> t) r s: - BAdd.big P f r * BAdd.big Q g s - = BAdd.big P (fun x => BAdd.big Q (fun y => f x * g y) s) r. + BAdd.#big [ x : r | P x ] (f x) * BAdd.#big [ y : s | Q y ] (g y) + = BAdd.#big [ x : r | P x ] (BAdd.#big [ y : s | Q y ] (f x * g y)). proof. elim: r s => [|x r ih] s; first by rewrite BAdd.big_nil mul0r. rewrite !BAdd.big_cons; case: (P x) => Px; last by rewrite ih. @@ -163,7 +165,7 @@ qed. (* -------------------------------------------------------------------- *) lemma subrXX (x y : t) n : 0 <= n => - exp x n - exp y n = (x - y) * (BAdd.bigi predT (fun i => exp x (n - 1 - i) * exp y i) 0 n). + exp x n - exp y n = (x - y) * (BAdd.#bigi [ i : 0, n ] (exp x (n - 1 - i) * exp y i)). proof. case: n => [|n ge0_n _]; first by rewrite !expr0 BAdd.big_geq // subrr mulr0. rewrite mulrBl !(BAdd.big_distrr mulr0 mulrDr). @@ -175,16 +177,16 @@ by rewrite -exprS 1:/# subr_eq0; do 2! congr => /#. qed. (* -------------------------------------------------------------------- *) -lemma mulr_const_cond p s c: - BMul.big<:'a> p (fun _ => c) s = exp c (count p s). +lemma mulr_const_cond ['a] (p : 'a -> bool) s c: + BMul.#big [ i : s | p i ] c = exp c (count p s). proof. rewrite BMul.big_const -MulMonoid.iteropE /exp. by rewrite IntOrder.ltrNge count_ge0. qed. (* -------------------------------------------------------------------- *) -lemma mulr_const s c: - BMul.big<:'a> predT (fun _ => c) s = exp c (size s). +lemma mulr_const ['a] (s : 'a list) c: + BMul.#big [ _ : s ] c = exp c (size s). proof. by rewrite mulr_const_cond count_predT. qed. end BigComRing. @@ -226,7 +228,7 @@ realize CR.unitout . proof. by apply/Num.Domain.unitout. qed. lemma ler_sum (P : 'a -> bool) (F1 F2 :'a -> t) s: (forall a, P a => F1 a <= F2 a) - => (BAdd.big P F1 s <= BAdd.big P F2 s). + => (BAdd.#big [ i : s | P i ] (F1 i) <= BAdd.#big [ i : s | P i ] (F2 i)). proof. apply: (@BAdd.big_ind2 (fun (x y : t) => x <= y)) => //=. by apply/ler_add. @@ -234,41 +236,41 @@ qed. lemma sumr_ge0 (P : 'a -> bool) (F : 'a -> t) s: (forall a, P a => zeror <= F a) - => zeror <= BAdd.big P F s. + => zeror <= BAdd.#big [ i : s | P i ] (F i). proof. move=> h; apply: (@BAdd.big_ind (fun x => zeror <= x)) => //=. by apply/addr_ge0. qed. -lemma sub_ler_sum (P1 P2 : 'a -> bool) (F1 F2 : 'a -> t) s : - (forall x, P1 x => P2 x) => +lemma sub_ler_sum (P1 P2 : 'a -> bool) (F1 F2 : 'a -> t) s : + (forall x, P1 x => P2 x) => (forall x, P1 x => F1 x <= F2 x) => (forall x, P2 x => !P1 x => zeror <= F2 x) => - BAdd.big P1 F1 s <= BAdd.big P2 F2 s. + BAdd.#big [ i : s | P1 i ] (F1 i) <= BAdd.#big [ i : s | P2 i ] (F2 i). proof. move => sub_P1_P2 le_F1_F2 pos_F2; rewrite (@BAdd.bigID P2 _ P1). have -> : predI P2 P1 = P1 by smt(). by rewrite -(addr0 (BAdd.big P1 F1 s)) ler_add ?ler_sum // sumr_ge0 /#. qed. -lemma sumr_norm P F s : +lemma sumr_norm ['a] (P : 'a -> bool) (F : 'a -> t) s : (forall x, P x => zeror <= F x) => - BAdd.big<:'a> P (fun x => `|F x|) s = BAdd.big P F s. + BAdd.#big [ x : s | P x ] `|F x| = BAdd.#big [ x : s | P x ] (F x). proof. by move=> ge0_F; apply: BAdd.eq_bigr => /= a Pa; rewrite ger0_norm /#. qed. -lemma prodr_ge0 (P : 'a -> bool) F s: +lemma prodr_ge0 (P : 'a -> bool) (F : 'a -> t) s: (forall a, P a => zeror <= F a) - => zeror <= BMul.big P F s. + => zeror <= BMul.#big [ i : s | P i ] (F i). proof. move=> h; apply: (@BMul.big_ind (fun x => zeror <= x)) => //=. by apply/mulr_ge0. qed. -lemma prodr_gt0 (P : 'a -> bool) F s: +lemma prodr_gt0 (P : 'a -> bool) (F : 'a -> t) s: (forall a, P a => zeror < F a) - => zeror < BMul.big P F s. + => zeror < BMul.#big [ i : s | P i ] (F i). proof. move=> h; apply: (@BMul.big_ind (fun x => zeror < x)) => //=. by apply/mulr_gt0. @@ -276,7 +278,7 @@ qed. lemma ler_prod (P : 'a -> bool) (F1 F2 :'a -> t) s: (forall a, P a => zeror <= F1 a <= F2 a) - => (BMul.big P F1 s <= BMul.big P F2 s). + => (BMul.#big [ i : s | P i ] (F1 i) <= BMul.#big [ i : s | P i ] (F2 i)). proof. move=> h; elim: s => [|x s ih]; first by rewrite !BMul.big_nil lerr. rewrite !BMul.big_cons; case: (P x)=> // /h [ge0F1x leF12x]. @@ -285,7 +287,7 @@ qed. lemma ler_sum_seq (P : 'a -> bool) (F1 F2 :'a -> t) s: (forall a, mem s a => P a => F1 a <= F2 a) - => (BAdd.big P F1 s <= BAdd.big P F2 s). + => (BAdd.#big [ i : s | P i ] (F1 i) <= BAdd.#big [ i : s | P i ] (F2 i)). proof. move=> h; rewrite !(@BAdd.big_seq_cond P). by rewrite ler_sum=> //= x []; apply/h. @@ -293,31 +295,31 @@ qed. lemma sumr_ge0_seq (P : 'a -> bool) (F : 'a -> t) s: (forall a, mem s a => P a => zeror <= F a) - => zeror <= BAdd.big P F s. + => zeror <= BAdd.#big [ i : s | P i ] (F i). proof. move=> h; rewrite !(@BAdd.big_seq_cond P). by rewrite sumr_ge0=> //= x []; apply/h. qed. -lemma prodr_ge0_seq (P : 'a -> bool) F s: +lemma prodr_ge0_seq (P : 'a -> bool) (F : 'a -> t) s: (forall a, mem s a => P a => zeror <= F a) - => zeror <= BMul.big P F s. + => zeror <= BMul.#big [ i : s | P i ] (F i). proof. move=> h; rewrite !(@BMul.big_seq_cond P). by rewrite prodr_ge0=> //= x []; apply/h. qed. -lemma prodr_gt0_seq (P : 'a -> bool) F s: +lemma prodr_gt0_seq (P : 'a -> bool) (F : 'a -> t) s: (forall a, mem s a => P a => zeror < F a) - => zeror < BMul.big P F s. + => zeror < BMul.#big [ i : s | P i ] (F i). proof. move=> h; rewrite !(@BMul.big_seq_cond P). by rewrite prodr_gt0=> //= x []; apply/h. qed. -lemma gt0_prodr_seq (P : 'a -> bool) (F : 'a -> t) (s : 'a list) : - (forall (a : 'a), a \in s => P a => zeror <= F a) => - zeror < BMul.big P F s => +lemma gt0_prodr_seq (P : 'a -> bool) (F : 'a -> t) (s : 'a list) : + (forall (a : 'a), a \in s => P a => zeror <= F a) => + zeror < BMul.#big [ i : s | P i ] (F i) => (forall (a : 'a), a \in s => P a => zeror < F a). proof. elim: s => // x s IHs F_ge0; rewrite BMul.big_cons. @@ -328,15 +330,15 @@ qed. lemma ler_prod_seq (P : 'a -> bool) (F1 F2 : 'a -> t) s: (forall a, mem s a => P a => zeror <= F1 a <= F2 a) - => (BMul.big P F1 s <= BMul.big P F2 s). + => (BMul.#big [ i : s | P i ] (F1 i) <= BMul.#big [ i : s | P i ] (F2 i)). proof. move=> h; rewrite !(@BMul.big_seq_cond P). by rewrite ler_prod=> //= x []; apply/h. qed. -lemma prodr_eq0 P F s: +lemma prodr_eq0 ['a] (P : 'a -> bool) (F : 'a -> t) s: (exists x, P x /\ x \in s /\ F x = zeror) - <=> BMul.big<:'a> P F s = zeror. + <=> BMul.#big [ i : s | P i ] (F i) = zeror. proof. split. + case=> x [# Px x_in_s z_Fx]; rewrite (@BMul.big_rem _ _ _ x) //. by rewrite Px /= z_Fx Num.Domain.mul0r. @@ -360,8 +362,8 @@ rewrite expr0 /= ltr_spaddr ?mul1r; 1: by rewrite expr_gt0 ltr_neqAle /#. by rewrite sumr_ge0 => /= i _; rewrite mulr_ge0 ?expr_ge0. qed. -lemma big_normr ['a] P F s : - `|BAdd.big<:'a> P F s| <= BAdd.big P (fun x => `|F x|) s. +lemma big_normr ['a] (P : 'a -> bool) (F : 'a -> t) s : + `|BAdd.#big [ x : s | P x ] (F x)| <= BAdd.#big [ x : s | P x ] `|F x|. proof. elim: s => [|x s ih]; first by rewrite !BAdd.big_nil normr0. rewrite !BAdd.big_cons /=; case: (P x) => // Px. @@ -370,7 +372,7 @@ by rewrite ler_add2l. qed. lemma sum_expr p n : 0 <= n => - (oner - p) * BAdd.bigi predT (fun i => exp p i) 0 n = oner - exp p n. + (oner - p) * BAdd.#bigi [ i : 0, n ] (exp p i) = oner - exp p n. proof. move=> hn; have /eq_sym := subrXX oner p n hn. rewrite expr1z // => <-; congr. @@ -380,14 +382,14 @@ qed. lemma sum_expr_le p n : 0 <= n => zeror <= p < oner - => (oner - p) * BAdd.bigi predT (fun i => exp p i) 0 n <= oner. + => (oner - p) * BAdd.#bigi [ i : 0, n ] (exp p i) <= oner. proof. move=> ge0_n [ge0_p lt1_p]; rewrite sum_expr //. by rewrite ler_subl_addr ler_paddr // expr_ge0. qed. lemma sum_iexpr_le p n : zeror <= p < oner => - exp (oner - p) 2 * BAdd.bigi predT (fun i => ofint i * exp p i) 0 n <= oner. + exp (oner - p) 2 * BAdd.#bigi [ i : 0, n ] (ofint i * exp p i) <= oner. proof. case=> [ge0_p lt1_p]; elim/natind: n => [n le0_n|n ge0_n ih]. + by rewrite BAdd.big_geq // mulr0. diff --git a/theories/algebra/Bigop.eca b/theories/algebra/Bigop.eca index 3d1e1a8272..d79328744e 100644 --- a/theories/algebra/Bigop.eca +++ b/theories/algebra/Bigop.eca @@ -24,21 +24,54 @@ abbrev bigi (P : int -> bool) (F : int -> t) i j = big P F (range i j). (* -------------------------------------------------------------------- *) -lemma big_nil (P : 'a -> bool) (F : 'a -> t): big P F [] = idm. +(* Surface notations. *) +(* *) +(* #big [ i : r ] F == big predT (fun i => F) r *) +(* #big [ i : r | P ] F == big (fun i => P) (fun i => F) r *) +(* #bigi [ i : a, b ] F == bigi predT (fun i => F) a b *) +(* #bigi [ i : a, b | P ] F == bigi (fun i => P) (fun i => F) a b *) +(* *) +(* The predicate slot [P] defaults to [predT] and the whole [`| P`] *) +(* group is omitted from the printed form when [P = predT]. *) +(* *) +(* The trailing form slot parses at simple-expression (sform) level so a *) +(* following equality like `= rhs` is not absorbed. Applications like *) +(* `F i` must therefore be parenthesized: `#big [...] (F i)`. *) + +notation #big ['a] #< i : 'a > + (r : 'a list) + (P : i ==> bool = predT) + (F : i ==> t) + "[" i " : " r ("| " P)? "] " F = + big P F r. + +notation #bigi #< i : int > + (a : int) (b : int) + (P : i ==> bool = predT) + (F : i ==> t) + "[" i " : " a ", " b ("| " P)? "] " F = + bigi P F a b. + +(* -------------------------------------------------------------------- *) +lemma big_nil (P : 'a -> bool) (F : 'a -> t): + #big [ i : [] | P i ] (F i) = idm. proof. by []. qed. (* -------------------------------------------------------------------- *) lemma big_cons (P : 'a -> bool) (F : 'a -> t) x s: - big P F (x :: s) = if P x then F x + big P F s else big P F s. + #big [ i : (x :: s) | P i ] (F i) + = if P x then F x + #big [ i : s | P i ] (F i) else #big [ i : s | P i ] (F i). proof. by rewrite {1}/big /= (@fun_if (map F)); case (P x). qed. lemma big_consT (F : 'a -> t) x s: - big predT F (x :: s) = F x + big predT F s. + #big [ i : (x :: s) ] (F i) = F x + #big [ i : s ] (F i). proof. by apply/big_cons. qed. (* -------------------------------------------------------------------- *) lemma big_rec (K : t -> bool) r P (F : 'a -> t): - K idm => (forall i x, P i => K x => K (F i + x)) => K (big P F r). + K idm + => (forall i x, P i => K x => K (F i + x)) + => K (#big [ i : r | P i ] (F i)). proof. move=> K0 Kop; elim: r => //= i r; rewrite big_cons. by case (P i) => //=; apply/Kop. @@ -47,7 +80,7 @@ qed. lemma big_ind (K : t -> bool) r P (F : 'a -> t): (forall x y, K x => K y => K (x + y)) => K idm => (forall i, P i => K (F i)) - => K (big P F r). + => K (#big [ i : r | P i ] (F i)). proof. move=> Kop Kidx K_F; apply/big_rec => //. by move=> i x Pi Kx; apply/Kop => //; apply/K_F. @@ -57,7 +90,7 @@ lemma big_rec2: forall (K : t -> t -> bool) r P (F1 F2 : 'a -> t), K idm idm => (forall i y1 y2, P i => K y1 y2 => K (F1 i + y1) (F2 i + y2)) - => K (big P F1 r) (big P F2 r). + => K (#big [ i : r | P i ] (F1 i)) (#big [ i : r | P i ] (F2 i)). proof. move=> K r P F1 F2 KI KF; elim: r => //= i r IHr. by rewrite !big_cons; case (P i) => ? //=; apply/KF. @@ -68,7 +101,7 @@ lemma big_ind2: (forall x1 x2 y1 y2, K x1 x2 => K y1 y2 => K (x1 + y1) (x2 + y2)) => K idm idm => (forall i, P i => K (F1 i) (F2 i)) - => K (big P F1 r) (big P F2 r). + => K (#big [ i : r | P i ] (F1 i)) (#big [ i : r | P i ] (F2 i)). proof. move=> K r P F1 F2 Kop KI KF; apply/big_rec2 => //. by move=> i x1 x2 Pi Kx1x2; apply/Kop => //; apply/KF. @@ -79,7 +112,8 @@ lemma big_endo (f : t -> t): f idm = idm => (forall (x y : t), f (x + y) = f x + f y) => forall r P (F : 'a -> t), - f (big P F r) = big P (f \o F) r. + f (#big [ i : r | P i ] (F i)) + = #big [ i : r | P i ] ((f \o F) i). proof. (* FIXME: should be a consequence of big_morph *) move=> fI fM; elim=> //= i r IHr P F; rewrite !big_cons. @@ -88,17 +122,20 @@ qed. (* -------------------------------------------------------------------- *) lemma big_map ['a 'b] (h : 'b -> 'a) (P : 'a -> bool) F s: - big P F (map h s) = big (P \o h) (F \o h) s. + #big [ i : (map h s) | P i ] (F i) + = #big [ i : s | (P \o h) i ] ((F \o h) i). proof. by elim: s => // x s; rewrite map_cons !big_cons=> ->. qed. lemma big_mapT ['a 'b] (h : 'b -> 'a) F s: (* -> big_map_predT *) - big predT F (map h s) = big predT (F \o h) s. + #big [ i : (map h s) ] (F i) = #big [ i : s ] ((F \o h) i). proof. by rewrite big_map. qed. (* -------------------------------------------------------------------- *) lemma big_comp ['a] (h : t -> t) (P : 'a -> bool) F s: - h idm = idm => morphism_2 h Support.(+) Support.(+) => - h (big P F s) = big P (h \o F) s. + h idm = idm + => morphism_2 h Support.(+) Support.(+) + => h (#big [ i : s | P i ] (F i)) + = #big [ i : s | P i ] ((h \o F) i). proof. move=> Hidm Hh;elim: s => // x s; rewrite !big_cons => <-. by rewrite /(\o) -Hh;case (P x) => //. @@ -106,24 +143,26 @@ qed. (* -------------------------------------------------------------------- *) lemma big_nth x0 (P : 'a -> bool) (F : 'a -> t) s: - big P F s = bigi (P \o (nth x0 s)) (F \o (nth x0 s)) 0 (size s). + #big [ i : s | P i ] (F i) + = #bigi [ k : 0, size s | (P \o (nth x0 s)) k ] ((F \o (nth x0 s)) k). proof. by rewrite -{1}(@mkseq_nth x0 s) /mkseq big_map. qed. (* -------------------------------------------------------------------- *) lemma big_const (P : 'a -> bool) x s: - big P (fun i => x) s = iter (count P s) ((+) x) idm. + #big [ i : s | P i ] x = iter (count P s) ((+) x) idm. proof. elim: s=> [|y s ih]; [by rewrite iter0 | rewrite big_cons /=]. by rewrite ih; case (P y) => //; rewrite addzC iterS // count_ge0. qed. (* -------------------------------------------------------------------- *) -lemma big_seq1 (F : 'a -> t) x: big predT F [x] = F x. +lemma big_seq1 (F : 'a -> t) x: #big [ i : [x] ] (F i) = F x. proof. by rewrite big_cons big_nil addm0. qed. (* -------------------------------------------------------------------- *) lemma big_mkcond (P : 'a -> bool) (F : 'a -> t) s: - big P F s = big predT (fun i => if P i then F i else idm) s. + #big [ i : s | P i ] (F i) + = #big [ i : s ] (if P i then F i else idm). proof. elim: s=> // x s ih; rewrite !big_cons -ih /predT /=. by case (P x)=> //; rewrite add0m. @@ -131,24 +170,25 @@ qed. (* -------------------------------------------------------------------- *) lemma big_filter (P : 'a -> bool) F s: - big predT F (filter P s) = big P F s. + #big [ i : (filter P s) ] (F i) = #big [ i : s | P i ] (F i). proof. by elim: s => //= x s; case (P x)=> //; rewrite !big_cons=> -> ->. qed. (* -------------------------------------------------------------------- *) lemma big_filter_cond (P1 P2 : 'a -> bool) F s: - big P2 F (filter P1 s) = big (predI P1 P2) F s. + #big [ i : (filter P1 s) | P2 i ] (F i) + = #big [ i : s | predI P1 P2 i ] (F i). proof. by rewrite -big_filter -(@big_filter _ _ s) predIC filter_predI. qed. (* -------------------------------------------------------------------- *) lemma eq_bigl (P1 P2 : 'a -> bool) (F : 'a -> t) s: (forall i, P1 i <=> P2 i) - => big P1 F s = big P2 F s. + => #big [ i : s | P1 i ] (F i) = #big [ i : s | P2 i ] (F i). proof. by move=> h; rewrite /big (eq_filter h). qed. (* -------------------------------------------------------------------- *) lemma eq_bigr (P : 'a -> bool) (F1 F2 : 'a -> t) s: (forall i, P i => F1 i = F2 i) - => big P F1 s = big P F2 s. + => #big [ i : s | P i ] (F1 i) = #big [ i : s | P i ] (F2 i). proof. (* FIXME: big_rec2 *) move=> eqF; elim: s=> // x s; rewrite !big_cons=> <-. by case (P x)=> // /eqF <-. @@ -158,7 +198,8 @@ qed. lemma big_distrl ['a] (op_ : t -> t -> t) (P : 'a -> bool) F s t: left_zero idm op_ => left_distributive op_ Support.(+) - => op_ (big P F s) t = big P (fun a => op_ (F a) t) s. + => op_ (#big [ i : s | P i ] (F i)) t + = #big [ i : s | P i ] (op_ (F i) t). proof. move=> mulm1 mulmDl; pose G := fun x => op_ x t. move: (big_comp G P) => @/G /= -> //. @@ -168,7 +209,8 @@ qed. lemma big_distrr ['a] (op_ : t -> t -> t) (P : 'a -> bool) F s t: right_zero idm op_ => right_distributive op_ Support.(+) - => op_ t (big P F s) = big P (fun a => op_ t (F a)) s. + => op_ t (#big [ i : s | P i ] (F i)) + = #big [ i : s | P i ] (op_ t (F i)). proof. move=> mul1m mulmDr; pose G := fun x => op_ t x. move: (big_comp G P) => @/G /= -> //. @@ -180,8 +222,9 @@ lemma big_distr ['a 'b] (op_ : t -> t -> t) commutative op_ => left_zero idm op_ => left_distributive op_ Support.(+) - => op_ (big P1 F1 s1) (big P2 F2 s2) = - big P1 (fun a1 => big P2 (fun a2 => op_ (F1 a1) (F2 a2)) s2) s1. + => op_ (#big [ i : s1 | P1 i ] (F1 i)) (#big [ j : s2 | P2 j ] (F2 j)) + = #big [ i : s1 | P1 i ] + (#big [ j : s2 | P2 j ] (op_ (F1 i) (F2 j))). proof. move=> mulmC mulm1 mulmDl; rewrite big_distrl //. apply/eq_bigr=> i _ /=; rewrite big_distrr //. @@ -191,14 +234,15 @@ qed. (* -------------------------------------------------------------------- *) lemma big_andbC (P Q : 'a -> bool) F s: - big (fun x => P x /\ Q x) F s = big (fun x => Q x /\ P x) F s. + #big [ i : s | P i /\ Q i ] (F i) + = #big [ i : s | Q i /\ P i ] (F i). proof. by apply/eq_bigl=> i. qed. (* -------------------------------------------------------------------- *) lemma eq_big (P1 P2 : 'a -> bool) (F1 F2 : 'a -> t) s: (forall i, P1 i <=> P2 i) => (forall i, P1 i => F1 i = F2 i) - => big P1 F1 s = big P2 F2 s. + => #big [ i : s | P1 i ] (F1 i) = #big [ i : s | P2 i ] (F2 i). proof. by move=> /eq_bigl <- /eq_bigr <-. qed. (* -------------------------------------------------------------------- *) @@ -206,29 +250,31 @@ lemma congr_big r1 r2 P1 P2 (F1 F2 : 'a -> t): r1 = r2 => (forall x, P1 x <=> P2 x) => (forall i, P1 i => F1 i = F2 i) - => big P1 F1 r1 = big P2 F2 r2. + => #big [ i : r1 | P1 i ] (F1 i) = #big [ i : r2 | P2 i ] (F2 i). proof. by move=> <-; apply/eq_big. qed. (* -------------------------------------------------------------------- *) -lemma big_hasC (P : 'a -> bool) (F : 'a -> t) s: !has P s => - big P F s = idm. +lemma big_hasC (P : 'a -> bool) (F : 'a -> t) s: + !has P s => #big [ i : s | P i ] (F i) = idm. proof. rewrite -big_filter has_count -size_filter. by rewrite ltz_def size_ge0 /= => /size_eq0 ->. qed. (* -------------------------------------------------------------------- *) -lemma big_pred0_eq (F : 'a -> t) s: big pred0 F s = idm. +lemma big_pred0_eq (F : 'a -> t) s: + #big [ i : s | pred0 i ] (F i) = idm. proof. by rewrite big_hasC // has_pred0. qed. (* -------------------------------------------------------------------- *) lemma big_pred0 (P : 'a -> bool) (F : 'a -> t) s: - (forall i, P i <=> false) => big P F s = idm. + (forall i, P i <=> false) => #big [ i : s | P i ] (F i) = idm. proof. by move=> h; rewrite -(@big_pred0_eq F s); apply/eq_bigl. qed. (* -------------------------------------------------------------------- *) lemma big_cat (P : 'a -> bool) (F : 'a -> t) s1 s2: - big P F (s1 ++ s2) = big P F s1 + big P F s2. + #big [ i : (s1 ++ s2) | P i ] (F i) + = #big [ i : s1 | P i ] (F i) + #big [ i : s2 | P i ] (F i). proof. rewrite !(@big_mkcond P); elim: s1 => /= [|i s1 ih]. by rewrite (@big_nil P F) add0m. @@ -236,25 +282,30 @@ proof. qed. (* -------------------------------------------------------------------- *) -lemma big_catl (P : 'a -> bool) (F : 'a -> t) s1 s2: !has P s2 => - big P F (s1 ++ s2) = big P F s1. +lemma big_catl (P : 'a -> bool) (F : 'a -> t) s1 s2: + !has P s2 + => #big [ i : (s1 ++ s2) | P i ] (F i) = #big [ i : s1 | P i ] (F i). proof. by rewrite big_cat => /big_hasC ->; rewrite addm0. qed. (* -------------------------------------------------------------------- *) -lemma big_catr (P : 'a -> bool) (F : 'a -> t) s1 s2: !has P s1 => - big P F (s1 ++ s2) = big P F s2. +lemma big_catr (P : 'a -> bool) (F : 'a -> t) s1 s2: + !has P s1 + => #big [ i : (s1 ++ s2) | P i ] (F i) = #big [ i : s2 | P i ] (F i). proof. by rewrite big_cat => /big_hasC ->; rewrite add0m. qed. (* -------------------------------------------------------------------- *) lemma big_rcons (P : 'a -> bool) (F : 'a -> t) s x: - big P F (rcons s x) = if P x then big P F s + F x else big P F s. + #big [ i : (rcons s x) | P i ] (F i) + = if P x then #big [ i : s | P i ] (F i) + F x + else #big [ i : s | P i ] (F i). proof. by rewrite -cats1 big_cat big_cons big_nil; case: (P x); rewrite !addm0. qed. (* -------------------------------------------------------------------- *) lemma eq_big_perm (P : 'a -> bool) (F : 'a -> t) s1 s2: - perm_eq s1 s2 => big P F s1 = big P F s2. + perm_eq s1 s2 + => #big [ i : s1 | P i ] (F i) = #big [ i : s2 | P i ] (F i). proof. move=> /perm_eqP; rewrite !(@big_mkcond P). elim s1 s2 => [|i s1 ih1] s2 eq_s12. @@ -269,44 +320,50 @@ qed. (* -------------------------------------------------------------------- *) lemma eq_big_perm_map (F : 'a -> t) s1 s2: - perm_eq (map F s1) (map F s2) => big predT F s1 = big predT F s2. + perm_eq (map F s1) (map F s2) + => #big [ i : s1 ] (F i) = #big [ i : s2 ] (F i). proof. by move=> peq; rewrite -!(@big_map F predT idfun) &(eq_big_perm). qed. (* -------------------------------------------------------------------- *) lemma big_seq_cond (P : 'a -> bool) (F : 'a -> t) s: - big P F s = big (fun i => mem s i /\ P i) F s. + #big [ i : s | P i ] (F i) + = #big [ i : s | mem s i /\ P i ] (F i). proof. by rewrite -!(@big_filter _ _ s); congr; apply/eq_in_filter. qed. (* -------------------------------------------------------------------- *) lemma big_seq (F : 'a -> t) s: - big predT F s = big (fun i => mem s i) F s. + #big [ i : s ] (F i) = #big [ i : s | mem s i ] (F i). proof. by rewrite big_seq_cond; apply/eq_bigl. qed. (* -------------------------------------------------------------------- *) lemma big_rem (P : 'a -> bool) (F : 'a -> t) s x: mem s x => - big P F s = (if P x then F x else idm) + big P F (rem x s). + #big [ i : s | P i ] (F i) + = (if P x then F x else idm) + #big [ i : (rem x s) | P i ] (F i). proof. by move/perm_to_rem/eq_big_perm=> ->; rewrite !(@big_mkcond P) big_cons. qed. (* -------------------------------------------------------------------- *) lemma bigD1 (F : 'a -> t) s x: mem s x => uniq s => - big predT F s = F x + big (predC1 x) F s. + #big [ i : s ] (F i) = F x + #big [ i : s | predC1 x i ] (F i). proof. by move=> /big_rem-> /rem_filter->; rewrite big_filter. qed. (* -------------------------------------------------------------------- *) lemma bigD1_cond P (F : 'a -> t) s x: P x => mem s x => uniq s => - big P F s = F x + big (predI P (predC1 x)) F s. + #big [ i : s | P i ] (F i) + = F x + #big [ i : s | predI P (predC1 x) i ] (F i). proof. move=> Px sx uqs; rewrite -big_filter (@bigD1 _ _ x) ?big_filter_cond //. by rewrite mem_filter Px. by rewrite filter_uniq. qed. (* -------------------------------------------------------------------- *) -lemma bigD1_cond_if P (F : 'a -> t) s x: uniq s => big P F s = - (if mem s x /\ P x then F x else idm) + big (predI P (predC1 x)) F s. +lemma bigD1_cond_if P (F : 'a -> t) s x: uniq s => + #big [ i : s | P i ] (F i) + = (if mem s x /\ P x then F x else idm) + + #big [ i : s | predI P (predC1 x) i ] (F i). proof. case: (mem s x /\ P x) => [[Px sx]|Nsx]; rewrite ?add0m /=. by apply/bigD1_cond. @@ -316,7 +373,8 @@ qed. (* -------------------------------------------------------------------- *) lemma big_split (P : 'a -> bool) (F1 F2 : 'a -> t) s: - big P (fun i => F1 i + F2 i) s = big P F1 s + big P F2 s. + #big [ i : s | P i ] (F1 i + F2 i) + = #big [ i : s | P i ] (F1 i) + #big [ i : s | P i ] (F2 i). proof. elim: s=> /= [|x s ih]; 1: by rewrite !big_nil addm0. rewrite !big_cons ih; case: (P x) => // _. @@ -325,7 +383,9 @@ qed. (* -------------------------------------------------------------------- *) lemma bigID (P : 'a -> bool) (F : 'a -> t) (a : 'a -> bool) s: - big P F s = big (predI P a) F s + big (predI P (predC a)) F s. + #big [ i : s | P i ] (F i) + = #big [ i : s | predI P a i ] (F i) + + #big [ i : s | predI P (predC a) i ] (F i). proof. rewrite !(@big_mkcond _ F) -big_split; apply/eq_bigr => i _ /=. by rewrite /predI /predC; case: (a i); rewrite ?addm0 ?add0m. @@ -333,7 +393,8 @@ qed. (* -------------------------------------------------------------------- *) lemma bigU ['a] (P Q : 'a -> bool) F s : (forall x, !(P x /\ Q x)) => - big (predU P Q) F s = big P F s + big Q F s. + #big [ i : s | predU P Q i ] (F i) + = #big [ i : s | P i ] (F i) + #big [ i : s | Q i ] (F i). proof. move=> dj_PQ; rewrite (@bigID (predU _ _) _ P). by congr; apply: eq_bigl => /#. @@ -341,35 +402,37 @@ qed. (* -------------------------------------------------------------------- *) lemma bigEM ['a] (P : 'a -> bool) (F : 'a -> t) s : - big predT F s = big P F s + big (predC P) F s. + #big [ i : s ] (F i) + = #big [ i : s | P i ] (F i) + #big [ i : s | predC P i ] (F i). proof. by rewrite -bigU 1:/#; apply: eq_bigl => /#. qed. (* -------------------------------------------------------------------- *) lemma big_reindex ['a 'b] (P : 'a -> bool) (F : 'a -> t) (f : 'b -> 'a) (f' : 'a -> 'b) (s : 'a list) : - (forall x, x \in s => f (f' x) = x) - => big P F s = big (P \o f) (F \o f) (map f' s). -proof. + (forall x, x \in s => f (f' x) = x) + => #big [ i : s | P i ] (F i) + = #big [ i : (map f' s) | (P \o f) i ] ((F \o f) i). +proof. by move => /eq_in_map id_ff'; rewrite -big_map -map_comp id_ff' id_map. qed. (* -------------------------------------------------------------------- *) -lemma big_pair_pswap ['a 'b] p f s : - big<:'a * 'b> p f s - = big<:'b * 'a> (p \o pswap) (f \o pswap) (map pswap s). +lemma big_pair_pswap ['a 'b] (p : 'a * 'b -> bool) (f : 'a * 'b -> t) s : + #big [ i : s | p i ] (f i) + = #big [ i : (map pswap s) | (p \o pswap) i ] ((f \o pswap) i). proof. by apply/big_reindex; case. qed. (* -------------------------------------------------------------------- *) lemma eq_big_seq (F1 F2 : 'a -> t) s: (forall x, mem s x => F1 x = F2 x) - => big predT F1 s = big predT F2 s. + => #big [ i : s ] (F1 i) = #big [ i : s ] (F2 i). proof. by move=> eqF; rewrite !big_seq; apply/eq_bigr. qed. (* -------------------------------------------------------------------- *) lemma congr_big_seq (P1 P2: 'a -> bool) (F1 F2 : 'a -> t) s: (forall x, mem s x => P1 x = P2 x) => (forall x, mem s x => P1 x => P2 x => F1 x = F2 x) - => big P1 F1 s = big P2 F2 s. + => #big [ i : s | P1 i ] (F1 i) = #big [ i : s | P2 i ] (F2 i). proof. move=> eqP eqH; rewrite big_mkcond eq_sym big_mkcond eq_sym. apply/eq_big_seq=> x x_in_s /=; rewrite eqP //. @@ -377,7 +440,7 @@ proof. qed. (* -------------------------------------------------------------------- *) -lemma big1_eq (P : 'a -> bool) s: big P (fun x => idm) s = idm. +lemma big1_eq (P : 'a -> bool) s: #big [ i : s | P i ] idm = idm. proof. rewrite big_const; elim/natind: (count _ _)=> n. by move/iter0<:t> => ->. @@ -386,24 +449,27 @@ qed. (* -------------------------------------------------------------------- *) lemma big1 (P : 'a -> bool) F s: - (forall i, P i => F i = idm) => big P F s = idm. + (forall i, P i => F i = idm) => #big [ i : s | P i ] (F i) = idm. proof. by move/eq_bigr=> ->; apply/big1_eq. qed. (* -------------------------------------------------------------------- *) lemma big1_seq (P : 'a -> bool) F s: - (forall i, P i /\ (mem s i) => F i = idm) => big P F s = idm. + (forall i, P i /\ (mem s i) => F i = idm) + => #big [ i : s | P i ] (F i) = idm. proof. by move=> eqF1; rewrite big_seq_cond big_andbC big1. qed. (* -------------------------------------------------------------------- *) lemma big_eq_idm_filter ['a] (P : 'a -> bool) (F : 'a -> t) s : - (forall (x : 'a), !P x => F x = idm) => big predT F s = big P F s. + (forall (x : 'a), !P x => F x = idm) + => #big [ i : s ] (F i) = #big [ i : s | P i ] (F i). proof. by move=> eq1; rewrite (@bigEM P) (@big1 (predC _)) // addm0. qed. (* -------------------------------------------------------------------- *) lemma big_flatten (P : 'a -> bool) F rr : - big P F (flatten rr) = big predT (fun s => big P F s) rr. + #big [ i : (flatten rr) | P i ] (F i) + = #big [ s : rr ] (#big [ i : s | P i ] (F i)). proof. elim: rr => /= [|r rr ih]; first by rewrite !big_nil. by rewrite flatten_cons big_cat big_cons -ih. @@ -411,10 +477,9 @@ qed. (* -------------------------------------------------------------------- *) lemma big_pair ['a 'b] F (s : ('a * 'b) list) : uniq s => - big predT F s = - big predT (fun a => - big predT F (filter (fun xy : _ * _ => xy.`1 = a) s)) - (undup (map fst s)). + #big [ i : s ] (F i) + = #big [ a : (undup (map fst s)) ] + (#big [ xy : (filter (fun xy : _ * _ => xy.`1 = a) s) ] (F xy)). proof. move=> /perm_eq_pair /eq_big_perm /(_ predT F) ->. by rewrite big_flatten big_map. @@ -422,7 +487,8 @@ qed. (* -------------------------------------------------------------------- *) lemma big_nseq_cond (P : 'a -> bool) F n x : - big P F (nseq n x) = if P x then iter n ((+) (F x)) idm else idm. + #big [ i : (nseq n x) | P i ] (F i) + = if P x then iter n ((+) (F x)) idm else idm. proof. elim/natind: n => [n le0_n|n ge0_n ih]; first by rewrite ?(nseq0_le, iter0). by rewrite nseqS // big_cons ih; case: (P x) => //; rewrite iterS. @@ -430,12 +496,14 @@ qed. (* -------------------------------------------------------------------- *) lemma big_nseq (F : 'a -> t) n x : - big predT F (nseq n x) = iter n ((+) (F x)) idm. + #big [ i : (nseq n x) ] (F i) = iter n ((+) (F x)) idm. proof. by apply/big_nseq_cond. qed. (* -------------------------------------------------------------------- *) lemma big_undup ['a] (P : 'a -> bool) F s : - big P F s = big P (fun a => iter (count (pred1 a) s) ((+) (F a)) idm) (undup s). + #big [ i : s | P i ] (F i) + = #big [ a : (undup s) | P a ] + (iter (count (pred1 a) s) ((+) (F a)) idm). proof. have <- := eq_big_perm P F _ _ (perm_undup_count s). rewrite big_flatten big_map (@big_mkcond P); apply/eq_big => //=. @@ -444,8 +512,8 @@ qed. (* -------------------------------------------------------------------- *) lemma exchange_big (P1 : 'a -> bool) (P2 : 'b -> bool) F s1 s2: - big P1 (fun a => big P2 (F a) s2) s1 = - big P2 (fun b => big P1 (fun a => F a b) s1) s2. + #big [ a : s1 | P1 a ] (#big [ b : s2 | P2 b ] (F a b)) + = #big [ b : s2 | P2 b ] (#big [ a : s1 | P1 a ] (F a b)). proof. elim: s1 s2 => [|a s1 ih] s2; first by rewrite big_nil big1_eq. rewrite big_cons ih; case: (P1 a)=> h; rewrite -?big_split; @@ -456,7 +524,9 @@ qed. lemma partition_big ['a 'b] (px : 'a -> 'b) P Q (F : 'a -> t) s s' : uniq s' => (forall x, mem s x => P x => mem s' (px x) /\ Q (px x)) - => big P F s = big Q (fun x => big (fun y => P y /\ px y = x) F s) s'. + => #big [ i : s | P i ] (F i) + = #big [ x : s' | Q x ] + (#big [ y : s | P y /\ px y = x ] (F y)). proof. move=> uq_s'; elim: s => /~= [|x xs ih] hm. by rewrite big_nil big1_eq. @@ -474,21 +544,22 @@ qed. (* -------------------------------------------------------------------- *) lemma big_allpairs f F s t: - big predT F (allpairs<:'a, 'b, 'c> f s t) - = big predT (fun x => big predT (fun y => F (f x y)) t) s. + #big [ i : (allpairs<:'a, 'b, 'c> f s t) ] (F i) + = #big [ x : s ] (#big [ y : t ] (F (f x y))). proof. -elim: s t => [|x s ih] t //=. +elim: s t => [|x s ih] t //=. by rewrite allpairs_consl big_cat ih big_consT big_map. qed. (* -------------------------------------------------------------------- *) lemma big_int_cond m n P F: - bigi P F m n = bigi (fun i => m <= i < n /\ P i) F m n. + #bigi [ i : m, n | P i ] (F i) + = #bigi [ i : m, n | m <= i < n /\ P i ] (F i). proof. by rewrite big_seq_cond; apply/eq_bigl=> i /=; rewrite mem_range. qed. (* -------------------------------------------------------------------- *) lemma big_int m n F: - bigi predT F m n = bigi (fun i => m <= i < n) F m n. + #bigi [ i : m, n ] (F i) = #bigi [ i : m, n | m <= i < n ] (F i). proof. by rewrite big_int_cond. qed. (* -------------------------------------------------------------------- *) @@ -496,7 +567,8 @@ lemma congr_big_int (m1 n1 m2 n2 : int) P1 P2 F1 F2: m1 = m2 => n1 = n2 => (forall i, m1 <= i < n2 => P1 i = P2 i) => (forall i, P1 i /\ (m1 <= i < n2) => F1 i = F2 i) - => bigi P1 F1 m1 n1 = bigi P2 F2 m2 n2. + => #bigi [ i : m1, n1 | P1 i ] (F1 i) + = #bigi [ i : m2, n2 | P2 i ] (F2 i). proof. move=> <- <- eqP12 eqF12; rewrite big_seq_cond (@big_seq_cond P2). by apply/eq_big=> i /=; rewrite mem_range #smt:(). @@ -505,29 +577,29 @@ qed. (* -------------------------------------------------------------------- *) lemma eq_big_int (m n : int) F1 F2: (forall i, m <= i < n => F1 i = F2 i) - => bigi predT F1 m n = bigi predT F2 m n. + => #bigi [ i : m, n ] (F1 i) = #bigi [ i : m, n ] (F2 i). proof. by move=> eqF; apply/congr_big_int. qed. (* -------------------------------------------------------------------- *) lemma big_ltn_cond (m n : int) P F: m < n => - let x = bigi P F (m+1) n in - bigi P F m n = if P m then F m + x else x. + let x = #bigi [ i : (m+1), n | P i ] (F i) in + #bigi [ i : m, n | P i ] (F i) = if P m then F m + x else x. proof. by move/range_ltn=> ->; rewrite big_cons. qed. (* -------------------------------------------------------------------- *) lemma big_ltn (m n : int) F: m < n => - bigi predT F m n = F m + bigi predT F (m+1) n. + #bigi [ i : m, n ] (F i) = F m + #bigi [ i : (m+1), n ] (F i). proof. by move/big_ltn_cond=> /= ->. qed. (* -------------------------------------------------------------------- *) lemma big_geq (m n : int) P F: n <= m => - bigi P F m n = idm. + #bigi [ i : m, n | P i ] (F i) = idm. proof. by move/range_geq=> ->; rewrite big_nil. qed. (* -------------------------------------------------------------------- *) lemma big_addn (m n a : int) P F: - bigi P F (m+a) n - = bigi (fun i => P (i+a)) (fun i => F (i+a)) m (n-a). + #bigi [ i : (m+a), n | P i ] (F i) + = #bigi [ i : m, (n-a) | P (i+a) ] (F (i+a)). proof. rewrite range_addl big_map; apply/eq_big. by move=> i /=; rewrite /(\o) addzC. @@ -535,43 +607,45 @@ by move=> i /= _; rewrite /(\o) addzC. qed. (* -------------------------------------------------------------------- *) -lemma big_int1 n F: bigi predT F n (n+1) = F n. +lemma big_int1 n F: #bigi [ i : n, (n+1) ] (F i) = F n. proof. by rewrite big_ltn 1:/# big_geq // addm0. qed. (* -------------------------------------------------------------------- *) lemma big_cat_int (n m p : int) P F: m <= n => n <= p => - bigi P F m p = (bigi P F m n) + (bigi P F n p). + #bigi [ i : m, p | P i ] (F i) + = #bigi [ i : m, n | P i ] (F i) + #bigi [ i : n, p | P i ] (F i). proof. by move=> lemn lenp; rewrite -big_cat -range_cat. qed. (* -------------------------------------------------------------------- *) lemma big_int_recl (n m : int) F: m <= n => - bigi predT F m (n+1) = F m + bigi predT (fun i => F (i+1)) m n. + #bigi [ i : m, (n+1) ] (F i) + = F m + #bigi [ i : m, n ] (F (i+1)). proof. by move=> lemn; rewrite big_ltn 1?big_addn /= 1:/#. qed. (* -------------------------------------------------------------------- *) lemma big_int_recr (n m : int) F: m <= n => - bigi predT F m (n+1) = bigi predT F m n + F n. + #bigi [ i : m, (n+1) ] (F i) = #bigi [ i : m, n ] (F i) + F n. proof. by move=> lemn; rewrite (@big_cat_int n) ?big_int1 //#. qed. (* -------------------------------------------------------------------- *) lemma big_int_recl_cond (n m : int) P F: m <= n => - bigi P F m (n+1) = - (if P m then F m else idm) + - bigi (fun i => P (i+1)) (fun i => F (i+1)) m n. + #bigi [ i : m, (n+1) | P i ] (F i) + = (if P m then F m else idm) + + #bigi [ i : m, n | P (i+1) ] (F (i+1)). proof. by move=> lemn; rewrite big_mkcond big_int_recl //= -big_mkcond. qed. (* -------------------------------------------------------------------- *) lemma big_int_recr_cond (n m : int) P F: m <= n => - bigi P F m (n+1) = - bigi P F m n + (if P n then F n else idm). + #bigi [ i : m, (n+1) | P i ] (F i) + = #bigi [ i : m, n | P i ] (F i) + (if P n then F n else idm). proof. by move=> lemn; rewrite !(@big_mkcond P) big_int_recr. qed. (* -------------------------------------------------------------------- *) lemma bigi_split_odd_even (n : int) (F : int -> t) : 0 <= n => - bigi predT (fun i => F (2 * i) + F (2 * i + 1)) 0 n - = bigi predT F 0 (2 * n). + #bigi [ i : 0, n ] (F (2 * i) + F (2 * i + 1)) + = #bigi [ i : 0, (2 * n) ] (F i). proof. move=> ge0_n; rewrite big_split; pose rg := range 0 n. rewrite -(@big_mapT (fun i => 2 * i)). diff --git a/theories/algebra/Binomial.ec b/theories/algebra/Binomial.ec index d250a593af..43563c5093 100644 --- a/theories/algebra/Binomial.ec +++ b/theories/algebra/Binomial.ec @@ -3,7 +3,7 @@ require import AllCore List Ring StdBigop StdOrder. (*---*) import Bigint IntOrder. (* -------------------------------------------------------------------- *) -op fact (n : int) = BIM.bigi predT idfun 1 (n+1). +op fact (n : int) = BIM.#bigi [ i : 1, (n+1) ] (idfun i). lemma fact0 (n : int) : n <= 0 => fact n = 1. proof. by move=> le0n; rewrite /fact BIM.big_geq // ler_naddl. qed. @@ -142,7 +142,7 @@ realize CR.unitout by exact/R.unitout . clear [BCR.* BCR.BAdd.* BCR.BMul.*]. lemma binomial (x y : t) n : 0 <= n => exp (x + y) n = - BAdd.bigi predT (fun i => intmul (exp x i * exp y (n - i)) (bin n i)) 0 (n + 1). + BAdd.#bigi [ i : 0, (n + 1) ] (intmul (exp x i * exp y (n - i)) (bin n i)). proof. elim: n => [|i ge0_i ih]. + by rewrite BAdd.big_int1 /= !expr0 mul1r bin0 // mulr1z. @@ -210,7 +210,7 @@ realize R.unitP by exact/RField.unitP . realize R.unitout by exact/RField.unitout . lemma binomial (x y : real) n : 0 <= n => (x + y) ^ n = - Bigreal.BRA.bigi predT (fun i => (bin n i)%r * (x ^ i * y ^ (n - i))) 0 (n + 1). + Bigreal.BRA.#bigi [ i : 0, (n + 1) ] ((bin n i)%r * (x ^ i * y ^ (n - i))). proof. move=> ge0_n; have := binomial_r x y n ge0_n => ->. by apply: Bigreal.BRA.eq_bigr=> /= k _; rewrite intmulr mulrC mulrA. diff --git a/theories/algebra/DynMatrix.eca b/theories/algebra/DynMatrix.eca index 8338e31700..688c14e294 100644 --- a/theories/algebra/DynMatrix.eca +++ b/theories/algebra/DynMatrix.eca @@ -27,10 +27,10 @@ import BAdd. (* TOTHINK: This lemma is very useful in mulrxA, other uses? *) lemma big_range0r (j' j i : int) P F : j' <= j => (forall x, j' <= x < j => P x => F x = zeror) => - bigi P F i j = bigi P F i j'. + #bigi [ x : i, j | P x ] (F x) = #bigi [ x : i, j' | P x ] (F x). proof. move => le_j'_j F0E; case (i <= j') => [le_i_j'|gt_i_j']. -- rewrite (big_cat_int j') 1,2:/# [bigi P F j' j]big1_seq ?addr0 //. +- rewrite (big_cat_int j') 1,2:/# [#bigi [ x : j', j | P x ] (F x)]big1_seq ?addr0 //. smt(mem_range). rewrite !big1_seq; smt(mem_range). qed. @@ -266,10 +266,10 @@ proof. smt(addvA addvC addvN addv0). qed. (* Inner product *) op[opaque] dotp (v1 v2 : vector) = - bigi predT (fun i => v1.[i] * v2.[i]) 0 (max (size v1) (size v2)). + #bigi [ i : 0, (max (size v1) (size v2)) ] (v1.[i] * v2.[i]). -lemma dotpE v1 v2: dotp v1 v2 = - bigi predT (fun i => v1.[i] * v2.[i]) 0 (max (size v1) (size v2)). +lemma dotpE v1 v2: dotp v1 v2 = + #bigi [ i : 0, (max (size v1) (size v2)) ] (v1.[i] * v2.[i]). proof. by rewrite /dotp. qed. lemma dotpC : commutative dotp. @@ -294,8 +294,8 @@ lemma dotpDr v1 v2 v3: dotp v1 (v2 + v3) = dotp v1 v2 + dotp v1 v3. proof. rewrite !dotpE size_addv; pose m := max _ (max _ _). (* FIXME: (max _ _) should be precise enough, but this matches m! *) -rewrite -[bigi _ _ 0 (max _ (size v2))](big_range0r _ m); 1,2: smt(getv0E mul0r). -rewrite -[bigi _ _ 0 (max _ (size v3))](big_range0r _ m); 1,2: smt(getv0E mul0r). +rewrite -[#bigi [ i : 0, (max _ (size v2)) | _ ] _](big_range0r _ m); 1,2: smt(getv0E mul0r). +rewrite -[#bigi [ i : 0, (max _ (size v3)) | _ ] _](big_range0r _ m); 1,2: smt(getv0E mul0r). by rewrite sumrD /= &(eq_bigr) /= => i _; rewrite get_addv mulrDr. qed. @@ -592,7 +592,7 @@ by apply size_ineq. qed. lemma dvector1E (d : R distr) (v : vector) : mu1 (dvector d (size v)) v = - BRM.bigi predT (fun i => mu1 d v.[i]) 0 (size v). + BRM.#bigi [ i : 0, (size v) ] (mu1 d v.[i]). proof. rewrite -{2}[v]tolistK dmapE /(\o) /pred1. rewrite (@mu_eq _ _ (pred1 (tolist v))). @@ -1153,15 +1153,15 @@ split => [| i j bound]; 1: smt(rows_mulmx cols_mulmx). rewrite !get_mulmx dotpE /= (big_range0r (rows m2)) 1:/#. - smt(getm0E mulr0 mul0r rows_mulmx cols_mulmx row0E). rewrite (eq_bigr _ _ (fun k => - bigi predT (fun (l : int) => m1.[i,k] * (m2.[k,l] * m3.[l,j])) 0 (rows m3))). + #bigi [ l : 0, (rows m3) ] (m1.[i,k] * (m2.[k,l] * m3.[l,j])))). - move => k /= _. rewrite get_mulmx dotpE mulr_sumr /= (big_range0r (rows m3)) // 1:/#. smt(getm0E mulr0 mul0r). rewrite exchange_big /= dotpE /=. -rewrite [bigi _ _ _ (max _ _)](big_range0r (rows m3)) // 1:/#. +rewrite [#bigi [ i : _, (max _ _) | _ ] _](big_range0r (rows m3)) // 1:/#. - smt(getm0E mulr0 mul0r). apply eq_bigr => k _ /=; rewrite get_mulmx dotpE mulr_suml /=. -rewrite [bigi _ _ _ (max _ _)](big_range0r (rows m2)) 1:/#. +rewrite [#bigi [ i : _, (max _ _) | _ ] _](big_range0r (rows m2)) 1:/#. - smt(getm0E mulr0 mul0r). by apply eq_bigr => l _ /=; rewrite mulrA. qed. @@ -1470,14 +1470,14 @@ rewrite get_catmr 3!get_mulmx. case (j < cols m2) => bound2. - rewrite [col m3 _]col0E 1:/# dotpv0 addr0 !dotpE 2!size_col rows_catmr. rewrite (big_cat_int (max (cols m1) (rows m2))) 1:/# size_row 1:/#. - rewrite [bigi _ _ (max _ _) _]big1_seq => [k [_ /mem_range bound3] /=|]. + rewrite [#bigi [ i : (max _ _), _ | _ ] _]big1_seq => [k [_ /mem_range bound3] /=|]. + by rewrite get_catmr [_ m2 _]getm0E 1:/# add0r [_ m3 _]getm0E 1:/# mulr0. rewrite addr0. apply eq_bigr => k _ /=. by rewrite get_catmr [_ m3 _]getm0E 1:/# addr0. - rewrite [col m2 _]col0E 1:/# dotpv0 add0r !dotpE 2!size_col rows_catmr. rewrite (big_cat_int (max (cols m1) (rows m3))) 1:/# size_row 1:/#. - rewrite [bigi _ _ (max _ _) _]big1_seq => [k [_ /mem_range bound3] /=|]. + rewrite [#bigi [ i : (max _ _), _ | _ ] _]big1_seq => [k [_ /mem_range bound3] /=|]. + by rewrite get_catmr [_ m3 _]getm0E 1:/# addr0 [_ m2 _]getm0E 1:/# mulr0. rewrite addr0. apply eq_bigr => k _ /=. @@ -1823,8 +1823,7 @@ apply size_dmatrix in cont => /#. qed. lemma dmatrix1E d m : mu1 (dmatrix d (rows m) (cols m)) m = - BRM.bigi predT (fun i => - BRM.bigi predT (fun j => mu1 d m.[i, j]) 0 (cols m)) 0 (rows m). + BRM.#bigi [ i : 0, (rows m) ] (BRM.#bigi [ j : 0, (cols m) ] (mu1 d m.[i, j])). proof. pose g (m: matrix) := mkseq (fun i => col m i) (cols m). rewrite (in_dmap1E_can _ _ g) /ofcols. diff --git a/theories/algebra/Ideal.ec b/theories/algebra/Ideal.ec index d938c383bd..c8865f740f 100644 --- a/theories/algebra/Ideal.ec +++ b/theories/algebra/Ideal.ec @@ -94,10 +94,10 @@ move=> ^iI [_ [+ _] Ix Iy] - /(_ x (-y)); rewrite opprK. by apply=> //; apply/idealN. qed. -lemma ideal_sum ['a] I P F s : +lemma ideal_sum ['a] I P (F : 'a -> t) s : ideal I => (forall x, P x => I (F x)) - => I (BAdd.big<:'a> P F s). + => I (BAdd.#big [ i : s | P i ] (F i)). proof. elim: s => [|x s ih] idI IF; first by rewrite BAdd.big_nil ideal0. rewrite BAdd.big_cons; case: (P x) => Px; last by apply/ih. @@ -190,11 +190,11 @@ qed. (* -------------------------------------------------------------------- *) op idgen (xs : t list) = fun (x : t) => - exists cs, x = BAdd.bigi predT (fun i => cs.[i] * xs.[i]) 0 (size xs). + exists cs, x = BAdd.#bigi [ i : 0, (size xs) ] (cs.[i] * xs.[i]). lemma idgenP (xs : t list) (x : t) : idgen xs x => exists cs, size cs = size xs - /\ x = BAdd.bigi predT (fun i => cs.[i] * xs.[i]) 0 (size xs). + /\ x = BAdd.#bigi [ i : 0, (size xs) ] (cs.[i] * xs.[i]). proof. case=> cs ->; exists (mkseq (fun i => cs.[i]) (size xs)); split. - by rewrite size_mkseq ler_maxr // size_ge0. @@ -387,9 +387,9 @@ proof. by rewrite /eqv -idealNP 1:ideal_p opprD. qed. lemma eqvD x1 x2 y1 y2 : eqv x1 x2 => eqv y1 y2 => eqv (x1 + y1) (x2 + y2). proof. by rewrite /eqv subrACA &(idealD) ideal_p. qed. -lemma eqv_sum ['a] P F1 F2 r : +lemma eqv_sum ['a] P (F1 F2 : 'a -> t) r : (forall x, P x => eqv (F1 x) (F2 x)) - => eqv (BAdd.big<:'a> P F1 r) (BAdd.big<:'a> P F2 r). + => eqv (BAdd.#big [ i : r | P i ] (F1 i)) (BAdd.#big [ i : r | P i ] (F2 i)). proof. move=> heqv; elim: r => [|x r ih]. - by rewrite !BAdd.big_nil eqvxx. diff --git a/theories/algebra/IntDiv.ec b/theories/algebra/IntDiv.ec index 8e6f9ef271..6cd629f36c 100644 --- a/theories/algebra/IntDiv.ec +++ b/theories/algebra/IntDiv.ec @@ -367,7 +367,7 @@ lemma modzBm m n d : (m %% d - n %% d) %% d = (m - n) %% d. proof. by rewrite -modzDm -modzNm !modz_mod modzNm modzDm. qed. lemma modz_prodm P F (s : 'a list) d : - (BIM.big P (fun i => F i %% d) s) %% d = BIM.big P F s %% d. + (BIM.#big [ i : s | P i ] (F i %% d)) %% d = BIM.#big [ i : s | P i ] (F i) %% d. proof. elim: s => [|x s ih]; first by rewrite !BIM.big_nil. rewrite !BIM.big_cons; case: (P x) => //. @@ -1201,7 +1201,7 @@ qed. (* -------------------------------------------------------------------- *) lemma Euclide_prod F (s : 'a list) a : - a %| BIM.big predT F s => prime a => + a %| BIM.#big [ i : s ] (F i) => prime a => exists x, x \in s /\ a %| F x. proof. elim: s => [|x s ih]; first by rewrite BIM.big_nil; smt(dvdz_le). @@ -1227,7 +1227,7 @@ have gt0_p: 0 < p by smt(gt1_prime). suff: p %| (fact (p-1) * (exp a (p-1) - 1)). - move/Euclide => /(_ prime_p) -[] // /Euclide_prod /(_ prime_p) /=. by case=> x [] /mem_range rg_x @/idfun; smt(dvdz_le). -rewrite mulrDr mulrN1 eqz_mod_dvd -/N (_ : N = bigi predT (fun i => i * a) 1 p). +rewrite mulrDr mulrN1 eqz_mod_dvd -/N (_ : N = #bigi [ i : 1, p ] (i * a)). - rewrite /N /fact /= BIM.big_split mulr_const; do 2? congr => //. by rewrite size_range /#. move=> {N}; rewrite -modz_prodm /=; do! congr. diff --git a/theories/algebra/Matrix.eca b/theories/algebra/Matrix.eca index 336ecd3f24..bda626dbce 100644 --- a/theories/algebra/Matrix.eca +++ b/theories/algebra/Matrix.eca @@ -120,7 +120,7 @@ lemma offunB (v1 v2 : vector) i : (v1 - v2).[i] = v1.[i] - v2.[i]. proof. done. qed. op dotp (v1 v2 : vector) = - bigi predT (fun i => v1.[i] * v2.[i]) 0 size. + #bigi [ i : 0, size ] (v1.[i] * v2.[i]). lemma dotpC : commutative dotp. proof. @@ -317,7 +317,7 @@ lemma offunB (m1 m2 : matrix) i j : (m1 - m2).[i, j] = m1.[i, j] - m2.[i, j]. proof. done. qed. op trace (m : matrix) = - bigi predT (fun i => m.[i, i]) 0 size. + #bigi [ i : 0, size ] (m.[i, i]). op trmx (m : matrix) = offunm (fun i j => m.[j, i]). @@ -346,10 +346,10 @@ lemma trace_trmx m : trace (trmx m) = trace m. proof. by apply: eq_bigr=> /= i _; rewrite trmxE. qed. op ( * ) (m1 m2 : matrix) = - offunm (fun i j => bigi predT (fun k => m1.[i, k] * m2.[k, j]) 0 size). + offunm (fun i j => #bigi [ k : 0, size ] (m1.[i, k] * m2.[k, j])). lemma offunM (m1 m2 : matrix) i j : - (m1 * m2).[i, j] = bigi predT (fun k => m1.[i, k] * m2.[k, j]) 0 size. + (m1 * m2).[i, j] = #bigi [ k : 0, size ] (m1.[i, k] * m2.[k, j]). proof. case: (mrange i j) => [rg_ij|Nrg_ij]; first by rewrite offunmE. rewrite getm_out // big1 // => /= k _; move: Nrg_ij. @@ -392,7 +392,7 @@ lemma mulmxA : associative Matrix.( * ). proof. move=> m1 m2 m3; apply/eq_matrixP=> i j rg_ij. pose M k l := m1.[i, k] * m2.[k, l] * m3.[l, j]. -pose E := bigi predT (fun k => bigi predT (M k) 0 size) 0 size. +pose E := #bigi [ k : 0, size ] (#bigi [ l : 0, size ] (M k l)). apply: (@eq_trans _ E); rewrite offunM. + apply: eq_bigr=> /= k _; rewrite mulr_sumr &(eq_bigr) /=. by move=> l _; rewrite mulrA. @@ -407,10 +407,10 @@ by apply: eq_bigr => /= k _; rewrite !trmxE mulrC. qed. op ( *^ ) (m : matrix) (v : vector) : vector = - offunv (fun i => bigi predT (fun j => m.[i, j] * v.[j]) 0 size). + offunv (fun i => #bigi [ j : 0, size ] (m.[i, j] * v.[j])). op ( ^* ) (v : vector) (m : matrix) : vector = - offunv (fun j => bigi predT (fun i => v.[i] * m.[i, j]) 0 size). + offunv (fun j => #bigi [ i : 0, size ] (v.[i] * m.[i, j])). lemma mulmxTv (m : matrix) (v : vector) : (trmx m) *^ v = v ^* m. proof. @@ -451,7 +451,7 @@ lemma mulmxvA (m1 m2 : matrix) (v : vector) : proof. apply/eq_vectorP=> i rgi; rewrite !offunvE //=. pose F j k := m1.[i,k] * m2.[k,j] * v.[j]. -pose E := bigi predT (fun j => bigi predT (F j) 0 size) 0 size. +pose E := #bigi [ j : 0, size ] (#bigi [ k : 0, size ] (F j k)). apply: (@eq_trans _ E). + by rewrite /E /F &(eq_bigr) => /= j _; rewrite mulr_suml. rewrite /E /F exchange_big !big_seq &(eq_bigr) /= => j. @@ -481,14 +481,14 @@ lemma mulvmxA (v : vector) (m1 m2 : matrix) : proof. by rewrite -!mulmxTv trmxM mulmxvA. qed. lemma mulmxvE (m : matrix) (v : vector) i : - (m *^ v).[i] = bigi predT (fun j => m.[i, j] * v.[j]) 0 size. + (m *^ v).[i] = #bigi [ j : 0, size ] (m.[i, j] * v.[j]). proof. case: (0 <= i < size) => [rg_i|rgN_i]; first by rewrite offunvE. by rewrite getv_out // big1 //= => j _; rewrite getm_outL // mul0r. qed. lemma mulvmxE (m : matrix) (v : vector) j : - (v ^* m).[j] = bigi predT (fun i => v.[i] * m.[i, j]) 0 size. + (v ^* m).[j] = #bigi [ i : 0, size ] (v.[i] * m.[i, j]). proof. by rewrite -mulmxTv mulmxvE; apply: eq_bigr => /= i _; rewrite trmxE mulrC. qed. @@ -548,7 +548,7 @@ qed. lemma dotp_mulmxv m v1 v2 : dotp (m *^ v1) v2 = dotp v1 (v2 ^* m). proof. pose F i j := m.[i, j] * v1.[j] * v2.[i]. -rewrite /dotp -(eq_bigr _ (fun i => bigi predT (F i) 0 size)) /=. +rewrite /dotp -(eq_bigr _ (fun i => #bigi [ j : 0, size ] (F i j))) /=. + by move=> i _ @/F; rewrite -mulr_suml mulmxvE. rewrite exchange_big &(eq_bigr) => /= i _ @/F. rewrite mulvmxE mulr_sumr &(eq_bigr) => /= j _. @@ -560,7 +560,7 @@ op dvector (d : R distr) = dmap (djoin (nseq size d)) (fun xs => offunv (nth witness xs)). lemma dvector1E (d : R distr) (v : vector) : mu1 (dvector d) v = - BRM.bigi predT (fun i => mu1 d v.[i]) 0 size. + BRM.#bigi [ i : 0, size ] (mu1 d v.[i]). proof. pose g v := mkseq (tofunv v) size; rewrite (@dmap1E_can _ _ g). + move=> {v} @/g v; apply/eq_vectorP=> /= i rgi. @@ -625,7 +625,7 @@ op dmatrix (d : R distr) = )). lemma dmatrix1E (d : R distr) (m : matrix) : mu1 (dmatrix d) m = - BRM.bigi predT (fun i => BRM.bigi predT (fun j => mu1 d m.[i, j]) 0 size) 0 size. + BRM.#bigi [ i : 0, size ] (BRM.#bigi [ j : 0, size ] (mu1 d m.[i, j])). proof. pose g m := mkseq (fun j => mkseq (fun i => tofunm m i j) size) size. rewrite BRM.exchange_big (@dmap1E_can _ _ g). diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index c6632537b7..5525f73015 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -79,7 +79,7 @@ op prepolyD (p q : poly ) = fun i => p.[i] + q.[i]. op prepolyN (p : poly ) = fun i => - p.[i]. op prepolyM (p q : poly) = fun k => - BCA.bigi predT (fun i => p.[i] * q.[k-i]) 0 (k+1). + BCA.#bigi [ i : 0, (k+1) ] (p.[i] * q.[k-i]). op prepolyZ (z : coeff) (p : poly) = fun k => z * p.[k]. @@ -170,7 +170,7 @@ lemma polyDE p q k : (p + q).[k] = p.[k] + q.[k]. proof. by rewrite coeffE 1:ispolyD. qed. lemma polyME p q k : (p * q).[k] = - BCA.bigi predT (fun i => p.[i] * q.[k-i]) 0 (k+1). + BCA.#bigi [ i : 0, (k+1) ] (p.[i] * q.[k-i]). proof. by rewrite coeffE 1:ispolyM. qed. lemma polyMXE p k : (p * X).[k] = p.[k-1]. @@ -416,7 +416,7 @@ proof. by move/lcDl; rewrite addrC. qed. (* -------------------------------------------------------------------- *) lemma polyMEw M p q k : (k <= M)%Int => (p * q).[k] = - BCA.bigi predT (fun i => p.[i] * q.[k-i]) 0 (M+1). + BCA.#bigi [ i : 0, (M+1) ] (p.[i] * q.[k-i]). proof. move=> le_kM; case: (k < 0) => [lt0_k|/lerNgt ge0_k]. + rewrite lt0_coeff // BCA.big_seq BCA.big1 //= => i. @@ -442,14 +442,14 @@ apply: (eq_trans _ _ _ (BCA.eq_big_perm _ _ _ (range 0 (k+1)) _)). qed. lemma polyMEwr M p q k : (k <= M)%Int => (p * q).[k] = - BCA.bigi predT (fun i => p.[k-i] * q.[i]) 0 (M+1). + BCA.#bigi [ i : 0, (M+1) ] (p.[k-i] * q.[i]). proof. rewrite mulpC => /polyMEw ->; apply: BCA.eq_bigr. by move=> i _ /=; rewrite mulrC. qed. lemma polyMEr p q k : (p * q).[k] = - BCA.bigi predT (fun i => p.[k-i] * q.[i]) 0 (k+1). + BCA.#bigi [ i : 0, (k+1) ] (p.[k-i] * q.[i]). proof. by rewrite (@polyMEwr k). qed. lemma mulpA : associative ( * ). @@ -678,8 +678,8 @@ clone include BigComRing with theory CR <- PolyComRing rename [theory] "BAdd" as "PCA" [theory] "BMul" as "PCM". -lemma polysumE ['a] P F s k : - (PCA.big<:'a> P F s).[k] = BCA.big P (fun i => (F i).[k]) s. +lemma polysumE ['a] P (F : 'a -> poly) s k : + (PCA.#big [ i : s | P i ] (F i)).[k] = BCA.#big [ i : s | P i ] ((F i).[k]). proof. elim: s => /= [|x s ih]; first by rewrite poly0E. rewrite !BCA.big_cons -ih PCA.big_cons /=. @@ -687,7 +687,7 @@ by rewrite -polyDE -(fun_if (fun q => q.[k])). qed. lemma polyE (p : poly) : - p = PCA.bigi predT (fun i => p.[i] ** exp X i) 0 (deg p). + p = PCA.#bigi [ i : 0, (deg p) ] (p.[i] ** exp X i). proof. apply/poly_eqP=> c ge0_c; rewrite polysumE /=; case: (c < deg p). - move=> lt_c_dp; rewrite (BCA.bigD1 _ _ c) ?(mem_range, range_uniq) //=. @@ -700,7 +700,7 @@ apply/poly_eqP=> c ge0_c; rewrite polysumE /=; case: (c < deg p). qed. lemma polywE n (p : poly) : deg p <= n => - p = PCA.bigi predT (fun i => p.[i] ** exp X i) 0 n. + p = PCA.#bigi [ i : 0, n ] (p.[i] ** exp X i). proof. move=> le_pn; rewrite (PCA.big_cat_int (deg p)) // ?ge0_deg. rewrite {1}polyE; pose c := PCA.big _ _ _. @@ -709,10 +709,10 @@ rewrite /d PCA.big_seq PCA.big1 => //= i /mem_range [gei _]. by rewrite gedeg_coeff // scale0p. qed. -lemma deg_sum ['a] P F r c : +lemma deg_sum ['a] P (F : 'a -> poly) r c : 0 <= c => (forall x, P x => deg (F x) <= c) - => deg (PCA.big<:'a> P F r) <= c. + => deg (PCA.#big [ i : r | P i ] (F i)) <= c. proof. move=> ge0_c le; elim: r => [|x r ih]; 1: by rewrite PCA.big_nil deg0. rewrite PCA.big_cons; case: (P x) => // Px. @@ -724,7 +724,7 @@ import BigPoly. (* -------------------------------------------------------------------- *) op peval (p : poly) (a : coeff) = - BCA.bigi predT (fun i => p.[i] * exp a i) 0 (deg p + 1). + BCA.#bigi [ i : 0, (deg p + 1) ] (p.[i] * exp a i). (* -------------------------------------------------------------------- *) abbrev root p a = peval p a = Coeff.zeror. diff --git a/theories/algebra/PolyReduce.ec b/theories/algebra/PolyReduce.ec index 7d65744eb0..fc04b69aae 100644 --- a/theories/algebra/PolyReduce.ec +++ b/theories/algebra/PolyReduce.ec @@ -130,20 +130,18 @@ proof. rewrite eqv_sym /eqv /[-] opprK /I mem_idgen1_gen. qed. (* -------------------------------------------------------------------- *) op reduce (p : poly) : poly = - PCA.bigi predT - (fun i => (exp (-Coeff.oner) (i %/ n) * p.[i]) ** exp X (i %% n)) - 0 (deg p). + PCA.#bigi [ i : 0, (deg p) ] + ((exp (-Coeff.oner) (i %/ n) * p.[i]) ** exp X (i %% n)). op reduced (p : poly) = (reduce p = p). (* -------------------------------------------------------------------- *) lemma reducewE k (p : poly) : deg p <= k => - reduce p = PCA.bigi predT - (fun i => (exp (-Coeff.oner) (i %/ n) * p.[i]) ** exp X (i %% n)) - 0 k. + reduce p = PCA.#bigi [ i : 0, k ] + ((exp (-Coeff.oner) (i %/ n) * p.[i]) ** exp X (i %% n)). proof. move=> len; rewrite (PCA.big_cat_int (deg p)) ?ge0_deg // /reduce. -pose c := big _ _ _; rewrite PCA.big_seq PCA.big1 /= ?addr0 //. +pose c := PCA.#big [ i : _ | _ ] _; rewrite PCA.big_seq PCA.big1 /= ?addr0 //. by move=> i /mem_range [gei _]; rewrite gedeg_coeff // mulr0 scale0p. qed. @@ -327,7 +325,7 @@ qed. (* -------------------------------------------------------------------- *) lemma reduced_sum ['a] (P : 'a -> bool) (F : 'a -> poly) (r : 'a list) : - (forall i, P i => reduced (F i)) => reduced (PCA.big P F r). + (forall i, P i => reduced (F i)) => reduced (PCA.#big [ i : r | P i ] (F i)). proof. move=> red; elim: r => [|x r ih]; 1: by rewrite big_nil reduced0. by rewrite big_cons; case: (P x) => // Px; rewrite reducedD // &(red). @@ -335,7 +333,7 @@ qed. (* -------------------------------------------------------------------- *) lemma rcoeff_sum ['a] (P : 'a -> bool) (F : 'a -> polyXnD1) (r : 'a list) k : - (XnD1CA.big P F r).[k] = BCA.big P (fun i => (F i).[k]) r. + (XnD1CA.#big [ i : r | P i ] (F i)).[k] = BCA.#big [ i : r | P i ] ((F i).[k]). proof. elim: r => [|x r ih]. - by rewrite XnD1CA.big_nil BCA.big_nil rcoeff0. @@ -345,7 +343,7 @@ qed. (* -------------------------------------------------------------------- *) lemma polyXnD1_sumN ['a] (P : 'a -> bool) (F : 'a -> polyXnD1) (r : 'a list) : - - (XnD1CA.big P F r) = (XnD1CA.big P (fun i => - (F i)) r). + - (XnD1CA.#big [ i : r | P i ] (F i)) = (XnD1CA.#big [ i : r | P i ] (- (F i))). proof. rewrite XnD1CA.big_endo //. + by rewrite ComRingDflInv.oppr0. @@ -384,9 +382,9 @@ move => rng_i; rewrite eq_expiXn_expXn 1:rng_i piK 1:reducedXn 2:polyXnE //#. qed. (* -------------------------------------------------------------------- *) -lemma rcoeffZ_sum (F : int -> coeff) (k : int) : +lemma rcoeffZ_sum (F : int -> coeff) (k : int) : 0 <= k < n => - (XnD1CA.bigi predT (fun i => (F i) ** ComRingDflInv.exp iX i) 0 n).[k] = F k. + (XnD1CA.#bigi [ i : 0, n ] ((F i) ** ComRingDflInv.exp iX i)).[k] = F k. proof. move => rng_k; rewrite rcoeff_sum (BCA.bigD1 _ _ k) /=. + by rewrite mem_range. @@ -398,15 +396,15 @@ qed. (* -------------------------------------------------------------------- *) lemma rcoeffM (p q : polyXnD1) k : 0 <= k < n => (p * q).[k] = - BCA.bigi predT (fun i => - p.[i] * q.[k - i] - p.[i] * q.[n + k - i]) 0 n. + BCA.#bigi [ i : 0, n ] + (p.[i] * q.[k - i] - p.[i] * q.[n + k - i]). proof. case=> ge0_k le_kn; elim/polyXnD1W: p => p rdp; elim/polyXnD1W: q => q rdq. rewrite mulE {1}/crepr; pose r := reduce _; have ->: r = reduce (p * q). - by apply/reduce_eqP/eqv_repr. rewrite (polywE n (reduce (p * q))) 1:&(deg_reduce). rewrite (PCA.bigD1 _ _ k) ?(mem_range, range_uniq) /= 1:/#. -rewrite polyDE; pose c := (bigi _ _ _ _); have ->: c.[k] = Coeff.zeror. +rewrite polyDE; pose c := (PCA.#bigi [ i : _, _ | _ ] _); have ->: c.[k] = Coeff.zeror. - rewrite /c polysumE BCA.big_seq_cond BCA.big1 ?addr0 //=. move=> i [/mem_range [ge0_i lt_in] @/predC1 ne_ik]. by rewrite polyZE polyXnE // (eq_sym k i) ne_ik /= mulr0. diff --git a/theories/algebra/StdBigop.ec b/theories/algebra/StdBigop.ec index c3c9821ddf..2733b5eb8e 100644 --- a/theories/algebra/StdBigop.ec +++ b/theories/algebra/StdBigop.ec @@ -23,7 +23,7 @@ clone include Bigop with proof Support.Axioms.* by smt(). lemma bigP (P F : 'a -> bool) (xs : 'a list): - big P F xs <=> has F (filter P xs). + #big [ i : xs | P i ] (F i) <=> has F (filter P xs). proof. elim: xs=> //= x xs ih. rewrite big_cons; case: (P x)=> //=. @@ -40,7 +40,7 @@ clone include Bigop with proof Support.Axioms.* by smt(). lemma bigP (P F : 'a -> bool) (xs : 'a list): - big P F xs <=> all F (filter P xs). + #big [ i : xs | P i ] (F i) <=> all F (filter P xs). proof. elim: xs=> //= x xs ih. rewrite big_cons; case: (P x)=> //=. @@ -79,20 +79,20 @@ clone include Bigalg.BigOrder with remove abbrev Num.Domain.(-) remove abbrev Num.Domain.(/). -lemma sumzE ss : sumz ss = BIA.big predT (fun x => x) ss. +lemma sumzE ss : sumz ss = BIA.#big [ x : ss ] x. proof. by elim: ss=> [|s ss ih] //=; rewrite BIA.big_cons -ih. qed. lemma big_constz (P : 'a -> bool) x s: - BIA.big P (fun i => x) s = x * (count P s). + BIA.#big [ i : s | P i ] x = x * (count P s). proof. by rewrite BIA.sumr_const -IntID.intmulz. qed. lemma bigi_constz x (n m:int): n <= m => - BIA.bigi predT (fun i => x) n m = x * (m - n). + BIA.#bigi [ _ : n, m ] x = x * (m - n). proof. by move=> ?; rewrite BIA.sumri_const // -IntID.intmulz. qed. lemma big_count (P : 'a -> bool) s: - BIA.big P (fun (x : 'a) => count (pred1 x) s) (undup s) + BIA.#big [ x : (undup s) | P x ] (count (pred1 x) s) = size (filter P s). proof. rewrite size_filter -(mul1r (count _ _)) -big_constz. @@ -105,7 +105,7 @@ case: (P x)=> [Px|NPx]; last rewrite count_pred0_eq //. + by move=> y @/predI @/pred1; case: (y = x). qed. -abbrev sumid i j = BIA.bigi predT (fun n => n) i j. +abbrev sumid i j = BIA.#bigi [ n : i, j ] n. lemma sumidE_r n : 0 <= n => 2 * sumid 0 n = (n * (n - 1)). @@ -150,66 +150,66 @@ clone include Bigalg.BigOrder with import Bigint.BIA Bigint.BIM BRA BRM. lemma sumr_ofint (P : 'a -> bool) F s : - (Bigint.BIA.big P F s)%r = (BRA.big P (fun i => (F i)%r) s). + (Bigint.BIA.#big [ i : s | P i ] (F i))%r = (BRA.#big [ i : s | P i ] ((F i)%r)). proof. elim: s => [//|x s ih]; rewrite !big_cons; case: (P x)=> // _. by rewrite fromintD ih. qed. lemma prodr_ofint (P : 'a -> bool) F s : - (Bigint.BIM.big P F s)%r = (BRM.big P (fun i => (F i)%r) s). + (Bigint.BIM.#big [ i : s | P i ] (F i))%r = (BRM.#big [ i : s | P i ] ((F i)%r)). proof. elim: s => [//|x s ih]; rewrite !big_cons; case: (P x)=> // _. by rewrite fromintM ih. qed. lemma sumr_const (P : 'a -> bool) (x : real) (s : 'a list): - BRA.big P (fun (i : 'a) => x) s = (count P s)%r * x. + BRA.#big [ i : s | P i ] x = (count P s)%r * x. proof. by rewrite sumr_const RField.intmulr RField.mulrC. qed. lemma sumri_const (x : real) (n m : int): - n <= m => - BRA.bigi predT (fun _ => x) n m = (m - n)%r * x. + n <= m => + BRA.#bigi [ _ : n, m ] x = (m - n)%r * x. proof. by move=> ?; rewrite sumri_const // RField.intmulr RField.mulrC. qed. lemma sumr1 (s : 'a list) : - BRA.big predT (fun i => 1%r) s = (size s)%r. + BRA.#big [ _ : s ] 1%r = (size s)%r. proof. by rewrite sumr_const count_predT RField.mulr1. qed. lemma sumr1_int (n : int) : 0 <= n => - BRA.bigi predT (fun i => 1%r) 0 n = n%r. + BRA.#bigi [ _ : 0, n ] 1%r = n%r. proof. by move=> ge0_n; rewrite sumr1 size_range ler_maxr. qed. lemma sumidE n : 0 <= n => - BRA.bigi predT (fun i => i%r) 0 n = (n * (n - 1))%r / 2%r. + BRA.#bigi [ i : 0, n ] (i%r) = (n * (n - 1))%r / 2%r. proof. move=> ge0_n; rewrite -sumr_ofint -sumidE_r //. by rewrite fromintM mulrAC divff. qed. lemma sumr_undup ['a] (P : 'a -> bool) (F : 'a -> real) s : - BRA.big P F s = BRA.big P (fun a => (count (pred1 a) s)%r * (F a)) (undup s). + BRA.#big [ a : s | P a ] (F a) = BRA.#big [ a : (undup s) | P a ] ((count (pred1 a) s)%r * (F a)). proof. rewrite BRA.sumr_undup; apply/BRA.eq_bigr=> x _ /=. by rewrite intmulr mulrC. qed. lemma sum_pow (p : real) (n : int) : 0 <= n => p <> 1%r => - BRA.bigi predT (fun i => p^i) 0 n = (1%r - p^n) / (1%r - p). + BRA.#bigi [ i : 0, n ] (p^i) = (1%r - p^n) / (1%r - p). proof. move=> ge0_n neq1_p; have <- := sum_expr p n ge0_n. by rewrite mulrAC divff 1:/#. qed. lemma sum_pow_le (p : real) (n : int) : 0 <= n => 0%r <= p < 1%r => - BRA.bigi predT (fun i => p^i) 0 n <= 1%r / (1%r - p). + BRA.#bigi [ i : 0, n ] (p^i) <= 1%r / (1%r - p). proof. move=> ge0_n rg_p; have h := sum_expr_le p n ge0_n rg_p. by rewrite &(RealOrder.ler_pdivl_mulr) 1:/# mulrC. qed. lemma sum_ipow_le (p : real) (n : int) : 0%r <= p < 1%r => - BRA.bigi predT (fun (i:int) => i%r*p^i) 0 n <= 1%r / (1%r - p)^2. + BRA.#bigi [ i : 0, n ] (i%r*p^i) <= 1%r / (1%r - p)^2. proof. move=> rg_p; have h := sum_iexpr_le p n rg_p. rewrite &(RealOrder.ler_pdivl_mulr) -1:mulrC //. @@ -241,7 +241,7 @@ clone include Bigop with proof Support.Axioms.* by (delta; smt()). lemma bigP (P : 'a -> bool) (s : 'a list): - big predT P s <=> (forall a, mem s a => P a). + #big [ a : s ] (P a) <=> (forall a, mem s a => P a). proof. elim: s => [|x s ih] //=; rewrite !big_cons {1}/predT /=. rewrite ih; split=> [[Px h] y [->|/h]|h] //. @@ -258,7 +258,7 @@ clone include Bigop with proof Support.Axioms.* by (delta; smt()). lemma bigP (P : 'a -> bool) (s : 'a list): - big predT P s <=> (exists a, mem s a /\ P a). + #big [ a : s ] (P a) <=> (exists a, mem s a /\ P a). proof. elim: s => [|x s ih] //=; rewrite big_cons /predT /=. rewrite ih; case: (P x)=> Px /=; first by exists x. @@ -268,7 +268,7 @@ split; case=> y [sy ^Py /h ne_yx]; exists y. qed. lemma b2i_big (P1 P2 : 'a -> bool) (s : 'a list) : - b2i (big P1 P2 s) <= BIA.big P1 (fun i => b2i (P2 i)) s. + b2i (#big [ i : s | P1 i ] (P2 i)) <= BIA.#big [ i : s | P1 i ] (b2i (P2 i)). proof. elim: s => [|x s ih] //=; rewrite big_cons BIA.big_cons. case: (P1 x)=> //= P1x; rewrite oraE b2i_or. @@ -277,7 +277,7 @@ by rewrite -b2i_and b2i_ge0. qed. lemma b2r_big (P1 P2 : 'a -> bool) (s : 'a list) : - b2r (big P1 P2 s) <= BRA.big P1 (fun i => b2r (P2 i)) s. + b2r (#big [ i : s | P1 i ] (P2 i)) <= BRA.#big [ i : s | P1 i ] (b2r (P2 i)). proof. rewrite b2rE (BRA.eq_bigr _ _ (fun i => (b2i (P2 i))%r)). by move=> x _ /=; rewrite b2rE. diff --git a/theories/analysis/RealExp.ec b/theories/analysis/RealExp.ec index b99a51e998..7b4be49cc8 100644 --- a/theories/analysis/RealExp.ec +++ b/theories/analysis/RealExp.ec @@ -401,14 +401,14 @@ require import StdBigop. (*---*) import Bigreal BRA BRM. lemma exp_sum (P : 'a -> bool) (F : 'a -> real) s: - exp (BRA.big P F s) = BRM.big P (fun a => exp (F a)) s. + exp (BRA.#big [ a : s | P a ] (F a)) = BRM.#big [ a : s | P a ] (exp (F a)). proof. elim: s => [|x s ih]; rewrite !(big_nil, big_cons) ?exp0 //. by case: (P x)=> // Px; rewrite expD ih. qed. lemma rpowe_sum (P : 'a -> bool) (F : 'a -> real) s: - e^(BRA.big P F s) = BRM.big P (fun a => e^(F a)) s. + e^(BRA.#big [ a : s | P a ] (F a)) = BRM.#big [ a : s | P a ] (e^(F a)). proof. by rewrite rpoweE exp_sum; apply/eq_bigr=> x _ /=; rewrite rpoweE. qed. (* -------------------------------------------------------------------- *) @@ -733,14 +733,14 @@ realize ZM.add0r by exact/add0r. realize ZM.addNr by exact/addNr. lemma dotp_sumr ['a] P F (s : 'a list) x : - dotp x (big P F s) = BRA.big P (fun y => dotp x (F y)) s. + dotp x (#big [ y : s | P y ] (F y)) = BRA.#big [ y : s | P y ] (dotp x (F y)). proof. elim: s => [|y s ih]; first by rewrite !big_nil dotpv0. by rewrite !big_cons; case: (P y) => // _; rewrite dotpDr ih. qed. lemma dotp_suml ['a] P F (s : 'a list) x : - dotp (big P F s) x = BRA.big P (fun y => dotp (F y) x) s. + dotp (#big [ y : s | P y ] (F y)) x = BRA.#big [ y : s | P y ] (dotp (F y) x). proof. by rewrite dotpC dotp_sumr; apply: BRA.eq_bigr => i _ /=; rewrite dotpC. qed. diff --git a/theories/analysis/RealSeq.ec b/theories/analysis/RealSeq.ec index e2120d0b85..e0d85b64bc 100644 --- a/theories/analysis/RealSeq.ec +++ b/theories/analysis/RealSeq.ec @@ -476,16 +476,16 @@ lemma convergeto_sum : (forall x, P x => convergeto (F x) (l x)) => convergeto - (fun n => big P (fun x => (F x n)) s) - (big P (fun x => l x) s). + (fun n => #big [ x : s | P x ] (F x n)) + (#big [ x : s | P x ] (l x)). proof. move=> cvg; elim: s => /= [|x s ih]. - by rewrite !big_nil &(@eq_cnvto (fun _ => 0%r)) //= &(cnvtoC). rewrite big_cons; case: (P x) => [Px|NPx]; last first. -- rewrite &(@eq_cnvto (fun n => big P (fun y => F y n) s)) /=. +- rewrite &(@eq_cnvto (fun n => #big [ y : s | P y ] (F y n))) /=. - by move=> n; rewrite big_cons NPx. - apply: ih. -pose G (n : int) := F x n + big P (fun y => F y n) s. +pose G (n : int) := F x n + #big [ y : s | P y ] (F y n). rewrite &(eq_cnvto G) => /= [n|]. - by rewrite /G big_cons Px. by apply: cnvtoD => //; apply: cvg. @@ -497,9 +497,9 @@ lemma converge_sum (s : 'a list) : (forall x, P x => converge (F x)) - => converge (fun n => big P (fun x => (F x n)) s). + => converge (fun n => #big [ x : s | P x ] (F x n)). proof. -move=> cvg; pose l := big P (fun x => lim (F x)) s. +move=> cvg; pose l := #big [ x : s | P x ] (lim (F x)). apply/(cnvP l)/convergeto_sum => /= x Px. by apply/limP/cvg. qed. @@ -510,8 +510,8 @@ lemma lim_sum (s : 'a list) : (forall x, P x => converge (F x)) - => big P (fun x => lim (F x)) s - = lim (fun n => big P (fun x => F x n) s). + => #big [ x : s | P x ] (lim (F x)) + = lim (fun n => #big [ x : s | P x ] (F x n)). proof. move=> cvg; pose l := fun x => lim (F x). have {cvg}cvg: forall x, P x => convergeto (F x) (l x). diff --git a/theories/analysis/RealSeries.ec b/theories/analysis/RealSeries.ec index ac61c29b7d..1e722a49ef 100644 --- a/theories/analysis/RealSeries.ec +++ b/theories/analysis/RealSeries.ec @@ -8,7 +8,7 @@ pragma +implicits. (* -------------------------------------------------------------------- *) op partial (s : int -> real) (n : int) : real = - bigi predT s 0 n. + #bigi [ i : 0, n ] (s i). op convergeto (s : int -> real) (x : real) = RealSeq.convergeto (partial s) x. @@ -19,7 +19,7 @@ op converge (s : int -> real) = (* -------------------------------------------------------------------- *) op summable (s : 'a -> real) = exists M, forall J, - uniq J => big predT (fun i => `|s i|) J <= M. + uniq J => #big [ i : J ] `|s i| <= M. (* -------------------------------------------------------------------- *) lemma sbl_countable (s : 'a -> real) : @@ -38,9 +38,9 @@ have fin_E: forall i, countable (E i); 1: (move=> i; apply/cnt_finite). - rewrite &(IntOrder.ler_trans i) 1:ltrW // ler_pmulr //. by rewrite ler_addr &(leup_intp) ltrW. case/(@NfiniteP n _ ge0_n) => J [[szJ uqJ] memJ]. - have := sbl_s _ uqJ; pose S := big _ _ _; move=> leSM. + have := sbl_s _ uqJ; pose S := #big [ i : _ | _ ] _; move=> leSM. suff: M < S by apply: (ler_lt_trans _ leSM). - apply/(@ltr_le_trans (big predT (fun _ => 1%r / i%r) J)); last first. + apply/(@ltr_le_trans (#big [ _ : J ] (1%r / i%r))); last first. - by rewrite /S !big_seq; apply/ler_sum=> x /= Px; apply/memJ. rewrite sumr_const intmulr count_predT mulrAC /=. apply/(ltr_le_trans (n%r / i%r)); last first. @@ -85,13 +85,13 @@ qed. lemma summable_from_bounded (s : 'a -> real) : forall (J : int -> 'a option), enumerate J (support s) - => (exists M, forall n, big predT (fun a => `|s a|) (pmap J (range 0 n)) <= M) + => (exists M, forall n, #big [ a : (pmap J (range 0 n)) ] `|s a| <= M) => summable s. proof. move=> J enm [M hb]; exists M => l hl. have [n hn] := enumerate_pmap_range J l (support s) enm. pose I := pmap J (range 0 n). -apply: (ler_trans (big predT (fun (a : 'a) => `|s a|) I)); last by apply hb. +apply: (ler_trans (#big [ a : I ] `|s a|)); last by apply hb. rewrite (@big_eq_idm_filter (support s)); 1:smt(). rewrite (@partition_big (fun x => x) _ predT _ _ I). + apply: pmap_inj_in_uniq; last by apply range_uniq. @@ -116,7 +116,7 @@ lemma eqL_notin_summable (I : 'a list) (s1 s2 : 'a -> real) : (forall x, !x \in I => s1 x = s2 x) => summable s1 => summable s2. proof. move => eq_J_s1_s2 [M sum_s1]. -pose R := big predT (fun x => `|s2 x|) (undup I). +pose R := #big [ x : (undup I) ] `|s2 x|. exists (M+R) => J uniq_J. rewrite (@bigEM (mem I)) addrC &(ler_add). - rewrite (@eq_bigr _ _ (fun x => `|s1 x|)) //= 1:/#. @@ -164,12 +164,12 @@ qed. (* -------------------------------------------------------------------- *) lemma summable_big ['a 'b] (F : 'a -> 'b -> real) (s : 'b list) : (forall y, y \in s => summable (fun x => F x y)) - => summable (fun x => big predT (F x) s). + => summable (fun x => #big [ y : s ] (F x y)). proof. elim: s => [|y s ih] sm; first by apply: (eqL_summable _ summable0). have sm1: summable (fun x => F x y). + by apply: sm; rewrite in_cons. -have sm2: summable (fun x => big predT (F x) s). +have sm2: summable (fun x => #big [ y : s ] (F x y)). + by apply: ih => z z_in_s; rewrite &(sm) in_cons z_in_s. apply: (eqL_summable _ (summableD sm1 sm2)) => /=. by move=> x; rewrite big_cons. @@ -203,7 +203,7 @@ qed. (* -------------------------------------------------------------------- *) lemma summableM_prod_dep ['a 'b] f g: summable<:'a> f - => (exists Mg, forall a J, uniq J => big predT ("`|_|"%Real \o g a) J <= Mg) + => (exists Mg, forall a J, uniq J => #big [ b : J ] (("`|_|"%Real \o g a) b) <= Mg) => summable (fun (ab : 'a * 'b) => f ab.`1 * g ab.`1 ab.`2). proof. case=> [Mf smf] [Mg smg]; exists (Mf * Mg) => J uqJ. @@ -211,7 +211,7 @@ pose J1 := undup (unzip1 J). pose F (ab : 'a * 'b) := `|f ab.`1| * `|g ab.`1 ab.`2|. rewrite (@eq_bigr _ _ F) /= => [ab _|]; 1: by rewrite normrM. rewrite /F (@sum_pair_dep ("`|_|"%Real \o f) ("`|_|"%Real \o2 g)) //=. -apply: (@ler_trans (big predT (fun i => `|f i| * Mg) J1)); last first. +apply: (@ler_trans (#big [ i : J1 ] (`|f i| * Mg))); last first. + rewrite -mulr_suml ler_wpmul2r; 1: by apply: (@smg witness [] _). by apply/smf/undup_uniq. apply: ler_sum => /= a _; rewrite ler_wpmul2l 1:normr_ge0. @@ -300,20 +300,20 @@ qed. (* -------------------------------------------------------------------- *) lemma summable_pos (s : 'a -> real) : summable s => summable (pos s). proof. -case=> M leM; exists M=> J /leM; (pose F := big _ _ _) => le. +case=> M leM; exists M=> J /leM; (pose F := #big [ i : _ | _ ] _) => le. by apply(ler_trans F)=> // @/F; apply/ler_sum=> a _; apply/abs_pos_ler. qed. lemma summable_neg (s : 'a -> real) : summable s => summable (neg s). proof. -case=> M leM; exists M=> J /leM; (pose F := big _ _ _) => le. +case=> M leM; exists M=> J /leM; (pose F := #big [ i : _ | _ ] _) => le. by apply(ler_trans F)=> // @/F; apply/ler_sum=> a _; apply/abs_neg_ler. qed. (* -------------------------------------------------------------------- *) lemma summable_has_lub (s : 'a -> real) : summable s => has_lub (fun M => - exists J, uniq J /\ M = big predT (fun x => `|s x|) J). + exists J, uniq J /\ M = #big [ x : J ] `|s x|). proof. case=> M hM; split; first by exists 0%r []; rewrite big_nil. by exists M => x [J [uqJ ->]]; apply/hM. @@ -321,7 +321,7 @@ qed. (* -------------------------------------------------------------------- *) op psum_pred (s : 'a -> real) = - fun M => exists J, uniq J /\ M = big predT (fun x => `|s x|) J. + fun M => exists J, uniq J /\ M = #big [ x : J ] `|s x|. lemma nz_psum_pred (s : 'a -> real) : nonempty (psum_pred s). proof. by exists 0%r; exists []. qed. @@ -397,10 +397,10 @@ lemma summable_pos_cnvto s : => support s <= p => summable s => RealSeq.convergeto - (fun n => big predT (fun x => `|s x|) (pmap J (range 0 n))) + (fun n => #big [ x : (pmap J (range 0 n)) ] `|s x|) (psum s). proof. -move=> J p enm sm sbl; pose u n := big predT _ (pmap J (range 0 n)). +move=> J p enm sm sbl; pose u n := #big [ i : (pmap J (range 0 n)) ] _. have uqJ: forall n, uniq (pmap J (range 0 n)). + move=> n; rewrite pmap_inj_in_uniq ?range_uniq //. by move=> x y v _ _; case: enm => + _; apply. @@ -466,10 +466,10 @@ lemma summable_cnvto s : enumerate J p => support s <= p => summable s - => RealSeq.convergeto (fun n => big predT s (pmap J (range 0 n))) (sum s). + => RealSeq.convergeto (fun n => #big [ x : (pmap J (range 0 n)) ] (s x)) (sum s). proof. move=> J p enm sm sbl; rewrite /sum sbl /=. -pose G f n := big predT f (pmap J (range 0 n)). +pose G f n := #big [ x : (pmap J (range 0 n)) ] (f x). rewrite -/(G s); have ->: G s = fun n => G (fun x => `|pos s x|) n - G (fun x => `|neg s x|) n. + apply/fun_ext=> i @/G; rewrite sumrB; apply/eq_bigr. @@ -489,7 +489,7 @@ lemma summable_cnv s : enumerate J p => support s <= p => summable s - => RealSeq.converge (fun n => big predT s (pmap J (range 0 n))). + => RealSeq.converge (fun n => #big [ x : (pmap J (range 0 n)) ] (s x)). proof. by move=> J P enm sm sbl; have /cnvP := summable_cnvto _ _ _ enm sm sbl. qed. @@ -500,7 +500,7 @@ lemma sumEw (s : 'a -> real) : enumerate J p => support s <= p => summable s - => sum s = lim (fun n => big predT s (pmap J (range 0 n))). + => sum s = lim (fun n => #big [ x : (pmap J (range 0 n)) ] (s x)). proof. by move=> J p enm le sm; have /lim_cnvto <- := summable_cnvto _ _ _ enm le sm. qed. @@ -510,12 +510,12 @@ lemma sumE (s : 'a -> real) : forall (J : int -> 'a option), enumerate J (support s) => summable s - => sum s = lim (fun n => big predT s (pmap J (range 0 n))). + => sum s = lim (fun n => #big [ x : (pmap J (range 0 n)) ] (s x)). proof. by move=> J /(@sumEw s J (support s)); apply. qed. (* -------------------------------------------------------------------- *) lemma sumEc (s : 'a -> real) : summable s => sum s = - lim (fun n => big predT s (pmap (cenum (support s)) (range 0 n))). + lim (fun n => #big [ x : (pmap (cenum (support s)) (range 0 n)) ] (s x)). proof. by move=> ^sns; apply/sumE/enum_cenum/sbl_countable. qed. (* -------------------------------------------------------------------- *) @@ -529,7 +529,7 @@ qed. lemma sumE_fin ['a] (s : 'a -> real) (J : 'a list) : uniq J => (forall x, s x <> 0%r => mem J x) - => sum s = big predT s J. + => sum s = #big [ x : J ] (s x). proof. move=> uqJ sJ; rewrite (@sumE _ (nth None (map Some J))); 1: split. + move=> i j x /=; pose n := size J; case: (0 <= i < n); last first. @@ -539,7 +539,7 @@ move=> uqJ sJ; rewrite (@sumE _ (nth None (map Some J))); 1: split. by move/(congr1 (fun x => index x J))=> /=; rewrite !index_uniq. + move=> x /sJ sx; exists (index x J); rewrite ?index_ge0 /=. by rewrite (@nth_map x) /= 1:index_ge0 1:index_mem // nth_index. -+ exists (big predT (fun x => `|s x|) (filter (fun x => s x <> 0%r) J))=> J' uniq_J'. ++ exists (#big [ x : (filter (fun x => s x <> 0%r) J) ] `|s x|)=> J' uniq_J'. rewrite -(eq_big_perm (:@perm_filterC (fun x => s x <> 0%r) J')). rewrite big_cat (@big1_seq _ _ (filter (fun (x : 'a) => s x = 0%r) J')) /=. * by move=> x @/predT; rewrite mem_filter /= =>- [] ->. @@ -562,7 +562,7 @@ qed. (* -------------------------------------------------------------------- *) lemma fin_sum_cond (P : 't -> bool) f : is_finite P => - sum (fun z => if P z then f z else 0%r) = big predT f (to_seq P). + sum (fun z => if P z then f z else 0%r) = #big [ x : (to_seq P) ] (f x). proof. move=> P_finite; rewrite (@sumE_fin _ (to_seq P)) /= ?uniq_to_seq //. - smt(mem_to_seq). @@ -578,8 +578,8 @@ by rewrite fin_sum_cond // sumr_const RField.intmulr count_predT RField.mulrC. qed. lemma fin_sum_type (s : 'a -> real) : - is_finite predT<:'a> => - sum s = big predT s (to_seq predT<:'a>). + is_finite predT<:'a> => + sum s = #big [ x : (to_seq predT<:'a>) ] (s x). proof. move=> fint; rewrite &(sumE_fin) 1:uniq_to_seq. by move=> x _; rewrite mem_to_seq. @@ -596,12 +596,12 @@ proof. by rewrite (@sumE_fin _ [true; false]) //= => -[]. qed. (* -------------------------------------------------------------------- *) lemma lerfin_sum (s : 'a -> real) M: summable s - => (forall J, uniq J => big predT s J <= M) + => (forall J, uniq J => #big [ x : J ] (s x) <= M) => sum s <= M. proof. move=> ^/sum_to_enum[J en_sJ] sm_s le_sM. have := summable_cnvto _ _ _ en_sJ _ sm_s => //. -(pose F n := big predT s (pmap J (range 0 n))) => cnv. +(pose F n := #big [ x : (pmap J (range 0 n)) ] (s x)) => cnv. apply: (@le_cnvto_from F (fun _ => M) _ _ _ cnv) => /=; last first. + by apply/cnvtoC. + by exists 0 => n _; apply/le_sM/(enum_uniq_pmap_range _ en_sJ). @@ -616,14 +616,14 @@ proof. move=> inj_h le_s12 ^sbl_s2 [M2 bs2]; have ^sbl_s1 [M1 bs1]: summable s1. + exists M2 => J uqJ; pose K := map h J; have: uniq K. * by apply: map_inj_in_uniq; first by move=> x y _ _ /inj_h. - move/bs2; (pose F := big _ _ _) => leFM. + move/bs2; (pose F := #big [ i : _ | _ ] _) => leFM. rewrite (ler_trans F) // /F big_map; apply/ler_sum. by move=> a _ /=; apply/le_s12. apply/ler_lub; first last; first split. + by exists 0%r []=> /=; apply/eq_sym/(@big_nil _ _). + by exists M2=> x [J] [+ ->] - /bs2. + by exists 0%r []=> /=; apply/eq_sym/(@big_nil _ _). -move=> x [J] [uqJ ->] /=; exists (big predT (fun x => `|s2 x|) (map h J)). +move=> x [J] [uqJ ->] /=; exists (#big [ x : (map h J) ] `|s2 x|). split; [exists (map h J) => /= | by rewrite big_map &(ler_sum)]. by apply: map_inj_in_uniq; first by move=> 4? /inj_h. qed. @@ -803,8 +803,8 @@ qed. (* -------------------------------------------------------------------- *) lemma sum_big ['a 'b] (F : 'a -> 'b -> real) (s : 'b list) : (forall y, y \in s => summable (fun x => F x y)) - => sum (fun x => big predT (F x) s) - = big predT (fun y => sum (fun x => F x y)) s. + => sum (fun x => #big [ y : s ] (F x y)) + = #big [ y : s ] (sum (fun x => F x y)). proof. elim: s => [|y s ih] sm; first by rewrite big_nil sum0. rewrite big_cons /predT /= -ih -?sumD /=. @@ -817,8 +817,8 @@ qed. (* -------------------------------------------------------------------- *) lemma psum_big ['a 'b] (F : 'a -> 'b -> real) (s : 'b list) : (forall y, y \in s => summable (fun x => F x y)) - => psum (fun x => big predT (fun y => `|F x y|) s) - = big predT (fun y => psum (fun x => F x y)) s. + => psum (fun x => #big [ y : s ] `|F x y|) + = #big [ y : s ] (psum (fun x => F x y)). proof. move=> sms; rewrite psum_sum. + by apply/summable_big=> b bs /=; apply/summable_norm/sms. @@ -830,7 +830,7 @@ qed. (* -------------------------------------------------------------------- *) lemma ler_psum_lub ['a] (s : 'a -> real) z : - (forall J, uniq J => big predT (fun x => `|s x|) J <= z) + (forall J, uniq J => #big [ x : J ] `|s x| <= z) => psum s <= z. proof. move=> le; have sm: summable s by exists z. @@ -847,15 +847,15 @@ qed. (* -------------------------------------------------------------------- *) lemma ler_big_psum ['a] s J : summable<:'a> s => uniq J => - big predT (fun x => `|s x|) J <= psum s. + #big [ x : J ] `|s x| <= psum s. proof. move=> sms uqJ @/psum; apply: lub_upper_bound. by apply: summable_has_lub. by exists J. qed. -lemma ler_big_sum (s : 'a -> real) (J : 'a list) : - (forall x, 0%r <= s x) => uniq J => summable s => - big predT s J <= sum s. +lemma ler_big_sum (s : 'a -> real) (J : 'a list) : + (forall x, 0%r <= s x) => uniq J => summable s => + #big [ x : J ] (s x) <= sum s. proof. move => *; rewrite (@sum_split _ (mem J)) //. apply ler_paddr; 1: smt(ge0_sum). @@ -865,7 +865,7 @@ qed. (* -------------------------------------------------------------------- *) lemma summable_psum_partition ['a 'b] (f : 'a -> 'b) s : summable<:'a> s => forall J, uniq J => - big predT (fun b => psum (fun a => if b = f a then s a else 0%r)) J <= psum s. + #big [ b : J ] (psum (fun a => if b = f a then s a else 0%r)) <= psum s. proof. move=> sms J uqJ; rewrite -psum_big /=. by move=> b _; apply/summable_cond. @@ -882,7 +882,7 @@ lemma psum_partition ['a 'b] (f : 'a -> 'b) s : summable s => psum s = psum (fun y => psum (fun x => if y = f x then s x else 0%r)). proof. move=> sms; pose v y x := if y = f x then `|s x| else 0%r. -have: forall J, uniq J => big predT (fun y => psum (v y)) J <= psum s. +have: forall J, uniq J => #big [ y : J ] (psum (v y)) <= psum s. + move=> J uqJ; have h := summable_psum_partition f s sms J uqJ. rewrite &(ler_trans _ _ h) lerr_eq &(eq_bigr) => b _ /=. by apply: eq_psum => a @/v /= /#. @@ -890,7 +890,7 @@ move=> sm; rewrite eqr_le; split => [|_]. + pose F x y := if y = f x then s x else 0%r. pose G y := psum (fun x => F x y). apply: ler_psum_lub => J uqJ; pose L := undup (map f J). - apply: (@ler_trans (big predT (fun y => `|G y|) L)); last first. + apply: (@ler_trans (#big [ y : L ] `|G y|)); last first. apply/ler_big_psum/undup_uniq => @/G @/F; case: (sms) => M smsM {J L uqJ}. exists M => J uqJ; apply/(@ler_trans (psum s))/ler_psum_lub => //. apply: (ler_trans _ _ (sm uqJ)); rewrite lerr_eq &(eq_bigr). @@ -1184,9 +1184,9 @@ qed. lemma prodrDl ['t 'u] (F : 't -> 'u -> real) (r : 't list) (s : 'u list) : uniq r => uniq s => - BRM.big predT (fun x => big predT (F x) s) r + BRM.#big [ x : r ] (#big [ y : s ] (F x y)) = sum (fun sigma => if fixfinfun (mem r) (mem s) sigma then - BRM.big predT (fun x => F x (sigma x)) r + BRM.#big [ x : r ] (F x (sigma x)) else 0%r). proof. move=> + uq_s; elim: r => /= [|x r ih [x_notin_r uq_r]]. @@ -1229,8 +1229,8 @@ qed. (* -------------------------------------------------------------------- *) lemma prodrDl2 (f g : 't -> real) r : is_finite_for predT r => - BRM.big predT (fun x => f x + g x) r - = sum (fun sigma => BRM.big predT (fun x => if sigma x then f x else g x) r). + BRM.#big [ x : r ] (f x + g x) + = sum (fun sigma => BRM.#big [ x : r ] (if sigma x then f x else g x)). proof. case=> [uq_r mem_r]; pose F x b := if b then f x else g x. have eq := prodrDl F r [true; false] _ _ => //. diff --git a/theories/crypto/GlobalHybrid.ec b/theories/crypto/GlobalHybrid.ec index ee33aa3958..3b1b021bb5 100644 --- a/theories/crypto/GlobalHybrid.ec +++ b/theories/crypto/GlobalHybrid.ec @@ -30,16 +30,16 @@ module type HYBRID = { lemma hybrid_gen (n : int) (p : int -> real) (M <: HYBRID) &m : 1 <= n => (forall (i : int), - 1 <= i < n => + 1 <= i < n => `|Pr[M.main(i) @ &m : res] - Pr[M.main(i + 1) @ &m : res]| <= p i) => `|Pr[M.main(1) @ &m : res] - Pr[M.main(n) @ &m : res]| <= - bigi predT p 1 n. + #bigi [ i : 1, n ] (p i). proof. move => ge1_n step. have ind : forall (i : int), 0 <= i => 1 <= i <= n => - `|Pr[M.main(1) @ &m : res] - Pr[M.main(i) @ &m : res]| <= bigi predT p 1 i. + `|Pr[M.main(1) @ &m : res] - Pr[M.main(i) @ &m : res]| <= #bigi [ j : 1, i ] (p j). elim => [// | i ge0_i IH [_ i_plus1_le_n]]. case (i = 0) => [-> /= |]. by rewrite ger0_norm // big_geq. diff --git a/theories/datatypes/BitEncoding.ec b/theories/datatypes/BitEncoding.ec index e4aee06893..6054d77e95 100644 --- a/theories/datatypes/BitEncoding.ec +++ b/theories/datatypes/BitEncoding.ec @@ -9,7 +9,7 @@ pragma +implicits. theory BS2Int. op bs2int (s : bool list) = - BIA.bigi predT (fun i => 2^i * b2i (nth false s i)) 0 (size s). + BIA.#bigi [ i : 0, (size s) ] (2^i * b2i (nth false s i)). op int2bs (N n : int) = mkseq (fun i => (n %/ 2^i) %% 2 <> 0) N. diff --git a/theories/datatypes/Xreal.ec b/theories/datatypes/Xreal.ec index 3b9c81fd05..27ef99a175 100644 --- a/theories/datatypes/Xreal.ec +++ b/theories/datatypes/Xreal.ec @@ -645,9 +645,9 @@ clone import Bigop as BXA with op Support.(+) <- Rpbar.xadd, theory Support.Axioms <- Rpbar.Axioms. -lemma is_real_bigRX ['a] (f : 'a -> xreal) l: - is_real f => - (BRA.big predT (to_real f) l)%xr = big predT f l. +lemma is_real_bigRX ['a] (f : 'a -> xreal) l: + is_real f => + (BRA.#big [ x : l ] (to_real f x))%xr = #big [ x : l ] (f x). proof. move=> hf; elim: l => //= x l hrec. rewrite big_cons BRA.big_cons /predT /= -hrec /to_real. @@ -655,36 +655,36 @@ proof. by rewrite of_realD // sumr_ge0 /= => a; apply to_realP. qed. -lemma bigR_to_real ['a] (f : 'a -> real) (l : 'a list) : +lemma bigR_to_real ['a] (f : 'a -> real) (l : 'a list) : (forall a, a \in l => 0%r <= f a) => - BRA.big predT (to_real (fun a => (f a)%xr)) l = BRA.big predT f l. + BRA.#big [ a : l ] (to_real (fun a => (f a)%xr) a) = BRA.#big [ a : l ] (f a). proof. move=> hpos; apply BRA.eq_big_seq; rewrite /to_real => x /hpos; smt(@Rp). qed. -lemma bigXR ['a] (f : 'a -> real) (l : 'a list) : +lemma bigXR ['a] (f : 'a -> real) (l : 'a list) : (forall a, a \in l => 0%r <= f a) => - big predT (fun x => (f x)%xr) l = (BRA.big predT f l)%xr. + #big [ x : l ] ((f x)%xr) = (BRA.#big [ x : l ] (f x))%xr. proof. by move=> hpos; rewrite -is_real_bigRX 1:// bigR_to_real. qed. -lemma bigXI ['a] (f : 'a -> int) (l : 'a list) : +lemma bigXI ['a] (f : 'a -> int) (l : 'a list) : (forall a, a \in l => 0 <= f a) => - big predT (fun x => (f x)%xr) l = (BIA.big predT f l)%xr. + #big [ x : l ] ((f x)%xr) = (BIA.#big [ x : l ] (f x))%xr. proof. by move=> h; rewrite bigXR 1:/# sumr_ofint. qed. -lemma bigiXR (f : int -> real) (m n : int) : +lemma bigiXR (f : int -> real) (m n : int) : (forall i, m <= i < n => 0%r <= f i) => - bigi predT (fun x => (f x)%xr) m n = (BRA.bigi predT f m n)%xr. + #bigi [ x : m, n ] ((f x)%xr) = (BRA.#bigi [ x : m, n ] (f x))%xr. proof. move=> hpos; apply bigXR => i /mem_range; apply hpos. qed. -lemma bigiXI (f : int -> int) (m n : int) : +lemma bigiXI (f : int -> int) (m n : int) : (forall i, m <= i < n => 0 <= f i) => - bigi predT (fun x => (f x)%xr) m n = (BIA.bigi predT f m n)%xr. + #bigi [ x : m, n ] ((f x)%xr) = (BIA.#bigi [ x : m, n ] (f x))%xr. proof. move=> hpos; apply bigXI => i /mem_range; apply hpos. qed. -lemma big_oo ['a] (J : 'a list) (f : 'a -> xreal) : - (exists (x : 'a), (x \in J) /\ f x = oo) => - big predT f J = oo. +lemma big_oo ['a] (J : 'a list) (f : 'a -> xreal) : + (exists (x : 'a), (x \in J) /\ f x = oo) => + #big [ x : J ] (f x) = oo. proof. move=> [x [hj hf]]; rewrite (bigID _ _ (pred1 x)) -big_filter predTI filter_pred1. have [n [hn ->]]: exists n, 0 <= n /\ count (pred1 x) J = n + 1. @@ -692,8 +692,8 @@ proof. by rewrite nseqS // big_cons /predT hf. qed. -lemma mulr_sumr ['a] (P : 'a -> bool) (F : 'a -> xreal) (s : 'a list) (x : realp) : - x ** (big P F s) = (big P (fun (i : 'a) => x ** F i) s). +lemma mulr_sumr ['a] (P : 'a -> bool) (F : 'a -> xreal) (s : 'a list) (x : realp) : + x ** (#big [ i : s | P i ] (F i)) = (#big [ i : s | P i ] (x ** F i)). proof. apply (big_comp (fun y => x ** y)) => //=; apply smulmDr. qed. @@ -820,10 +820,10 @@ proof. qed. (* -------------------------------------------------------------------- *) -lemma Ep_fin ['a] J (d : 'a distr) f : - uniq J => +lemma Ep_fin ['a] J (d : 'a distr) f : + uniq J => (forall (x : 'a), mu1 d x <> 0%r => x \in J) => - Ep d f = big predT (d ** f) J. + Ep d f = #big [ x : J ] ((d ** f) x). proof. move=> hu hJ; rewrite /Ep /=. case: (is_real (d ** f)) => his. @@ -950,7 +950,7 @@ proof. rewrite /dmap Ep_dlet; apply eq_Ep => x _ /=; apply Ep_dunit. qed. (* -------------------------------------------------------------------- *) lemma Ep_duniform ['a] (s : 'a list) (f : 'a -> xreal) : Ep (duniform s) f = - of_reald (1%r / (size ((undup s)))%r) ** big predT f (undup s). + of_reald (1%r / (size ((undup s)))%r) ** #big [ x : (undup s) ] (f x). proof. rewrite (Ep_fin (undup s)) 1:undup_uniq. + move=> x hx; rewrite mem_undup -supp_duniform; smt(ge0_mu). @@ -975,9 +975,9 @@ qed. (* -------------------------------------------------------------------- *) lemma Ep_dinterval (f : int -> xreal) i j: - Ep [i..j] f = - (if i <= j then 1%r / (j - i + 1)%r else 0%r) ** - big predT f (range i (j + 1)). + Ep [i..j] f = + (if i <= j then 1%r / (j - i + 1)%r else 0%r) ** + #big [ x : (range i (j + 1)) ] (f x). proof. rewrite (Ep_fin (range i (j + 1))) 1:range_uniq. + by move=> x; have := supp_dinter i j x; rewrite mem_range; smt (ge0_mu). @@ -986,8 +986,8 @@ proof. qed. lemma Ep_dinterval_le (f : int -> xreal) (i j : int) : - i <= j => - Ep [i..j] f = (1%r / (j - i + 1)%r) ** big predT f (range i (j + 1)). + i <= j => + Ep [i..j] f = (1%r / (j - i + 1)%r) ** #big [ x : (range i (j + 1)) ] (f x). proof. by move=> h; rewrite Ep_dinterval h. qed. (* -------------------------------------------------------------------- *) diff --git a/theories/distributions/DList.ec b/theories/distributions/DList.ec index da0ba6d614..b1300b5072 100644 --- a/theories/distributions/DList.ec +++ b/theories/distributions/DList.ec @@ -109,7 +109,7 @@ proof. by move=> ge0_n; case/(supp_dlist d n xs ge0_n). qed. lemma dlistE x0 (d : 'a distr) (p : int -> 'a -> bool) n : mu (dlist d n) (fun xs : 'a list => forall i, (0 <= i) && (i < n) => (p i (nth x0 xs i))) - = bigi predT (fun i => mu d (p i)) 0 n. + = #bigi [ i : 0, n ] (mu d (p i)). proof. elim/natind : n p => [n n_le0|n n_ge0 IHn] p. - rewrite dlist0 // dunitE range_geq //= big_nil; smt(). @@ -128,7 +128,7 @@ lemma dlist1E (d : 'a distr) n xs: 0 <= n => mu1 (dlist d n) xs = if n = size xs - then big predT (fun x => mu1 d x) xs + then #big [ x : xs ] (mu1 d x) else 0%r. proof. move=> le0_n; case (n = size xs)=> [->|]. diff --git a/theories/distributions/Dfilter.ec b/theories/distributions/Dfilter.ec index c07aed7f3c..4964fde50f 100644 --- a/theories/distributions/Dfilter.ec +++ b/theories/distributions/Dfilter.ec @@ -17,7 +17,7 @@ lemma isdistr_mfilter (m : 'a -> real) (P : 'a -> bool) : proof. move=> [] ge0_m le1_m; split=> [x|x /le1_m {le1_m} le1_m]. + by rewrite /mfilter; case (P x)=> //= _; exact/ge0_m. -apply/(@ler_trans (big predT m x) _ _ _ le1_m)/ler_sum=> a _. +apply/(@ler_trans (#big [ a : x ] (m a)) _ _ _ le1_m)/ler_sum=> a _. by rewrite /mfilter fun_if2 ge0_m. qed. diff --git a/theories/distributions/Distr.ec b/theories/distributions/Distr.ec index f4c8ddf94e..6b4ce80710 100644 --- a/theories/distributions/Distr.ec +++ b/theories/distributions/Distr.ec @@ -62,7 +62,7 @@ op mk : ('a -> real) -> 'a distr. inductive isdistr (m : 'a -> real) = | Distr of (forall x, 0%r <= m x) - & (forall s, uniq s => big predT m s <= 1%r). + & (forall s, uniq s => #big [ x : s ] (m x) <= 1%r). lemma eq_isdistr (d1 d2 : 'a -> real) : d1 == d2 => isdistr d1 = isdistr d2. @@ -75,7 +75,7 @@ lemma le1_isdistr (d : 'a -> real) x : isdistr d => d x <= 1%r. proof. by case=> _ /(_ [x] _) //; rewrite big_seq1. qed. lemma le1_sum_isdistr (d : 'a -> real) s : - isdistr d => uniq s => big predT d s <= 1%r. + isdistr d => uniq s => #big [ x : s ] (d x) <= 1%r. proof. by case=> _; apply. qed. axiom distrW (P : 'a distr -> bool): @@ -105,7 +105,7 @@ qed. hint exact : ge0_mu1. lemma le1_mu1_fin ['a] (d : 'a distr) (s : 'a list) : - uniq s => big predT (mu1 d) s <= 1%r. + uniq s => #big [ x : s ] (mu1 d x) <= 1%r. proof. by elim/distrW: d => m dm; rewrite muK' //; apply le1_sum_isdistr. qed. lemma le1_mu1 ['a] (d : 'a distr) x : mu1 d x <= 1%r. @@ -153,7 +153,7 @@ qed. lemma le1_mu (d : 'a distr) p : mu d p <= 1%r. proof. rewrite muE &(lerfin_sum) 1:&(summable_mu1_cond) => J uqJ. -apply: (@ler_trans (big predT (mu1 d) J)). +apply: (@ler_trans (#big [ a : J ] (mu1 d a))). + by apply: ler_sum => /= a _; case: (p a). + by apply: le1_mu1_fin. qed. @@ -178,7 +178,7 @@ lemma isdistr_finP (s : 'a list) (m : 'a -> real) : uniq s => (forall x, m x <> 0%r => mem s x) => (forall x, 0%r <= m x) - => (isdistr m <=> (big predT m s <= 1%r)). + => (isdistr m <=> (#big [ x : s ] (m x) <= 1%r)). proof. move=> uq_s fin ge0_m; split=> [[_ /(_ s uq_s)]|le1_m] //. split=> // s' uq_s'; rewrite (@bigID _ _ (mem s)) addrC big1 /=. @@ -424,7 +424,7 @@ qed. (* -------------------------------------------------------------------- *) lemma mu_has_le ['a 'b] (P : 'a -> 'b -> bool) (d : 'a distr) (s : 'b list) : - mu d (fun a => has (P a) s) <= BRA.big predT (fun b => mu d (fun a => P a b)) s. + mu d (fun a => has (P a) s) <= BRA.#big [ b : s ] (mu d (fun a => P a b)). proof. elim: s => [|x s ih]; first by rewrite big_nil mu0. rewrite big_cons {1}/predT /= mu_or. @@ -437,14 +437,14 @@ lemma mu_has_leM ['a 'b] (P : 'a -> 'b -> bool) (d : 'a distr) (s : 'b list) r : (forall b, b \in s => mu d (fun a => P a b) <= r) => mu d (fun a => has (P a) s) <= (size s)%r * r. proof. -move=> le; apply/(ler_trans (big predT (fun x => r) s)). +move=> le; apply/(ler_trans (#big [ _ : s ] r)). + by have /ler_trans := mu_has_le P d s; apply; apply/ler_sum_seq => ? /le. by rewrite Bigreal.sumr_const count_predT. qed. (* -------------------------------------------------------------------- *) lemma mu_mem_uniq ['a] (d : 'a distr) (s : 'a list) : - uniq s => mu d (mem s) = BRA.big predT (mu1 d) s. + uniq s => mu d (mem s) = BRA.#big [ x : s ] (mu1 d x). proof. elim: s => [_|x s ih [xs uq_s]]; first by rewrite big_nil mu0. rewrite big_cons {1}/predT /= -ih // -mu_disjointL => [y ->//|]. @@ -452,14 +452,14 @@ by apply/mu_eq=> y. qed. lemma mu_mem ['a] (d : 'a distr) (s : 'a list) : - mu d (mem s) = BRA.big predT (mu1 d) (undup s). + mu d (mem s) = BRA.#big [ x : (undup s) ] (mu1 d x). proof. rewrite -mu_mem_uniq ?undup_uniq; apply/mu_eq. by move=> x; rewrite mem_undup. qed. lemma mu_mem_le ['a] (d : 'a distr) (s : 'a list) : - mu d (mem s) <= BRA.big predT (mu1 d) s. + mu d (mem s) <= BRA.#big [ x : s ] (mu1 d x). proof. rewrite sumr_undup mu_mem; apply/ler_sum_seq => //= x. rewrite mem_undup => x_in_s _; rewrite intmulr. @@ -470,13 +470,13 @@ qed. lemma mu_mem_le_mu1 ['a] (d : 'a distr) (s : 'a list) r : (forall x, mu1 d x <= r) => mu d (mem s) <= (size s)%r * r. proof. -move=> le; apply/(ler_trans (big predT (fun (x : 'a) => r) s)). +move=> le; apply/(ler_trans (#big [ _ : s ] r)). + by have := mu_mem_le d s => /ler_trans; apply; apply/ler_sum. by rewrite Bigreal.sumr_const count_predT. qed. lemma fin_muE (d : 'a distr) (E : 'a -> bool) : is_finite (support d) => - mu d E = big E (mu1 d) (to_seq (support d)). + mu d E = #big [ x : (to_seq (support d)) | E x ] (mu1 d x). proof. move => fin_d. rewrite (@mu_eq_support d _ (mem (filter E (to_seq (support d))))). @@ -495,7 +495,7 @@ move => nFE; have := NfiniteP (ceil (inv eps) + 1) E _ nFE; 1: smt(ceil_ge). case => L /> size_L L_uniq sub_L_E. apply (ltr_le_trans (mu d (mem L))); last by apply mu_le => /#. rewrite mu_mem_uniq //. -apply (ltr_le_trans (big predT (fun (x : 'a) => eps) L)); +apply (ltr_le_trans (#big [ _ : L ] eps)); last by apply ler_sum_seq. rewrite sumr_const count_predT intmulr. apply (ltr_le_trans (eps * (ceil (inv eps) + 1)%r)); last smt(). @@ -1776,9 +1776,9 @@ rewrite (@partition_big ofst _ predT _ _ (undup (unzip1 s))). + by case=> a b ab_in_s _; rewrite mem_undup map_f. pose P := fun x ab => ofst<:'a, 'b> ab = x. pose F := fun (ab : 'a * 'b) => mb ab.`2. -rewrite -(@eq_bigr _ (fun x => ma x * big (P x) F s)) => /= [x _|]. +rewrite -(@eq_bigr _ (fun x => ma x * #big [ ab : s | P x ab ] (F ab))) => /= [x _|]. + by rewrite mulr_sumr; apply/eq_bigr=> -[a b] /= @/P <-. -pose s' := undup _; apply/(@ler_trans (big predT (fun x => ma x) s')). +pose s' := undup _; apply/(@ler_trans (#big [ x : s' ] (ma x))). + apply/ler_sum=> a _ /=; apply/ler_pimulr; first by apply/ge0_isdistr. rewrite -big_filter -(@big_map snd predT) le1_sum_isdistr //. rewrite map_inj_in_uniq ?filter_uniq //; case=> [a1 b1] [a2 b2]. @@ -2089,7 +2089,7 @@ hint rewrite djoinE : djoin_nil djoin_cons. lemma djoin1E (ds : 'a distr list) xs: mu1 (djoin ds) xs = if size ds = size xs - then BRM.big predT (fun xy : _ * _ => mu1 xy.`1 xy.`2) (zip ds xs) + then BRM.#big [ xy : (zip ds xs) ] (mu1 xy.`1 xy.`2) else 0%r. proof. elim: ds xs => [|d ds ih] xs /=; 1: rewrite djoin_nil dunitE. @@ -2175,7 +2175,7 @@ by move=> z @/(\o) /=; rewrite cats1. qed. lemma weight_djoin (ds : 'a distr list) : - weight (djoin ds) = BRM.big predT weight ds. + weight (djoin ds) = BRM.#big [ d : ds ] (weight d). proof. elim: ds => [|d ds ih]; rewrite djoinE /=. + by rewrite dunit_ll BRM.big_nil. @@ -2323,7 +2323,7 @@ type t. clone FinType as FinT with type t <- t. op mfun ['u] (d : t -> 'u distr) (f : t -> 'u) = - BRM.big predT (fun x => mu1 (d x) (f x)) FinT.enum. + BRM.#big [ x : FinT.enum ] (mu1 (d x) (f x)). lemma mfunE ['u] (d : t -> 'u distr) (f : t -> 'u) : mfun d f = mu1 (djoin (map d FinT.enum)) (map f FinT.enum). @@ -2350,7 +2350,7 @@ qed. op dfun ['u] (d : t -> 'u distr) = mk (mfun d). lemma dfun1E ['u] (d : t -> 'u distr) f : - mu1 (dfun d) f = BRM.big predT (fun x => mu1 (d x) (f x)) FinT.enum. + mu1 (dfun d) f = BRM.#big [ x : FinT.enum ] (mu1 (d x) (f x)). proof. by rewrite muK 1:isdistr_dfun &(BRM.eq_bigr). qed. @@ -2435,7 +2435,7 @@ qed. lemma dfunE ['u] du (p : t -> 'u -> bool) : mu (dfun du) (fun (f : t -> 'u) => forall x, p x (f x)) - = BRM.big predT (fun x => mu (du x) (p x)) FinT.enum. + = BRM.#big [ x : FinT.enum ] (mu (du x) (p x)). proof. pose P f := all (fun x => p x (f x)) FinT.enum. rewrite -(@mu_eq _ P) => [f|] @/P; first rewrite allP /=. @@ -2456,7 +2456,7 @@ by rewrite (@djoin_consE _ _ _ (p x) (P xs)) ih. qed. lemma weight_dfun ['u] (df : t -> 'u distr) : - weight (dfun df) = BRM.big predT (fun x => weight (df x)) FinT.enum. + weight (dfun df) = BRM.#big [ x : FinT.enum ] (weight (df x)). proof. by have /= -> := dfunE df (fun _ _ => true). qed. lemma dfun_ll ['u] (d : t -> 'u distr) : @@ -3106,7 +3106,7 @@ qed. (* -------------------------------------------------------------------- *) lemma exp_duniform ['a] (s : 'a list) f : - E (duniform s) f = (1%r / (size (undup s))%r) * BRA.big predT f (undup s). + E (duniform s) f = (1%r / (size (undup s))%r) * BRA.#big [ x : (undup s) ] (f x). proof. rewrite /E (@sumE_fin _ (undup s)) 1:undup_uniq /=. - move=> a; rewrite mulf_eq0 negb_or; case=> _. @@ -3343,7 +3343,7 @@ qed. lemma E_splits ['a] p f d k : hasE d f => partition d p k - => E<:'a> d f = BRA.bigi predT (fun i => mu d (p i) * Ec d f (p i)) 0 k. + => E<:'a> d f = BRA.#bigi [ i : 0, k ] (mu d (p i) * Ec d f (p i)). proof. move=> Edf; elim/natind: k d Edf => [k le0_k|k ge0_k ih] d Edf hpdk. - rewrite BRA.big_geq // (_ : d = dnull) -1:exp_dnull //. @@ -3398,7 +3398,7 @@ qed. (* -------------------------------------------------------------------- *) lemma fin_expE (d : 'a distr) (f : 'a -> real) : is_finite (support d) => - E d f = big predT (fun x => f x * mu1 d x) (to_seq (support d)). + E d f = #big [ x : (to_seq (support d)) ] (f x * mu1 d x). proof. move => fin_d; rewrite /E (@sumE_fin _ (to_seq (support d))) ?uniq_to_seq //. by move => x; rewrite mem_to_seq //; smt(supportP). diff --git a/theories/distributions/SDist.ec b/theories/distributions/SDist.ec index 70610147a0..f0df011fa0 100644 --- a/theories/distributions/SDist.ec +++ b/theories/distributions/SDist.ec @@ -260,9 +260,9 @@ module type Distinguisher = { proc guess (x : in_t) : out_t }. -lemma uniq_big_res (A <: Distinguisher) &m x' (bs : out_t list) : +lemma uniq_big_res (A <: Distinguisher) &m x' (bs : out_t list) : uniq bs => - big predT (fun b => Pr[A.guess(x') @ &m : res = b]) bs = + #big [ b : bs ] (Pr[A.guess(x') @ &m : res = b]) = Pr[A.guess(x') @ &m : res \in bs]. proof. elim: bs => [_|b bs IHbs /= [bNbs uq_bs]]. diff --git a/theories/encryption/Means.ec b/theories/encryption/Means.ec index 7ba0edb18c..a8a9a6fe36 100644 --- a/theories/encryption/Means.ec +++ b/theories/encryption/Means.ec @@ -45,7 +45,8 @@ lemma introOrs (A <: Worker) &m (ev:input -> glob A -> output -> bool): => let sup = to_seq (support d) in Pr[Rand(A).main() @ &m: ev (fst res) (glob A) (snd res)] = Pr[Rand(A).main() @ &m: - big predT (fun v=> ev v (glob A) (snd res) /\ v = fst res) sup]. + StdBigop.Bigbool.BBOr.#big + [ v : sup ] (ev v (glob A) (snd res) /\ v = fst res)]. proof. move=> Fsup sup. byequiv (: ={glob A} ==> ={glob A, res} /\ (fst res{1}) \in d)=> //. @@ -61,7 +62,7 @@ lemma Mean (A <: Worker) &m (ev:input -> glob A -> output -> bool): is_finite (support d) => let sup = to_seq (support d) in Pr[Rand(A).main()@ &m: ev (fst res) (glob A) (snd res)] - = big predT (fun v, mu1 d v * Pr[A.work(v)@ &m:ev v (glob A) res]) sup. + = #big [ v : sup ] (mu1 d v * Pr[A.work(v)@ &m:ev v (glob A) res]). proof. move=> Fsup /=. have:= introOrs A &m ev _=> //= ->. @@ -70,10 +71,12 @@ elim: (to_seq (support d)) (uniq_to_seq (support d))=> //= + by rewrite big_nil; byphoare (: true ==> false). rewrite big_cons {2}/predT /=. have ->: Pr[Rand(A).main() @ &m: - big predT (fun v=> ev v (glob A) res.`2 /\ v = res.`1) (v::vs)] + StdBigop.Bigbool.BBOr.#big + [ v : (v::vs) ] (ev v (glob A) res.`2 /\ v = res.`1)] = Pr[Rand(A).main() @ &m: (ev v (glob A) (snd res) /\ v = fst res) \/ - big predT (fun v=> ev v (glob A) res.`2 /\ v = res.`1) vs]. + StdBigop.Bigbool.BBOr.#big + [ v : vs ] (ev v (glob A) res.`2 /\ v = res.`1)]. + by rewrite Pr[mu_eq]. rewrite Pr[mu_disjoint]. + move=> /> &0; rewrite negb_and negb_and //=. @@ -90,7 +93,7 @@ lemma Mean_uni (A <: Worker) &m (ev : input -> glob A -> output -> bool) r: => is_finite (support d) => let sup = to_seq (support d) in Pr[Rand(A).main()@ &m: ev (fst res) (glob A) (snd res)] - = r * big predT (fun v=> Pr[A.work(v) @ &m:ev v (glob A) res]) sup. + = r * #big [ v : sup ] (Pr[A.work(v) @ &m:ev v (glob A) res]). proof. move=> Hd Hfin /=. have := Mean A &m ev => /= -> //. diff --git a/theories/modules/EventPartitioning.ec b/theories/modules/EventPartitioning.ec index 4939f847eb..5cc0d5d5f0 100644 --- a/theories/modules/EventPartitioning.ec +++ b/theories/modules/EventPartitioning.ec @@ -22,8 +22,7 @@ abstract theory ListPartitioning. (P : partition list) &m: uniq P => Pr[M.f(i) @ &m: E i (glob M) res] - = big predT (fun a => - Pr[M.f(i) @ &m: E i (glob M) res /\ phi i (glob M) res = a]) P + = #big [ a : P ] (Pr[M.f(i) @ &m: E i (glob M) res /\ phi i (glob M) res = a]) + Pr[M.f(i) @ &m: E i (glob M) res /\ !mem P (phi i (glob M) res)]. proof. move=> uniq_P. rewrite Pr[mu_split (mem P (phi i (glob M) res))]; congr. @@ -66,8 +65,7 @@ abstract theory FSetPartitioning. (phi : input -> (glob M) -> output -> partition) (P : partition fset) &m: Pr[M.f(i) @ &m: E i (glob M) res] - = big predT (fun a => - Pr[M.f(i) @ &m: E i (glob M) res /\ phi i (glob M) res = a]) (elems P) + = #big [ a : (elems P) ] (Pr[M.f(i) @ &m: E i (glob M) res /\ phi i (glob M) res = a]) + Pr[M.f(i) @ &m: E i (glob M) res /\ !mem P (phi i (glob M) res)]. proof. have->: Pr[M.f(i) @ &m : @@ -99,8 +97,7 @@ abstract theory FPredPartitioning. (P : partition -> bool) &m: is_finite P => Pr[M.f(i) @ &m: E i (glob M) res] - = big predT (fun a => - Pr[M.f(i) @ &m: E i (glob M) res /\ phi i (glob M) res = a]) (to_seq P) + = #big [ a : (to_seq P) ] (Pr[M.f(i) @ &m: E i (glob M) res /\ phi i (glob M) res = a]) + Pr[M.f(i) @ &m: E i (glob M) res /\ !P (phi i (glob M) res)]. proof. move=> /mem_to_seq H. @@ -125,7 +122,7 @@ theory ResultPartitioning. (X : input -> output list) &m: Pr[M.f(i) @ &m: E i (glob M) res] - = big predT (fun a=> Pr[M.f(i) @ &m: E i (glob M) res /\ res = a]) (undup (X i)) + = #big [ a : (undup (X i)) ] (Pr[M.f(i) @ &m: E i (glob M) res /\ res = a]) + Pr[M.f(i) @ &m: E i (glob M) res /\ !mem (X i) res]. proof. have->:Pr[M.f(i) @ &m : E i (glob M){hr} res{hr} /\ ! (res{hr} \in X i)]= @@ -149,7 +146,7 @@ theory TotalResultPartitioning. &m: (forall i, hoare [M.f: arg = i ==> mem (X i) res]) => Pr[M.f(i) @ &m: E i (glob M) res] - = big predT (fun a => Pr[M.f(i) @ &m: E i (glob M) res /\ res = a]) (undup (X i)). + = #big [ a : (undup (X i)) ] (Pr[M.f(i) @ &m: E i (glob M) res /\ res = a]). proof. move=> support_M. rewrite (@result_partitioning M i E X &m). diff --git a/theories/modules/Reflection.eca b/theories/modules/Reflection.eca index f5ce4b14b5..62161f29fa 100644 --- a/theories/modules/Reflection.eca +++ b/theories/modules/Reflection.eca @@ -18,11 +18,9 @@ local module P2 = { } }. -local lemma gen_fact &m a (l : (r * (glob P)) list): uniq l - => Pr[ P.p(a) @ &m : (res , (glob P)) \in l ] - = big predT (fun (x : (r * (glob P))) => - Pr[P.p(a) @ &m: res=x.`1 /\ (glob P) = x.`2]) - l. +local lemma gen_fact &m a (l : (r * (glob P)) list): uniq l + => Pr[ P.p(a) @ &m : (res , (glob P)) \in l ] + = #big [ x : l ] (Pr[P.p(a) @ &m: res=x.`1 /\ (glob P) = x.`2]). proof. move: l; apply list_ind => /= [|x l p1 [x_nin uniq_l]]. - by rewrite Pr[mu_false] big_nil. @@ -54,8 +52,8 @@ have PRP: (PR (glob P){m}) a = fun (x : (r * (glob P))) rewrite eq_iff; split => [/#|<- &n gl_eq]. byequiv (_: ={arg, glob P} ==> ={res, glob P})=> //; 1:sim; smt(). have distr_PR: isdistr (PR (glob P){m} a). -- have : (forall (s : ((r * (glob P)) list)), uniq s => - big predT (PR (glob P){m} a) s <= 1%r). +- have : (forall (s : ((r * (glob P)) list)), uniq s => + #big [ x : s ] (PR (glob P){m} a x) <= 1%r). + rewrite PRP. apply list_ind => /=[|x l q1 q2]. * by rewrite big_nil. diff --git a/theories/modules/TotalProb.ec b/theories/modules/TotalProb.ec index c513cc7d7f..bac60f2023 100644 --- a/theories/modules/TotalProb.ec +++ b/theories/modules/TotalProb.ec @@ -98,9 +98,7 @@ qed. lemma total_prob' (supp : t list) (dt' : t distr) (i' : input) &m : is_finite_for (support dt') supp => Pr[Rand(M).f(dt', i') @ &m : res] = - big predT - (fun x' => mu1 dt' x' * Pr[M.main(i', x') @ &m : res]) - supp. + #big [ x' : supp ] (mu1 dt' x' * Pr[M.main(i', x') @ &m : res]). proof. move => [uniq_supp supp_iff]. have ->: @@ -129,9 +127,7 @@ end section. lemma total_prob (M <: T) (supp : t list) (dt : t distr) (i : input) &m : is_finite_for (support dt) supp => Pr[Rand(M).f(dt, i) @ &m : res] = - big predT - (fun (x : t) => mu1 dt x * Pr[M.main(i, x) @ &m : res]) - supp. + #big [ x : supp ] (mu1 dt x * Pr[M.main(i, x) @ &m : res]). proof. exact: (total_prob' M). qed. end TotalGeneral. @@ -171,9 +167,7 @@ proof *. lemma total_prob_drange (M <: T) (m n : int) (i : input) &m : m < n => Pr[Rand(M).f(drange m n, i) @ &m : res] = - bigi predT - (fun (j : int) => Pr[M.main(i, j) @ &m : res] / (n - m)%r) - m n. + #bigi [ j : m, n ] (Pr[M.main(i, j) @ &m : res] / (n - m)%r). proof. move => lt_m_n; rewrite (total_prob M (range m n)). + by rewrite /is_finite_for; smt(range_uniq mem_range supp_drange). @@ -199,9 +193,7 @@ proof *. lemma total_prob_uniform (M <: T) (xs : t list) (i : input) &m : uniq xs => xs <> [] => Pr[Rand(M).f(duniform xs, i) @ &m : res] = - big predT - (fun (x : t) => Pr[M.main(i, x) @ &m : res] / (size xs)%r) - xs. + #big [ x : xs ] (Pr[M.main(i, x) @ &m : res] / (size xs)%r). proof. move => uniq_xs xs_ne_nil; rewrite (total_prob M xs). + smt(supp_duniform).