The Coq mailing list

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

I know a class of second-order properties more general than induction principles. There is a kind of types called (generic) container types. A container type is (Container : Type -> Type) that the type parameter is only used in strictly positive positions. For example, lists, trees and association lists (with the index type fixed and the content type as parameter) are container types. A more sophisticated example is that we can define a generic value type to represent values of programming languages, including basic values, lists and structs. The type of basic value can be a parameter, so the value type is a container type.

In order to define relations between containers, we define a Forall relation whose type is (Forall : forall A B (P : A -> B -> Prop), Container A -> Container B -> Prop). Forall is defined as the two containers have the same structure and each pair of corresponding elements satisfies P. For example, Coq.Lists.List.Forall2 is the Forall relation for lists. For each particular relation on interest, we parametrize Forall with a particular P. In order to prove lemmas about these relations, we prove a bunch of general second-order lemmas, for example,
Forall2_impl:
  forall {A B : Type} (P Q : A -> B -> Prop),
  (forall (a : A) (b : B), P a b -> Q a b) ->
  forall (l1 : list A) (l2 : list B), Forall2 P l1 l2 -> Forall2 Q l1 l2

Forall2_refl :
  forall {A : Type} (f : A -> A -> Prop),
  (forall x : A, f x x) -> forall v : list A, Forall2 f v v

Forall2_sym :
  forall {A B : Type} (f : A -> B -> Prop) (g : B -> A -> Prop),
  (forall (a : A) (b : B), f a b -> g b a) ->
  forall (v1 : list A) (v2 : list B), Forall2 f v1 v2 -> Forall2 g v2 v1

Forall2_trans :
  forall {A B C : Type} (f : A -> B -> Prop) (g : B -> C -> Prop) (h : A -> C -> Prop),
  rel_trans f g h ->
  forall (v1 : list A) (v2 : list B) (v3 : list C),
  Forall2 f v1 v2 -> Forall2 g v2 v3 -> Forall2 h v1 v3

Using these general lemmas, the task of proving lemmas about Forall relations is reduced to proving lemmas about pointwise relations.

Thanks,

Qinshi

On Thu, Jun 9, 2022 at 12:14 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.