The Coq mailing list

[Qinshi Wang <qinshiw AT cs.princeton.edu>]

I agree that traversal is a generalization of induction. Induction schemes apply homogeneous rules for each node, but traversal schemes can chain them together. But although I don't quite understand Lawrence's real-world examples, I think he suggests traversal schemes are generalization of induction schemes and laws of traversal schemes are generalization of laws of Forall relations. The latter is not so similar to induction schemes.

Thanks,

Qinshi

On Fri, Jun 10, 2022 at 10:50 PM Ralf Jung <jung AT mpi-sws.org> wrote:

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