The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Randy,

I am not sure this is an answer to your problem in its full generality
but regarding the difficulty of working in Coq with nested inductive
type like ptrm, I suggest you write a powerful dependent induction
principle by hand corresponding to your nested type. For instance,
this is what I would do in the case of ptrm:

Best regards,

Dominique

(****************************************************)

Require Import List.

Set Implicit Arguments.

(* The type of occurences in a list *)

Fixpoint Occ X (x : X) ll : Set :=
  match ll with
    | nil   => False
    | y::ll => ((x = y) + Occ x ll)%type
  end.

(* The nested elimination Scheme generated by Coq is too weak *)

Unset Elimination Schemes.

Inductive ptrm : Set :=
| ptRel : ptrm
| ptApp : ptrm -> list ptrm -> ptrm.

Set Elimination Schemes.

(* I suggest writing a much more powerful one like this dependent one *)

Section ptrm_rect.

  Variable P : ptrm -> Type.

  Hypothesis HP_Rel : P (ptRel).
  Hypothesis HP_App : forall a ll, P a -> (forall x, Occ x ll -> P x) ->
P (ptApp a ll).

  Fixpoint ptrm_rect t : P t.
  Proof.
    refine(
    match t return P t with
      | ptRel      => HP_Rel
      | ptApp a ll => HP_App _ (ptrm_rect a) _
    end).
    induction ll as [ | y ll IH ]; intros x.
    intros [].
    intros [ H | H ].
    subst x.
    apply ptrm_rect.
    apply IH, H.
  Defined.

  (* with the fixpoint equations that are crucial if you want to
     program (and not just prove) with the recursion principle *)

  Hypothesis HP_App_ext : forall a ll pa f1 f2,
        (forall x Hx, f1 x Hx = f2 x Hx)
     -> @HP_App a ll pa f1 = HP_App ll pa f2.

  Fact ptrm_rect_Rel_fix : ptrm_rect ptRel = HP_Rel.
  Proof. reflexivity. Qed.

  Fact ptrm_rect_App_fix a ll :
            ptrm_rect (ptApp a ll)
          = HP_App ll (ptrm_rect a) (fun t _ => ptrm_rect t).
  Proof.
    simpl.
    apply HP_App_ext.
    clear a; intros a Ha.
    induction ll; destruct Ha; simpl; subst; auto.
  Qed.

End ptrm_rect.

Section ptrm_recursion.

  (* the particular case when the output type does not depend on the ptrm
     is usually easier to work with, if the full dependent principle is not
     required

     the extensionality assumption fades away
   *)

  Variables (Y : Type)
            (y : Y)
            (f : ptrm -> list ptrm -> Y -> list Y -> Y).

  Definition ptrm_recursion : ptrm -> Y.
  Proof.
    apply ptrm_rect.
    exact y.
    intros x ll Hx Hll.
    apply (f x ll Hx).
    clear x Hx f.
    induction ll as [ | x ll IH ].
    exact nil.
    apply cons.
    apply Hll with x; left; auto.
    apply IH.
    intros a Ha; apply Hll with a; right; assumption.
  Defined.

  (* these are the fixpoint equations you want *)

  Fact ptrm_recursion_Rel_fix : ptrm_recursion ptRel = y.
  Proof.
    simpl; auto.
  Qed.

  Fact ptrm_recursion_App_fix a ll :
      ptrm_recursion (ptApp a ll)
    = f a ll (ptrm_recursion a) (map ptrm_recursion ll).
  Proof.
    unfold ptrm_recursion at 1.
    rewrite ptrm_rect_App_fix.
    f_equal.
    induction ll; simpl; f_equal; auto.
    clear a ll.
    intros a ll pa f1 f2 H12.
    f_equal.
    induction ll; simpl; f_equal; auto.
  Qed.

End ptrm_recursion.

(* now you can use the ptrm_recursion principle to write your size
function *)

Definition ptrmSize (t:ptrm) : nat.
Proof.
  induction t as [ | a ll IHa IHll ] using ptrm_recursion.
  exact 1.
  exact (S (IHa + fold_left (fun x y => x + y) IHll 0)).
Defined.

(* and prove the two fixpoint equations that you need for this size
function *)

Fact ptrmSize_Rel_fix : ptrmSize ptRel = 1.
Proof. auto. Qed.

Fact fold_left_map_plus X (f : X -> nat) ll n : fold_left (fun x y => x
+ y) (map f ll) n = fold_left (fun x y => x + f y) ll n.
Proof.
  revert n; induction ll; intros n; simpl; f_equal; auto.
Qed.

Fact ptrmSize_App_Fix a ll : ptrmSize (ptApp a ll) = S (ptrmSize a +
fold_left (fun x y => x + ptrmSize y) ll 0).
Proof.
  rewrite <- fold_left_map_plus.
  unfold ptrmSize at 1.
  apply ptrm_recursion_App_fix.
Qed.






On 06/20/2016 12:46 PM, Randy Pollack wrote:
> Consider the well known contrasting approaches to definition:
> 
> Inductive ptrm : Set :=
> | ptRel : ptrm
> | ptApp : ptrm -> list ptrm -> ptrm.
> 
> Inductive Trm : Set :=
> | TRel  : Trm
> | TApp  : Trm -> Trms -> Trm
> with Trms : Set :=
> | tnil  : Trms
> | tcons : Trm -> Trms -> Trms.
> 
> It is possible to directly define a size function for both definitions
> of terms, e.g.
> 
> Function ptrmSize (t:ptrm) : nat :=
>   match t with
>     | ptRel => 1
>     | ptApp fn args =>
>       S (ptrmSize fn +
>         (fold_left (fun x y => x + ptrmSize y) args 0))
>   end.
> 
> Function TrmSize (t:Trm) : nat :=
>   match t with
>     | TRel => 1
>     | TApp fn args => S (TrmSize fn + TrmsSize args)
>   end
> with TrmsSize (ts:Trms) : nat :=
>        match ts with
>          | tnil => 0
>          | tcons u us => (TrmSize u + TrmsSize us)
>        end.
> 
> BUT, the definition of ptrmSize in Coq (8.5pl1) is not able to
> mechanically generate a functional induction principle, while the
> definition of TrmSize is able to generate a functional induction
> principle.
> 
> Is there a definition of size for ptrm that can mechanically generate
> a functional induction principle?  (I insist on "mechanically
> generate" because my real application is much bigger than this
> example, and I'm interested in functions other than "size".)
> 
> I know of one way to do it: recurse over something different than the
> term structure.  E.g. use a "fuel" parameter:
> 
> Function ptrmSize' (n:nat) (t:ptrm) {struct n} : option nat :=
>   match n with
>     | 0 => None
>     | S n => match t with
>                | ptRel => Some 1
>                | ptApp fn args =>
>                  match ptrmSize' n fn, ptrmsSize n args with
>                    | Some x, Some y => Some (S (x + y))
>                    | _, _ => None
>                  end
>              end
>   end
> with ptrmsSize (n:nat) (ts:list ptrm) {struct n} : option nat :=
>        match n with
>          | 0 => None
>          | S n => match ts with
>                     | nil => Some 0
>                     | cons u us =>
>                       match ptrmSize' n u, ptrmsSize n us with
>                         | Some x, Some y => Some (x + y)
>                         | _, _ => None
>                       end
>                   end
>        end.
> 
> Does anyone know a cleaner way?
> 
> Thanks,
> Randy
>