The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

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 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.

--------------------------------------------------------
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