Why can I sometimes prove a goal via a lemma, but not directly?

Question

Consider the function defined below. It's not really important what it does.

Require Import Ring.
Require Import Vector.
Require Import ArithRing.

Fixpoint
  ScatHUnion_0 {A} (n:nat) (pad:nat) : t A n -> t (option A) ((S pad) * n).
 refine (
  match n return (t A n) -> (t (option A) ((S pad)*n)) with
  | 0 => fun _ =>  (fun H => _)(@nil (option A))
  | S p =>
    fun a =>
      let foo := (@ScatHUnion_0 A p pad (tl a)) in
      (fun H => _) (cons _ (Some (hd a)) _ (append (const None pad) foo))
  end
   ).
 rewrite  <-(mult_n_O (S pad)); auto.
 replace  (S pad * S p) with ( (S (pad + S pad * p)) ); auto; ring.
Defined.

I want to prove

Lemma test0:  @ScatHUnion_0 nat 0 0 ( @nil nat) = ( @nil (option nat)).

After doing

  simpl. unfold eq_rect_r. unfold eq_rect.

the goal is

         match mult_n_O 1 in (_ = y) return (t (option nat) y) with
         | eq_refl => nil (option nat)
         end = nil (option nat)

When trying to finish it off with

  apply trans_eq with (Vector.const (@None nat) (1 * 0)); auto.
  destruct (mult_n_O 1); auto.

the destruct doesn't work (see below for error message). However, If I first prove exactly the same goal in a lemma or even with assert inside the proof, I can apply and solve it, like this:

Lemma test1:  @ScatHUnion_0 nat 0 0 ( @nil nat) = ( @nil (option nat)).
  simpl. unfold eq_rect_r. unfold eq_rect.

  assert (
      match mult_n_O 1 in (_ = y) return (t (option nat) y) with
        | eq_refl => nil (option nat)
      end = nil (option nat)
    ) as H.
  {
    apply trans_eq with (Vector.const (@None nat) (1 * 0)); auto.
    destruct (mult_n_O 1); auto.
  }
    apply H.
Qed.

Can someone explain why this is, and how one should think about this situation when one encounters it?

In Coq 8.4 I get the error

      Toplevel input, characters 0-21:
      Error: Abstracting over the terms "n" and "e" leads to a term
      "fun (n : nat) (e : 0 = n) =>
       match e in (_ = y) return (t (option nat) y) with
       | eq_refl => nil (option nat)
       end = const None n" which is ill-typed.

and in Coq 8.5 I get the error

      Error: Abstracting over the terms "n" and "e" leads to a term
      fun (n0 : nat) (e0 : 0 = n0) =>
      match e0 in (_ = y) return (t (option nat) y) with
      | eq_refl => nil (option nat)
      end = const None n0
      which is ill-typed.
      Reason is: Illegal application: 
      The term "@eq" of type "forall A : Type, A -> A -> Prop"
      cannot be applied to the terms
       "t (option nat) 0" : "Set"
       "match e0 in (_ = y) return (t (option nat) y) with
        | eq_refl => nil (option nat)
        end" : "t (option nat) n0"
       "const None n0" : "t (option nat) n0"
      The 2nd term has type "t (option nat) n0" which should be coercible to
       "t (option nat) 0".

larsr larsr · Accepted Answer · 2015-06-08T12:01:52

@Vinz answer explained the reason, and suggested Set Printing All. which shows what the difference is. The problem was that simpl. simplified the return type of the match. Using unfold ScatHUnion_0. instead of simpl. enabled me to use the destruct directly on the goal.

Fundamentally, my troubles stemmed from me wanting to convince the type system that 0=0 is the same as 0=1*0. (Btw, I still don't know the best way to do this.) I was using mult_n_O to show that, but it is opaque, so the type system couldn't unfold it when checking that the two types were equal.

When I replaced it with my own Fixpoint variant (which is not opaque),

Fixpoint mult_n_O n: 0 = n*0 :=
    match n as n0 return (0 = n0 * 0) with
  | 0 => eq_refl
  | S n' => mult_n_O n'
  end.

and used it in the definition of ScatHUnion_0, the lemma was trivial to prove:

Lemma test0:  @ScatHUnion_0 nat 0 0 ( @nil nat) = ( @nil (option nat)).
  reflexivity.
Qed.

Additional comment:

Here is a proof that works with the original opaque mult_n_O definition. It is based on a proof by Jason Gross. It manipulates the type of mult_n_O 1 to be 0=0 by using generalize. It uses set to modify the term's implicit parts, such as the type in eq_refl, which is only visible after the Set Printing All. command. change can also do that, but replace and rewrite don't seem to be able to do that.

Lemma test02:
  match mult_n_O 1 in (_ = y) return (t (option nat) y) with
    | eq_refl => nil (option nat)
  end = nil (option nat).
Proof.
  Set Printing All.
  generalize (mult_n_O 1 : 0=0).
  simpl.
  set (z:=0) at 2 3.
  change (nil (option nat)) with (const (@None nat) z) at 2.
  destruct e.
  reflexivity.
Qed.

Update: Here is an even simpler proof thanks to the people at coq-club.

Lemma test03:
  match mult_n_O 1 in (_ = y) return (t (option nat) y) with
    | eq_refl => nil (option nat)
  end = nil (option nat).
Proof.
  replace (mult_n_O 1) with (@eq_refl nat 0);
  auto using Peano_dec.UIP_nat.
Qed.

Why can I sometimes prove a goal via a lemma, but not directly?

2 Answers