75 lines
2.3 KiB
Coq
75 lines
2.3 KiB
Coq
|
Require Import Nat.
|
||
|
|
Require Import PeanoNat.
|
||
|
|
Require Import List.
|
||
|
|
Import ListNotations.
|
||
|
|
|
||
|
|
|
||
|
|
Definition subsequence (l s : list nat) :=
|
||
|
|
exists (l1: list nat) (l2 : list (list nat)),
|
||
|
|
length s = length l2
|
||
|
|
/\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
|
||
|
|
|
||
|
|
Definition subsequence2 (l s : list nat) :=
|
||
|
|
exists (t: list bool),
|
||
|
|
length t = length l /\ s = map snd (filter fst (combine t l)).
|
||
|
|
|
||
|
|
Theorem subsequence_eq_def : forall l s, subsequence l s <-> subsequence2 l s.
|
||
|
|
Proof.
|
||
|
|
intro l. induction l.
|
||
|
|
(* first part of the induction *)
|
||
|
|
intro s. unfold subsequence. unfold subsequence2.
|
||
|
|
split. exists nil. split. reflexivity. simpl.
|
||
|
|
destruct H. destruct H. destruct H.
|
||
|
|
assert (x = nil). destruct x. reflexivity. simpl in H0.
|
||
|
|
apply nil_cons in H0. contradiction H0. rewrite H1 in H0.
|
||
|
|
simpl in H0. assert (combine s x0 = nil).
|
||
|
|
destruct (combine s x0). reflexivity. simpl in H0.
|
||
|
|
apply nil_cons in H0. contradiction H0.
|
||
|
|
destruct x0. destruct s. reflexivity. simpl in H.
|
||
|
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
||
|
|
destruct s. reflexivity. simpl in H2.
|
||
|
|
symmetry in H2. apply nil_cons in H2. contradiction H2.
|
||
|
|
exists nil. exists nil. destruct s. simpl. easy.
|
||
|
|
destruct H. destruct H.
|
||
|
|
assert (x = nil). destruct x. reflexivity. simpl in H.
|
||
|
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
||
|
|
rewrite H1 in H0. simpl in H0.
|
||
|
|
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
||
|
|
(* second part of the induction *)
|
||
|
|
intro s. destruct s. unfold subsequence. unfold subsequence2. split.
|
||
|
|
exists (repeat false (S (length l))). rewrite repeat_length.
|
||
|
|
split. easy. simpl.
|
||
|
|
assert (forall u,
|
||
|
|
(nil: list nat)
|
||
|
|
= map snd (filter fst (combine (repeat false (length u)) u))).
|
||
|
|
intro u. induction u. reflexivity. simpl. assumption. apply H0.
|
||
|
|
exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity.
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
destruct H. destruct H. destruct H.
|
||
|
|
assert (x0 = nil). symmetry in H. apply length_zero_iff_nil in H.
|
||
|
|
assumption. rewrite H1 in H0. simpl in H0.
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
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.
|