标签: logical-foundations

这是我对回文的归纳定义:

Inductive pal { X : Type } : list X -> Prop :=
  | pal0 : pal []
  | pal1 : forall ( x : X ), pal [x]
  | pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ).

我想从Software Foundations中证明这个定理:

Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ),
  l = rev l -> …

我正在使用在线书籍“软件基础”来了解 Coq。

第二章要求证明“plus_assoc”定理：

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.

我利用了两个先前证明的定理：

Theorem plus_comm : forall n m : nat, n + m = m + n.
Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).

我在 n 上使用归纳证明了 plus_assoc 定理：

Proof.
  intros n m p.
  induction n as [ | n' ].
    reflexivity.

    rewrite plus_comm.
    rewrite <- plus_n_Sm.
    rewrite …

感谢软件基金会的电子书，我目前正在学习 coq 。我成功地添加了如下内容：

Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition plus (n m : cnat) : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).

但由于以下错误，我坚持使用 exp：

Definition exp (n m : cnat) : cnat :=
  m cnat (mult n) n.
(*
In environment
n : cnat
m : cnat
The term "cnat" has type "Type@{cnat.u0+1}"
while …

我正在努力完成逻辑基础归纳命题章节中le_exercises的一系列练习。

该系列主要基于归纳关系le，定义如下：

Inductive le : nat -> nat -> Prop :=\n  | le_n (n : nat)                : le n n\n  | le_S (n m : nat) (H : le n m) : le n (S m).\n\nNotation "n <= m" := (le n m).\n

我所坚持的特定定理如下：

Theorem add_le_cases : forall n m p q,\n  n + m <= p + q -> n <= p \\/ m <= q.\n

到目前为止我成功证明的本系列中的先前定理是：

Lemma le_trans …

在逻辑章节中介绍了反向列表函数的尾递归版本。我们需要证明它可以正常工作：

Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
  match l1 with
  | [] => l2
  | x :: l1' => rev_append l1' (x :: l2)
  end.

(* Tail recursion rev *)
Definition tr_rev {X} (l : list X) : list X :=
  rev_append l [].

但在证明它之前，我想证明一个引理：

Lemma rev_append_app: forall (X: Type) (x: X) (l : list X),
    rev_append l [x] = rev_append l [] ++ [x].
Proof.
  intros X x l. induction l as [| …

我试图证明以下引理：

Inductive even : nat \xe2\x86\x92 Prop :=\n| ev_0 : even 0\n| ev_SS (n : nat) (H : even n) : even (S (S n)).\n\nLemma even_Sn_not_even_n : forall n,\n    even (S n) <-> not (even n).\nProof.\n  intros n. split.\n  + intros H. unfold not. intros H1. induction H1 as [|n\' E\' IHn].\n    - inversion H.\n    - inversion_clear H. apply IHn in H0. apply H0.\n  + unfold not. intros H. induction n as [|n\' E\' IHn].\n    -\nQed.\n

这是我最后得到的：

试图理解@keep_learning的答案，我一步一步地浏览了这段代码：

Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).

Example test_nostutter_4: not (nostutter [3;1;1;4]).
Proof.
  intro.
  inversion_clear H.
  inversion_clear H0.
  unfold not in H2.
  (* We are here *)
  specialize (H2 eq_refl).
  apply H2.
Qed.

这是我们在执行 specialize 之前所拥有的

H1 : 3 …