The Coq mailing list

[kirang <kirang AT comp.nus.edu.sg>]

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.