Coq中使用Equations库重写目标失败问题求助

问题场景 #

当前目标表达式：

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).
(* 该定义告知Coq，我们将通过证明(measure term)会递减（lt）来验证良基性wf *)
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.

解决方法 #

问题核心是evalMS_unfold_clause_1的第二个参数要求依赖对类型为{b | evalS t1 = b}，但inspect o的类型是{b | o = b}，直接rewrite会破坏类型依赖关系。

方法1：用case_eq拆分情况 #

通过case_eq对evalS (if_then_else t1_1 t1_2 t1_3)进行分情况讨论，结合假设H匹配到对应分支：

case_eq (evalS (if_then_else t1_1 t1_2 t1_3)); intro Heq.
rewrite H in Heq. simpl Heq.
(* 此时目标会自动匹配到evalMS的else分支，简化为None *)

方法2：使用Equations生成的归纳原理 #

直接调用Equations为evalMS生成的归纳原理evalMS_elim，对目标的evalMS调用进行归纳，结合H来推导：

apply evalMS_elim with (1 := H); auto.

方法3：手动构造符合类型要求的依赖对 #

基于假设H构造出{b | evalS (if_then_else t1_1 t1_2 t1_3) = b}类型的项，替换原有的inspect项：

pose proof (exist _ None H) as H_inspect.
replace (inspect (evalS (if_then_else t1_1 t1_2 t1_3))) with H_inspect.
(* 替换后即可正常rewrite或简化 *)

内容的提问来源于stack exchange，提问作者Mohamed Elsheikh