The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I am wondering what is a good approach to trying to prove some things like 
this:

Require Import Vector.
Require Import ArithRing.

Program Fixpoint ScatHUnion_0 {A} {n:nat} (pad:nat): t A n -> t (option A) 
((S pad)*n) :=
  match n return (t A n) -> (t (option A) ((S pad)*n)) with
  | 0 => fun _ => @nil (option A)
  | S p => fun a => cons _ (Some (hd a)) _ (append (const None pad) 
(ScatHUnion_0 pad (tl a)))
  end.
Next Obligation.
  ring.
Defined.

(This definition works only under Coq 8.5. Under 8.4 I had to define it 
differently).
I stuck proving the following trivial lemma:

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

I could not get much further than:

test0 < compute.
1 subgoal

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

Any suggestions how to deal with proving constructs like this?
Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva