The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

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.