Skip to Content.
Sympa Menu

coq-club - [Coq-Club] (no subject)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] (no subject)


chronological Thread 
  • From: "Woon Ming" <woon_ming AT comp.nus.edu.sg>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] (no subject)
  • Date: Tue, 17 Feb 2009 02:06:30 +0800 (SGT)
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi all,

I was working with a toy program (attached FindMax.java) and was trying to
find a way to solve memory structure modeled by Coq (using 'shift',
'select' and 'store'). However, I am stuck at a particular one which has
the subgoal as follows:

select intM_intP (shift t j) <= select intM_intP (shift t 0)

I am unable to find this lemma in both my FindMax.v file nor in the
library at the Coq website. Can anyone help me with this and enlighten me
on how to solve this kind of problem?


Best Regards,
Woon Ming





Archive powered by MhonArc 2.6.16.

Top of Page