The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

 Hi Norman,

The general problem here is you do want to have full control over your proof term if proofs are relevant. In particular, when you invoke tactics, you will lose such control. At the very least, you want to finish the existential part first, then use proof mode to handle prop.

In my opinion, to define this function and lemma, there is no need to invoke K or anything. I suppose that if you can define tail by unpacking the subset type first, and then do recursion on the list directly, your lemma should be easier to prove, as the usage of the size information becomes quite limited and should not stand in your way when you establish the lemma.

Thanks,
Jason Hu

On Feb 5, 2019 04:59, Norman Rink <norman.rink AT tu-dresden.de> wrote:

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