coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] existT

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] existT
Date: Tue, 1 Oct 2019 07:57:05 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=YPvU8xKbHXLFmODuACJJfZ6YlWtaI6E9sALrWAcm+zw=; b=gQOfi8TPPxEvkyq5y7dy3j1Jexqgwn8cpwUD3KuKm3/WiYWj8u5Fua8HunpjavJg7dXg9aXHKKGyaokfY7TRuxvr5K+E3wAqVahzmPwIfrt8jc/OHOr/KavO3pTJqmH9yPh0AkEn4KlBAwSATatBESMlE9552L8gb/SJag/qrXWLRHfzlh8q681Wi3VNhIjP3R20kk9kxPvVjizTU5YTCxWcTKovYOjqHVgdpgqCkaQ4dxRdYzwKK4GVDa8qbFgdNx7gL/eOlU3cxp5VqZY4+zk9zqZnvA8JudsZryqVn/QHXASF8ovJjHMYwkyi9oJ4BAVbJ/Ef/Qv0dN/AmCMDuQ==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=PhiuX4vny4pSL9F48K2EZFsh/7Gzv91KS1SKsgyUAXXjtLQbMH1Ndo9gWqHXaadhxhhGNhjZaqssje3xEdvMYUwhr8od2ziuhyHLrb3PNofhQRC/8R9APySbp9s80pGa67XLAL+D+xKjJexX4TPMzg/IxQhR9YqOWb40UqP1MEx2gNLoGAhXgxSVtF0dEM2lFqwC1zyQqQCXB4pWrrP2dSFQGZfZpXc3hqAgd6F1MK+j+1YLYH96sZECKYPAULxOtJ63PtF24vFTJSmTBmvAEioUM29HsuB2KaRDTw06f1hdlfgAeSTLRPXfTsqT1DxdQ7SaRhjtefqj+6vUlTtDHg==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:s9tncx1GBDHo6yRbsmDT+DRfVm0co7zxezQtwd8ZseIeLvad9pjvdHbS+e9qxAeQG9mCsLQY0KGP6fmocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbal9IRi4ogndq9cajZZ/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+jLxVrg+9pxJxwIDUYZ2aOvVxca7GYdMVXnBMUtpNWyBdAI6xaZYEAeobPeZfqonwv18AogWkBQayAePuyiJDiHHs0qw0yOQhFgfG1xEnEtwKrnvUtsv6NKISUOyvwqfH1zvCb+hR2Tf784XHaBYhoeyWUb1ubMXR1FMjGBnYjliJr4HuIjCb1vwVvmWU8+ZsT/+jh3Ilpg1rvzSiyMUhhpPUio8byl3I7Th1zYYpKdGiVkJ3fdCpHIFOuy2HK4d6WN4uTm9stSoixL0Jp522cDQPxZkixBPTdvyKfJON7x/jTumePCp0iXdqdb2hnBm9702txffiWcWpzFlHqDdOnMPWuXAXzRPT79CKSvtj8Uel3jaCzxze5e9ZL0woiKbXMoMvzbw+m5YKtkTMBTH5lF/xjK+LakUr4e+o6/nhYrr7vJOcL5V0igbiMqswhsO/HeU4Mg8IX2SB/uS8yaHj/Un+QLVNjf06iLXWsJffJcgDp665BRFa0po75huwEzuqyskUkWUFIV5fZR6KgYrkN0vTLP32Dfqzm1Gsny1qx/DCML3hGJLNLn3bnbnlY7l98VBTyA8zzNxF6ZxbEL8AIOn0Wk/3r9HXFBk5MxGuz+n5Fdp9y5kSVniSAqOBKqPdrUeI5v4zI+mLfIIapDH9K+E86/HyiX85hEQScLKy3ZoXbXC4Bu5pL1+YYXrqmNcBEH0FshAwTOzw2xW+VmsZbHGrGqk4+zsTCYS8DI6FSJrnyOiK2z7+FZlLbEhHDEqNGDHmbdPXde0LbXewL9Vsly1MebG+UIgnnUWMuRX3zqshAuPL4SoenZvlyZ546/CVnAxkpm88NNiUz2zYFzI8pWgPXTJjhPki83w48U+K1O1Du9IdFdFX4K8WAC4HDsaFitdLUJX1UA+HecqVQlG7RNngGSs2Ut86394JZQB6BsmmiRfAmSGtBu1Mzu3ZNNkP6qvZmkPJCYN4wnfC2rMmigB8EMJJKCurirM5/hWBXteVwXXcrL6jcOEn5ACI7H2KlDDctUdFFgN8TOPMQCJHaw==

Hi,

I have an inductive definition:

Inductive
in_dersrec (X : Type) (rules : rlsT X) (prems : X -> Type)
(concl : X) (d : derrec rules prems concl)
: forall concls : list X, dersrec rules prems concls -> Type :=
in_dersrec1 : forall (concls : list X) (ds : dersrec rules prems
concls),
in_dersrec d (dlCons d ds)
| in_dersrec2 : forall (concl' : X) (d' : derrec rules prems concl')
(concls : list X) (ds : dersrec rules prems concls),
in_dersrec d ds -> in_dersrec d (dlCons d' ds)

When I have a goal with
X0 : in_dersrec d ds
among the assumptions,
inversion X0. gives new assumptions

ds0 : dersrec rules prems concls
H0, H2 : p :: concls = ps
H3 : existT (fun x : list X => dersrec rules prems x)
(p :: concls) (dlCons d ds0) =
existT (fun x : list X => dersrec rules prems x) ps ds

What I would expect to get is also
dlCons d ds0 = ds

Whay do I get this strange assumption?

Furthermore, it seems that existT is a constructor for the inductive
definition of sigT. That being so, why doesn't injection H3
give that the respective arguments of the two occurrences of existT are
equal?

thanks for any help

Jeremy

[Coq-Club] existT, Jeremy Dawson, 10/01/2019
- Re: [Coq-Club] existT, Pierre Casteran, 10/01/2019
- Re: [Coq-Club] existT, Dominique Larchey-Wendling, 10/01/2019
  - Re: [Coq-Club] existT, Jeremy Dawson, 10/02/2019
    - Re: [Coq-Club] existT, Dominique Larchey-Wendling, 10/02/2019
      - Re: [Coq-Club] existT, Chris Dams, 10/02/2019
        
        Re: [Coq-Club] existT, Tom de Jong, 10/02/2019
        
        Re: [Coq-Club] existT, Jeremy Dawson, 10/16/2019
        
        Re: [Coq-Club] existT, Sylvain Boulmé, 10/16/2019
        Re: [Coq-Club] existT, Laurent Thery, 10/16/2019
        
        Re: [Coq-Club] existT, Matthieu Sozeau, 10/16/2019