如何 destruct/generalize 重写程序的匹配语句

Question

当使用 Program 时，匹配语句被重写为 "proof-passing" 样式。这使得匹配的证据在分支中可用——这可能很关键。

然而，这似乎也让案例分析变得更加困难。例如：

Require Import ZArith.

Open Scope Z_scope.

Program Definition test (x:Z) : option (x <= 100) :=
  match Z_le_gt_dec x 100 with
  | left bound => Some _
  | right bound => None
  end.

Lemma test_gt_100 : forall x:Z, x > 100 -> test x = None.
Proof.
  intros x bound.
  unfold test.

此时，通常destruct (Z_le_gt_dec x 100)，证明就很容易了。然而，重写的匹配给出了这个上下文：

x : Z
bound : x > 100
============================
 match
   Z_le_gt_dec x 100 as x0
   return (x0 = Z_le_gt_dec x 100 -> option (x <= 100))
 with
 | left bound0 =>
     fun Heq_anonymous : left bound0 = Z_le_gt_dec x 100 =>
     Some (test_obligation_1 x bound0 Heq_anonymous)
 | right bound0 => fun _ : right bound0 = Z_le_gt_dec x 100 => None
 end eq_refl = None

这样，破坏就失败了：

Toplevel input, characters 20-48:
Error: Abstracting over the term "s" leads to a term
"fun s : {x <= 100} + {x > 100} =>
 match s as x0 return (x0 = s -> option (x <= 100)) with
 | left bound =>
     fun Heq_anonymous : left bound = s =>
     Some (test_obligation_1 x bound Heq_anonymous)
 | right bound => fun _ : right bound = s => None
 end eq_refl = None" which is ill-typed.

放慢速度并尝试 generalize (Z_le_gt_dec x 100) 说明原因：

Toplevel input, characters 0-30:
Error: Illegal application (Type Error): 
The term "test_obligation_1" of type
 "forall x : Z,
  let filtered_var := Z_le_gt_dec x 100 in
  forall bound : x <= 100, left bound = filtered_var -> x <= 100"
cannot be applied to the terms
 "x" : "Z"
 "bound0" : "x <= 100"
 "Heq_anonymous" : "left bound0 = s"
The 3rd term has type "left bound0 = s" which should be coercible to
 "left bound0 = Z_le_gt_dec x 100".

虽然这有一定道理，但我不知道该怎么做。

（如果有用的话，我已经把它放在 collacoq 中了。不要忘记首先只执行注释行，然后等到所有库都已加载后再导入 ZArith。）

Answer 1

这里的问题是你依赖于一个特定的相等项，对它进行抽象应该允许你继续。（陈述独立于证明的引理是一般的良好做法）。

这是您的示例，使用 ssreflect 的重写。抱歉，我无法指示 Coq 的程序进行正确的模式选择。

Comments "pkgs: coq-reals".
From mathcomp Require Import ssreflect.
Require Import Coq.ZArith.ZArith.

Open Scope Z_scope.

Program Definition test (x:Z) : option (x <= 100) :=
  match Z_le_gt_dec x 100 with
  | left  bound => Some _
  | right bound => None
  end.

Lemma test_gt_100 : forall x:Z, x > 100 -> test x = None.
Proof.
intros x hb; unfold test.
assert (Z_le_gt_dec x 100 = right hb) as Hz. admit.
move: eq_refl; rewrite {1 3}Hz.
done.

[也在 https://x80.org/collacoq/xareboqura.coq]

问候，E.

编辑：更详细一点：在开始时，匹配的参数是eq_refl : forall x, x = x，这是可以的，因为匹配中的函数需要一个Z.le .... = Z.le ....类型的术语。但是，在执行重写时，匹配注释中的类型将变成 Z_le ... = right ... 形式，但如果参数仍然是 eq_refl，这将导致键入错误的术语，因为 eq_refl 可以永远不要输入 Z.le ... = right ...!

因此，我们修改了我们的目标，使相等性的证明不一定是eq_refl，然后我们重写。

为什么首先用 eq_refl 来证明？通常这样做是为了在存在相等性证明的情况下具有良好的归约行为。

为你的程序添加证明无关支持会很有趣。（如果已经有一些，我会忽略）。

如何 destruct/generalize 重写程序的匹配语句

How to destruct/generalize over Program's rewritten match statements

coq