coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: 朱立平 <zlponline AT 163.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Merge similar theorems
- Date: Sun, 2 Feb 2020 17:30:22 +0800 (CST)
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=zlponline AT 163.com; spf=Pass smtp.mailfrom=zlponline AT 163.com; spf=None smtp.helo=postmaster AT m13-122.163.com
- Ironport-phdr: 9a23:s6oPVxx1S+hGpo7XCy+O+j09IxM/srCxBDY+r6Qd1OgVIJqq85mqBkHD//Il1AaPAdyHra4ZwLKN++C4ACpcuM3H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMjoZvKqk9xgfHr3BVf+ha2X5kKUickhrh6Mq85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTy1BDI28YYUREuQPJ+FWoJXyqFUNthaxHxWgCfn0xTJSmnP4was32PkhHwHc2wwgGsoDtmzJq9DxM6QXSOCwx7TPwDTCa/NWwTD96I7MchAgp/GDQ6l9fdfQxEQhDQ/KklKQqYn8Mj6Ty+8DsHCb4vJ+We6xl2IrsRx9rzuyyss2l4XEiJgZxk3a+Sln2Io5OMC0RFNhbdK5E5ZcrSWXOolsTs8/QGxltyA3waAct5GhZigF0pEnygbfa/OZd4iI5QruVOOMLTp2nX5pZayziwio/US9y+DxWNO430pNripAitXMt3YN2ALP6sWfVPdx4Fut1SyS2w3Q9+1IO104mKTBJ5I83LI8iIIfsUHZES/3nEX2grWWdkIh+uWw6uXnZq3mppiaN49wiwH+NLohl9eiDek5PAUCRXSU+eO51LH75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKXNOaSkCZHQJFDClq3gdPBz8R1y0g02mG7bTlj63/lVMvbrXUn1tdrVJkZnaEq/xOOxW4Y17Z8XRW/aWvzRC6jVq1LdvrtzcdnJX5ccvXPGE9Zg/+Tn3C1gxwRbdq6sj8NONSKIW89+KkDcWkLCx9cMFWBT4Vg7Fbev0QfYF2cNPDC5WKduvmhqWrLjNp/KQ8WWuJLE2S66GpNMYWUXWAnSSjHjcIDWAvo=
I have two(and may be more) theorems as follows and I don't think proving them one by one is a good way.
Theorem app1_access_self_ok :
forall (ea : Z),
ea_in_app1_range ea ->
let tlbe := find_tlbe CPUContextAPP1 ea TLB in
( tlb_hit tlbe
/\ addr_translate_ok tlbe ea
/\ access_granted CPUContextAPP1 tlbe).
Theorem app2_access_self_ok :
forall (ea : Z),
ea_in_app2_range ea ->
let tlbe := find_tlbe CPUContextAPP2 ea TLB in
( tlb_hit tlbe
/\ addr_translate_ok tlbe ea
/\ access_granted CPUContextAPP2 tlbe).
The differences are
Definition ea_in_app1_range (ea : Z) : Prop := (to_Z "0x40040000") <= ea <=(to_Z "0x4004ffff") .
Definition ea_in_app2_range (ea : Z) : Prop := (to_Z "0x40050000") <= ea <=(to_Z "0x4005ffff") .
and
Definition CPUContextAPP1 := mk_cpucontext true true true (1).
Definition CPUContextAPP2 := mk_cpucontext true true true (2).
Is there an elegant way to prove them in one theorem? Will high-order be used in this scenario? Thanks!
Best,
Julian
- [Coq-Club] Merge similar theorems, 朱立平, 02/02/2020
- Re: [Coq-Club] Merge similar theorems, Gabriel Scherer, 02/02/2020
- <Possible follow-up(s)>
- Re: [Coq-Club] Merge similar theorems, Jason -Zhong Sheng- Hu, 02/03/2020
Archive powered by MHonArc 2.6.18.