The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The shortish version (I'll let someone else fill in the details):
1. The guard condition changed from 8.4 to 8.5, to eliminate the inconsistency with propositional extensionality (in early enough versions of 8.4, you can prove [(forall P Q : Prop, (P <-> Q) -> P = Q) -> False], which is bad)
2. To get Coq v8.5 to accept {struct pt1}, pass [merge_partial_tuple pt1_tail] into your inner match statement, rather than passing in [pt1_tail] (that is, note that you apply [merge_partial_tuple] to [pt1_tail'] in both branches of the match inner, and do common subexpression elimination to bring the application out of the inner match)
3. Coq will only reduce applications of fixpoints that have a constructor in their structural position.  Suppose it did otherwise, and consider the following function:
Fixpoint id (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n' => S (id n')
  end.
What is the normal form of [fun n => id n]?  If Coq can unfold (well, beta-reduce) fixpoints applied to variables, then this term would have an infinite normal form!
4. There is a way to fix your proof with the new definition.  The most systematic way to do this is to write a lemma that lets you reduce your fixpoint a single step: prove that your fixpoint is equal to it's body by destructing pt2, and then rewrite with that lemma in the theorem you're trying to prove.

-Jason

On Wed, Oct 26, 2016, 7:41 AM Hendrik Tews <hendrik AT askra.de> wrote:

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 ====================================================