The Coq mailing list

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

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