如何用某个属性的术语替换某个术语？

Question

如果这个例子是人为设计的，我深表歉意，我试图证明一个类似的引理，其功能比 list_even 更复杂。我想证明一些关于列表翻译的属性。

Require Import Coq.Lists.List.
Import ListNotations.

Definition list_even (c : list nat) := map Nat.even c.

Lemma list_even_split : forall (c : list nat),
  c = nil \/
    exists c1 c2 b,
      c = c1 ++ c2
      /\ list_even c1 = b :: nil
      /\ list_even c = b :: list_even c2.

我得出的证明如下。

Proof.
  intros c.
  induction c.
  - left. reflexivity.
  - right.
    exists [a].
    exists c.
    (* I am stuck here. *)
    assert (e := Nat.even a).

如果我要亲手证明这一点，我的论点如下。

让c = [a] :: c2，所以c1 = [a]。通过Nat.Even_or_Odd，a为偶数或为奇数。如果 a 是偶数，则 b = true 等

  c = [a] ++ c2 /\
  list_even [a] = [true] /\
  list_even c = true :: list_even c2

如果 a 是奇数，那么 b = false 等等

  c = [a] ++ c2 /\
  list_even [a] = [false] /\
  list_even c = false :: list_even c2

通过简化和反身性成立。

但是，我不知道如何翻译

的证明状态

a : nat
  c : list nat
  IHc : c = [] \/
        (exists (c1 c2 : list nat) (b : bool),
           c = c1 ++ c2 /\
           list_even c1 = [b] /\ list_even c = b :: list_even c2)
  ============================
  exists b : bool,
    a :: c = [a] ++ c /\
    list_even [a] = [b] /\ list_even (a :: c) = b :: list_even c

变成了a.

的均匀度

我也不认为我需要对此进行归纳。

Answer 1

均匀性对于这个目标实际上并不重要，因为它只是关于映射的一个事实。 c 是空列表，或者 c 的形式是 c = x :: xs = [x] ++ xs 所以 map Nat.even c = Nat.even x ++ map Nat.even xs。因此，你可以得到像

这样的证明

Lemma list_even_split : forall (c : list nat),
  c = nil \/
    exists c1 c2 b,
      c = c1 ++ c2
      /\ list_even c1 = b :: nil
      /\ list_even c = b :: list_even c2.
Proof.
  intros c. 
   destruct c as [|x xs]; [left; auto 
                    |right; exists (x::nil); do 2 eexists; repeat split; eauto].
Qed.

然而，在其他需要变量均匀性的情况下，您可以通过

记录它

destruct (Nat.even x) eqn : NAT_IS_EVEN

如何用某个属性的术语替换某个术语？

How to replace a term with some property of the term?

coq

coq-tactic

如何用某个 属性 的术语替换某个术语？

How to replace a term with some property of the term?

coq

coq-tactic

如何用某个属性的术语替换某个术语？