From aad563b8cd528a88869680ba5c99ad671256f396 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 14:02:22 +0300 Subject: [PATCH 01/18] Remmoving a lemma from FinExtras.v --- theories/VLSM/Lib/FinExtras.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/VLSM/Lib/FinExtras.v b/theories/VLSM/Lib/FinExtras.v index 3bec5d19..9ef45560 100644 --- a/theories/VLSM/Lib/FinExtras.v +++ b/theories/VLSM/Lib/FinExtras.v @@ -11,12 +11,12 @@ Fixpoint up_to_n_listing | S n' => n' :: up_to_n_listing n' end. -Lemma up_to_n_listing_length +(*Lemma up_to_n_listing_length (n : nat) : length (up_to_n_listing n) = n. Proof. induction n; simpl; congruence. -Qed. +Qed.*) Lemma up_to_n_full (n : nat) From 49aa2954ab67000a979c34d1a5181d9beadab58f Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 14:18:05 +0300 Subject: [PATCH 02/18] Removing a lemma from FinFunExtras.v --- theories/VLSM/Lib/FinFunExtras.v | 9 --------- 1 file changed, 9 deletions(-) diff --git a/theories/VLSM/Lib/FinFunExtras.v b/theories/VLSM/Lib/FinFunExtras.v index 063584f5..dbe3d35d 100644 --- a/theories/VLSM/Lib/FinFunExtras.v +++ b/theories/VLSM/Lib/FinFunExtras.v @@ -68,13 +68,4 @@ Proof. by destruct a;simpl;congruence. Qed. -Lemma right_finite - (sum_finite : Listing sum_listing) - : Listing (right_listing sum_finite). -Proof. - revert sum_finite. - apply map_option_listing with (g:=inr); [| done]. - by destruct a;simpl;congruence. -Qed. - End sum_listing. From a00225e5efc27be6b01968086d1db81b70846b75 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 14:26:25 +0300 Subject: [PATCH 03/18] Removing a lemma from FinSetExtras.v --- theories/VLSM/Lib/FinSetExtras.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/VLSM/Lib/FinSetExtras.v b/theories/VLSM/Lib/FinSetExtras.v index 61bbc1c1..cbddce77 100644 --- a/theories/VLSM/Lib/FinSetExtras.v +++ b/theories/VLSM/Lib/FinSetExtras.v @@ -58,13 +58,13 @@ Proof. lia. Qed. -Lemma intersection_size1 +(*Lemma intersection_size1 (X Y : C) : size (X ∩ Y) <= size X. Proof. apply (subseteq_size (X ∩ Y) X). set_solver. -Qed. +Qed.*) Lemma intersection_size2 (X Y : C) : From b609de3add7640567b897d8698bd06448146d193 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 15:25:25 +0300 Subject: [PATCH 04/18] Removing lemmas from ListExtras.v --- theories/VLSM/Lib/ListExtras.v | 189 ++++++++++++++++----------------- 1 file changed, 94 insertions(+), 95 deletions(-) diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v index 4637e14b..b9494eb1 100644 --- a/theories/VLSM/Lib/ListExtras.v +++ b/theories/VLSM/Lib/ListExtras.v @@ -6,13 +6,13 @@ From VLSM Require Import Lib.Preamble. (** * Utility lemmas about lists *) (** A list is empty if it has no members *) -Lemma empty_nil [X:Type] (l:list X) : +(*Lemma empty_nil [X:Type] (l:list X) : (forall v, ~In v l) -> l = []. Proof. clear. destruct l as [| a]; [done |]. simpl. intro H. elim (H a). by left. -Qed. +Qed.*) (** It is decidable whether a list is null or not *) Lemma null_dec {S} (l : list S) : Decision (l = []). @@ -59,13 +59,13 @@ Proof. by induction tl as [| hd tl IHl]. Qed. -Lemma remove_hd_last {X} : +(*Lemma remove_hd_last {X} : forall (hd1 hd2 d1 d2 : X) (tl : list X), List.last (hd1 :: hd2 :: tl) d1 = List.last (hd2 :: tl) d2. Proof. intros. induction tl; [done |]. cbn in *. by destruct tl. -Qed. +Qed.*) Lemma unroll_last {S} : forall (random a : S) (l : list S), List.last (a :: l) random = List.last l a. @@ -108,14 +108,14 @@ Proof. by destruct l; [|inversion Herr; apply unroll_last]. Qed. -Lemma incl_empty : forall A (l : list A), +(*Lemma incl_empty : forall A (l : list A), incl l nil -> l = nil. Proof. intros A [] H; [done |]. by destruct (H a); left. -Qed. +Qed.*) -Lemma incl_singleton {A} : forall (l : list A) (a : A), +(*Lemma incl_singleton {A} : forall (l : list A) (a : A), incl l [a] -> forall b, In b l -> b = a. Proof. @@ -124,7 +124,7 @@ Proof. - apply IHl; [| done]. apply incl_tran with (a0 :: l); [| done]. apply incl_tl. apply incl_refl. -Qed. +Qed.*) Lemma Exists_first {A : Type} @@ -205,19 +205,19 @@ Proof. by split; intros Hincl x Hx; apply in_correct; apply Hincl. Qed. -Definition incl_correct `{EqDecision A} +(*Definition incl_correct `{EqDecision A} (l1 l2 : list A) : incl l1 l2 <-> inclb l1 l2 = true - := incl_function l1 l2. + := incl_function l1 l2.*) -Lemma map_incl {A B} (f : B -> A) : forall s s', +(*Lemma map_incl {A B} (f : B -> A) : forall s s', incl s s' -> incl (map f s) (map f s'). Proof. intros s s' Hincl fx Hin. apply in_map_iff . apply in_map_iff in Hin as (x & Heq & Hin). eauto. -Qed. +Qed.*) Definition app_cons {A} (a : A) @@ -225,21 +225,21 @@ Definition app_cons {A} : [a] ++ l = a :: l := eq_refl. -Lemma append_nodup_left {A}: +(*Lemma append_nodup_left {A}: forall (l1 l2 : list A), List.NoDup (l1 ++ l2) -> List.NoDup l1. Proof. induction l1; intros. - constructor. - inversion H. apply IHl1 in H3. constructor; [| done]. rewrite in_app_iff in H2. itauto. -Qed. +Qed.*) -Lemma append_nodup_right {A}: +(*Lemma append_nodup_right {A}: forall (l1 l2 : list A), List.NoDup (l1 ++ l2) -> List.NoDup l2. Proof. induction l1; cbn; intros; [done |]. inversion H. auto. -Qed. +Qed.*) Lemma last_is_last {A} : forall (l : list A) (x dummy: A), List.last (l ++ [x]) dummy = x. @@ -267,11 +267,11 @@ Fixpoint is_member {W} `{StrictlyComparable W} (w : W) (l : list W) : bool := end end. -Definition compareb {A} `{StrictlyComparable A} (a1 a2 : A) : bool := +(*Definition compareb {A} `{StrictlyComparable A} (a1 a2 : A) : bool := match compare a1 a2 with | Eq => true | _ => false - end. + end.*) Lemma is_member_correct {W} `{StrictlyComparable W} : forall l (w : W), is_member w l = true <-> In w l. @@ -285,21 +285,21 @@ Proof. + rewrite <- compare_eq. rewrite <- compare_asymmetric in Hcmp. itauto congruence. Qed. -Lemma is_member_correct' {W} `{StrictlyComparable W} +(*Lemma is_member_correct' {W} `{StrictlyComparable W} : forall l (w : W), is_member w l = false <-> ~ In w l. Proof. intros. apply mirror_reflect. intros; apply is_member_correct. -Qed. +Qed.*) -Lemma In_app_comm {X} : forall l1 l2 (x : X), In x (l1 ++ l2) <-> In x (l2 ++ l1). +(*Lemma In_app_comm {X} : forall l1 l2 (x : X), In x (l1 ++ l2) <-> In x (l2 ++ l1). Proof. intros l1 l2 x; split; intro H_in; apply in_or_app; apply in_app_or in H_in; destruct H_in as [cat | dog]; itauto. -Qed. +Qed.*) Lemma nth_error_last {A : Type} @@ -354,7 +354,7 @@ Fixpoint list_prefix | S n, a :: l => a :: list_prefix l n end. -Lemma list_prefix_split +(*Lemma list_prefix_split {A : Type} (l left right: list A) (left_len : nat) @@ -385,7 +385,7 @@ Proof. rewrite Hsplit. simpl. by rewrite IHleft_len. -Qed. +Qed.*) Lemma list_prefix_map {A B : Type} @@ -528,7 +528,7 @@ Proof. by apply dsig_eq. Qed. -Lemma list_annotate_eq +(*Lemma list_annotate_eq {A : Type} (P : A -> Prop) {Pdec : forall a, Decision (P a)} @@ -545,7 +545,7 @@ Proof. inversion H. apply IHl1 in H2. by subst. -Qed. +Qed.*) Lemma list_annotate_unroll {A : Type} @@ -557,7 +557,7 @@ Lemma list_annotate_unroll : list_annotate P (a :: l) Hs = dexist a (Forall_hd Hs) :: list_annotate P l (Forall_tl Hs). Proof. done. Qed. -Lemma list_annotate_app +(*Lemma list_annotate_app {A : Type} (P : A -> Prop) {Pdec : forall a, Decision (P a)} @@ -569,9 +569,9 @@ Proof. simpl. f_equal. - by apply dsig_eq. - rewrite IHl1. f_equal; apply list_annotate_pi. -Qed. +Qed.*) -Lemma nth_error_list_annotate +(*Lemma nth_error_list_annotate {A : Type} (P : A -> Prop) (Pdec : forall a, Decision (P a)) @@ -589,7 +589,7 @@ Proof. by rewrite list_annotate_unroll. - by exists None. - rewrite list_annotate_unroll; eauto. -Qed. +Qed.*) Fixpoint nth_error_filter_index {A} P `{∀ (x:A), Decision (P x)} @@ -608,7 +608,7 @@ Fixpoint nth_error_filter_index option_map S (nth_error_filter_index P l n) end. -Lemma nth_error_filter_index_le +(*Lemma nth_error_filter_index_le {A} P `{∀ (x:A), Decision (P x)} (l : list A) (n1 n2 : nat) @@ -652,7 +652,7 @@ Proof. ; subst; clear Hin2. specialize (IHl n0 eq_refl n3 eq_refl). lia. -Qed. +Qed.*) Fixpoint Forall_filter {A : Type} @@ -818,7 +818,7 @@ Proof. - by rewrite unroll_last, unroll_last. Qed. -Lemma list_suffix_last_default +(*Lemma list_suffix_last_default {A : Type} (l : list A) (i : nat) @@ -828,9 +828,9 @@ Lemma list_suffix_last_default Proof. revert l Hlast. induction i; intros [|a l] Hlast; try done. apply IHi. by inversion Hlast. -Qed. +Qed.*) -Lemma list_segment_nth +(*Lemma list_segment_nth {A : Type} (l : list A) (n1 n2 : nat) @@ -843,9 +843,9 @@ Proof. unfold list_segment. rewrite list_suffix_nth; [| done]. by apply list_prefix_nth. -Qed. +Qed.*) -Lemma list_segment_app +(*Lemma list_segment_app {A : Type} (l : list A) (n1 n2 n3 : nat) @@ -865,9 +865,9 @@ Proof. rewrite <- Hl2 in Hl1. rewrite <- app_assoc in Hl1. by apply app_inv_head in Hl1. -Qed. +Qed.*) -Lemma list_segment_singleton +(*Lemma list_segment_singleton {A : Type} (l : list A) (n : nat) @@ -893,9 +893,9 @@ Proof. destruct x; inversion Hlength. destruct x; inversion H0. by simpl in Hlast1; subst. -Qed. +Qed.*) -Lemma nth_error_map +(*Lemma nth_error_map {A B : Type} (f : A -> B) (l : list A) @@ -903,7 +903,7 @@ Lemma nth_error_map : nth_error (List.map f l) n = option_map f (nth_error l n). Proof. revert n. induction l; intros [| n]; firstorder. -Qed. +Qed.*) Lemma exists_finite `{finite.Finite index} @@ -1019,17 +1019,17 @@ Qed. Definition cat_option {A : Type} : list (option A) -> list A := @map_option (option A) A id. -Example cat_option1 : cat_option [Some 1; Some 5; None; Some 6; None] = [1; 5; 6]. -Proof. itauto. Qed. +(*Example cat_option1 : cat_option [Some 1; Some 5; None; Some 6; None] = [1; 5; 6]. +Proof. itauto. Qed.*) -Lemma cat_option_length +(*Lemma cat_option_length {A : Type} (l : list (option A)) (Hfl : Forall (fun a => a <> None) l) : length (cat_option l) = length l. Proof. apply map_option_length; itauto. -Qed. +Qed.*) Lemma cat_option_length_le {A : Type} @@ -1042,7 +1042,7 @@ Proof. destruct (id a) eqn : eq_id; simpl in *; subst a; simpl; lia. Qed. -Lemma cat_option_app +(*Lemma cat_option_app {A : Type} (l1 l2 : list (option A)) : cat_option (l1 ++ l2) = cat_option l1 ++ cat_option l2. @@ -1050,9 +1050,9 @@ Proof. induction l1. - simpl in *. itauto. - by destruct a; cbn in *; rewrite IHl1. -Qed. +Qed.*) -Lemma cat_option_nth +(*Lemma cat_option_nth {A : Type} (l : list (option A)) (Hfl : Forall (fun a => a <> None) l) @@ -1085,10 +1085,10 @@ Proof. apply IHl1. intro n. apply (Hnth (S n)). -Qed. +Qed.*) (* TODO remove (we have Exists_first) *) -Lemma exists_first +(*Lemma exists_first {A : Type} (l : list A) (P : A -> Prop) @@ -1110,9 +1110,9 @@ Proof. destruct IHl as [prefix [suffix [first [Hfirst [Heq Hprefix]]]]]. exists (a :: prefix), suffix, first. split_and!; subst; [done | done |]. by inversion 1; subst. -Qed. +Qed.*) -Lemma in_fast +(*Lemma in_fast {A : Type} (l : list A) (a : A) @@ -1122,7 +1122,7 @@ Lemma in_fast In a l. Proof. by destruct Hin. -Qed. +Qed.*) Fixpoint one_element_decompositions {A : Type} @@ -1192,7 +1192,7 @@ Definition two_element_decompositions ) (one_element_decompositions l). -Lemma in_two_element_decompositions_iff +(*Lemma in_two_element_decompositions_iff {A : Type} (l : list A) (pre mid suf : list A) @@ -1216,9 +1216,9 @@ Proof. split; [done |]. apply in_map_iff. exists (mid, y, suf). by rewrite in_one_element_decompositions_iff. -Qed. +Qed.*) -Lemma order_decompositions +(*Lemma order_decompositions {A : Type} (pre1 suf1 pre2 suf2 : list A) (Heq : pre1 ++ suf1 = pre2 ++ suf2) @@ -1236,7 +1236,7 @@ Proof. inversion Heq; subst a2; clear Heq. destruct (IHl pre1 suf1 pre2 suf2 H1 H2) as [Heq | [[suf1' Hgt] | [suf2' Hlt]]]; subst; eauto. -Qed. +Qed.*) Lemma list_max_exists (l : list nat) @@ -1253,7 +1253,7 @@ Proof. by rewrite H; left. Qed. -Lemma list_max_exists2 +(*Lemma list_max_exists2 (l : list nat) (Hne : l <> []) : In (list_max l) l. @@ -1268,7 +1268,7 @@ Proof. simpl. lia. - specialize (list_max_exists l) as Hmax. spec Hmax. lia. rewrite <- eq_max. itauto. -Qed. +Qed.*) (* Returns all values which occur with maximum frequency in the given list. Note that these values are returned with their original multiplicity. *) @@ -1279,8 +1279,8 @@ Definition mode let mode_value := list_max (List.map (count_occ decide_eq l) l) in filter (fun a => (count_occ decide_eq l a) = mode_value) l. -Example mode1 : mode [1; 1; 2; 3; 3] = [1; 1; 3; 3]. -Proof. itauto. Qed. +(*Example mode1 : mode [1; 1; 2; 3; 3] = [1; 1; 3; 3]. +Proof. itauto. Qed.*) (* Computes the list suff which satisfies <> or reports that no such list exists. *) @@ -1301,10 +1301,10 @@ Fixpoint complete_prefix end end. -Example complete_prefix_some : complete_prefix [1;2;3;4] [1;2] = Some [3;4]. -Proof. itauto. Qed. -Example complete_prefix_none : complete_prefix [1;2;3;4] [1;3] = None. -Proof. itauto. Qed. +(*Example complete_prefix_some : complete_prefix [1;2;3;4] [1;2] = Some [3;4]. +Proof. itauto. Qed.*) +(*Example complete_prefix_none : complete_prefix [1;2;3;4] [1;3] = None. +Proof. itauto. Qed.*) Lemma complete_prefix_empty `{EqDecision A} @@ -1365,8 +1365,8 @@ Definition complete_suffix | Some ls => Some (rev ls) end. -Example complete_suffix_some : complete_suffix [1;2;3;4] [3;4] = Some [1;2]. -Proof. itauto. Qed. +(*Example complete_suffix_some : complete_suffix [1;2;3;4] [3;4] = Some [1;2]. +Proof. itauto. Qed.*) Lemma complete_suffix_correct `{EqDecision A} @@ -1422,12 +1422,12 @@ Definition list_sum_project_right := map_option sum_project_right x. -Lemma fold_right_andb_false l: +(*Lemma fold_right_andb_false l: fold_right andb false l = false. Proof. induction l; [done |]. simpl. rewrite IHl. apply andb_false_r. -Qed. +Qed.*) Definition Listing_finite_transparent `{EqDecision A} {l : list A} (finite_l : Listing l) : finite.Finite A. Proof. @@ -1521,19 +1521,19 @@ Inductive ForAllSuffix : list A -> Prop := | SNil : P [] -> ForAllSuffix [] | SHereAndFurther : forall a l, P (a :: l) -> ForAllSuffix l -> ForAllSuffix (a :: l). -Lemma fsHere : forall l, ForAllSuffix l -> P l. -Proof. by inversion 1. Qed. +(*Lemma fsHere : forall l, ForAllSuffix l -> P l. +Proof. by inversion 1. Qed.*) Lemma fsFurther : forall a l, ForAllSuffix (a :: l) -> ForAllSuffix l. Proof. by inversion 1. Qed. -Lemma ForAll_list_suffix : forall m x, ForAllSuffix x -> ForAllSuffix (list_suffix x m). +(*Lemma ForAll_list_suffix : forall m x, ForAllSuffix x -> ForAllSuffix (list_suffix x m). Proof. induction m; simpl; intros [] **. 1-3: done. by apply fsFurther in H; apply IHm. -Qed. +Qed.*) -Lemma ForAllSuffix_induction +(*Lemma ForAllSuffix_induction (Inv : list A -> Prop) (InvThenP : forall l, Inv l -> P l) (InvIsStable : forall a l, Inv (a :: l) -> Inv l) @@ -1544,30 +1544,30 @@ Proof. - constructor. + by apply InvThenP. + by eapply IHl, InvIsStable. -Qed. +Qed.*) End suffix_quantifiers. -Lemma ForAllSuffix_subsumption [A : Type] (P Q : list A -> Prop) +(*Lemma ForAllSuffix_subsumption [A : Type] (P Q : list A -> Prop) (HPQ : forall l, P l -> Q l) : forall l, ForAllSuffix P l -> ForAllSuffix Q l. Proof. induction 1; constructor; auto. -Qed. +Qed.*) Definition ForAllSuffix1 [A : Type] (P : A -> Prop) : list A -> Prop := ForAllSuffix (fun l => match l with | [] => True | a :: _ => P a end). -Lemma ForAllSuffix1_Forall [A : Type] (P : A -> Prop) +(*Lemma ForAllSuffix1_Forall [A : Type] (P : A -> Prop) : forall l, ForAllSuffix1 P l <-> Forall P l. Proof. split; induction 1; constructor; auto. -Qed. +Qed.*) Definition ExistsSuffix1 [A : Type] (P : A -> Prop) : list A -> Prop := ExistsSuffix (fun l => match l with | [] => False | a :: _ => P a end). -Lemma ExistsSuffix1_Exists [A : Type] (P : A -> Prop) +(*Lemma ExistsSuffix1_Exists [A : Type] (P : A -> Prop) : forall l, ExistsSuffix1 P l <-> Exists P l. Proof. split; induction 1. @@ -1575,7 +1575,7 @@ Proof. - by right. - by left. - by right. -Qed. +Qed.*) Definition ForAllSuffix2 [A : Type] (R : A -> A -> Prop) : list A -> Prop := ForAllSuffix (fun l => match l with | a :: b :: _ => R a b | _ => True end). @@ -1607,13 +1607,12 @@ Proof. - apply IHl. by eapply fsFurther2_transitive. Qed. - -Lemma list_subseteq_tran : forall (A : Type) (l m n : list A), +(*Lemma list_subseteq_tran : forall (A : Type) (l m n : list A), l ⊆ m → m ⊆ n → l ⊆ n. Proof. intros A l m n Hlm Hmn x y. by apply Hmn, Hlm. -Qed. +Qed.*) #[global] Instance list_subseteq_dec `{EqDecision A} : RelDecision (@subseteq (list A) _). Proof. @@ -1702,12 +1701,12 @@ Proof. Qed. (** If <> is zero, then the result of [lastn] is [[]]. *) -Lemma lastn_0 : +(*Lemma lastn_0 : forall {A : Type} (l : list A), lastn 0 l = []. Proof. by intros A l; unfold lastn; rewrite take_0. -Qed. +Qed.*) (** If <> is greater than the length of the list, [lastn] returns the whole list. *) Lemma lastn_ge : @@ -1755,7 +1754,7 @@ Qed. (** If <> is less than (or equal to) <>, then <> is shorter than <> and therefore is its suffix. *) -Lemma suffix_lastn : +(*Lemma suffix_lastn : forall {A : Type} (l : list A) (n1 n2 : nat), n1 <= n2 -> suffix (lastn n1 l) (lastn n2 l). Proof. @@ -1765,24 +1764,24 @@ Proof. exists (take (n2 - n1) (drop n1 (rev l))). rewrite take_take_drop. by f_equal; lia. -Qed. +Qed.*) (** The length of <> is the smaller of <> and the length of <>. *) -Lemma length_lastn : +(*Lemma length_lastn : forall {A : Type} (n : nat) (l : list A), length (lastn n l) = min n (length l). Proof. intros A n l. unfold lastn. by rewrite rev_length, take_length, rev_length. -Qed. +Qed.*) -Program Definition not_null_element +(*Program Definition not_null_element `{EqDecision A} [l : list A] (Hl : l <> []) : dsig (fun i => i ∈ l) := dexist (is_Some_proj (proj2 (head_is_Some l) Hl)) _. Next Obligation. by intros A ? [| h t] ?; [| left]. -Qed. +Qed.*) Program Definition element_of_subseteq `{EqDecision A} [l1 l2 : list A] (Hsub : l1 ⊆ l2) @@ -1792,7 +1791,7 @@ Next Obligation. by intros; cbn; destruct_dec_sig di i Hi Heq; subst; apply Hsub. Qed. -Definition element_of_filter +(*Definition element_of_filter `{EqDecision A} [P : A -> Prop] `{∀ x, Decision (P x)} [l : list A] : dsig (fun i => i ∈ filter P l) -> dsig (fun i => i ∈ l) := - element_of_subseteq (list_filter_subseteq P l). + element_of_subseteq (list_filter_subseteq P l).*) From 0f24ddafa6eb747f2859723c356e0ca6d951ad4f Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 15:44:35 +0300 Subject: [PATCH 05/18] Fixing the build error of the last commit --- theories/VLSM/Lib/ListExtras.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v index b9494eb1..44536cb8 100644 --- a/theories/VLSM/Lib/ListExtras.v +++ b/theories/VLSM/Lib/ListExtras.v @@ -1067,7 +1067,7 @@ Proof. unfold id in *. apply H. all : itauto. -Qed. +Qed.*) Lemma nth_error_eq {A : Type} @@ -1085,7 +1085,7 @@ Proof. apply IHl1. intro n. apply (Hnth (S n)). -Qed.*) +Qed. (* TODO remove (we have Exists_first) *) (*Lemma exists_first From d908110acb54ef0f86a1417c21cc74af48a7de00 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 15:58:30 +0300 Subject: [PATCH 06/18] Removing lemmas from ListSetExtras.v --- theories/VLSM/Lib/ListSetExtras.v | 76 +++++++++++++++---------------- 1 file changed, 38 insertions(+), 38 deletions(-) diff --git a/theories/VLSM/Lib/ListSetExtras.v b/theories/VLSM/Lib/ListSetExtras.v index a93be976..1d41b907 100644 --- a/theories/VLSM/Lib/ListSetExtras.v +++ b/theories/VLSM/Lib/ListSetExtras.v @@ -27,12 +27,12 @@ Proof. by intros s1 s2 []. Qed. -Lemma set_eq_proj2 {A} : forall (s1 s2 : set A), +(*Lemma set_eq_proj2 {A} : forall (s1 s2 : set A), set_eq s1 s2 -> s2 ⊆ s1. Proof. by intros s1 s2 []. -Qed. +Qed.*) Lemma set_eq_refl {A} : forall (s : list A), set_eq s s. Proof. @@ -76,7 +76,7 @@ Proof. firstorder. Qed. -Lemma set_eq_Forall +(*Lemma set_eq_Forall {A : Type} (s1 s2 : set A) (H12 : set_eq s1 s2) @@ -84,7 +84,7 @@ Lemma set_eq_Forall : Forall P s1 <-> Forall P s2. Proof. rewrite !Forall_forall. firstorder. -Qed. +Qed.*) Lemma set_union_comm `{EqDecision A} : forall (s1 s2 : list A), set_eq (set_union s1 s2) (set_union s2 s1). @@ -92,14 +92,14 @@ Proof. intros s1 s2; split; intro x; rewrite !set_union_iff; itauto. Qed. -Lemma set_union_empty `{EqDecision A} : forall (s1 s2 : list A), +(*Lemma set_union_empty `{EqDecision A} : forall (s1 s2 : list A), set_union s1 s2 = [] -> s1 = [] /\ s2 = []. Proof. intros. destruct s2; [done |]. by cbn in H; apply set_add_not_empty in H. -Qed. +Qed.*) Lemma set_union_nodup_left `{EqDecision A} (l l' : set A) : NoDup l -> NoDup (set_union l l'). @@ -169,7 +169,7 @@ Proof. + right. apply IHss. by exists x. Qed. -Lemma set_union_iterated_subseteq +(*Lemma set_union_iterated_subseteq `{EqDecision A} (ss ss': list (set A)) (Hincl : ss ⊆ ss') : @@ -185,9 +185,9 @@ Proof. unfold incl in Hincl. split; [| done]. by apply Hincl. -Qed. +Qed.*) -Lemma set_union_empty_left `{EqDecision A} : forall (s : list A), +(*Lemma set_union_empty_left `{EqDecision A} : forall (s : list A), NoDup s -> set_eq (set_union [] s) s. Proof. intros. split; intros x Hin. @@ -195,7 +195,7 @@ Proof. + inversion H0. + done. - by apply set_union_intro; right. -Qed. +Qed.*) Lemma map_list_subseteq {A B} : forall (f : B -> A) (s s' : list B), s ⊆ s' -> (map f s) ⊆ (map f s'). @@ -278,15 +278,15 @@ Proof. by split; destruct H; apply set_map_subseteq. Qed. -Lemma set_map_singleton {A B} `{EqDecision A} (f : B -> A) : forall s a, +(*Lemma set_map_singleton {A B} `{EqDecision A} (f : B -> A) : forall s a, set_map f s = [a] -> forall b, b ∈ s -> f b = a. Proof. intros. apply (set_map_elem_of f) in H0. rewrite H in H0. apply elem_of_cons in H0. destruct H0; [done | inversion H0]. -Qed. +Qed.*) -Lemma filter_set_add `{StrictlyComparable X} P +(*Lemma filter_set_add `{StrictlyComparable X} P `{∀ (x:X), Decision (P x)} : forall (l:list X) x, ~ P x -> filter P l = filter P (set_add x l). @@ -295,7 +295,7 @@ Proof. - by rewrite decide_False. - destruct (decide (x = hd)); cbn; [done |]. by destruct (decide (P hd)); rewrite <- (IHl). -Qed. +Qed.*) Lemma set_add_ignore `{StrictlyComparable X} : forall (l : list X) (x : X), @@ -307,16 +307,16 @@ Proof. - rewrite IHl; [| done]. by destruct (decide (x = hd)). Qed. -Lemma set_add_new `{EqDecision A}: +(*Lemma set_add_new `{EqDecision A}: forall (x:A) l, ~x ∈ l -> set_add x l = l++[x]. Proof. induction l; cbn; [done |]; intros H_not_in. rewrite decide_False; cycle 1. - by intros ->; apply H_not_in; left. - rewrite elem_of_cons in H_not_in. rewrite IHl; itauto. -Qed. +Qed.*) -Lemma set_remove_not_elem_of `{EqDecision A} : forall x (s : list A), +(*Lemma set_remove_not_elem_of `{EqDecision A} : forall x (s : list A), ~ x ∈ s -> set_remove x s = s. Proof. @@ -324,7 +324,7 @@ Proof. rewrite decide_False; cycle 1. + by intros ->; contradict H; left. + rewrite IHs; [done |]. rewrite elem_of_cons in H. itauto. -Qed. +Qed.*) Lemma set_remove_elim `{EqDecision A} : forall x (s : list A), NoDup s -> ~ x ∈ (set_remove x s). @@ -338,7 +338,7 @@ Proof. by intros x y s ->; cbn; rewrite decide_True. Qed. -Lemma set_remove_nodup_1 `{EqDecision A} : forall x (s : list A), +(*Lemma set_remove_nodup_1 `{EqDecision A} : forall x (s : list A), NoDup (set_remove x s) -> ~ x ∈ (set_remove x s) -> NoDup s. @@ -356,7 +356,7 @@ Proof. * apply IHs; [done |]. intro Hx. by contradict H0; right. -Qed. +Qed.*) Lemma set_remove_elem_of_iff `{EqDecision A} : forall x y (s : list A), NoDup s -> @@ -409,7 +409,7 @@ Proof. split; intros a Hin; rewrite set_remove_iff in *; itauto. Qed. -Lemma subseteq_remove_union `{EqDecision A} : forall x (s1 s2 : list A), +(*Lemma subseteq_remove_union `{EqDecision A} : forall x (s1 s2 : list A), NoDup s1 -> NoDup s2 -> (set_remove x (set_union s1 s2)) ⊆ @@ -419,7 +419,7 @@ Proof. - apply set_union_intro. destruct Hin. apply set_union_elim in H1. rewrite set_remove_iff; itauto. - by apply set_union_nodup. -Qed. +Qed.*) Lemma set_eq_remove_union_elem_of `{EqDecision A} : forall x (s1 s2 : list A), NoDup s1 -> @@ -463,7 +463,7 @@ Qed. for the second argument. *) (* TODO(palmskog): consider submitting a PR to Coq's stdlib. *) -Lemma set_diff_nodup' `{EqDecision A} (l l' : list A) +(*Lemma set_diff_nodup' `{EqDecision A} (l l' : list A) : NoDup l -> NoDup (set_diff l l'). Proof. induction 1 as [|x l H H' IH]; simpl. @@ -471,7 +471,7 @@ induction 1 as [|x l H H' IH]; simpl. - case_decide. + by apply IH. + by apply set_add_nodup, IH. -Qed. +Qed.*) Lemma diff_app_nodup `{EqDecision A} : forall (s1 s2 : list A), NoDup s1 -> @@ -497,7 +497,7 @@ Proof. rewrite Heq, IHlv; itauto. Qed. -Lemma set_union_iterated_empty `{EqDecision A} : +(*Lemma set_union_iterated_empty `{EqDecision A} : forall ss : list (set A), (forall s : list A, s ∈ ss -> s = []) -> fold_right set_union [] ss = []. Proof. @@ -505,7 +505,7 @@ Proof. rewrite IHss; cycle 1. - by intros s Hel; apply H; right. - by cbn; apply H; left. -Qed. +Qed.*) (** For each element X of l1, exactly one occurrence of X is removed from l2. If no such occurrence exists, nothing happens. *) @@ -513,11 +513,11 @@ Qed. Definition set_remove_list `{EqDecision A} (l1 l2 : list A) : list A := fold_right set_remove l2 l1. -Example set_remove_list1 : set_remove_list [3;1;3] [1;1;2;3;3;3;3] = [1;2;3;3]. -Proof. done. Qed. +(*Example set_remove_list1 : set_remove_list [3;1;3] [1;1;2;3;3;3;3] = [1;2;3;3]. +Proof. done. Qed.*) -Example set_remove_list2 : set_remove_list [4] [1;2;3] = [1;2;3]. -Proof. done. Qed. +(*Example set_remove_list2 : set_remove_list [4] [1;2;3] = [1;2;3]. +Proof. done. Qed.*) Lemma set_remove_list_1 `{EqDecision A} @@ -533,7 +533,7 @@ Proof. by apply set_remove_1, IHl1 in Hin. Qed. -Lemma set_prod_nodup `(s1: set A) `(s2: set B): +(*Lemma set_prod_nodup `(s1: set A) `(s2: set B): NoDup s1 -> NoDup s2 -> NoDup (set_prod s1 s2). @@ -551,7 +551,7 @@ Proof. * intros [a b]. rewrite elem_of_list_prod, elem_of_list_fmap. intros [Ha _] [_ [[= Hax _] _]]. congruence. -Qed. +Qed.*) (** An alternative to [set_diff]. Unlike [set_diff], the result may contain @@ -569,7 +569,7 @@ Definition set_diff_filter `{EqDecision A} (l r : list A) := The characteristic membership property, parallel to [set_diff_iff]. *) -Lemma set_diff_filter_iff `{EqDecision A} (a:A) l r: +(*Lemma set_diff_filter_iff `{EqDecision A} (a:A) l r: a ∈ (set_diff_filter l r) <-> (a ∈ l /\ ~a ∈ r). Proof. induction l;simpl. @@ -582,14 +582,14 @@ Proof. split; itauto congruence. * rewrite elem_of_cons. split;itauto congruence. -Qed. +Qed.*) -Lemma set_diff_filter_nodup `{EqDecision A} (l r:list A): +(*Lemma set_diff_filter_nodup `{EqDecision A} (l r:list A): NoDup l -> NoDup (set_diff_filter l r). Proof. intros H. by apply NoDup_filter. -Qed. +Qed.*) (** Prove that subtracting a superset cannot produce @@ -682,7 +682,7 @@ Add Parametric Morphism A : (@elem_of_list A) with signature @eq A ==> @list_subseteq A ==> Basics.impl as set_elem_of_subseteq. Proof. firstorder. Qed. -Lemma set_union_iterated_preserves_prop +(*Lemma set_union_iterated_preserves_prop `{EqDecision A} (ss : list (set A)) (P : A -> Prop) @@ -694,7 +694,7 @@ Proof. destruct H as [s [Hins Hina]]. apply Hp with (s := s). itauto. -Qed. +Qed.*) Lemma filter_set_eq {X} P Q `{∀ (x:X), Decision (P x)} `{∀ (x:X), Decision (Q x)} From d12e69750184eefad2d9e04bf080b107d6454d17 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 18:01:46 +0300 Subject: [PATCH 07/18] Removing lemmas from RealsExtras.v --- theories/VLSM/Lib/RealsExtras.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/theories/VLSM/Lib/RealsExtras.v b/theories/VLSM/Lib/RealsExtras.v index 75ef3b0e..c16ebdb0 100644 --- a/theories/VLSM/Lib/RealsExtras.v +++ b/theories/VLSM/Lib/RealsExtras.v @@ -4,20 +4,20 @@ From stdpp Require Import prelude. (** * Real number utility lemmas *) (** This lemma is needed in fault_weight_state_backwards **) -Lemma Rplusminus_assoc : forall r1 r2 r3, +(*Lemma Rplusminus_assoc : forall r1 r2 r3, (r1 + r2 - r3)%R = (r1 + (r2 - r3))%R. Proof. intros. unfold Rminus. apply Rplus_assoc. -Qed. +Qed.*) (** This lemma is needed in fault_weight_state_sorted_subset **) -Lemma Rplusminus_assoc_r : forall r1 r2 r3, +(*Lemma Rplusminus_assoc_r : forall r1 r2 r3, (r1 - r2 + r3)%R = (r1 + (- r2 + r3))%R. Proof. intros. unfold Rminus. apply Rplus_assoc. -Qed. +Qed.*) (** This lemma is needed in fault_weight_state_sorted_subset **) Lemma Rplus_opp_l : forall r, (Ropp r + r)%R = 0%R. @@ -28,7 +28,7 @@ Proof. Qed. (** This lemma is needed in fault_weight_state_sorted_subset **) -Lemma Rplus_ge_reg_neg_r : forall r1 r2 r3, +(*Lemma Rplus_ge_reg_neg_r : forall r1 r2 r3, (r2 <= 0)%R -> (r3 <= r1 + r2)%R -> (r3 <= r1)%R. Proof. intros. @@ -36,26 +36,26 @@ Proof. apply Rle_ge in H. apply Rle_ge in H0. apply (Rplus_ge_reg_neg_r r1 r2 r3 H H0). -Qed. +Qed.*) (** This lemma is needed in fault_weight_state_sorted_subset **) -Lemma Rminus_lt_r : forall r1 r2, +(*Lemma Rminus_lt_r : forall r1 r2, (0 <= r2)%R -> (r1 - r2 <= r1)%R. Proof. intros. rewrite <- Rplus_0_r. unfold Rminus. by apply Rplus_le_compat_l, Rge_le, Ropp_0_le_ge_contravar. -Qed. +Qed.*) -Lemma Rminus_lt_r_strict : forall r1 r2, +(*Lemma Rminus_lt_r_strict : forall r1 r2, (0 < r2)%R -> (r1 - r2 <= r1)%R. Proof. intros. rewrite <- Rplus_0_r. unfold Rminus. by apply Rplus_le_compat_l, Rge_le, Ropp_0_le_ge_contravar, Rlt_le. -Qed. +Qed.*) Lemma Rtotal_le_gt : forall x y, (x <= y)%R \/ (x > y)%R. From 7160f699109edd54d14abf984ca3c314410f36de Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 18:08:33 +0300 Subject: [PATCH 08/18] Removing lemmas from SortedLists.v --- theories/VLSM/Lib/SortedLists.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/VLSM/Lib/SortedLists.v b/theories/VLSM/Lib/SortedLists.v index 0e5b435e..7b3d58d4 100644 --- a/theories/VLSM/Lib/SortedLists.v +++ b/theories/VLSM/Lib/SortedLists.v @@ -58,13 +58,13 @@ Fixpoint add_in_sorted_list_fn {A} (compare : A -> A -> comparison) (x : A) (l : end end. -Lemma add_in_sorted_list_no_empty {A} (compare : A -> A -> comparison) : forall msg sigma, +(*Lemma add_in_sorted_list_no_empty {A} (compare : A -> A -> comparison) : forall msg sigma, add_in_sorted_list_fn compare msg sigma <> []. Proof. unfold not. intros. destruct sigma; simpl in H. - inversion H. - destruct (compare msg a); inversion H. -Qed. +Qed.*) Lemma add_in_sorted_list_in {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} : forall msg msg' sigma, msg' ∈ (add_in_sorted_list_fn compare msg sigma) -> @@ -176,7 +176,7 @@ Proof. - do 2 inversion 1; subst; firstorder. Qed. -Lemma add_in_sorted_list_existing {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} : forall msg sigma, +(*Lemma add_in_sorted_list_existing {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} : forall msg sigma, LocallySorted (compare_lt compare) sigma -> msg ∈ sigma -> add_in_sorted_list_fn compare msg sigma = sigma. @@ -192,7 +192,7 @@ Proof. apply (@LocallySorted_elem_of_lt _ _ compare_lt_strict_order msg a sigma H0) in Hin. unfold compare_lt in Hin. apply compare_asymmetric in Hin. rewrite Hin in Hcmp. inversion Hcmp. -Qed. +Qed.*) Lemma set_eq_first_equal {A} {lt : relation A} `{StrictOrder A lt} : forall x1 x2 s1 s2, @@ -330,7 +330,7 @@ Proof. apply elem_of_app; right; left. Qed. -Lemma lsorted_pair_wise_unordered +(*Lemma lsorted_pair_wise_unordered {A : Type} (l : list A) (R : A -> A -> Prop) @@ -369,4 +369,4 @@ Proof. rewrite Hconcat2 in Hconcat1. specialize (lsorted_pairwise_ordered l R Hsorted Htransitive x y pref1 pref2 suf2 Hconcat1). by intros; right; left. -Qed. +Qed.*) From 1e88e8daf40cba82a5355399da7f9f8bdc3c4967 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 18:15:37 +0300 Subject: [PATCH 09/18] Removing lemmas from SsrExport.v --- theories/VLSM/Lib/SsrExport.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/VLSM/Lib/SsrExport.v b/theories/VLSM/Lib/SsrExport.v index 40fa561a..d81fa57e 100644 --- a/theories/VLSM/Lib/SsrExport.v +++ b/theories/VLSM/Lib/SsrExport.v @@ -4,4 +4,4 @@ From Coq Require Export ssreflect. #[export] Set SsrOldRewriteGoalsOrder. #[export] Set Asymmetric Patterns. #[export] Set Bullet Behavior "None". -Definition iYC2 := True. +(*Definition iYC2 := True.*) From f1da8c357ec60b5d3b47d2a6e36b253d3a249f81 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 18:44:40 +0300 Subject: [PATCH 10/18] Removing lemmas from StdppExtras.v --- theories/VLSM/Lib/StdppExtras.v | 36 ++++++++++++++++----------------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v index b1a62155..77857a8b 100644 --- a/theories/VLSM/Lib/StdppExtras.v +++ b/theories/VLSM/Lib/StdppExtras.v @@ -145,7 +145,7 @@ Proof. by rewrite existsb_Exists, <- Forall_Exists_neg, Forall_forall. Qed. -Lemma existsb_first +(*Lemma existsb_first {A : Type} (l : list A) (f : A -> bool) @@ -162,7 +162,7 @@ Proof. apply Exists_first. - typeclasses eauto. - by apply existsb_Exists. -Qed. +Qed.*) (* Returns all elements X of l such that X does not compare less than any other element w.r.t to the precedes relation *) @@ -172,11 +172,11 @@ Definition maximal_elements_list : list A := filter (fun a => Forall (fun b => (~ precedes a b)) l) l. -Example maximal_elements_list1: maximal_elements_list Nat.lt [1; 4; 2; 4] = [4;4]. -Proof. itauto. Qed. +(*Example maximal_elements_list1: maximal_elements_list Nat.lt [1; 4; 2; 4] = [4;4]. +Proof. itauto. Qed.*) -Example maximal_elements_list2 : maximal_elements_list Nat.le [1; 4; 2; 4] = []. -Proof. itauto. Qed. +(*Example maximal_elements_list2 : maximal_elements_list Nat.le [1; 4; 2; 4] = []. +Proof. itauto. Qed.*) (** Returns all elements <> of a set <> such that <> does not compare less @@ -229,7 +229,7 @@ Proof. destruct (decide (P a)); destruct (decide (Q a)); itauto. Qed. -Lemma NoDup_elem_of_remove A (l l' : list A) a : +(*Lemma NoDup_elem_of_remove A (l l' : list A) a : NoDup (l ++ a :: l') -> NoDup (l ++ l') /\ a ∉ (l ++ l'). Proof. intros Hnda. @@ -240,17 +240,17 @@ Proof. destruct Hnda as [Ha' Hnd']; split. - by apply NoDup_app; firstorder. - by rewrite elem_of_app; firstorder. -Qed. +Qed.*) -Lemma list_lookup_lt [A] (is : list A) : +(*Lemma list_lookup_lt [A] (is : list A) : forall i, is_Some (is !! i) -> forall j, j < i -> is_Some (is !! j). Proof. intros; apply lookup_lt_is_Some. by etransitivity; [| apply lookup_lt_is_Some]. -Qed. +Qed.*) -Lemma list_suffix_lookup +(*Lemma list_suffix_lookup {A : Type} (s : list A) (n : nat) @@ -259,7 +259,7 @@ Lemma list_suffix_lookup : list_suffix s n !! (i - n) = s !! i. Proof. revert s n Hi; induction i; intros [| a s] [| n] Hi; cbn; try done; [| apply IHi]; lia. -Qed. +Qed.*) Lemma list_difference_singleton_not_in `{EqDecision A} : forall (l : list A) (a : A), a ∉ l -> @@ -285,7 +285,7 @@ Proof. - by inversion 1; subst; [done |]; cbn; spec IHl; [| lia]. Qed. -Lemma longer_subseteq_has_dups `{EqDecision A} : +(*Lemma longer_subseteq_has_dups `{EqDecision A} : forall l1 l2 : list A, l1 ⊆ l2 -> length l1 > length l2 -> exists (i1 i2 : nat) (a : A), i1 ≠ i2 ∧ l1 !! i1 = Some a /\ l1 !! i2 = Some a. Proof. @@ -304,7 +304,7 @@ Proof. + cbn in Hlen12. assert (Ha : a ∈ l2) by (apply Hl12; left). specialize (list_difference_singleton_length_in _ _ Ha) as Hlen'; lia. -Qed. +Qed.*) Lemma ForAllSuffix2_lookup [A : Type] (R : A -> A -> Prop) l : ForAllSuffix2 R l <-> forall n a b, l !! n = Some a -> l !! (S n) = Some b -> R a b. @@ -339,7 +339,7 @@ Qed. (** If the <>-th element of <> is <>, then we can decompose long enough suffixes of <> into <> and a suffix shorter by 1. *) -Lemma lastn_length_cons : +(*Lemma lastn_length_cons : forall {A : Type} (n : nat) (l : list A) (x : A), l !! n = Some x -> lastn (length l - n) l = x :: lastn (length l - S n) l. Proof. @@ -347,7 +347,7 @@ Proof. unfold lastn. rewrite <- rev_length, <- !skipn_rev, rev_involutive. by apply drop_S. -Qed. +Qed.*) Lemma filter_in {A} P `{∀ (x:A), Decision (P x)} x s : In x s -> @@ -718,7 +718,7 @@ Qed. the list into three parts separated by the elements (and this can be done in two ways, depending on the order of the elements). *) -Lemma elem_of_list_split_2 : +(*Lemma elem_of_list_split_2 : forall {A : Type} (l : list A) (x y : A), x ∈ l -> y ∈ l -> x = y \/ exists l1 l2 l3 : list A, @@ -733,4 +733,4 @@ Proof. by rewrite <- app_assoc. - apply elem_of_list_split in Hy as (l21 & l22 & ->). by right; exists l1, l21, l22; left; cbn. -Qed. +Qed.*) From 198a1f4f4ebbd1ee80fc936303c7b58a38d4dab4 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 18:55:12 +0300 Subject: [PATCH 11/18] Removing lemmas from StreamExtras.v --- theories/VLSM/Lib/StreamExtras.v | 64 ++++++++++++++++---------------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/theories/VLSM/Lib/StreamExtras.v b/theories/VLSM/Lib/StreamExtras.v index ba6624e6..35fd28dc 100644 --- a/theories/VLSM/Lib/StreamExtras.v +++ b/theories/VLSM/Lib/StreamExtras.v @@ -49,13 +49,13 @@ Qed. Definition ForAll1 [A : Type] (P : A -> Prop) := ForAll (fun s => P (hd s)). -Lemma ForAll1_subsumption [A:Type] (P Q: A -> Prop) +(*Lemma ForAll1_subsumption [A:Type] (P Q: A -> Prop) (HPQ : forall a, P a -> Q a) : forall s, ForAll1 P s -> ForAll1 Q s. Proof. apply ForAll_subsumption. intro s. apply HPQ. -Qed. +Qed.*) Lemma ForAll1_forall [A : Type] (P : A -> Prop) s : ForAll1 P s <-> forall n, P (Str_nth n s). @@ -124,7 +124,7 @@ Proof. by induction l; cbn; f_equal. Qed. -Lemma stream_app_f_equal +(*Lemma stream_app_f_equal {A : Type} (l1 l2 : list A) (s1 s2 : Stream A) @@ -133,7 +133,7 @@ Lemma stream_app_f_equal : EqSt (stream_app l1 s1) (stream_app l2 s2). Proof. by subst; induction l2; [ | constructor]. -Qed. +Qed.*) Lemma stream_app_inj_l {A : Type} @@ -248,7 +248,7 @@ Proof. right. apply IHn. exists k. split; [lia | done]. Qed. -Lemma stream_prefix_app_l +(*Lemma stream_prefix_app_l {A : Type} (l : list A) (s : Stream A) @@ -259,9 +259,9 @@ Proof. revert n Hle; induction l; intros [| n] Hle. 1-3: by inversion Hle. by cbn in *; rewrite IHl; [| lia]. -Qed. +Qed.*) -Lemma stream_prefix_app_r +(*Lemma stream_prefix_app_r {A : Type} (l : list A) (s : Stream A) @@ -275,7 +275,7 @@ Proof. - intros s [| a l] Hge; cbn in *; [done | lia]. - intros s [| a l] Hge; cbn in *; [done |]. rewrite <- IHn; [done | lia]. -Qed. +Qed.*) Lemma stream_prefix_map {A B : Type} @@ -301,7 +301,7 @@ element or two consecutive elements at a time with corresponding list quantifiers applied on their finite prefixes. *) -Lemma stream_prefix_ForAll +(*Lemma stream_prefix_ForAll {A : Type} (P : A -> Prop) (s : Stream A) @@ -322,7 +322,7 @@ Proof. specialize (Hi _ _ Hn). apply nth_error_nth with (d := hd s) in Hi. by rewrite Hi in Hp. -Qed. +Qed.*) Lemma stream_prefix_ForAll2 {A : Type} @@ -369,7 +369,7 @@ Proof. by apply Hp. Qed. -Lemma ForAll2_strict_lookup_rev [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R} +(*Lemma ForAll2_strict_lookup_rev [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R} (l : Stream A) (Hl : ForAll2 R l) : forall m n, R (Str_nth m l) (Str_nth n l) -> m < n. Proof. @@ -383,9 +383,9 @@ Proof. - specialize (Hl n m). spec Hl; [lia|]. elim (HI (Str_nth n l)). by transitivity (Str_nth m l). -Qed. +Qed.*) -Lemma ForAll2_strict_lookup_inj +(*Lemma ForAll2_strict_lookup_inj [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R} (l : Stream A) (Hl : ForAll2 R l) : forall m n, Str_nth m l = Str_nth n l -> m = n. @@ -398,7 +398,7 @@ Proof. by destruct (decide (m < n)) ; [spec Hl m n|spec Hl n m]; (spec Hl; [lia|]) ; rewrite Hmn in Hl. -Qed. +Qed.*) Definition stream_suffix {A : Type} @@ -407,7 +407,7 @@ Definition stream_suffix : Stream A := Str_nth_tl n l. -Lemma stream_suffix_S +(*Lemma stream_suffix_S {A : Type} (l : Stream A) (n : nat) @@ -416,7 +416,7 @@ Proof. revert l. induction n; intros. - by destruct l. - by apply IHn. -Qed. +Qed.*) Lemma stream_suffix_nth {A : Type} @@ -459,7 +459,7 @@ Definition stream_segment : list A := list_suffix (stream_prefix l n2) n1. -Lemma stream_segment_nth +(*Lemma stream_segment_nth {A : Type} (l : Stream A) (n1 n2 : nat) @@ -472,7 +472,7 @@ Proof. unfold stream_segment. rewrite list_suffix_nth; [| done]. by apply stream_prefix_nth. -Qed. +Qed.*) Definition stream_segment_alt {A : Type} @@ -481,7 +481,7 @@ Definition stream_segment_alt : list A := stream_prefix (stream_suffix l n1) (n2 - n1). -Lemma stream_segment_alt_iff +(*Lemma stream_segment_alt_iff {A : Type} (l : Stream A) (n1 n2 : nat) @@ -504,7 +504,7 @@ Proof. assert (Hs: n1 + k - n1 = k) by lia. rewrite Hs in Heq. rewrite Heq, stream_prefix_nth; [do 2 f_equal |]; lia. -Qed. +Qed.*) Lemma stream_prefix_segment {A : Type} @@ -535,7 +535,7 @@ Proof. by rewrite stream_prefix_segment. Qed. -Lemma stream_segment_app +(*Lemma stream_segment_app {A : Type} (l : Stream A) (n1 n2 n3 : nat) @@ -558,7 +558,7 @@ Proof. repeat rewrite list_suffix_length. repeat rewrite stream_prefix_length. lia. -Qed. +Qed.*) Definition monotone_nat_stream_prop (s : Stream nat) @@ -599,10 +599,10 @@ Proof. spec Hs; lia. Qed. -Definition monotone_nat_stream := - {s : Stream nat | monotone_nat_stream_prop s}. +(*Definition monotone_nat_stream := + {s : Stream nat | monotone_nat_stream_prop s}.*) -Lemma monotone_nat_stream_tl +(*Lemma monotone_nat_stream_tl (s : Stream nat) (Hs : monotone_nat_stream_prop s) : monotone_nat_stream_prop (tl s). @@ -611,7 +611,7 @@ Proof. specialize (Hs (S n1) (S n2)). apply Hs. lia. -Qed. +Qed.*) CoFixpoint nat_sequence_from (n : nat) : Stream nat := Cons n (nat_sequence_from (S n)). @@ -638,8 +638,8 @@ Proof. apply ForAll2_forall. intro m. rewrite !nat_sequence_from_nth. lia. Qed. -Definition nat_sequence_sorted : ForAll2 lt nat_sequence := - nat_sequence_from_sorted 0. +(*Definition nat_sequence_sorted : ForAll2 lt nat_sequence := + nat_sequence_from_sorted 0.*) Lemma nat_sequence_from_prefix_sorted : forall m n, LocallySorted lt (stream_prefix (nat_sequence_from m) n). @@ -694,17 +694,17 @@ Definition FinitelyMany : Stream A -> Prop := Definition FinitelyManyBound (s : Stream A) : Type := { n : nat | ForAll1 (fun a => ~ P a) (Str_nth_tl n s)}. -Lemma FinitelyMany_from_bound +(*Lemma FinitelyMany_from_bound : forall s, FinitelyManyBound s -> FinitelyMany s. Proof. intros s [n Hn]. apply Exists_Str_nth_tl. by exists n. -Qed. +Qed.*) -Lemma InfinitelyOften_tl s +(*Lemma InfinitelyOften_tl s : InfinitelyOften s -> InfinitelyOften (tl s). -Proof. by inversion 1. Qed. +Proof. by inversion 1. Qed.*) Definition InfinitelyOften_nth_tl : forall n s, InfinitelyOften s -> InfinitelyOften (Str_nth_tl n s) From 72ca2b2ab114c5f14d679484c48b63522034ce32 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 19:06:59 +0300 Subject: [PATCH 12/18] Removing lemmas from StreamFilters.v --- theories/VLSM/Lib/StreamFilters.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/theories/VLSM/Lib/StreamFilters.v b/theories/VLSM/Lib/StreamFilters.v index d70f59d4..18dace60 100644 --- a/theories/VLSM/Lib/StreamFilters.v +++ b/theories/VLSM/Lib/StreamFilters.v @@ -41,7 +41,7 @@ Proof. by apply filtering_subsequence_sorted in Hfs. Qed. -Lemma filtering_subsequence_iff +(*Lemma filtering_subsequence_iff {A : Type} (P Q : A -> Prop) (HPQ : forall a, P a <-> Q a) @@ -52,7 +52,7 @@ Proof. unfold filtering_subsequence. rewrite !ForAll2_forall. by setoid_rewrite <- HPQ. -Qed. +Qed.*) (** Each element in a [filtering_subsequence] is a position in the base stream for which the predicate holds. @@ -276,7 +276,7 @@ Next Obligation. by apply filtering_subsequence_prefix_length. Qed. -Lemma stream_filter_Forall +(*Lemma stream_filter_Forall {A : Type} (P : A -> Prop) (s : Stream A) @@ -291,7 +291,7 @@ Proof. unfold stream_subsequence. rewrite Str_nth_map. by apply filtering_subsequence_witness. -Qed. +Qed.*) (** ** Obtaining [filtering_sequences] for streams @@ -383,7 +383,7 @@ Proof. rewrite Heq. simpl. lia. Qed. -Lemma stream_filter_fst_pos_nth_tl_has_property +(*Lemma stream_filter_fst_pos_nth_tl_has_property (s : Stream A) (n : nat) (sn := Str_nth_tl n s) @@ -403,7 +403,7 @@ Proof. subst i. rewrite <- Str_nth_plus. apply Hnp. simpl in *. lia. -Qed. +Qed.*) (** Given as stream <> for which predicate <

> holds [InfinitelyOften] produces the streams of all its position at which <

> holds in a strictly @@ -463,7 +463,7 @@ Proof. replace (n0 + S (k + kn)) with (S (n0 + kn + k)) by lia. eauto. Qed. -Lemma stream_filter_positions_monotone +(*Lemma stream_filter_positions_monotone (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat) : monotone_nat_stream_prop (stream_filter_positions s Hinf n). Proof. @@ -473,7 +473,7 @@ Proof. intros. constructor; simpl; [|apply H]. apply stream_filter_fst_pos_le. -Qed. +Qed.*) (** [stream_filter_positions] produces a [filtering_sequence]. *) @@ -519,11 +519,11 @@ Definition stream_filter_map (** Stream filtering is obtained as a specialization of [stream_filter_map]. *) -Definition stream_filter +(*Definition stream_filter (s : Stream A) (Hinf : InfinitelyOften P s) : Stream A := - stream_filter_map proj1_sig s Hinf. + stream_filter_map proj1_sig s Hinf.*) End stream_filter_positions. @@ -547,7 +547,7 @@ Definition stream_map_option : Stream B := stream_filter_map P (fun k : dsig P => is_Some_proj (proj2_dsig k)) s Hinf. -Lemma stream_map_option_prefix +(*Lemma stream_map_option_prefix (Hinf : InfinitelyOften P s) (n : nat) (map_opt_pre := map_option f (stream_prefix s n)) @@ -557,7 +557,7 @@ Proof. subst map_opt_pre m. rewrite !(map_option_as_filter f (stream_prefix s n)). apply fitering_subsequence_stream_filter_map_prefix. -Qed. +Qed.*) Program Definition stream_map_option_prefix_ex (Hinf : InfinitelyOften P s) @@ -570,10 +570,10 @@ Next Obligation. by intros; cbn; rewrite !map_option_as_filter. Qed. -Definition bounded_stream_map_option +(*Definition bounded_stream_map_option (Hfin : FinitelyManyBound P s) : list B := - map_option f (stream_prefix s (` Hfin)). + map_option f (stream_prefix s (` Hfin)).*) End stream_map_option. From 8667164a4f8e3b5e59baf6586a0472abc365288b Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 19:35:22 +0300 Subject: [PATCH 13/18] Removing a lemma from Temporal.v --- theories/VLSM/Lib/Temporal.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/VLSM/Lib/Temporal.v b/theories/VLSM/Lib/Temporal.v index dc2a1ab6..900abe90 100644 --- a/theories/VLSM/Lib/Temporal.v +++ b/theories/VLSM/Lib/Temporal.v @@ -116,7 +116,7 @@ Lemma refutation [A:Type] [R:A -> A-> Prop] (HR: well_founded R) by eapply H0; eauto. Qed. -Lemma forall_forever: forall [A B:Type] (P: A -> Stream B -> Prop) [s: Stream B], +(*Lemma forall_forever: forall [A B:Type] (P: A -> Stream B -> Prop) [s: Stream B], (forall (a:A), Forever (P a) s) -> Forever (fun s => forall a, P a s) s. Proof. intros A B P. @@ -127,7 +127,7 @@ Proof. - intro a. by destruct (H a). - apply forall_forever. intro a. by destruct (H a). -Qed. +Qed.*) Lemma not_forever [A:Type] (P: Stream A -> Prop): forall s, ~Forever P s -> Eventually (fun s => ~ P s) s. From 8e31e8098ce941169251956d792f1a939c124cca Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 19:40:52 +0300 Subject: [PATCH 14/18] Removing lemmas from Topsort.v --- theories/VLSM/Lib/TopSort.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/theories/VLSM/Lib/TopSort.v b/theories/VLSM/Lib/TopSort.v index 60a9a663..95ce414d 100644 --- a/theories/VLSM/Lib/TopSort.v +++ b/theories/VLSM/Lib/TopSort.v @@ -135,7 +135,7 @@ Proof. by destruct (decide (precedes a a)). Qed. -Lemma precedes_asymmetric +(*Lemma precedes_asymmetric (a b : A) (Ha : P a) (Hb : P b) @@ -148,7 +148,7 @@ Proof. (exist P a Ha) (exist P b Hb) Hab Hba ). -Qed. +Qed.*) Lemma precedes_transitive (a b c : A) @@ -340,7 +340,7 @@ Qed. As a corollary of the above, if <> then <> can be found before <> in l. *) -Corollary top_sort_precedes +(*Corollary top_sort_precedes (a b : A) (Hab : precedes a b) (Ha : a ∈ l) @@ -354,7 +354,7 @@ Proof. destruct Ha12 as [l1 [l2 Ha12]]. subst l12. exists l1, l2, l3. by rewrite Hb', <- app_assoc. -Qed. +Qed.*) End topologically_sorted_fixed_list. End topologically_sorted. @@ -761,7 +761,7 @@ Proof. by intro; apply Forall_forall. Qed. -Corollary simple_topologically_sorted_precedes_closed_remove_last +(*Corollary simple_topologically_sorted_precedes_closed_remove_last (l : list A) (Hts : topologically_sorted precedes l) (init : list A) @@ -772,36 +772,36 @@ Corollary simple_topologically_sorted_precedes_closed_remove_last Proof. eapply topologically_sorted_precedes_closed_remove_last; [typeclasses eauto | apply Forall_True | done..]. -Qed. +Qed.*) -Corollary simple_top_sort_correct : forall l, +(*Corollary simple_top_sort_correct : forall l, topological_sorting precedes l (top_sort precedes l). Proof. intro; eapply top_sort_correct; [typeclasses eauto | apply Forall_True]. -Qed. +Qed.*) -Corollary simple_maximal_element_in l +(*Corollary simple_maximal_element_in l (a : A) (Hmax : get_maximal_element precedes l = Some a) : a ∈ l. Proof. eapply maximal_element_in; [typeclasses eauto | apply Forall_True | done]. -Qed. +Qed.*) -Corollary simple_get_maximal_element_correct l +(*Corollary simple_get_maximal_element_correct l (a max : A) (Hina : a ∈ l) (Hmax : get_maximal_element precedes l = Some max) : ~ precedes max a. Proof. eapply get_maximal_element_correct; [typeclasses eauto | apply Forall_True | done..]. -Qed. +Qed.*) -Corollary simple_get_maximal_element_some +(*Corollary simple_get_maximal_element_some l (Hne : l <> []) : exists a, get_maximal_element precedes l = Some a. Proof. eapply get_maximal_element_some; [apply Forall_True | done]. -Qed. +Qed.*) End sec_simple_top_sort. From 152864fdb0f6cca4ddc39b8a665076238b70a553 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 19:51:14 +0300 Subject: [PATCH 15/18] Removing lemmas from TraceClassicalProperties.v --- theories/VLSM/Lib/TraceClassicalProperties.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/VLSM/Lib/TraceClassicalProperties.v b/theories/VLSM/Lib/TraceClassicalProperties.v index c365864e..c41a281f 100644 --- a/theories/VLSM/Lib/TraceClassicalProperties.v +++ b/theories/VLSM/Lib/TraceClassicalProperties.v @@ -16,22 +16,22 @@ Context {A B : Type}. (** ** Relating finiteness and infiniteness *) -Lemma not_infiniteT_finiteT : forall tr : trace, +(*Lemma not_infiniteT_finiteT : forall tr : trace, ~ infiniteT tr -> finiteT tr. Proof. move => tr Hnot. case: (classic (finiteT tr)) => Hinf //. case: Hnot. exact: not_finiteT_infiniteT. -Qed. +Qed.*) -Lemma finiteT_infiniteT : forall tr : trace, +(*Lemma finiteT_infiniteT : forall tr : trace, finiteT tr \/ infiniteT tr. Proof. move => tr. case: (classic (finiteT tr)) => Hinf; first by left. right; exact: not_finiteT_infiniteT. -Qed. +Qed.*) Definition finiteT_infiniteT_dec (tr : trace) : { finiteT tr }+{ infiniteT tr } := match excluded_middle_informative (finiteT tr) with @@ -71,10 +71,10 @@ exists (midp h2); split. - exact: (midpointT_after (midpointT_midp h2)). Qed. -Lemma AppendT_assoc_R: forall (p1 p2 p3 : propT), (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3. +(*Lemma AppendT_assoc_R: forall (p1 p2 p3 : propT), (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3. Proof. move => [f1 hf1] [f2 hf2] [f3 hf3] tr0 /= h1. exact: appendT_assoc_R. -Qed. +Qed.*) End TraceClassicalProperties. From e816ebc3443936fb362e697aafcd3e1700a4b524 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Tue, 2 Aug 2022 20:15:24 +0300 Subject: [PATCH 16/18] Removing lemmas from TraceProperties.v --- theories/VLSM/Lib/TraceProperties.v | 276 ++++++++++++++-------------- 1 file changed, 138 insertions(+), 138 deletions(-) diff --git a/theories/VLSM/Lib/TraceProperties.v b/theories/VLSM/Lib/TraceProperties.v index 4388b338..75079c48 100644 --- a/theories/VLSM/Lib/TraceProperties.v +++ b/theories/VLSM/Lib/TraceProperties.v @@ -41,13 +41,13 @@ Qed. Definition InfiniteT : propT := exist _ (fun tr => infiniteT tr) infiniteT_setoidT. -Lemma infiniteT_cons : forall a b tr, +(*Lemma infiniteT_cons : forall a b tr, infiniteT (Tcons a b tr) -> infiniteT tr. Proof. by move => a b tr Hinf; inversion Hinf. -Qed. +Qed.*) -Lemma infiniteT_trace_append : +(*Lemma infiniteT_trace_append : forall tr, infiniteT tr -> forall tr', infiniteT (tr' +++ tr). Proof. cofix CIH. @@ -55,16 +55,16 @@ move => tr Htr. case => [a|a b tr']; first by rewrite trace_append_nil. rewrite trace_append_cons. exact/infiniteT_delay/CIH. -Qed. +Qed.*) -Lemma trace_append_infiniteT : +(*Lemma trace_append_infiniteT : forall tr, infiniteT tr -> forall tr', infiniteT (tr +++ tr'). Proof. cofix CIH. case => [a|a b tr0] Hinf; inversion Hinf => tr'; subst. rewrite trace_append_cons. exact/infiniteT_delay/CIH. -Qed. +Qed.*) (** ** Finiteness property *) @@ -91,20 +91,20 @@ Proof. by inversion h. Defined. (** Equality coincides with bisimilarity for finite traces. *) -Lemma finiteT_bisim_eq : forall tr, +(*Lemma finiteT_bisim_eq : forall tr, finiteT tr -> forall tr', bisim tr tr' -> tr = tr'. Proof. move => tr; elim => [a tr'|a b tr0 Hfin IH tr'] Hbis; invs Hbis => //. by rewrite (IH _ H3). -Qed. +Qed.*) (** Basic connections between finiteness and infiniteness. *) -Lemma finiteT_infiniteT_not : forall tr, +(*Lemma finiteT_infiniteT_not : forall tr, finiteT tr -> infiniteT tr -> False. Proof. by move => tr; elim => [a|a b tr' Hfin IH] Hinf; inversion Hinf. -Qed. +Qed.*) Lemma not_finiteT_infiniteT : forall tr, ~ finiteT tr -> infiniteT tr. @@ -133,19 +133,19 @@ Inductive finalTB : trace -> B -> Prop := finalTB tr b' -> finalTB (Tcons a b tr) b'. -Lemma finalTA_finiteT : forall tr a, finalTA tr a -> finiteT tr. +(*Lemma finalTA_finiteT : forall tr a, finalTA tr a -> finiteT tr. Proof. move => tr a; elim => [a1|a1 b a2 tr' Hfinal IH]. - exact: finiteT_nil. - exact/finiteT_delay/IH. -Qed. +Qed.*) -Lemma finalTB_finiteT : forall tr b, finalTB tr b -> finiteT tr. +(*Lemma finalTB_finiteT : forall tr b, finalTB tr b -> finiteT tr. Proof. move => tr b; elim => [a1 b1 a2|a1 b1 b2 a2 Hfin IH]. - exact/finiteT_delay/finiteT_nil. - exact: finiteT_delay. -Qed. +Qed.*) Fixpoint finalA (tr : trace) (h : finiteT tr) {struct h} : A := match tr as tr' return (finiteT tr' -> A) with @@ -153,21 +153,21 @@ match tr as tr' return (finiteT tr' -> A) with | Tcons a b tr => fun h => finalA (invert_finiteT_delay h) end h. -Lemma finiteT_finalTA : forall tr (h : finiteT tr), +(*Lemma finiteT_finalTA : forall tr (h : finiteT tr), finalTA tr (finalA h). Proof. refine (fix IH tr h {struct h} := _). case: tr h => [a|a b tr] h; dependent inversion h => /=. - exact: finalTA_nil. - exact: finalTA_delay. -Qed. +Qed.*) -Lemma finalTA_hd_append_trace : forall tr0 a, +(*Lemma finalTA_hd_append_trace : forall tr0 a, finalTA tr0 a -> forall tr1, hd tr1 = a -> hd (tr0 +++ tr1) = hd tr0. Proof. by move => tr a; elim => {tr a} [a tr <-|a b a' tr Hfinal IH tr'] //=. -Qed. +Qed.*) (** ** Basic trace properties and connectives *) @@ -184,8 +184,8 @@ Definition ffT : trace -> Prop := fun tr => False. Lemma ffT_setoidT : setoidT ffT. Proof. by []. Qed. -Definition FfT : propT := -exist _ ffT ffT_setoidT. +(*Definition FfT : propT := +exist _ ffT ffT_setoidT.*) Definition notT (p : trace -> Prop) : trace -> Prop := fun tr => ~ p tr. @@ -195,20 +195,20 @@ move => p hp tr h1 tr' h2 h3. apply: h1. apply: hp _ h3 _ (bisim_sym h2). Qed. -Definition NotT (p : propT) : propT := +(*Definition NotT (p : propT) : propT := let: exist f hf := p in -exist _ (notT f) (notT_setoidT hf). +exist _ (notT f) (notT_setoidT hf).*) Definition satisfyT (p : propT) : trace -> Prop := fun tr => let: exist f0 h0 := p in f0 tr. -Program Definition ExT {T: Type} (p: T -> propT) : propT := +(*Program Definition ExT {T: Type} (p: T -> propT) : propT := exist _ (fun tr => exists x, satisfyT (p x) tr) _. Next Obligation. move => tr0 [x h0] tr1 h1. exists x. case: (p x) h0 => [f0 h2] /= h0. exact: h2 _ h0 _ h1. -Defined. +Defined.*) Lemma andT_setoidT : forall f0 f1, setoidT f0 -> setoidT f1 -> @@ -247,29 +247,29 @@ forall tr, satisfyT p1 tr -> satisfyT p2 tr. #[local] Infix "=>>" := propT_imp (at level 60, right associativity). -Lemma propT_imp_conseq_L: forall p0 p1 q, p0 =>> p1 -> p1 =>> q -> p0 =>> q. +(*Lemma propT_imp_conseq_L: forall p0 p1 q, p0 =>> p1 -> p1 =>> q -> p0 =>> q. Proof. move => [p0 hp0] [p1 hp1] [q hq] h0 h1 tr0 /= h2. exact/h1/h0. -Qed. +Qed.*) -Lemma propT_imp_conseq_R: forall p q0 q1, +(*Lemma propT_imp_conseq_R: forall p q0 q1, q0 =>> q1 -> p =>> q0 -> p =>> q1. Proof. move => [p hp] [q0 hq0] [q1 hq1] h0 h1 tr0 /= h2. exact/h0/h1. -Qed. +Qed.*) -Lemma propT_imp_andT: forall p q0 q1, +(*Lemma propT_imp_andT: forall p q0 q1, p =>> q0 -> p =>> q1 -> p =>> (q0 andT q1). Proof. move => [p hp] [q0 hq0] [q1 hq1] h0 h1 tr0 /= h2. split. - exact: h0. - exact: h1. -Qed. +Qed.*) -Lemma propT_imp_refl : forall p, p =>> p. -Proof. by move => p. Qed. +(*Lemma propT_imp_refl : forall p, p =>> p. +Proof. by move => p. Qed.*) Lemma satisfyT_cont : forall p0 p1, p0 =>> p1 -> forall tr, satisfyT p0 tr -> satisfyT p1 tr. @@ -284,15 +284,15 @@ move => p q r h0 h1 tr0 h2. exact/(satisfyT_cont h1)/(satisfyT_cont h0 h2). Qed. -Lemma OrT_left : forall p1 p2, p1 =>> (p1 orT p2). +(*Lemma OrT_left : forall p1 p2, p1 =>> (p1 orT p2). Proof. by move => [f1 hf1] [f2 hf2] tr /= h1; left. -Qed. +Qed.*) -Lemma OrT_right: forall p1 p2, p2 =>> (p1 orT p2). +(*Lemma OrT_right: forall p1 p2, p2 =>> (p1 orT p2). Proof. by move => [f1 hf1] [f2 hf2] tr /= h1; right. -Qed. +Qed.*) (** ** Basic trace element properties and connectives *) @@ -310,8 +310,8 @@ Definition andA (u1 u2: propA) : propA := fun a => u1 a /\ u2 a. #[local] Infix "andA" := andA (at level 60, right associativity). -Definition exA {T : Type} (u: T -> propA) : propA := -fun st => exists x, u x st. +(*Definition exA {T : Type} (u: T -> propA) : propA := +fun st => exists x, u x st.*) (** ** Singleton property *) @@ -327,12 +327,12 @@ move => u tr0 [a [h0 h2]] tr1 h1; invs h2; invs h1. exact: nil_singletonT. Qed. -Lemma singletonT_cont : forall u v, u ->> v -> +(*Lemma singletonT_cont : forall u v, u ->> v -> forall tr, singletonT u tr -> singletonT v tr. Proof. move => u v huv tr0 [a [h0 h1]]; invs h1. exact/nil_singletonT/huv. -Qed. +Qed.*) Lemma singletonT_nil: forall u a, singletonT u (Tnil a) -> u a. Proof. by move => u st [a [h0 h1]]; invs h1. Qed. @@ -342,11 +342,11 @@ exist _ (singletonT u) (@singletonT_setoidT u). #[local] Notation "[| p |]" := (SingletonT p) (at level 80). -Lemma SingletonT_cont: forall u v, u ->> v -> [|u|] =>> [|v|]. +(*Lemma SingletonT_cont: forall u v, u ->> v -> [|u|] =>> [|v|]. Proof. move => u v h0 tr0 [a [h1 h2]]; invs h2. exact/nil_singletonT/h0. -Qed. +Qed.*) (** ** Duplicate element property *) @@ -379,11 +379,11 @@ exist _ (dupT u b) (@dupT_setoidT u b). #[local] Notation "<< p ; b >>" := (DupT p b) (at level 80). -Lemma DupT_cont: forall u v b, u ->> v -> <> =>> <>. +(*Lemma DupT_cont: forall u v b, u ->> v -> <> =>> <>. Proof. move => u v b h0 tr0 /=. exact: dupT_cont. -Qed. +Qed.*) (** ** Follows property *) @@ -427,14 +427,14 @@ move => tr0 tr1 h0 tr2 h1 tr3 h2; invs h0. exact: (followsT_delay a b (CIH _ _ H _ H5 _ H4)). Qed. -Lemma followsT_setoidT_L : forall p, +(*Lemma followsT_setoidT_L : forall p, forall tr0 tr1, followsT p tr0 tr1 -> forall tr2, bisim tr0 tr2 -> followsT p tr2 tr1. Proof. move => p. cofix CIH. move => tr tr0 h0 tr1 h1; invs h0; invs h1. - exact: followsT_nil. - exact: (followsT_delay a b (CIH _ _ H _ H4)). -Qed. +Qed.*) Lemma followsT_setoidT_R : forall (p: trace -> Prop) (hp: forall tr0, p tr0 -> forall tr1, bisim tr0 tr1 -> p tr1), @@ -448,7 +448,7 @@ move => tr tr0 h0 tr1 h1; invs h0. - invs h1. exact: (followsT_delay a b (CIH _ _ H _ H4)). Qed. -Lemma followsT_cont : forall (p q : trace -> Prop), +(*Lemma followsT_cont : forall (p q : trace -> Prop), (forall tr, p tr -> q tr) -> forall tr0 tr1, followsT p tr0 tr1 -> followsT q tr0 tr1. Proof. @@ -456,7 +456,7 @@ move => p q hpq. cofix CIH. move => tr0 tr1 h0; invs h0. - apply: followsT_nil => //. exact: hpq _ H0. - exact/followsT_delay/CIH. -Qed. +Qed.*) Lemma followsT_singletonT: forall u tr0 tr1, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1. @@ -467,7 +467,7 @@ move => u. cofix CIH. move => tr0 tr1 h0; invs h0. - exact/bisim_cons/CIH. Qed. -Lemma followsT_singleton_andA_L: forall u0 u1 tr0, +(*Lemma followsT_singleton_andA_L: forall u0 u1 tr0, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0. Proof. @@ -479,9 +479,9 @@ move => u0 u1. cofix CIH. case. exact: nil_singletonT. - move => a b tr0 h0; invs h0. exact/followsT_delay/CIH. -Qed. +Qed.*) -Lemma followsT_singleton_andA_R: forall u0 u1 tr0, +(*Lemma followsT_singleton_andA_R: forall u0 u1 tr0, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0. Proof. @@ -493,9 +493,9 @@ move => u0 u1. cofix CIH. case. exact: nil_singletonT. - move => a b tr0 h0; invs h0. exact/followsT_delay/CIH. -Qed. +Qed.*) -Lemma singletonT_andA_followsT: forall u v tr, +(*Lemma singletonT_andA_followsT: forall u v tr, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr. Proof. @@ -504,15 +504,15 @@ move => u v. cofix CIH. move => tr h0 h1; invs h0; invs h1. apply: nil_singletonT. by split; apply: singletonT_nil. - exact/followsT_delay/CIH. -Qed. +Qed.*) -Lemma followsT_ttA : forall tr, followsT (singletonT ttA) tr tr. +(*Lemma followsT_ttA : forall tr, followsT (singletonT ttA) tr tr. Proof. cofix CIH. case => [a|a b tr0]. - apply: followsT_nil => //. exact: nil_singletonT. - exact/followsT_delay/CIH. -Qed. +Qed.*) (** ** Append property *) @@ -545,13 +545,13 @@ move => p0 p1 q hp tr. exact: (@appendT_cont _ _ q q hp _). Qed. -Lemma appendT_cont_R: forall (p q0 q1: trace -> Prop), +(*Lemma appendT_cont_R: forall (p q0 q1: trace -> Prop), (forall tr, q0 tr -> q1 tr) -> forall tr, (appendT p q0 tr) -> (appendT p q1 tr). Proof. move => p q0 q1 hq tr. exact: (@appendT_cont p p _ _ _ hq). -Qed. +Qed.*) Lemma appendT_setoidT: forall (p0 p1: trace -> Prop), setoidT p1 -> setoidT (appendT p0 p1). @@ -561,7 +561,7 @@ move: h0 => [tr2 [h0 h2]]. exists tr2; split; first by apply: h0. exact: (followsT_setoidT_R hp1 h2 h1). Qed. -Lemma followsT_followsT: forall p q tr0 tr1 tr2, followsT p tr0 tr1 -> +(*Lemma followsT_followsT: forall p q tr0 tr1 tr2, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2. Proof. move => p q. cofix CIH. case. @@ -569,7 +569,7 @@ move => p q. cofix CIH. case. apply: followsT_nil => //. by exists tr1. - move => a b tr0 tr1 tr2 h0 h1; invs h0; invs h1. exact: followsT_delay _ _ (CIH _ _ _ H3 H4). -Qed. +Qed.*) Lemma appendT_assoc_L : forall p1 p2 p3 tr, (appendT (appendT p1 p2) p3) tr -> appendT p1 (appendT p2 p3) tr. @@ -583,7 +583,7 @@ move => tr0 tr1 tr2 h1 h2; invs h2. - invs h1. exact: followsT_delay _ _ (CIH _ _ _ H4 H). Qed. -Lemma appendT_finalTA: forall (p q : trace -> Prop) tr0 tr1, +(*Lemma appendT_finalTA: forall (p q : trace -> Prop) tr0 tr1, p tr0 -> q tr1 -> finalTA tr0 (hd tr1) -> (p *+* q) (tr0 +++ tr1). Proof. @@ -594,7 +594,7 @@ move: {hp} tr0 tr1 hq hfin. cofix CIH. case. - move => a b tr0 tr1 h0 h1; invs h1. rewrite [Tcons a b tr0 +++ tr1]trace_destr /=. exact/followsT_delay/CIH. -Qed. +Qed.*) Definition AppendT (p1 p2: propT) : propT := let: exist f0 h0 := p1 in @@ -603,19 +603,19 @@ exist _ (appendT f0 f1) (appendT_setoidT h1). #[local] Infix "***" := AppendT (at level 60, right associativity). -Lemma AppendT_assoc_L: forall p1 p2 p3, ((p1 *** p2) *** p3) =>> (p1 *** p2 *** p3). +(*Lemma AppendT_assoc_L: forall p1 p2 p3, ((p1 *** p2) *** p3) =>> (p1 *** p2 *** p3). Proof. move => [f1 hf1] [f2 hf2] [f3 hf3] tr0 /= h1. exact: appendT_assoc_L. -Qed. +Qed.*) -Lemma AppendT_cont : forall p1 p2 q1 q2, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> (p2 *** q2). +(*Lemma AppendT_cont : forall p1 p2 q1 q2, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> (p2 *** q2). Proof. move => [p1 hp1] [p2 hp2] [q1 hq1] [q2 hq2] h0 h1 tr0 /= h2. apply: (appendT_cont _ _ h2). - exact: h0. - exact: h1. -Qed. +Qed.*) Lemma AppendT_cont_L: forall p1 p2 q, p1 =>> p2 -> (p1 *** q) =>> (p2 *** q). Proof. @@ -629,7 +629,7 @@ move => [q hq] [p1 hp1] [p2 hp2] h0 tr0 /= h1. exact: (@appendT_cont q q p1 p2). Qed. -Lemma AppendT_ttA: forall p, p =>> (p *** [|ttA|]). +(*Lemma AppendT_ttA: forall p, p =>> (p *** [|ttA|]). Proof. move => [f hp] tr0 /= h0. exists tr0; split => //. @@ -637,72 +637,72 @@ move: {h0 hp} tr0. cofix CIH. case => [a|a b tr0]. - exact/followsT_nil/nil_singletonT. - exact/followsT_delay/CIH. -Qed. +Qed.*) -Lemma SingletonT_DupT_AppendT_andA_DupT : forall u v b, ([|u|] *** <>) =>> <>. +(*Lemma SingletonT_DupT_AppendT_andA_DupT : forall u v b, ([|u|] *** <>) =>> <>. Proof. move => u v b tr0 [tr1 [[a [h0 h2]] h1]] /=; invs h2; invs h1. move: H1 => [a [h1 h2]]; invs h2; invs H1. exact: dupT_Tcons. -Qed. +Qed.*) -Lemma DupT_andA_AppendT_SingletonT_DupT : forall u v b, <> =>> ([|u|] *** <>). +(*Lemma DupT_andA_AppendT_SingletonT_DupT : forall u v b, <> =>> ([|u|] *** <>). Proof. move => u v b tr0 [a [[hu hv] h1]]; invs h1; invs H1. exists (Tnil a); split; first by apply: nil_singletonT. apply: followsT_nil => //. exact: dupT_Tcons. -Qed. +Qed.*) -Lemma DupT_andA_AppendT_SingletonT : forall u v b, <> =>> <> *** [|v|]. +(*Lemma DupT_andA_AppendT_SingletonT : forall u v b, <> =>> <> *** [|v|]. Proof. move => u v b tr0 [a [[hu hv] h0]]; invs h0; invs H1. exists (Tcons a b (Tnil a)); split. - exact: dupT_Tcons. - apply: followsT_delay. apply: followsT_nil => //. exact: nil_singletonT. -Qed. +Qed.*) -Lemma DupT_AppendT_SingletonT_andA_DupT : forall u v b, (<> *** [|v|]) =>> <>. +(*Lemma DupT_AppendT_SingletonT_andA_DupT : forall u v b, (<> *** [|v|]) =>> <>. Proof. move => u v b tr0 [tr1 [[a [hu h0]] h1]]. invs h0; invs H1; invs h1; invs H3; move: H1 => [a [hv h0]]; invs h0 => /=. exact: dupT_Tcons. -Qed. +Qed.*) -Lemma AppendT_andA : forall u v, ([|u|] *** [|v|]) =>> [|u andA v|]. +(*Lemma AppendT_andA : forall u v, ([|u|] *** [|v|]) =>> [|u andA v|]. Proof. move => u v tr0 [tr1 [[a [hu h0]] h1]]. invs h0; invs h1; move: H1 => [a [hv h0]]; invs h0 => /=. exact: nil_singletonT. -Qed. +Qed.*) -Lemma andA_AppendT: forall u v, [|u andA v|] =>> [|u|] *** [|v|]. +(*Lemma andA_AppendT: forall u v, [|u andA v|] =>> [|u|] *** [|v|]. Proof. move => u v tr0 [a [[hu hv] h0]]; invs h0. exists (Tnil a); split; first by apply: nil_singletonT. apply: followsT_nil => //. exact: nil_singletonT. -Qed. +Qed.*) Lemma SingletonT_AppendT: forall v p, ([|v|] *** p) =>> p. Proof. by move => v [p hp] tr0 /= [tr1 [[a [h0 h2]] h1]]; invs h1; invs h2. Qed. -Lemma ttA_AppendT_implies : forall p, ([|ttA|] *** p) =>> p. +(*Lemma ttA_AppendT_implies : forall p, ([|ttA|] *** p) =>> p. Proof. move => p. exact: SingletonT_AppendT. -Qed. +Qed.*) -Lemma implies_ttA_AppendT: forall p, p =>> [|ttA|] *** p. +(*Lemma implies_ttA_AppendT: forall p, p =>> [|ttA|] *** p. Proof. move => [p hp] tr0 /= htr0. exists (Tnil (hd tr0)); split. - exact: nil_singletonT. - exact: followsT_nil. -Qed. +Qed.*) Lemma appendT_singletonT: forall p (hp: setoidT p) u tr, appendT p (singletonT u) tr -> p tr. @@ -717,13 +717,13 @@ move => [p hp] v tr0 /=. exact: appendT_singletonT. Qed. -Lemma AppendT_ttA_implies : forall p, (p *** [|ttA|]) =>> p. +(*Lemma AppendT_ttA_implies : forall p, (p *** [|ttA|]) =>> p. Proof. move => p. exact: AppendT_Singleton. -Qed. +Qed.*) -Lemma implies_AppendT_ttA: forall p, p =>> p *** [|ttA|]. +(*Lemma implies_AppendT_ttA: forall p, p =>> p *** [|ttA|]. Proof. move => [p hp] tr0 /= htr0. exists tr0; split => //. @@ -732,48 +732,48 @@ case => [a|a b tr0]. - apply: followsT_nil => //. exact: nil_singletonT. - exact/followsT_delay/CIH. -Qed. +Qed.*) -Lemma TtT_AppendT_idem: (TtT *** TtT) =>> TtT. -Proof. by []. Qed. +(*Lemma TtT_AppendT_idem: (TtT *** TtT) =>> TtT. +Proof. by []. Qed.*) -Lemma AppendT_FiniteT_idem : (FiniteT *** FiniteT) =>> FiniteT. +(*Lemma AppendT_FiniteT_idem : (FiniteT *** FiniteT) =>> FiniteT. Proof. move => tr0 [tr1 [Hfin Hfol]]. elim: Hfin tr0 Hfol => [a tr0'|a b tr1' h0 IH tr0] Hfol; invs Hfol => //. exact/finiteT_delay/IH. -Qed. +Qed.*) -Lemma FiniteT_AppendT_idem : FiniteT =>> FiniteT *** FiniteT. +(*Lemma FiniteT_AppendT_idem : FiniteT =>> FiniteT *** FiniteT. Proof. move => tr0 h0. exists (Tnil (hd tr0)); split. - exact: finiteT_nil. - exact: followsT_nil. -Qed. +Qed.*) -Lemma FiniteT_SingletonT: forall u, (FiniteT *** [|u|]) =>> FiniteT. +(*Lemma FiniteT_SingletonT: forall u, (FiniteT *** [|u|]) =>> FiniteT. Proof. move => u tr /= [tr1 [h0 h1]]. exact: (finiteT_setoidT h0 (followsT_singletonT h1)). -Qed. +Qed.*) -Lemma InfiniteT_implies_AppendT : InfiniteT =>> (TtT *** [|ffA|]). +(*Lemma InfiniteT_implies_AppendT : InfiniteT =>> (TtT *** [|ffA|]). Proof. move => tr0 [a b tr1] HinfT /=. exists (Tcons a b tr1); split => {tr0} //. move: a b tr1 HinfT. cofix CIH. move => a b tr1 HinfT; invs HinfT. exact/followsT_delay/CIH. -Qed. +Qed.*) -Lemma AppendT_implies_InfiniteT: (TtT *** [|ffA|]) =>> InfiniteT. +(*Lemma AppendT_implies_InfiniteT: (TtT *** [|ffA|]) =>> InfiniteT. Proof. move => tr0 [tr1 [_ h1]] /=. move: tr0 tr1 h1; cofix CIH => tr0 tr1 h1; invs h1. - by move: H0 => [a [h1 h2]]; inversion h1. - exact: infiniteT_delay _ _ (CIH _ _ H). -Qed. +Qed.*) (** ** Iteration property *) @@ -811,7 +811,7 @@ move => tr0 h0; invs h0; first by apply: iterT_stop. exact: iterT_loop (hp _ H) (h _ _ H0). Qed. -Lemma iterT_appendT_dupT: forall (u : propA) p b tr, +(*Lemma iterT_appendT_dupT: forall (u : propA) p b tr, u (hd tr) -> iterT (appendT p (dupT u b)) tr -> followsT (singletonT u) tr tr. Proof. @@ -825,7 +825,7 @@ move => u p b. cofix CIH. move => tr h0 h1; invs h1. invs h3; invs H1; invs h1; invs H3. exact/followsT_delay/CIH. + invs h1. exact: followsT_delay _ _ (CIH1 _ _ _ H H4). -Qed. +Qed.*) Definition IterT (p : propT) : propT := let: exist f0 h0 := p in @@ -844,11 +844,11 @@ move => p tr h0; invs h0. - by right; exists tr0. Qed. -Lemma IterT_unfold_0: forall p, IterT p =>> ([|ttA|] orT (p *** IterT p)). +(*Lemma IterT_unfold_0: forall p, IterT p =>> ([|ttA|] orT (p *** IterT p)). Proof. move => [p hp] tr0 /= h0. exact: iterT_split_1 h0. -Qed. +Qed.*) Lemma iterT_split_2: forall tr p, (singletonT ttA tr) \/ (appendT p (iterT p) tr) -> iterT p tr. @@ -858,11 +858,11 @@ move => tr p [[a [h0 h1]]|[tr0 [h0 h1]]]. - exact: iterT_loop h0 h1. Qed. -Lemma IterT_fold_0 : forall p, ([|ttA|] orT (p *** IterT p)) =>> IterT p. +(*Lemma IterT_fold_0 : forall p, ([|ttA|] orT (p *** IterT p)) =>> IterT p. Proof. move => [p hp] tr0 /=. exact: iterT_split_2. -Qed. +Qed.*) Lemma iterT_unfold_1 : forall p tr, (iterT p *+* p) tr -> iterT p tr. Proof. @@ -880,30 +880,30 @@ move => tr0 tr1 h0 h1; invs h0. exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed. -Lemma IterT_unfold_1 : forall p, (IterT p *** p) =>> IterT p. +(*Lemma IterT_unfold_1 : forall p, (IterT p *** p) =>> IterT p. Proof. move => [p hp] tr /= h0. exact: iterT_unfold_1 h0. -Qed. +Qed.*) -Lemma IterT_unfold_2: forall p, ([|ttA|] orT (IterT p *** p)) =>> IterT p. +(*Lemma IterT_unfold_2: forall p, ([|ttA|] orT (IterT p *** p)) =>> IterT p. Proof. move => [p hp] tr0 /= [[a [_ h0]]|H]. - invs h0. exact: iterT_stop. - exact: iterT_unfold_1 H. -Qed. +Qed.*) -Lemma stop_IterT : forall p, [|ttA|] =>> IterT p. +(*Lemma stop_IterT : forall p, [|ttA|] =>> IterT p. Proof. move => [p hp] /= t0 [x [_ h0]]; invs h0 => /=. exact: iterT_stop. -Qed. +Qed.*) -Lemma IterT_fold_L : forall p, (p *** IterT p) =>> IterT p. +(*Lemma IterT_fold_L : forall p, (p *** IterT p) =>> IterT p. Proof. move => [p hp] tr0 /= [tr1 [h0 h1]]. exact: (iterT_loop h0). -Qed. +Qed.*) Lemma iterT_iterT_2 : forall p tr, iterT p tr -> appendT (iterT p) (iterT p) tr. Proof. @@ -915,11 +915,11 @@ case => [a|a b tr0]. - exact/followsT_delay/CIH. Qed. -Lemma IterT_IterT_2 : forall p, IterT p =>> (IterT p *** IterT p). +(*Lemma IterT_IterT_2 : forall p, IterT p =>> (IterT p *** IterT p). Proof. move => [p hp] tr0 /=. exact: iterT_iterT_2. -Qed. +Qed.*) Lemma iterT_iterT : forall p tr, appendT (iterT p) (iterT p) tr -> (iterT p) tr. Proof. @@ -934,8 +934,8 @@ move: tr1 tr0 h0 h1. cofix CIH. move => tr0 tr1 h0; invs h0 => h0. exact: followsT_delay _ _ (CIH2 _ _ _ H H4). Qed. -Lemma IterT_IterT : forall p, (IterT p *** IterT p) =>> IterT p. -Proof. move => [p hp] tr /=. exact: iterT_iterT. Qed. +(*Lemma IterT_IterT : forall p, (IterT p *** IterT p) =>> IterT p. +Proof. move => [p hp] tr /=. exact: iterT_iterT. Qed.*) Lemma IterT_DupT : forall v b, ([|v|] *** (IterT (TtT *** <>))) =>> (TtT *** [|v|]). @@ -975,27 +975,27 @@ move => [f hf] [g hg] /= h0. exact/lastA_cont/h0. Qed. -Lemma LastA_SingletonT_fold : forall u, LastA ([|u|]) ->> u. +(*Lemma LastA_SingletonT_fold : forall u, LastA ([|u|]) ->> u. Proof. by move => u a [tr0 [[st1 [h1 h3]] h2]]; invs h3; invs h2. -Qed. +Qed.*) -Lemma LastA_SingletonT_unfold : forall u, u ->> LastA ([|u|]). +(*Lemma LastA_SingletonT_unfold : forall u, u ->> LastA ([|u|]). Proof. move => u a h0. exists (Tnil a); split. - exact: nil_singletonT. - exact: finalTA_nil. -Qed. +Qed.*) -Lemma lastA_appendA : forall p q a, lastA (appendT p q) a -> lastA q a. +(*Lemma lastA_appendA : forall p q a, lastA (appendT p q) a -> lastA q a. Proof. move => p q a [tr0 [[tr [_ h2]] h1]]. move: h1 tr h2; elim => {tr0 a} [a|a b a' tr0 Hfinal IH] tr h0; invs h0. - exists (Tnil a). by split; last by apply: finalTA_nil. - exists (Tcons a b tr0). by split; last by apply: finalTA_delay. - exact: IH _ H1. -Qed. +Qed.*) Lemma LastA_AppendA : forall p v, LastA (p *** [|v|]) ->> v. Proof. @@ -1006,16 +1006,16 @@ move: h1 tr' h0; elim => {tr a} [a|a b a' tr Hfinal IH] tr0 h0; invs h0. - exact: IH _ H1. Qed. -Lemma LastA_andA : forall p u, ((LastA p) andA u) ->> LastA (p *** [|u|]). +(*Lemma LastA_andA : forall p u, ((LastA p) andA u) ->> LastA (p *** [|u|]). Proof. move => [p hp] u a [[tr0 [h2 h3]] h1]. exists tr0. split => //. exists tr0. split => //. move: {h2} tr0 a h3 h1. cofix CIH. move => tr0 a h0; invs h0 => h0. - exact/followsT_nil/nil_singletonT. - exact: followsT_delay _ _ (CIH _ _ H h0). -Qed. +Qed.*) -Lemma LastA_IterA : forall v b p, +(*Lemma LastA_IterA : forall v b p, LastA ([|v|] *** (IterT (p *** <>))) ->> v. Proof. move => v b p a h0. @@ -1023,9 +1023,9 @@ have h1: p =>> TtT by []. have h2 := LastA_cont (AppendT_cont_R (IterT_cont (AppendT_cont_L h1))) h0. have := LastA_cont (@IterT_DupT v b) h2. exact: LastA_AppendA. -Qed. +Qed.*) -Lemma IterT_LastA_DupT : forall v b, +(*Lemma IterT_LastA_DupT : forall v b, (<> *** (IterT (TtT *** <>))) =>> (TtT *** [|v|]). Proof. move => v b tr0 [tr1 [[a [h0 h2]] h1]]. @@ -1040,9 +1040,9 @@ move: tr' h0 H1. cofix CIH. move => tr0 h0 h1; invs h1. invs h2; invs H1; invs h1; invs H3. exact/followsT_delay/CIH. + invs h1. exact: followsT_delay _ _ (CIH0 _ _ _ H H4). -Qed. +Qed.*) -Lemma LastA_LastA : forall p q, +(*Lemma LastA_LastA : forall p q, (LastA ([|LastA p|] *** q)) ->> (LastA (p *** q)). Proof. move => [p hp] [q hq] a /= [tr1 [[tr0 [[tr2 [h0 h3]] h2]] h1]]; invs h3; invs h2. @@ -1060,16 +1060,16 @@ exists (tr2 +++ tr1). split. + rewrite trace_append_cons. apply: finalTA_delay. exact: IH _ h0 h1. -Qed. +Qed.*) -Lemma SingletonT_andA_AppendT : forall u v, +(*Lemma SingletonT_andA_AppendT : forall u v, (v andA u) ->> LastA ([|v|] *** [|u|]). Proof. move => u v a [h0 h1]. exists (Tnil a); split; last by apply: finalTA_nil. exists (Tnil a); split; first by apply: nil_singletonT. exact/followsT_nil/nil_singletonT. -Qed. +Qed.*) CoFixpoint lastdup (tr : trace) (b : B) : trace := match tr with @@ -1077,10 +1077,10 @@ match tr with | Tcons a b' tr' => Tcons a b' (lastdup tr' b) end. -Lemma lastdup_hd: forall tr b, hd tr = hd (lastdup tr b). +(*Lemma lastdup_hd: forall tr b, hd tr = hd (lastdup tr b). Proof. by case => [a b|a b tr b0]; rewrite [lastdup _ _]trace_destr. -Qed. +Qed.*) Lemma followsT_dupT : forall u tr b, followsT (singletonT u) tr tr -> @@ -1105,7 +1105,7 @@ move => tr a b1; elim => {tr a} [a|a1 b2 a2 tr Hfinal IH]. exact: finalTA_delay. Qed. -Lemma LastA_DupT : forall p u b, +(*Lemma LastA_DupT : forall p u b, LastA (p *** [|u|]) ->> LastA (p *** <>). Proof. move => [p hp] u b a [tr0 [[tr1 [h0 h2]] h1]]. @@ -1115,7 +1115,7 @@ exists tr0; split. - exact: hp _ h0 _ h3. - have h4 := followsT_setoidT (@singletonT_setoidT _) h2 h3 (bisim_refl _) => {h2}. exact: followsT_dupT b h4. -Qed. +Qed.*) (** ** Midpoint property *) From f58e6a24a818785a56e10e24b69475f4e55e19c5 Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Wed, 3 Aug 2022 13:50:23 +0300 Subject: [PATCH 17/18] Removing the lemmas from the previous commits (and uncommenting the ones in files) --- theories/VLSM/Lib/FinExtras.v | 7 - theories/VLSM/Lib/FinSetExtras.v | 8 - theories/VLSM/Lib/ListExtras.v | 554 +------------------ theories/VLSM/Lib/ListSetExtras.v | 206 +------ theories/VLSM/Lib/RealsExtras.v | 46 -- theories/VLSM/Lib/SortedLists.v | 67 --- theories/VLSM/Lib/SsrExport.v | 2 +- theories/VLSM/Lib/StdppExtras.v | 114 +--- theories/VLSM/Lib/StreamExtras.v | 207 ------- theories/VLSM/Lib/StreamFilters.v | 89 --- theories/VLSM/Lib/Temporal.v | 13 - theories/VLSM/Lib/TopSort.v | 78 --- theories/VLSM/Lib/TraceClassicalProperties.v | 12 +- theories/VLSM/Lib/TraceProperties.v | 276 ++++----- 14 files changed, 163 insertions(+), 1516 deletions(-) diff --git a/theories/VLSM/Lib/FinExtras.v b/theories/VLSM/Lib/FinExtras.v index 9ef45560..519a1aad 100644 --- a/theories/VLSM/Lib/FinExtras.v +++ b/theories/VLSM/Lib/FinExtras.v @@ -11,13 +11,6 @@ Fixpoint up_to_n_listing | S n' => n' :: up_to_n_listing n' end. -(*Lemma up_to_n_listing_length - (n : nat) - : length (up_to_n_listing n) = n. -Proof. - induction n; simpl; congruence. -Qed.*) - Lemma up_to_n_full (n : nat) : forall i, i < n <-> i ∈ up_to_n_listing n. diff --git a/theories/VLSM/Lib/FinSetExtras.v b/theories/VLSM/Lib/FinSetExtras.v index cbddce77..0f133359 100644 --- a/theories/VLSM/Lib/FinSetExtras.v +++ b/theories/VLSM/Lib/FinSetExtras.v @@ -58,14 +58,6 @@ Proof. lia. Qed. -(*Lemma intersection_size1 - (X Y : C) : - size (X ∩ Y) <= size X. -Proof. - apply (subseteq_size (X ∩ Y) X). - set_solver. -Qed.*) - Lemma intersection_size2 (X Y : C) : size (X ∩ Y) <= size Y. diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v index 44536cb8..55fb89f3 100644 --- a/theories/VLSM/Lib/ListExtras.v +++ b/theories/VLSM/Lib/ListExtras.v @@ -6,13 +6,6 @@ From VLSM Require Import Lib.Preamble. (** * Utility lemmas about lists *) (** A list is empty if it has no members *) -(*Lemma empty_nil [X:Type] (l:list X) : - (forall v, ~In v l) -> l = []. -Proof. - clear. - destruct l as [| a]; [done |]. - simpl. intro H. elim (H a). by left. -Qed.*) (** It is decidable whether a list is null or not *) Lemma null_dec {S} (l : list S) : Decision (l = []). @@ -59,14 +52,6 @@ Proof. by induction tl as [| hd tl IHl]. Qed. -(*Lemma remove_hd_last {X} : - forall (hd1 hd2 d1 d2 : X) (tl : list X), - List.last (hd1 :: hd2 :: tl) d1 = List.last (hd2 :: tl) d2. -Proof. - intros. induction tl; [done |]. - cbn in *. by destruct tl. -Qed.*) - Lemma unroll_last {S} : forall (random a : S) (l : list S), List.last (a :: l) random = List.last l a. Proof. @@ -108,24 +93,6 @@ Proof. by destruct l; [|inversion Herr; apply unroll_last]. Qed. -(*Lemma incl_empty : forall A (l : list A), - incl l nil -> l = nil. -Proof. - intros A [] H; [done |]. - by destruct (H a); left. -Qed.*) - -(*Lemma incl_singleton {A} : forall (l : list A) (a : A), - incl l [a] -> - forall b, In b l -> b = a. -Proof. - intros. induction l; inversion H0; subst. - - destruct (H b); [by left | done | inversion H1]. - - apply IHl; [| done]. - apply incl_tran with (a0 :: l); [| done]. - apply incl_tl. apply incl_refl. -Qed.*) - Lemma Exists_first {A : Type} (l : list A) @@ -205,42 +172,12 @@ Proof. by split; intros Hincl x Hx; apply in_correct; apply Hincl. Qed. -(*Definition incl_correct `{EqDecision A} - (l1 l2 : list A) - : incl l1 l2 <-> inclb l1 l2 = true - := incl_function l1 l2.*) - -(*Lemma map_incl {A B} (f : B -> A) : forall s s', - incl s s' -> - incl (map f s) (map f s'). -Proof. - intros s s' Hincl fx Hin. - apply in_map_iff . - apply in_map_iff in Hin as (x & Heq & Hin). eauto. -Qed.*) - Definition app_cons {A} (a : A) (l : list A) : [a] ++ l = a :: l := eq_refl. -(*Lemma append_nodup_left {A}: - forall (l1 l2 : list A), List.NoDup (l1 ++ l2) -> List.NoDup l1. -Proof. - induction l1; intros. - - constructor. - - inversion H. apply IHl1 in H3. constructor; [| done]. - rewrite in_app_iff in H2. itauto. -Qed.*) - -(*Lemma append_nodup_right {A}: - forall (l1 l2 : list A), List.NoDup (l1 ++ l2) -> List.NoDup l2. -Proof. - induction l1; cbn; intros; [done |]. - inversion H. auto. -Qed.*) - Lemma last_is_last {A} : forall (l : list A) (x dummy: A), List.last (l ++ [x]) dummy = x. Proof. @@ -267,12 +204,6 @@ Fixpoint is_member {W} `{StrictlyComparable W} (w : W) (l : list W) : bool := end end. -(*Definition compareb {A} `{StrictlyComparable A} (a1 a2 : A) : bool := - match compare a1 a2 with - | Eq => true - | _ => false - end.*) - Lemma is_member_correct {W} `{StrictlyComparable W} : forall l (w : W), is_member w l = true <-> In w l. Proof. @@ -285,22 +216,6 @@ Proof. + rewrite <- compare_eq. rewrite <- compare_asymmetric in Hcmp. itauto congruence. Qed. -(*Lemma is_member_correct' {W} `{StrictlyComparable W} - : forall l (w : W), is_member w l = false <-> ~ In w l. -Proof. - intros. - apply mirror_reflect. - intros; apply is_member_correct. -Qed.*) - -(*Lemma In_app_comm {X} : forall l1 l2 (x : X), In x (l1 ++ l2) <-> In x (l2 ++ l1). -Proof. - intros l1 l2 x; split; intro H_in; - apply in_or_app; apply in_app_or in H_in; - destruct H_in as [cat | dog]; - itauto. -Qed.*) - Lemma nth_error_last {A : Type} (l : list A) @@ -354,39 +269,6 @@ Fixpoint list_prefix | S n, a :: l => a :: list_prefix l n end. -(*Lemma list_prefix_split - {A : Type} - (l left right: list A) - (left_len : nat) - (Hlen : left_len = length left) - (Hsplit : l = left ++ right) : - list_prefix l left_len = left. -Proof. - generalize dependent l. - generalize dependent left. - generalize dependent right. - generalize dependent left_len. - induction left_len. - - intros. - symmetry in Hlen. - rewrite length_zero_iff_nil in Hlen. - rewrite Hlen. - unfold list_prefix. - by destruct l. - - intros. - destruct left; [done |]. - assert (left_len = length left). - { - simpl in Hlen. - inversion Hlen. - itauto. - } - specialize (IHleft_len right left H (left ++ right) eq_refl). - rewrite Hsplit. - simpl. - by rewrite IHleft_len. -Qed.*) - Lemma list_prefix_map {A B : Type} (f : A -> B) @@ -528,25 +410,6 @@ Proof. by apply dsig_eq. Qed. -(*Lemma list_annotate_eq - {A : Type} - (P : A -> Prop) - {Pdec : forall a, Decision (P a)} - (l1 : list A) - (Hl1 : Forall P l1) - (l2 : list A) - (Hl2 : Forall P l2) - : list_annotate P l1 Hl1 = list_annotate P l2 Hl2 <-> l1 = l2. -Proof. - split; [|intro; subst; apply list_annotate_pi]. - revert Hl1 l2 Hl2. - induction l1; destruct l2; simpl; intros. - 1-3: done. - inversion H. - apply IHl1 in H2. - by subst. -Qed.*) - Lemma list_annotate_unroll {A : Type} (P : A -> Prop) @@ -557,40 +420,6 @@ Lemma list_annotate_unroll : list_annotate P (a :: l) Hs = dexist a (Forall_hd Hs) :: list_annotate P l (Forall_tl Hs). Proof. done. Qed. -(*Lemma list_annotate_app - {A : Type} - (P : A -> Prop) - {Pdec : forall a, Decision (P a)} - (l1 l2 : list A) - (Hs : Forall P (l1 ++ l2)) - : list_annotate P (l1 ++ l2) Hs = list_annotate P l1 (proj1 (proj1 (@Forall_app _ P l1 l2) Hs)) ++ list_annotate P l2 (proj2 (proj1 (@Forall_app _ P l1 l2) Hs)). -Proof. - induction l1; [apply list_annotate_pi|]. - simpl. f_equal. - - by apply dsig_eq. - - rewrite IHl1. f_equal; apply list_annotate_pi. -Qed.*) - -(*Lemma nth_error_list_annotate - {A : Type} - (P : A -> Prop) - (Pdec : forall a, Decision (P a)) - (l : list A) - (Hs : Forall P l) - (n : nat) - : exists (oa : option (dsig P)), - nth_error (list_annotate P l Hs) n = oa - /\ option_map (@proj1_sig _ _) oa = nth_error l n. -Proof. - generalize dependent l. - induction n; intros [| a l] Hs. - - by exists None. - - inversion Hs; subst. exists (Some (dexist a (Forall_hd Hs))). - by rewrite list_annotate_unroll. - - by exists None. - - rewrite list_annotate_unroll; eauto. -Qed.*) - Fixpoint nth_error_filter_index {A} P `{∀ (x:A), Decision (P x)} (l : list A) @@ -608,52 +437,6 @@ Fixpoint nth_error_filter_index option_map S (nth_error_filter_index P l n) end. -(*Lemma nth_error_filter_index_le - {A} P `{∀ (x:A), Decision (P x)} - (l : list A) - (n1 n2 : nat) - (Hle : n1 <= n2) - (in1 in2 : nat) - (Hin1 : nth_error_filter_index P l n1 = Some in1) - (Hin2 : nth_error_filter_index P l n2 = Some in2) - : in1 <= in2. -Proof. - generalize dependent in2. - generalize dependent in1. - generalize dependent n2. - generalize dependent n1. - induction l; intros. - - inversion Hin1. - - simpl in Hin1. simpl in Hin2. - destruct (decide (P a)). - + destruct n1; destruct n2. - * by inversion Hin1; inversion Hin2; subst. - * destruct (nth_error_filter_index P l n2) - ; inversion Hin1; inversion Hin2; subst. - lia. - * inversion Hle. - * { destruct in1, in2. - - lia. - - lia. - - destruct (nth_error_filter_index P l n2); inversion Hin2. - - assert (Hle' : n1 <= n2) by lia. - specialize (IHl n1 n2 Hle'). - destruct (nth_error_filter_index P l n1) eqn:Hin1'; inversion Hin1; - subst; clear Hin1. - destruct (nth_error_filter_index P l n2) eqn:Hin2'; inversion Hin2 - ; subst; clear Hin2. - specialize (IHl in1 eq_refl in2 eq_refl). - lia. - } - + specialize (IHl n1 n2 Hle). - destruct (nth_error_filter_index P l n1) eqn:Hin1'; inversion Hin1 - ; subst; clear Hin1. - destruct (nth_error_filter_index P l n2) eqn:Hin2'; inversion Hin2 - ; subst; clear Hin2. - specialize (IHl n0 eq_refl n3 eq_refl). - lia. -Qed.*) - Fixpoint Forall_filter {A : Type} (P : A -> Prop) @@ -818,93 +601,6 @@ Proof. - by rewrite unroll_last, unroll_last. Qed. -(*Lemma list_suffix_last_default - {A : Type} - (l : list A) - (i : nat) - (Hlast : i = length l) - (_default : A) - : List.last (list_suffix l i) _default = _default. -Proof. - revert l Hlast. induction i; intros [|a l] Hlast; try done. - apply IHi. by inversion Hlast. -Qed.*) - -(*Lemma list_segment_nth - {A : Type} - (l : list A) - (n1 n2 : nat) - (Hn : n1 <= n2) - (i : nat) - (Hi1 : n1 <= i) - (Hi2 : i < n2) - : nth_error (list_segment l n1 n2) (i - n1) = nth_error l i. -Proof. - unfold list_segment. - rewrite list_suffix_nth; [| done]. - by apply list_prefix_nth. -Qed.*) - -(*Lemma list_segment_app - {A : Type} - (l : list A) - (n1 n2 n3 : nat) - (H12 : n1 <= n2) - (H23 : n2 <= n3) - : list_segment l n1 n2 ++ list_segment l n2 n3 = list_segment l n1 n3. -Proof. - assert (Hle : n1 <= n3) by lia. - specialize (list_prefix_segment_suffix l n1 n3 Hle); intro Hl1. - specialize (list_prefix_segment_suffix l n2 n3 H23); intro Hl2. - rewrite <- Hl2 in Hl1 at 4. clear Hl2. - repeat rewrite app_assoc in Hl1. - apply app_inv_tail in Hl1. - specialize (list_prefix_suffix (list_prefix l n2) n1); intro Hl2. - specialize (list_prefix_prefix l n1 n2 H12); intro Hl3. - rewrite Hl3 in Hl2. - rewrite <- Hl2 in Hl1. - rewrite <- app_assoc in Hl1. - by apply app_inv_head in Hl1. -Qed.*) - -(*Lemma list_segment_singleton - {A : Type} - (l : list A) - (n : nat) - (a : A) - (Hnth : nth_error l n = Some a) - : list_segment l n (S n) = [a]. -Proof. - unfold list_segment. - assert (Hle : S n <= length l) - by (apply nth_error_length in Hnth; done). - assert (Hlt : n < length (list_prefix l (S n))) - by (rewrite list_prefix_length; try constructor; done). - specialize (list_suffix_last (list_prefix l (S n)) n Hlt a); intro Hlast1. - specialize (list_prefix_nth_last l n a Hnth a); intro Hlast2. - rewrite <- Hlast2 in Hlast1. - specialize (list_suffix_length (list_prefix l (S n)) n). - rewrite list_prefix_length; [| done]. - intro Hlength. - assert (Hs: S n - n = 1) by lia. - rewrite Hs in Hlength. - remember (list_suffix (list_prefix l (S n)) n) as x. - clear -Hlength Hlast1. - destruct x; inversion Hlength. - destruct x; inversion H0. - by simpl in Hlast1; subst. -Qed.*) - -(*Lemma nth_error_map - {A B : Type} - (f : A -> B) - (l : list A) - (n : nat) - : nth_error (List.map f l) n = option_map f (nth_error l n). -Proof. - revert n. induction l; intros [| n]; firstorder. -Qed.*) - Lemma exists_finite `{finite.Finite index} (P : index -> Prop) @@ -1019,17 +715,8 @@ Qed. Definition cat_option {A : Type} : list (option A) -> list A := @map_option (option A) A id. -(*Example cat_option1 : cat_option [Some 1; Some 5; None; Some 6; None] = [1; 5; 6]. -Proof. itauto. Qed.*) - -(*Lemma cat_option_length - {A : Type} - (l : list (option A)) - (Hfl : Forall (fun a => a <> None) l) - : length (cat_option l) = length l. -Proof. - apply map_option_length; itauto. -Qed.*) +Example cat_option1 : cat_option [Some 1; Some 5; None; Some 6; None] = [1; 5; 6]. +Proof. itauto. Qed. Lemma cat_option_length_le {A : Type} @@ -1042,33 +729,6 @@ Proof. destruct (id a) eqn : eq_id; simpl in *; subst a; simpl; lia. Qed. -(*Lemma cat_option_app - {A : Type} - (l1 l2 : list (option A)) : - cat_option (l1 ++ l2) = cat_option l1 ++ cat_option l2. -Proof. - induction l1. - - simpl in *. itauto. - - by destruct a; cbn in *; rewrite IHl1. -Qed.*) - -(*Lemma cat_option_nth - {A : Type} - (l : list (option A)) - (Hfl : Forall (fun a => a <> None) l) - (n := length l) - (i : nat) - (Hi : i < n) - (dummya : A) - : Some (nth i (cat_option l) dummya) = (nth i l (Some dummya)). -Proof. - specialize (@map_option_nth (option A) A id l). simpl in *. - intros. - unfold id in *. - apply H. - all : itauto. -Qed.*) - Lemma nth_error_eq {A : Type} (l1 l2 : list A) @@ -1088,41 +748,6 @@ Proof. Qed. (* TODO remove (we have Exists_first) *) -(*Lemma exists_first - {A : Type} - (l : list A) - (P : A -> Prop) - (Pdec : forall a : A, {P a } + {~P a}) - (Hsomething : Exists P l) : - exists (prefix : list A) - (suffix : list A) - (first : A), - (P first) /\ - l = prefix ++ [first] ++ suffix /\ - ~Exists P prefix. -Proof. - induction l. - - inversion Hsomething. - - destruct (Pdec a). - + exists [], l, a. rewrite Exists_nil. itauto. - + assert (Hl : Exists P l) by (inversion Hsomething; subst; done). - specialize (IHl Hl). - destruct IHl as [prefix [suffix [first [Hfirst [Heq Hprefix]]]]]. - exists (a :: prefix), suffix, first. split_and!; subst; [done | done |]. - by inversion 1; subst. -Qed.*) - -(*Lemma in_fast - {A : Type} - (l : list A) - (a : A) - (b : A) - (Hin : In a (b :: l)) - (Hneq : b <> a) : - In a l. -Proof. - by destruct Hin. -Qed.*) Fixpoint one_element_decompositions {A : Type} @@ -1192,52 +817,6 @@ Definition two_element_decompositions ) (one_element_decompositions l). -(*Lemma in_two_element_decompositions_iff - {A : Type} - (l : list A) - (pre mid suf : list A) - (x y : A) - : In (pre, x, mid, y, suf) (two_element_decompositions l) - <-> pre ++ [x] ++ mid ++ [y] ++ suf = l. -Proof. - unfold two_element_decompositions. - rewrite in_flat_map. - split. - - intros [((pre', x'), sufx) [Hdecx Hin]]. - apply in_map_iff in Hin. - destruct Hin as [((mid', y'), suf') [Hdec Hin]]. - inversion Hdec. subst. clear Hdec. - apply in_one_element_decompositions_iff in Hdecx. - apply in_one_element_decompositions_iff in Hin. - by subst. - - remember (mid ++ [y] ++ suf) as sufx. - intro H. - exists (pre, x, sufx). apply in_one_element_decompositions_iff in H. - split; [done |]. - apply in_map_iff. exists (mid, y, suf). - by rewrite in_one_element_decompositions_iff. -Qed.*) - -(*Lemma order_decompositions - {A : Type} - (pre1 suf1 pre2 suf2 : list A) - (Heq : pre1 ++ suf1 = pre2 ++ suf2) - : pre1 = pre2 - \/ (exists suf1', pre1 = pre2 ++ suf1') - \/ (exists suf2', pre2 = pre1 ++ suf2'). -Proof. - remember (pre1 ++ suf1) as l. - revert pre1 suf1 pre2 suf2 Heql Heq. - induction l; intros. - - left. symmetry in Heql, Heq. - by apply app_nil in Heql as [-> ->], Heq as [-> ->]. - - destruct pre1 as [| a1 pre1]; destruct pre2 as [|a2 pre2]. 1-3: eauto. - inversion Heql; subst a1; clear Heql. - inversion Heq; subst a2; clear Heq. - destruct (IHl pre1 suf1 pre2 suf2 H1 H2) - as [Heq | [[suf1' Hgt] | [suf2' Hlt]]]; subst; eauto. -Qed.*) - Lemma list_max_exists (l : list nat) (nz : list_max l > 0) : @@ -1253,23 +832,6 @@ Proof. by rewrite H; left. Qed. -(*Lemma list_max_exists2 - (l : list nat) - (Hne : l <> []) : - In (list_max l) l. -Proof. - destruct (list_max l) eqn : eq_max. - - destruct l;[itauto congruence|]. - specialize (list_max_le (n :: l) 0) as Hle. - destruct Hle as [Hle _]. - rewrite eq_max in Hle. spec Hle. apply Nat.le_refl. - rewrite Forall_forall in Hle. - specialize (Hle n). spec Hle; [left |]. - simpl. lia. - - specialize (list_max_exists l) as Hmax. - spec Hmax. lia. rewrite <- eq_max. itauto. -Qed.*) - (* Returns all values which occur with maximum frequency in the given list. Note that these values are returned with their original multiplicity. *) @@ -1279,8 +841,8 @@ Definition mode let mode_value := list_max (List.map (count_occ decide_eq l) l) in filter (fun a => (count_occ decide_eq l a) = mode_value) l. -(*Example mode1 : mode [1; 1; 2; 3; 3] = [1; 1; 3; 3]. -Proof. itauto. Qed.*) +Example mode1 : mode [1; 1; 2; 3; 3] = [1; 1; 3; 3]. +Proof. itauto. Qed. (* Computes the list suff which satisfies <> or reports that no such list exists. *) @@ -1301,10 +863,10 @@ Fixpoint complete_prefix end end. -(*Example complete_prefix_some : complete_prefix [1;2;3;4] [1;2] = Some [3;4]. -Proof. itauto. Qed.*) -(*Example complete_prefix_none : complete_prefix [1;2;3;4] [1;3] = None. -Proof. itauto. Qed.*) +Example complete_prefix_some : complete_prefix [1;2;3;4] [1;2] = Some [3;4]. +Proof. itauto. Qed. +Example complete_prefix_none : complete_prefix [1;2;3;4] [1;3] = None. +Proof. itauto. Qed. Lemma complete_prefix_empty `{EqDecision A} @@ -1365,8 +927,8 @@ Definition complete_suffix | Some ls => Some (rev ls) end. -(*Example complete_suffix_some : complete_suffix [1;2;3;4] [3;4] = Some [1;2]. -Proof. itauto. Qed.*) +Example complete_suffix_some : complete_suffix [1;2;3;4] [3;4] = Some [1;2]. +Proof. itauto. Qed. Lemma complete_suffix_correct `{EqDecision A} @@ -1422,13 +984,6 @@ Definition list_sum_project_right := map_option sum_project_right x. -(*Lemma fold_right_andb_false l: - fold_right andb false l = false. -Proof. - induction l; [done |]. - simpl. rewrite IHl. apply andb_false_r. -Qed.*) - Definition Listing_finite_transparent `{EqDecision A} {l : list A} (finite_l : Listing l) : finite.Finite A. Proof. exists l. @@ -1521,62 +1076,17 @@ Inductive ForAllSuffix : list A -> Prop := | SNil : P [] -> ForAllSuffix [] | SHereAndFurther : forall a l, P (a :: l) -> ForAllSuffix l -> ForAllSuffix (a :: l). -(*Lemma fsHere : forall l, ForAllSuffix l -> P l. -Proof. by inversion 1. Qed.*) - Lemma fsFurther : forall a l, ForAllSuffix (a :: l) -> ForAllSuffix l. Proof. by inversion 1. Qed. -(*Lemma ForAll_list_suffix : forall m x, ForAllSuffix x -> ForAllSuffix (list_suffix x m). -Proof. - induction m; simpl; intros [] **. 1-3: done. - by apply fsFurther in H; apply IHm. -Qed.*) - -(*Lemma ForAllSuffix_induction - (Inv : list A -> Prop) - (InvThenP : forall l, Inv l -> P l) - (InvIsStable : forall a l, Inv (a :: l) -> Inv l) - : forall l, Inv l -> ForAllSuffix l. -Proof. - induction l; intros. - - by constructor; apply InvThenP. - - constructor. - + by apply InvThenP. - + by eapply IHl, InvIsStable. -Qed.*) - End suffix_quantifiers. -(*Lemma ForAllSuffix_subsumption [A : Type] (P Q : list A -> Prop) - (HPQ : forall l, P l -> Q l) - : forall l, ForAllSuffix P l -> ForAllSuffix Q l. -Proof. - induction 1; constructor; auto. -Qed.*) - Definition ForAllSuffix1 [A : Type] (P : A -> Prop) : list A -> Prop := ForAllSuffix (fun l => match l with | [] => True | a :: _ => P a end). -(*Lemma ForAllSuffix1_Forall [A : Type] (P : A -> Prop) - : forall l, ForAllSuffix1 P l <-> Forall P l. -Proof. - split; induction 1; constructor; auto. -Qed.*) - Definition ExistsSuffix1 [A : Type] (P : A -> Prop) : list A -> Prop := ExistsSuffix (fun l => match l with | [] => False | a :: _ => P a end). -(*Lemma ExistsSuffix1_Exists [A : Type] (P : A -> Prop) - : forall l, ExistsSuffix1 P l <-> Exists P l. -Proof. - split; induction 1. - - by destruct l; [| left]. - - by right. - - by left. - - by right. -Qed.*) - Definition ForAllSuffix2 [A : Type] (R : A -> A -> Prop) : list A -> Prop := ForAllSuffix (fun l => match l with | a :: b :: _ => R a b | _ => True end). @@ -1607,13 +1117,6 @@ Proof. - apply IHl. by eapply fsFurther2_transitive. Qed. -(*Lemma list_subseteq_tran : forall (A : Type) (l m n : list A), - l ⊆ m → m ⊆ n → l ⊆ n. -Proof. - intros A l m n Hlm Hmn x y. - by apply Hmn, Hlm. -Qed.*) - #[global] Instance list_subseteq_dec `{EqDecision A} : RelDecision (@subseteq (list A) _). Proof. intros x. @@ -1701,12 +1204,6 @@ Proof. Qed. (** If <> is zero, then the result of [lastn] is [[]]. *) -(*Lemma lastn_0 : - forall {A : Type} (l : list A), - lastn 0 l = []. -Proof. - by intros A l; unfold lastn; rewrite take_0. -Qed.*) (** If <> is greater than the length of the list, [lastn] returns the whole list. *) Lemma lastn_ge : @@ -1754,34 +1251,8 @@ Qed. (** If <> is less than (or equal to) <>, then <> is shorter than <> and therefore is its suffix. *) -(*Lemma suffix_lastn : - forall {A : Type} (l : list A) (n1 n2 : nat), - n1 <= n2 -> suffix (lastn n1 l) (lastn n2 l). -Proof. - intros A l n1 n2 Hle. - unfold lastn. - apply suffix_rev. - exists (take (n2 - n1) (drop n1 (rev l))). - rewrite take_take_drop. - by f_equal; lia. -Qed.*) (** The length of <> is the smaller of <> and the length of <>. *) -(*Lemma length_lastn : - forall {A : Type} (n : nat) (l : list A), - length (lastn n l) = min n (length l). -Proof. - intros A n l. - unfold lastn. - by rewrite rev_length, take_length, rev_length. -Qed.*) - -(*Program Definition not_null_element - `{EqDecision A} [l : list A] (Hl : l <> []) : dsig (fun i => i ∈ l) := - dexist (is_Some_proj (proj2 (head_is_Some l) Hl)) _. -Next Obligation. - by intros A ? [| h t] ?; [| left]. -Qed.*) Program Definition element_of_subseteq `{EqDecision A} [l1 l2 : list A] (Hsub : l1 ⊆ l2) @@ -1790,8 +1261,3 @@ Program Definition element_of_subseteq Next Obligation. by intros; cbn; destruct_dec_sig di i Hi Heq; subst; apply Hsub. Qed. - -(*Definition element_of_filter - `{EqDecision A} [P : A -> Prop] `{∀ x, Decision (P x)} [l : list A] - : dsig (fun i => i ∈ filter P l) -> dsig (fun i => i ∈ l) := - element_of_subseteq (list_filter_subseteq P l).*) diff --git a/theories/VLSM/Lib/ListSetExtras.v b/theories/VLSM/Lib/ListSetExtras.v index 1d41b907..79bbc7d3 100644 --- a/theories/VLSM/Lib/ListSetExtras.v +++ b/theories/VLSM/Lib/ListSetExtras.v @@ -27,13 +27,6 @@ Proof. by intros s1 s2 []. Qed. -(*Lemma set_eq_proj2 {A} : forall (s1 s2 : set A), - set_eq s1 s2 -> - s2 ⊆ s1. -Proof. - by intros s1 s2 []. -Qed.*) - Lemma set_eq_refl {A} : forall (s : list A), set_eq s s. Proof. by induction s. @@ -76,31 +69,12 @@ Proof. firstorder. Qed. -(*Lemma set_eq_Forall - {A : Type} - (s1 s2 : set A) - (H12 : set_eq s1 s2) - (P : A -> Prop) - : Forall P s1 <-> Forall P s2. -Proof. - rewrite !Forall_forall. firstorder. -Qed.*) - Lemma set_union_comm `{EqDecision A} : forall (s1 s2 : list A), set_eq (set_union s1 s2) (set_union s2 s1). Proof. intros s1 s2; split; intro x; rewrite !set_union_iff; itauto. Qed. -(*Lemma set_union_empty `{EqDecision A} : forall (s1 s2 : list A), - set_union s1 s2 = [] -> - s1 = [] /\ s2 = []. -Proof. - intros. - destruct s2; [done |]. - by cbn in H; apply set_add_not_empty in H. -Qed.*) - Lemma set_union_nodup_left `{EqDecision A} (l l' : set A) : NoDup l -> NoDup (set_union l l'). Proof. @@ -169,34 +143,6 @@ Proof. + right. apply IHss. by exists x. Qed. -(*Lemma set_union_iterated_subseteq - `{EqDecision A} - (ss ss': list (set A)) - (Hincl : ss ⊆ ss') : - (fold_right set_union [] ss) ⊆ - (fold_right set_union [] ss'). -Proof. - intros a H. - apply set_union_in_iterated in H. - apply set_union_in_iterated. - rewrite Exists_exists in *. - destruct H as [x [Hx Ha]]. - exists x. - unfold incl in Hincl. - split; [| done]. - by apply Hincl. -Qed.*) - -(*Lemma set_union_empty_left `{EqDecision A} : forall (s : list A), - NoDup s -> set_eq (set_union [] s) s. -Proof. - intros. split; intros x Hin. - - apply set_union_elim in Hin. destruct Hin. - + inversion H0. - + done. - - by apply set_union_intro; right. -Qed.*) - Lemma map_list_subseteq {A B} : forall (f : B -> A) (s s' : list B), s ⊆ s' -> (map f s) ⊆ (map f s'). Proof. @@ -278,25 +224,6 @@ Proof. by split; destruct H; apply set_map_subseteq. Qed. -(*Lemma set_map_singleton {A B} `{EqDecision A} (f : B -> A) : forall s a, - set_map f s = [a] -> - forall b, b ∈ s -> f b = a. -Proof. - intros. apply (set_map_elem_of f) in H0. rewrite H in H0. apply elem_of_cons in H0. - destruct H0; [done | inversion H0]. -Qed.*) - -(*Lemma filter_set_add `{StrictlyComparable X} P - `{∀ (x:X), Decision (P x)} : - forall (l:list X) x, ~ P x -> - filter P l = filter P (set_add x l). -Proof. - induction l as [|hd tl IHl]; intros x H_false; cbn. - - by rewrite decide_False. - - destruct (decide (x = hd)); cbn; [done |]. - by destruct (decide (P hd)); rewrite <- (IHl). -Qed.*) - Lemma set_add_ignore `{StrictlyComparable X} : forall (l : list X) (x : X), x ∈ l -> @@ -307,25 +234,6 @@ Proof. - rewrite IHl; [| done]. by destruct (decide (x = hd)). Qed. -(*Lemma set_add_new `{EqDecision A}: - forall (x:A) l, ~x ∈ l -> set_add x l = l++[x]. -Proof. - induction l; cbn; [done |]; intros H_not_in. - rewrite decide_False; cycle 1. - - by intros ->; apply H_not_in; left. - - rewrite elem_of_cons in H_not_in. rewrite IHl; itauto. -Qed.*) - -(*Lemma set_remove_not_elem_of `{EqDecision A} : forall x (s : list A), - ~ x ∈ s -> - set_remove x s = s. -Proof. - induction s; cbn; intros; [done |]. - rewrite decide_False; cycle 1. - + by intros ->; contradict H; left. - + rewrite IHs; [done |]. rewrite elem_of_cons in H. itauto. -Qed.*) - Lemma set_remove_elim `{EqDecision A} : forall x (s : list A), NoDup s -> ~ x ∈ (set_remove x s). Proof. @@ -338,26 +246,6 @@ Proof. by intros x y s ->; cbn; rewrite decide_True. Qed. -(*Lemma set_remove_nodup_1 `{EqDecision A} : forall x (s : list A), - NoDup (set_remove x s) -> - ~ x ∈ (set_remove x s) -> - NoDup s. -Proof. - induction s; intros. - - constructor. - - simpl in H0 . destruct (decide (x = a)). - + cbn in H; subst. constructor; [done |]. by rewrite decide_True in H. - + rewrite elem_of_cons in H0. - simpl in H. - rewrite decide_False in H; auto. - inversion H; subst. - constructor. - * intro Ha; apply (set_remove_3 _ x) in Ha; auto. - * apply IHs; [done |]. - intro Hx. - by contradict H0; right. -Qed.*) - Lemma set_remove_elem_of_iff `{EqDecision A} : forall x y (s : list A), NoDup s -> y ∈ s -> @@ -409,18 +297,6 @@ Proof. split; intros a Hin; rewrite set_remove_iff in *; itauto. Qed. -(*Lemma subseteq_remove_union `{EqDecision A} : forall x (s1 s2 : list A), - NoDup s1 -> - NoDup s2 -> - (set_remove x (set_union s1 s2)) ⊆ - (set_union s1 (set_remove x s2)). -Proof. - intros. intros y Hin. apply set_remove_iff in Hin. - - apply set_union_intro. destruct Hin. apply set_union_elim in H1. - rewrite set_remove_iff; itauto. - - by apply set_union_nodup. -Qed.*) - Lemma set_eq_remove_union_elem_of `{EqDecision A} : forall x (s1 s2 : list A), NoDup s1 -> NoDup s2 -> @@ -463,15 +339,6 @@ Qed. for the second argument. *) (* TODO(palmskog): consider submitting a PR to Coq's stdlib. *) -(*Lemma set_diff_nodup' `{EqDecision A} (l l' : list A) - : NoDup l -> NoDup (set_diff l l'). -Proof. -induction 1 as [|x l H H' IH]; simpl. -- constructor. -- case_decide. - + by apply IH. - + by apply set_add_nodup, IH. -Qed.*) Lemma diff_app_nodup `{EqDecision A} : forall (s1 s2 : list A), NoDup s1 -> @@ -497,27 +364,17 @@ Proof. rewrite Heq, IHlv; itauto. Qed. -(*Lemma set_union_iterated_empty `{EqDecision A} : - forall ss : list (set A), - (forall s : list A, s ∈ ss -> s = []) -> fold_right set_union [] ss = []. -Proof. - induction ss; [done |]; cbn; intros H. - rewrite IHss; cycle 1. - - by intros s Hel; apply H; right. - - by cbn; apply H; left. -Qed.*) - (** For each element X of l1, exactly one occurrence of X is removed from l2. If no such occurrence exists, nothing happens. *) Definition set_remove_list `{EqDecision A} (l1 l2 : list A) : list A := fold_right set_remove l2 l1. -(*Example set_remove_list1 : set_remove_list [3;1;3] [1;1;2;3;3;3;3] = [1;2;3;3]. -Proof. done. Qed.*) +Example set_remove_list1 : set_remove_list [3;1;3] [1;1;2;3;3;3;3] = [1;2;3;3]. +Proof. done. Qed. -(*Example set_remove_list2 : set_remove_list [4] [1;2;3] = [1;2;3]. -Proof. done. Qed.*) +Example set_remove_list2 : set_remove_list [4] [1;2;3] = [1;2;3]. +Proof. done. Qed. Lemma set_remove_list_1 `{EqDecision A} @@ -533,26 +390,6 @@ Proof. by apply set_remove_1, IHl1 in Hin. Qed. -(*Lemma set_prod_nodup `(s1: set A) `(s2: set B): - NoDup s1 -> - NoDup s2 -> - NoDup (set_prod s1 s2). -Proof. - intros Hs1 HS2. - induction Hs1. - + constructor. - + simpl. - apply nodup_append. - * apply NoDup_fmap; [congruence | done]. - * done. - * intros [a b]. - rewrite elem_of_list_fmap, elem_of_list_prod. - intros [_ [[= <- _] _]]. itauto. - * intros [a b]. - rewrite elem_of_list_prod, elem_of_list_fmap. - intros [Ha _] [_ [[= Hax _] _]]. congruence. -Qed.*) - (** An alternative to [set_diff]. Unlike [set_diff], the result may contain duplicates if the first argument list <> does. @@ -569,27 +406,6 @@ Definition set_diff_filter `{EqDecision A} (l r : list A) := The characteristic membership property, parallel to [set_diff_iff]. *) -(*Lemma set_diff_filter_iff `{EqDecision A} (a:A) l r: - a ∈ (set_diff_filter l r) <-> (a ∈ l /\ ~a ∈ r). -Proof. - induction l;simpl. - - cbn. split; intros; [|itauto]. - inversion H. - - unfold set_diff_filter in *. - rewrite filter_cons. - destruct (decide (~ a0 ∈ r)). - * rewrite 2 elem_of_cons, IHl. - split; itauto congruence. - * rewrite elem_of_cons. - split;itauto congruence. -Qed.*) - -(*Lemma set_diff_filter_nodup `{EqDecision A} (l r:list A): - NoDup l -> NoDup (set_diff_filter l r). -Proof. - intros H. - by apply NoDup_filter. -Qed.*) (** Prove that subtracting a superset cannot produce @@ -682,20 +498,6 @@ Add Parametric Morphism A : (@elem_of_list A) with signature @eq A ==> @list_subseteq A ==> Basics.impl as set_elem_of_subseteq. Proof. firstorder. Qed. -(*Lemma set_union_iterated_preserves_prop - `{EqDecision A} - (ss : list (set A)) - (P : A -> Prop) - (Hp : forall (s : set A), forall (a : A), (s ∈ ss /\ a ∈ s) -> P a) : - forall (a : A), a ∈ (fold_right set_union [] ss) -> P a. -Proof. - intros. - apply set_union_in_iterated in H. rewrite Exists_exists in H. - destruct H as [s [Hins Hina]]. - apply Hp with (s := s). - itauto. -Qed.*) - Lemma filter_set_eq {X} P Q `{∀ (x:X), Decision (P x)} `{∀ (x:X), Decision (Q x)} (l : list X) diff --git a/theories/VLSM/Lib/RealsExtras.v b/theories/VLSM/Lib/RealsExtras.v index c16ebdb0..a966fedb 100644 --- a/theories/VLSM/Lib/RealsExtras.v +++ b/theories/VLSM/Lib/RealsExtras.v @@ -3,22 +3,6 @@ From stdpp Require Import prelude. (** * Real number utility lemmas *) -(** This lemma is needed in fault_weight_state_backwards **) -(*Lemma Rplusminus_assoc : forall r1 r2 r3, - (r1 + r2 - r3)%R = (r1 + (r2 - r3))%R. -Proof. - intros. unfold Rminus. - apply Rplus_assoc. -Qed.*) - -(** This lemma is needed in fault_weight_state_sorted_subset **) -(*Lemma Rplusminus_assoc_r : forall r1 r2 r3, - (r1 - r2 + r3)%R = (r1 + (- r2 + r3))%R. -Proof. - intros. unfold Rminus. - apply Rplus_assoc. -Qed.*) - (** This lemma is needed in fault_weight_state_sorted_subset **) Lemma Rplus_opp_l : forall r, (Ropp r + r)%R = 0%R. Proof. @@ -27,36 +11,6 @@ Proof. apply Rplus_opp_r. Qed. -(** This lemma is needed in fault_weight_state_sorted_subset **) -(*Lemma Rplus_ge_reg_neg_r : forall r1 r2 r3, - (r2 <= 0)%R -> (r3 <= r1 + r2)%R -> (r3 <= r1)%R. -Proof. - intros. - apply Rge_le. - apply Rle_ge in H. - apply Rle_ge in H0. - apply (Rplus_ge_reg_neg_r r1 r2 r3 H H0). -Qed.*) - -(** This lemma is needed in fault_weight_state_sorted_subset **) -(*Lemma Rminus_lt_r : forall r1 r2, - (0 <= r2)%R -> (r1 - r2 <= r1)%R. -Proof. - intros. - rewrite <- Rplus_0_r. - unfold Rminus. - by apply Rplus_le_compat_l, Rge_le, Ropp_0_le_ge_contravar. -Qed.*) - -(*Lemma Rminus_lt_r_strict : forall r1 r2, - (0 < r2)%R -> (r1 - r2 <= r1)%R. -Proof. - intros. - rewrite <- Rplus_0_r. - unfold Rminus. - by apply Rplus_le_compat_l, Rge_le, Ropp_0_le_ge_contravar, Rlt_le. -Qed.*) - Lemma Rtotal_le_gt : forall x y, (x <= y)%R \/ (x > y)%R. Proof. diff --git a/theories/VLSM/Lib/SortedLists.v b/theories/VLSM/Lib/SortedLists.v index 7b3d58d4..6adc3365 100644 --- a/theories/VLSM/Lib/SortedLists.v +++ b/theories/VLSM/Lib/SortedLists.v @@ -58,14 +58,6 @@ Fixpoint add_in_sorted_list_fn {A} (compare : A -> A -> comparison) (x : A) (l : end end. -(*Lemma add_in_sorted_list_no_empty {A} (compare : A -> A -> comparison) : forall msg sigma, - add_in_sorted_list_fn compare msg sigma <> []. -Proof. - unfold not. intros. destruct sigma; simpl in H. - - inversion H. - - destruct (compare msg a); inversion H. -Qed.*) - Lemma add_in_sorted_list_in {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} : forall msg msg' sigma, msg' ∈ (add_in_sorted_list_fn compare msg sigma) -> msg = msg' \/ msg' ∈ sigma. @@ -176,24 +168,6 @@ Proof. - do 2 inversion 1; subst; firstorder. Qed. -(*Lemma add_in_sorted_list_existing {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} : forall msg sigma, - LocallySorted (compare_lt compare) sigma -> - msg ∈ sigma -> - add_in_sorted_list_fn compare msg sigma = sigma. -Proof. - induction sigma; intros. - - inversion H1. - - rewrite elem_of_cons in H1. - destruct H1 as [Heq | Hin]. - + by subst; simpl; rewrite compare_eq_refl. - + apply LocallySorted_tl in H0 as LS. - spec IHsigma LS Hin. simpl. - destruct (compare msg a) eqn:Hcmp; try rewrite IHsigma. 1, 3: done. - apply (@LocallySorted_elem_of_lt _ _ compare_lt_strict_order msg a sigma H0) in Hin. - unfold compare_lt in Hin. apply compare_asymmetric in Hin. - rewrite Hin in Hcmp. inversion Hcmp. -Qed.*) - Lemma set_eq_first_equal {A} {lt : relation A} `{StrictOrder A lt} : forall x1 x2 s1 s2, LocallySorted lt (x1 :: s1) -> @@ -329,44 +303,3 @@ Proof. spec Hneed; [| done]. apply elem_of_app; right; left. Qed. - -(*Lemma lsorted_pair_wise_unordered - {A : Type} - (l : list A) - (R : A -> A -> Prop) - (Hsorted : LocallySorted R l) - (Htransitive : Transitive R) - (x y : A) - (Hin_x : x ∈ l) - (Hin_y : y ∈ l) : - x = y \/ R x y \/ R y x. -Proof. - apply elem_of_list_split in Hin_x. - destruct Hin_x as [pref1 [suf1 Hconcat1]]. - rewrite Hconcat1 in Hin_y. - apply elem_of_app in Hin_y. - rewrite elem_of_cons in Hin_y. - assert (y =x \/ y ∈ (pref1 ++ suf1)). { - destruct Hin_y as [Hin_y|Hin_y]; [|destruct Hin_y]. - - by right; apply elem_of_app; left. - - by left. - - by right; apply elem_of_app; right. - } - clear Hin_y. - rename H into Hin_y. - destruct Hin_y as [Hin_y|Hin_y]. - - symmetry in Hin_y. - itauto. - - apply elem_of_app in Hin_y; destruct Hin_y. - * apply elem_of_list_split in H. - destruct H as [pref2 [suf2 Hconcat2]]. - rewrite Hconcat2 in Hconcat1. - rewrite <- app_assoc in Hconcat1. - specialize (lsorted_pairwise_ordered l R Hsorted Htransitive y x pref2 suf2 suf1 Hconcat1). - by intros; right; right. - * apply elem_of_list_split in H. - destruct H as [pref2 [suf2 Hconcat2]]. - rewrite Hconcat2 in Hconcat1. - specialize (lsorted_pairwise_ordered l R Hsorted Htransitive x y pref1 pref2 suf2 Hconcat1). - by intros; right; left. -Qed.*) diff --git a/theories/VLSM/Lib/SsrExport.v b/theories/VLSM/Lib/SsrExport.v index d81fa57e..30ba8c57 100644 --- a/theories/VLSM/Lib/SsrExport.v +++ b/theories/VLSM/Lib/SsrExport.v @@ -4,4 +4,4 @@ From Coq Require Export ssreflect. #[export] Set SsrOldRewriteGoalsOrder. #[export] Set Asymmetric Patterns. #[export] Set Bullet Behavior "None". -(*Definition iYC2 := True.*) + diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v index 77857a8b..cb9f3483 100644 --- a/theories/VLSM/Lib/StdppExtras.v +++ b/theories/VLSM/Lib/StdppExtras.v @@ -145,25 +145,6 @@ Proof. by rewrite existsb_Exists, <- Forall_Exists_neg, Forall_forall. Qed. -(*Lemma existsb_first - {A : Type} - (l : list A) - (f : A -> bool) - (Hsomething : existsb f l = true) : - exists (prefix : list A) - (suffix : list A) - (first : A), - (f first = true) /\ - l = prefix ++ [first] ++ suffix /\ - (existsb f prefix = false). -Proof. - setoid_rewrite <-not_true_iff_false. - setoid_rewrite existsb_Exists. - apply Exists_first. - - typeclasses eauto. - - by apply existsb_Exists. -Qed.*) - (* Returns all elements X of l such that X does not compare less than any other element w.r.t to the precedes relation *) @@ -172,11 +153,11 @@ Definition maximal_elements_list : list A := filter (fun a => Forall (fun b => (~ precedes a b)) l) l. -(*Example maximal_elements_list1: maximal_elements_list Nat.lt [1; 4; 2; 4] = [4;4]. -Proof. itauto. Qed.*) +Example maximal_elements_list1: maximal_elements_list Nat.lt [1; 4; 2; 4] = [4;4]. +Proof. itauto. Qed. -(*Example maximal_elements_list2 : maximal_elements_list Nat.le [1; 4; 2; 4] = []. -Proof. itauto. Qed.*) +Example maximal_elements_list2 : maximal_elements_list Nat.le [1; 4; 2; 4] = []. +Proof. itauto. Qed. (** Returns all elements <> of a set <> such that <> does not compare less @@ -229,38 +210,6 @@ Proof. destruct (decide (P a)); destruct (decide (Q a)); itauto. Qed. -(*Lemma NoDup_elem_of_remove A (l l' : list A) a : - NoDup (l ++ a :: l') -> NoDup (l ++ l') /\ a ∉ (l ++ l'). -Proof. - intros Hnda. - apply NoDup_app in Hnda. - destruct Hnda as [Hnd [Ha Hnda]]. - apply NoDup_cons in Hnda. - setoid_rewrite elem_of_cons in Ha. - destruct Hnda as [Ha' Hnd']; split. - - by apply NoDup_app; firstorder. - - by rewrite elem_of_app; firstorder. -Qed.*) - -(*Lemma list_lookup_lt [A] (is : list A) : - forall i, is_Some (is !! i) -> - forall j, j < i -> is_Some (is !! j). -Proof. - intros; apply lookup_lt_is_Some. - by etransitivity; [| apply lookup_lt_is_Some]. -Qed.*) - -(*Lemma list_suffix_lookup - {A : Type} - (s : list A) - (n : nat) - (i : nat) - (Hi : n <= i) - : list_suffix s n !! (i - n) = s !! i. -Proof. - revert s n Hi; induction i; intros [| a s] [| n] Hi; cbn; try done; [| apply IHi]; lia. -Qed.*) - Lemma list_difference_singleton_not_in `{EqDecision A} : forall (l : list A) (a : A), a ∉ l -> list_difference l [a] = l. @@ -285,27 +234,6 @@ Proof. - by inversion 1; subst; [done |]; cbn; spec IHl; [| lia]. Qed. -(*Lemma longer_subseteq_has_dups `{EqDecision A} : - forall l1 l2 : list A, l1 ⊆ l2 -> length l1 > length l2 -> - exists (i1 i2 : nat) (a : A), i1 ≠ i2 ∧ l1 !! i1 = Some a /\ l1 !! i2 = Some a. -Proof. - induction l1; [inversion 2 |]. - intros l2 Hl12 Hlen12. - destruct (decide (a ∈ l1)). - - exists 0. - apply elem_of_list_lookup_1 in e as [i2 Hi2]. - by exists (S i2), a. - - edestruct (IHl1 (list_difference l2 [a])) - as (i1 & i2 & a' & Hi12 & Hli1 & Hli2); cycle 2. - + exists (S i1), (S i2), a'; cbn; itauto. - + intros x Hx. - rewrite elem_of_list_difference, elem_of_list_singleton. - by split; [apply Hl12; right | by contradict n; subst]. - + cbn in Hlen12. - assert (Ha : a ∈ l2) by (apply Hl12; left). - specialize (list_difference_singleton_length_in _ _ Ha) as Hlen'; lia. -Qed.*) - Lemma ForAllSuffix2_lookup [A : Type] (R : A -> A -> Prop) l : ForAllSuffix2 R l <-> forall n a b, l !! n = Some a -> l !! (S n) = Some b -> R a b. Proof. @@ -337,18 +265,6 @@ Proof. by transitivity c; [apply IHk | eapply Hall]. Qed. -(** If the <>-th element of <> is <>, then we can decompose long enough - suffixes of <> into <> and a suffix shorter by 1. *) -(*Lemma lastn_length_cons : - forall {A : Type} (n : nat) (l : list A) (x : A), - l !! n = Some x -> lastn (length l - n) l = x :: lastn (length l - S n) l. -Proof. - intros A n l x H. - unfold lastn. - rewrite <- rev_length, <- !skipn_rev, rev_involutive. - by apply drop_S. -Qed.*) - Lemma filter_in {A} P `{∀ (x:A), Decision (P x)} x s : In x s -> P x -> @@ -712,25 +628,3 @@ Proof. rewrite contra in H0. destruct H0; inversion H0. Qed. - -(** - When a list contains two elements, either they are equal or we can split - the list into three parts separated by the elements (and this can be done - in two ways, depending on the order of the elements). -*) -(*Lemma elem_of_list_split_2 : - forall {A : Type} (l : list A) (x y : A), - x ∈ l -> y ∈ l -> - x = y \/ exists l1 l2 l3 : list A, - l = l1 ++ x :: l2 ++ y :: l3 \/ l = l1 ++ y :: l2 ++ x :: l3. -Proof. - intros A x y l Hx Hy. - apply elem_of_list_split in Hx as (l1 & l2 & ->). - rewrite elem_of_app, elem_of_cons in Hy. - destruct Hy as [Hy | [-> | Hy]]; [| by left |]. - - apply elem_of_list_split in Hy as (l11 & l12 & ->). - right; exists l11, l12, l2; right; cbn. - by rewrite <- app_assoc. - - apply elem_of_list_split in Hy as (l21 & l22 & ->). - by right; exists l1, l21, l22; left; cbn. -Qed.*) diff --git a/theories/VLSM/Lib/StreamExtras.v b/theories/VLSM/Lib/StreamExtras.v index 35fd28dc..b3bfdbd0 100644 --- a/theories/VLSM/Lib/StreamExtras.v +++ b/theories/VLSM/Lib/StreamExtras.v @@ -49,14 +49,6 @@ Qed. Definition ForAll1 [A : Type] (P : A -> Prop) := ForAll (fun s => P (hd s)). -(*Lemma ForAll1_subsumption [A:Type] (P Q: A -> Prop) - (HPQ : forall a, P a -> Q a) - : forall s, ForAll1 P s -> ForAll1 Q s. -Proof. - apply ForAll_subsumption. - intro s. apply HPQ. -Qed.*) - Lemma ForAll1_forall [A : Type] (P : A -> Prop) s : ForAll1 P s <-> forall n, P (Str_nth n s). Proof. @@ -124,17 +116,6 @@ Proof. by induction l; cbn; f_equal. Qed. -(*Lemma stream_app_f_equal - {A : Type} - (l1 l2 : list A) - (s1 s2 : Stream A) - (Hl : l1 = l2) - (Hs : EqSt s1 s2) - : EqSt (stream_app l1 s1) (stream_app l2 s2). -Proof. - by subst; induction l2; [ | constructor]. -Qed.*) - Lemma stream_app_inj_l {A : Type} (l1 l2 : list A) @@ -248,35 +229,6 @@ Proof. right. apply IHn. exists k. split; [lia | done]. Qed. -(*Lemma stream_prefix_app_l - {A : Type} - (l : list A) - (s : Stream A) - (n : nat) - (Hle : n <= length l) - : stream_prefix (stream_app l s) n = list_prefix l n. -Proof. - revert n Hle; induction l; intros [| n] Hle. - 1-3: by inversion Hle. - by cbn in *; rewrite IHl; [| lia]. -Qed.*) - -(*Lemma stream_prefix_app_r - {A : Type} - (l : list A) - (s : Stream A) - (n : nat) - (Hge : n >= length l) - : stream_prefix (stream_app l s) n = l ++ stream_prefix s (n - length l). -Proof. - generalize dependent l. - generalize dependent s. - induction n. - - intros s [| a l] Hge; cbn in *; [done | lia]. - - intros s [| a l] Hge; cbn in *; [done |]. - rewrite <- IHn; [done | lia]. -Qed.*) - Lemma stream_prefix_map {A B : Type} (f : A -> B) @@ -301,29 +253,6 @@ element or two consecutive elements at a time with corresponding list quantifiers applied on their finite prefixes. *) -(*Lemma stream_prefix_ForAll - {A : Type} - (P : A -> Prop) - (s : Stream A) - : ForAll1 P s <-> forall n : nat, Forall P (stream_prefix s n). -Proof. - rewrite ForAll1_forall. - setoid_rewrite (Forall_nth P (hd s)). - setoid_rewrite stream_prefix_length. - specialize (stream_prefix_nth s) as Hi. - split. - - intros Hp n i Hlt. - specialize (Hi _ _ Hlt). - apply nth_error_nth with (d := hd s) in Hi. - rewrite Hi. apply Hp. - - intros Hp n. - assert (Hn : n < S n) by lia. - specialize (Hp _ _ Hn). - specialize (Hi _ _ Hn). - apply nth_error_nth with (d := hd s) in Hi. - by rewrite Hi in Hp. -Qed.*) - Lemma stream_prefix_ForAll2 {A : Type} (R : A -> A -> Prop) @@ -369,37 +298,6 @@ Proof. by apply Hp. Qed. -(*Lemma ForAll2_strict_lookup_rev [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R} - (l : Stream A) (Hl : ForAll2 R l) - : forall m n, R (Str_nth m l) (Str_nth n l) -> m < n. -Proof. - intros m n Hr. - destruct (decide (n <= m)); [|lia]. - exfalso. - destruct HR as [HI HT]. - rewrite ForAll2_transitive_lookup in Hl by done. - destruct (decide (m = n)); subst. - - by elim (HI (Str_nth n l)). - - specialize (Hl n m). spec Hl; [lia|]. - elim (HI (Str_nth n l)). - by transitivity (Str_nth m l). -Qed.*) - -(*Lemma ForAll2_strict_lookup_inj - [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R} - (l : Stream A) (Hl : ForAll2 R l) - : forall m n, Str_nth m l = Str_nth n l -> m = n. -Proof. - intros m n Hmn. - destruct HR as [HI HT]. - rewrite ForAll2_transitive_lookup in Hl by done. - destruct (decide (m = n)); [done |]. - elim (HI (Str_nth n l)). - by destruct (decide (m < n)) - ; [spec Hl m n|spec Hl n m]; (spec Hl; [lia|]) - ; rewrite Hmn in Hl. -Qed.*) - Definition stream_suffix {A : Type} (l : Stream A) @@ -407,17 +305,6 @@ Definition stream_suffix : Stream A := Str_nth_tl n l. -(*Lemma stream_suffix_S - {A : Type} - (l : Stream A) - (n : nat) - : stream_suffix l n = Cons (Str_nth n l) (stream_suffix l (S n)). -Proof. - revert l. induction n; intros. - - by destruct l. - - by apply IHn. -Qed.*) - Lemma stream_suffix_nth {A : Type} (s : Stream A) @@ -459,21 +346,6 @@ Definition stream_segment : list A := list_suffix (stream_prefix l n2) n1. -(*Lemma stream_segment_nth - {A : Type} - (l : Stream A) - (n1 n2 : nat) - (Hn : n1 <= n2) - (i : nat) - (Hi1 : n1 <= i) - (Hi2 : i < n2) - : nth_error (stream_segment l n1 n2) (i - n1) = Some (Str_nth i l). -Proof. - unfold stream_segment. - rewrite list_suffix_nth; [| done]. - by apply stream_prefix_nth. -Qed.*) - Definition stream_segment_alt {A : Type} (l : Stream A) @@ -481,31 +353,6 @@ Definition stream_segment_alt : list A := stream_prefix (stream_suffix l n1) (n2 - n1). -(*Lemma stream_segment_alt_iff - {A : Type} - (l : Stream A) - (n1 n2 : nat) - : stream_segment l n1 n2 = stream_segment_alt l n1 n2. -Proof. - apply nth_error_eq. - intro k. - unfold stream_segment_alt. unfold stream_segment. - destruct (decide (n2 - n1 <= k)). - - specialize (nth_error_None (list_suffix (stream_prefix l n2) n1) k); intros [_ H]. - specialize (nth_error_None (stream_prefix (stream_suffix l n1) (n2 - n1)) k); intros [_ H_alt]. - rewrite H, H_alt; [done | |]. - + by rewrite stream_prefix_length. - + by rewrite list_suffix_length, stream_prefix_length. - - rewrite stream_prefix_nth, stream_suffix_nth by lia. - assert (Hle : n1 <= n1 + k) by lia. - specialize (list_suffix_nth (stream_prefix l n2) n1 (n1 + k) Hle) - ; intro Heq. - clear Hle. - assert (Hs: n1 + k - n1 = k) by lia. - rewrite Hs in Heq. - rewrite Heq, stream_prefix_nth; [do 2 f_equal |]; lia. -Qed.*) - Lemma stream_prefix_segment {A : Type} (l : Stream A) @@ -535,31 +382,6 @@ Proof. by rewrite stream_prefix_segment. Qed. -(*Lemma stream_segment_app - {A : Type} - (l : Stream A) - (n1 n2 n3 : nat) - (H12 : n1 <= n2) - (H23 : n2 <= n3) - : stream_segment l n1 n2 ++ stream_segment l n2 n3 = stream_segment l n1 n3. -Proof. - assert (Hle : n1 <= n3) by lia. - specialize (stream_prefix_segment_suffix l n1 n3 Hle); intro Hl1. - specialize (stream_prefix_segment_suffix l n2 n3 H23); intro Hl2. - rewrite <- Hl2 in Hl1 at 4. clear Hl2. - apply stream_app_inj_l in Hl1. - - specialize (list_prefix_suffix (stream_prefix l n2) n1); intro Hl2. - specialize (stream_prefix_prefix l n1 n2 H12); intro Hl3. - rewrite Hl3 in Hl2. - rewrite <- Hl2, <- app_assoc in Hl1. - by apply app_inv_head in Hl1. - - repeat rewrite app_length. - unfold stream_segment. - repeat rewrite list_suffix_length. - repeat rewrite stream_prefix_length. - lia. -Qed.*) - Definition monotone_nat_stream_prop (s : Stream nat) := forall n1 n2 : nat, n1 < n2 -> Str_nth n1 s < Str_nth n2 s. @@ -599,20 +421,6 @@ Proof. spec Hs; lia. Qed. -(*Definition monotone_nat_stream := - {s : Stream nat | monotone_nat_stream_prop s}.*) - -(*Lemma monotone_nat_stream_tl - (s : Stream nat) - (Hs : monotone_nat_stream_prop s) - : monotone_nat_stream_prop (tl s). -Proof. - intros n1 n2 Hlt. - specialize (Hs (S n1) (S n2)). - apply Hs. - lia. -Qed.*) - CoFixpoint nat_sequence_from (n : nat) : Stream nat := Cons n (nat_sequence_from (S n)). @@ -638,9 +446,6 @@ Proof. apply ForAll2_forall. intro m. rewrite !nat_sequence_from_nth. lia. Qed. -(*Definition nat_sequence_sorted : ForAll2 lt nat_sequence := - nat_sequence_from_sorted 0.*) - Lemma nat_sequence_from_prefix_sorted : forall m n, LocallySorted lt (stream_prefix (nat_sequence_from m) n). Proof. @@ -694,18 +499,6 @@ Definition FinitelyMany : Stream A -> Prop := Definition FinitelyManyBound (s : Stream A) : Type := { n : nat | ForAll1 (fun a => ~ P a) (Str_nth_tl n s)}. -(*Lemma FinitelyMany_from_bound - : forall s, FinitelyManyBound s -> FinitelyMany s. -Proof. - intros s [n Hn]. - apply Exists_Str_nth_tl. - by exists n. -Qed.*) - -(*Lemma InfinitelyOften_tl s - : InfinitelyOften s -> InfinitelyOften (tl s). -Proof. by inversion 1. Qed.*) - Definition InfinitelyOften_nth_tl : forall n s, InfinitelyOften s -> InfinitelyOften (Str_nth_tl n s) := (@ForAll_Str_nth_tl _ (Exists1 P)). diff --git a/theories/VLSM/Lib/StreamFilters.v b/theories/VLSM/Lib/StreamFilters.v index 18dace60..2b5db905 100644 --- a/theories/VLSM/Lib/StreamFilters.v +++ b/theories/VLSM/Lib/StreamFilters.v @@ -41,19 +41,6 @@ Proof. by apply filtering_subsequence_sorted in Hfs. Qed. -(*Lemma filtering_subsequence_iff - {A : Type} - (P Q : A -> Prop) - (HPQ : forall a, P a <-> Q a) - (s : Stream A) - (ss : Stream nat) - : filtering_subsequence P s ss <-> filtering_subsequence Q s ss. -Proof. - unfold filtering_subsequence. - rewrite !ForAll2_forall. - by setoid_rewrite <- HPQ. -Qed.*) - (** Each element in a [filtering_subsequence] is a position in the base stream for which the predicate holds. *) @@ -276,23 +263,6 @@ Next Obligation. by apply filtering_subsequence_prefix_length. Qed. -(*Lemma stream_filter_Forall - {A : Type} - (P : A -> Prop) - (s : Stream A) - (ss : Stream nat) - (s' := stream_subsequence s ss) - (Hfs : filtering_subsequence P s ss) - : ForAll1 P s'. -Proof. - apply ForAll1_forall. - intro n. - unfold s'. - unfold stream_subsequence. - rewrite Str_nth_map. - by apply filtering_subsequence_witness. -Qed.*) - (** ** Obtaining [filtering_sequences] for streams Given a stream, a decidable predicate on its elements, and a guarantee that the @@ -383,28 +353,6 @@ Proof. rewrite Heq. simpl. lia. Qed. -(*Lemma stream_filter_fst_pos_nth_tl_has_property - (s : Stream A) - (n : nat) - (sn := Str_nth_tl n s) - (Hev : Exists1 P sn) - (fpair := stream_filter_fst_pos (Str_nth_tl n s) Hev n) - : P (Str_nth fpair.1 s) /\ - forall i, n <= i < fpair.1 -> ~ P (Str_nth i s). -Proof. - specialize (stream_filter_fst_pos_characterization sn Hev n) - as [k [Heq [Hp Hnp]]]. - subst sn fpair. - rewrite Heq. - clear -Hp Hnp. rewrite Str_nth_plus, Nat.add_comm in Hp. - split; [done |]. - intros i [Hlt_i Hilt]. - apply le_plus_dec in Hlt_i as [i' Hi]. - subst i. - rewrite <- Str_nth_plus. - apply Hnp. simpl in *. lia. -Qed.*) - (** Given as stream <> for which predicate <

> holds [InfinitelyOften] produces the streams of all its position at which <

> holds in a strictly increasing order (shifted by the given argument <>). @@ -463,18 +411,6 @@ Proof. replace (n0 + S (k + kn)) with (S (n0 + kn + k)) by lia. eauto. Qed. -(*Lemma stream_filter_positions_monotone - (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat) - : monotone_nat_stream_prop (stream_filter_positions s Hinf n). -Proof. - apply monotone_nat_stream_prop_from_successor. - revert s Hinf n. - cofix H. - intros. - constructor; simpl; [|apply H]. - apply stream_filter_fst_pos_le. -Qed.*) - (** [stream_filter_positions] produces a [filtering_sequence]. *) Lemma stream_filter_positions_filtering_subsequence @@ -517,14 +453,6 @@ Definition stream_filter_map : Stream B := filtering_subsequence_stream_filter_map P f _ _ (stream_filter_positions_filtering_subsequence s Hinf). -(** Stream filtering is obtained as a specialization of [stream_filter_map]. -*) -(*Definition stream_filter - (s : Stream A) - (Hinf : InfinitelyOften P s) - : Stream A := - stream_filter_map proj1_sig s Hinf.*) - End stream_filter_positions. Section stream_map_option. @@ -547,18 +475,6 @@ Definition stream_map_option : Stream B := stream_filter_map P (fun k : dsig P => is_Some_proj (proj2_dsig k)) s Hinf. -(*Lemma stream_map_option_prefix - (Hinf : InfinitelyOften P s) - (n : nat) - (map_opt_pre := map_option f (stream_prefix s n)) - (m := length map_opt_pre) - : stream_prefix (stream_map_option Hinf) m = map_opt_pre. -Proof. - subst map_opt_pre m. - rewrite !(map_option_as_filter f (stream_prefix s n)). - apply fitering_subsequence_stream_filter_map_prefix. -Qed.*) - Program Definition stream_map_option_prefix_ex (Hinf : InfinitelyOften P s) (Hfs := stream_filter_positions_filtering_subsequence _ _ Hinf) @@ -570,11 +486,6 @@ Next Obligation. by intros; cbn; rewrite !map_option_as_filter. Qed. -(*Definition bounded_stream_map_option - (Hfin : FinitelyManyBound P s) - : list B := - map_option f (stream_prefix s (` Hfin)).*) - End stream_map_option. (** For a totally defined function, [stream_map_option] corresponds to the diff --git a/theories/VLSM/Lib/Temporal.v b/theories/VLSM/Lib/Temporal.v index 900abe90..4a7b40e9 100644 --- a/theories/VLSM/Lib/Temporal.v +++ b/theories/VLSM/Lib/Temporal.v @@ -116,19 +116,6 @@ Lemma refutation [A:Type] [R:A -> A-> Prop] (HR: well_founded R) by eapply H0; eauto. Qed. -(*Lemma forall_forever: forall [A B:Type] (P: A -> Stream B -> Prop) [s: Stream B], - (forall (a:A), Forever (P a) s) -> Forever (fun s => forall a, P a s) s. -Proof. - intros A B P. - cofix forall_forever. - destruct s. - intro H. - constructor. - - intro a. by destruct (H a). - - apply forall_forever. - intro a. by destruct (H a). -Qed.*) - Lemma not_forever [A:Type] (P: Stream A -> Prop): forall s, ~Forever P s -> Eventually (fun s => ~ P s) s. Proof. diff --git a/theories/VLSM/Lib/TopSort.v b/theories/VLSM/Lib/TopSort.v index 95ce414d..cad25df0 100644 --- a/theories/VLSM/Lib/TopSort.v +++ b/theories/VLSM/Lib/TopSort.v @@ -135,21 +135,6 @@ Proof. by destruct (decide (precedes a a)). Qed. -(*Lemma precedes_asymmetric - (a b : A) - (Ha : P a) - (Hb : P b) - (Hab : precedes a b) - : ~ precedes b a. -Proof. - intro Hba. - exact - (StrictOrder_Asymmetric Hso - (exist P a Ha) (exist P b Hb) - Hab Hba - ). -Qed.*) - Lemma precedes_transitive (a b c : A) (Ha : P a) @@ -336,26 +321,6 @@ Proof. right; left. Qed. -(** -As a corollary of the above, if <> then <> can be found before -<> in l. -*) -(*Corollary top_sort_precedes - (a b : A) - (Hab : precedes a b) - (Ha : a ∈ l) - (Hb : b ∈ l) - : exists l1 l2 l3, l = l1 ++ [a] ++ l2 ++ [b] ++ l3. -Proof. - apply elem_of_list_split in Hb. - destruct Hb as [l12 [l3 Hb']]. - specialize (top_sort_before a b Hab Ha l12 l3 Hb'). - intros Ha12. apply elem_of_list_split in Ha12. - destruct Ha12 as [l1 [l2 Ha12]]. - subst l12. - exists l1, l2, l3. by rewrite Hb', <- app_assoc. -Qed.*) - End topologically_sorted_fixed_list. End topologically_sorted. @@ -761,47 +726,4 @@ Proof. by intro; apply Forall_forall. Qed. -(*Corollary simple_topologically_sorted_precedes_closed_remove_last - (l : list A) - (Hts : topologically_sorted precedes l) - (init : list A) - (final : A) - (Hinit : l = init ++ [final]) - (Hpc : precedes_closed precedes l) - : precedes_closed precedes init. -Proof. - eapply topologically_sorted_precedes_closed_remove_last; - [typeclasses eauto | apply Forall_True | done..]. -Qed.*) - -(*Corollary simple_top_sort_correct : forall l, - topological_sorting precedes l (top_sort precedes l). -Proof. - intro; eapply top_sort_correct; [typeclasses eauto | apply Forall_True]. -Qed.*) - -(*Corollary simple_maximal_element_in l - (a : A) - (Hmax : get_maximal_element precedes l = Some a) : - a ∈ l. -Proof. - eapply maximal_element_in; [typeclasses eauto | apply Forall_True | done]. -Qed.*) - -(*Corollary simple_get_maximal_element_correct l - (a max : A) - (Hina : a ∈ l) - (Hmax : get_maximal_element precedes l = Some max) : - ~ precedes max a. -Proof. - eapply get_maximal_element_correct; [typeclasses eauto | apply Forall_True | done..]. -Qed.*) - -(*Corollary simple_get_maximal_element_some - l (Hne : l <> []) : - exists a, get_maximal_element precedes l = Some a. -Proof. - eapply get_maximal_element_some; [apply Forall_True | done]. -Qed.*) - End sec_simple_top_sort. diff --git a/theories/VLSM/Lib/TraceClassicalProperties.v b/theories/VLSM/Lib/TraceClassicalProperties.v index c41a281f..c365864e 100644 --- a/theories/VLSM/Lib/TraceClassicalProperties.v +++ b/theories/VLSM/Lib/TraceClassicalProperties.v @@ -16,22 +16,22 @@ Context {A B : Type}. (** ** Relating finiteness and infiniteness *) -(*Lemma not_infiniteT_finiteT : forall tr : trace, +Lemma not_infiniteT_finiteT : forall tr : trace, ~ infiniteT tr -> finiteT tr. Proof. move => tr Hnot. case: (classic (finiteT tr)) => Hinf //. case: Hnot. exact: not_finiteT_infiniteT. -Qed.*) +Qed. -(*Lemma finiteT_infiniteT : forall tr : trace, +Lemma finiteT_infiniteT : forall tr : trace, finiteT tr \/ infiniteT tr. Proof. move => tr. case: (classic (finiteT tr)) => Hinf; first by left. right; exact: not_finiteT_infiniteT. -Qed.*) +Qed. Definition finiteT_infiniteT_dec (tr : trace) : { finiteT tr }+{ infiniteT tr } := match excluded_middle_informative (finiteT tr) with @@ -71,10 +71,10 @@ exists (midp h2); split. - exact: (midpointT_after (midpointT_midp h2)). Qed. -(*Lemma AppendT_assoc_R: forall (p1 p2 p3 : propT), (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3. +Lemma AppendT_assoc_R: forall (p1 p2 p3 : propT), (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3. Proof. move => [f1 hf1] [f2 hf2] [f3 hf3] tr0 /= h1. exact: appendT_assoc_R. -Qed.*) +Qed. End TraceClassicalProperties. diff --git a/theories/VLSM/Lib/TraceProperties.v b/theories/VLSM/Lib/TraceProperties.v index 75079c48..4388b338 100644 --- a/theories/VLSM/Lib/TraceProperties.v +++ b/theories/VLSM/Lib/TraceProperties.v @@ -41,13 +41,13 @@ Qed. Definition InfiniteT : propT := exist _ (fun tr => infiniteT tr) infiniteT_setoidT. -(*Lemma infiniteT_cons : forall a b tr, +Lemma infiniteT_cons : forall a b tr, infiniteT (Tcons a b tr) -> infiniteT tr. Proof. by move => a b tr Hinf; inversion Hinf. -Qed.*) +Qed. -(*Lemma infiniteT_trace_append : +Lemma infiniteT_trace_append : forall tr, infiniteT tr -> forall tr', infiniteT (tr' +++ tr). Proof. cofix CIH. @@ -55,16 +55,16 @@ move => tr Htr. case => [a|a b tr']; first by rewrite trace_append_nil. rewrite trace_append_cons. exact/infiniteT_delay/CIH. -Qed.*) +Qed. -(*Lemma trace_append_infiniteT : +Lemma trace_append_infiniteT : forall tr, infiniteT tr -> forall tr', infiniteT (tr +++ tr'). Proof. cofix CIH. case => [a|a b tr0] Hinf; inversion Hinf => tr'; subst. rewrite trace_append_cons. exact/infiniteT_delay/CIH. -Qed.*) +Qed. (** ** Finiteness property *) @@ -91,20 +91,20 @@ Proof. by inversion h. Defined. (** Equality coincides with bisimilarity for finite traces. *) -(*Lemma finiteT_bisim_eq : forall tr, +Lemma finiteT_bisim_eq : forall tr, finiteT tr -> forall tr', bisim tr tr' -> tr = tr'. Proof. move => tr; elim => [a tr'|a b tr0 Hfin IH tr'] Hbis; invs Hbis => //. by rewrite (IH _ H3). -Qed.*) +Qed. (** Basic connections between finiteness and infiniteness. *) -(*Lemma finiteT_infiniteT_not : forall tr, +Lemma finiteT_infiniteT_not : forall tr, finiteT tr -> infiniteT tr -> False. Proof. by move => tr; elim => [a|a b tr' Hfin IH] Hinf; inversion Hinf. -Qed.*) +Qed. Lemma not_finiteT_infiniteT : forall tr, ~ finiteT tr -> infiniteT tr. @@ -133,19 +133,19 @@ Inductive finalTB : trace -> B -> Prop := finalTB tr b' -> finalTB (Tcons a b tr) b'. -(*Lemma finalTA_finiteT : forall tr a, finalTA tr a -> finiteT tr. +Lemma finalTA_finiteT : forall tr a, finalTA tr a -> finiteT tr. Proof. move => tr a; elim => [a1|a1 b a2 tr' Hfinal IH]. - exact: finiteT_nil. - exact/finiteT_delay/IH. -Qed.*) +Qed. -(*Lemma finalTB_finiteT : forall tr b, finalTB tr b -> finiteT tr. +Lemma finalTB_finiteT : forall tr b, finalTB tr b -> finiteT tr. Proof. move => tr b; elim => [a1 b1 a2|a1 b1 b2 a2 Hfin IH]. - exact/finiteT_delay/finiteT_nil. - exact: finiteT_delay. -Qed.*) +Qed. Fixpoint finalA (tr : trace) (h : finiteT tr) {struct h} : A := match tr as tr' return (finiteT tr' -> A) with @@ -153,21 +153,21 @@ match tr as tr' return (finiteT tr' -> A) with | Tcons a b tr => fun h => finalA (invert_finiteT_delay h) end h. -(*Lemma finiteT_finalTA : forall tr (h : finiteT tr), +Lemma finiteT_finalTA : forall tr (h : finiteT tr), finalTA tr (finalA h). Proof. refine (fix IH tr h {struct h} := _). case: tr h => [a|a b tr] h; dependent inversion h => /=. - exact: finalTA_nil. - exact: finalTA_delay. -Qed.*) +Qed. -(*Lemma finalTA_hd_append_trace : forall tr0 a, +Lemma finalTA_hd_append_trace : forall tr0 a, finalTA tr0 a -> forall tr1, hd tr1 = a -> hd (tr0 +++ tr1) = hd tr0. Proof. by move => tr a; elim => {tr a} [a tr <-|a b a' tr Hfinal IH tr'] //=. -Qed.*) +Qed. (** ** Basic trace properties and connectives *) @@ -184,8 +184,8 @@ Definition ffT : trace -> Prop := fun tr => False. Lemma ffT_setoidT : setoidT ffT. Proof. by []. Qed. -(*Definition FfT : propT := -exist _ ffT ffT_setoidT.*) +Definition FfT : propT := +exist _ ffT ffT_setoidT. Definition notT (p : trace -> Prop) : trace -> Prop := fun tr => ~ p tr. @@ -195,20 +195,20 @@ move => p hp tr h1 tr' h2 h3. apply: h1. apply: hp _ h3 _ (bisim_sym h2). Qed. -(*Definition NotT (p : propT) : propT := +Definition NotT (p : propT) : propT := let: exist f hf := p in -exist _ (notT f) (notT_setoidT hf).*) +exist _ (notT f) (notT_setoidT hf). Definition satisfyT (p : propT) : trace -> Prop := fun tr => let: exist f0 h0 := p in f0 tr. -(*Program Definition ExT {T: Type} (p: T -> propT) : propT := +Program Definition ExT {T: Type} (p: T -> propT) : propT := exist _ (fun tr => exists x, satisfyT (p x) tr) _. Next Obligation. move => tr0 [x h0] tr1 h1. exists x. case: (p x) h0 => [f0 h2] /= h0. exact: h2 _ h0 _ h1. -Defined.*) +Defined. Lemma andT_setoidT : forall f0 f1, setoidT f0 -> setoidT f1 -> @@ -247,29 +247,29 @@ forall tr, satisfyT p1 tr -> satisfyT p2 tr. #[local] Infix "=>>" := propT_imp (at level 60, right associativity). -(*Lemma propT_imp_conseq_L: forall p0 p1 q, p0 =>> p1 -> p1 =>> q -> p0 =>> q. +Lemma propT_imp_conseq_L: forall p0 p1 q, p0 =>> p1 -> p1 =>> q -> p0 =>> q. Proof. move => [p0 hp0] [p1 hp1] [q hq] h0 h1 tr0 /= h2. exact/h1/h0. -Qed.*) +Qed. -(*Lemma propT_imp_conseq_R: forall p q0 q1, +Lemma propT_imp_conseq_R: forall p q0 q1, q0 =>> q1 -> p =>> q0 -> p =>> q1. Proof. move => [p hp] [q0 hq0] [q1 hq1] h0 h1 tr0 /= h2. exact/h0/h1. -Qed.*) +Qed. -(*Lemma propT_imp_andT: forall p q0 q1, +Lemma propT_imp_andT: forall p q0 q1, p =>> q0 -> p =>> q1 -> p =>> (q0 andT q1). Proof. move => [p hp] [q0 hq0] [q1 hq1] h0 h1 tr0 /= h2. split. - exact: h0. - exact: h1. -Qed.*) +Qed. -(*Lemma propT_imp_refl : forall p, p =>> p. -Proof. by move => p. Qed.*) +Lemma propT_imp_refl : forall p, p =>> p. +Proof. by move => p. Qed. Lemma satisfyT_cont : forall p0 p1, p0 =>> p1 -> forall tr, satisfyT p0 tr -> satisfyT p1 tr. @@ -284,15 +284,15 @@ move => p q r h0 h1 tr0 h2. exact/(satisfyT_cont h1)/(satisfyT_cont h0 h2). Qed. -(*Lemma OrT_left : forall p1 p2, p1 =>> (p1 orT p2). +Lemma OrT_left : forall p1 p2, p1 =>> (p1 orT p2). Proof. by move => [f1 hf1] [f2 hf2] tr /= h1; left. -Qed.*) +Qed. -(*Lemma OrT_right: forall p1 p2, p2 =>> (p1 orT p2). +Lemma OrT_right: forall p1 p2, p2 =>> (p1 orT p2). Proof. by move => [f1 hf1] [f2 hf2] tr /= h1; right. -Qed.*) +Qed. (** ** Basic trace element properties and connectives *) @@ -310,8 +310,8 @@ Definition andA (u1 u2: propA) : propA := fun a => u1 a /\ u2 a. #[local] Infix "andA" := andA (at level 60, right associativity). -(*Definition exA {T : Type} (u: T -> propA) : propA := -fun st => exists x, u x st.*) +Definition exA {T : Type} (u: T -> propA) : propA := +fun st => exists x, u x st. (** ** Singleton property *) @@ -327,12 +327,12 @@ move => u tr0 [a [h0 h2]] tr1 h1; invs h2; invs h1. exact: nil_singletonT. Qed. -(*Lemma singletonT_cont : forall u v, u ->> v -> +Lemma singletonT_cont : forall u v, u ->> v -> forall tr, singletonT u tr -> singletonT v tr. Proof. move => u v huv tr0 [a [h0 h1]]; invs h1. exact/nil_singletonT/huv. -Qed.*) +Qed. Lemma singletonT_nil: forall u a, singletonT u (Tnil a) -> u a. Proof. by move => u st [a [h0 h1]]; invs h1. Qed. @@ -342,11 +342,11 @@ exist _ (singletonT u) (@singletonT_setoidT u). #[local] Notation "[| p |]" := (SingletonT p) (at level 80). -(*Lemma SingletonT_cont: forall u v, u ->> v -> [|u|] =>> [|v|]. +Lemma SingletonT_cont: forall u v, u ->> v -> [|u|] =>> [|v|]. Proof. move => u v h0 tr0 [a [h1 h2]]; invs h2. exact/nil_singletonT/h0. -Qed.*) +Qed. (** ** Duplicate element property *) @@ -379,11 +379,11 @@ exist _ (dupT u b) (@dupT_setoidT u b). #[local] Notation "<< p ; b >>" := (DupT p b) (at level 80). -(*Lemma DupT_cont: forall u v b, u ->> v -> <> =>> <>. +Lemma DupT_cont: forall u v b, u ->> v -> <> =>> <>. Proof. move => u v b h0 tr0 /=. exact: dupT_cont. -Qed.*) +Qed. (** ** Follows property *) @@ -427,14 +427,14 @@ move => tr0 tr1 h0 tr2 h1 tr3 h2; invs h0. exact: (followsT_delay a b (CIH _ _ H _ H5 _ H4)). Qed. -(*Lemma followsT_setoidT_L : forall p, +Lemma followsT_setoidT_L : forall p, forall tr0 tr1, followsT p tr0 tr1 -> forall tr2, bisim tr0 tr2 -> followsT p tr2 tr1. Proof. move => p. cofix CIH. move => tr tr0 h0 tr1 h1; invs h0; invs h1. - exact: followsT_nil. - exact: (followsT_delay a b (CIH _ _ H _ H4)). -Qed.*) +Qed. Lemma followsT_setoidT_R : forall (p: trace -> Prop) (hp: forall tr0, p tr0 -> forall tr1, bisim tr0 tr1 -> p tr1), @@ -448,7 +448,7 @@ move => tr tr0 h0 tr1 h1; invs h0. - invs h1. exact: (followsT_delay a b (CIH _ _ H _ H4)). Qed. -(*Lemma followsT_cont : forall (p q : trace -> Prop), +Lemma followsT_cont : forall (p q : trace -> Prop), (forall tr, p tr -> q tr) -> forall tr0 tr1, followsT p tr0 tr1 -> followsT q tr0 tr1. Proof. @@ -456,7 +456,7 @@ move => p q hpq. cofix CIH. move => tr0 tr1 h0; invs h0. - apply: followsT_nil => //. exact: hpq _ H0. - exact/followsT_delay/CIH. -Qed.*) +Qed. Lemma followsT_singletonT: forall u tr0 tr1, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1. @@ -467,7 +467,7 @@ move => u. cofix CIH. move => tr0 tr1 h0; invs h0. - exact/bisim_cons/CIH. Qed. -(*Lemma followsT_singleton_andA_L: forall u0 u1 tr0, +Lemma followsT_singleton_andA_L: forall u0 u1 tr0, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0. Proof. @@ -479,9 +479,9 @@ move => u0 u1. cofix CIH. case. exact: nil_singletonT. - move => a b tr0 h0; invs h0. exact/followsT_delay/CIH. -Qed.*) +Qed. -(*Lemma followsT_singleton_andA_R: forall u0 u1 tr0, +Lemma followsT_singleton_andA_R: forall u0 u1 tr0, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0. Proof. @@ -493,9 +493,9 @@ move => u0 u1. cofix CIH. case. exact: nil_singletonT. - move => a b tr0 h0; invs h0. exact/followsT_delay/CIH. -Qed.*) +Qed. -(*Lemma singletonT_andA_followsT: forall u v tr, +Lemma singletonT_andA_followsT: forall u v tr, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr. Proof. @@ -504,15 +504,15 @@ move => u v. cofix CIH. move => tr h0 h1; invs h0; invs h1. apply: nil_singletonT. by split; apply: singletonT_nil. - exact/followsT_delay/CIH. -Qed.*) +Qed. -(*Lemma followsT_ttA : forall tr, followsT (singletonT ttA) tr tr. +Lemma followsT_ttA : forall tr, followsT (singletonT ttA) tr tr. Proof. cofix CIH. case => [a|a b tr0]. - apply: followsT_nil => //. exact: nil_singletonT. - exact/followsT_delay/CIH. -Qed.*) +Qed. (** ** Append property *) @@ -545,13 +545,13 @@ move => p0 p1 q hp tr. exact: (@appendT_cont _ _ q q hp _). Qed. -(*Lemma appendT_cont_R: forall (p q0 q1: trace -> Prop), +Lemma appendT_cont_R: forall (p q0 q1: trace -> Prop), (forall tr, q0 tr -> q1 tr) -> forall tr, (appendT p q0 tr) -> (appendT p q1 tr). Proof. move => p q0 q1 hq tr. exact: (@appendT_cont p p _ _ _ hq). -Qed.*) +Qed. Lemma appendT_setoidT: forall (p0 p1: trace -> Prop), setoidT p1 -> setoidT (appendT p0 p1). @@ -561,7 +561,7 @@ move: h0 => [tr2 [h0 h2]]. exists tr2; split; first by apply: h0. exact: (followsT_setoidT_R hp1 h2 h1). Qed. -(*Lemma followsT_followsT: forall p q tr0 tr1 tr2, followsT p tr0 tr1 -> +Lemma followsT_followsT: forall p q tr0 tr1 tr2, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2. Proof. move => p q. cofix CIH. case. @@ -569,7 +569,7 @@ move => p q. cofix CIH. case. apply: followsT_nil => //. by exists tr1. - move => a b tr0 tr1 tr2 h0 h1; invs h0; invs h1. exact: followsT_delay _ _ (CIH _ _ _ H3 H4). -Qed.*) +Qed. Lemma appendT_assoc_L : forall p1 p2 p3 tr, (appendT (appendT p1 p2) p3) tr -> appendT p1 (appendT p2 p3) tr. @@ -583,7 +583,7 @@ move => tr0 tr1 tr2 h1 h2; invs h2. - invs h1. exact: followsT_delay _ _ (CIH _ _ _ H4 H). Qed. -(*Lemma appendT_finalTA: forall (p q : trace -> Prop) tr0 tr1, +Lemma appendT_finalTA: forall (p q : trace -> Prop) tr0 tr1, p tr0 -> q tr1 -> finalTA tr0 (hd tr1) -> (p *+* q) (tr0 +++ tr1). Proof. @@ -594,7 +594,7 @@ move: {hp} tr0 tr1 hq hfin. cofix CIH. case. - move => a b tr0 tr1 h0 h1; invs h1. rewrite [Tcons a b tr0 +++ tr1]trace_destr /=. exact/followsT_delay/CIH. -Qed.*) +Qed. Definition AppendT (p1 p2: propT) : propT := let: exist f0 h0 := p1 in @@ -603,19 +603,19 @@ exist _ (appendT f0 f1) (appendT_setoidT h1). #[local] Infix "***" := AppendT (at level 60, right associativity). -(*Lemma AppendT_assoc_L: forall p1 p2 p3, ((p1 *** p2) *** p3) =>> (p1 *** p2 *** p3). +Lemma AppendT_assoc_L: forall p1 p2 p3, ((p1 *** p2) *** p3) =>> (p1 *** p2 *** p3). Proof. move => [f1 hf1] [f2 hf2] [f3 hf3] tr0 /= h1. exact: appendT_assoc_L. -Qed.*) +Qed. -(*Lemma AppendT_cont : forall p1 p2 q1 q2, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> (p2 *** q2). +Lemma AppendT_cont : forall p1 p2 q1 q2, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> (p2 *** q2). Proof. move => [p1 hp1] [p2 hp2] [q1 hq1] [q2 hq2] h0 h1 tr0 /= h2. apply: (appendT_cont _ _ h2). - exact: h0. - exact: h1. -Qed.*) +Qed. Lemma AppendT_cont_L: forall p1 p2 q, p1 =>> p2 -> (p1 *** q) =>> (p2 *** q). Proof. @@ -629,7 +629,7 @@ move => [q hq] [p1 hp1] [p2 hp2] h0 tr0 /= h1. exact: (@appendT_cont q q p1 p2). Qed. -(*Lemma AppendT_ttA: forall p, p =>> (p *** [|ttA|]). +Lemma AppendT_ttA: forall p, p =>> (p *** [|ttA|]). Proof. move => [f hp] tr0 /= h0. exists tr0; split => //. @@ -637,72 +637,72 @@ move: {h0 hp} tr0. cofix CIH. case => [a|a b tr0]. - exact/followsT_nil/nil_singletonT. - exact/followsT_delay/CIH. -Qed.*) +Qed. -(*Lemma SingletonT_DupT_AppendT_andA_DupT : forall u v b, ([|u|] *** <>) =>> <>. +Lemma SingletonT_DupT_AppendT_andA_DupT : forall u v b, ([|u|] *** <>) =>> <>. Proof. move => u v b tr0 [tr1 [[a [h0 h2]] h1]] /=; invs h2; invs h1. move: H1 => [a [h1 h2]]; invs h2; invs H1. exact: dupT_Tcons. -Qed.*) +Qed. -(*Lemma DupT_andA_AppendT_SingletonT_DupT : forall u v b, <> =>> ([|u|] *** <>). +Lemma DupT_andA_AppendT_SingletonT_DupT : forall u v b, <> =>> ([|u|] *** <>). Proof. move => u v b tr0 [a [[hu hv] h1]]; invs h1; invs H1. exists (Tnil a); split; first by apply: nil_singletonT. apply: followsT_nil => //. exact: dupT_Tcons. -Qed.*) +Qed. -(*Lemma DupT_andA_AppendT_SingletonT : forall u v b, <> =>> <> *** [|v|]. +Lemma DupT_andA_AppendT_SingletonT : forall u v b, <> =>> <> *** [|v|]. Proof. move => u v b tr0 [a [[hu hv] h0]]; invs h0; invs H1. exists (Tcons a b (Tnil a)); split. - exact: dupT_Tcons. - apply: followsT_delay. apply: followsT_nil => //. exact: nil_singletonT. -Qed.*) +Qed. -(*Lemma DupT_AppendT_SingletonT_andA_DupT : forall u v b, (<> *** [|v|]) =>> <>. +Lemma DupT_AppendT_SingletonT_andA_DupT : forall u v b, (<> *** [|v|]) =>> <>. Proof. move => u v b tr0 [tr1 [[a [hu h0]] h1]]. invs h0; invs H1; invs h1; invs H3; move: H1 => [a [hv h0]]; invs h0 => /=. exact: dupT_Tcons. -Qed.*) +Qed. -(*Lemma AppendT_andA : forall u v, ([|u|] *** [|v|]) =>> [|u andA v|]. +Lemma AppendT_andA : forall u v, ([|u|] *** [|v|]) =>> [|u andA v|]. Proof. move => u v tr0 [tr1 [[a [hu h0]] h1]]. invs h0; invs h1; move: H1 => [a [hv h0]]; invs h0 => /=. exact: nil_singletonT. -Qed.*) +Qed. -(*Lemma andA_AppendT: forall u v, [|u andA v|] =>> [|u|] *** [|v|]. +Lemma andA_AppendT: forall u v, [|u andA v|] =>> [|u|] *** [|v|]. Proof. move => u v tr0 [a [[hu hv] h0]]; invs h0. exists (Tnil a); split; first by apply: nil_singletonT. apply: followsT_nil => //. exact: nil_singletonT. -Qed.*) +Qed. Lemma SingletonT_AppendT: forall v p, ([|v|] *** p) =>> p. Proof. by move => v [p hp] tr0 /= [tr1 [[a [h0 h2]] h1]]; invs h1; invs h2. Qed. -(*Lemma ttA_AppendT_implies : forall p, ([|ttA|] *** p) =>> p. +Lemma ttA_AppendT_implies : forall p, ([|ttA|] *** p) =>> p. Proof. move => p. exact: SingletonT_AppendT. -Qed.*) +Qed. -(*Lemma implies_ttA_AppendT: forall p, p =>> [|ttA|] *** p. +Lemma implies_ttA_AppendT: forall p, p =>> [|ttA|] *** p. Proof. move => [p hp] tr0 /= htr0. exists (Tnil (hd tr0)); split. - exact: nil_singletonT. - exact: followsT_nil. -Qed.*) +Qed. Lemma appendT_singletonT: forall p (hp: setoidT p) u tr, appendT p (singletonT u) tr -> p tr. @@ -717,13 +717,13 @@ move => [p hp] v tr0 /=. exact: appendT_singletonT. Qed. -(*Lemma AppendT_ttA_implies : forall p, (p *** [|ttA|]) =>> p. +Lemma AppendT_ttA_implies : forall p, (p *** [|ttA|]) =>> p. Proof. move => p. exact: AppendT_Singleton. -Qed.*) +Qed. -(*Lemma implies_AppendT_ttA: forall p, p =>> p *** [|ttA|]. +Lemma implies_AppendT_ttA: forall p, p =>> p *** [|ttA|]. Proof. move => [p hp] tr0 /= htr0. exists tr0; split => //. @@ -732,48 +732,48 @@ case => [a|a b tr0]. - apply: followsT_nil => //. exact: nil_singletonT. - exact/followsT_delay/CIH. -Qed.*) +Qed. -(*Lemma TtT_AppendT_idem: (TtT *** TtT) =>> TtT. -Proof. by []. Qed.*) +Lemma TtT_AppendT_idem: (TtT *** TtT) =>> TtT. +Proof. by []. Qed. -(*Lemma AppendT_FiniteT_idem : (FiniteT *** FiniteT) =>> FiniteT. +Lemma AppendT_FiniteT_idem : (FiniteT *** FiniteT) =>> FiniteT. Proof. move => tr0 [tr1 [Hfin Hfol]]. elim: Hfin tr0 Hfol => [a tr0'|a b tr1' h0 IH tr0] Hfol; invs Hfol => //. exact/finiteT_delay/IH. -Qed.*) +Qed. -(*Lemma FiniteT_AppendT_idem : FiniteT =>> FiniteT *** FiniteT. +Lemma FiniteT_AppendT_idem : FiniteT =>> FiniteT *** FiniteT. Proof. move => tr0 h0. exists (Tnil (hd tr0)); split. - exact: finiteT_nil. - exact: followsT_nil. -Qed.*) +Qed. -(*Lemma FiniteT_SingletonT: forall u, (FiniteT *** [|u|]) =>> FiniteT. +Lemma FiniteT_SingletonT: forall u, (FiniteT *** [|u|]) =>> FiniteT. Proof. move => u tr /= [tr1 [h0 h1]]. exact: (finiteT_setoidT h0 (followsT_singletonT h1)). -Qed.*) +Qed. -(*Lemma InfiniteT_implies_AppendT : InfiniteT =>> (TtT *** [|ffA|]). +Lemma InfiniteT_implies_AppendT : InfiniteT =>> (TtT *** [|ffA|]). Proof. move => tr0 [a b tr1] HinfT /=. exists (Tcons a b tr1); split => {tr0} //. move: a b tr1 HinfT. cofix CIH. move => a b tr1 HinfT; invs HinfT. exact/followsT_delay/CIH. -Qed.*) +Qed. -(*Lemma AppendT_implies_InfiniteT: (TtT *** [|ffA|]) =>> InfiniteT. +Lemma AppendT_implies_InfiniteT: (TtT *** [|ffA|]) =>> InfiniteT. Proof. move => tr0 [tr1 [_ h1]] /=. move: tr0 tr1 h1; cofix CIH => tr0 tr1 h1; invs h1. - by move: H0 => [a [h1 h2]]; inversion h1. - exact: infiniteT_delay _ _ (CIH _ _ H). -Qed.*) +Qed. (** ** Iteration property *) @@ -811,7 +811,7 @@ move => tr0 h0; invs h0; first by apply: iterT_stop. exact: iterT_loop (hp _ H) (h _ _ H0). Qed. -(*Lemma iterT_appendT_dupT: forall (u : propA) p b tr, +Lemma iterT_appendT_dupT: forall (u : propA) p b tr, u (hd tr) -> iterT (appendT p (dupT u b)) tr -> followsT (singletonT u) tr tr. Proof. @@ -825,7 +825,7 @@ move => u p b. cofix CIH. move => tr h0 h1; invs h1. invs h3; invs H1; invs h1; invs H3. exact/followsT_delay/CIH. + invs h1. exact: followsT_delay _ _ (CIH1 _ _ _ H H4). -Qed.*) +Qed. Definition IterT (p : propT) : propT := let: exist f0 h0 := p in @@ -844,11 +844,11 @@ move => p tr h0; invs h0. - by right; exists tr0. Qed. -(*Lemma IterT_unfold_0: forall p, IterT p =>> ([|ttA|] orT (p *** IterT p)). +Lemma IterT_unfold_0: forall p, IterT p =>> ([|ttA|] orT (p *** IterT p)). Proof. move => [p hp] tr0 /= h0. exact: iterT_split_1 h0. -Qed.*) +Qed. Lemma iterT_split_2: forall tr p, (singletonT ttA tr) \/ (appendT p (iterT p) tr) -> iterT p tr. @@ -858,11 +858,11 @@ move => tr p [[a [h0 h1]]|[tr0 [h0 h1]]]. - exact: iterT_loop h0 h1. Qed. -(*Lemma IterT_fold_0 : forall p, ([|ttA|] orT (p *** IterT p)) =>> IterT p. +Lemma IterT_fold_0 : forall p, ([|ttA|] orT (p *** IterT p)) =>> IterT p. Proof. move => [p hp] tr0 /=. exact: iterT_split_2. -Qed.*) +Qed. Lemma iterT_unfold_1 : forall p tr, (iterT p *+* p) tr -> iterT p tr. Proof. @@ -880,30 +880,30 @@ move => tr0 tr1 h0 h1; invs h0. exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed. -(*Lemma IterT_unfold_1 : forall p, (IterT p *** p) =>> IterT p. +Lemma IterT_unfold_1 : forall p, (IterT p *** p) =>> IterT p. Proof. move => [p hp] tr /= h0. exact: iterT_unfold_1 h0. -Qed.*) +Qed. -(*Lemma IterT_unfold_2: forall p, ([|ttA|] orT (IterT p *** p)) =>> IterT p. +Lemma IterT_unfold_2: forall p, ([|ttA|] orT (IterT p *** p)) =>> IterT p. Proof. move => [p hp] tr0 /= [[a [_ h0]]|H]. - invs h0. exact: iterT_stop. - exact: iterT_unfold_1 H. -Qed.*) +Qed. -(*Lemma stop_IterT : forall p, [|ttA|] =>> IterT p. +Lemma stop_IterT : forall p, [|ttA|] =>> IterT p. Proof. move => [p hp] /= t0 [x [_ h0]]; invs h0 => /=. exact: iterT_stop. -Qed.*) +Qed. -(*Lemma IterT_fold_L : forall p, (p *** IterT p) =>> IterT p. +Lemma IterT_fold_L : forall p, (p *** IterT p) =>> IterT p. Proof. move => [p hp] tr0 /= [tr1 [h0 h1]]. exact: (iterT_loop h0). -Qed.*) +Qed. Lemma iterT_iterT_2 : forall p tr, iterT p tr -> appendT (iterT p) (iterT p) tr. Proof. @@ -915,11 +915,11 @@ case => [a|a b tr0]. - exact/followsT_delay/CIH. Qed. -(*Lemma IterT_IterT_2 : forall p, IterT p =>> (IterT p *** IterT p). +Lemma IterT_IterT_2 : forall p, IterT p =>> (IterT p *** IterT p). Proof. move => [p hp] tr0 /=. exact: iterT_iterT_2. -Qed.*) +Qed. Lemma iterT_iterT : forall p tr, appendT (iterT p) (iterT p) tr -> (iterT p) tr. Proof. @@ -934,8 +934,8 @@ move: tr1 tr0 h0 h1. cofix CIH. move => tr0 tr1 h0; invs h0 => h0. exact: followsT_delay _ _ (CIH2 _ _ _ H H4). Qed. -(*Lemma IterT_IterT : forall p, (IterT p *** IterT p) =>> IterT p. -Proof. move => [p hp] tr /=. exact: iterT_iterT. Qed.*) +Lemma IterT_IterT : forall p, (IterT p *** IterT p) =>> IterT p. +Proof. move => [p hp] tr /=. exact: iterT_iterT. Qed. Lemma IterT_DupT : forall v b, ([|v|] *** (IterT (TtT *** <>))) =>> (TtT *** [|v|]). @@ -975,27 +975,27 @@ move => [f hf] [g hg] /= h0. exact/lastA_cont/h0. Qed. -(*Lemma LastA_SingletonT_fold : forall u, LastA ([|u|]) ->> u. +Lemma LastA_SingletonT_fold : forall u, LastA ([|u|]) ->> u. Proof. by move => u a [tr0 [[st1 [h1 h3]] h2]]; invs h3; invs h2. -Qed.*) +Qed. -(*Lemma LastA_SingletonT_unfold : forall u, u ->> LastA ([|u|]). +Lemma LastA_SingletonT_unfold : forall u, u ->> LastA ([|u|]). Proof. move => u a h0. exists (Tnil a); split. - exact: nil_singletonT. - exact: finalTA_nil. -Qed.*) +Qed. -(*Lemma lastA_appendA : forall p q a, lastA (appendT p q) a -> lastA q a. +Lemma lastA_appendA : forall p q a, lastA (appendT p q) a -> lastA q a. Proof. move => p q a [tr0 [[tr [_ h2]] h1]]. move: h1 tr h2; elim => {tr0 a} [a|a b a' tr0 Hfinal IH] tr h0; invs h0. - exists (Tnil a). by split; last by apply: finalTA_nil. - exists (Tcons a b tr0). by split; last by apply: finalTA_delay. - exact: IH _ H1. -Qed.*) +Qed. Lemma LastA_AppendA : forall p v, LastA (p *** [|v|]) ->> v. Proof. @@ -1006,16 +1006,16 @@ move: h1 tr' h0; elim => {tr a} [a|a b a' tr Hfinal IH] tr0 h0; invs h0. - exact: IH _ H1. Qed. -(*Lemma LastA_andA : forall p u, ((LastA p) andA u) ->> LastA (p *** [|u|]). +Lemma LastA_andA : forall p u, ((LastA p) andA u) ->> LastA (p *** [|u|]). Proof. move => [p hp] u a [[tr0 [h2 h3]] h1]. exists tr0. split => //. exists tr0. split => //. move: {h2} tr0 a h3 h1. cofix CIH. move => tr0 a h0; invs h0 => h0. - exact/followsT_nil/nil_singletonT. - exact: followsT_delay _ _ (CIH _ _ H h0). -Qed.*) +Qed. -(*Lemma LastA_IterA : forall v b p, +Lemma LastA_IterA : forall v b p, LastA ([|v|] *** (IterT (p *** <>))) ->> v. Proof. move => v b p a h0. @@ -1023,9 +1023,9 @@ have h1: p =>> TtT by []. have h2 := LastA_cont (AppendT_cont_R (IterT_cont (AppendT_cont_L h1))) h0. have := LastA_cont (@IterT_DupT v b) h2. exact: LastA_AppendA. -Qed.*) +Qed. -(*Lemma IterT_LastA_DupT : forall v b, +Lemma IterT_LastA_DupT : forall v b, (<> *** (IterT (TtT *** <>))) =>> (TtT *** [|v|]). Proof. move => v b tr0 [tr1 [[a [h0 h2]] h1]]. @@ -1040,9 +1040,9 @@ move: tr' h0 H1. cofix CIH. move => tr0 h0 h1; invs h1. invs h2; invs H1; invs h1; invs H3. exact/followsT_delay/CIH. + invs h1. exact: followsT_delay _ _ (CIH0 _ _ _ H H4). -Qed.*) +Qed. -(*Lemma LastA_LastA : forall p q, +Lemma LastA_LastA : forall p q, (LastA ([|LastA p|] *** q)) ->> (LastA (p *** q)). Proof. move => [p hp] [q hq] a /= [tr1 [[tr0 [[tr2 [h0 h3]] h2]] h1]]; invs h3; invs h2. @@ -1060,16 +1060,16 @@ exists (tr2 +++ tr1). split. + rewrite trace_append_cons. apply: finalTA_delay. exact: IH _ h0 h1. -Qed.*) +Qed. -(*Lemma SingletonT_andA_AppendT : forall u v, +Lemma SingletonT_andA_AppendT : forall u v, (v andA u) ->> LastA ([|v|] *** [|u|]). Proof. move => u v a [h0 h1]. exists (Tnil a); split; last by apply: finalTA_nil. exists (Tnil a); split; first by apply: nil_singletonT. exact/followsT_nil/nil_singletonT. -Qed.*) +Qed. CoFixpoint lastdup (tr : trace) (b : B) : trace := match tr with @@ -1077,10 +1077,10 @@ match tr with | Tcons a b' tr' => Tcons a b' (lastdup tr' b) end. -(*Lemma lastdup_hd: forall tr b, hd tr = hd (lastdup tr b). +Lemma lastdup_hd: forall tr b, hd tr = hd (lastdup tr b). Proof. by case => [a b|a b tr b0]; rewrite [lastdup _ _]trace_destr. -Qed.*) +Qed. Lemma followsT_dupT : forall u tr b, followsT (singletonT u) tr tr -> @@ -1105,7 +1105,7 @@ move => tr a b1; elim => {tr a} [a|a1 b2 a2 tr Hfinal IH]. exact: finalTA_delay. Qed. -(*Lemma LastA_DupT : forall p u b, +Lemma LastA_DupT : forall p u b, LastA (p *** [|u|]) ->> LastA (p *** <>). Proof. move => [p hp] u b a [tr0 [[tr1 [h0 h2]] h1]]. @@ -1115,7 +1115,7 @@ exists tr0; split. - exact: hp _ h0 _ h3. - have h4 := followsT_setoidT (@singletonT_setoidT _) h2 h3 (bisim_refl _) => {h2}. exact: followsT_dupT b h4. -Qed.*) +Qed. (** ** Midpoint property *) From d1b44edb2411552b8a025f085ae917fe37615daa Mon Sep 17 00:00:00 2001 From: Dafina Trufas Date: Thu, 4 Aug 2022 09:54:24 +0300 Subject: [PATCH 18/18] Addressing reviews --- theories/VLSM/Lib/FinSetExtras.v | 8 ++++ theories/VLSM/Lib/ListSetExtras.v | 45 +++++++++++++++++++ theories/VLSM/Lib/SsrExport.v | 2 +- theories/VLSM/Lib/StdppExtras.v | 41 +++++++++++++++++ theories/VLSM/Lib/TopSort.v | 74 +++++++++++++++++++++++++++++++ 5 files changed, 169 insertions(+), 1 deletion(-) diff --git a/theories/VLSM/Lib/FinSetExtras.v b/theories/VLSM/Lib/FinSetExtras.v index 0f133359..61bbc1c1 100644 --- a/theories/VLSM/Lib/FinSetExtras.v +++ b/theories/VLSM/Lib/FinSetExtras.v @@ -58,6 +58,14 @@ Proof. lia. Qed. +Lemma intersection_size1 + (X Y : C) : + size (X ∩ Y) <= size X. +Proof. + apply (subseteq_size (X ∩ Y) X). + set_solver. +Qed. + Lemma intersection_size2 (X Y : C) : size (X ∩ Y) <= size Y. diff --git a/theories/VLSM/Lib/ListSetExtras.v b/theories/VLSM/Lib/ListSetExtras.v index d2dc0779..fc72bd5d 100644 --- a/theories/VLSM/Lib/ListSetExtras.v +++ b/theories/VLSM/Lib/ListSetExtras.v @@ -27,6 +27,13 @@ Proof. by intros s1 s2 []. Qed. +Lemma set_eq_proj2 {A} : forall (s1 s2 : set A), + set_eq s1 s2 -> + s2 ⊆ s1. +Proof. + by intros s1 s2 []. +Qed. + Lemma set_eq_refl {A} : forall (s : list A), set_eq s s. Proof. by induction s. @@ -69,12 +76,31 @@ Proof. firstorder. Qed. +Lemma set_eq_Forall + {A : Type} + (s1 s2 : set A) + (H12 : set_eq s1 s2) + (P : A -> Prop) + : Forall P s1 <-> Forall P s2. +Proof. + rewrite !Forall_forall. firstorder. +Qed. + Lemma set_union_comm `{EqDecision A} : forall (s1 s2 : list A), set_eq (set_union s1 s2) (set_union s2 s1). Proof. intros s1 s2; split; intro x; rewrite !set_union_iff; itauto. Qed. +Lemma set_union_empty `{EqDecision A} : forall (s1 s2 : list A), + set_union s1 s2 = [] -> + s1 = [] /\ s2 = []. +Proof. + intros. + destruct s2; [done |]. + by cbn in H; apply set_add_not_empty in H. +Qed. + Lemma set_union_nodup_left `{EqDecision A} (l l' : set A) : NoDup l -> NoDup (set_union l l'). Proof. @@ -234,6 +260,25 @@ Proof. - rewrite IHl; [| done]. by destruct (decide (x = hd)). Qed. +Lemma set_add_new `{EqDecision A}: + forall (x:A) l, ~x ∈ l -> set_add x l = l++[x]. +Proof. + induction l; cbn; [done |]; intros H_not_in. + rewrite decide_False; cycle 1. + - by intros ->; apply H_not_in; left. + - rewrite elem_of_cons in H_not_in. rewrite IHl; itauto. +Qed. + +Lemma set_remove_not_elem_of `{EqDecision A} : forall x (s : list A), + ~ x ∈ s -> + set_remove x s = s. +Proof. + induction s; cbn; intros; [done |]. + rewrite decide_False; cycle 1. + + by intros ->; contradict H; left. + + rewrite IHs; [done |]. rewrite elem_of_cons in H. itauto. +Qed. + Lemma set_remove_elim `{EqDecision A} : forall x (s : list A), NoDup s -> ~ x ∈ (set_remove x s). Proof. diff --git a/theories/VLSM/Lib/SsrExport.v b/theories/VLSM/Lib/SsrExport.v index 30ba8c57..40fa561a 100644 --- a/theories/VLSM/Lib/SsrExport.v +++ b/theories/VLSM/Lib/SsrExport.v @@ -4,4 +4,4 @@ From Coq Require Export ssreflect. #[export] Set SsrOldRewriteGoalsOrder. #[export] Set Asymmetric Patterns. #[export] Set Bullet Behavior "None". - +Definition iYC2 := True. diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v index cb9f3483..dbc702a8 100644 --- a/theories/VLSM/Lib/StdppExtras.v +++ b/theories/VLSM/Lib/StdppExtras.v @@ -145,6 +145,25 @@ Proof. by rewrite existsb_Exists, <- Forall_Exists_neg, Forall_forall. Qed. +Lemma existsb_first + {A : Type} + (l : list A) + (f : A -> bool) + (Hsomething : existsb f l = true) : + exists (prefix : list A) + (suffix : list A) + (first : A), + (f first = true) /\ + l = prefix ++ [first] ++ suffix /\ + (existsb f prefix = false). +Proof. + setoid_rewrite <-not_true_iff_false. + setoid_rewrite existsb_Exists. + apply Exists_first. + - typeclasses eauto. + - by apply existsb_Exists. +Qed. + (* Returns all elements X of l such that X does not compare less than any other element w.r.t to the precedes relation *) @@ -628,3 +647,25 @@ Proof. rewrite contra in H0. destruct H0; inversion H0. Qed. + +(** + When a list contains two elements, either they are equal or we can split + the list into three parts separated by the elements (and this can be done + in two ways, depending on the order of the elements). +*) +Lemma elem_of_list_split_2 : + forall {A : Type} (l : list A) (x y : A), + x ∈ l -> y ∈ l -> + x = y \/ exists l1 l2 l3 : list A, + l = l1 ++ x :: l2 ++ y :: l3 \/ l = l1 ++ y :: l2 ++ x :: l3. +Proof. + intros A x y l Hx Hy. + apply elem_of_list_split in Hx as (l1 & l2 & ->). + rewrite elem_of_app, elem_of_cons in Hy. + destruct Hy as [Hy | [-> | Hy]]; [| by left |]. + - apply elem_of_list_split in Hy as (l11 & l12 & ->). + right; exists l11, l12, l2; right; cbn. + by rewrite <- app_assoc. + - apply elem_of_list_split in Hy as (l21 & l22 & ->). + by right; exists l1, l21, l22; left; cbn. +Qed. diff --git a/theories/VLSM/Lib/TopSort.v b/theories/VLSM/Lib/TopSort.v index cad25df0..902a93f7 100644 --- a/theories/VLSM/Lib/TopSort.v +++ b/theories/VLSM/Lib/TopSort.v @@ -135,6 +135,21 @@ Proof. by destruct (decide (precedes a a)). Qed. +Lemma precedes_asymmetric + (a b : A) + (Ha : P a) + (Hb : P b) + (Hab : precedes a b) + : ~ precedes b a. +Proof. + intro Hba. + exact + (StrictOrder_Asymmetric Hso + (exist P a Ha) (exist P b Hb) + Hab Hba + ). +Qed. + Lemma precedes_transitive (a b c : A) (Ha : P a) @@ -321,6 +336,22 @@ Proof. right; left. Qed. +Corollary top_sort_precedes + (a b : A) + (Hab : precedes a b) + (Ha : a ∈ l) + (Hb : b ∈ l) + : exists l1 l2 l3, l = l1 ++ [a] ++ l2 ++ [b] ++ l3. +Proof. + apply elem_of_list_split in Hb. + destruct Hb as [l12 [l3 Hb']]. + specialize (top_sort_before a b Hab Ha l12 l3 Hb'). + intros Ha12. apply elem_of_list_split in Ha12. + destruct Ha12 as [l1 [l2 Ha12]]. + subst l12. + exists l1, l2, l3. by rewrite Hb', <- app_assoc. +Qed. + End topologically_sorted_fixed_list. End topologically_sorted. @@ -726,4 +757,47 @@ Proof. by intro; apply Forall_forall. Qed. +Corollary simple_topologically_sorted_precedes_closed_remove_last + (l : list A) + (Hts : topologically_sorted precedes l) + (init : list A) + (final : A) + (Hinit : l = init ++ [final]) + (Hpc : precedes_closed precedes l) + : precedes_closed precedes init. +Proof. + eapply topologically_sorted_precedes_closed_remove_last; + [typeclasses eauto | apply Forall_True | done..]. +Qed. + +Corollary simple_top_sort_correct : forall l, + topological_sorting precedes l (top_sort precedes l). +Proof. + intro; eapply top_sort_correct; [typeclasses eauto | apply Forall_True]. +Qed. + +Corollary simple_maximal_element_in l + (a : A) + (Hmax : get_maximal_element precedes l = Some a) : + a ∈ l. +Proof. + eapply maximal_element_in; [typeclasses eauto | apply Forall_True | done]. +Qed. + +Corollary simple_get_maximal_element_correct l + (a max : A) + (Hina : a ∈ l) + (Hmax : get_maximal_element precedes l = Some max) : + ~ precedes max a. +Proof. + eapply get_maximal_element_correct; [typeclasses eauto | apply Forall_True | done..]. +Qed. + +Corollary simple_get_maximal_element_some + l (Hne : l <> []) : + exists a, get_maximal_element precedes l = Some a. +Proof. + eapply get_maximal_element_some; [apply Forall_True | done]. +Qed. + End sec_simple_top_sort.