The Coq mailing list

[Jim Apple <coq-club AT jbapple.com>]

(*

Adam Megacz wrote:

> In particular it's very hard to use "refine" on these
> nested-fix terms and still pass the final structurally-decreasing check
> -- I'm even starting to suspect the check is slightly stricter when
> using tacticals, or that there's a special exception for nested fix that
> isn't being allowed when building a term using tactics.

I'm encountering something that might be related. (v8.2 from SVN HEAD
in February or so) For the same type of datatype ("inductive types
which have a constructor which takes a polymorphic container (tree,
list, etc) instantiated at the type being defined"), I'm using
auxiliary functions instead of the nexted fix trick:

*)

Set Implicit Arguments.
Require Import List.

Section Over.

Variable A:Type.
Variable NAT:Type.

(* A B+ tree with size annotations: *)

Inductive FullTree :=
  Leaf : A -> FullTree
| Branch : NAT -> list (FullTree * A) -> FullTree.

(* A fold for lists with distinct nil and singleton cases: *)

Definition childReduce (S T U:Type)
  (reduce:S -> U ->T)
  (zero:T)
  (more:T -> T -> T)
   :=
  fix help (xs:list (S*U)) : T :=
  match xs with
    | nil => zero
    | (y,b)::nil => reduce y b
    | (y,b)::ys => more (reduce y b) (help ys)
  end.

(* A fold for FullTrees: *)

Definition treeReduce (T:Type)
  (leaf:A -> option A -> T)
  (branch:NAT -> T -> option A -> T)
  (zero:T)
  (more:T -> T -> T) :=
  fix help (x:FullTree) (b:option A) : T :=
  match x with
    | Leaf v => leaf v b
    | Branch n c =>
      let helper x y := help x (Some y)
        in branch n (childReduce helper zero more c) b
  end.

(* An example of the usage of treeReduce: *)

Definition toList :=
  treeReduce
  (fun x _ => cons x nil)
  (fun _ x _ => x)
  nil
  (@app _).

(* I want to prove things about the results of childReduce: *)

Definition childInductStmt :=
    forall S T U (P:list (S*U) -> T -> Prop) reduce zero more,
    P nil zero ->
    (forall y b, P ((y,b)::nil) (reduce y b)) ->
    (forall y b z zs res,
      P (z::zs) res -> P ((y,b)::z::zs) (more (reduce y b) res)) ->
    forall xs, P xs (childReduce reduce zero more xs).

(* A proof using just tactics: *)

Lemma childInduct : childInductStmt.
Proof.
  intros S T U P reduce zero more pzero preduce pmore.
  induction xs.
  simpl; assumption.
  destruct xs.
  simpl. destruct a. apply preduce.
  simpl. destruct a.
  apply pmore.
  (* note how weak the IH is here *)
  simpl in IHxs.
  apply IHxs.
Qed.

(* A proof using refine + tactics. Is refine giving a stronger IH than
can be justified? *)

Lemma childInductRefine : childInductStmt.
Proof.
  unfold childInductStmt.
  refine
    (fun S T U (P:list (S*U) -> T -> Prop) reduce zero more
      pzero preduce pmore =>
      fix help xs :=
      match xs as xs' return P xs' (childReduce reduce zero more xs') with
        | nil => pzero
        | (y,b)::nil => preduce y b
        | (y,b)::z::zs => pmore _ _ _ _ _ _
      end).
  (* The IH 'help' looks much too strong here *)
  pose (help (z :: zs)) as ans.
  unfold childReduce in ans.
  (*Guarded.*)
Abort.

End Over.

(* To my eye, this looks like refine is being more optimistic than I expect. 
*)