Update

src/subsequences2.v

@@ -161,80 +161,52 @@ Proof.
 Qed.
 
 
-Lemma subsequence_dec_alt {X: Type}:
-  (forall x y : X, {x = y} + {x <> y})
-  -> forall (l s : list X), { exists (t: list bool),
-        length t = length l /\ s = map snd (filter fst (combine t l)) }
-    + { ~ exists (t: list bool),
-        length t = length l /\ s = map snd (filter fst (combine t l)) }.
-Proof.
-
-  intro H.
-  intro l. induction l; intro s. destruct s. left.
-  rewrite <- subsequence_bools. apply Subsequence_nil_r.
-  right. rewrite <- subsequence_bools. apply Subsequence_nil_cons_r.
-
-  assert (
-      { exists (t: list bool),
-        length t = length l /\ s = map snd (filter fst (combine t l)) }
-    + { ~ exists (t: list bool),
-        length t = length l /\ s = map snd (filter fst (combine t l)) }).
-
-  apply IHl.
-  destruct H0.
-  rewrite <- subsequence_bools in e.
-
-  rewrite <- Subsequence_cons_eq with (a := a) in e.
-  apply Subsequence_cons_r in e. rewrite subsequence_bools in e.
-  left; assumption.
-
-  destruct s. rewrite <- subsequence_bools in n.
-  left.
-  rewrite <- subsequence_bools.
-  apply Subsequence_nil_r.
-  assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
-  destruct IHl with (s := s); [ left | right ];
-  rewrite <- subsequence_bools;
-  rewrite Subsequence_cons_eq. rewrite subsequence_bools. assumption.
-  rewrite subsequence_bools. assumption.
-
-  right. intro I.
-  destruct I. destruct H0. destruct x0.
-  symmetry in H1.
-  apply nil_cons in H1. contradiction H1.
-  destruct b.
-  inversion H1. rewrite H3 in n0. easy.
-  apply n. exists x0; split; inversion H0; easy.
-Qed.
-
-
 Theorem Subsequence_dec {X: Type}:
   (forall x y : X, {x = y} + {x <> y})
   -> forall (l s : list X), { Subsequence l s } + { ~ Subsequence l s }.
 Proof.
-  intro H. intros l s.
+  intro H. intro l. induction l; intro s. destruct s. left.
-  assert (
+  apply Subsequence_nil_r. right. apply Subsequence_nil_cons_r.
-      { exists (t: list bool),
+
-        length t = length l /\ s = map snd (filter fst (combine t l)) }
+  assert ({ Subsequence l s} + { ~ Subsequence l s }).
-    + { ~ exists (t: list bool),
+  apply IHl. destruct H0.
-        length t = length l /\ s = map snd (filter fst (combine t l)) }).
+
-  apply subsequence_dec_alt. assumption. destruct H0.
+  rewrite <- Subsequence_cons_eq with (a := a) in s0.
-  rewrite <- subsequence_bools in e. left. assumption.
+  apply Subsequence_cons_r in s0. rewrite subsequence_bools in s0.
-  right. intro I. apply subsequence_bools in I. apply n in I. contradiction I.
+  left. rewrite subsequence_bools. assumption.
+
+  destruct s. left. apply Subsequence_nil_r.
+  assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
+  destruct IHl with (s := s); [ left | right ];
+  rewrite Subsequence_cons_eq. assumption. assumption.
+
+  right. intro I. rewrite subsequence_bools in I.
+  destruct I. destruct H0. destruct x0.
+  symmetry in H1. apply nil_cons in H1. contradiction H1.
+  destruct b. inversion H1. rewrite H3 in n0. easy.
+  apply n. rewrite subsequence_bools. exists x0; split; inversion H0; easy.
 Qed.
 
 
 (** * Various general properties
 *)
 
-Theorem subsequence_id {X: Type} :
+Theorem Subsequence_id {X: Type} :
-  forall u : list X, subsequence u u.
+  forall u : list X, Subsequence u u.
 Proof.
-  intro u. apply subsequence_eq_def_3.
+  intro u. induction u. easy. exists nil. exists u. split; easy.
-  induction u. easy. exists nil. exists u.
-  split; easy.
 Qed.
 
+
+
+
+
+
+
+
+
+
+
 Theorem subsequence_app {X: Type} :
   forall l1 s1 l2 s2 : list X,
   subsequence l1 s1 -> subsequence l2 s2 -> subsequence (l1++l2) (s1++s2).