从软件基础 Color.v 寻求有关Sin_domain证明的一些帮助

Question

这是完整的模块： https://softwarefoundations.cis.upenn.edu/vfa-current/Color.html

手头的定理：

Exercise: 3 stars (Sin_domain)
Lemma Sin_domain: ∀ A n (g: M.t A), S.In n (Mdomain g) ↔ M.In n g.

通常，3 星表示很难但不太难，但我正在努力弄清楚如何解决这个问题。如果你展开Mdomain，它就会变成一个折叠，然后变成M.xfoldi，这是相当低的水平。我有一种感觉，我如何证明一堆关于 xfoldi 如何作用于各种指数的低级引理，但是......我觉得一定有更好的方法吗？也就是说，它确实有这个免责声明

This seems so obvious! But I didn't find a really simple proof of it.

我对这种事情的第一直觉总是尝试证明手头事情的某种分布原则，例如

Mdomain (M.Node s1 o s2) 

但是由于Mdomain是按折叠实现的，因此它很快就会变得复杂。同样，可能不是不可逾越的，但是...我想知道是否有更好的方法(鉴于我刚刚在Sremove_cardinal_less和Mremove_cardinal_less上花了很多很多小时！

Answer 1

提示：使用WP.fold_rec_bis来证明地图与折叠结果之间的关系P(带M.fold(。它是归纳原理的一种形式：

• 基本情况：空映射和初始累加器之间的关系必须成立;
• 归纳步骤：如果某个映射(和累加器(的关系成立，那么在插入新的键值对(并相应地更新累加器(后，它成立。

作为技术性，它还需要一个"兼容性"假设(这是一个明确的证明，证明你的关系P独立于插入顺序(。

Theorem fold_rec_bis :
forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
forall (i:A)(m:t elt),
(forall m m' a, Equal m m' -> P m a -> P m' a) ->  (* Compatibility *)
(P (empty _) i) ->                                 (* Base case *)
(forall k e a m', MapsTo k e m -> ~In k m' ->      (* Induction step *)
P m' a -> P (add k e m') (f k e a)) ->
P m (fold f m i).