The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

1: you shouldn't need the refine in the tail definition (tail of list of 
length 1 isn't special)

2: again in the definition of tail, if you swap "inversion e" and 
"exists x" the resulting proof term is much simpler as the first 
projection won't depend on the size proof. Then you won't need to 
destruct the identity later as it won't be blocking. Try Print-ing the 
lemma before and after the change to see what it affects.

If you know that S is injective you can also avoid using inversion while 
defining tail (inversion is known for producing ugly proof terms, this 
isn't a problem in regular proofs as you don't care about the terms but 
should be avoided when using Defined) and instead apply the injectivity 
proof (find it with Search (S _ = S _ -> _ = _)).

If for some reason you really have to prove something where an equality 
blocks you, you may want to look into working with relevant identities. 
For this learn to use HoTT (the parts which don't rely on the HoTT 
axioms can be used in any Coq development). This is nontrivial.

Gaëtan Gilbert

On 05/02/2019 10:59, Norman Rink 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