The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

I would say traversal over a data structure is a form of induction. But that is 
probably a matter of definition. ;)

; Ralf

On 09.06.22 23:12, kirang wrote:
> 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$ 

--
Website: https://ralfj.de/research