Problem with recursion

[jwiegley]

Problem with recursion

[mattam82]

Indeed when doing a recursion, the relation has to be homogeneous, whereas here it depends on the arguments a tys dom and codom. One way to phrase your recursion is in terms of the subterm relation which allows to compare Term's of different indies, i.e.:

Derive Signature for Term.

Section assoc.  
  Context {a : nat} {tys : Vector.t (obj_idx * obj_idx) a}.

  Equations comp_assoc_simpl_rec {dom cod}
            (t : @Term a tys dom cod) : @Term a tys dom cod :=
  comp_assoc_simpl_rec t by rec (signature_pack t) (Term_subterm a tys) :=
  comp_assoc_simpl_rec (Comp f g) <= comp_assoc_simpl_rec f => {
    | Comp i j => Comp i (comp_assoc_simpl_rec (Comp j g));
    | x => Comp x (comp_assoc_simpl_rec g)
  };
  comp_assoc_simpl_rec x := x.

We put ourselves in a section where a and tys are fixed and do recursion on the packing of t with its indices dom and codom. You get obligations corresponding to the recursive calls in this case. However it is clearly not a structurally recursive definition as it is a case of nested recursion (you call recursively on Comp j g where j comes from a previous recursive call). In that case I'm afraid you have to do something more complicated along the lines of the following. You define an heterogeneous size measure and have to add a post-condition to your function, proving that it indeed always returns smaller or equal terms. For some reason the unfolding proof fails but can be easily done by hand. You'll get the elimination principle for that definition, that you can use to prove properties about the "less-dependent" one without the post-condition.

Derive Signature for Term.

Definition packed_term_size {a tys} (x : sigma _ (fun x => Term_sig a tys x)) :=
  term_size (x.(pr2)).

Section assoc.  
  Context {a : nat} {tys : Vector.t (obj_idx * obj_idx) a}.

  Equations comp_assoc_simpl_rec {dom cod}
            (t : @Term a tys dom cod) : sigma (@Term a tys dom cod) (fun t' => term_size t' <= term_size t) :=
  comp_assoc_simpl_rec t by rec (signature_pack t) (MR lt (@packed_term_size a tys)) :=
  comp_assoc_simpl_rec (Comp f g) <= comp_assoc_simpl_rec f => {
    | sigmaI (Comp i j) Hle => sigmaI _ (Comp i (comp_assoc_simpl_rec (Comp j g)).(pr1)) _;
    | sigmaI x Hle => sigmaI _ (Comp x (comp_assoc_simpl_rec g).(pr1)) _
  };
  comp_assoc_simpl_rec x := sigmaI _ x _.

  Require Import Omega.
  Next Obligation. red. unfold packed_term_size. simpl. omega. Defined.
  Next Obligation. red. unfold packed_term_size. simpl. omega. Defined.
  Next Obligation.
    destruct comp_assoc_simpl_rec_comp_proj. simpl. omega.
  Defined.
  
  Next Obligation.
    red. unfold packed_term_size. simpl. omega.
  Defined.
  
  Next Obligation.
    destruct comp_assoc_simpl_rec_comp_proj. simpl. omega.
  Defined.

  Next Obligation.
    red; unfold packed_term_size. simpl. omega.
  Defined.
  
  Next Obligation.
    destruct comp_assoc_simpl_rec_comp_proj.
    simpl. simpl in pr2. omega.
  Defined.
  
  Next Obligation.
    unfold comp_assoc_simpl_rec.
    Subterm.unfold_recursor.
    destruct t. reflexivity. reflexivity.
    simpl. 
    match goal with
      |- comp_assoc_simpl_rec_obligation_10 _ _ _ _ _ _ ?X =
        _ _ _ _ _ _ ?Y => change X with Y end.
    destruct (comp_assoc_simpl_rec t1).
    unfold comp_assoc_simpl_rec_obligation_10.
    simpl. 
    destruct pr1.
    simpl; reflexivity. reflexivity. reflexivity.
  Defined.
End assoc.

Definition comp_assoc_simpl {a} {tys} {dom cod}
           (t : @Term a tys dom cod) : @Term a tys dom cod :=
  (comp_assoc_simpl_rec t).(pr1).

[mattam82]

About the bug proper, we should raise an error indeed if the relation is not a closed term.

[mattam82]

Also, we could rather use subset types and Program to avoid the packing/unpacking but I wanted to show the encoding of the post-condition here.