Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Is there a name for this trick in programming with dependent types?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is there a name for this trick in programming with dependent types?


Chronological Thread 
  • From: Shengyi Wang <txyyss AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Is there a name for this trick in programming with dependent types?
  • Date: Fri, 1 Mar 2019 01:48:02 +0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=txyyss AT gmail.com; spf=Pass smtp.mailfrom=txyyss AT gmail.com; spf=None smtp.helo=postmaster AT mail-it1-f195.google.com
  • Ironport-phdr: 9a23:1wkbsxUYCma8arDvpqyWitLnVTrV8LGtZVwlr6E/grcLSJyIuqrYYxWEt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7YisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAfcBPelGqYn9qFsPrRqjDgasHuzvzDBIjWLx0K0m3OUgEQHH3Bc7H98Vv3TUqc/6NKYWUeyv0KbIyjDDYupQ1Dzg5obIdRUhruuNXbJ2acfRxkgvFx/FjlWNsoPpJS+a1uMIs2Wd8uFuVvqvhnY5pw1tpjWj3MQhh4nTio4Iy13J9D91zJsxKNC4TkNwfMSqH4FKty6AMot7WsMiTH9suCY90rAGvIS0fCkOyJg+xh7fd+GLf5GG4h7+UOucIS10hH1ieLK4iBay9VavxvfgWcmz1VZGtitFkt/SuXARzxHf9NSLR/9n8kqi2TuDzR3f5+BFLEwuiKbWL54szqY1lpUJsETDGiH2mF/xjK+Tbkgk5uep6uTnY7X9vZ+RLIB0igTkPaQvnsyzG/g3Mg8LX2SD4+SzyKXj/VHlQLVNlvA5jq7ZsInDKcsHoq65HhRa35046xe/CjemyM4XkWMGLFJDYhKHjpLmN0vAIPDiXr+DhAGnly4uzPTbNJXgBI/MJz7NiuTPZ7F4vnVcxQw83NEX2JtSBflVPOLiS1TqnNPdBx49dQezxrC0W51GyooCVDfXUeeiO6TIvArQv7N9E6y3fIYQ/Q3FBb0g7v/qg2U+nAZEL6as1JoTLnu/G6Y/ehnLUT/Xmt4EVFwykE8mVuWz0Q+NVDdSYzC5WKduvmhmWrLjNp/KQ8WWuJLE3Cq/GccINGVPC1TJEGuxMovdCqpKZyWVLcts1DcDUOr5Rg==

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



Archive powered by MHonArc 2.6.18.

Top of Page