无法使用 Coq 中的方程包重写目标？

Question

我正在 coq 中使用方程包，目前我的目标中有这个表达式：

evalMS (if_then_else (if_then_else t1_1 t1_2 t1_3) t4 t5)

这在我的背景下

H: None = evalS (if_then_else t1_1 t1_2 t1_3)

我想评估第一个表达式，但我无法弄清楚。 首先我使用了

simp evalMS

。并得到了

evalMS_unfold_clause_1 (if_then_else t1_1 t1_2 t1_3)
  (inspect (evalS (if_then_else t1_1 t1_2 t1_3))) t4 t5

然后当我尝试

rewrite <- H.

时，我收到此错误

Abstracting over the term "evalS (if_then_else t1_1 t1_2 t1_3)" leads to a term
fun o : option FCPLang =>
evalMS_unfold_clause_1 (if_then_else t1_1 t1_2 t1_3) (inspect o) t4 t5 =
evalBS (if_then_else (if_then_else t1_1 t1_2 t1_3) t4 t5)
which is ill-typed.
Reason is: Illegal application: 
The term "evalMS_unfold_clause_1" of type
 "forall t1 : FCPLang,
  {b : option FCPLang | evalS t1 = b} -> FCPLang -> FCPLang -> option FCPLang"
cannot be applied to the terms
 "if_then_else t1_1 t1_2 t1_3" : "FCPLang"
 "inspect o" : "{b : option FCPLang | o = b}"
 "t4" : "FCPLang"
 "t5" : "FCPLang"
The 2nd term has type "{b : option FCPLang | o = b}" which should be a subtype of
 "{b : option FCPLang | evalS (if_then_else t1_1 t1_2 t1_3) = b}".

这也是我对 evalMS 的定义：

Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl.
Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
(*This definition tells Coq we'll prove the well-foundedness wf by showing that
the (measure term) will decrease (lt).*)
Equations? evalMS (term : FCPLang) : (option FCPLang) by wf (measure term) lt :=
evalMS (if_then_else t1 t2 t3) with inspect (evalS t1) => {
| Some (b true) eqn: eq1 => evalMS t2;
| Some (b false) eqn: eq2 => evalMS t3;
| Some (n n0) eqn:eq3 => None;
| Some A' eqn: eq4 => evalMS (if_then_else A' t2 t3);
| _ => None
};
evalMS (n C) := Some (n C);
evalMS (b B) := Some (b B).
- apply PeanoNat.Nat.lt_succ_r. rewrite (PeanoNat.Nat.add_comm (measure t1)). rewrite Arith_prebase.plus_assoc_reverse_stt. apply PeanoNat.Nat.le_add_r.
- apply PeanoNat.Nat.lt_succ_r. rewrite (PeanoNat.Nat.add_comm). apply PeanoNat.Nat.le_add_r.
- destruct t1. * discriminate eq4. * discriminate eq4.
* simpl. apply decreasing_measure in eq4. simpl in eq4. apply Arith_prebase.lt_n_S_stt. apply Arith_prebase.lt_n_S_stt. apply Arith_prebase.lt_S_n in eq4.
rewrite Arith_prebase.plus_assoc_reverse_stt. rewrite (PeanoNat.Nat.add_comm (measure f + measure f0 + measure f1)).
rewrite (Arith_prebase.plus_assoc_reverse_stt (measure t1_1 + measure t1_2 + measure t1_3)). rewrite (PeanoNat.Nat.add_comm (measure t1_1 + measure t1_2 + measure t1_3)).
apply Plus.plus_lt_compat_l_stt. assumption. Qed.

Answer 1

您能否编辑您的问题以提供一个在复制和粘贴时可以工作的 MWE，以便可以试用？如果不尝试的话，调试是非常困难的（有时是不可能的）。

您能否指定您正在使用哪个版本的方程？等式 8.20 中改进了一些内容，例如 with 子句的处理。

否则，我只能看到这似乎是一个依赖问题。您正在尝试重写一个变量，但另一个变量依赖于它或类似的东西。 您可以先尝试展开/破坏检查，看看发生了什么。