- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我有一个二进制数表示,加上一些与 Nat 的转换:
open import Data.Nat
open import Data.Nat.Properties
open import Function
open import Relation.Binary.PropositionalEquality hiding (trans; cong; subst; sym)
open import Relation.Binary.HeterogeneousEquality
open import Data.Unit
open import Algebra
module CS = CommutativeSemiring commutativeSemiring
data Bin : ℕ → Set where
zero : Bin zero
2*n : ∀ {n} → Bin n → Bin (n + n)
2*n+1 : ∀ {n} → Bin n → Bin (suc (n + n))
suc-lem : ∀ n → suc (suc (n + n)) ≡ suc n + suc n
suc-lem zero = refl
suc-lem (suc n) rewrite
CS.+-comm n (suc n)
| suc-lem n | CS.+-comm n (suc (suc n))
| CS.+-comm n (suc n) = refl
inc : ∀ {n} → Bin n → Bin (suc n)
inc zero = 2*n+1 zero
inc (2*n b) = 2*n+1 b
inc (2*n+1 {n} b) rewrite suc-lem n = 2*n (inc b)
nat2bin : (n : ℕ) → Bin n
nat2bin zero = zero
nat2bin (suc n) = inc (nat2bin n)
bin2nat : ∀ {n} → Bin n → ℕ
bin2nat {n} b = n
lem : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) =
subst
(λ b → 2*n+1 (inc (inc (nat2bin n))) ≅ inc (inc b))
(sym $ lem ?) ?
n
进入
sym $ lem ?
,但这会导致错误,提示
suc (n + n) != n + suc n
.
最佳答案
进口:
open import Level hiding (zero; suc)
open import Function
open import Relation.Binary.HeterogeneousEquality
renaming (sym to hsym; trans to htrans; cong to hcong; subst to hsubst)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin hiding (_+_)
open import Algebra
open import Data.Nat.Properties
module ℕplus = CommutativeSemiring commutativeSemiring
inc
稍微简化一下:
inc : ∀ {n} → Bin n → Bin (suc n)
inc zero = 2*n+1 zero
inc (2*n b) = 2*n+1 b
inc (2*n+1 {n} b) = subst (Bin ∘ suc) (ℕplus.+-comm n (suc n)) (2*n (inc b))
lem : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) = {!!}
2*n+1 (inc (inc (nat2bin n))) ≅
inc
(subst ((λ {.x} → Bin) ∘ suc) (ℕplus.+-comm (suc n) (suc (suc n)))
(2*n (inc (inc (nat2bin n)))))
≡-subst-removable : ∀ {a p} {A : Set a}
(P : A → Set p) {x y} (eq : x ≡ y) z →
P.subst P eq z ≅ z
≡-subst-removable P refl z = refl
hsym $
≡-subst-removable
(Bin ∘ suc)
(ℕplus.+-comm (suc n) (suc (suc n)))
(2*n $ inc $ inc $ nat2bin n)
(2*n $ inc $ inc $ nat2bin n) ≅
subst ((λ {.x} → Bin) ∘ suc) (ℕplus.+-comm (suc n) (suc (suc n)))
(2*n $ inc $ inc $ nat2bin n)
hcong inc
,但编译器拒绝它。
cong
的实现:
cong : ∀ {a b} {A : Set a} {B : A → Set b} {x y}
(f : (x : A) → B x) → x ≅ y → f x ≅ f y
cong f refl = refl
x
和
y
必须是同一类型
A
, 而我们的
subst
改变类型。
hcong
的实现,我们需要:
hcong' : {α β γ : Level} {I : Set α} {i j : I}
-> (A : I -> Set β) {B : {k : I} -> A k -> Set γ} {x : A i} {y : A j}
-> i ≡ j
-> (f : {k : I} -> (x : A k) -> B x)
-> x ≅ y
-> f x ≅ f y
hcong' _ refl _ refl = refl
lem : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) =
hcong'
(Bin ∘ suc)
(ℕplus.+-comm (suc n) (suc (suc n)))
inc
$ hsym
$ ≡-subst-removable
(Bin ∘ suc)
(ℕplus.+-comm (suc n) (suc (suc n)))
(2*n $ inc $ inc $ nat2bin n)
subst-removable
和
cong
:
≡-cong-subst-removable : {α β γ : Level} {I : Set α} {i j : I}
-> (A : I -> Set β) {B : {k : I} -> A k -> Set γ}
-> (e : i ≡ j)
-> (x : A i)
-> (f : {k : I} -> (x : A k) -> B x)
-> f (subst A e x) ≅ f x
≡-cong-subst-removable _ refl _ _ = refl
lem' : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem' zero = refl
lem' (suc n) = hsym $
≡-cong-subst-removable
(Bin ∘ suc)
(ℕplus.+-comm (suc n) (suc (suc n)))
(2*n $ inc $ inc $ nat2bin n)
inc
data Bin : Set where
zero : Bin
2*n : Bin → Bin
2*n+1 : Bin → Bin
contrived-example : {n : ℕ} {f : Fin (n + suc n)}
-> f ≅ fromℕ (n + suc n)
-> f ≅ fromℕ (suc n + n)
contrived-example {n} eq = htrans eq $ hcong fromℕ $ ≡-to-≅ $ ℕplus.+-comm n (suc n)
hsubst' : {C1 C2 : Set} {x : C1} {y : C2}
-> (P : {C : Set} -> C -> Set)
-> x ≅ y
-> P x
-> P y
hsubst' _ refl x = x
contrived-example' :
∀ n
→ (f : Fin (n + suc n))
→ (fromℕ (n + suc n) ≅ fromℕ (suc n + n))
→ (f ≅ fromℕ (n + suc n))
→ (f ≅ fromℕ (suc n + n))
contrived-example' n f eq p = hsubst' (λ f' → f ≅ f') eq p
关于agda - 卡在异质相等的证明上,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/24139810/
在 Android 的 API > 19 中是否有任何方法可以获取可移动 SD 卡的路径? 与外部 SD 卡一样,我们有 Environment.getExternalStorageDirectory
一些 Android 设备有 microSD(或其他存储卡)插槽,通常安装为 /storage/sdcard1 据我所知,自 Android 4.4 起 Google 限制了对此内存的访问,并在 An
我使用 Java Card 2.1.2 SDK 和 GPShell 作为与设备通信的方式在 Java Card 上构建一个项目。我从 GpShell 测试了 helloworld 示例,并成功发送了
我开发了一个应用程序,它有一个来电接收器,它适用于所有手机。一位用户有一部双 SIM 卡安卓手机。该应用程序适用于第一张 SIM 卡。但是当有人调用他的第二张 SIM 卡时,我们的应用程序不会被调用。
我有一个带预览的文件输入。 这是笔 Codepen 我想强制高度,我无法理解我该怎么做。我想将此组件的高度固定为 300px(示例),我还需要保持加载图像的正确纵横比,用灰色背景填充空白。现在我保持宽
关闭。这个问题不符合Stack Overflow guidelines .它目前不接受答案。 想改进这个问题?将问题更新为 on-topic对于堆栈溢出。 6年前关闭。 Improve this qu
我正在使用此代码访问 SD card : import os from os.path import join from jnius import autoclass #from android.pe
我正在为数据记录设备编写固件。它以 20 Hz 的频率从传感器读取数据并将数据写入 SD 卡。但是,向SD卡写入数据的时间并不一致(大约200-300 ms)。因此,一种解决方案是以一致的速率将数据写
我正在使用以下代码将视频放到网站上,但是在垂直方向上,手机屏幕上只能看到视频的左半部分 我不是网络开发人员。有人可以告诉我确切的内容吗,如何使其正确放置在手机屏幕上? 是在youtube iframe
我正在使用 Vuetify 1.5 和 Vuetify 网格系统来设置我的布局。现在我有一个组件 HelloWorld我将其导入到我的 Parent 中成分。我已经在我的 HelloWorld 中设置
我使用 python 制作了一个简单的二十一点游戏。我制作了游戏的其余部分,但我正在努力放入 ASCII 卡,所以这只是代码的一小部分。我尝试将 * len(phand) 放在附加行的末尾。虽然这确实
我正在使用玩家卡设置 Twitter 卡。它可以在预览工具中运行,但文档说它需要在“twitter.com 现代桌面浏览器? native iOs 和 Android Twitter 应用程序?mob
任何旧的 GSM 兼容 SIM 卡(3G USIM 的奖励)。 我想我需要一些硬件?谁能为业余爱好者推荐一些便宜的东西,以及一些更专业的东西? 我认为会有一个带有硬件的 API 的完整文档,所以也许这
我使用 python 制作了一个简单的二十一点游戏。我制作了游戏的其余部分,但我正在努力放入 ASCII 卡,所以这只是代码的一小部分。我尝试将 * len(phand) 放在附加行的末尾。虽然这确实
我记得前一段时间读到有 cpu 卡供系统添加额外的处理能力来进行大规模并行化。任何人都有这方面的经验和任何资源来研究项目的硬件和软件方面吗?这项技术是否不如传统集群?它更注重功率吗? 最佳答案 有两个
我检查外部存储是否已安装并且可用于读/写,然后从中读取。我使用的是确切的官方 Android 示例代码 ( from here )。 它说外部存储未安装。 getExternalFilesDir(nu
在 Android 2.1 及更低版本中,Android 应用程序可以请求下载到 SD 卡上吗?另外我想知道应用程序是否可以请求一些包含视频的文件夹下载到 SD 卡上?以及如何做到这一点? 提前致谢。
我们编写了一个 Windows 设备驱动程序来访问我们的自定义 PCI 卡。驱动程序使用 CreateFile 获取卡的句柄。 我们最近在一次安装中遇到了问题,卡似乎停止工作了。我们尝试更换卡(更换似
有些新设备(例如 Samsung Galaxy)带有两个 SD 卡。我想知道是否有任何方法可以确定设备是否有两张 SD 卡或一张 SD 卡。谢谢 最佳答案 我认为唯一的方法是使用 检查可用根的列表 F
我正在尝试将文件读/写到 SD 卡。我已经尝试在我的真实手机和 Eclipse 中的模拟器上执行此操作。在这两种设备上,对/mnt/sdcard/或/sdcard 的权限仅为“d--------”,我
我是一名优秀的程序员,十分优秀!