2

我是 Coq 的新手，但通过一些努力，我能够证明各种归纳引理。但是，我卡在所有使用以下归纳定义的练习中：

Inductive In (A:Type) (y:A) : list A -> Prop :=
     | InHead : forall xs:list A, In y (cons y xs)
     | InTail : forall (x:A) (xs:list A), In y xs -> In y (cons x xs).

我得到的最远的是以下引理：

Lemma my_In_rev : forall (A:Type) (x:A) (l:list A), In x l -> In x (rev l).
Proof.
induction l.
simpl.
trivial.
simpl.
intros.

以下两个引理我无法通过第一步，因为我exists在使用intros.

Lemma my_In_map :  forall (A B:Type) (y:B) (f:A->B) (l:list A), In y (map f l) -> exists x : A, In x l /\ y = f x.

Lemma my_In_split : forall (A:Type) (x:A) (l : list A), In x l -> exists l1, exists l2, l = l1 ++ (x::l2).
Proof.

任何帮助，将不胜感激！

4

2 回答 2

2

对于您的第一个引理，我添加了两个简单的子引理（您可以在列表库中找到）。其他两个更直接。

Require Import List.

Lemma In_concat_l: forall (A: Type) (l1 l2: list A) (x:A), 
   In x l1 -> In x (l1 ++ l2).
Proof.
intros A.
induction l1 as [ | hd tl hi ]; intros l2 x hIn; simpl in *.
- contradiction.
- destruct hIn.
  + left; assumption.
  + right; now apply hi.
Qed.

Lemma In_concat_r: forall (A: Type) (l1 l2: list A) (x:A), 
   In x l2 -> In x (l1 ++ l2).
intros A.
induction l1 as [ | hd tl hi ]; intros l2 x hIn; simpl in *.
- assumption.
- right; now apply hi.
Qed.

Lemma my_In_rev : forall (A:Type) (x:A) (l:list A), In x l -> In x (rev l).
Proof.
intros A x l.
induction l as [ | hd tl hi ]; intros hIn; simpl in *.
- contradiction.
- destruct hIn.
  + apply In_concat_r.
    rewrite H.
    now constructor.
  + apply In_concat_l.
    now apply hi.
Qed.

Lemma my_In_map :  forall (A B:Type) (y:B) (f:A->B) (l:list A), In y (map f l) -> exists x : A, In x l /\ y = f x.
Proof.
intros A B y f l.
induction l as [ | hd tl hi]; intros hIn; simpl in *.
- contradiction.
- destruct hIn.
  + exists hd; split.
    left; reflexivity.
    symmetry; assumption.
  + destruct (hi H) as [x0 [ h1 h2]].
    exists x0; split.
    right; assumption.
    assumption.
Qed.

Lemma my_In_split : forall (A:Type) (x:A) (l : list A), In x l -> exists l1, exists l2, l = l1 ++ (x::l2).
Proof.
intros A x l.
induction l as [ | hd tl hi]; intros hIn; simpl in *.
- contradiction.
- destruct hIn.
  rewrite H.
  exists nil; exists tl; simpl; reflexivity.
  destruct (hi H) as [ l1 [ l2 h ]].
  exists (hd :: l1); exists l2.
  rewrite <- app_comm_cons; rewrite h.
  reflexivity.
Qed.

我不会说它没有 Rui 的答案那么复杂，但我发现这个解决方案更容易理解。但最终，他们还是比较接近的。

干杯，V。

于 2013-06-10T07:39:10.643 回答
1

当目标被存在量化时，您必须给出具有所述属性的对象的具体示例，并且当假设被存在量化时，您可以假设存在一个这样的对象并引入它。请参阅常见问题解答47、53和54。顺便说一句，谓词已经定义在. 在这里查看。Coq 策略的参考在这里。InCoq.Lists.List

第一个引理的证明：

Require Import Coq.Lists.List.
Require Import Coq.Setoids.Setoid.

Inductive In {A : Type} (y : A) : list A -> Prop :=
  | InHead : forall xs : list A, In y (cons y xs)
  | InTail : forall (x : A) (xs : list A), In y xs -> In y (cons x xs).

Lemma L1 : forall (t1 : Type) (l1 : list t1) (o1 o2 : t1),
  In o1 (o2 :: l1) <-> o1 = o2 \/ In o1 l1.
Proof.
intros t1 l1 o1 o2. split.
  intros H1. inversion H1 as [l2 [H3 H4] | o3 l2 H2 [H3 H4]].
    left. reflexivity.
    right. apply H2.
  intros H1. inversion H1 as [H2 | H2].
    rewrite H2. apply InHead.
    apply InTail. apply H2.
Qed.

Lemma my_In_map : forall (A B : Type) (l : list A) (y : B) (f : A -> B),
  In y (map f l) -> exists x : A, In x l /\ y = f x.
Proof.
intros A B. induction l as [| z l H1].
  intros y f H2. simpl in *. inversion H2.
  intros y f H2. simpl in *. rewrite L1 in H2. inversion H2 as [H3 | H3].
    exists z. split.
      apply InHead.
      apply H3.
    assert (H4 := H1 _ _ H3). inversion H4 as [x [H5 H6]]. exists x. split.
      rewrite L1. right. apply H5.
      apply H6.
Qed.
于 2013-06-09T13:47:47.303 回答