当没有打字信息时，如何在Coq问题中断言（H4：[] = [] ++ []）？

Question

我被限制在以下证明中，因为我不知道如何断言（H4：[] = [] ++ []）。在下面的最后一行中，因此应用MApp，因为上下文中没有已知的类型信息。另外，我不能从以前的练习中应用app_nil_r，或者如果我不确定该怎么做-我正在尝试应用（app_nil_r []）。任何提示如何解决此问题？

错误：无法在...中推断类型为“ Type”的nil的隐式参数X

Fixpoint match_eps (re: @reg_exp ascii) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr => true
  | Char _ => false
  | App r1 r2 => (match_eps r1) && (match_eps r2)
  | Union r1 r2 => (match_eps r1) || (match_eps r2)
  | Star r => match_eps r
  end.

Lemma match_eps_refl : refl_matches_eps match_eps.
Proof.
  unfold refl_matches_eps.
  intros.
  induction re.
  - simpl. apply ReflectF. unfold not. intros. inversion H.
  - simpl. apply ReflectT. apply MEmpty.
  - simpl. apply ReflectF. unfold not. intros.  inversion H.
  - simpl. inversion IHre1. inversion IHre2. 
    simpl. apply ReflectT.
    assert (H4: [] = [] ++ []).

Answer 1

您可以将MApp与显式字符串作为参数来应用以避免歧义：

apply (MApp [] _ []).  (* Provided the goal is of the form   ([] ++ []) =~ App re0 re1   (i.e., the conclusion of the type of MApp) or   [] =~ App re0 re1  *)
                       (* (this should be fine because ([] ++ []) is definitionally equal to []) *)

---

声明[] = [] ++ []是有问题的，因为[]的类型不明确。在这里，此断言不是必需的，但是通常，您可以显式地应用nil构造函数以固定其类型：

assert (@nil ascii = [] ++ []).  (* Note: [] is notation for "@nil _", leaving _ to be determined by type inference. All we're doing here is replacing "_" with something explicit. *)