The Coq mailing list

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

Perfect, yes, I guess traversal functions are a class of second-order 
properties in Coq other than induction that would satisfy what I was 
looking for.

Thanks for the links in this thread, I'll look through them.

Thanks,
Kiran.

On 2022-06-09 21:48, Castéran Pierre wrote:
> - External Email -
>
> Hi,
>
>  Maybe  the proof that the Ackermann function is not primitive
> recursive ?
> It is based on an induction on any PR function on any arity, using
> Russel O’Connor’s formalization from  his Goedel contrib.
>
> There is a version in https://github.com/coq-community/hydra-battles
>
> Pierre
>
> > Le 9 juin 2022 à 21:19, Lawrence Dunn <dunnla AT seas.upenn.edu> a
> > écrit :
> >
> > 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 [1]
> >
> > Fixpoint R [2] (T [3]:ty [4]) (t [5]:tm [6]) : Prop :=
> > empty ⊢ [7] t [5] \ [7]in [7] T [3] ∧ [8] halts [9] t [5] ∧
> > [8]
> > ( [8]match T [3] with
> > | <{ [10] Bool }> [10] ⇒ True [11]
> > | <{ [10] T1 → T2 }> [10] ⇒ (∀ s [12], R [13] T1 s [12] →
> > R [13] T2 <{ [10]t [5] s [12]}> [10] )
> > end) [8].
> >
> > 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
> > [14]
> >
> > You'll find many variations on this theme under the name of "Logical
> > Relations", e.g. in CertiKOS here:
> > https://github.com/CertiKOS/coqrel [15]
> >
> > 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.
>
>
>
> Links:
> ------
> [1] https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html
> [2] https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#R
> [3] 
> https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#T:155
> [4] https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#ty
> [5] 
> https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#t:156
> [6] https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#tm
> [7]
> https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#3b5796de2387691122e67a3516cd710b
> [8]
> https://urldefense.com/v3/__http://coq.inria.fr/library/*Coq.Init.Logic.html*ba2b0e492d2b4675a0acf3ea92aabadd__;LyM!!IBzWLUs!XzenuuQhk5IHfh9MDKtfeV-KjIg6jJeGYBFj4NG05sB6StYr9llXJ7lCHNJmLLTC634zWDNg5J4GCRTb-2yS$
> [9] 
> https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#halts
> [10]
> https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#96e24cc1b3765f349012b832d1dd22ad
> [11]
> https://urldefense.com/v3/__http://coq.inria.fr/library/*Coq.Init.Logic.html*True__;LyM!!IBzWLUs!XzenuuQhk5IHfh9MDKtfeV-KjIg6jJeGYBFj4NG05sB6StYr9llXJ7lCHNJmLLTC634zWDNg5J4GCVanGy1p$
> [12] 
> https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#s:159
> [13] 
> https://softwarefoundations.cis.upenn.edu/plf-current/Norm.html#R:157
> [14]
> https://urldefense.com/v3/__https://github.com/coq-community/autosubst/blob/master/examples/ssr/SystemF_CBV.v__;!!IBzWLUs!XzenuuQhk5IHfh9MDKtfeV-KjIg6jJeGYBFj4NG05sB6StYr9llXJ7lCHNJmLLTC634zWDNg5J4GCTPWlZY6$
> [15]
> https://urldefense.com/v3/__https://github.com/CertiKOS/coqrel__;!!IBzWLUs!XzenuuQhk5IHfh9MDKtfeV-KjIg6jJeGYBFj4NG05sB6StYr9llXJ7lCHNJmLLTC634zWDNg5J4GCZYINiCE$