coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Speeding up inversion on large inductives

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Speeding up inversion on large inductives
Date: Thu, 10 Sep 2015 13:01:01 +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
Ironport-phdr: 9a23:zdTNwxJEuTNuBa1DMdmcpTZWNBhigK39O0sv0rFitYgULf3xwZ3uMQTl6Ol3ixeRBMOAu64C0rSd7vGocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC04LuiavvqtX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVG679ZuEzSaFSJDUgKWE8osPx/1GXRgyWo3AYT28+kxxSAgGD4gusDbnrtS6v/NF61SaGJ8ruCfgRWD+i5qpvAle8jSYMNzc09CfMjcF/kLhcuDqgoQByx8jfZ4TDZ6k2Rb/UYd5PHTkJZc1WTSEUWo4=

Dear Enrico, Pierre,

thanks for the information, it explains the situation well. It is still hard
to imagine how a 400 constructor inductive can generate almost 10GB of
inversion lemmas. I guess one has to see this to understand it.

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, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/07/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/08/2015
  - Re: [Coq-Club] Speeding up inversion on large inductives, Xavier Leroy, 09/09/2015
    - Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
      - Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/09/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
        
        RE: [Coq-Club] Speeding up inversion on large inductives, Soegtrop, Michael, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Pierre Courtieu, 09/10/2015
        Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Enrico Tassi, 09/10/2015
        RE: [Coq-Club] Speeding up inversion on large inductives, Soegtrop, Michael, 09/10/2015
      - Re: [Coq-Club] Speeding up inversion on large inductives, Robbert Krebbers, 09/09/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Thomas Braibant, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/11/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Alan Schmitt, 09/15/2015
    - Re: [Coq-Club] Speeding up inversion on large inductives, Vladimir Voevodsky, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Gregory Malecha, 09/08/2015
  - Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/09/2015
    - Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/09/2015
      - Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015