3

我正在使用立方标准库中定义的有限多重集类型： https ://github.com/agda/cubical/blob/0d272ccbf6f3b142d1b723cead28209444bc896f/Cubical/HITs/FiniteMultiset/Base.agda#L15

data FMSet (A : Type ℓ) : Type ℓ where
  []    : FMSet A
  _∷_   : (x : A) → (xs : FMSet A) → FMSet A
  comm  : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : isSet (FMSet A)

我能够重现计数可扩展性的证明，并且我的一个引理表明你可以从等式的两边删除一个元素并保持等式。

它类似于这个：https ://github.com/agda/cubical/blob/0d272ccbf6f3b142d1b723cead28209444bc896f/Cubical/HITs/FiniteMultiset/Properties.agda#L183

 remove1-≡-lemma : ∀ {a} {x} xs → a ≡ x → xs ≡ remove1 a (x ∷ xs)
 remove1-≡-lemma {a} {x} xs a≡x with discA a x
 ...                            | yes _   = refl
 ...                            | no  a≢x = ⊥.rec (a≢x a≡x)

我的证明没有使用相同的语法，但在核心库语法中它是

 cons-path-lemma : ∀ {x} xs ys → (x ∷ xs) ≡ (x ∷ ys) → xs ≡ ys

其中证明使用remove1-≡-lemma由路径两侧组成的路径，该路径是在功能上由 组成的参数路径remove1 x。

这要求值的类型具有可判定的相等性，因为没有它 remove1 没有意义。但是引理本身并没有提到可判定的相等性，所以我想我会在没有假设的情况下尝试证明它。现在是一周后，我不知所措，因为这看起来很“明显”，但很难证明。

我认为我对这一点可证明的直觉可能来自我的经典数学背景，因此它并没有建设性地/持续地遵循。

所以我的问题是：在没有元素类型假设的情况下，这是否可以证明？如果是这样，证明的一般结构会是什么样子，我很难获得想要同时在两个 FMSets 上进行感应的证明（因为我主要是在尝试根据需要排列路径时猜测）。如果没有假设就无法证明，是否有可能证明它在某种形式上与必要的假设等价？

4

1 回答 1

4

我不能提供一个证明，而是一个论点，为什么它应该是可证明的，而不假设可判定性。我认为有限多重集可以表示为多重集之间的函数和Fin n -> A相等性，并由排列给出（即在 上的可逆函数），使得. 现在fgphi : Fin n ~ Fin nFin nf o phi = g

(a :: f) 0 = a (a :: f) (suc i) = f i

如果phi : Fin (suc n) ~ Fin (suc n)证明a :: f = a :: g你可以构造一个psi : Fin n ~ Fin n证明f = g. If phi 0 = 0thenpsi n = phi (suc n)否则你必须psi通过分配phi^-1 0来获得phi 0. 但是，此案例分析正在进行中Fin n。

我认为通过交换相邻元素来表示排列组只是这个问题的不方便表示。

于 2020-06-09T12:24:35.137 回答