The Coq mailing list

[Lawrence Dunn <dunnla AT seas.upenn.edu>]

If it is not too far afield, a class of examples comes from considering operations that are polymorphic over a class of functors, second-order in the same sense as in this paper: https://arxiv.org/abs/1402.1699. This is one approach to datatype-generic programming (and proving). This is actually related to the example involving finitary containers, aka traversable functors, which may be characterized entirely by law-abiding 'traverse' operation whose type is polymorphic over a choice of applicative functor, as discussed in the paper above. The type of a traversal over a container datatype T (list, tree, etc)  is `traverse : forall (Applicative F) (A B : Type), (A -> F B) -> T A -> F (T B).`

At first the traverse operation looks like "just" an elimination principle for defining operations on T, used this way in functional programming. But it can also be used in proofs about finitary containers, so more like an induction principle. In fact the example Forall given earlier is just a special case defined by traversing with the binary relation, where one views the "powerset" functor `(X \mapsto (X -> Prop))` as applicative. The properties of Forall can be derived from the laws of traversals. So a law-abiding traversal would seem to meet your criteria as a second-order property used in proofs which is not just induction.

A real-world example in Coq would be found in my library Tealeaves (https://github.com/dunnl/tealeaves), intended to be used for datatype-generic reasoning about syntax. One quantifies over a choice of traversable monad and can prove lemmas such as "two simultaneous substitutions in 't' are equal just if they are equal pointwise on the variables that occur in 't'," using a law-abiding second-order operation which generalizes traverse. See e.g. the lemmas derived at

https://github.com/dunnl/tealeaves/blob/dcff3c3d0f8c5982d2996f77e932d12cedcf2f0e/Tealeaves/Classes/DecoratedTraversableMonad.v#L958

and the relatively high-level theorems like

https://github.com/dunnl/tealeaves/blob/dcff3c3d0f8c5982d2996f77e932d12cedcf2f0e/LN/Theory.v#L871

which use this method of proof.

This isn't fully written up yet but I hope it makes some sense.

Best,

Lawrence

On Thu, Jun 9, 2022 at 2:45 PM roux cody <cody.roux AT gmail.com> wrote:

Here's a classic example, involving the proof of normalization of a typed lambda calculus from https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html

Fixpoint R (T:ty) (t:tm) : Prop :=
  empty ⊢ t \in T ∧ halts t ∧
  (match T with
   | <{ Bool }> ⇒ True
   | <{ T₁ → T₂ }> ⇒ (∀ s, R T₁ s → R T₂ <{t s}> )
   end).

Obviously this doesn't *quantify* on a relation, though any similar proof for System F must crucially use it, see e.g. here: https://github.com/coq-community/autosubst/blob/master/examples/ssr/SystemF_CBV.v

You'll find many variations on this theme under the name of "Logical Relations", e.g. in CertiKOS here: https://github.com/CertiKOS/coqrel

Hope this helps,

Cody

On Thu, Jun 9, 2022 at 2:22 AM kirang <kirang AT comp.nus.edu.sg> 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.