This commit is contained in:
Thomas Baruchel 2023-11-22 15:15:29 +01:00
parent 528cb76db3
commit dedf79490b

View File

@ -332,6 +332,14 @@ Qed.
(** * Various general properties
*)
Theorem subsequence_id {X: Type} :
forall u : list X, subsequence u u.
Proof.
intro u. apply subsequence_eq_def_3.
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).
@ -442,7 +450,7 @@ Proof.
Qed.
Theorem subsequence_id {X: Type} :
Theorem subsequence_eq {X: Type} :
forall (u v: list X),
subsequence u v -> subsequence v u -> u = v.
Proof.
@ -499,6 +507,39 @@ Proof.
contradiction H5. assumption.
Qed.
Theorem subsequence_reverse {X: Type} :
forall (u v: list X), subsequence u v -> subsequence (rev u) (rev v).
Proof.
intros u v. intro H.
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
apply subsequence_eq_def_1 in H. destruct H. destruct H.
exists (rev x). split. rewrite rev_length. rewrite rev_length.
assumption. rewrite H0.
assert (LEMMA : forall (l1: list bool) (l2: list X),
length l1 = length l2
-> combine (rev l1) (rev l2) = rev (combine l1 l2)).
intro l1. induction l1; intro l2; intro I. reflexivity.
destruct l2. inversion I. inversion I. apply IHl1 in H2.
simpl.
assert (LEMMA2 : forall (u w : list bool) (v x : list X),
length u = length v
-> combine (u ++ w) (v ++ x) = (combine u v) ++ (combine w x)).
intro u0. induction u0; intros w v0 x1; intro J.
symmetry in J. apply length_zero_iff_nil in J. rewrite J.
reflexivity. destruct v0. inversion J. inversion J.
apply IHu0 with (w := w) (x := x1) in H3. simpl. rewrite H3.
reflexivity. rewrite LEMMA2. rewrite IHl1. reflexivity.
inversion I. reflexivity. rewrite rev_length. rewrite rev_length.
inversion I. reflexivity. rewrite LEMMA. rewrite <- map_rev.
assert (LEMMA3: forall v (w: list (bool * X)),
rev (filter v w) = filter v (rev w)).
intros v0 w. induction w. reflexivity. simpl. rewrite filter_app.
simpl. destruct (v0 a). simpl. rewrite IHw. reflexivity.
rewrite IHw. symmetry. apply app_nil_r. rewrite LEMMA3.
reflexivity. assumption.
Qed.
@ -526,3 +567,107 @@ Proof.
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.