为容器类型组合 sumbool

如何解决为容器类型组合 sumbool

我正在尝试为简单类型构建一个返回 sumbool 而不是 bool 的相等谓词：

Inductive state_type : Set := State : nat -> nat -> state_type.

这是一个可行的解决方案，它根据字段是否匹配（一次一个）拆分为多个子目标。

DeFinition state_eq : forall (s1 s2 : state_type),{s1 = s2} + {s1 <> s2}.
  intros.
  destruct s1 as [a1 b1]. destruct s2 as [a2 b2].
  destruct (eq_nat_dec a1 a2) as [Aeq | Aneq]. destruct (eq_nat_dec b1 b2) as [Beq | Bneq].
  left. congruence.
  right. congruence.
  right. congruence.
Defined.

证明是可读的，但我想要更直接的证明，使用 refine：

DeFinition state_eq2 : forall (s1 s2 : state_type),{s1 = s2} + {s1 <> s2}.
  refine (fun (s1 s2 : state_type) =>
            match s1,s2 with State a1 b1,State a2 b2 =>
               if (eq_nat_dec a1 a2)
               then if (eq_nat_dec b1 b2)
                    then left _ _
                    else right _ _
               else right _ _
            end).
Defined.

三个返回值最终成为子目标，但它们的上下文都失去了 eq_nat_dec 假设，使它们无法证明。我怎样才能保留这些假设来完成证明？

解决方法

似乎 if ... then ... else 是失去这些假设的原因。用显式匹配替换它可以保留假设，允许 congruence 像以前一样完成证明：

Definition state_eq : forall (s1 s2 : state_type),{s1 = s2} + {s1 <> s2}.
  refine (fun (s1 s2 : state_type) =>
            match s1,s2 with State a1 b1,State a2 b2 =>
               match (eq_nat_dec a1 a2) with
                 | left _ => match (eq_nat_dec b1 b2) with
                               | left _ => left _ _
                               | right _ => right _ _
                             end
                 | right _ => right _ _
               end
            end); congruence.
Defined.