The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Duraj,

 

for rewriting under fold_left you need to use setoid_rewrite and you need to show that fold_left is a proper function which respects the equalities of its arguments.

 

I am myself still struggling with the concepts of this, so I took this as an exercise. Maybe one of the experts can review my comments / explanations of the required “Proper term”.

 

Best regards,

 

Michael

 

 

Require Import List.

Require Import Setoid.

Require Import Morphisms.

 

(*

For rewriting under f : A->B->C we need an Instance of

 

  Proper ( equality of A ==> equality of B ==> equality of C ) f

 

The equality is usually (@eq type).

The usual equality for a function parameter p D->E->F is pointwise equality

 

  pointwise_relation D (pointwise_relation E (@eq F))

 

Afaik if (and only if) the equalities for all arguments and result types is (@eq type), the usual rewrite can be used.

For fold_left, the problematic parameter is the function f, which requires pointwise equality.

*)

 

(* So for rewriting under fold_left we need: *)

 

Instance fold_left_proper(A B : Type) : Proper (

        pointwise_relation A (pointwise_relation B (@eq A))

    ==> @eq (list B)

    ==> @eq A

    ==> @eq A

  ) (fold_left (B:=B)).

Proof.

  unfold Proper, respectful, pointwise_relation.

  intros f1 f2 Hf l1 l2 Hl.

  subst.

  induction l2.

  - intros n1 n2 Hn. subst. reflexivity.

  - intros n1 n2 Hn. subst. simpl.

    apply IHl2. apply Hf.

Qed.

 

Lemma fold_left_zero {a : Type}: forall (l : list a) (n : nat), fold_left (fun (n1 : nat) (_ : a) => n1) l n = n.

Admitted.

 

Parameter x : Set.

Definition y := x.

Parameter elements : list x.

 

Goal fold_left

  (fun (n : nat) (_ : x) =>

   fold_left (fun (n0 : nat) (_ : y) => n0) elements n)

  elements 0 = 0.

 

  setoid_rewrite fold_left_zero.

  rewrite fold_left_zero.

  reflexivity.

Qed.

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928