Update

src/subsequences2.v

@@ -304,69 +304,66 @@ Proof.
 Qed.
 
 
-
-
-
-
-
-Theorem subsequence_eq {X: Type} :
+Theorem Subsequence_eq {X: Type} :
   forall (u v: list X),
-  subsequence u v -> subsequence v u -> u = v.
+  Subsequence u v -> Subsequence v u -> u = v.
 Proof.
-  intro u. induction u; intro v; intros H I;
-  apply subsequence_eq_def_1 in H; apply subsequence_eq_def_1 in I.
+  intro u. induction u; intro v; intros H I.
 
   destruct v. reflexivity.
-  apply subsequence2_nil_cons_r in H. contradiction H.
-  destruct v. apply subsequence2_nil_cons_r in I. contradiction I.
+  apply Subsequence_nil_cons_r in H. contradiction H.
+  destruct v. apply Subsequence_nil_cons_r in I. contradiction I.
+
+  apply Subsequence_bools in H. apply Subsequence_bools in I.
 
   destruct H. destruct H. destruct I. destruct H1.
   destruct x0. apply O_S in H. contradiction H.
   destruct x1. apply O_S in H1. contradiction H1.
   destruct b; destruct b0.
 
-  assert (subsequence2 u v). exists x0.
+  assert (Subsequence u v). apply Subsequence_bools. exists x0.
   split; inversion H; inversion H0; reflexivity.
-  assert (subsequence2 v u). exists x1.
+  assert (Subsequence v u). apply Subsequence_bools. exists x1.
   split; inversion H1; inversion H2; reflexivity.
-  apply subsequence_eq_def_2 in H3; apply subsequence_eq_def_3 in H3.
-  apply subsequence_eq_def_2 in H4; apply subsequence_eq_def_3 in H4.
   apply IHu in H4. rewrite H4. inversion H0. reflexivity. assumption.
 
-  assert (subsequence2 u v). exists x0.
+  assert (Subsequence u v). apply Subsequence_bools. exists x0.
   split; inversion H; inversion H0; reflexivity.
-  assert (subsequence2 v (a::u)). exists x1.
+  assert (Subsequence v (a::u)). apply Subsequence_bools. exists x1.
   split; inversion H1; inversion H2; reflexivity.
-  assert (subsequence u (a::u)). apply subsequence_trans with (l2 := v);
-  apply subsequence_eq_def_3; apply subsequence_eq_def_2; assumption.
-  apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
+  assert (Subsequence u (a::u)).
+  apply Subsequence_trans with (l2 := v); assumption.
+  apply Subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
+  contradiction.
+
+  assert (Subsequence u (x::v)). apply Subsequence_bools. exists x0.
+  split; inversion H; inversion H0; reflexivity.
+  assert (Subsequence v u). apply Subsequence_bools. exists x1.
+  split; inversion H1; inversion H2; reflexivity.
+  assert (Subsequence v (x::v)). apply Subsequence_trans with (l2 := u);
+  assumption.
+  apply Subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
   contradiction H5.
 
-  assert (subsequence2 u (x::v)). exists x0.
+  assert (Subsequence u (x::v)). apply Subsequence_bools. exists x0.
   split; inversion H; inversion H0; reflexivity.
-  assert (subsequence2 v u). exists x1.
+  assert (Subsequence v (a::u)). apply Subsequence_bools. exists x1.
   split; inversion H1; inversion H2; reflexivity.
-  assert (subsequence v (x::v)). apply subsequence_trans with (l2 := u);
-  apply subsequence_eq_def_3; apply subsequence_eq_def_2; assumption.
-  apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
-  contradiction H5.
-
-  assert (subsequence2 u (x::v)). exists x0.
-  split; inversion H; inversion H0; reflexivity.
-  assert (subsequence2 v (a::u)). exists x1.
-  split; inversion H1; inversion H2; reflexivity.
-  apply subsequence2_cons_r in H3. apply subsequence2_cons_r in H4.
-  apply subsequence_eq_def_2 in H3. apply subsequence_eq_def_2 in H4.
-  apply subsequence_eq_def_3 in H3. apply subsequence_eq_def_3 in H4.
+  apply Subsequence_cons_r in H3. apply Subsequence_cons_r in H4.
   apply IHu in H4. rewrite H4 in H0. rewrite H4 in H.
-  simpl in H0. assert (subsequence2 v (x::v)). exists x0.
+  simpl in H0.
+  assert (Subsequence v (x::v)). apply Subsequence_bools. exists x0.
   split. inversion H. reflexivity. assumption.
-  apply subsequence_eq_def_2 in H5. apply subsequence_eq_def_3 in H5.
-  apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
+  apply Subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
   contradiction H5. assumption.
 Qed.
 
 
+
+
+
+
+
 Theorem subsequence_length_eq {X: Type} :
   forall (u v: list X),
   subsequence u v -> length u = length v -> u = v.