The Coq mailing list

[Lily Chung <ikdc AT mit.edu>]

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