The Coq mailing list

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

Hi Qinshi,

Thanks for the suggestion, yes that seems like a nice example of a small 
self-contained example of second order property used in Coq scripts.

Thanks,
Kiran.

On 2022-06-09 19:03, Qinshi Wang wrote:
> - External Email -
>
> 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.