diff --git a/CaseStudies/Gathering/Definitions.v b/CaseStudies/Gathering/Definitions.v index c144450b85e8f43e5dcaa5421c887b3c94df78f0..c36036550495c4449d146da111ec430c85a1d5ed 100644 --- a/CaseStudies/Gathering/Definitions.v +++ b/CaseStudies/Gathering/Definitions.v @@ -43,7 +43,7 @@ Context `{inactive_choice}. Context {UpdFun : update_function _ _ _}. Context {InaFun : inactive_function _}. -Notation "!!" := (fun config => obs_from_config config origin). +(* Notation "!!" := (fun config => obs_from_config config origin). *) (** [gathered_at conf pt] means that in configuration [conf] all good robots are at the same location [pt] (exactly). *) diff --git a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v index d17e0aa2aed237d385f7889bfc765f5c6cac2a72..7882e3c0c72defc1796d99819a4a6de3b202fbe9 100644 --- a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v +++ b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v @@ -86,6 +86,61 @@ Ltac rename_hyp ::= rename_hyp_2. End LibHyps_stuff.*) +(* Preventing coq bug https://github.com/coq/coq/issues/19861 from +biting us at "Print Assumptions". This takes precedence over the +"abstract lia" hints. + +To check hints: +Print Hint *. + + *) +#[local] +Hint Extern 9 (_ = _ :>nat) => lia: zarith. +#[local] +Hint Extern 9 (_ <= _) => lia: zarith. +#[local] +Hint Extern 9 (_ < _) => lia: zarith. +#[local] +Hint Extern 9 (_ >= _) => lia: zarith. +#[local] +Hint Extern 9 (_ > _) => lia: zarith. + +#[local] +Hint Extern 9 (_ <> _ :>nat) => lia: zarith. +#[local] +Hint Extern 9 (~ _ <= _) => lia: zarith. +#[local] +Hint Extern 9 (~ _ < _) => lia: zarith. +#[local] +Hint Extern 9 (~ _ >= _) => lia: zarith. +#[local] +Hint Extern 9 (~ _ > _) => lia: zarith. + +#[local] +Hint Extern 9 (_ = _ :>Z) => lia: zarith. +#[local] +Hint Extern 9 (_ <= _)%Z => lia: zarith. +#[local] +Hint Extern 9 (_ < _)%Z => lia: zarith. +#[local] +Hint Extern 9 (_ >= _)%Z => lia: zarith. +#[local] +Hint Extern 9 (_ > _)%Z => lia: zarith. + +#[local] +Hint Extern 9 (_ <> _ :>Z) => lia: zarith. +#[local] +Hint Extern 9 (~ (_ <= _)%Z) => lia: zarith. +#[local] +Hint Extern 9 (~ (_ < _)%Z) => lia: zarith. +#[local] +Hint Extern 9 (~ (_ >= _)%Z) => lia: zarith. +#[local] +Hint Extern 9 (~ (_ > _)%Z) => lia: zarith. + +#[local] +Hint Extern 9 False => lia: zarith. + Set Implicit Arguments. Close Scope R_scope. @@ -323,7 +378,7 @@ Qed. Lemma weber_calc_seg_correct_2 : forall c w1 w2, weber_calc_seg (pos_list c) = (w1, w2) -> forall w, Weber (pos_list c) w <-> segment w1 w2 w. -Proof. +Proof using lt_0n. intros c w1 w2 H w. apply weber_calc_seg_correct_1;auto. apply pos_list_non_nil. @@ -397,7 +452,7 @@ unfold pos_list. rewrite (@InA_map_iff _ _ equiv equiv) ; autoclass. Qed. Lemma n_nGnB: n = nG + nB. -Proof. +Proof using Type. rewrite <- names_length. assert (config:configuration). { red. @@ -421,7 +476,7 @@ Qed. Lemma n_nG: n = nG. -Proof. +Proof using lt_0n. rewrite n_nGnB. rewrite nB_eq_0. lia. @@ -594,7 +649,7 @@ Lemma list_perm_find_none: Proper (equiv ==> equiv) f -> find f l = None -> find f l' = None. -Proof. +Proof using Type. intros A SA f l l' H HProper H0. specialize find_none with (1:=H0) as H0'. destruct (find f l') eqn:heq_find. @@ -719,17 +774,17 @@ Proof using Type. apply cardinal_obs_from_config. Qed. - Lemma invalid_config_obs: forall c info, invalid c <-> invalid_obs ((obs_from_config c info)). -Proof using Type. +Proof using lt_0n. intros c i. split;[intros h | intros h]. - red in h . decompose [ex and] h. clear h. red. rewrite n_cardinal. - exists x , x0;intuition. + exists x , x0. + repeat split;intuition. - red. (* specialize (h (0%VS, 0%VS, ratio_0)). *) red in h. @@ -738,7 +793,6 @@ Proof using Type. exists x , x0;intuition. Qed. - Lemma fold_left_st_snd: forall T `{FMS: FMapInterface.FMapSpecs T} l o n, (forall xn : T * nat, InA eq_pair xn l -> o[fst xn] = snd xn /\ snd xn > 0) -> List.fold_left (fun (acc : nat) (xn : T * nat) => snd xn + acc) l n = @@ -791,6 +845,10 @@ Proof using. reflexivity. + intros x y z. lia. +(* rewrite Nat.add_assoc. + setoid_rewrite Nat.add_comm at 2. + rewrite Nat.add_assoc. + reflexivity.*) + symmetry. eapply support_map_elements. + reflexivity. @@ -852,6 +910,10 @@ Proof using Type. apply Exp_prop.div2_not_R0. clear lt_0n. (* otherwise it is used by lia *) lia. +(* rewrite Nat.add_1_r. + apply -> Nat.succ_lt_mono. + now apply Nat.neq_0_lt_0. + (*lia. (* otherwise it is used by lia *)*)*) Qed. Lemma elements_subset: forall (o:multiset location) l l', @@ -859,7 +921,7 @@ Lemma elements_subset: forall (o:multiset location) l l', is_elements (l++l') -> PermutationA equiv (elements o) (l ++ l') -> Subset (from_elements l) o. -Proof. +Proof using Type. intros o l l' hnodup hperm. foldR2. @@ -881,7 +943,7 @@ Qed. Lemma doubleton_subset: forall o (x y : location), x =/= y -> Subset (from_elements ((x,o[x]):: (y,o[y]) :: nil)) o. -Proof. +Proof using Type. intros o x y H0. assert (filter (fun a:location => mem (location_EqDec) a (x :: (y :: nil))) o == (from_elements ((x,o[x]):: (y,o[y]) :: nil))). { cbn [from_elements]. @@ -919,7 +981,7 @@ Lemma tripleton_subset: forall o (x y z : location), -> x =/= z -> y =/= z -> Subset (from_elements ((x,o[x]):: (y,o[y]) :: (z,o[z]):: nil)) o. -Proof. +Proof using Type. intros o x y z hxy hxz hyz. assert (h_filter: @@ -991,7 +1053,7 @@ Lemma support_mult_pos: {FM: FMultisetsOn elt Ops}, forall ms x, InA equiv x (support ms) <-> ms[x]>0. -Proof. +Proof using Type. clear lt_0n. intros. split. @@ -1016,7 +1078,7 @@ Lemma remove_all_cardinal_plus: forall {elt : Type} {S0 : Setoid elt} {H : EqDec S0} {Ops : FMOps elt H} {FM: FMultisetsOn elt Ops}, forall (x : elt) (m : multiset elt), cardinal (remove_all x m) + m[x] = cardinal m. -Proof. +Proof using Type. clear lt_0n delta_g0 delta n. intros elt S0 H Ops h_FMultisetsOn_Ops_ x m . assert (m[x] <= cardinal m). @@ -1032,7 +1094,7 @@ Lemma obs_invalid_doubleton1: x =/= y -> o[x] + o[y] >= (cardinal o) -> forall z, z =/= x -> z =/= y -> o[z]=0. -Proof. +Proof using Type. clear lt_0n. intros elt S0 H Ops h_FMultisetsOn_Ops_ o x y h_nequiv_x_y_ h_ge_add_mult_mult_card_o_ z h_nequiv_z_x_ h_nequiv_z_y_ . specialize remove_all_cardinal_plus with (x:=x)(m:=o). @@ -1063,7 +1125,7 @@ Lemma obs_invalid_doubleton2: -> o[y] > 0 -> o[x] + o[y] >= (cardinal o) -> PermutationA equiv (support o) (x::y::nil). -Proof. +Proof using Type. clear lt_0n delta_g0 delta n. intros elt S0 H Ops h_FMultisetsOn_Ops_ o x y h_nequiv_x_y_ h_gt_mult_x_o_0_ h_gt_mult_y_o_0_ h_ge_add_mult_mult_card_o_ . specialize (obs_invalid_doubleton1 _ h_nequiv_x_y_ h_ge_add_mult_mult_card_o_). @@ -1131,7 +1193,7 @@ Lemma support_div2_split: forall o x y, o[x] = Nat.div2 (cardinal o + 1) -> o[y] = Nat.div2 (cardinal o + 1) -> o[x] + o[y] >= cardinal o. -Proof. +Proof using Type. clear lt_0n delta_g0 delta n. intros elt S0 H Ops h_FMultisetsOn_Ops_ o x y h_eq_mult_x_o_div2_add_ h_eq_mult_y_o_div2_add_ . specialize div2_sum_p1_ge with (n:=cardinal o). @@ -1147,7 +1209,7 @@ Lemma obs_invalid_doubleton (o:observation): /\ o[x] = Nat.div2 (cardinal o + 1) /\ o[y] = Nat.div2 (cardinal o + 1) /\ forall z, z =/= x -> z =/= y -> o[z]=0. -Proof. +Proof using Type. clear lt_0n. intros h. unfold invalid_obs in h. @@ -1173,7 +1235,7 @@ Proof. Qed. Lemma NoDupA_2fst: forall [A : Type] (eqA : relation A) (x y: A) l, NoDupA eqA (x::y::l) -> ~ eqA x y. -Proof. +Proof using Type. intros A eqA x y l H. inversion H;subst. intro abs. @@ -1322,7 +1384,7 @@ Lemma obs_invalid_dec_compat_left: forall o o': observation, forall h, obs_invalid_dec o = left h -> exists h', obs_invalid_dec o' = left h'. -Proof. +Proof using Type. intros o o' h_equiv_o_o'_ h_invalid_obs_o_ h_eq_obs_invalid_dec_left_ . destruct (obs_invalid_dec o') as [h_invalid_obs_o'_ | h_not_invalid_obs_ ] eqn:h_eq_obs_invalid_dec_ ;eauto. foldR2. @@ -1337,7 +1399,7 @@ Lemma obs_invalid_dec_compat_right: forall o o': observation, forall h, obs_invalid_dec o = right h -> exists h', obs_invalid_dec o' = right h'. -Proof. +Proof using Type. intros o o' h_equiv_o_o'_ h_not_invalid_obs_ h_eq_obs_invalid_dec_right_ . destruct (obs_invalid_dec o') eqn:h_eq_obs_invalid_dec_;eauto. foldR2. @@ -1473,7 +1535,7 @@ Qed. Lemma multi_support_non_nil2 (config : configuration): multi_support (!! config) <> []. -Proof. +Proof using lt_0n. intro abs. specialize (@multi_support_config config) as h. foldR2. @@ -1758,7 +1820,7 @@ Lemma multi_set_length_cardinal: forall {elt : Type} {S0 : Setoid elt} {H : EqDec S0} {Ops : FMOps elt H} {FM: FMultisetsOn elt Ops}, forall o, length (multi_support o) = cardinal o. -Proof. +Proof using lt_0n. intros elt S0 H Ops FM o. (* rewrite cardinal_map_support. *) @@ -2270,7 +2332,7 @@ assert ( invalid_obs obs -> invalid_obs (obs_from_config config (config (Good g) rewrite map_cardinal;try typeclasses eauto. rewrite n_cardinal. reflexivity. - -- apply injective. + -- apply Bijection.injective. * rewrite n_cardinal. assert (y == (sim (sim â»Â¹ y))) as h_eq'. { rewrite (Bijection.section_retraction sim y). @@ -2281,7 +2343,7 @@ assert ( invalid_obs obs -> invalid_obs (obs_from_config config (config (Good g) rewrite map_cardinal;try typeclasses eauto. rewrite n_cardinal. reflexivity. - -- apply injective. + -- apply Bijection.injective. * apply f_compat. } assert (Hmult : robot_with_mult (Nat.div2 (cardinal obs+1)) (multi_support obs) == option_map sim (robot_with_mult (Nat.div2 (n+1)) (pos_list config))). @@ -3043,7 +3105,7 @@ ps <> nil -> (forall w : R2, Weber ps w <-> segment w1 w2 w) -> w1 =/= w2 -> line_dir L =/= 0%VS. -Proof. +Proof using Type. intros h_nonnil h_align h_web_seg h_neq. apply (line_dir_nonnul _ w1 w2). - apply h_neq. @@ -4406,7 +4468,7 @@ unfold measure. case (get_location (c id) =?= (middle r1 r2)) as [Hloc | Hloc]. Qed. Lemma inv4_diff c L w1 w2: inv4 c L w1 w2 -> w1 =/= w2. -Proof. +Proof using Type. intros Hinv4. intros Ew12. rewrite Ew12 in Hinv4. unfold inv4 in Hinv4. @@ -4415,7 +4477,7 @@ Proof. Qed. Lemma inv3_diff c L w1 w2: inv3 c L w1 w2 -> w1 =/= w2. -Proof. +Proof using Type. intros Hinv3. red in Hinv3. decompose [and] Hinv3; clear Hinv3. diff --git a/_CoqProject b/_CoqProject index efb8a74d63cd6ad2977f542b926581a50bd25049..a3d6ed3bb38e551f0bc1a494d475508ba6b31132 100644 --- a/_CoqProject +++ b/_CoqProject @@ -119,7 +119,7 @@ CaseStudies/Gathering/InR2/Weber/Align_flex_ssync.v CaseStudies/Gathering/InR2/Weber/Align_flex_async.v CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v # Seg Fault? -# CaseStudies/Gathering/InR2/Weber/Gather_flex_async_Assumptions.v +CaseStudies/Gathering/InR2/Weber/Gather_flex_async_Assumptions.v ## Case Study: Ring Exploration