The Coq mailing list

[Norman Rink <norman.rink AT tu-dresden.de>]

Dear Coq-club,

I am relatively new to Coq. While I feel comfortable with “pedestrian”-style 
Coq developments – by which I mean specifying comparably simply-typed 
functions in Gallina and proving theorems about these functions outside of 
the definitions – I am now trying to use Coq/Gallina more effectively by 
writing dependently-typed functions (hoping that this will save some 
outside-of-definitions proof effort).

In this context, I would like to introduce my own tuples, i.e. lists of fixed 
finite length. For these tuples, I then want to introduce “typical” list 
functions like ‘append’, ‘tail’ etc. My tuple definition and ‘tail’ function 
appear below.

Definition MyTuple (n:nat) := { l:list nat | length l = n }.

Definition tail {n:nat} : MyTuple (S n) -> MyTuple n.
Proof.
  refine(match n with
           | 0    => fun _ => exist _ [] eq_refl
           | S n' => fun t => _
         end).
  destruct t.
  destruct x.
    inversion e.
    inversion e. exists x. reflexivity.
Defined.

Since the definition of ‘tail’ is a little non-transparent (and the code for 
the proof is quite cryptic – try printing it), I am compelled to verify that 
my ‘tail’ function behaves as expected. This means I want my taking-the-tail 
operation to commute with projecting the list out of ‘MyTuple’, i.e.:

Lemma tail_correct : forall (n:nat) (t:MyTuple (S n)),
  proj1_sig (tail t) = tl (proj1_sig t).

When attempting to prove this lemma (by induction on n), I run into the 
problem that I would like to “destruct” an equality proof ‘e’:

e : length (n0 :: x) = S (S n)

The only constructor for ‘e’ is of course ‘eq_refl’, but I cannot seem to 
convince Coq of this since ‘eq_refl’ has type ‘x = x’ while my ‘e’ from above 
is typed at ‘length (n0 :: x) = S (S n)’. I wonder if there is anything that 
I am obviously doing wrong.

I am aware of the discussion of similar looking issues in Chapter 10 of the 
CPDT book. http://adam.chlipala.net/cpdt/
However, the techniques from there (proof irrelevance, ’UIP’, ‘StreicherK’) 
do not quite seem to work for me since all of them eventually talk about 
proofs of ‘x = x’. (Heterogeneous equality ‘JMeq’ also does not seem to be a 
good fit since it appears that ‘JMeq’ can be put to use most effectively if 
it is indeed used at the same types eventually.)

In case anyone feels compelled to suggest I use finite-length vectors instead 
of subtypes of lists: I ultimately run into similar problems with equality 
between different types (not for the ‘tail’ function specifically but in 
attempted proofs of lemmas similar to “tail_correct” above). It would be 
great if I could somehow eliminate ‘eq_rec’/‘eq_rect’ from terms in my 
proofs, but I understand that this is a bit of a rush (wishful) fix.

Any help or pointers would be greatly appreciated. Many thanks.

Best regards,

Norman Rink



Dr. Norman Rink
Postdoctoral Researcher

Technische Universität Dresden 
Faculty of Computer Science
Chair for Compiler Construction
Helmholtzstrasse 18
Barkhausenbau, BAR III.59
01062 Dresden 

phone: +49 (0)351 463 43711
email: 
norman.rink AT tu-dresden.de
www: https://cfaed.tu-dresden.de/ccc-staff-rink