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 06:50:55 +01:00
parent 0717e31ca9
commit 1e55808cff
1 changed files with 76 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
src/subsequences.v
View File

@ -3,6 +3,8 @@ Require Import PeanoNat.
Require Import List.
Import ListNotations.
Require Import Lia.
Definition subsequence (l s : list Type) :=
exists (l1: list Type) (l2 : list (list Type)),
@ -13,6 +15,13 @@ Definition subsequence2 (l s : list Type) :=
exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)).
(*
TODO: problème, les éléments de l ne sont pas uniques ; or
il doit pouvoir y avoir des différences dans la décision de les
prendre ou non
Definition subsequence3 (l s : list Type) :=
exists f, s = fst (partition f l).
*)
Theorem subsequence_nil_r : forall (l : list Type), subsequence l nil.
Proof.
@ -52,6 +61,33 @@ Proof.
Qed.
Theorem subsequence2_cons_l : forall (l s: list Type) (a: Type),
subsequence2 l s -> subsequence2 (a::l) s.
Proof.
intros l s a. intro H. unfold subsequence2 in H.
destruct H. destruct H. exists (false::x).
split. simpl. apply eq_S. assumption.
simpl. assumption.
Qed.
Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type),
subsequence2 l (a::s) -> subsequence2 l s.
Proof.
intro l. induction l. intros. apply subsequence2_nil_cons_r in H.
contradiction H. intros s a0 . intro H. 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. inversion H0.
unfold subsequence2. exists (false::x). split.
rewrite <- H. reflexivity. reflexivity.
simpl in H0.
apply subsequence2_cons_l. apply IHl with (a := a0).
unfold subsequence2. exists (x). split. inversion H.
reflexivity. assumption.
Qed.
Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
Proof.
@ -82,6 +118,31 @@ Proof.
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.
@ -89,12 +150,27 @@ Proof.
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.
Theorem subsequence2_dec :