Stream: math-comp users

Topic: Understanding extremum_spec

Ricardo (Mar 11 2023 at 17:34):

Hi everyone. Hope you're having a lovely Saturday. I'm trying to understand the advantage of writing extremumP in this way

Context {T : eqType} (ord : rel T) {I : finType} (P : pred I) (F : I -> T).
Variant extremum_spec : I -> Type :=
  ExtremumSpec (i : I) of P i & (forall j : I, P j -> ord (F i) (F j)) :
                   extremum_spec ord P F i.

Lemma extremumP : extremum_spec ord P F extremum.

instead of simply

Lemma extremumP : forall j : I, ord (F extremum) (F j)

or something like that.

Cyril Cohen (Mar 11 2023 at 18:24):

(sorry I have only a few seconds) The purpose of "spec" lemmas is to be used with the case tactic. I or someone else will come back later to cite the related section of the mathcomp book.

Ricardo (Mar 11 2023 at 19:35):

Thank you @Cyril Cohen :smile:

Pierre Roux (Mar 11 2023 at 19:43):

See section 5.2.1 of the mathcomp book: https://math-comp.github.io/mcb/

Last updated: Oct 13 2024 at 01:02 UTC