This commit is contained in:
Thomas Baruchel 2023-10-30 16:40:11 +01:00
parent c49f18c94a
commit f5c5c7928e

View File

@ -6,12 +6,12 @@ Import ListNotations.
Require Import Lia.
Definition subsequence (l s : list Type) :=
exists (l1: list Type) (l2 : list (list Type)),
Definition subsequence {X: Type} (l s : list X) :=
exists (l1: list X) (l2 : list (list X)),
length s = length l2
/\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
Definition subsequence2 (l s : list Type) :=
Definition subsequence2 {X: Type} (l s : list X) :=
exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)).
@ -112,10 +112,10 @@ Proof.
destruct x. destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
simpl in H0. inversion H0. exists l0. exists x0.
inversion H. split; reflexivity.
inversion H. rewrite H3. split; reflexivity.
destruct x0. simpl in H0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
exists (x ++ (a::l0)). exists x0. inversion H. split. reflexivity.
exists (x ++ (a::l0)). exists x0. inversion H. rewrite H2. split. reflexivity.
inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
rewrite app_comm_cons. reflexivity.
@ -130,7 +130,7 @@ Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
Proof.
intros l s a. split. intro H. unfold subsequence2 in H.
destruct H. destruct H. destruct x. inversion H0.
destruct b. exists (x). split. inversion H. reflexivity. simpl in H0.
destruct b. exists (x). split. inversion H. rewrite H2. reflexivity. simpl in H0.
inversion H0. reflexivity. simpl in H0. inversion H.
assert (subsequence2 l (a::s)). exists x. split; assumption.
apply subsequence2_cons_r with (a := a). assumption.
@ -200,7 +200,7 @@ Qed.
Theorem subsequence_eq_def :
(forall x y : Type, {x = y} + {x <> y})
-> (forall l s, subsequence l s <-> subsequence2 l s).
-> (forall l s : list Type, subsequence l s <-> subsequence2 l s).
Proof.
intro I. intro l. induction l.
(* first part of the induction *)