The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi list, another question.

I want to define a good induction principle for the following
function, à la fold_rec {dep}, which basically fold through two lists
of the same length.

Section list_fold_i_sum_2.
  Variables X Y Z Z' : Type.
  Variable null : Z'.
  Variable (f: Z -> nat -> X -> Y -> Z + Z').

  Fixpoint list_fold_i_sum_2 i acc lx ly: Z + Z' :=
  match lx,ly with
    | x::xq, y::yq => match f acc i x y with inl acc =>
list_fold_i_sum_2 (S i) acc  xq yq | r => r end
    | nil,nil => inl _ acc
    | _,_  => inr _ null
  end.
End list_fold_i_sum_2.

Lately, I played with the induction principles of ordered FSets (like
set_induction), and I found out that they were provable using
something similar to the proof of Prect (see the code below), by
building an inductive, and recursing on it. Using this trick, one can
prove the same induction principles as the ones in the library (and
those could maybe be used to prove lemmas about fold in the ordered
FMap library).

So, I followed the same scheme, building an inductive, and a fixpoint
on it, and proved the equality between these two functions (the
complete code is copied below, for the curious)
  Inductive combine : nat -> list X -> list Y -> Type :=
  | cnil : forall n, combine n nil nil
  | ccons : forall n lx ly x y, combine (S n) lx ly -> combine  n
(x::lx) (y::ly).

  Program Fixpoint list_fold_combine lx ly n (c : combine n lx ly)
(acc : Z)  :=
    match c with
      | cnil n => inl _ acc
      | ccons n lx ly x y c =>
        match f acc n x y with
          | inl acc => @list_fold_combine _ _ _ c acc
          |  r => r
        end
    end.

   Program Fixpoint build_combine n lx ly (H:List.length lx =
List.length ly): combine n lx ly := ....
   Variable lx : list X.
   Variable ly : list Y.
   Hypothesis H : List.length lx = List.length ly.
   Lemma equality n acc : list_fold_i_sum_2 n acc lx ly =
list_fold_combine (build_combine n H) acc.

Then, to make proofs about list_fold_i_sum_2, I rewrite the equality
lemma, and make an induction on build_combine (which can be tedious,
because of depandancies problems). I wonder if someone would have
another solution to express, and prove, an induction principle about
this function.

Any comments welcome
With best regards,

Thomas Braibant

<----- snippet for FSets for the curious ----->


Inductive lva : t -> Type :=
    | lnila :  forall s, Equal s empty ->  lva s
    | lconsa : forall x p, lva p -> ~In x p -> Above x p -> forall s,
Equal s (add x p) ->  lva s
.

Program Definition lva_iter
(P : t -> Type)
(a : forall s, Equal s empty -> P s)
(f : forall p x, P p -> ~In x p -> Above x p -> forall s, Equal s (add
x p) -> P s)
      :=
fix iter p (q : lva p) : P p :=
        match q in lva p return P p with
          | lnila  s hs  => a s hs
          | lconsa x p lvp _ _ _ _ => f p x (iter _ lvp) _ _ _ _
        end.
Program Fixpoint lVA s {measure cardinal s}: lva s :=
      match max_elt s with
        | None => @lnila _ _
        | Some x =>
          @lconsa x  _ (lVA (remove x s)) _ _ _ _
      end

Definition srecta
(P:t->Type)
(a:forall s, Equal s empty ->P s)
(f:forall p x, P p -> ~ In x p -> Above x p -> forall s, Equal s(add x
p) -> P s)
(s: t) :=
      lva_iter P a f s (lVA s).


<---------------- the code for list_fold_i_sum_2 ------------------>
Section list_fold_i_sum_2.
  Variables X Y Z Z' : Type.
  Variable null : Z'.
  Variable (f: Z -> nat -> X -> Y -> Z + Z').

  Fixpoint list_fold_i_sum_2 i acc lx ly: Z + Z' :=
  match lx,ly with
    | x::xq, y::yq => match f acc i x y with inl acc =>
list_fold_i_sum_2 (S i) acc  xq yq | r => r end
    | nil,nil => inl _ acc
    | _,_  => inr _ null
  end.

  Inductive combine : nat -> list X -> list Y -> Type :=
  | cnil : forall n, combine n nil nil
  | ccons : forall n lx ly x y, combine (S n) lx ly -> combine  n
(x::lx) (y::ly).

  Program Fixpoint list_fold_combine lx ly n (c : combine n lx ly)
(acc : Z)  :=
    match c with
      | cnil n => inl _ acc
      | ccons n lx ly x y c =>
        match f acc n x y with
          | inl acc => @list_fold_combine _ _ _ c acc
          |  r => r
        end
    end.

  Section build.

    Program Fixpoint build_combine n lx ly (H:List.length lx =
List.length ly): combine n lx ly :=
      match lx with
        | x::qx => match ly with y::qy =>  @ccons _ _ _ _ _
(@build_combine (S n) _ _ _ ) | nil => @cnil _ end
        | _ => @cnil  _
      end.
    Next Obligation.
      destruct lx. reflexivity.  specialize (H0 x lx). tauto.
    Defined.
    Next Obligation.
      assert (lx = nil).
        destruct lx. reflexivity.  specialize (H0 x lx). tauto.
        rewrite H1 in H. clear - H. destruct ly. reflexivity. discriminate.
      Defined.

    Variable lx : list X.
    Variable ly : list Y.
    Hypothesis H : List.length lx = List.length ly.

    Lemma equality n acc : list_fold_i_sum_2 n acc lx ly =
list_fold_combine (build_combine n H) acc.
    Proof.
      intros n.
      set (x := build_combine n H).
      dependent induction x. simpl. reflexivity.
      intros.
      simpl. destruct (f acc n x y). apply IHx. auto.
      reflexivity.
      reflexivity.
    Qed.

  End build.
End list_fold_i_sum_2.