coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Cell: +65-83509639
- [Coq-Club] Is there a name for this trick in programming with dependent types?, Shengyi Wang, 02/28/2019
- Re: [Coq-Club] Is there a name for this trick in programming with dependent types?, Lily Chung, 02/28/2019
- Re: [Coq-Club] Is there a name for this trick in programming with dependent types?, Jason Gross, 02/28/2019
- Re: [Coq-Club] Is there a name for this trick in programming with dependent types?, Lily Chung, 02/28/2019
Archive powered by MHonArc 2.6.18.