Coq: проблемы со списком в индуктивном

Я новичок в 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.

Любая помощь будет оценена по достоинству!


theorem-proving induction coq
person Cristiano Sousa    schedule 08.06.2013    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Для вашей первой леммы я добавил две простые подзадачи (которые вы можете найти в библиотеке списков). Два других более прямолинейны.

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.

Я не скажу, что это менее сложно, чем ответ Руи, но я считаю, что это решение немного проще для понимания. Но в итоге они относительно близки.

Ура, В.

person Vinz    schedule 10.06.2013
comment
Я изо всех сил пытаюсь понять такую ​​тактику induction l1 as [ | hd tl hi ]; intros l2 x hIn; simpl in *. Я пытаюсь доказать леммы самостоятельно, имея ваши решения в качестве руководства, и я всегда избегаю использования такой последовательной тактики. Но я не могу воспроизвести доказательство, не прибегая к нему. - person Cristiano Sousa; 10.06.2013
comment
Забудьте о моем предыдущем комментарии. Используя вспомогательные леммы, вы и Руи предположили, что я могу доказать леммы самостоятельно. Большое тебе спасибо! - person Cristiano Sousa; 10.06.2013
comment
Для протокола, induction foo as [ pattern ] здесь только для того, чтобы назвать новые термины, которые создаст тактика индукции. Вы можете забыть об этом и использовать автоматическое именование. The; Оператор позволяет связать несколько тактик. A ; B означает выполнение тактики A для текущей цели, затем выполнение B для всех созданных подцелей, которые могли быть сгенерированы. В моем случае это было просто для того, чтобы представить вещи в контексте и упростить все выражения. Надеюсь, поможет. - person Vinz; 11.06.2013
comment
induction l1 as [ | hd tl hi] означает выполнение индукции по l1. В случае nil (первый случай) ничего не делать. В минусах (второй случай, после |) переименуйте голову hd, хвост tl и гипотезу индукции hi. - person Vinz; 11.06.2013

arrow_upward
1
arrow_downward

Когда цель экзистенциально определена количественно, вы должны привести конкретный пример объекта с заявленным свойством, а когда гипотеза экзистенциально количественно определена, вам разрешено предположить, что один такой объект существует, и представить его. См. Ответы на часто задаваемые вопросы 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.
person Community    schedule 09.06.2013
comment
Доказательство намного сложнее, чем я ожидал, и по сравнению со всеми другими упражнениями, которые я делал. - person Cristiano Sousa; 09.06.2013