The Coq mailing list

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

Btw, a usefull application of the dependent induction principle
is the decidability of equality over ptrm for instance:

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

Definition list_eq_dec X (ll mm : list X) : (forall x y, Occ x ll -> Occ
y mm -> { x = y } + { x <> y }) -> { ll = mm } + { ll <> mm }.
Proof.
  revert mm; induction ll as [ | x ll IH ]; intros [ | y mm ] IHll.
  left; auto.
  right; discriminate.
  right; discriminate.
  destruct (IHll x y) as [ | C ].
  left; auto.
  left; auto.
  2: right; contradict C; injection C; auto.
  subst y.
  destruct IH with (mm := mm) as [ | C ].
  intros; apply IHll; right; auto.
  left; subst; auto.
  right; contradict C; injection C; auto.
Qed.

Definition ptrm_eq_dec (s t : ptrm) : { s = t } + { s <> t }.
Proof.
  revert t; induction s as [ | a ll IHa IHll ] using ptrm_rect.
  intros [ | ]; [ left | right ]; auto; discriminate.
  intros [ | b mm ].
  right; discriminate.
  destruct (IHa b) as [ | C ].
  2: right; contradict C; injection C; auto.
  subst b.
  destruct (list_eq_dec ll mm) as [ | C ].
  intros; apply IHll; auto.
  2: right; contradict C; injection C; auto.
  left; subst; auto.
Qed.

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

On 06/20/2016 03:29 PM, Dominique Larchey-Wendling wrote:
> 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
>>
>