coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Software foundation ceval_deterministic

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Software foundation ceval_deterministic
Date: Mon, 5 Dec 2016 14:44:06 +1100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f52.google.com
Ironport-phdr: 9a23:E5+xTxV7D6e5t6pn+nVX2mxdNlXV8LGtZVwlr6E/grcLSJyIuqrYYx2At8tkgFKBZ4jH8fUM07OQ6PG7HzBfqs3Y+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe71/IRG4oAnLucQbg4RuJ6gsxhDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuBKvqRJ8zYDJfo+aKOFzcbnBcd4AX2dNQtpdWi5HD4ihb4UPFe0BPeNAoon4ulsOrgWxBRKsBOjy1j9Ih3H30rcg0+QgDArL2wkgH88NsHvKt9X1NLsSUeG7zabS1zXDbula2Tb86IjJbhAhpOqBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvWac7+plT+2vimgnphl+ojiu2scsipTJiZkPxl/Y8iV5xZ45JcCgSEFlZ96kFoFcuD+HOItrRM4pXmJmuD4ix7EYpZK2eDIGxZcnyhLFdfCLbouF7gjjWeqPJzpzmWhrd6ilhxmo9Eit0u38Wdew0FZNtidFl8PDtnEJ1xDK7ciHS+dx8l6v2TuPyQzf8O5EIUczlarUL54u3KQ8mYYUsUTGBiP2mUP2g7GKdkg85OSk9+Dqbq/lq5KcLYN4lBzyP6c0lsG/H+g0Kg0OUHKa+eS42r3j50r5QLBSg/0zj6nZs47VJd8bpq6lAg9U3Jws6wy+Dzu80dQYnHgHLE5AeB+cgIjpPkvBIPH8Dfuln1uslzJry+jcPrL9GpXNMmTDkLD5cLlh7E5c0RM/wsxb55JJEb4MO+nzW0/0tNzAFBA1KQ20w+D9CNV8zIwSQ2yPArXKeJ/V5FSP/6ckJ/SGTI4Tojf0bfY/tND0inpsnEIecLKplYcWd3miH7wyJliabGHsntYeGH0L+As/TfDvoFKHWD9XIX21WvRvtXkAFIu6ANKbFciWi7ub0XLjEw==

Hello everyone,
I am trying to prove Theorem ceval_deterministic: ∀(c:com) st st1 st2 s1 s2, c / st ⇓ s1 / st1 →
c / st ⇓ s2 / st2 → st1 = st2 ∧ s1 = s2. [1]
but stuck with goal [2]. I looked at John Wiegley's solution [3], but I am getting "Error: congruence failed". I am using

u5935541@newport:~/Mukesh$ coqtop
Welcome to Coq 8.5pl2 (July 2016)

Could some one please tell me how to solve this goal.

Best regards,

Mukesh Tiwari

[1]https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html
[2] https://gist.github.com/mukeshtiwari/6555aa5b74e630a800defd121e6ba3ff
[3] https://gist.github.com/jwiegley/80b39aefca77e7d28da14e389f0f9958

[Coq-Club] Software foundation ceval_deterministic, mukesh tiwari, 12/05/2016