Update

src/subsequences.v

@@ -712,13 +712,17 @@ Proof.
  Qed.
 
 
- Theorem subsequence_single {X: Type} :
-   forall (u: list X) a, In a u -> subsequence u [a].
+ Theorem subsequence_in {X: Type} :
+   forall (u: list X) a, In a u <-> subsequence u [a].
  Proof.
-   intro u. induction u; intro x; intro H. apply in_nil in H. contradiction.
+   intros u a. split.
+   induction u; intro H. apply in_nil in H. contradiction.
    destruct H. rewrite H. exists nil. exists [u]. split. reflexivity.
    simpl. rewrite app_nil_r. reflexivity. apply subsequence_cons_l.
    apply IHu. assumption.
+   intro H. destruct H. destruct H. destruct H. rewrite H0. apply in_or_app.
+   right. destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
+   left. reflexivity.
 Qed.
 
 
@@ -741,140 +745,10 @@ Proof.
   apply subsequence_incl in H1. apply incl_cons_inv in H1.
   destruct H1.
   assert (In a (filter f x)). apply filter_In. split; assumption.
-  apply subsequence_single. assumption. apply IHv. assumption.
+  apply subsequence_in. assumption. apply IHv. assumption.
   rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3.
   rewrite H0 in H3. assumption. reflexivity.
   simpl. rewrite H0. apply IHv. apply subsequence_cons_r in H.
   assumption.
 Qed.
 
-
-
-
-
-(** * Tests
-*)
-
-Example test1: subsequence [1;2;3;4;5] [1;3;5].
-Proof.
-  unfold subsequence.
-  exists [].
-  exists [[2];[4];[]]. simpl. easy.
-Qed.
-
-Example test2: subsequence [1;2;3;4;5] [2;4].
-Proof.
-  unfold subsequence.
-  exists [1].
-  exists [[3];[5]]. simpl. easy.
-Qed.
-
-Example test3: subsequence [1;2;3;4;5] [1;3;5].
-Proof.
-  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
-  exists [true; false; true; false; true].
-  split; reflexivity.
-Qed.
-
-
-
-
-
-
-
-Fixpoint smerge {X: Type} (l s1 s2 : list X) : Prop :=
-  match l with
-  | nil    => s1 = nil /\ s2 = nil
-  | hd::tl => match s1, s2 with
-              | nil, nil => False
-              | nil, _ => hd::tl = s2
-              | _, nil => hd::tl = s1
-              | hd1::tl1, hd2::tl2 =>
-                  (hd1 = hd2 /\ hd = hd1 /\ smerge tl tl1 tl2)
-                  \/ (hd1 <> hd2 /\ hd = hd1 /\ smerge tl tl1 s2)
-                  \/ (hd1 <> hd2 /\ hd = hd2 /\ smerge tl s1 tl2)
-              end
-  end.
-
-
-Theorem smerge_exchange {X: Type}:
-  forall (l s1 s2: list X), smerge l s1 s2 -> smerge l s2 s1.
-Proof.
-  intro l. induction l; intros s1 s2; intro H.
-  destruct s1; destruct s2. split; reflexivity.
-  destruct H. symmetry in H0. apply nil_cons in H0. contradiction H0.
-  destruct H. symmetry in H. apply nil_cons in H. contradiction H.
-  destruct H. symmetry in H. apply nil_cons in H. contradiction H.
-  destruct s1; destruct s2. assumption.
-  rewrite H. reflexivity. rewrite H. reflexivity.
-  destruct H. destruct H. destruct H0.
-  rewrite H0. rewrite H. apply IHl in H1. simpl. left.
-  split. reflexivity. split. reflexivity. assumption.
-  destruct H. destruct H. destruct H0. rewrite H0.
-  apply IHl in H1. right. right.
-  split. symmetry. assumption. split. reflexivity. assumption.
-  destruct H. destruct H0. apply IHl in H1. rewrite H0.
-  right. left. split. symmetry. assumption.
-  split. reflexivity. assumption.
-Qed.
-
-
-Theorem smerge_subsequence {X: Type}:
-  (forall x y : X, {x = y} + {x <> y})
-  -> forall (l s1 s2: list X),
-      smerge l s1 s2 -> subsequence l s1.
-Proof.
-  intro H. intro l. induction l; intros s1 s2; intro I.
-  destruct s1. apply subsequence_nil_r.
-  destruct I. symmetry in H0. apply nil_cons in H0. contradiction H0.
-
-  destruct s1; destruct s2.
-  apply subsequence_nil_r. apply subsequence_nil_r.
-  assert ({a = x} + {a <> x}). apply H. destruct H0. rewrite e in I.
-  rewrite e. simpl in I. rewrite I. apply subsequence_id.
-  simpl in I. inversion I. apply n in H1. contradiction H1.
-  assert ({a = x} + {a <> x}). apply H. destruct H0. rewrite e in I.
-  simpl in I. destruct I. destruct H0. destruct H1. apply IHl in H2.
-  rewrite e.
-  apply subsequence_eq_def_3. simpl. exists nil. exists l.
-  split. easy. apply subsequence_eq_def_2. apply subsequence_eq_def_1.
-  assumption.
-  destruct H0. destruct H0. destruct H1. apply IHl in H2.
-  rewrite e.
-  apply subsequence_eq_def_3. simpl. exists nil. exists l.
-  split. easy. apply subsequence_eq_def_2. apply subsequence_eq_def_1.
-  assumption. destruct H0. destruct H1. apply H0 in H1. contradiction H1.
-  destruct I. destruct H0. destruct H1. apply IHl in H2.
-  rewrite H1.
-  apply subsequence_eq_def_3. simpl. exists nil. exists l.
-  split. easy. apply subsequence_eq_def_2. apply subsequence_eq_def_1.
-  assumption. destruct H0. destruct H0. destruct H1.
-  apply n in H1. contradiction H1.
-  destruct H0. destruct H1. apply IHl in H2.
-  apply subsequence_cons_l. assumption.
-Qed.
-
-Theorem smerge_subsequence2 {X: Type}:
-  (forall x y : X, {x = y} + {x <> y})
-  -> forall (l s1 s2: list X), smerge l s1 s2 -> subsequence l s2.
-Proof.
-  intros. apply smerge_exchange in H.
-  apply smerge_subsequence with (s2 := s1); assumption.
-Qed. 
-
-
-
-
-
-
-
-
-
-Example test4: smerge [1; 2; 3; 2; 1] [1;2;1] [3;2].
-Proof.
-  simpl. right. left. split. easy.
-  split. reflexivity. right. left.
-  split. easy. split. reflexivity.
-  right. right. split. easy. split. easy.
-  right. right. split; easy.
-Qed.