The Coq mailing list

[Hendrik Tews <hendrik AT askra.de>]

Hi everybody,

I have a problem with updating a dependently typed function from
8.4 to 8.5 (see the source below). In 8.4, coq accepts the
definition of merge_partial_tuple with {struct pt1} and the proof
of the little lemma is very simple.

In 8.5, {struct pt1} is rejected, coq does not see anymore that
pt1_tail' and pt1_tail are identical.

First question: Is this an intended change?

However, in 8.5 the definition is accepted with {struct pt2}. For
this, I would say, coq has to infer that pt2 and pt2' are
identical, which does not seem to be a problem.

I don't care too much about the decreasing argument. My problem
is that with {struct pt2} the term

  merge_partial_tuple (counted_nil _) something

is not convertible to (counted_nil _). (This behavior is the same
in 8.4 and 8.5.) I would be grateful if somebody could tell me
why coq does not use the obvious first case in the pattern match
to reduce the term. Indeed,

  change (merge_partial_tuple (counted_nil (option nat)) pt) with
         (counted_nil (option nat)).

fails with "Not convertible.", which I really don't understand.

Thanks in advance,

Hendrik

==================== 8.4 version 
==============================================
Section Counted_list.
  Variable A : Type.
  Inductive counted_list : nat -> Type := (* lists of fixed length *)
    | counted_nil : counted_list 0
    | counted_cons : forall(n : nat), 
        A -> counted_list n -> counted_list (S n).
End Counted_list.

Definition partial_tuple(n : nat) : Type := counted_list (option nat) n.

(* this function should do
  [Some 0; Some 1; None] [None, Some 2; None] => [Some 0; Some 1; None]
*)
Fixpoint merge_partial_tuple{l : nat}(pt1 pt2 : partial_tuple l)
                                              {struct pt1} : partial_tuple l 
:=
  match pt1 in counted_list _  l1
    return partial_tuple l1 -> partial_tuple l1
  with
    | counted_nil  => fun _ => counted_nil _
    | counted_cons pl1 no1 pt1_tail => fun(pt2' : partial_tuple (S pl1)) =>
        match pt2' in counted_list _ l2
          return match l2 with
                   | 0 => nat (* impossible case *)
                   | S pl2 => partial_tuple pl2 -> partial_tuple (S pl2)
                 end
        with
          | counted_nil => 0 (* impossible case *)
          | counted_cons _ no2 pt2_tail => fun pt1_tail' =>
              match no1 with
                | Some n1 => counted_cons _ _ (Some n1) 
                               (merge_partial_tuple pt1_tail' pt2_tail)
                | None => match no2 with
                    | Some n2 => counted_cons _ _ (Some n2)
                                   (merge_partial_tuple pt1_tail' pt2_tail)
                    | None => counted_cons _ _ None
                                   (merge_partial_tuple pt1_tail' pt2_tail)
                  end
              end
        end pt1_tail
  end pt2.

Lemma merge_partial_tuple_nil :
  forall(pt : partial_tuple 0),
    merge_partial_tuple (counted_nil _) pt = (counted_nil _).
Proof.
  intros pt.
  simpl.
  reflexivity.
Qed.
==================== end 8.4 version 
===========================================


======================= 8.5 version of merge_partial_tuple 
=====================
Fixpoint merge_partial_tuple{l : nat}(pt1 pt2 : partial_tuple l)
                                              {struct pt2} : partial_tuple l 
:=
  match pt1 in counted_list _  l1
    return partial_tuple l1 -> partial_tuple l1
  with
    | counted_nil _ => fun _ => counted_nil _
    | counted_cons _ pl1 no1 pt1_tail => fun(pt2' : partial_tuple (S pl1)) =>
        match pt2' in counted_list _ l2
          return match l2 with
                   | 0 => nat (* impossible case *)
                   | S pl2 => partial_tuple pl2 -> partial_tuple (S pl2)
                 end
        with
          | counted_nil _ => 0 (* impossible case *)
          | counted_cons _ _ no2 pt2_tail => fun pt1_tail' =>
              match no1 with
                | Some n1 => counted_cons _ _ (Some n1) 
                               (merge_partial_tuple pt1_tail' pt2_tail)
                | None => match no2 with
                    | Some n2 => counted_cons _ _ (Some n2)
                                   (merge_partial_tuple pt1_tail' pt2_tail)
                    | None => counted_cons _ _ None
                                   (merge_partial_tuple pt1_tail' pt2_tail)
                  end
              end
        end pt1_tail
  end pt2.
======================= end 
====================================================