The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Predicate-transformer semantics can be viewed as some sort of induction 
principle over state-transformer semantics.

Hence, theorems about predicate-transformers give examples of 
second-order theorems...

For example, see 
http://www-verimag.imag.fr/~boulme/HOARE_LOGIC_TUTORIAL/html/HoareTut.partialhoarelogic.html#PartialHoareLogic.wp_sound

Regards,

Sylvain.

Le 10/06/2022 à 16:09, Steve Zdancewic a écrit :
> The Interaction Trees Library 
> (https://github.com/DeepSpec/InteractionTrees) has many examples of 
> lemmas that quantify over predicates.  We use that feature to define 
> bisimulations and relational reasoning principles over interaction trees 
> (and monadic computations more generally).  See the definitions in 
> https://github.com/DeepSpec/InteractionTrees/blob/master/theories/Eq/Eqit.v 
> and uses of such reasoning in the various example directories.
>
> -Steve
>
> On 6/10/22 2:07 AM, kirang wrote:
> > Hi all,
> >
> > I've recieved a couple of messages asking for clarification on what 
> > exactly I mean by a second order property here.
> >
> > I don't have a too clear definition of what I mean by an "interesting 
> > second order property" in Coq, I have just been going off a 
> > know-it-when-I-see it basis up till now.
> >
> > I guess if you had to push me, I'd say any non-trivial theorem[1] that 
> > quantifies over a predicate (i.e something matching the pattern 
> > `forall ... (P: _ ... -> Prop) .., ...)`).
> >
> > Induction principles would trivially fit into this pattern because 
> > they're all of the form `forall (P: _ -> .. -> Prop), P .. -> ... -> P 
> > _`, the part of interest being the fact that `P: _ -> .. -> Prop` is 
> > quantified over.
> >
> >
> > Thanks,
> > Kiran.
> >
> >
> > [1] Thereby excluding properties like excluded middle or proof 
> > irrelevance.
> >
> > On 2022-06-09 05:14, kirang wrote:
> > > Hi Coq Club,
> > >
> > > For various reasons, I'm currently doing a light survey of examples of
> > > interesting uses of second order properties/lemmas in Coq proof
> > > scripts.
> > >
> > > Currently, the main examples I've found in the wild have mostly been
> > > using various induction principles for custom datatypes and the such
> > > (found through searching Github/using Coq's search mechanism).
> > >
> > > I've seemingly exhausted searching through Github for now and so I
> > > thought I might reach out to the magnanimous wisdom and experience of
> > > the Coq club community in this search.
> > >
> > > Do you have any interesting examples of other classes of second order
> > > properties (i.e other than induction principles) you have seen/used in
> > > your own proofs?
> > >
> > >
> > > Thanks,
> > > Kiran.