The Coq mailing list

[Steve Zdancewic <stevez AT seas.upenn.edu>]

    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.
>         
>