coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with large existential

From: Tj Barclay <tjbarclay AT ku.edu>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Problem with large existential
Date: Thu, 2 Apr 2020 13:54:57 -0500
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass (sender ip is 129.237.207.24) smtp.rcpttodomain=inria.fr smtp.mailfrom=ku.edu; dmarc=bestguesspass action=none header.from=ku.edu; dkim=none (message not signed); 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=qEP6Gx+fFOv9giOAPW5ohIL8UW/FHB2BdEeLoJUfZMI=; b=ATskZzs1XJH0ATTs68d5tdd62zshcSWuURiEaTqlZfntiLo0+RP/f3+Y8+6var+yCCUhs6mLwG0HQVuRTL4jeGjG+dFzGTkQVsEGDCoj1cZQgE2LMGhrxQOPZ46PwiIV6X1SMLaOLGhJAzvoMXxRDyeBXtPNxRAB9GJHVHlXu5RicBB5bqIkgUP7RZrpKQgYuCcU7cCmiiGA+7NS6dEiLojPzog3qfv0mBXYbtMmwpDleqUkLghh3nCPhTHYkpi35nf64Be4UtxM3rB+/KovNlYV6E4VqN/W/DBHBWsweACxiKGClIcH4jFRe1Y/Urgt5eBKKTx7oT57St8yIoZXmA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=WhSd0eXPecRjX8PirqheaIv5qAKWTFXjfLzV9QSo3TtBnO8aYl/V+4o8FAvgOGpKYSFJHSn+4WUl8tq89uZukg4uF8vvHWzyaNLsAwi7VzIkEShBHbVFuymNwBsCzV8G9vbKklhPW/dzQOGf2l74O+d2TXP12wGRtefi2gWRS35OGoAURouThloC2a60UT17mgZE56nZCM94/dZ9Qb53II0xamQK4eOxBaYXISEVGz1vV6vqaX8jQsNOz70bVfzvap6IaKq32ifJSKwB4PZpbCj1zWyN6KxL0dnE3Ur1ZicE6zwXWSPX22z2eY3y924xeFcqwLmt0YoMjUuw/DrNcA==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tjbarclay AT ku.edu; spf=Pass smtp.mailfrom=tjbarclay AT ku.edu; spf=Pass smtp.helo=postmaster AT NAM10-BN7-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:kfZTRh9hlpJFI/9uRHKM819IXTAuvvDOBiVQ1KB+1ugcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS46tL2HV9ym56idXERHiPyJ0IP70E8jclZLk+fq1/sjvYU1ijSC2ZbpjZEGqrw/YrMISiJpKKbt3xxfU9CgbM99KzH9lcArA1y334d29qcY6r3Zg/sk5/ssFap3UOrwiROwKDylgPmwotpWy6EvzCDCX735ZaV041xpFBw+Zs0Pcd7Ko6m7QkLU43yOXe8rrUbozRDKuqb9xTwPlgzsGMDh/93zLjst3j+RQpxfz/kUukb6RW5mcMb9FRo2YeNobQWRbWcMBBS9cRI6wctlWAg==

Howdy All,

I am currently running into some issues with large data structures causing Coq to break, and wonder if anyone's got any tips here.

I have a programming language with a relationally defined semantics. I'm trying to use an existential quantifier in order to "discover" the environment created by evaluating an _expression_ in the language.

For example I can write :

exists (e : ENV), evalRel *initalEnv* *_expression_* *value* e

Then I can proceed to use tactics like econstructor to let the prover generate the proper value for e. This works for small expressions, but when given an entire program Coq eventually hangs while in the middle of proving. It seems like the large size of the value generated for the environment is causing problems. I've tried this inside Proof General, CoqIDE, and coqc, but all three eventually crash.

Thanks in advance,

TJ

TJ Barclay

Electrcial Engineering & Computer Science, University of Kansas

tjbarclay AT ku.edu

+1 316 259 2250

[Coq-Club] Problem with large existential, Tj Barclay, 04/02/2020