时间戳

首页 > 解决方案 > 由 case_eq 和 Coq 重写导致的抽象/打字错误

coq - 由 case_eq 和 Coq 重写导致的抽象/打字错误

问题描述

考虑下面代码描述的情况，其中我有一个“分段”函数，其h行为不同（likef或 like g）取决于condition其输入的某些（可h确定的）属性（使用定义case_eq）。假设我可以证明 a在应用任何一个部分函数或后property的图像是有保证的；我应该能够证明整个函数使用一个简单的证明来保证，不是吗？然而，以下代码拒绝了该步骤：xfghpropertycase_eqrewrite

Section Error.

Variables X Y : Type.
Variables n m : Y.
Variable condition : X -> bool.
Variable property : Y -> Prop.

Definition type1 (x : X) : Prop := condition x = true.
Definition type2 (x : X) : Prop := condition x = false.

Variable f : {x:X | type1 x} -> Y.
Variable g : {x:X | type2 x} -> Y.

Definition h : X -> Y. intro x. case_eq (condition x); intro.
  - exact (f (exist type1 x H)).
  - exact (g (exist type2 x H)).
Defined.

Hypothesis Hf : forall x, property (f x).
Hypothesis Hg : forall x, property (g x).

Theorem hRange : forall x, property (h x).
Proof. intro. case_eq (condition x); intro.
  - unfold h. rewrite H.

有错误

Abstracting over the term "condition x" leads to a term
fun b : bool =>
property
  ((if b as b0 return (b = b0 -> Y)
    then fun H0 : b = true => f (exist type1 x H0)
    else fun H0 : b = false => g (exist type2 x H0)) eq_refl)
which is ill-typed.
Reason is: Illegal application: 
The term "exist" of type "forall (A : Type) (P : A -> Prop) (x : A), P x -> {x : A | P x}"
cannot be applied to the terms
 "X" : "Type"
 "type1" : "X -> Prop"
 "x" : "X"
 "H0" : "b = true"
The 4th term has type "b = true" which should be coercible to "type1 x".

当然，我希望它会删除该if子句，将目标重写为，property (f (exist type1 x H))但 Coq 不喜欢这样。为什么不？

case_eq如果定义中生成的假设不涉及结果，我觉得 Coq 不会h这样（在这种情况下，我可以h用一个match子句重写，这不会给我带来任何问题。在目前的情况下，只需假设该假设对于构建f xor的某些“非计算”部分至关重要g x，例如 ifY本身是 sig 类型）。我已经阅读过类似this和this的其他主题，但就我理解它们而言，它们并不能帮助我理解我的情况。

标签： coq

解决方案

当您尝试破坏或重写所有出现的子项时，会出现此问题。在这里，你重写 condition x了 的类型H0，这会导致exist type1 x H0类型错误（你能明白为什么吗？）。

解决方案是将破坏或重写限制为仅某些子项。这可能需要您概括部分目标。例如：

From Coq Require Import ssreflect.

Section Error.

Variables X Y : Type.
Variables n m : Y.
Variable condition : X -> bool.
Variable property : Y -> Prop.

Definition type1 (x : X) : Prop := condition x = true.
Definition type2 (x : X) : Prop := condition x = false.

Variable f : {x:X | type1 x} -> Y.
Variable g : {x:X | type2 x} -> Y.

Definition h : X -> Y. intro x. case_eq (condition x); intro.
  - exact (f (exist type1 x H)).
  - exact (g (exist type2 x H)).
Defined.

Hypothesis Hf : forall x, property (f x).
Hypothesis Hg : forall x, property (g x).

Theorem hRange : forall x, property (h x).
Proof.
intro; unfold h; generalize (eq_refl (condition x)).
case: {2 3}(condition x).
- intros H. apply Hf.
- intros H. apply Hg.
Qed.

End Error.

概括后eq_refl，目标如下：

1 subgoal (ID 16)


  X, Y : Type
  n, m : Y
  condition : X -> bool
  property : Y -> Prop
  f : {x : X | type1 x} -> Y
  g : {x : X | type2 x} -> Y
  Hf : forall x : {x : X | type1 x}, property (f x)
  Hg : forall x : {x : X | type2 x}, property (g x)
  x : X
  ============================
  forall e : condition x = condition x,
  property
    ((if condition x as b return (condition x = b -> Y)
      then fun H : condition x = true => f (exist type1 x H)
      else fun H : condition x = false => g (exist type2 x H)) e)

该策略case: {2 3}...是从 进口的ssreflect，它说condition x应该只在 RHS 上e和在if.

推荐阅读