The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le mardi 06 mars 2007 00:20, Sean Wilson a écrit :
> Hi,
Hi,

> Given the usual definition for lists indexed by length:
>
> Inductive vect [A:Set] : nat -> Set :=
>
> | nil : (vect A O)
> | cons : (x:A)(n:nat)(vect A n)->(vect A (S n)).
>
> Can anyone explain what the difference is between using terms of this type
> and terms of type {x:list A | length = n}, particularly in the domain of
> writing certified programs (e.g. in the specification of a
> head/tail/take/append function)? When and why would you pick one
> representation over the other?

They're equivalent representations in Coq, i.e. you can easily build
vect A n <-> {x : list A | length x = n}.

Extraction-wise they're different as in the first case you will have the 
length of the sublist appearing at each cons node while in the second version 
it won't appear in the list structure ; rather, each list will be accompanied 
by its length (other systems allow one not to keep the index during 
conversion and/or extraction, so this may be a moot point). 

Specification-wise it can certainly be argued that one or the other is the 
most elegant but the real problem is that Coq has no built-in support for
either styles, especially it lacks built-in heterogeneous equality hence you 
can't write " v : vect (n + 0), v': vect n |- v = v' ", while " v JMeq v' " 
is OK and in contexts where "n + 0 = n" you will be able to get the leibniz 
equality out. Similarly, it has no intrinsic support for subsets hence you're 
forced to write proof-modifying code, which is almost always ugly and 
impratical. So if you need to stay in Coq proper i would advise using the 
good old simple types specification style instead.
        
<publicity length="long">
  Using the Program vernacular, the situation changes a bit:

  When using subsets with the Program vernacular, you will be able to write:

 Program Fixpoint app (l : list A) (l' : list A) { struct l } :
    { r : list A | length r = length l + length l' } :=
    match l with
      | nil => l'
      | hd :: tl => hd :: (tl ++ l')
    end 
    where "x ++ y" := (app x y).
   
  Next Obligation.
    destruct_call app ; subtac_simpl.
  Defined.  
  
  Program Lemma app_id_r : forall x (l : { l : list A | length l = x }), 
        (`l) = app l nil.
    intros.
    subtac_simpl.
    induction x0 ; simpl ; auto.
    rewrite <- IHx0 ; reflexivity.
  Qed.

  This works because we are comparing vectors as if they were lists, ignoring 
the index (` is the first projection for subset types). On the other hand, 
Program also has support for working with dependent inductives, you can have 
for example:

Set Implicit Arguments.

Variable A : Type.

(* Inverse vectors *)
Inductive tcev : nat -> Type :=
| vnil : tcev 0
| vcons : forall n, tcev n -> A -> tcev (S n).

Program Fixpoint app (n : nat) (v : tcev n) (m : nat) (v' : tcev m) { struct 
v' } : tcev (n + m) :=
  match v' with
    | vnil => v
    | vcons n'' v'' x => app (vcons v x) v'' 
  end.

This definition can't be accepted by the Fixpoint command because in the 
first 
case v is of type "tvec n" while something of type "tvec (n + ?)" is 
required. Program solves the problem by adding the appopriate coercions here, 
and begs for a proof that " m = 0 -> JMeq v' vnil -> n = n + m " which is 
trivially solved.

Now, you need to use heterogeneous equality to relate objects of type tcev:

Require Import JMeq.
Require Import Coq.subtac.Utils.

Lemma app_id_r_JMeq : forall n (v : tcev n), JMeq (app v vnil) v.
Proof.
  intros.
  induction v ; simpl ; auto ; elim_eq_rect ; simpl ; auto.
Qed.

Alternatively you can define:

Program Definition app_id_r_stmt (n : nat) (v : tcev n) := app v vnil = v.

Here a coercion is applied to v to put it in the 'tcev (n + 0)' type.

Lemma app_id_r : forall n (v : tcev n), app_id_r_stmt v.
Proof.
  red ; simpl ; intros.
  elim_eq_rect.
  rewrite (proof_irrelevance _ t (app_id_r_stmt_obligation_1 v)).
  reflexivity.
Qed.

In this second case, you will need to use proof irrelevance and elimination 
of 
eq_rect to use app_id_r as well. Actually, all this business require fiddling 
with eq_rect and proof-irrelevance (only PI for subsets) which is not very 
nice but can surely be better automated. On another note, it becomes 
impossible to compute when using dependently typed functions where coercions 
appear because of the irreducible eq_rect calls. OTOH, you can usually 
compute with functions using subset types when using a lazy strategy.

My small experience with this is that subsets are good for 
pre/post-conditions 
and pushing invariants on subojects in datastructures while dependent 
inductives shine when you need 'whole-structure' indexes and use 
index-modifying operations. 

Disclaimer: anything may change in Program and support for dependent 
inductive 
types is only available using the current svn version (which may be broken as 
well).

Sorry for the long answer but I think it might be useful to others as well. 
</publicity>

-- 
Matthieu Sozeau
http://www.lri.fr/~sozeau