The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Note that you can use a sort-of small inversions trick to make the definition more compact:

Definition ihd {n: nat} (l: ilist (S n)): A :=
match l in (ilist m) return (match m with O => True | S _ => A end) with
| Nil => I
| Cons _ h _ => h
end.

In fact, Coq is powerful enough to infer this, and the following works as well:

Definition ihd {n: nat} (l: ilist (S n)): A :=

  match l with

  | Cons _ h _ => h

  end.

Print ihd.

(* ihd =

fun (n : nat) (l : ilist (S n)) =>

match l in (ilist n0) return match n0 with

                             | 0 => IDProp

                             | S _ => A

                             end with

| Nil => idProp

| Cons _ h _ => h

end

     : forall n : nat, ilist (S n) -> A

*)

On Thu, Feb 28, 2019, 13:15 Lily Chung <ikdc AT mit.edu> wrote:

Seems to me that this is exactly the convoy pattern, just with a different proposition than equality.

On Feb 28, 2019 12:48, Shengyi Wang <txyyss AT gmail.com> wrote:

Hi,

Inspired by the definition of addvect in https://github.com/coq-contribs/matrices/blob/master/operators.v , I made a definition of head for length-indexed lists as follows:

Require Import Coq.Arith.PeanoNat.

Section ilist.

  Variable A : Set.

  

  Inductive ilist : nat -> Set :=

  | Nil : ilist O

  | Cons : forall n, A -> ilist n -> ilist (S n).

  Definition ihd {n: nat} (l: ilist (S n)): A :=

    match l in (ilist m) return (O < m -> A) with

    | Nil => fun p => False_rect _ (Nat.nle_succ_0 _ p)

    | Cons _ h _ => fun _ => h

    end (Nat.lt_0_succ n).

End ilist.

This definition introduces an extra parameter "O < m"  in return clause and applies the whole match to the proof "(Nat.lt_0_succ n)" to eliminate the parameter. With this trick we can claim false for the impossible branch.

I'm curious if there is a name for this trick like the "convoy pattern" trick named in Adam Chlipala's "Certified Programming with Dependent Types".

Thank you very much,

Shengyi Wang

Cell: +65-83509639