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.

次の 2 つの補題は、最初のステップを通過できませ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

最初のレンマとして、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.

ルイの答えよりも複雑ではないとは言いませんが、この解決策は少し理解しやすいと思います。しかし、結局のところ、それらは比較的近いものです。

乾杯、V.

于 2013-06-10T07:39:10.643 に答える
1

目標が存在論的に量化されている場合は、述べられた特性を持つオブジェクトの具体例を示す必要があり、仮説が存在論的に量化されている場合は、そのようなオブジェクトが存在すると仮定して導入することができます。FAQ 47、53 、および54を参照してください。ちなみにIn述語は既に で定義されていCoq.Lists.Listます。ここでチェックしてください。Coq タクティクスのリファレンスはこちらです。

最初の補題の証明:

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 に答える