baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-10-30 07:51:59 +01:00
parent c046150aa9
commit 951e3cb244
1 changed files with 5 additions and 91 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

96
src/subsequences.v
View File

@ -98,45 +98,12 @@ Proof.
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.
intro H. destruct H. destruct H. exists (true :: x).
split. simpl. apply eq_S. assumption. simpl. rewrite H0. reflexivity.
Qed.
(* pas mal *)
intros l s. generalize l. induction s.
intros l0 a. split; intro H. apply subsequence2_nil_r.
exists (true :: (map (fun x => false) l0)).
split. simpl. rewrite map_length. reflexivity.
simpl. induction l0. reflexivity.
assert (subsequence2 l0 []). apply subsequence2_nil_r.
apply IHl0 in H0. simpl. assumption.
intros l0 a0. split. intro H.
(* pas mal *)
intro l. induction l. intros s a. split. intro H.
destruct s. apply subsequence2_nil_r.
unfold subsequence2 in H. destruct H. destruct H.
destruct x. symmetry in H0. apply nil_cons in H0. contradiction H0.
destruct b.
simpl in H0. destruct x.
simpl in H0. inversion H0. inversion H.
simpl in H0. destruct x.
simpl in H0. inversion H0. inversion H.
intro H. destruct s. exists [true]. split; reflexivity.
apply subsequence2_nil_cons_r in H. contradiction H.
intros s a0. split. intro H.
(*
assert (forall (l s: list Type) t,
s = map snd (filter fst (combine t l))
-> length t = length l
@ -161,60 +128,7 @@ Proof.
apply IHt with (l := l0). inversion J. simpl.
reflexivity. inversion K. reflexivity.
(* fin de la démonstration de H *)
intros l1 l2 a. split; intro I.
unfold subsequence2 in I. destruct I. destruct H0.
(*
induction x. symmetry in H0.
apply Nat.neq_succ_0 in H0. contradiction H0.
destruct a0. inversion H1. unfold subsequence2. exists x.
split. inversion H0. reflexivity. reflexivity.
simpl in H1.
apply IHx.
*)
assert (count_occ Bool.bool_dec x true = length (a::l2)).
apply H with (l := a::l1); assumption.
assert (In true x). rewrite count_occ_In with (eq_dec := Bool.bool_dec).
rewrite H2. simpl. lia. (* TODO *)
apply In_split in H3. destruct H2. destruct H2.
intros l1 l2 a. split; intro I.
unfold subsequence2 in I. destruct I. destruct H0. destruct x.
simpl in H0. symmetry in H0.
apply PeanoNat.Nat.neq_succ_0 in H0. contradiction H0.
destruct b. simpl in H0. inversion H1. rewrite <- H3.
unfold subsequence2. exists x. split. inversion H0. reflexivity.
assumption.
(*
simpl in H1. unfold subsequence2. exists x. split. inversion H0.
reflexivity.
*)
simpl in H1.
apply H in H1. simpl in H1.
assert (count_occ Bool.bool_dec x true = length l2).
apply H with (l := l1). assumption. inversion H0. assumption.
assert (count_occ Bool.bool_dec x true = length (a::l2)).
apply H with (l := l1). assumption. inversion H0. assumption.
destruct x. symmetry in H2. apply PeanoNat.Nat.neq_succ_0 in H2.
contradiction H2.
*)