coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match
Date: Tue, 20 Aug 2019 14:59:13 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga03.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.2.0.6
Ironport-phdr: 9a23:PD47ixKmm16V8czfFdmcpTZWNBhigK39O0sv0rFitYgeLPzxwZ3uMQTl6Ol3ixeRBMOHsqgC0raP+P+xEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCejbb9oMRm7ohjdusYUjIZmN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqJFrhy8uxxxzY3aYI+XO/p/YqzSctwUSHFdXslKUyFNHp+wY5cNAucHIO1Wr5P9p1wLrRamCwWiGeTvxSFHhn/qx6061PwhHRnb1wInHtIBrHTUo8/rO6cWX+y+0a7FzTDCb/xK2Tfy8pbHchQ7rfGXWrJ/b8XRyVU1FwPCllWdso3lPzWJ1usTt2iX9fZvVeWqi2M+rQx6vzahxsApiobTh4IVzEjJ9SR/wIYpO9K4TFR3bsO6H5ZWqiqUNJN2T9s/T2xmtys20KAKtJC0cSQQ1ZgqyR/SZ+aGfoWI+h7vSeecLDliiH9rdr+znQi+/Eakx+HmS8W500hGojJYntTNsn0BzQLf58iIR/dn4EutwzSC2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmEX5lqCaaksp9vKp6+ThfrXpuJucO5VohQH5N6Qigs2/AeImPQgSR2WX5Oqx2bL58UHkTrhHgec6nrTXvZ3bP8gWp660DxdQ0ok56ha/Czmm0M4fnXkCNF9FfROHgJTpO17UPv/4Ce2zg0+rkDh1yPDGIqfhApLVLnXYkbfhe6p95FBYyAYp0d9f4JdUBqkbIP3vQk/xqMDYDhghPgOoxObnEcxx2Z8aWWKSGaCUK7jSsF+N5uI3OeaAfo4VuDDnK/gk/fHil3E5mUVONZWuiNEcb2n9FfB7KW2YZ2Dti5EPCy1C6gE5VanhjECIeT9VfXe7GawmsGIVEoWjWM34QY2inKaGxGPzO5xdZmlLDhrERXLpfIWNVvNKcyWfLdN7lSQsVL69Rotn3har4lypg4F7J/bZr3VL/ano08J4srWKxEMCsAdsBsHY6FmjCmR9n2cGXTgzhfktoEphx1PF2q990aUBSY5joshRWwJ/DqbyivRgAomrCAPHYtqNDl2hR4f+WGxjfpcK29YLJn1FNZCigxTEhnX4BrAcz+fNBZoo/6aa1H/0dZ5w

Dear Laurent,

> and you don't need the return clause in this case :
>
> Fixpoint first_col {T : Type} {m n : nat} : @matrix T m (S n) -> matrix m 1
> :=

neat, very elegant! Also many thanks for the insightful explanation - very
helpful!

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match, Soegtrop, Michael, 08/20/2019
- Re: [Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match, Laurent Thery, 08/20/2019
  - Re: [Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match, Laurent Thery, 08/20/2019
    - RE: [Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match, Soegtrop, Michael, 08/20/2019
    - RE: [Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match, Soegtrop, Michael, 08/21/2019
      - Re: [Coq-Club] Struggling to convert a simple Program Fixpoint using just induction and exact into a Fixpoint with match, Laurent Thery, 08/21/2019