coq - Coq 的子类型

Question

我尝试练习subtypes在Coq ，并使用ssreflect简化事情。但我在重写子类型时总是遇到一些问题。例如:

Require Import Omega.
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.

(* a type A to build X *)
Inductive A: Set :=
| mkA: nat -> A.

Definition getNat_A (a: A) :=
match a with
| mkA n => n
end.

Inductive X: Set :=
| r1 : A -> X.

(* subtype of X that satisfying some property *)
Definition Instantiated_X (x : X) : bool :=
  match x with
  | r1 a => (getNat_A a) > 10
end.

Definition iX : Set := {x:X | (Instantiated_X x)}.

(* rewrite constructor of X, stating the fact of elements of A, under certain condition creates element of iX *)
Program Definition r1_rewrite : A -> option iX :=
fun a: A =>
 match (Instantiated_X (r1 a)) with 
 | true => Some (exist _ (r1 a) _)
 | false => None
 end.

(* try to prove r1_rewrite is surjective *)
Example r1_rewrite_surj: 
forall t : iX, exists (a : A),
 match (r1_rewrite a) with
 | None => True
 | Some e => eq t e
 end.
 Proof.
  intros.
  destruct t eqn: caseiX.
  destruct x eqn: caseX.
  exists a.
  destruct (r1_rewrite a) eqn: r_res.
   - destruct (10 < getNat_A a) eqn: guard.
     destruct i0.
     destruct x0.
     unfold r1_rewrite in r_res.
     simpl in r_res.
     rewrite <- guard in r_res. (* <- stuck *)
Abort.

我不明白为什么它卡在那里。错误消息显示:

Error: Abstracting over the term "true" leads to a term: ... 
which is ill-typed.

我认为 Coq 会替换所有出现的 (10 < getNat_A a)与 true在r_res ，这会导致类似的结果:

Some (exist (fun x : X => Instantiated_X x) (r1 a)
          (r1_rewrite_obligation_1 a Heq_anonymous) =
Some (exist (fun x : X => Instantiated_X x) (r1 a0) i0)

以及proof irrelevance和r1 injectivity ，让我的证明通过。所以，我想知道我能得到一些关于如何按摩的建议r_res在这种情况下，它有助于重写。

编辑:删除 Eq类型类及其实例，使示例更加简洁

Answer 1

你的证明尝试的问题在于你必须小心重写的方式。这是一个可能的解决方案。

Example r1_rewrite_surj:
forall t : iX, exists (a : A),
 match (r1_rewrite a) with
 | None => True
 | Some e => eq t e
 end.
Proof.
move=> [[a] Pa]; exists a; rewrite /r1_rewrite.
move: (erefl _); rewrite {1 3}Pa.
by move=> e; rewrite (eq_irrelevance (r1_rewrite_obligation_1 _ _) Pa).
Qed.

要了解这里发生的情况有点棘手。第一行之后，证明状态如下所示:

  a : A
  Pa : Instantiated_X (r1 a)
  ============================
  match
    (if Instantiated_X (r1 a) as b return b = Instantiated_X (r1 a) -> option iX
     then
      fun H : true = Instantiated_X (r1 a) =>
      Some (exist (fun x : X => Instantiated_X x) (r1 a) (r1_rewrite_obligation_1 a H))
     else fun _ : false = Instantiated_X (r1 a) => None) (erefl (Instantiated_X (r1 a)))
  with
  | Some e => exist (fun x : X => Instantiated_X x) (r1 a) Pa = e
  | None => True
  end

如果我们尝试在以下任何情况下使用 Pa 重写，我们将收到类型错误。例如:

1. 如果我们尝试替换第一次出现的 Instantiated_X (r1 a)，Coq 将不允许我们将 if 的结果应用到 (erefl (Instantiated_X (r1 a)).

2. 我们可以通过将第一个、第二个和第六个(erefl 上的那个)出现的 Instantiated_X (r1 a) 替换为 true。这也不起作用，因为它会使 r1_rewrite_obligation_1 的应用程序类型错误。

解决方案是泛化erefl(使用调用move: (erefl _))，导致以下证明状态:

  forall e : Instantiated_X (r1 a) = Instantiated_X (r1 a),
  match
    (if Instantiated_X (r1 a) as b return b = Instantiated_X (r1 a) -> option iX
     then
      fun H : true = Instantiated_X (r1 a) =>
      Some (exist (fun x : X => Instantiated_X x) (r1 a) (r1_rewrite_obligation_1 a H))
     else fun _ : false = Instantiated_X (r1 a) => None) e
  with
  | Some e0 => exist (fun x : X => Instantiated_X x) (r1 a) Pa = e0
  | None => True
  end

可能不容易看出，但此时可以安全地用 Pa 重写来替换第一次和第三次出现的 Instantiated_X (r1 a)，并允许 if 减少。然后我们可以通过证明 bool 相等性的无关性来得出结论。

不用说，以这种方式推理打字问题是一场噩梦。正如 ejgallego 指出的，在这种情况下，重用 ssreflect 的子类型机制要容易得多。例如:

(* Other definitions remain the same *)
Definition r1_rewrite a : option iX := insub (r1 a).

Example r1_rewrite_surj:
forall t : iX, exists (a : A),
 match (r1_rewrite a) with
 | None => True
 | Some e => eq t e
 end.
Proof.
by move=> [[a] Pa]; exists a; rewrite /r1_rewrite insubT.
Qed.

insub 函数是 r1_rewrite 的通用版本。它检查定义子类型的属性是否成立，如果成立，则将该对象与相应的证明配对。 insubT 引理表明，当属性成立时，insub 返回 Some。