Induction principles for "exotic" functions

[Thomas Braibant-2]

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.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Pierre Courtieu-3]

Hello,

Have you tried the induction scheme given by Function?

 Function list_fold_i_sum_2 (i:nat) (acc:Z) (lx:list X) (ly:list Y) {struct lx}: 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.

See for example list_fold_i_sum_2_ind. It is a bit hard to read because it contains a lot of equalities, but it is generally useful for reasoning about functions.

Cheers,
Pierre Courtieu

PS I removed some "_" from inl and inr, that my version of coq was complaining about.

2009/10/19 Thomas Braibant <thomas.braibant@...>

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.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Thomas Braibant-2]

Hi,

> Have you tried the induction scheme given by Function?

Indeed, I had tried the inductions scheme given by Function, which was
quite hard to read, and to use. My question was more something like :
is this Function scheme complicated because it need to be that
complicated to be powerful enough, or is it as powerful as the
induction scheme combine_ind given by the inductive combine, which is
much simpler (to read and apply) ?

I think there is also a difference in proof strategies between these
two versions: using the Function's scheme, you will not see
list_fold_i_sum_2 in the subgoals nor in your induction hypotheses,
while using combine_rec, you are doing an induction on the underlying
datastructure, and you rely on the fact that you can reduce (using
Coq's reduction or rewriting) the function to apply your induction
hypothesis. Is one better than the other ?

>
> 2009/10/19 Thomas Braibant <thomas.braibant@...>
>>
>> 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.
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.saclay.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>          http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Pierre Courtieu-3]

Hello,

Well I am not sure of the difference between both principles. The functional principle is built from a graph built from the function, which is very similar to your combine (with more equalities).

However, typing:

functional induction (list_fold_i_sum_2 i acc lx ly).

is not that hard!

The principle is a bit complex because it keeps track of all case splitting equalities. This is useful to see were you are in the tree, and It is also very important too keep equalities when case splitting is done on non variable terms.

However, if you do "functional induction...;subst". Then the subgoals should be quite easy to read.

The functional principle takes the function into account.

For example:

Function div2 (n:nat) : nat :=
  match n with
  | O => 0
  | S O => 0
  | S (S n') => S (div2 n')
  end.
Check
div2_ind
     : forall P : nat -> nat -> Prop,
       (forall n : nat, n = 0 -> P 0 0) ->
       (forall n : nat, n = 1 -> P 1 0) ->
       (forall n n' : nat,
        n = S (S n') -> P n' (div2 n') -> P (S (S n')) (S (div2 n'))) ->
       forall n : nat, P n (div2 n)

As you can see, the property P takes (div2 n) as an argument, so it is easy to prove things about it.

Notice that you also get list_fold_i_sum_2_equation for free if you prefer rewriting instead of reducing.

Function has drawbacks: dependently typed functions are not well treated yet (unless structurally decreasing of course). But here I don't see any problem to use it.

Can you give us some examples of properties you want to prove on this function please?

Cheers,
Pierre

2009/10/20 Thomas Braibant <thomas.braibant@...>

Hi,

> Have you tried the induction scheme given by Function?

Indeed, I had tried the inductions scheme given by Function, which was
quite hard to read, and to use. My question was more something like :
is this Function scheme complicated because it need to be that
complicated to be powerful enough, or is it as powerful as the
induction scheme combine_ind given by the inductive combine, which is
much simpler (to read and apply) ?

I think there is also a difference in proof strategies between these
two versions: using the Function's scheme, you will not see
list_fold_i_sum_2 in the subgoals nor in your induction hypotheses,
while using combine_rec, you are doing an induction on the underlying
datastructure, and you rely on the fact that you can reduce (using
Coq's reduction or rewriting) the function to apply your induction
hypothesis. Is one better than the other ?

>
> 2009/10/19 Thomas Braibant <thomas.braibant@...>
>>
>> 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.
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.saclay.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>          http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>