From 29cefdb316bdc7aee4b04b5b86a08fe58ee3a8ac Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 28 Oct 2023 18:46:27 +0200 Subject: [PATCH] fix deprecations of intuition auto with star --- theories/Raft/DecompositionWithPostState.v | 37 ++++--- theories/Raft/Linearizability.v | 8 +- theories/Raft/RaftLinearizableProofs.v | 25 ++--- theories/Raft/RefinementSpecLemmas.v | 8 +- theories/Raft/SpecLemmas.v | 22 ++-- .../RaftProofs/AllEntriesLeaderSublogProof.v | 4 +- theories/RaftProofs/AllEntriesLogProof.v | 97 +++++++---------- .../RaftProofs/AllEntriesTermSanityProof.v | 2 +- .../RaftProofs/AllEntriesVotesWithLogProof.v | 12 +-- .../RaftProofs/AppendEntriesLeaderProof.v | 3 +- .../AppendEntriesReplySublogProof.v | 5 +- .../AppendEntriesRequestLeaderLogsProof.v | 8 +- ...ndEntriesRequestReplyCorrespondenceProof.v | 60 ++++++----- .../AppendEntriesRequestTermSanityProof.v | 1 - ...ppendEntriesRequestsCameFromLeadersProof.v | 6 +- .../RaftProofs/AppliedEntriesMonotonicProof.v | 32 +++--- .../RaftProofs/AppliedImpliesInputProof.v | 4 +- theories/RaftProofs/CandidateEntriesProof.v | 13 +-- .../RaftProofs/CausalOrderPreservedProof.v | 7 +- theories/RaftProofs/CroniesCorrectProof.v | 10 +- theories/RaftProofs/CroniesTermProof.v | 8 +- theories/RaftProofs/CurrentTermGtZeroProof.v | 2 +- theories/RaftProofs/GhostLogAllEntriesProof.v | 2 +- theories/RaftProofs/GhostLogCorrectProof.v | 2 +- theories/RaftProofs/InputBeforeOutputProof.v | 37 +++---- .../LastAppliedCommitIndexMatchingProof.v | 12 +-- .../LastAppliedLeCommitIndexProof.v | 2 +- theories/RaftProofs/LeaderCompletenessProof.v | 4 +- .../RaftProofs/LeaderLogsContiguousProof.v | 2 +- .../RaftProofs/LeaderLogsLogMatchingProof.v | 9 +- .../RaftProofs/LeaderLogsPreservedProof.v | 2 +- theories/RaftProofs/LeaderLogsSublogProof.v | 4 +- .../RaftProofs/LeaderLogsTermSanityProof.v | 30 +++--- theories/RaftProofs/LogMatchingProof.v | 58 +++++----- theories/RaftProofs/LogsLeaderLogsProof.v | 12 ++- .../RaftProofs/MatchIndexAllEntriesProof.v | 6 +- .../RaftProofs/OneLeaderLogPerTermProof.v | 2 +- theories/RaftProofs/OutputCorrectProof.v | 16 +-- theories/RaftProofs/OutputGreatestIdProof.v | 6 +- .../RaftProofs/OutputImpliesAppliedProof.v | 6 +- theories/RaftProofs/PrefixWithinTermProof.v | 26 ++--- .../RaftProofs/PrevLogLeaderSublogProof.v | 5 +- theories/RaftProofs/RaftMsgRefinementProof.v | 45 ++++---- theories/RaftProofs/RaftRefinementProof.v | 28 ++--- .../RequestVoteReplyMoreUpToDateProof.v | 7 +- .../RequestVoteReplyTermSanityProof.v | 2 +- .../RaftProofs/RequestVoteTermSanityProof.v | 2 +- theories/RaftProofs/SortedProof.v | 21 ++-- .../RaftProofs/StateMachineCorrectProof.v | 8 +- .../RaftProofs/StateMachineSafetyPrimeProof.v | 11 +- theories/RaftProofs/StateMachineSafetyProof.v | 100 ++++++++---------- theories/RaftProofs/TermSanityProof.v | 29 ++--- .../TermsAndIndicesFromOneLogProof.v | 2 +- theories/RaftProofs/TransitiveCommitProof.v | 2 +- .../RaftProofs/VotedForMoreUpToDateProof.v | 4 +- theories/RaftProofs/VotesLeCurrentTermProof.v | 2 +- .../RaftProofs/VotesWithLogTermSanityProof.v | 2 +- 57 files changed, 445 insertions(+), 437 deletions(-) diff --git a/theories/Raft/DecompositionWithPostState.v b/theories/Raft/DecompositionWithPostState.v index 59f8d55..85d3741 100644 --- a/theories/Raft/DecompositionWithPostState.v +++ b/theories/Raft/DecompositionWithPostState.v @@ -195,7 +195,8 @@ Section DecompositionWithPostState. nwPackets := (send_packets (pDst p) (l0 ++ l1)) ++ xs ++ ys; nwState := (update name_eq_dec (update name_eq_dec (nwState net) (pDst p) r) (pDst p) r0) |}) by (eapply RIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| + in_crush_tac (intuition (auto with datatypes))]). assert (HREACH3 : raft_intermediate_reachable {| @@ -205,11 +206,12 @@ Section DecompositionWithPostState. { eapply RIR_doGenericServer; eauto. - simpl in *. break_if; try congruence; eauto. - intros. simpl. - repeat do_in_app. intuition; try solve [in_crush]. + repeat do_in_app. intuition auto; + try solve [in_crush_tac (intuition (auto with datatypes))]. simpl in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. - + left. in_crush. left. in_crush. - + left. in_crush. left. in_crush. + + left. in_crush. left. in_crush_tac (intuition auto). + + left. in_crush. left. in_crush_tac (intuition auto). + in_crush. } eapply_prop raft_net_invariant_do_generic_server'. eauto. eapply_prop raft_net_invariant_do_leader'. eauto. @@ -223,7 +225,7 @@ Section DecompositionWithPostState. apply HREACH2. simpl. break_if; intuition eauto. intros. simpl. repeat break_if; subst; eauto. - simpl. in_crush. auto. + simpl. in_crush_tac (intuition (auto with datatypes)). auto. { simpl in HREACH3. match goal with @@ -241,11 +243,12 @@ Section DecompositionWithPostState. repeat rewrite update_neq by auto; auto. simpl. intros. simpl. - repeat do_in_app. intuition; try solve [in_crush]. + repeat do_in_app. intuition auto; + try solve [in_crush_tac (intuition auto with datatypes)]. simpl in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. - * left. in_crush. left. in_crush. - * left. in_crush. left. in_crush. + * left. in_crush. left. in_crush_tac (intuition auto). + * left. in_crush. left. in_crush_tac (intuition auto). * in_crush. + unfold RaftInputHandler in *. repeat break_let. repeat find_inversion. @@ -261,7 +264,7 @@ Section DecompositionWithPostState. nwPackets := (send_packets h (l0 ++ l2)) ++ (nwPackets net); nwState := (update name_eq_dec (update name_eq_dec (nwState net) h r) h r0) |}) by (eapply RIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| in_crush_tac (intuition (auto with datatypes))]). assert (HREACH3 : raft_intermediate_reachable {| @@ -271,11 +274,12 @@ Section DecompositionWithPostState. { eapply RIR_doGenericServer; eauto. - simpl in *. break_if; try congruence; eauto. - intros. simpl. - repeat do_in_app. intuition; try solve [in_crush]. + repeat do_in_app. intuition auto; + try solve [in_crush_tac (intuition (auto with datatypes))]. simpl in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. - + left. in_crush. left. in_crush. - + left. in_crush. left. in_crush. + + left. in_crush. left. in_crush_tac (intuition auto). + + left. in_crush. left. in_crush_tac (intuition auto). + in_crush. } eapply_prop raft_net_invariant_do_generic_server'. eauto. eapply_prop raft_net_invariant_do_leader'. eauto. @@ -288,7 +292,7 @@ Section DecompositionWithPostState. auto. apply HREACH2. simpl. break_if; intuition eauto. - eauto. simpl. in_crush. + eauto. simpl. in_crush_tac (intuition (auto with datatypes)). auto. { simpl in HREACH3. @@ -303,11 +307,12 @@ Section DecompositionWithPostState. simpl. break_if; congruence. simpl. intros. repeat break_if; subst; eauto. intros. simpl. - repeat do_in_app. intuition; try solve [in_crush]. + repeat do_in_app. intuition auto; + try solve [in_crush_tac (intuition (auto with datatypes))]. simpl in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. - * left. in_crush. left. in_crush. - * left. in_crush. left. in_crush. + * left. in_crush. left. in_crush_tac (intuition auto). + * left. in_crush. left. in_crush_tac (intuition auto). * in_crush. + match goal with | [ H : nwPackets ?net = _ |- _ {| nwPackets := ?ps ; nwState := ?st |} ] => diff --git a/theories/Raft/Linearizability.v b/theories/Raft/Linearizability.v index 55f8c7a..90f59a5 100644 --- a/theories/Raft/Linearizability.v +++ b/theories/Raft/Linearizability.v @@ -1062,7 +1062,7 @@ Section Linearizability. In (I k) (xs ++ ys). Proof using. intros. - apply in_middle_reduce with (y := I k'); intuition. + apply in_middle_reduce with (y := I k'); intuition (auto with datatypes). find_inversion. auto using get_IR_output_keys_complete_U. Qed. @@ -1332,12 +1332,12 @@ Section Linearizability. * eauto using subseq_NoDup, subseq_get_op_input_keys, subseq_2_3. * eauto using subseq_NoDup, subseq_get_op_output_keys, subseq_2_3. + simpl. intuition congruence. - + intuition. + + intuition (auto with datatypes). } * { break_if. - simpl in *. intuition (try congruence). exfalso. eauto using get_IR_output_keys_complete_U. - - exfalso. apply n. red. intuition. + - exfalso. apply n. red. intuition (auto with datatypes). } - (* IRU case. *) match goal with @@ -1370,7 +1370,7 @@ Section Linearizability. break_if. * exfalso. intuition eauto using in_middle_insert, in_cons, in_eq, acknowledged_op_defn. - * rewrite if_decider_true by intuition. + * rewrite if_decider_true by intuition (auto with datatypes). { constructor. constructor. rewrite acknowledge_all_ops_func_target_ext_strong with (t' := ir). - apply IHP; auto. diff --git a/theories/Raft/RaftLinearizableProofs.v b/theories/Raft/RaftLinearizableProofs.v index 2443e71..4592663 100644 --- a/theories/Raft/RaftLinearizableProofs.v +++ b/theories/Raft/RaftLinearizableProofs.v @@ -338,10 +338,10 @@ Section RaftLinearizableProofs. intros. induction log; simpl in *; intuition. - subst. break_exists. - repeat break_match; intuition. + repeat break_match; intuition (auto with datatypes). simpl in *. subst. congruence. - - repeat break_match; in_crush. + - repeat break_match; in_crush_tac (intuition (auto with datatypes)). Qed. Theorem In_get_output' : @@ -450,7 +450,7 @@ Section RaftLinearizableProofs. In (I k) (import tr). Proof using. induction tr; intros; simpl in *; intuition; subst. - - rewrite <- surjective_pairing. intuition. + - rewrite <- surjective_pairing. intuition (auto with datatypes). - break_match; simpl; eauto. subst. destruct (key_eq_dec (c, n) k). @@ -602,7 +602,8 @@ Section RaftLinearizableProofs. key_of e <> (c, i). Proof using. intros. unfold has_key, key_of in *. - break_match. subst. simpl in *. break_if; try congruence. repeat (do_bool; intuition); congruence. + break_match. subst. simpl in *. break_if; try congruence. + repeat (do_bool; intuition auto); congruence. Qed. Lemma key_of_has_key_false : @@ -781,7 +782,7 @@ Section RaftLinearizableProofs. Proof using. intros; induction tr; simpl in *; intuition. - repeat break_match; subst; simpl in *; intuition; try congruence. - break_if; repeat (do_bool; intuition); try congruence. + break_if; repeat (do_bool; intuition auto); try congruence. destruct k; subst; simpl in *; intuition. - repeat break_match; subst; simpl in *; intuition; try congruence. + destruct k. @@ -965,12 +966,12 @@ Section RaftLinearizableProofs. * specialize (H0 o o0 d0). repeat concludes. apply exported_snoc_IO; congruence. * apply exported_snoc_IU; auto. - + intros. apply H. intuition. + + intros. apply H. intuition (auto with datatypes). + intros. subst. eapply (H0 _ (ys ++ [x])). - rewrite <- app_assoc. simpl. eauto. - eauto. - eauto. - eauto. + * rewrite <- app_assoc. simpl. eauto. + * eauto. + * eauto. + * eauto. Qed. Lemma exported_execute_log : @@ -1015,9 +1016,9 @@ Section RaftLinearizableProofs. intros. induction tr; simpl in *; try congruence. repeat break_let. subst. repeat break_match; simpl in *; intuition; subst; - try solve [unfold in_output_trace in *;break_exists_exists; intuition]. + try solve [unfold in_output_trace in *;break_exists_exists; intuition (auto with datatypes)]. find_inversion. find_apply_lem_hyp get_output'_In. - repeat eexists; eauto; in_crush. + repeat eexists; eauto; in_crush_tac (intuition auto). Qed. Lemma deduplicate_partition : diff --git a/theories/Raft/RefinementSpecLemmas.v b/theories/Raft/RefinementSpecLemmas.v index 62c973b..92d8ec3 100644 --- a/theories/Raft/RefinementSpecLemmas.v +++ b/theories/Raft/RefinementSpecLemmas.v @@ -351,7 +351,8 @@ Section SpecLemmas. t' = t /\ es' = es /\ (forall e, In e es -> In e (log st') \/ haveNewEntries st es = false /\ log st' = log st). Proof using. intros. unfold handleAppendEntries in *. - repeat break_match; find_inversion; simpl in *; intuition; eauto using advanceCurrentTerm_log. + repeat break_match; find_inversion; simpl in *; intuition (auto with datatypes); + eauto using advanceCurrentTerm_log. Qed. Lemma update_elections_data_appendEntries_allEntries : @@ -368,7 +369,6 @@ Section SpecLemmas. - left. apply in_map_iff. eexists; eauto. Qed. - Lemma update_elections_data_appendEntries_allEntries_term : forall h st t h' pli plt es ci te e, In (te, e) (allEntries (update_elections_data_appendEntries h st t h' pli plt es ci)) -> @@ -567,7 +567,7 @@ Section SpecLemmas. unfold update_elections_data_appendEntries. intros. break_let. break_match; auto. break_if; auto. - simpl. intuition. + simpl. intuition (auto with datatypes). Qed. Lemma update_elections_data_request_vote_votesWithLog_old : @@ -652,7 +652,7 @@ Section SpecLemmas. repeat find_rewrite. unfold handleRequestVote, advanceCurrentTerm in *. repeat break_match; repeat find_inversion; simpl in *; auto; try congruence; - find_inversion; auto; do_bool; intuition; try congruence. + find_inversion; auto; do_bool; intuition (auto with arith); try congruence. do_bool. subst. intuition. Qed. End SpecLemmas. diff --git a/theories/Raft/SpecLemmas.v b/theories/Raft/SpecLemmas.v index 927c2d3..75d498f 100644 --- a/theories/Raft/SpecLemmas.v +++ b/theories/Raft/SpecLemmas.v @@ -29,7 +29,7 @@ Section SpecLemmas. repeat break_match; repeat find_inversion; intuition idtac. - simpl in *. discriminate. - unfold advanceCurrentTerm in *. - break_if; simpl in *; do_bool; intuition. + break_if; simpl in *; do_bool; intuition (auto with arith). Qed. Lemma handleRequestVoteReply_term_votedFor_cases : @@ -230,7 +230,7 @@ Section SpecLemmas. currentTerm (advanceCurrentTerm st t) = t. Proof using. intros. unfold advanceCurrentTerm in *. - break_if; do_bool; intuition. + break_if; do_bool; intuition (auto with arith). Qed. Theorem handleAppendEntries_log_detailed : @@ -460,8 +460,8 @@ Section SpecLemmas. Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try right; congruence. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition auto; try right; congruence. Qed. Lemma handleRequestVoteReply_spec' : @@ -479,8 +479,8 @@ Section SpecLemmas. Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try right; congruence. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition (auto with arith); try right; congruence. Qed. Theorem handleTimeout_not_is_append_entries : @@ -531,7 +531,7 @@ Section SpecLemmas. (type st' = Follower /\ currentTerm st' >= currentTerm st). Proof using. intros. unfold handleAppendEntriesReply, advanceCurrentTerm in *. - repeat break_match; tuple_inversion; do_bool; intuition. + repeat break_match; tuple_inversion; do_bool; intuition (auto with arith). Qed. Lemma handleRequestVote_type : @@ -539,7 +539,7 @@ Section SpecLemmas. handleRequestVote h st t h' lli llt = (st', m) -> (type st' = type st /\ currentTerm st' = currentTerm st) \/ type st' = Follower. - Proof using. + Proof using. intros. unfold handleRequestVote, advanceCurrentTerm in *. repeat break_match; find_inversion; auto. Qed. @@ -562,7 +562,7 @@ Section SpecLemmas. (type st = Candidate /\ type st' = Leader /\ currentTerm st' = currentTerm st). Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; subst; do_bool; intuition. + repeat break_match; subst; do_bool; intuition auto. Qed. Lemma handleClientRequest_type : @@ -1017,7 +1017,7 @@ Section SpecLemmas. Proof using. intros. unfold handleRequestVote, advanceCurrentTerm in *. repeat break_match; find_inversion; subst; auto; - intuition; break_exists; congruence. + intuition auto; break_exists; congruence. Qed. Theorem handleClientRequest_no_append_entries : @@ -1170,7 +1170,7 @@ Section SpecLemmas. (r = true /\ v = h' /\ currentTerm (handleRequestVoteReply h st h' t r) = t). Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; subst; simpl in *; do_bool; intuition. + repeat break_match; subst; simpl in *; do_bool; intuition (auto with arith). Qed. Theorem handleTimeout_log_term_type : diff --git a/theories/RaftProofs/AllEntriesLeaderSublogProof.v b/theories/RaftProofs/AllEntriesLeaderSublogProof.v index 3f04c30..1149044 100644 --- a/theories/RaftProofs/AllEntriesLeaderSublogProof.v +++ b/theories/RaftProofs/AllEntriesLeaderSublogProof.v @@ -177,8 +177,8 @@ Section AllEntriesLeaderSublog. Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try right; congruence. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition (try lia); try right; congruence. Qed. Lemma allEntries_leader_sublog_request_vote_reply : diff --git a/theories/RaftProofs/AllEntriesLogProof.v b/theories/RaftProofs/AllEntriesLogProof.v index 062e560..f82fe71 100644 --- a/theories/RaftProofs/AllEntriesLogProof.v +++ b/theories/RaftProofs/AllEntriesLogProof.v @@ -112,18 +112,18 @@ Ltac all f ls := Proof using. intros. destruct l2; intuition. simpl in *. right. - destruct l1; intuition. + destruct l1; intuition (auto with arith). find_copy_eapply_lem_hyp findAtIndex_None; simpl in *; eauto. unfold contiguous_range_exact_lo in *. simpl in *. intuition. - destruct (lt_eq_lt_dec 0 (eIndex e)); intuition; eauto. - destruct (lt_eq_lt_dec (eIndex e0) (eIndex e)); intuition. - exfalso. repeat break_if; do_bool; intuition. + destruct (lt_eq_lt_dec 0 (eIndex e)); intuition (try lia); eauto. + destruct (lt_eq_lt_dec (eIndex e0) (eIndex e)); intuition (try lia). + exfalso. repeat break_if; do_bool; intuition (try lia). match goal with | H : forall _, _ < _ <= _ -> _ |- _ => specialize (H (eIndex e)) end; conclude_using lia. - simpl in *. break_exists. intuition; subst; intuition. + simpl in *. break_exists. intuition auto; subst; intuition (try lia). eapply findAtIndex_None; eauto. Qed. @@ -204,24 +204,6 @@ Ltac all f ls := end; eauto. lia. Qed. -(* - Lemma sorted_app_in3_in4_prefix : - forall l1 l2 l3 l4 e e', - sorted (l1 ++ l3) -> - sorted (l2 ++ l4) -> - Prefix l4 l3 -> - In e l3 -> - In e' (l2 ++ l4) -> - eIndex e' = eIndex e -> - In e' l4. - Proof. - intros. do_in_app. intuition. - match goal with - | H : sorted (?l ++ ?l'), _ : In _ ?l, _ : In _ ?l' |- _ => - eapply sorted_app_in_in in H - end; eauto. lia. - Qed. -*) Lemma sorted_term_index_le : forall l e e', sorted l -> @@ -230,10 +212,11 @@ Ltac all f ls := eTerm e' < eTerm e -> eIndex e' <= eIndex e. Proof using. - induction l; intros; simpl in *; intuition; subst_max; intuition. - - find_apply_hyp_hyp. intuition. - - find_apply_hyp_hyp. intuition. + induction l; intros; simpl in *; intuition; subst_max; intuition auto. + - find_apply_hyp_hyp. intuition (auto with arith). + - find_apply_hyp_hyp. intuition lia. Qed. + Lemma term_ne_in_l2 : forall l e e' l1 l2, sorted l -> @@ -249,7 +232,7 @@ Ltac all f ls := assert (eIndex e' <= eIndex e) by (eapply sorted_term_index_le; eauto; find_apply_hyp_hyp; - destruct (lt_eq_lt_dec (eTerm e') (eTerm e)); intuition). + destruct (lt_eq_lt_dec (eTerm e') (eTerm e)); intuition lia). find_eapply_lem_hyp removeAfterIndex_le_In; eauto. repeat find_rewrite. do_in_app. intuition. @@ -300,7 +283,7 @@ Ltac all f ls := [|right; break_exists_exists; intuition; repeat find_higher_order_rewrite; destruct_update; simpl in *; eauto; try rewrite update_elections_data_appendEntries_leaderLogs; eauto; subst; - find_apply_lem_hyp handleAppendEntries_currentTerm_leaderId; intuition; + find_apply_lem_hyp handleAppendEntries_currentTerm_leaderId; intuition (try lia); repeat find_rewrite; auto]. destruct (in_dec entry_eq_dec e (log d)); intuition. right. @@ -319,17 +302,17 @@ Ltac all f ls := [repeat find_higher_order_rewrite; destruct_update; simpl in *; eauto; rewrite update_elections_data_appendEntries_leaderLogs; eauto|]; - split; auto; intuition; + split; auto; (intuition (try lia)); [break_exists; intuition; find_eapply_lem_hyp leaderLogs_contiguous_invariant; eauto; lia|]. - subst. repeat find_rewrite. intuition. + subst. repeat find_rewrite. intuition (auto with datatypes). + subst. find_eapply_lem_hyp allEntries_leaderLogs_term_invariant; eauto. intuition. * subst. exfalso. find_copy_eapply_lem_hyp logs_leaderLogs_invariant; eauto. pose proof H1 as H1'. eapply append_entries_leaderLogs_invariant in H1; eauto. - break_exists; intuition; + break_exists; (intuition (try lia)); [break_exists; intuition; find_eapply_lem_hyp leaderLogs_contiguous_invariant; eauto; lia|]. subst. clean. @@ -349,7 +332,7 @@ Ltac all f ls := (eapply removeAfterIndex_le_In; eauto) end. repeat find_rewrite. - do_in_app; intuition. + do_in_app; intuition (auto with datatypes). assert (exists e', eIndex e' = eIndex e /\ In e' (x1 ++ x4)) by (eapply entries_contiguous_nw_invariant; eauto; intuition; [eapply entries_contiguous_invariant; eauto|]; @@ -371,7 +354,7 @@ Ltac all f ls := * exfalso. pose proof H1 as H1'. eapply append_entries_leaderLogs_invariant in H1; eauto. - break_exists; intuition; + break_exists; (intuition (try lia)); [break_exists; intuition; find_eapply_lem_hyp leaderLogs_contiguous_invariant; eauto; lia|]. subst. clean. @@ -396,17 +379,17 @@ Ltac all f ls := destruct_update; simpl in *; eauto; rewrite update_elections_data_appendEntries_leaderLogs; eauto|]; split; auto. - intuition; + (intuition (try lia)); [break_exists; intuition; find_eapply_lem_hyp leaderLogs_contiguous_invariant; eauto; lia|]. - subst. repeat find_rewrite. intuition. + subst. repeat find_rewrite. intuition (auto with datatypes). + subst. find_eapply_lem_hyp allEntries_leaderLogs_term_invariant; eauto. intuition. * { subst. exfalso. find_copy_eapply_lem_hyp logs_leaderLogs_invariant; eauto. pose proof H1 as H1'. eapply append_entries_leaderLogs_invariant in H1; eauto. - break_exists; intuition; + break_exists; (intuition (try lia)); [break_exists; intuition; find_eapply_lem_hyp leaderLogs_contiguous_invariant; eauto; lia|]. subst. clean. @@ -426,7 +409,7 @@ Ltac all f ls := (eapply removeAfterIndex_le_In; eauto) end. repeat find_rewrite. - do_in_app; intuition. + do_in_app; intuition (auto with datatypes). find_apply_lem_hyp findAtIndex_elim. intuition. find_copy_apply_lem_hyp maxIndex_non_empty. break_exists. @@ -478,7 +461,7 @@ Ltac all f ls := * exfalso. pose proof H1 as H1'. eapply append_entries_leaderLogs_invariant in H1; eauto. - break_exists; intuition; + break_exists; (intuition (try lia)); [break_exists; intuition; find_eapply_lem_hyp leaderLogs_contiguous_invariant; eauto; lia|]. subst. clean. @@ -533,7 +516,7 @@ Ltac all f ls := apply removeAfterIndex_le_In; auto. eapply maxIndex_is_max; eauto. } - * contradict n0. intuition. + * contradict n0. intuition (auto with datatypes). + subst. find_eapply_lem_hyp allEntries_leaderLogs_term_invariant; eauto. intuition. * { subst. exfalso. @@ -635,7 +618,7 @@ Ltac all f ls := eapply entries_sorted_nw_invariant; eauto]. match goal with | H : In e _ -> False |- _ => apply H - end. intuition. + end. intuition (auto with datatypes). - subst. destruct (le_lt_dec (eIndex e) (eIndex x6)). + match goal with @@ -678,7 +661,7 @@ Ltac all f ls := end; eauto using sorted_uniqueIndices. subst. auto. * match goal with | H : In e _ -> False |- _ => apply H - end. intuition. + end. intuition (auto with datatypes). } * { exfalso. find_copy_apply_lem_hyp append_entries_leaderLogs_invariant; eauto. @@ -704,7 +687,7 @@ Ltac all f ls := eapply prefix_contiguous; eauto. eapply contiguous_app; [|eapply entries_contiguous_nw_invariant; eauto]; eapply entries_sorted_nw_invariant; eauto. - - subst. intuition. + - subst. intuition (auto with datatypes). } - find_copy_eapply_lem_hyp allEntries_term_sanity_invariant; eauto. destruct (lt_eq_lt_dec t0 t); intuition; unfold ghost_data in *; simpl in *; try lia. @@ -750,7 +733,7 @@ Ltac all f ls := apply removeAfterIndex_le_In; auto. eapply maxIndex_is_max; eauto. } - * contradict n0. intuition. + * contradict n0. intuition (auto with datatypes). + subst. find_eapply_lem_hyp allEntries_leaderLogs_term_invariant; eauto. intuition. * { subst. exfalso. @@ -778,7 +761,7 @@ Ltac all f ls := eapply removeAfterIndex_in with (i := (eIndex e)). unfold raft_data, ghost_data in *; simpl in *. unfold raft_data, ghost_data in *; simpl in *. - repeat find_rewrite. intuition. + repeat find_rewrite. intuition (auto with datatypes). - simpl in *. match goal with | H : forall _, ?e = _ \/ _ -> _ |- _ => @@ -796,10 +779,10 @@ Ltac all f ls := eapply maxIndex_is_max; eauto; eapply leaderLogs_sorted_invariant; eauto). assert (eIndex x7 < eIndex e0) by - (eapply entries_contiguous_nw_invariant; eauto; intuition). - intuition. + (eapply entries_contiguous_nw_invariant; eauto; intuition (auto with datatypes)). + intuition (try lia). + break_exists. break_and. - unfold Prefix_sane in *. intuition. + unfold Prefix_sane in *. intuition (try lia). find_copy_eapply_lem_hyp Prefix_maxIndex_eq; eauto. find_eapply_lem_hyp entries_sorted_nw_invariant; eauto. find_eapply_lem_hyp sorted_gt_maxIndex; eauto; lia. @@ -832,7 +815,7 @@ Ltac all f ls := eapply prefix_contiguous; eauto. eapply contiguous_app; [|eapply entries_contiguous_nw_invariant; eauto]; eapply entries_sorted_nw_invariant; eauto. - - subst. intuition. + - subst. intuition (auto with datatypes). } Qed. @@ -853,8 +836,9 @@ Ltac all f ls := repeat find_higher_order_rewrite. find_copy_apply_lem_hyp handleAppendEntriesReply_log. find_apply_lem_hyp handleAppendEntriesReply_currentTerm_leaderId. - destruct_update; simpl in *; eauto; find_apply_hyp_hyp; repeat find_rewrite; intuition; - right; break_exists_exists; repeat find_rewrite; intuition; + destruct_update; simpl in *; eauto; find_apply_hyp_hyp; + repeat find_rewrite; intuition; + right; break_exists_exists; repeat find_rewrite; intuition (try lia); find_higher_order_rewrite; destruct_update; simpl in *; auto. Qed. @@ -890,7 +874,7 @@ Ltac all f ls := destruct_update; simpl in *; eauto; try find_rewrite_lem update_elections_data_requestVote_allEntries; find_apply_hyp_hyp; repeat find_rewrite; intuition; - right; break_exists_exists; intuition; repeat find_higher_order_rewrite; + right; break_exists_exists; intuition (try lia); repeat find_higher_order_rewrite; destruct_update; simpl in *; auto; rewrite update_elections_data_requestVote_leaderLogs; auto. Qed. @@ -912,7 +896,7 @@ Ltac all f ls := try rewrite handleRequestVoteReply_log'; try find_rewrite_lem update_elections_data_requestVoteReply_allEntries; find_apply_hyp_hyp; repeat find_rewrite; intuition; - right; break_exists_exists; repeat find_rewrite; intuition; + right; break_exists_exists; repeat find_rewrite; intuition (try lia); find_higher_order_rewrite; destruct_update; simpl in *; auto; apply update_elections_data_requestVoteReply_leaderLogs; auto. @@ -929,7 +913,7 @@ Ltac all f ls := unfold update_elections_data_client_request in *. repeat break_match; repeat find_inversion; auto. simpl in *. intuition. - find_inversion. repeat find_rewrite. intuition. + find_inversion. repeat find_rewrite. intuition (auto with datatypes). Qed. Lemma handleClientRequest_currentTerm_leaderId : @@ -984,7 +968,7 @@ Ltac all f ls := find_apply_lem_hyp handleTimeout_currentTerm_leaderId; repeat find_rewrite; find_apply_hyp_hyp; intuition; - right; break_exists_exists; intuition; + right; break_exists_exists; intuition (try lia); repeat find_higher_order_rewrite; destruct_update; simpl in *; auto; rewrite update_elections_data_timeout_leaderLogs; auto. @@ -1014,11 +998,10 @@ Ltac all f ls := find_copy_apply_lem_hyp doLeader_log. find_apply_lem_hyp doLeader_currentTerm_leaderId. destruct_update; simpl in *; eauto; find_apply_hyp_hyp; repeat find_rewrite; intuition; - right; break_exists_exists; intuition; find_higher_order_rewrite; + right; break_exists_exists; intuition (try lia); find_higher_order_rewrite; destruct_update; simpl in *; auto. Qed. - Lemma doGenericServer_currentTerm_leaderId : forall st h out st' m, doGenericServer h st = (out, st', m) -> @@ -1045,7 +1028,7 @@ Ltac all f ls := find_copy_apply_lem_hyp doGenericServer_log. find_apply_lem_hyp doGenericServer_currentTerm_leaderId. destruct_update; simpl in *; eauto; find_apply_hyp_hyp; repeat find_rewrite; intuition; - right; break_exists_exists; intuition; find_higher_order_rewrite; + right; break_exists_exists; intuition (try lia); find_higher_order_rewrite; destruct_update; simpl in *; auto. Qed. diff --git a/theories/RaftProofs/AllEntriesTermSanityProof.v b/theories/RaftProofs/AllEntriesTermSanityProof.v index b435fa2..32f0921 100644 --- a/theories/RaftProofs/AllEntriesTermSanityProof.v +++ b/theories/RaftProofs/AllEntriesTermSanityProof.v @@ -33,7 +33,7 @@ Section AllEntriesTermSanity. subst. repeat find_higher_order_rewrite. destruct_update; simpl in *; eauto. find_copy_eapply_lem_hyp update_elections_data_appendEntries_allEntries_term'; eauto. - intuition. + intuition (try lia). find_apply_lem_hyp handleAppendEntries_currentTerm_monotonic; find_apply_hyp_hyp; lia. Qed. diff --git a/theories/RaftProofs/AllEntriesVotesWithLogProof.v b/theories/RaftProofs/AllEntriesVotesWithLogProof.v index 2c441bd..5d6e496 100644 --- a/theories/RaftProofs/AllEntriesVotesWithLogProof.v +++ b/theories/RaftProofs/AllEntriesVotesWithLogProof.v @@ -117,8 +117,8 @@ Section AllEntriesVotesWithLog. unfold update_elections_data_requestVote. intros. repeat break_match; repeat tuple_inversion; intuition; - simpl in *; intuition; - tuple_inversion; intuition; repeat (do_bool; intuition); + simpl in *; intuition; + tuple_inversion; intuition; repeat (do_bool; intuition (auto with bool)); try congruence; unfold raft_data, ghost_data in *; simpl in *; repeat find_rewrite; repeat find_inversion; @@ -147,15 +147,15 @@ Section AllEntriesVotesWithLog. intuition. right. break_exists_exists. repeat find_higher_order_rewrite. simpl in *. - destruct_update; simpl in *; intuition; + destruct_update; simpl in *; intuition (try lia); try rewrite leaderLogs_update_elections_data_requestVote; eauto. - + subst. + + subst. find_apply_lem_hyp handleRequestVote_log. repeat find_rewrite. find_copy_eapply_lem_hyp allEntries_log_invariant; eauto. intuition. right. break_exists_exists. repeat find_higher_order_rewrite. simpl in *. - destruct_update; simpl in *; intuition; + destruct_update; simpl in *; intuition (try lia); try rewrite leaderLogs_update_elections_data_requestVote; eauto. - eapply_prop_hyp votesWithLog votesWithLog; eauto; intuition; right; break_exists_exists; intuition; @@ -254,7 +254,7 @@ Section AllEntriesVotesWithLog. find_copy_apply_lem_hyp handleTimeout_log_same. repeat find_rewrite. find_apply_lem_hyp allEntries_log_invariant; eauto. intuition. right. - break_exists_exists; intuition; + break_exists_exists; intuition (try lia); find_higher_order_rewrite; destruct_update; simpl in *; auto; rewrite update_elections_data_timeout_leaderLogs; auto. - eapply_prop_hyp votesWithLog votesWithLog; eauto; intuition; diff --git a/theories/RaftProofs/AppendEntriesLeaderProof.v b/theories/RaftProofs/AppendEntriesLeaderProof.v index 399f8bb..9b9e947 100644 --- a/theories/RaftProofs/AppendEntriesLeaderProof.v +++ b/theories/RaftProofs/AppendEntriesLeaderProof.v @@ -219,7 +219,8 @@ Section AppendEntriesLeader. Proof using. unfold handleRequestVoteReply. intros. - repeat break_match; repeat find_inversion; do_bool; subst; simpl; intuition. + repeat break_match; repeat find_inversion; do_bool; subst; simpl; + intuition (auto with arith). Qed. Lemma update_elections_data_RVR_ascending_leaderLog : diff --git a/theories/RaftProofs/AppendEntriesReplySublogProof.v b/theories/RaftProofs/AppendEntriesReplySublogProof.v index f7e27ae..42618ab 100644 --- a/theories/RaftProofs/AppendEntriesReplySublogProof.v +++ b/theories/RaftProofs/AppendEntriesReplySublogProof.v @@ -64,7 +64,7 @@ Section AppendEntriesReplySublog. match goal with | H : In _ (nwPackets _) |- _ => clear H end. - assert (In aer (nwPackets net')) by (repeat find_rewrite; intuition). + assert (In aer (nwPackets net')) by (repeat find_rewrite; intuition (auto with datatypes)). match goal with | H : nwState net' = nwState net |- _ => rewrite <- H in *; clear H @@ -73,6 +73,7 @@ Section AppendEntriesReplySublog. Qed. Instance aersi : append_entries_reply_sublog_interface. - split. exact append_entries_reply_sublog_invariant. + Proof using aeli rri aerrci. + split. exact append_entries_reply_sublog_invariant. Qed. End AppendEntriesReplySublog. diff --git a/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v b/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v index 2c2e97a..d976cb5 100644 --- a/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v +++ b/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v @@ -107,10 +107,12 @@ Section AppendEntriesRequestLeaderLogs. match goal with | [ _ : nwPackets ?net = _, _ : In ?p _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; do_in_app; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; do_in_app; intuition (auto with datatypes)) | [ _ : nwPackets ?net = _, _ : pBody ?p = _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; intuition (auto with datatypes)) end. Lemma append_entries_leaderLogs_appendEntries : @@ -329,7 +331,7 @@ Section AppendEntriesRequestLeaderLogs. | _ : S _ = pred ?x |- context [pred ?y] => assert (pred x = pred y) by auto end. - repeat find_rewrite. intuition. + repeat find_rewrite. intuition lia. Qed. Lemma lift_nextIndex_safety : diff --git a/theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v b/theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v index 227e69e..4d31daa 100644 --- a/theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v +++ b/theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v @@ -40,9 +40,9 @@ Section AppendEntriesRequestReplyCorrespondence. eapply @RIR_handleInput with (net := net') (inp := Timeout); eauto; simpl; repeat find_rewrite; eauto. intros. - do_in_app. intuition. + do_in_app. intuition (auto with datatypes). find_apply_hyp_hyp. - intuition. + intuition (auto with datatypes). - exfalso. do_in_map. subst. simpl in *. unfold handleTimeout, tryToBecomeLeader in *. @@ -72,16 +72,15 @@ Section AppendEntriesRequestReplyCorrespondence. eapply @RIR_handleInput with (net := net') (inp := ClientRequest client id c); eauto; simpl; repeat find_rewrite; eauto. intros. - do_in_app. intuition. + do_in_app. intuition (auto with datatypes). find_apply_hyp_hyp. - intuition. + intuition (auto with datatypes). - exfalso. do_in_map. subst. simpl in *. unfold handleClientRequest in *. repeat break_match; find_inversion; intuition; do_in_map; subst; simpl in *; congruence. Qed. - Lemma append_entries_request_reply_correspondence_do_leader : raft_net_invariant_do_leader append_entries_request_reply_correspondence. Proof using. @@ -105,9 +104,9 @@ Section AppendEntriesRequestReplyCorrespondence. eapply @RIR_doLeader with (net := net'); eauto; simpl; repeat find_rewrite; eauto. intros. - do_in_app. intuition. + do_in_app. intuition (auto with datatypes). find_apply_hyp_hyp. - intuition. + intuition (auto with datatypes). - exfalso. do_in_map. subst. simpl in *. unfold doLeader in *. @@ -137,9 +136,9 @@ Section AppendEntriesRequestReplyCorrespondence. eapply @RIR_doGenericServer with (net := net'); eauto; simpl; repeat find_rewrite; eauto. intros. - do_in_app. intuition. + do_in_app. intuition (auto with datatypes). find_apply_hyp_hyp. - intuition. + intuition (auto with datatypes). - exfalso. do_in_map. subst. simpl in *. unfold doGenericServer in *. @@ -219,7 +218,7 @@ Section AppendEntriesRequestReplyCorrespondence. - simpl in *. repeat find_rewrite. apply functional_extensionality. eauto. - simpl. - intros. repeat find_rewrite. do_in_app. intuition. + intros. repeat find_rewrite. do_in_app. intuition (auto with datatypes). Qed. Lemma handleAppendEntries_reply_spec: @@ -267,7 +266,8 @@ Section AppendEntriesRequestReplyCorrespondence. simpl; repeat find_rewrite; eauto; simpl; repeat break_let; eauto; try find_inversion; eauto. intros. do_in_app. simpl in *. - intuition; try find_apply_hyp_hyp; intuition; in_crush. + intuition auto; try find_apply_hyp_hyp; intuition auto; + in_crush_tac (intuition (auto with datatypes)). - subst. simpl in *. subst. unfold exists_equivalent_network_with_aer. find_eapply_lem_hyp RIR_step_failure; [|eapply StepFailure_dup with (failed := [])]; eauto. remember mkNetwork as mkN. @@ -328,14 +328,14 @@ Section AppendEntriesRequestReplyCorrespondence. simpl; repeat find_rewrite; eauto; simpl; repeat break_let; eauto; try find_inversion; eauto. intros. do_in_app. simpl in *. - intuition; try find_apply_hyp_hyp; intuition; in_crush. + intuition auto; try find_apply_hyp_hyp; intuition auto; + in_crush_tac (intuition (auto with datatypes)). - do_in_map. subst. simpl in *. find_apply_lem_hyp handleAppendEntriesReply_packets. subst. simpl in *. intuition. Qed. - Lemma append_entries_request_reply_correspondence_request_vote : raft_net_invariant_request_vote append_entries_request_reply_correspondence. Proof using. @@ -367,7 +367,8 @@ Section AppendEntriesRequestReplyCorrespondence. simpl; repeat find_rewrite; eauto; simpl; repeat break_let; eauto; try find_inversion; eauto. intros. do_in_app. simpl in *. - intuition; try find_apply_hyp_hyp; intuition; in_crush. + intuition auto; try find_apply_hyp_hyp; intuition auto; + in_crush_tac (intuition (auto with datatypes)). - subst. simpl in *. subst. unfold handleRequestVote in *. repeat break_match; find_inversion; congruence. @@ -404,24 +405,25 @@ Section AppendEntriesRequestReplyCorrespondence. simpl; repeat find_rewrite; eauto; simpl; repeat break_let; eauto; try find_inversion; eauto. intros. do_in_app. simpl in *. - intuition; try find_apply_hyp_hyp; intuition; in_crush. + intuition auto; try find_apply_hyp_hyp; intuition auto; + in_crush_tac (intuition (auto with datatypes)). Qed. Instance aerrci : append_entries_request_reply_correspondence_interface. - split. - intros. apply raft_net_invariant; auto. - - exact append_entries_request_reply_correspondence_init. - - exact append_entries_request_reply_correspondence_client_request. - - exact append_entries_request_reply_correspondence_timeout. - - exact append_entries_request_reply_correspondence_append_entries. - - exact append_entries_request_reply_correspondence_append_entries_reply. - - exact append_entries_request_reply_correspondence_request_vote. - - exact append_entries_request_reply_correspondence_request_vote_reply. - - exact append_entries_request_reply_correspondence_do_leader. - - exact append_entries_request_reply_correspondence_do_generic_server. - - exact append_entries_request_reply_correspondence_state_same_packet_subset. - - exact append_entries_request_reply_correspondence_reboot. + Proof using. + split. + intros. apply raft_net_invariant; auto. + - exact append_entries_request_reply_correspondence_init. + - exact append_entries_request_reply_correspondence_client_request. + - exact append_entries_request_reply_correspondence_timeout. + - exact append_entries_request_reply_correspondence_append_entries. + - exact append_entries_request_reply_correspondence_append_entries_reply. + - exact append_entries_request_reply_correspondence_request_vote. + - exact append_entries_request_reply_correspondence_request_vote_reply. + - exact append_entries_request_reply_correspondence_do_leader. + - exact append_entries_request_reply_correspondence_do_generic_server. + - exact append_entries_request_reply_correspondence_state_same_packet_subset. + - exact append_entries_request_reply_correspondence_reboot. Qed. - End AppendEntriesRequestReplyCorrespondence. diff --git a/theories/RaftProofs/AppendEntriesRequestTermSanityProof.v b/theories/RaftProofs/AppendEntriesRequestTermSanityProof.v index 4c70ca8..edd05e2 100644 --- a/theories/RaftProofs/AppendEntriesRequestTermSanityProof.v +++ b/theories/RaftProofs/AppendEntriesRequestTermSanityProof.v @@ -3,7 +3,6 @@ From VerdiRaft Require Import Raft RaftRefinementInterface SortedInterface. From VerdiRaft Require Import AppendEntriesRequestTermSanityInterface. Section AppendEntriesRequestTermSanity. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v b/theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v index a290699..09a6271 100644 --- a/theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v +++ b/theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v @@ -22,10 +22,12 @@ Section AppendEntriesRequestsCameFromLeaders. match goal with | [ _ : nwPackets ?net = _, _ : In ?p _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; do_in_app; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; do_in_app; intuition (auto with datatypes)) | [ _ : nwPackets ?net = _, _ : pBody ?p = _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; intuition (auto with datatypes)) end. Ltac contra := (exfalso; intuition; find_false; diff --git a/theories/RaftProofs/AppliedEntriesMonotonicProof.v b/theories/RaftProofs/AppliedEntriesMonotonicProof.v index 8439863..8298204 100644 --- a/theories/RaftProofs/AppliedEntriesMonotonicProof.v +++ b/theories/RaftProofs/AppliedEntriesMonotonicProof.v @@ -85,7 +85,7 @@ Section AppliedEntriesMonotonicProof. Proof using. intros. unfold committed in *. - break_exists_exists. intuition. + break_exists_exists. intuition (try lia). unfold log_matching, log_matching_hosts in *. intuition. unfold entries_match in *. rewrite deghost_snd in *. @@ -142,14 +142,15 @@ Section AppliedEntriesMonotonicProof. find_apply_hyp_hyp. intuition. Qed. + (* FIXME: redundant with other files *) Lemma sorted_app : forall l l', sorted (l ++ l') -> sorted l. Proof using. induction l; simpl in *; intros; intuition eauto. - - apply H0. intuition. - - apply H0. intuition. + - apply H0. intuition (auto with datatypes). + - apply H0. intuition (auto with datatypes). Qed. Lemma handleMessage_applied_entries : @@ -188,14 +189,14 @@ Section AppliedEntriesMonotonicProof. find_apply_lem_hyp logs_contiguous; auto; lia. * intros. find_copy_apply_lem_hyp log_matching_invariant. - unfold log_matching, log_matching_hosts in *. intuition. + unfold log_matching, log_matching_hosts in *. intuition (auto with datatypes). match goal with | H : forall _ _, _ <= _ <= _ -> _ |- _ => specialize (H h (eIndex e)); forward H end; copy_eapply_prop_hyp log_matching_nw AppendEntries; eauto; repeat (forwards; [intuition eauto; lia|]; concludes); - intuition; [eapply Nat.le_trans; eauto|]. + (intuition (auto with arith)); [eapply Nat.le_trans; eauto|]. match goal with | H : exists _, _ |- _ => destruct H as [e'] end. @@ -237,7 +238,7 @@ Section AppliedEntriesMonotonicProof. unfold state_machine_safety_nw in *. eapply_prop_hyp commit_recorded In; intuition; eauto; try lia; try solve [find_apply_lem_hyp logs_contiguous; auto; lia]. - unfold commit_recorded. intuition. + unfold commit_recorded. intuition lia. + repeat find_rewrite. find_copy_apply_lem_hyp logs_sorted_invariant. unfold logs_sorted in *. intuition. @@ -256,7 +257,7 @@ Section AppliedEntriesMonotonicProof. simpl in *. intuition eauto. forwards; eauto. concludes. forwards; [unfold commit_recorded in *; intuition eauto|]. concludes. - intuition; apply in_app_iff; + intuition (auto with datatypes); apply in_app_iff; try solve [right; eapply removeAfterIndex_le_In; eauto; lia]; exfalso. find_eapply_lem_hyp findAtIndex_max_thing; eauto using entries_max_thing. @@ -281,7 +282,7 @@ Section AppliedEntriesMonotonicProof. simpl in *. intuition eauto. forwards; eauto. concludes. forwards; [unfold commit_recorded in *; intuition eauto|]. concludes. - intuition; apply in_app_iff; + intuition (auto with datatypes); apply in_app_iff; try solve [right; eapply removeAfterIndex_le_In; eauto; lia]. subst. find_apply_lem_hyp maxIndex_non_empty. @@ -293,7 +294,7 @@ Section AppliedEntriesMonotonicProof. unfold state_machine_safety_nw in *. eapply rachet; eauto using sorted_app, sorted_uniqueIndices. copy_eapply_prop_hyp commit_recorded In; intuition; eauto; try lia; - unfold commit_recorded; intuition. + unfold commit_recorded; intuition (try lia). - exfalso. pose proof entries_gt_pli. eapply_prop_hyp AppendEntries AppendEntries; @@ -412,7 +413,8 @@ Section AppliedEntriesMonotonicProof. find_copy_apply_lem_hyp doLeader_appliedEntries. find_copy_eapply_lem_hyp RIR_handleMessage; eauto. find_eapply_lem_hyp RIR_doLeader; simpl in *; eauto. - find_apply_lem_hyp handleMessage_applied_entries; auto; [|destruct p; find_rewrite; in_crush]. + find_apply_lem_hyp handleMessage_applied_entries; auto; + [|destruct p; find_rewrite; in_crush_tac (intuition auto)]. unfold raft_data in *. simpl in *. unfold raft_data in *. simpl in *. match goal with | H : applied_entries (update _ (update _ _ _ _) _ _) = @@ -446,9 +448,9 @@ Section AppliedEntriesMonotonicProof. repeat find_rewrite. repeat match goal with H : applied_entries _ = applied_entries _ |- _ => clear H end. eauto using doGenericServer_applied_entries. - - exists nil; intuition. - - exists nil; intuition. - - exists nil; intuition. + - exists nil; intuition (auto with datatypes). + - exists nil; intuition (auto with datatypes). + - exists nil; intuition (auto with datatypes). - exists nil. rewrite app_nil_r. apply applied_entries_log_lastApplied_same; @@ -463,11 +465,11 @@ Section AppliedEntriesMonotonicProof. In e (applied_entries (nwState net')). Proof using lacimi misi smsi uii lmi si. intros. find_eapply_lem_hyp applied_entries_monotonic'; eauto. - break_exists. find_rewrite. in_crush. + break_exists. find_rewrite. in_crush_tac (intuition (auto with datatypes)). Qed. Instance aemi : applied_entries_monotonic_interface. - Proof. + Proof using lacimi misi smsi uii lmi si. split; eauto using applied_entries_monotonic, applied_entries_monotonic'. diff --git a/theories/RaftProofs/AppliedImpliesInputProof.v b/theories/RaftProofs/AppliedImpliesInputProof.v index 9e5623c..68db7f5 100644 --- a/theories/RaftProofs/AppliedImpliesInputProof.v +++ b/theories/RaftProofs/AppliedImpliesInputProof.v @@ -18,7 +18,7 @@ Section AppliedImpliesInputProof. in_input_trace c id i (tr1 ++ tr2). Proof using. unfold in_input_trace. - intuition; break_exists_exists; intuition. + intuition; break_exists_exists; intuition (auto with datatypes). Qed. Section inner. @@ -400,7 +400,7 @@ Section AppliedImpliesInputProof. Defined. Next Obligation. unfold in_input_trace in *. break_exists_exists. - intuition. + intuition (auto with datatypes). Defined. Next Obligation. unfold applied_implies_input_state. intro. break_exists. break_and. diff --git a/theories/RaftProofs/CandidateEntriesProof.v b/theories/RaftProofs/CandidateEntriesProof.v index 90f8f57..1e5fb86 100644 --- a/theories/RaftProofs/CandidateEntriesProof.v +++ b/theories/RaftProofs/CandidateEntriesProof.v @@ -242,12 +242,11 @@ Section CandidateEntriesProof. Proof using. intros. unfold handleAppendEntries, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try solve [break_exists; congruence]; - in_crush; eauto using removeAfterIndex_in. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition auto; try solve [break_exists; congruence]; + in_crush_tac (intuition (auto with arith)); eauto using removeAfterIndex_in. Qed. - Lemma handleAppendEntries_term_same_or_type_follower : forall h t n pli plt es ci d m st, handleAppendEntries h st t n pli plt es ci = (d, m) -> @@ -362,10 +361,12 @@ Section CandidateEntriesProof. match goal with | [ _ : nwPackets ?net = _, _ : In ?p _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; do_in_app; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; do_in_app; intuition (auto with datatypes)) | [ _ : nwPackets ?net = _, _ : pBody ?p = _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; intuition (auto with datatypes)) end. Lemma candidate_entries_append_entries_reply : diff --git a/theories/RaftProofs/CausalOrderPreservedProof.v b/theories/RaftProofs/CausalOrderPreservedProof.v index e60b66d..2559ac6 100644 --- a/theories/RaftProofs/CausalOrderPreservedProof.v +++ b/theories/RaftProofs/CausalOrderPreservedProof.v @@ -33,8 +33,9 @@ Section CausalOrderPreserved. intuition. break_exists. unfold in_input_trace in *. break_exists. do_in_app. intuition; - [find_apply_hyp_hyp; simpl in *; break_if; repeat (do_bool; intuition)|]. - invcs H0; intuition. + [find_apply_hyp_hyp; simpl in *; break_if; + repeat (do_bool; intuition (auto with bool))|]. + invcs H0; intuition (try lia). - break_if; congruence. - find_inversion; try congruence. repeat (do_bool; intuition). @@ -51,7 +52,7 @@ Section CausalOrderPreserved. induction tr; simpl in *; intuition. - unfold key_in_output_trace. unfold is_output_with_key in *. repeat break_match; try congruence. - subst. do 2 eexists. intuition; eauto. + subst. do 2 eexists. intuition (auto with datatypes); eauto. - unfold key_in_output_trace in *. break_exists_exists. simpl; intuition. Qed. diff --git a/theories/RaftProofs/CroniesCorrectProof.v b/theories/RaftProofs/CroniesCorrectProof.v index fd77117..b244e1c 100644 --- a/theories/RaftProofs/CroniesCorrectProof.v +++ b/theories/RaftProofs/CroniesCorrectProof.v @@ -329,7 +329,7 @@ Section CroniesCorrectProof. Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; simpl in *; subst; simpl in *; do_bool; intuition. + repeat break_match; simpl in *; subst; simpl in *; do_bool; intuition (auto with arith). Qed. Lemma handleRequestVoteReply_leader : @@ -396,7 +396,7 @@ Section CroniesCorrectProof. match goal with | H : pBody _ = _, Hpbody : forall _ _, pBody _ = _ -> _ |- _ => apply Hpbody in H - end; [|solve [repeat find_rewrite; in_crush]]. + end; [|solve [repeat find_rewrite; in_crush_tac (intuition auto)]]. repeat find_rewrite; eauto. * repeat find_rewrite. unfold votes_received_cronies in *. @@ -416,7 +416,7 @@ Section CroniesCorrectProof. match goal with | H : pBody _ = _, Hpbody : forall _ _, pBody _ = _ -> _ |- _ => apply Hpbody in H - end; [|solve [repeat find_rewrite; in_crush]]. + end; [|solve [repeat find_rewrite; in_crush_tac (intuition auto)]]. repeat find_rewrite; eauto. * repeat find_rewrite. unfold votes_received_cronies in *. @@ -443,7 +443,7 @@ Section CroniesCorrectProof. match goal with | H : pBody _ = _, Hpbody : forall _ _, pBody _ = _ -> _ |- _ => apply Hpbody in H - end; [|solve [repeat find_rewrite; in_crush]]. + end; [|solve [repeat find_rewrite; in_crush_tac (intuition auto)]]. repeat find_rewrite; eauto. * repeat find_rewrite. unfold votes_received_cronies in *. @@ -463,7 +463,7 @@ Section CroniesCorrectProof. match goal with | H : pBody _ = _, Hpbody : forall _ _, pBody _ = _ -> _ |- _ => apply Hpbody in H - end; [|solve [repeat find_rewrite; in_crush]]. + end; [|solve [repeat find_rewrite; in_crush_tac (intuition auto)]]. repeat find_rewrite; eauto. * repeat find_rewrite. unfold votes_received_cronies in *. diff --git a/theories/RaftProofs/CroniesTermProof.v b/theories/RaftProofs/CroniesTermProof.v index d1c98f9..ebc699b 100644 --- a/theories/RaftProofs/CroniesTermProof.v +++ b/theories/RaftProofs/CroniesTermProof.v @@ -55,7 +55,7 @@ Section CroniesTermProof. intros. subst. simpl in *. repeat find_higher_order_rewrite. update_destruct; subst; rewrite_update; eauto. simpl in *. - find_eapply_lem_hyp handleTimeout_spec; eauto. intuition. + find_eapply_lem_hyp handleTimeout_spec; eauto. intuition (try lia). eapply Nat.le_trans; [|eauto]; eauto. Qed. @@ -153,7 +153,7 @@ Section CroniesTermProof. intros. unfold handleAppendEntriesReply, advanceCurrentTerm in *. repeat break_match; try find_inversion; subst; simpl in *; - do_bool; intuition. + do_bool; intuition lia. Qed. @@ -202,7 +202,6 @@ Section CroniesTermProof. eapply Nat.le_trans; [|eauto]; eauto. Qed. - Lemma handleRequestVoteReply_spec : forall h st h' t v st', st' = handleRequestVoteReply h st h' t v -> @@ -213,10 +212,9 @@ Section CroniesTermProof. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition. + do_bool; intuition lia. Qed. - Lemma cronies_term_request_vote_reply : refined_raft_net_invariant_request_vote_reply cronies_term. Proof using. diff --git a/theories/RaftProofs/CurrentTermGtZeroProof.v b/theories/RaftProofs/CurrentTermGtZeroProof.v index 31c6109..449cceb 100644 --- a/theories/RaftProofs/CurrentTermGtZeroProof.v +++ b/theories/RaftProofs/CurrentTermGtZeroProof.v @@ -29,7 +29,7 @@ Section CurrentTermGtZero. Proof using. unfold raft_net_invariant_timeout, current_term_gt_zero. simpl. intuition. find_higher_order_rewrite. update_destruct; subst; rewrite_update. - - find_apply_lem_hyp handleTimeout_type_strong. intuition. + - find_apply_lem_hyp handleTimeout_type_strong. intuition (try lia). repeat find_rewrite. auto. - auto. Qed. diff --git a/theories/RaftProofs/GhostLogAllEntriesProof.v b/theories/RaftProofs/GhostLogAllEntriesProof.v index 57ad97e..053ff91 100644 --- a/theories/RaftProofs/GhostLogAllEntriesProof.v +++ b/theories/RaftProofs/GhostLogAllEntriesProof.v @@ -45,7 +45,7 @@ Section GhostLogAllEntriesProof. unfold update_elections_data_appendEntries. intros. break_let. break_match; auto. break_if; auto. - simpl. intuition. + simpl. intuition (auto with datatypes). Qed. Lemma ghost_log_allEntries_append_entries : diff --git a/theories/RaftProofs/GhostLogCorrectProof.v b/theories/RaftProofs/GhostLogCorrectProof.v index a0d8339..fbae16b 100644 --- a/theories/RaftProofs/GhostLogCorrectProof.v +++ b/theories/RaftProofs/GhostLogCorrectProof.v @@ -181,7 +181,7 @@ Section GhostLogCorrectProof. eapply contiguous_findAtIndex; [eapply lifted_entries_sorted_invariant; eauto| eapply lifted_entries_contiguous_invariant; eauto|]. - intuition. + intuition (auto with arith). repeat find_rewrite. erewrite doLeader_getNextIndex; eauto. eapply lifted_nextIndex_safety_invariant; eauto. diff --git a/theories/RaftProofs/InputBeforeOutputProof.v b/theories/RaftProofs/InputBeforeOutputProof.v index 60495c0..516f8fa 100644 --- a/theories/RaftProofs/InputBeforeOutputProof.v +++ b/theories/RaftProofs/InputBeforeOutputProof.v @@ -59,8 +59,9 @@ Section InputBeforeOutput. induction (applied_entries (nwState net)); simpl in *; try congruence; intuition. - break_exists; intuition. - break_if; try congruence. - do_bool. - break_exists; break_if; try congruence; intuition; do_bool; subst; eauto. + do_bool. + break_exists; break_if; try congruence; + intuition (try lia); do_bool; subst; eauto. Qed. Lemma doGenericServer_applied_entries : @@ -77,14 +78,14 @@ Section InputBeforeOutput. use_applyEntries_spec. subst. simpl in *. unfold raft_data in *. simpl in *. break_if; [|rewrite applied_entries_safe_update; simpl in *; eauto; - exists nil; simpl in *; intuition]. + exists nil; simpl in *; intuition (auto with datatypes)]. do_bool. match goal with | |- context [update _ ?sigma ?h ?st] => pose proof applied_entries_update sigma h st end. simpl in *. assert (commitIndex (sigma h) >= lastApplied (sigma h)) by lia. - concludes. intuition; [find_rewrite; exists nil; simpl in *; intuition|]. + concludes. intuition; [find_rewrite; exists nil; simpl in *; intuition (auto with datatypes)|]. pose proof applied_entries_cases sigma. intuition; repeat find_rewrite; eauto; [eexists; intuition; eauto; @@ -226,10 +227,10 @@ Section InputBeforeOutput. forall l l', sorted (l ++ l') -> sorted l. - Proof using. + Proof using. induction l; simpl in *; intros; intuition eauto. - - apply H0. intuition. - - apply H0. intuition. + - apply H0. intuition (auto with datatypes). + - apply H0. intuition (auto with datatypes). Qed. Lemma handleMessage_applied_entries : @@ -275,7 +276,7 @@ Section InputBeforeOutput. end; copy_eapply_prop_hyp log_matching_nw AppendEntries; eauto; repeat (forwards; [intuition eauto; lia|]; concludes); - intuition; [eapply Nat.le_trans; eauto|]. + (intuition (auto with arith)); [eapply Nat.le_trans; eauto|]. match goal with | H : exists _, _ |- _ => destruct H as [e'] end. @@ -317,7 +318,7 @@ Section InputBeforeOutput. unfold state_machine_safety_nw in *. eapply_prop_hyp commit_recorded In; intuition; eauto; try lia; try solve [find_apply_lem_hyp logs_contiguous; auto; lia]. - unfold commit_recorded. intuition. + unfold commit_recorded. intuition lia. + repeat find_rewrite. find_copy_apply_lem_hyp logs_sorted_invariant. unfold logs_sorted in *. intuition. @@ -336,7 +337,7 @@ Section InputBeforeOutput. simpl in *. intuition eauto. forwards; eauto. concludes. forwards; [unfold commit_recorded in *; intuition eauto|]. concludes. - intuition; apply in_app_iff; + intuition (auto with datatypes); apply in_app_iff; try solve [right; eapply removeAfterIndex_le_In; eauto; lia]; exfalso. find_eapply_lem_hyp findAtIndex_max_thing; eauto using entries_max_thing. @@ -361,7 +362,7 @@ Section InputBeforeOutput. simpl in *. intuition eauto. forwards; eauto. concludes. forwards; [unfold commit_recorded in *; intuition eauto|]. concludes. - intuition; apply in_app_iff; + intuition (auto with datatypes); apply in_app_iff; try solve [right; eapply removeAfterIndex_le_In; eauto; lia]. subst. find_apply_lem_hyp maxIndex_non_empty. @@ -373,7 +374,7 @@ Section InputBeforeOutput. unfold state_machine_safety_nw in *. eapply rachet; eauto using sorted_app, sorted_uniqueIndices. copy_eapply_prop_hyp commit_recorded In; intuition; eauto; try lia; - unfold commit_recorded; intuition. + unfold commit_recorded; intuition (try lia). - exfalso. pose proof entries_gt_pli. eapply_prop_hyp AppendEntries AppendEntries; @@ -501,7 +502,7 @@ Section InputBeforeOutput. find_eapply_lem_hyp RIR_doLeader; simpl in *; eauto. simpl in *. find_copy_apply_lem_hyp handleMessage_applied_entries; repeat find_rewrite; eauto; - try solve [destruct p; simpl in *; intuition]. + try solve [destruct p; simpl in *; intuition (auto with datatypes)]. find_copy_apply_lem_hyp doLeader_appliedEntries. find_eapply_lem_hyp doGenericServer_applied_entries; eauto. break_exists. intuition. @@ -511,7 +512,7 @@ Section InputBeforeOutput. + contradict H1. eexists; intuition; repeat find_rewrite; eauto. + find_apply_hyp_hyp. break_exists. intuition. eapply handleMessage_log with (h'' := x1); eauto; - [destruct p; simpl in *; repeat find_rewrite; intuition|]. + [destruct p; simpl in *; repeat find_rewrite; intuition (auto with datatypes)|]. update_destruct; subst; rewrite_update; eauto. find_apply_lem_hyp doLeader_log. repeat find_rewrite. auto. - unfold RaftInputHandler in *. repeat break_let. subst. @@ -598,11 +599,11 @@ Section InputBeforeOutput. apply Bool.not_true_iff_false. intuition. find_false. unfold is_output_with_key in *. break_match; subst. repeat break_match; try congruence. - exists l, n. intuition. + exists l, n. intuition (auto with datatypes). * conclude_using eauto. conclude_using ltac:(intros; find_false; unfold key_in_output_trace in *; - break_exists_exists; intuition). + break_exists_exists; intuition (auto with datatypes)). eauto. Qed. @@ -620,10 +621,10 @@ Section InputBeforeOutput. apply Bool.not_true_iff_false. intuition. find_false. unfold is_output_with_key in *. break_match; subst. repeat break_match; try congruence. - exists l, n. intuition. + exists l, n. intuition (auto with datatypes). + conclude_using ltac:(intros; find_false; unfold key_in_output_trace in *; - break_exists_exists; intuition). + break_exists_exists; intuition (auto with datatypes)). eauto. Qed. diff --git a/theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v b/theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v index 01cbb8a..c60ca89 100644 --- a/theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v +++ b/theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v @@ -39,7 +39,7 @@ Section LastAppliedCommitIndexMatching. cut (e = e'); [intros; subst; auto|] end. eapply_prop state_machine_safety_host; unfold commit_recorded; intuition eauto; - simpl in *; intuition. + simpl in *; intuition lia. - unfold log_matching_hosts in *. intuition. simpl in *. match goal with | H : forall (_ : name) (_ : nat), _ |- In ?e (_ (_ ?h)) => @@ -55,7 +55,7 @@ Section LastAppliedCommitIndexMatching. cut (e = e'); [intros; subst; auto|] end. eapply_prop state_machine_safety_host; unfold commit_recorded; intuition eauto; - simpl in *; intuition. + simpl in *; intuition lia. Qed. Theorem commitIndex_lastApplied_match_invariant : @@ -84,7 +84,7 @@ Section LastAppliedCommitIndexMatching. cut (e = e'); [intros; subst; auto|] end. eapply_prop state_machine_safety_host; unfold commit_recorded; intuition eauto; - simpl in *; intuition. + simpl in *; intuition lia. - unfold log_matching_hosts in *. intuition. simpl in *. match goal with | H : forall (_ : name) (_ : nat), _ |- In ?e (_ (_ ?h)) => @@ -100,7 +100,7 @@ Section LastAppliedCommitIndexMatching. cut (e = e'); [intros; subst; auto|] end. eapply_prop state_machine_safety_host; unfold commit_recorded; intuition eauto; - simpl in *; intuition. + simpl in *; intuition lia. Qed. Theorem lastApplied_lastApplied_match_invariant : @@ -129,7 +129,7 @@ Section LastAppliedCommitIndexMatching. cut (e = e'); [intros; subst; auto|] end. eapply_prop state_machine_safety_host; unfold commit_recorded; intuition eauto; - simpl in *; intuition. + simpl in *; intuition lia. - unfold log_matching_hosts in *. intuition. simpl in *. match goal with | H : forall (_ : name) (_ : nat), _ |- In ?e (_ (_ ?h)) => @@ -145,7 +145,7 @@ Section LastAppliedCommitIndexMatching. cut (e = e'); [intros; subst; auto|] end. eapply_prop state_machine_safety_host; unfold commit_recorded; intuition eauto; - simpl in *; intuition. + simpl in *; intuition lia. Qed. Instance lacimi : lastApplied_commitIndex_match_interface. diff --git a/theories/RaftProofs/LastAppliedLeCommitIndexProof.v b/theories/RaftProofs/LastAppliedLeCommitIndexProof.v index 80b0acc..b8ffbe5 100644 --- a/theories/RaftProofs/LastAppliedLeCommitIndexProof.v +++ b/theories/RaftProofs/LastAppliedLeCommitIndexProof.v @@ -92,7 +92,7 @@ Section LastAppliedLeCommitIndex. intros. do_in_map. subst. find_apply_lem_hyp filter_In. - repeat (intuition; do_bool). + repeat (intuition (auto with arith); do_bool). Qed. Lemma doLeader_same_commitIndex : diff --git a/theories/RaftProofs/LeaderCompletenessProof.v b/theories/RaftProofs/LeaderCompletenessProof.v index 7c5d924..0bad450 100644 --- a/theories/RaftProofs/LeaderCompletenessProof.v +++ b/theories/RaftProofs/LeaderCompletenessProof.v @@ -159,8 +159,8 @@ Section LeaderCompleteness. In h nodes -> In (t', l) (contradicting_leader_logs_on_leader (leaderLogs (fst (nwState net h))) t e) -> In (t', h, l) (contradicting_leader_logs net nodes t e). - Proof using. - induction nodes; intros; simpl in *; intuition. + Proof using. + induction nodes; intros; simpl in *; intuition (auto with datatypes). apply in_or_app. subst. left. apply in_map_iff. eexists. intuition eauto. simpl. auto. Qed. diff --git a/theories/RaftProofs/LeaderLogsContiguousProof.v b/theories/RaftProofs/LeaderLogsContiguousProof.v index 9a5e0d5..1fc20c7 100644 --- a/theories/RaftProofs/LeaderLogsContiguousProof.v +++ b/theories/RaftProofs/LeaderLogsContiguousProof.v @@ -64,7 +64,7 @@ Section LeaderLogsContiguous. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition. + do_bool; intuition (auto with arith). Qed. Lemma update_elections_data_requestVoteReply_leaderLogs : diff --git a/theories/RaftProofs/LeaderLogsLogMatchingProof.v b/theories/RaftProofs/LeaderLogsLogMatchingProof.v index a116095..993fcb8 100644 --- a/theories/RaftProofs/LeaderLogsLogMatchingProof.v +++ b/theories/RaftProofs/LeaderLogsLogMatchingProof.v @@ -350,7 +350,7 @@ Section LeaderLogsLogMatching. match goal with | [ H : _ |- _ ] => eapply H; [|eauto]; - repeat find_rewrite; intuition + repeat find_rewrite; intuition (auto with datatypes) end. Lemma handleAppendEntries_doesn't_send_AE : @@ -426,7 +426,8 @@ Section LeaderLogsLogMatching. - eapply leaderLogs_entries_match_nw_packet_set; eauto; simpl. + intros. find_apply_hyp_hyp. repeat find_rewrite. intuition; [eauto with *|]. find_apply_lem_hyp handleAppendEntriesReply_packets. subst. simpl in *. intuition. - + intros. repeat find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto; find_rewrite; auto. + + intros. repeat find_higher_order_rewrite; update_destruct_simplify; rewrite_update; + auto; find_rewrite; auto. Qed. Lemma handleRequestVote_packets : @@ -436,7 +437,7 @@ Section LeaderLogsLogMatching. Proof using. intros. unfold handleRequestVote, advanceCurrentTerm in *. repeat break_match; find_inversion; - subst; intuition; break_exists; congruence. + subst; intuition auto; break_exists; congruence. Qed. Lemma leaderLogs_entries_match_request_vote : @@ -548,7 +549,7 @@ Section LeaderLogsLogMatching. remember (x) as index; specialize (H index); forward H end. - + intuition; auto using Nat.neq_0_lt_0. + + intuition (try lia); auto using Nat.neq_0_lt_0. find_apply_lem_hyp findGtIndex_necessary. break_and. eapply Nat.le_trans. * apply Nat.lt_le_incl. eauto. diff --git a/theories/RaftProofs/LeaderLogsPreservedProof.v b/theories/RaftProofs/LeaderLogsPreservedProof.v index 73925e8..f94ae6d 100644 --- a/theories/RaftProofs/LeaderLogsPreservedProof.v +++ b/theories/RaftProofs/LeaderLogsPreservedProof.v @@ -91,7 +91,7 @@ Section LeaderLogsPreserved. simpl in *. intuition. find_inversion. right. unfold handleRequestVoteReply in *. - repeat break_match; simpl in *; intuition; try congruence; + repeat break_match; simpl in *; intuition auto; try congruence; break_if; try congruence; do_bool; eauto using Nat.le_antisymm. Qed. diff --git a/theories/RaftProofs/LeaderLogsSublogProof.v b/theories/RaftProofs/LeaderLogsSublogProof.v index 282527a..7ae83b7 100644 --- a/theories/RaftProofs/LeaderLogsSublogProof.v +++ b/theories/RaftProofs/LeaderLogsSublogProof.v @@ -192,8 +192,8 @@ Section LeaderLogsSublog. Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try right; congruence. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition (auto with arith); try right; congruence. Qed. Lemma contradict_leaderLogs_term_sanity : diff --git a/theories/RaftProofs/LeaderLogsTermSanityProof.v b/theories/RaftProofs/LeaderLogsTermSanityProof.v index fac9ccd..9db2ed9 100644 --- a/theories/RaftProofs/LeaderLogsTermSanityProof.v +++ b/theories/RaftProofs/LeaderLogsTermSanityProof.v @@ -134,7 +134,7 @@ Section LeaderLogsTermSanity. Proof using. currentTerm_sanity_unchanged. - apply update_elections_data_client_request_leaderLogs. - - find_apply_lem_hyp handleClientRequest_type. intuition. + - find_apply_lem_hyp handleClientRequest_type. intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_timeout : @@ -142,7 +142,7 @@ Section LeaderLogsTermSanity. Proof using. currentTerm_sanity_unchanged. - apply update_elections_data_timeout_leaderLogs. - - find_apply_lem_hyp handleTimeout_type_strong. intuition. + - find_apply_lem_hyp handleTimeout_type_strong. intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_append_entries : @@ -150,14 +150,14 @@ Section LeaderLogsTermSanity. Proof using. currentTerm_sanity_unchanged. - apply update_elections_data_appendEntries_leaderLogs. - - find_apply_lem_hyp handleAppendEntries_type_term. intuition. + - find_apply_lem_hyp handleAppendEntries_type_term. intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_append_entries_reply : refined_raft_net_invariant_append_entries_reply leaderLogs_currentTerm_sanity. Proof using. currentTerm_sanity_unchanged. - - find_apply_lem_hyp handleAppendEntriesReply_type_term. intuition. + - find_apply_lem_hyp handleAppendEntriesReply_type_term. intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_request_vote : @@ -165,7 +165,7 @@ Section LeaderLogsTermSanity. Proof using. currentTerm_sanity_unchanged. - apply leaderLogs_update_elections_data_requestVote. - - find_apply_lem_hyp handleRequestVote_type_term. intuition. + - find_apply_lem_hyp handleRequestVote_type_term. intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_request_vote_reply : @@ -188,7 +188,7 @@ Section LeaderLogsTermSanity. Proof using. currentTerm_sanity_unchanged. - find_rewrite. auto. - - find_rewrite. simpl. find_apply_lem_hyp doLeader_type. intuition. + - find_rewrite. simpl. find_apply_lem_hyp doLeader_type. intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_do_generic_server : @@ -196,7 +196,7 @@ Section LeaderLogsTermSanity. Proof using. currentTerm_sanity_unchanged. - find_rewrite. auto. - - find_rewrite. simpl. find_apply_lem_hyp doGenericServer_type. intuition. + - find_rewrite. simpl. find_apply_lem_hyp doGenericServer_type. intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_state_same_packet_subset : @@ -268,8 +268,8 @@ Section LeaderLogsTermSanity. Proof using. ctsc_unchanged. - apply update_elections_data_client_request_leaderLogs. - - find_apply_lem_hyp handleClientRequest_type; intuition. - - find_apply_lem_hyp handleClientRequest_type; intuition. + - find_apply_lem_hyp handleClientRequest_type; intuition lia. + - find_apply_lem_hyp handleClientRequest_type; intuition lia. Qed. Lemma leaderLogs_currentTerm_sanity_candidate_timeout : @@ -280,7 +280,7 @@ Section LeaderLogsTermSanity. find_apply_lem_hyp handleTimeout_type_strong. intuition. - repeat find_reverse_rewrite. find_apply_hyp_hyp. lia. - find_apply_lem_hyp leaderLogs_currentTerm_sanity_invariant; auto. - repeat find_rewrite. intuition. + repeat find_rewrite. intuition (auto with arith). Qed. Lemma leaderLogs_currentTerm_sanity_candidate_append_entries : @@ -288,7 +288,7 @@ Section LeaderLogsTermSanity. Proof using. ctsc_unchanged. - apply update_elections_data_appendEntries_leaderLogs. - - find_apply_lem_hyp handleAppendEntries_type_term. intuition. + - find_apply_lem_hyp handleAppendEntries_type_term. intuition lia. - find_apply_lem_hyp handleAppendEntries_type_term. intuition. right. congruence. Qed. @@ -296,7 +296,7 @@ Section LeaderLogsTermSanity. refined_raft_net_invariant_append_entries_reply leaderLogs_currentTerm_sanity_candidate. Proof using. ctsc_unchanged. - - find_apply_lem_hyp handleAppendEntriesReply_type_term. intuition. + - find_apply_lem_hyp handleAppendEntriesReply_type_term. intuition lia. - find_apply_lem_hyp handleAppendEntriesReply_type_term. intuition. right. congruence. Qed. @@ -305,7 +305,7 @@ Section LeaderLogsTermSanity. Proof using. ctsc_unchanged. - apply leaderLogs_update_elections_data_requestVote. - - find_apply_lem_hyp handleRequestVote_type_term. intuition. + - find_apply_lem_hyp handleRequestVote_type_term. intuition lia. - find_apply_lem_hyp handleRequestVote_type_term. intuition. right. congruence. Qed. @@ -327,7 +327,7 @@ Section LeaderLogsTermSanity. Proof using. ctsc_unchanged. - find_rewrite. auto. - - find_rewrite. simpl. find_apply_lem_hyp doLeader_type. intuition. + - find_rewrite. simpl. find_apply_lem_hyp doLeader_type. intuition lia. - find_rewrite. simpl. find_apply_lem_hyp doLeader_type. intuition. Qed. @@ -336,7 +336,7 @@ Section LeaderLogsTermSanity. Proof using. ctsc_unchanged. - find_rewrite. auto. - - find_rewrite. simpl. find_apply_lem_hyp doGenericServer_type. intuition. + - find_rewrite. simpl. find_apply_lem_hyp doGenericServer_type. intuition lia. - find_rewrite. simpl. find_apply_lem_hyp doGenericServer_type. intuition. Qed. diff --git a/theories/RaftProofs/LogMatchingProof.v b/theories/RaftProofs/LogMatchingProof.v index de55974..03a691f 100644 --- a/theories/RaftProofs/LogMatchingProof.v +++ b/theories/RaftProofs/LogMatchingProof.v @@ -114,7 +114,7 @@ Section LogMatchingProof. | [ H : forall _ _ _ _ _ _ _, In _ _ -> Net.pBody _ = _ -> _, H' : Net.pBody ?p = AppendEntries _ _ _ _ ?xs _, _ : In ?p (nwPackets _) |- _] => - apply H in H'; clear H; intuition + apply H in H'; clear H; intuition (auto with datatypes) end. Ltac rewrite_if_log := @@ -158,23 +158,23 @@ Section LogMatchingProof. | [ H : forall _, uniqueIndices _ |- _ ] => apply H end. - Ltac use_log_matching_nw_nw := + Tactic Notation "use_log_matching_nw_nw_tac" tactic(tac) := match goal with | [ H : forall _ _ _ _ _ _ _, In _ _ -> _, Hp' : Net.pBody ?p' = AppendEntries _ _ _ _ ?entries' _, Hp : Net.pBody ?p = _ |- context [ In _ ?entries' ] ] => - apply H in Hp; clear H; intuition + apply H in Hp; clear H; tac | [ H : forall _ _ _ _ _ _ _, In _ _ -> _, Hp : Net.pBody _ = AppendEntries _ _ _ _ _ _, Hp' : Net.pBody _ = AppendEntries _ _ (eIndex ?e'') _ _ _ |- _ ] => - apply H in Hp; auto; intuition; clear H + apply H in Hp; auto; tac; clear H | [ H : forall _ _ _ _ _ _ _, In _ _ -> _, Hp' : Net.pBody ?p' = AppendEntries _ _ _ ?plt' _ _, Hp : Net.pBody ?p = _ |- ?plt = ?plt' ] => - apply H in Hp; auto; intuition; clear H + apply H in Hp; auto; tac; clear H end; try match goal with | [ H : forall _ _ _ _ _ _ _, In _ _ -> _, @@ -182,7 +182,10 @@ Section LogMatchingProof. Hp : Net.pBody ?p = _ |- _ ] => eapply H with (e1:=e)(e2:=e') in Hp; eauto - end; intuition. + end; tac. + + Tactic Notation "use_log_matching_nw_nw" := + use_log_matching_nw_nw_tac intuition. Ltac shouldSend_true := match goal with @@ -226,7 +229,7 @@ Section LogMatchingProof. | [ _ : eIndex ?e = eIndex ?e', H : forall _ _ _, In _ _ -> _ |- context [?h] ] => specialize (H h e e') - end; repeat concludes; intuition. + end; repeat concludes; intuition (auto with zarith). + simpl in *. shouldSend_true. unfold log_matching_hosts in *. @@ -261,7 +264,7 @@ Section LogMatchingProof. | [ H : forall _ _, 1 <= _ <= _ -> _ |- context [eIndex _ = ?x] ] => remember (x) as index; specialize (H leaderId index); forward H end. - * intuition; try (destruct index; intuition; lia). + * intuition auto; try (destruct index; intuition auto; lia). match goal with | _ : eIndex ?e > index, _ : In ?e ?l |- _ => pose proof maxIndex_is_max l e @@ -305,7 +308,7 @@ Section LogMatchingProof. eexists; intuition; eauto; eauto using findGtIndex_sufficient. unfold logs_sorted in *. - apply findGtIndex_sufficient; intuition. + apply findGtIndex_sufficient; intuition (auto; try lia). - use_packet_subset_clear. + unfold log_matching, log_matching_nw in *; intuition. use_nw_invariant. + shouldSend_true. simpl in *. clean. @@ -367,7 +370,7 @@ Section LogMatchingProof. simpl in *. clean. repeat do_in_map. simpl in *. do 2 (find_inversion; simpl in *). repeat do_elim. - use_log_matching_nw_host; repeat concludes; intuition. + use_log_matching_nw_host; repeat concludes; intuition (try lia). break_exists. intuition. match goal with | _ : eIndex ?x = eIndex ?y |- context [ ?y ] => @@ -407,7 +410,7 @@ Section LogMatchingProof. concludes. unfold logs_sorted in *. forwards; - [find_apply_lem_hyp maxIndex_is_max; intuition; lia|]. + [find_apply_lem_hyp maxIndex_is_max; intuition auto; lia|]. concludes. break_exists. intuition. eapply findAtIndex_None; intuition eauto. + shouldSend_true. simpl in *. clean. @@ -713,7 +716,7 @@ Ltac assert_do_leader := match goal with | [ _ : S (maxIndex ?l) <= eIndex ?e, He : In ?e ?l |- _ ] => - exfalso; apply maxIndex_is_max in He; intuition; lia + exfalso; apply maxIndex_is_max in He; intuition auto; lia end. Lemma handleClientRequest_log_matching_hosts_entries_match : @@ -845,12 +848,12 @@ Ltac assert_do_leader := - right. unfold log_matching_nw in *. intuition. find_apply_hyp_hyp. intuition. use_nw_invariant. - use_log_matching_nw_host. intuition. + use_log_matching_nw_host. intuition (auto with zarith). } * unfold log_matching_nw in *. find_apply_hyp_hyp. intuition. use_nw_invariant. - use_log_matching_nw_host. intuition. + use_log_matching_nw_host. intuition (auto with zarith). + break_if; subst. * { intuition. - subst. simpl in *. find_copy_apply_lem_hyp leader_sublog_invariant_invariant. @@ -880,7 +883,7 @@ Ltac assert_do_leader := use_nw_invariant. + unfold log_matching_nw in *. do 2 (find_apply_hyp_hyp; intuition). subst. - use_log_matching_nw_nw. + use_log_matching_nw_nw_tac (intuition (auto with zarith)). + unfold log_matching_nw in *. do 2 (find_apply_hyp_hyp; intuition). subst. use_log_matching_nw_nw. @@ -1071,7 +1074,8 @@ Ltac assert_do_leader := match goal with | _ : nwPackets ?net = ?xs ++ ?p :: ?ys, p : packet |- _ => - assert (In p (nwPackets net)) by (repeat find_rewrite; in_crush) + assert (In p (nwPackets net)) by + (repeat find_rewrite; in_crush_tac (intuition (auto with datatypes))) end. Ltac contradict_append_entries := @@ -1195,8 +1199,8 @@ Ltac assert_do_leader := eapply Nat.le_lt_trans; [lia|eapply H; eauto] end. congruence. - + use_nw_invariant; try solve [in_crush]. - use_log_matching_nw_host. intuition. + + use_nw_invariant; try solve [in_crush_tac (intuition auto)]. + use_log_matching_nw_host. intuition (auto with zarith). - break_if. + subst. match goal with @@ -1231,7 +1235,7 @@ Ltac assert_do_leader := | H : pBody _ = AppendEntries _ _ _ _ (log _) _ |- _ => clear H end. - use_log_matching_nw_nw. + use_log_matching_nw_nw_tac (intuition (auto with zarith)). - match goal with | H : pBody _ = AppendEntries _ _ _ _ (log _) _ |- _ => clear H @@ -1280,7 +1284,7 @@ Ltac assert_do_leader := * unfold log_matching_nw in *. prove_in. use_nw_invariant. - find_apply_hyp_hyp. intuition. + find_apply_hyp_hyp. intuition lia. * find_apply_lem_hyp removeAfterIndex_in. unfold log_matching_hosts in *. intuition eauto. + unfold log_matching_hosts in *. intuition eauto. @@ -1352,7 +1356,7 @@ Ltac assert_do_leader := } - apply in_or_app. left. unfold log_matching_nw in *. - use_log_matching_nw_nw. + use_log_matching_nw_nw_tac (intuition (auto with zarith)). } * (* e2 old *) apply in_or_app. right. @@ -1362,11 +1366,11 @@ Ltac assert_do_leader := find_apply_lem_hyp removeAfterIndex_in. apply removeAfterIndex_le_In; [lia|]. use_log_matching_nw_host. - intuition. eapply_prop logs_sorted_host. + intuition (auto with zarith). eapply_prop logs_sorted_host. + unfold log_matching_nw in *. use_nw_invariant. use_log_matching_nw_host. - intuition. + intuition (auto with zarith). - simpl in *. { break_if. - subst. repeat find_rewrite. @@ -1426,11 +1430,11 @@ Ltac assert_do_leader := repeat find_rewrite. exists x1. intuition. apply in_or_app. right. - apply removeAfterIndex_le_In; intuition. + apply removeAfterIndex_le_In; intuition lia. * subst. break_exists. intuition. do_elim. eexists; intuition eauto. apply in_or_app. right. - apply removeAfterIndex_le_In; intuition. + apply removeAfterIndex_le_In; intuition lia. * match goal with | [ H : forall _, pli < _ <= _ -> _ |- _ ] => specialize (H prevLogIndex); @@ -1443,7 +1447,7 @@ Ltac assert_do_leader := eapply maxIndex_is_max; eauto]) end. - break_exists. exists x. intuition. + break_exists. exists x. intuition (auto with datatypes). + (* e2 old *) unfold log_matching_nw in *. repeat find_rewrite. @@ -1476,7 +1480,7 @@ Ltac assert_do_leader := - simpl in *. unfold log_matching_nw in *. repeat find_rewrite. - use_log_matching_nw_nw. + use_log_matching_nw_nw_tac (intuition (auto with zarith)). - simpl in *. unfold log_matching_nw in *. repeat find_rewrite. diff --git a/theories/RaftProofs/LogsLeaderLogsProof.v b/theories/RaftProofs/LogsLeaderLogsProof.v index 30deb6c..5053873 100644 --- a/theories/RaftProofs/LogsLeaderLogsProof.v +++ b/theories/RaftProofs/LogsLeaderLogsProof.v @@ -176,10 +176,12 @@ Section LogsLeaderLogs. match goal with | [ _ : nwPackets ?net = _, _ : In ?p _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; do_in_app; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; do_in_app; intuition (auto with datatypes)) | [ _ : nwPackets ?net = _, _ : pBody ?p = _ |- _] => - assert (In p (nwPackets net)) by (repeat find_rewrite; intuition) + assert (In p (nwPackets net)) by + (repeat find_rewrite; intuition (auto with datatypes)) end. Lemma contiguous_log_property : @@ -268,7 +270,7 @@ Section LogsLeaderLogs. | _ : removeAfterIndex _ ?index = _ ++ ?e :: _ |- _ => assert (In e es) by (apply removeAfterIndex_in with (i := index); - repeat find_rewrite; intuition) + repeat find_rewrite; intuition (auto with datatypes)) end. eapply_prop_hyp In In. lia. } subst. rewrite app_nil_r in *. @@ -350,7 +352,7 @@ Section LogsLeaderLogs. | _ : removeAfterIndex _ ?index = _ ++ ?e :: _ |- _ => assert (In e es) by (apply removeAfterIndex_in with (i := index); - repeat find_rewrite; intuition) + repeat find_rewrite; intuition (auto with datatypes)) end. clear H0 H7. eapply_prop_hyp In In. lia. @@ -599,7 +601,7 @@ Section LogsLeaderLogs. | _ : S _ = pred ?x |- context [pred ?y] => assert (pred x = pred y) by auto end. - repeat find_rewrite. intuition. + repeat find_rewrite. intuition lia. Qed. Lemma logs_leaderLogs_inductive_doLeader : diff --git a/theories/RaftProofs/MatchIndexAllEntriesProof.v b/theories/RaftProofs/MatchIndexAllEntriesProof.v index 0b15d32..1efd2b0 100644 --- a/theories/RaftProofs/MatchIndexAllEntriesProof.v +++ b/theories/RaftProofs/MatchIndexAllEntriesProof.v @@ -411,7 +411,7 @@ Section MatchIndexAllEntries. repeat (do_bool; repeat break_and). + find_apply_lem_hyp not_empty_true_elim. pose proof maxIndex_non_empty es ltac:(auto). - break_exists_exists. intuition. + break_exists_exists. intuition (auto with datatypes). + break_or_hyp. * find_apply_lem_hyp not_empty_false_elim. congruence. * break_match; try discriminate. @@ -816,10 +816,10 @@ Section MatchIndexAllEntries. Proof using. unfold handleRequestVoteReply. intros. - repeat break_match; repeat find_inversion; do_bool; subst; simpl; intuition. + repeat break_match; repeat find_inversion; do_bool; subst; simpl; + intuition (auto with arith). Qed. - Lemma match_index_all_entries_request_vote_reply : refined_raft_net_invariant_request_vote_reply match_index_all_entries_inv. Proof using cci vci cei laei taifoli rri. diff --git a/theories/RaftProofs/OneLeaderLogPerTermProof.v b/theories/RaftProofs/OneLeaderLogPerTermProof.v index cac7b9f..0476762 100644 --- a/theories/RaftProofs/OneLeaderLogPerTermProof.v +++ b/theories/RaftProofs/OneLeaderLogPerTermProof.v @@ -106,7 +106,7 @@ Section OneLeaderLogPerTerm. simpl in *. intuition. find_inversion. right. unfold handleRequestVoteReply in *. - repeat break_match; simpl in *; intuition; try congruence; + repeat break_match; simpl in *; intuition auto; try congruence; break_if; try congruence; do_bool; eauto using Nat.le_antisymm. Qed. diff --git a/theories/RaftProofs/OutputCorrectProof.v b/theories/RaftProofs/OutputCorrectProof.v index f75f812..5237be9 100644 --- a/theories/RaftProofs/OutputCorrectProof.v +++ b/theories/RaftProofs/OutputCorrectProof.v @@ -54,7 +54,7 @@ Section OutputCorrect. unfold in_output_list in *. break_exists. find_eapply_lem_hyp find_none; eauto. simpl in *. find_apply_lem_hyp Bool.andb_false_elim. - break_if; repeat (intuition; do_bool). + break_if; repeat (intuition (auto with bool); do_bool). break_if; congruence. Qed. @@ -148,7 +148,7 @@ Section OutputCorrect. in_output_list c i o l2. Proof using. unfold in_output_list. - intuition. + intuition (auto with datatypes). Qed. Lemma in_output_trace_inp_inv : @@ -355,7 +355,7 @@ Section OutputCorrect. end. intros. find_eapply_lem_hyp find_none; eauto. - simpl in *. break_if; repeat (do_bool; intuition); try congruence. + simpl in *. break_if; repeat (do_bool; intuition auto); try congruence. Qed. (* FIXME: move to StructTact *) @@ -514,7 +514,8 @@ Section OutputCorrect. Proof using. unfold applyEntry. intros. - repeat break_match; repeat find_inversion. intuition. + repeat break_match; repeat find_inversion. + intuition (auto with datatypes). Qed. Lemma cacheApplyEntry_clientCache : @@ -658,12 +659,13 @@ Section OutputCorrect. { intuition. - eapply_prop_hyp In In. break_exists. break_and. find_copy_eapply_lem_hyp cacheAppliedEntry_clientCache_preserved; eauto. - break_exists_exists. intuition. + break_exists_exists. + intuition lia. - subst. find_copy_apply_lem_hyp cacheApplyEntry_clientCache. intuition. + break_exists. break_and. find_copy_eapply_lem_hyp cacheAppliedEntry_clientCache_preserved; eauto. - break_exists_exists. intuition. + break_exists_exists. intuition lia. + break_let. break_and. unfold getLastId. repeat find_rewrite. eexists. eexists. rewrite get_set_same. intuition eauto. + break_let. break_and. unfold getLastId. repeat find_rewrite. @@ -752,7 +754,7 @@ Section OutputCorrect. match goal with | |- context [applied_entries (update _ ?sigma ?h ?st)] => pose proof applied_entries_update sigma h st - end. conclude_using intuition. + end. conclude_using ltac:(intuition (auto with arith)). intuition; simpl in *; unfold raft_data in *; simpl in *; find_rewrite; auto using Prefix_refl. unfold applied_entries in *. diff --git a/theories/RaftProofs/OutputGreatestIdProof.v b/theories/RaftProofs/OutputGreatestIdProof.v index 07f20a2..4128348 100644 --- a/theories/RaftProofs/OutputGreatestIdProof.v +++ b/theories/RaftProofs/OutputGreatestIdProof.v @@ -89,7 +89,7 @@ Section OutputGreatestId. Proof using. intros. unfold has_key in *. break_match. simpl in *. subst. - break_if; repeat (do_bool; intuition); try congruence. + break_if; repeat (do_bool; intuition (auto with bool)); try congruence. Qed. Lemma applyEntries_cache : @@ -222,7 +222,7 @@ Section OutputGreatestId. find_apply_lem_hyp In_rev; apply Bool.not_true_iff_false; intuition; unfold has_key in *; - break_match; break_if; repeat (do_bool; intuition); simpl in *; + break_match; break_if; repeat (do_bool; intuition (auto with bool)); simpl in *; eapply_prop_hyp client_cache_complete In; eauto; break_exists; intuition; simpl in *; subst; @@ -240,7 +240,7 @@ Section OutputGreatestId. match goal with | |- context [applied_entries (update _ ?sigma ?h ?st)] => pose proof applied_entries_update sigma h st - end. conclude_using intuition. + end. conclude_using ltac:(intuition (auto with arith)). intuition; simpl in *; unfold raft_data in *; simpl in *; find_rewrite; auto using Prefix_refl. unfold applied_entries in *. diff --git a/theories/RaftProofs/OutputImpliesAppliedProof.v b/theories/RaftProofs/OutputImpliesAppliedProof.v index e5892d2..ed50ebf 100644 --- a/theories/RaftProofs/OutputImpliesAppliedProof.v +++ b/theories/RaftProofs/OutputImpliesAppliedProof.v @@ -116,7 +116,7 @@ Section OutputImpliesApplied. match goal with | |- context [update _ ?st ?h ?st'] => pose proof applied_entries_update st h st' - end. forwards; [simpl in *; intuition|]. concludes. + end. forwards; [simpl in *; intuition (auto with arith)|]. concludes. intuition. - simpl in *. unfold raft_data in *. simpl in *. find_rewrite. @@ -127,7 +127,7 @@ Section OutputImpliesApplied. match goal with | |- In _ (rev ?l') => apply in_rev with (l := l') end. - apply removeAfterIndex_le_In; intuition. + apply removeAfterIndex_le_In; intuition (try lia). find_copy_apply_lem_hyp log_matching_invariant. find_copy_apply_lem_hyp max_index_sanity_invariant. find_apply_lem_hyp state_machine_safety_invariant. @@ -136,7 +136,7 @@ Section OutputImpliesApplied. match goal with | [ e : entry, H : forall _ _, _ <= _ <= _ -> _, Hm : maxIndex_lastApplied _ |- In _ (log (_ _ ?h)) ] => - specialize (H h (eIndex e)); specialize (Hm h); forward H; intuition + specialize (H h (eIndex e)); specialize (Hm h); forward H; intuition (try lia) end. break_exists. intuition. find_apply_lem_hyp findGtIndex_necessary. intuition. match goal with diff --git a/theories/RaftProofs/PrefixWithinTermProof.v b/theories/RaftProofs/PrefixWithinTermProof.v index 8104615..8c252aa 100644 --- a/theories/RaftProofs/PrefixWithinTermProof.v +++ b/theories/RaftProofs/PrefixWithinTermProof.v @@ -171,7 +171,7 @@ Section PrefixWithinTerm. end. find_eapply_lem_hyp one_leaderLog_per_term_log_invariant; eauto. conclude_using eauto. subst. - intuition; subst. + intuition auto; subst. - destruct (lt_eq_lt_dec (eIndex e) pli'); intuition. left. match goal with @@ -375,7 +375,7 @@ Section PrefixWithinTerm. end. all:eauto. all:intuition. * eapply_prop_hyp eTerm In. congruence. * replace (eIndex e) with (eIndex x8). - eapply_prop (contiguous_range_exact_lo (x1 ++ x2)); eauto. in_crush. + eapply_prop (contiguous_range_exact_lo (x1 ++ x2)); eauto. in_crush_tac (intuition auto). + exfalso. find_eapply_lem_hyp Prefix_maxIndex; [|idtac|eauto]; eauto. match goal with @@ -731,7 +731,7 @@ Section PrefixWithinTerm. eapply H with (es := es) (p := p) (p' := p') end. 7: { eauto. } - all:repeat find_rewrite. all:eauto. intuition. + all:repeat find_rewrite. all:eauto. intuition lia. + exfalso. find_eapply_lem_hyp Prefix_maxIndex; [|idtac|eauto]; eauto. find_eapply_lem_hyp contiguous_0_app; eauto. lia. @@ -964,10 +964,10 @@ Section PrefixWithinTerm. find_apply_lem_hyp allEntries_gt_0_invariant; eauto. lia. + unfold prefix_within_term, allEntries_append_entries_prefix_within_term_nw in *. intros. - find_apply_lem_hyp update_elections_data_appendEntries_allEntries. intuition. + find_apply_lem_hyp update_elections_data_appendEntries_allEntries. intuition (auto with datatypes). do_in_app. intuition. * { - copy_eapply_prop_hyp pBody pBody; eauto. intuition. + copy_eapply_prop_hyp pBody pBody; eauto. intuition (auto with datatypes). - subst. apply in_app_iff. right. apply removeAfterIndex_le_In; auto. break_exists. intuition. @@ -999,7 +999,7 @@ Section PrefixWithinTerm. intros. do_in_app. intuition. * { - copy_eapply_prop_hyp pBody pBody; eauto. intuition. + copy_eapply_prop_hyp pBody pBody; eauto. intuition (auto with datatypes). - subst. apply in_app_iff. right. apply removeAfterIndex_le_In; auto. break_exists. intuition. @@ -1079,12 +1079,12 @@ Section PrefixWithinTerm. end. conclude_using ltac:(repeat find_rewrite; in_crush). concludes. - conclude_using ltac:(repeat find_rewrite; in_crush). + conclude_using ltac:(repeat find_rewrite; in_crush_tac (intuition auto)). repeat concludes. intuition. * exfalso. match goal with | _ : eIndex ?e = 0 |- _ => - cut (eIndex e > 0); [intuition|] + cut (eIndex e > 0); [intuition (try lia)|] end. eapply entries_gt_0_nw_invariant; [|idtac|idtac|eauto]; [|idtac|eauto]; eauto. * lia. @@ -1101,8 +1101,8 @@ Section PrefixWithinTerm. end. conclude_using ltac:(repeat find_rewrite; in_crush). concludes. - conclude_using ltac:(repeat find_rewrite; in_crush). - repeat concludes. intuition. + conclude_using ltac:(repeat find_rewrite; in_crush_tac (intuition auto)). + repeat concludes. intuition (auto with datatypes). + (* use log matching *) break_exists. intuition. subst. @@ -1127,7 +1127,7 @@ Section PrefixWithinTerm. 6: { eauto. } 5: { eauto. } 2: { eauto. } - all:eauto; repeat find_rewrite; intuition. + all:eauto; repeat find_rewrite; intuition lia. - apply in_app_iff. right. find_copy_apply_lem_hyp removeAfterIndex_in. find_apply_lem_hyp removeAfterIndex_In_le; [|eapply entries_sorted_invariant; eauto]. @@ -1326,7 +1326,7 @@ Section PrefixWithinTerm. | _ : S _ = pred ?x |- context [pred ?y] => assert (pred x = pred y) by auto end. - repeat find_rewrite. intuition. + repeat find_rewrite. intuition lia. Qed. Lemma doLeader_in_entries_in_log : @@ -1336,7 +1336,7 @@ Section PrefixWithinTerm. snd m = AppendEntries t n pli plt es ci -> In e es -> In e (log st). Proof using. - intros. unfold doLeader, advanceCommitIndex in *. + intros. unfold doLeader, advanceCommitIndex in *. break_match; try solve [find_inversion; simpl in *; intuition]. break_if; try solve [find_inversion; simpl in *; intuition]. find_inversion. do_in_map. subst. simpl in *. find_inversion. diff --git a/theories/RaftProofs/PrevLogLeaderSublogProof.v b/theories/RaftProofs/PrevLogLeaderSublogProof.v index 9058845..a41b206 100644 --- a/theories/RaftProofs/PrevLogLeaderSublogProof.v +++ b/theories/RaftProofs/PrevLogLeaderSublogProof.v @@ -42,7 +42,7 @@ Section PrevLogLeaderSublogProof. find_apply_lem_hyp handleClientRequest_log. intuition. - find_rewrite. auto. - - break_exists. intuition. find_rewrite. intuition. + - break_exists. intuition. find_rewrite. intuition (auto with datatypes). Qed. Lemma prevLog_leader_sublog_client_request : @@ -252,7 +252,8 @@ Section PrevLogLeaderSublogProof. Proof using. unfold handleRequestVoteReply. intros. - repeat break_match; repeat find_inversion; subst; simpl in *; auto; do_bool; intuition. + repeat break_match; repeat find_inversion; subst; simpl in *; auto; + do_bool; intuition lia. Qed. Lemma prevLog_leader_sublog_request_vote_reply : diff --git a/theories/RaftProofs/RaftMsgRefinementProof.v b/theories/RaftProofs/RaftMsgRefinementProof.v index 8451449..225c1fb 100644 --- a/theories/RaftProofs/RaftMsgRefinementProof.v +++ b/theories/RaftProofs/RaftMsgRefinementProof.v @@ -91,7 +91,7 @@ Section RaftMsgRefinement. (post_ghost_state, r0) l4); nwState := update name_eq_dec (nwState net) (pDst p) (post_ghost_state, r0) |}) - by (subst; eapply MRRIR_handleMessage; eauto; in_crush). + by (subst; eapply MRRIR_handleMessage; eauto; in_crush_tac (intuition auto)). assert (msg_refined_raft_intermediate_reachable {| @@ -106,7 +106,7 @@ Section RaftMsgRefinement. nwState := update name_eq_dec (nwState net) (pDst p) (post_ghost_state, r1) |}) by (eapply MRRIR_doLeader; eauto; - try solve [in_crush]; + try solve [in_crush_tac (intuition (auto with datatypes))]; simpl in *; intros; repeat break_if; try congruence; auto). subst. eapply_prop msg_refined_raft_net_invariant_do_generic_server. eauto. @@ -134,7 +134,7 @@ Section RaftMsgRefinement. simpl in *. intros. repeat break_if; auto. intros. simpl in *. - in_crush. + in_crush_tac (intuition (auto with datatypes)). unfold add_ghost_msg in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. * left. apply in_app_iff. left. apply in_app_iff. right. @@ -161,8 +161,7 @@ Section RaftMsgRefinement. simpl in *. rewrite map_map. apply in_map_iff. - eexists; intuition; eauto. - + eexists; intuition; eauto. + unfold mgv_refined_input_handlers in *. simpl in *. unfold refined_input_handlers in *. simpl in *. unfold RaftInputHandler in *. @@ -179,7 +178,7 @@ Section RaftMsgRefinement. (post_ghost_state, r0) l4); nwState := update name_eq_dec (nwState net) h (post_ghost_state, r0) |}) - by (subst; eapply MRRIR_handleInput; eauto; in_crush). + by (subst; eapply MRRIR_handleInput; eauto; in_crush_tac (intuition auto)). assert (msg_refined_raft_intermediate_reachable {| @@ -194,7 +193,7 @@ Section RaftMsgRefinement. nwState := update name_eq_dec (nwState net) h (post_ghost_state, r1) |}) by (eapply MRRIR_doLeader; eauto; - try solve [in_crush]; + try solve [in_crush_tac (intuition (auto with datatypes))]; simpl in *; intros; repeat break_if; try congruence; auto). subst. eapply_prop msg_refined_raft_net_invariant_do_generic_server. eauto. @@ -222,7 +221,7 @@ Section RaftMsgRefinement. simpl in *. intros. repeat break_if; auto. intros. simpl in *. - in_crush. + in_crush_tac (intuition (auto with datatypes)). unfold add_ghost_msg in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. * left. apply in_app_iff. left. apply in_app_iff. right. @@ -369,7 +368,7 @@ Section RaftMsgRefinement. (post_ghost_state, r0) l4); nwState := update name_eq_dec (nwState net) (pDst p) (post_ghost_state, r0) |}) as Hr0 - by (subst; eapply MRRIR_handleMessage; eauto; in_crush). + by (subst; eapply MRRIR_handleMessage; eauto; in_crush_tac (intuition auto)). assert (msg_refined_raft_intermediate_reachable {| @@ -384,7 +383,7 @@ Section RaftMsgRefinement. nwState := update name_eq_dec (nwState net) (pDst p) (post_ghost_state, r1) |}) as Hr1 by (eapply MRRIR_doLeader; eauto; - try solve [in_crush]; + try solve [in_crush_tac (intuition (auto with datatypes))]; simpl in *; intros; repeat break_if; try congruence; auto). subst. eapply_prop msg_refined_raft_net_invariant_do_generic_server'. eauto. @@ -394,13 +393,13 @@ Section RaftMsgRefinement. exact Hr1. simpl. break_if; intuition eauto. simpl. intros. break_if; intuition eauto. - simpl. in_crush. auto. auto. + simpl. in_crush_tac (intuition (auto with datatypes)). auto. auto. simpl. break_if; eauto; congruence. simpl. intros. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. in_crush. + simpl. in_crush_tac (intuition (auto with datatypes)). (* here *) unfold add_ghost_msg in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. @@ -458,7 +457,7 @@ Section RaftMsgRefinement. (post_ghost_state, r0) l4); nwState := update name_eq_dec (nwState net) h (post_ghost_state, r0) |}) as Hr0 - by (subst; eapply MRRIR_handleInput; eauto; in_crush). + by (subst; eapply MRRIR_handleInput; eauto; in_crush_tac (intuition auto)). assert (msg_refined_raft_intermediate_reachable {| @@ -473,7 +472,7 @@ Section RaftMsgRefinement. nwState := update name_eq_dec (nwState net) h (post_ghost_state, r1) |}) as Hr1 by (eapply MRRIR_doLeader; eauto; - try solve [in_crush]; + try solve [in_crush_tac (intuition (auto with datatypes))]; simpl in *; intros; repeat break_if; try congruence; auto). subst. eapply_prop msg_refined_raft_net_invariant_do_generic_server'. eauto. @@ -483,13 +482,13 @@ Section RaftMsgRefinement. exact Hr1. simpl. break_if; intuition eauto. simpl. intros. break_if; intuition eauto. - simpl. in_crush. auto. auto. + simpl. in_crush_tac (intuition (auto with datatypes)). auto. auto. simpl. break_if; eauto; congruence. simpl. intros. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. in_crush. + simpl. in_crush_tac (intuition (auto with datatypes)). unfold add_ghost_msg in *. do_in_map. subst. do_in_app. intuition; try do_in_app; intuition. * left. apply in_app_iff. right. apply in_app_iff. left. @@ -722,7 +721,7 @@ Section RaftMsgRefinement. |})) by (unfold mgv_deghost in *; repeat break_match; simpl in *; eapply MRRIR_handleInput; repeat break_match; simpl in *; eauto; - simpl in *; in_crush). + simpl in *; in_crush_tac (intuition auto)). pose proof map_subset _ _ mgv_deghost_packet (nwPackets x ++ @send_packets _ raft_msg_refined_multi_params h @@ -771,7 +770,7 @@ Section RaftMsgRefinement. { unfold mgv_deghost in *; repeat break_match; simpl in *. eapply MRRIR_handleMessage. eauto. simpl. eauto. simpl. eauto. simpl. eauto. simpl. auto. - simpl in *; in_crush. + simpl in *; in_crush_tac (intuition auto). } pose proof map_subset _ _ mgv_deghost_packet ((xs' ++ ys') ++ @@ -791,13 +790,13 @@ Section RaftMsgRefinement. rewrite map_app. in_crush. - left. apply in_map_iff. - eexists; intuition; eauto. + eexists; intuition (auto with datatypes); eauto. - left. apply in_map_iff. - eexists; intuition; eauto. + eexists; intuition (auto with datatypes); eauto. - right. unfold add_ghost_msg. repeat rewrite map_map. simpl in *. - in_crush. + in_crush_tac (intuition auto). } concludes. break_exists_name dps'. @@ -819,7 +818,7 @@ Section RaftMsgRefinement. |})). { unfold mgv_deghost in *; repeat break_match; simpl in *. eapply MRRIR_doLeader; repeat break_match; simpl in *; eauto; - simpl in *; in_crush. + simpl in *; in_crush_tac (intuition auto). } pose proof map_subset _ _ mgv_deghost_packet (nwPackets x ++ @@ -860,7 +859,7 @@ Section RaftMsgRefinement. |})). { unfold mgv_deghost in *; repeat break_match; simpl in *. eapply MRRIR_doGenericServer; repeat break_match; simpl in *; eauto; - simpl in *; in_crush. + simpl in *; in_crush_tac (intuition auto). } pose proof map_subset _ _ mgv_deghost_packet (nwPackets x ++ diff --git a/theories/RaftProofs/RaftRefinementProof.v b/theories/RaftProofs/RaftRefinementProof.v index 62d1b7b..3ab3e45 100644 --- a/theories/RaftProofs/RaftRefinementProof.v +++ b/theories/RaftProofs/RaftRefinementProof.v @@ -86,7 +86,7 @@ Section RaftRefinementProof. (pSrc p) (pBody p) (nwState net (pDst p)), r0) |}) - by (eapply RRIR_handleMessage; eauto; in_crush). + by (eapply RRIR_handleMessage; eauto; in_crush_tac (intuition auto)). assert (refined_raft_intermediate_reachable {| @@ -108,7 +108,7 @@ Section RaftRefinementProof. (pSrc p) (pBody p) (nwState net (pDst p)), r1) |}) by (eapply RRIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| in_crush_tac (intuition auto)]). eapply_prop refined_raft_net_invariant_do_generic_server. eauto. eapply_prop refined_raft_net_invariant_do_leader. eauto. eapply refined_raft_invariant_handle_message with (P := P); eauto using in_app_or. @@ -121,7 +121,7 @@ Section RaftRefinementProof. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. in_crush. + simpl. in_crush_tac (intuition (auto with datatypes)). + unfold refined_input_handlers in *. simpl in *. unfold RaftInputHandler, update_elections_data_input in *. repeat break_let. repeat find_inversion. @@ -133,7 +133,7 @@ Section RaftRefinementProof. (update_elections_data_input h inp (nwState net h), r0) |}) - by (eapply RRIR_handleInput; eauto; in_crush). + by (eapply RRIR_handleInput; eauto; in_crush_tac (intuition auto)). assert (refined_raft_intermediate_reachable {| @@ -153,7 +153,7 @@ Section RaftRefinementProof. (update_elections_data_input h inp (nwState net h), r1) |}) by (eapply RRIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| in_crush_tac (intuition auto)]). eapply_prop refined_raft_net_invariant_do_generic_server. eauto. eapply_prop refined_raft_net_invariant_do_leader. eauto. eapply refined_raft_invariant_handle_input with (P := P); eauto using in_app_or. @@ -167,11 +167,12 @@ Section RaftRefinementProof. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. unfold send_packets. intros. in_crush. + simpl. unfold send_packets. intros. in_crush_tac (intuition (auto with datatypes)). + match goal with | [ H : nwPackets ?net = _ |- _ {| nwPackets := ?ps ; nwState := ?st |} ] => assert (forall p, In p (nwPackets {| nwPackets := ps ; nwState := st |}) -> - In p (nwPackets net)) by (intros; simpl in *; find_rewrite; in_crush) + In p (nwPackets net)) by + (intros; simpl in *; find_rewrite; in_crush_tac (intuition auto)) end. eapply_prop refined_raft_net_invariant_state_same_packet_subset; [|eauto|idtac|]; eauto. @@ -285,7 +286,7 @@ Section RaftRefinementProof. (pSrc p) (pBody p) (nwState net (pDst p)), r0) |}) - by (eapply RRIR_handleMessage; eauto; in_crush). + by (eapply RRIR_handleMessage; eauto; in_crush_tac (intuition auto)). assert (refined_raft_intermediate_reachable {| @@ -306,7 +307,7 @@ Section RaftRefinementProof. (pSrc p) (pBody p) (nwState net (pDst p)), r1) |}) by (eapply RRIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| in_crush_tac (intuition auto)]). eapply_prop refined_raft_net_invariant_do_generic_server'. eauto. eapply_prop refined_raft_net_invariant_do_leader'. eauto. eapply refined_raft_invariant_handle_message' with (P := P); auto. @@ -320,7 +321,7 @@ Section RaftRefinementProof. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. in_crush. + simpl. in_crush_tac (intuition (auto with datatypes)). + match goal with | [ H : refined_raft_intermediate_reachable _ |- _ ?x ] => assert (refined_raft_intermediate_reachable x) as Hpost @@ -344,7 +345,7 @@ Section RaftRefinementProof. (update_elections_data_input h inp (nwState net h), r0) |}) - by (eapply RRIR_handleInput; eauto; in_crush). + by (eapply RRIR_handleInput; eauto; in_crush_tac (intuition auto)). assert (refined_raft_intermediate_reachable {| @@ -364,7 +365,7 @@ Section RaftRefinementProof. (update_elections_data_input h inp (nwState net h), r1) |}) by (eapply RRIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| in_crush_tac (intuition auto)]). eapply_prop refined_raft_net_invariant_do_generic_server'. eauto. eapply_prop refined_raft_net_invariant_do_leader'. eauto. eapply refined_raft_invariant_handle_input' with (P := P); auto. @@ -378,7 +379,8 @@ Section RaftRefinementProof. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. unfold send_packets. intros. in_crush. + simpl. unfold send_packets. intros. + in_crush_tac (intuition (auto with datatypes)). + match goal with | [ H : nwPackets ?net = _ |- _ {| nwPackets := ?ps ; nwState := ?st |} ] => assert (forall p, In p (nwPackets {| nwPackets := ps ; nwState := st |}) -> diff --git a/theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v b/theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v index 9119d27..f322037 100644 --- a/theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v +++ b/theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v @@ -77,8 +77,9 @@ Section RequestVoteReplyMoreUpToDate. * find_apply_lem_hyp requestVote_maxIndex_maxTerm_invariant. eapply_prop_hyp requestVote_maxIndex_maxTerm pBody; eauto. concludes. intuition; subst. - eexists; intuition; eauto. - - find_copy_apply_lem_hyp handleRequestVote_log_term_type; intuition; try congruence. + eexists; intuition (auto with datatypes); eauto. + - find_copy_apply_lem_hyp handleRequestVote_log_term_type; + intuition auto; try congruence. repeat find_rewrite. find_apply_hyp_hyp. intuition. + assert (In p0 (nwPackets net)) by (repeat find_rewrite; in_crush). @@ -105,7 +106,7 @@ Section RequestVoteReplyMoreUpToDate. * find_apply_lem_hyp requestVote_maxIndex_maxTerm_invariant. eapply_prop_hyp requestVote_maxIndex_maxTerm pBody; eauto. concludes. intuition; subst. - eexists; intuition; eauto. + eexists; intuition (auto with datatypes); eauto. - find_apply_hyp_hyp. intuition. + assert (In p0 (nwPackets net)) by (repeat find_rewrite; in_crush). repeat find_rewrite. diff --git a/theories/RaftProofs/RequestVoteReplyTermSanityProof.v b/theories/RaftProofs/RequestVoteReplyTermSanityProof.v index dc688eb..3d890c5 100644 --- a/theories/RaftProofs/RequestVoteReplyTermSanityProof.v +++ b/theories/RaftProofs/RequestVoteReplyTermSanityProof.v @@ -62,7 +62,7 @@ Section RequestVoteReplyTermSanity. + remember (pDst p0). subst p0. simpl in *. subst. find_copy_apply_lem_hyp handleRequestVote_reply_true'. - intuition. + intuition lia. - find_apply_hyp_hyp. intuition. + assert (In p0 (nwPackets net)) by (repeat find_rewrite; in_crush). find_copy_apply_lem_hyp handleRequestVote_currentTerm_leaderId. diff --git a/theories/RaftProofs/RequestVoteTermSanityProof.v b/theories/RaftProofs/RequestVoteTermSanityProof.v index cc095f3..44e9c1e 100644 --- a/theories/RaftProofs/RequestVoteTermSanityProof.v +++ b/theories/RaftProofs/RequestVoteTermSanityProof.v @@ -82,7 +82,7 @@ Section RequestVoteTermSanity. + find_apply_lem_hyp handleTimeout_log_term_type. intuition; repeat find_rewrite; eauto. + do_in_map. remember (pSrc p). subst p. simpl in *. - find_eapply_lem_hyp handleTimeout_messages; eauto; intuition. + find_eapply_lem_hyp handleTimeout_messages; eauto; intuition lia. - find_apply_hyp_hyp. intuition. + find_apply_lem_hyp handleTimeout_log_term_type. intuition; repeat find_rewrite; eauto. diff --git a/theories/RaftProofs/SortedProof.v b/theories/RaftProofs/SortedProof.v index 1b1e5c8..f2f34bd 100644 --- a/theories/RaftProofs/SortedProof.v +++ b/theories/RaftProofs/SortedProof.v @@ -269,7 +269,7 @@ Section SortedProof. Proof using. induction l; intros; simpl in *; intuition. - subst_max. intuition. - - subst. find_apply_hyp_hyp. intuition. + - subst. find_apply_hyp_hyp. intuition lia. - subst. find_apply_hyp_hyp. intuition. Qed. @@ -363,13 +363,13 @@ Section SortedProof. repeat find_higher_order_rewrite. break_match; try find_rewrite; eauto. - find_apply_lem_hyp handleAppendEntriesReply_packets. subst. simpl in *. eapply logs_sorted_nw_packets_unchanged; eauto. - intros. find_apply_hyp_hyp. find_rewrite. in_crush. + intros. find_apply_hyp_hyp. find_rewrite. in_crush_tac (intuition (auto with datatypes)). - find_apply_lem_hyp handleAppendEntriesReply_packets. subst. simpl in *. eapply packets_gt_prevIndex_packets_unchanged; eauto. - intros. find_apply_hyp_hyp. find_rewrite. in_crush. + intros. find_apply_hyp_hyp. find_rewrite. in_crush_tac (intuition (auto with datatypes)). - find_apply_lem_hyp handleAppendEntriesReply_packets. subst. simpl in *. eapply packets_ge_prevTerm_packets_unchanged; eauto. - intros. find_apply_hyp_hyp. find_rewrite. in_crush. + intros. find_apply_hyp_hyp. find_rewrite. in_crush_tac (intuition (auto with datatypes)). Qed. Lemma handleRequestVote_packets : @@ -379,7 +379,7 @@ Section SortedProof. Proof using. intros. unfold handleRequestVote, advanceCurrentTerm in *. repeat break_match; find_inversion; - subst; intuition; break_exists; congruence. + subst; intuition auto; break_exists; congruence. Qed. Theorem logs_sorted_request_vote : @@ -392,15 +392,18 @@ Section SortedProof. repeat find_higher_order_rewrite. break_match; try find_rewrite; eauto. - find_apply_lem_hyp handleRequestVote_packets. subst. simpl in *. eapply logs_sorted_nw_not_append_entries; eauto. - + intros. find_apply_hyp_hyp. find_rewrite. in_crush. + + intros. find_apply_hyp_hyp. find_rewrite. + in_crush_tac (intuition (auto with datatypes)). + simpl. auto. - find_apply_lem_hyp handleRequestVote_packets. subst. simpl in *. eapply packets_gt_prevIndex_not_append_entries; eauto. - + intros. find_apply_hyp_hyp. find_rewrite. in_crush. + + intros. find_apply_hyp_hyp. find_rewrite. + in_crush_tac (intuition (auto with datatypes)). + simpl. auto. - find_apply_lem_hyp handleRequestVote_packets. subst. simpl in *. eapply packets_ge_prevTerm_not_append_entries; eauto. - + intros. find_apply_hyp_hyp. find_rewrite. in_crush. + + intros. find_apply_hyp_hyp. find_rewrite. + in_crush_tac (intuition (auto with datatypes)). + simpl. auto. Qed. @@ -454,7 +457,7 @@ Section SortedProof. subst. simpl in *. find_inversion. find_apply_lem_hyp findGtIndex_necessary; intuition. - unfold replicaMessage in *. do_in_map. simpl in *. - subst. simpl in *. find_inversion. break_match; intuition. + subst. simpl in *. find_inversion. break_match; intuition (auto with arith). find_apply_lem_hyp findGtIndex_necessary; intuition. find_apply_lem_hyp findAtIndex_elim. simpl in *. intuition. repeat find_rewrite. diff --git a/theories/RaftProofs/StateMachineCorrectProof.v b/theories/RaftProofs/StateMachineCorrectProof.v index b7042c3..616383c 100644 --- a/theories/RaftProofs/StateMachineCorrectProof.v +++ b/theories/RaftProofs/StateMachineCorrectProof.v @@ -271,7 +271,7 @@ Section StateMachineCorrect. filter (fun x => eIndex x <=? i) (findGtIndex l i') ++ removeAfterIndex l i'. Proof using. intros. induction l; simpl in *; auto. - repeat (break_match; simpl in *); do_bool; intuition; try lia; try congruence. + repeat (break_match; simpl in *); do_bool; intuition (auto with arith); try lia; try congruence. f_equal. repeat find_reverse_rewrite. rewrite removeAfterIndex_eq; auto. intros. find_apply_hyp_hyp. lia. @@ -416,7 +416,7 @@ Section StateMachineCorrect. intros. pose proof max_id_for_client_default_or_entry c l x. pose proof max_id_for_client_default_or_entry c l' x. - intuition; break_exists; intuition; repeat find_rewrite. + intuition (try lia); break_exists; intuition; repeat find_rewrite. - eapply Nat.le_trans; [|eapply Nat.eq_le_incl]. apply max_id_for_client_default_ge_default. eauto. @@ -622,7 +622,7 @@ Section StateMachineCorrect. * repeat find_rewrite. unfold assoc_default in *. find_rewrite. specialize (IHl (assoc_set clientId_eq_dec ks (eClient a) (eId a)) (eId a)). conclude_using ltac:(now rewrite get_set_same). - break_exists_exists. intuition. + break_exists_exists. intuition lia. * rewrite log_to_ks'_assoc_set_diff by auto. auto. + auto. @@ -701,7 +701,7 @@ Section StateMachineCorrect. unfold log_matching, log_matching_hosts in *. intuition. copy_eapply_prop_hyp In In. copy_eapply_prop_hyp pBody pBody; eauto. - intuition. + intuition (auto with datatypes). + apply in_app_iff. right. apply removeAfterIndex_le_In; eauto; lia. + apply in_app_iff. right. diff --git a/theories/RaftProofs/StateMachineSafetyPrimeProof.v b/theories/RaftProofs/StateMachineSafetyPrimeProof.v index fff41b6..302407f 100644 --- a/theories/RaftProofs/StateMachineSafetyPrimeProof.v +++ b/theories/RaftProofs/StateMachineSafetyPrimeProof.v @@ -233,9 +233,10 @@ Section StateMachineSafety'. Prefix l l' -> In x l -> In x l'. - Proof using. + Proof using. induction l; intros; simpl in *; intuition; - subst; break_match; intuition; subst; intuition. + subst; break_match; intuition auto; subst; + intuition (auto with datatypes). Qed. Ltac get_invariant i := @@ -261,7 +262,7 @@ Section StateMachineSafety'. unfold state_machine_safety_nw'. intros. unfold committed in *. break_exists; intuition. - destruct (lt_eq_lt_dec (eTerm x0) t); intuition. + destruct (lt_eq_lt_dec (eTerm x0) t); intuition (try lia). - find_copy_apply_lem_hyp append_entries_leaderLogs_invariant. copy_eapply_prop_hyp append_entries_leaderLogs AppendEntries; eauto. break_exists; break_and. @@ -474,7 +475,7 @@ Section StateMachineSafety'. | H : forall _ _, In _ _ -> _ |- _ => eapply H end; eauto). assert (0 < eIndex e) by lia. - do_in_app. intuition. + do_in_app. intuition (auto with datatypes). destruct (le_gt_dec (eIndex e) (maxIndex (new_msg_entries ++ old_msg_entries))); intuition. right. right. right. match goal with @@ -507,7 +508,7 @@ Section StateMachineSafety'. Qed. Instance sms'i : state_machine_safety'interface. - Proof. + Proof using aelli aerlli lci llci llli lllmi llsi lmi lsi ollpti rlmli rri uii. split. intuition. split. diff --git a/theories/RaftProofs/StateMachineSafetyProof.v b/theories/RaftProofs/StateMachineSafetyProof.v index fe763b5..90dc001 100644 --- a/theories/RaftProofs/StateMachineSafetyProof.v +++ b/theories/RaftProofs/StateMachineSafetyProof.v @@ -121,7 +121,7 @@ Section StateMachineSafetyProof. - simpl in *. break_and. destruct (log st); simpl in *. + lia. - + find_insterU. conclude_using eauto. intuition. + + find_insterU. conclude_using eauto. intuition lia. Qed. Lemma lifted_sorted_host : @@ -236,8 +236,9 @@ Section StateMachineSafetyProof. maxIndex l2 <= maxIndex (l1 ++ l2). Proof using. induction l1; intros; simpl in *; intuition. - destruct l2; intuition. simpl in *. - specialize (H0 e). conclude H0 intuition. intuition. + destruct l2; intuition (auto with arith). simpl in *. + specialize (H0 e). conclude H0 ltac:(intuition (auto with datatypes)). + intuition (auto with arith). Qed. Lemma max_min_thing: @@ -246,7 +247,7 @@ Section StateMachineSafetyProof. max a (min b c) <= c. Proof using. intros. - destruct (max a (min b c)) using (Nat.max_case _ _); intuition. + destruct (max a (min b c)) using (Nat.max_case _ _); intuition lia. Qed. Lemma in_ghost_packet : @@ -506,7 +507,7 @@ Section StateMachineSafetyProof. destruct (le_lt_dec (lastApplied (snd (nwState net (pDst p)))) (maxIndex (log d))); auto. exfalso. - assert (In p (nwPackets net)) by (find_rewrite; intuition). + assert (In p (nwPackets net)) by (find_rewrite; intuition (auto with datatypes)). assert (exists x, eIndex x = maxIndex (log d) /\ In x (log (snd (nwState net (pDst p))))). { eapply contiguous_range_exact_lo_elim_exists. @@ -526,13 +527,13 @@ Section StateMachineSafetyProof. destruct (le_lt_dec (lastApplied (snd (nwState net (pDst p)))) (maxIndex (log d))); auto. exfalso. - assert (In p (nwPackets net)) by (find_rewrite; intuition). + assert (In p (nwPackets net)) by (find_rewrite; intuition (auto with datatypes)). break_exists; intuition. find_apply_lem_hyp findAtIndex_elim; intuition. find_eapply_lem_hyp msg_lifted_sms_nw; eauto; [|eapply msg_commit_recorded_lift_intro; eauto; left; repeat find_rewrite; auto using Nat.lt_le_incl]. - intuition. + intuition (try lia). * subst. assert (0 < eIndex x) by (eapply lifted_entries_contiguous_invariant; eauto). lia. @@ -544,12 +545,11 @@ Section StateMachineSafetyProof. break_exists; break_and; erewrite maxIndex_removeAfterIndex by (eauto; apply msg_lifted_sorted_host; auto); auto|]; [idtac]. - destruct (le_lt_dec (lastApplied (snd (nwState net (pDst p)))) (maxIndex es)); intuition; [match goal with | |- context [ maxIndex (?ll1 ++ ?ll2) ] => pose proof maxIndex_app ll1 ll2 - end; simpl in *; intuition|]; [idtac]. + end; simpl in *; intuition lia|]; [idtac]. assert (exists x, eIndex x = maxIndex es /\ In x (log (snd (nwState net (pDst p))))). { eapply contiguous_range_exact_lo_elim_exists. @@ -575,29 +575,26 @@ Section StateMachineSafetyProof. end; eauto. * congruence. * apply msg_lifted_sorted_host. auto. - + destruct (le_lt_dec (lastApplied (snd (nwState net (pDst p)))) (maxIndex es)); intuition; + + destruct (le_lt_dec (lastApplied (snd (nwState net (pDst p)))) (maxIndex es)); intuition; [match goal with | |- context [ maxIndex (?ll1 ++ ?ll2) ] => pose proof maxIndex_app ll1 ll2 - end; simpl in *; intuition|]; [idtac]. + end; simpl in *; (intuition lia)|]; [idtac]. exfalso. - assert (In p (nwPackets net)) by (find_rewrite; intuition). + assert (In p (nwPackets net)) by (find_rewrite; intuition (auto with datatypes)). break_exists; intuition. find_apply_lem_hyp findAtIndex_elim; intuition. find_copy_apply_lem_hyp maxIndex_non_empty. break_exists. intuition. - find_eapply_lem_hyp msg_lifted_sms_nw; eauto; [|eapply msg_commit_recorded_lift_intro; eauto; left; repeat find_rewrite; auto using Nat.lt_le_incl]. - match goal with | _ : In ?x es, _ : maxIndex es = eIndex ?x |- _ => assert (pli < eIndex x) by ( eapply contiguous_range_exact_lo_elim_lt; eauto; eapply lifted_entries_contiguous_nw_invariant; eauto) end. - intuition. - + intuition (try lia). match goal with | H : _ = _ ++ _ |- _ => symmetry in H end. @@ -608,7 +605,7 @@ Section StateMachineSafetyProof. match goal with | _ : eIndex ?x' = eIndex ?x, H : context [eIndex ?x'] |- _ => specialize (H x); conclude H ltac:(apply in_app_iff; auto) - end; intuition. + end; intuition lia. - assert (sorted (log d)) by (eauto using lifted_handleAppendEntries_logs_sorted). match goal with | _ : handleAppendEntries ?h ?s ?t ?n ?pli ?plt ?es ?ci = (?s', ?m) |- _ => @@ -624,7 +621,7 @@ Section StateMachineSafetyProof. destruct (le_lt_dec (commitIndex (snd (nwState net (pDst p)))) (maxIndex (log d))); auto. exfalso. - assert (In p (nwPackets net)) by (find_rewrite; intuition). + assert (In p (nwPackets net)) by (find_rewrite; intuition (auto with datatypes)). assert (exists x, eIndex x = maxIndex (log d) /\ In x (log (snd (nwState net (pDst p))))). { eapply contiguous_range_exact_lo_elim_exists. @@ -644,13 +641,12 @@ Section StateMachineSafetyProof. destruct (le_lt_dec (commitIndex (snd (nwState net (pDst p)))) (maxIndex (log d))); auto. exfalso. - assert (In p (nwPackets net)) by (find_rewrite; intuition). + assert (In p (nwPackets net)) by (find_rewrite; intuition (auto with datatypes)). break_exists; intuition. find_apply_lem_hyp findAtIndex_elim; intuition. - find_eapply_lem_hyp msg_lifted_sms_nw; eauto; [|eapply msg_commit_recorded_lift_intro; eauto; - right; repeat find_rewrite; intuition]. - intuition. + right; repeat find_rewrite; intuition lia]. + intuition (try lia). * subst. assert (0 < eIndex x) by (eapply lifted_entries_contiguous_invariant; eauto). lia. @@ -665,7 +661,7 @@ Section StateMachineSafetyProof. [match goal with | |- context [ maxIndex (?ll1 ++ ?ll2) ] => pose proof maxIndex_app ll1 ll2 - end; simpl in *; intuition|]; [idtac]. + end; simpl in *; intuition lia|]; [idtac]. assert (exists x, eIndex x = maxIndex es /\ In x (log (snd (nwState net (pDst p))))). { eapply contiguous_range_exact_lo_elim_exists. @@ -695,24 +691,22 @@ Section StateMachineSafetyProof. [match goal with | |- context [ maxIndex (?ll1 ++ ?ll2) ] => pose proof maxIndex_app ll1 ll2 - end; simpl in *; intuition|]; [idtac]. + end; simpl in *; intuition lia|]; [idtac]. exfalso. - assert (In p (nwPackets net)) by (find_rewrite; intuition). + assert (In p (nwPackets net)) by (find_rewrite; intuition (auto with datatypes)). break_exists; intuition. find_apply_lem_hyp findAtIndex_elim; intuition. find_copy_apply_lem_hyp maxIndex_non_empty. break_exists. intuition. - find_eapply_lem_hyp msg_lifted_sms_nw; eauto; [|eapply msg_commit_recorded_lift_intro; eauto; - right; repeat find_rewrite; intuition]. + right; repeat find_rewrite; intuition lia]. match goal with | _ : In ?x es, _ : maxIndex es = eIndex ?x |- _ => assert (pli < eIndex x) by (eapply contiguous_range_exact_lo_elim_lt; eauto; eapply lifted_entries_contiguous_nw_invariant; eauto) end. - - intuition. + intuition (try lia). * match goal with | H : _ = _ ++ _ |- _ => symmetry in H end. @@ -723,7 +717,7 @@ Section StateMachineSafetyProof. match goal with | _ : eIndex ?x' = eIndex ?x, H : context [eIndex ?x'] |- _ => specialize (H x); conclude H ltac:(apply in_app_iff; auto) - end; intuition. + end; intuition lia. Qed. Lemma lifted_maxIndex_sanity_append_entries_reply : @@ -1183,7 +1177,7 @@ Section StateMachineSafetyProof. | [ |- context [ allEntries ?x ] ] => destruct (allEntries x) using (update_elections_data_client_request_allEntries_ind ltac:(eauto)) - end; intuition. + end; intuition (auto with datatypes). Qed. Lemma handleClientRequest_preservers_log : @@ -1193,7 +1187,8 @@ Section StateMachineSafetyProof. In e (log st'). Proof using. intros. - destruct (log st') using (handleClientRequest_log_ind ltac:(eauto)); intuition. + destruct (log st') using (handleClientRequest_log_ind ltac:(eauto)); + intuition (auto with datatypes). Qed. Lemma committed_log_allEntries_preserved : @@ -1433,16 +1428,14 @@ Section StateMachineSafetyProof. t <= t' -> lifted_committed net e t'. Proof using. - unfold lifted_committed. - intros. + unfold lifted_committed. intros. break_exists_exists. - intuition. + intuition lia. Qed. - Lemma commit_invariant_timeout : msg_refined_raft_net_invariant_timeout commit_invariant. - Proof using rmri. + Proof using rmri. unfold msg_refined_raft_net_invariant_timeout, commit_invariant. simpl. intuition. - unfold commit_invariant_host in *. @@ -1560,7 +1553,7 @@ Section StateMachineSafetyProof. unfold update_elections_data_appendEntries. intros. break_let. break_match; auto. break_if; auto. - simpl. intuition. + simpl. intuition (auto with datatypes). Qed. Lemma lifted_transitive_commit_invariant : @@ -1649,14 +1642,14 @@ Section StateMachineSafetyProof. | |- In ?e _ => assert (lifted_committed net e (currentTerm (snd (nwState net host)))) by (unfold lifted_committed; - exists host, e'; intuition; + exists host, e'; intuition (try lia); eapply lifted_no_entries_past_current_term_host_invariant; eauto) end. find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. assert (eIndex x > 0) by (eapply lifted_entries_gt_0_invariant; eauto). - intuition; lia. + intuition lia. + find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. - intuition; + (intuition (auto with datatypes)); try solve [apply in_app_iff; right; apply removeAfterIndex_le_In; auto; lia]; [idtac]. @@ -1676,7 +1669,7 @@ Section StateMachineSafetyProof. * enough (eIndex e <= maxIndex (log (snd (nwState net host)))) by lia. apply maxIndex_is_max; auto. + find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. - intuition; + (intuition (auto with datatypes)); try solve [apply in_app_iff; right; apply removeAfterIndex_le_In; auto; lia]; [idtac]. @@ -1694,7 +1687,7 @@ Section StateMachineSafetyProof. | |- In ?e _ => assert (lifted_committed net e (currentTerm (snd (nwState net host)))) by (unfold lifted_committed; - exists host, e'; intuition; + exists host, e'; intuition (try lia); eapply lifted_no_entries_past_current_term_host_invariant; eauto) end. find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. @@ -1744,14 +1737,14 @@ Section StateMachineSafetyProof. | |- In ?e _ => assert (lifted_committed net e (currentTerm (snd (nwState net host)))) by (unfold lifted_committed; - exists host, e'; intuition; + exists host, e'; intuition (try lia); eapply lifted_no_entries_past_current_term_host_invariant; eauto) end. find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. assert (eIndex x > 0) by (eapply lifted_entries_gt_0_invariant; eauto). - intuition; lia. + intuition lia. + find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. - intuition; + (intuition (auto with datatypes)); try solve [apply in_app_iff; right; apply removeAfterIndex_le_In; auto; lia]; [idtac]. @@ -1771,7 +1764,7 @@ Section StateMachineSafetyProof. * enough (eIndex e' <= maxIndex (log (snd (nwState net host)))) by lia. apply maxIndex_is_max; auto. + find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. - intuition; + (intuition (auto with datatypes)); try solve [apply in_app_iff; right; apply removeAfterIndex_le_In; auto; lia]; [idtac]. @@ -1789,7 +1782,7 @@ Section StateMachineSafetyProof. | |- In ?e _ => assert (lifted_committed net e (currentTerm (snd (nwState net host)))) by (unfold lifted_committed; - exists host, e'; intuition; + exists host, e'; intuition (try lia); eapply lifted_no_entries_past_current_term_host_invariant; eauto) end. find_copy_eapply_lem_hyp lifted_state_machine_safety_nw'_invariant; eauto. @@ -2245,7 +2238,7 @@ Section StateMachineSafetyProof. end. eapply lifted_committed_monotonic; eauto. find_apply_lem_hyp handleRequestVote_currentTerm_leaderId. - intuition. + intuition (auto with arith). unfold mgv_refined_base_params, raft_refined_base_params, refined_base_params in *. simpl in *. repeat find_rewrite. auto. @@ -2300,7 +2293,7 @@ Section StateMachineSafetyProof. | [ H : context [log] |- _ ] => erewrite handleRequestVoteReply_same_log in H end. eapply lifted_committed_monotonic; eauto. - intuition; repeat find_rewrite; auto. + intuition (auto with arith); repeat find_rewrite; auto. + rewrite_update. eapply handleRequestVoteReply_preserves_committed; eauto. simpl. subst. auto. - unfold commit_invariant_nw. simpl. @@ -2310,7 +2303,6 @@ Section StateMachineSafetyProof. simpl. subst. auto. Qed. - Lemma committed_ext' : forall ps ps' st st' t e, (forall h, st' h = st h) -> @@ -2398,7 +2390,7 @@ Section StateMachineSafetyProof. match goal with | [ H : context [fold_left Nat.max ?l ?x] |- _ ] => pose proof fold_left_maximum_cases l x - end. intuition. + end. intuition (auto with zarith). break_exists. break_and. find_apply_lem_hyp in_map_iff. break_exists_name witness. break_and. @@ -2406,7 +2398,7 @@ Section StateMachineSafetyProof. find_apply_lem_hyp findGtIndex_necessary. do_bool. break_and. do_bool. break_and. do_bool. unfold committed. - exists h, witness. intuition. + exists h, witness. intuition (try lia). eapply haveQuorum_directly_committed; eauto. Qed. @@ -2493,7 +2485,7 @@ Section StateMachineSafetyProof. intuition. subst. unfold mgv_refined_base_params, raft_refined_base_params, refined_base_params in *. simpl in *. - repeat find_rewrite. intuition. + repeat find_rewrite. intuition (auto with datatypes). Qed. Definition lifted_leaders_have_leaderLogs (net : ghost_log_network) : Prop := diff --git a/theories/RaftProofs/TermSanityProof.v b/theories/RaftProofs/TermSanityProof.v index a532b77..b09bf97 100644 --- a/theories/RaftProofs/TermSanityProof.v +++ b/theories/RaftProofs/TermSanityProof.v @@ -155,7 +155,7 @@ Section TermSanityProof. ( forall m, In m ms -> ~ is_append_entries (snd m)). Proof using. intros. unfold handleTimeout, tryToBecomeLeader in *. - repeat break_match; find_inversion; subst; intuition; + repeat break_match; find_inversion; subst; intuition (auto with arith); do_in_map; subst; simpl in *; congruence. Qed. @@ -185,9 +185,9 @@ Section TermSanityProof. Proof using. intros. unfold handleAppendEntries, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try solve [break_exists; congruence]; - in_crush; eauto using removeAfterIndex_in. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition auto; try solve [break_exists; congruence]; + in_crush_tac (intuition (auto with arith)); eauto using removeAfterIndex_in. Qed. Lemma no_entries_past_current_term_append_entries : @@ -208,7 +208,8 @@ Section TermSanityProof. eapply no_entries_past_current_term_nw_not_append_entries with (p' := {| pSrc := ps; pDst := pd; pBody := pb |}) end; eauto. - intros. find_apply_hyp_hyp. find_rewrite. in_crush. + intros. find_apply_hyp_hyp. find_rewrite. + in_crush_tac (intuition (auto with datatypes)). Qed. Lemma no_entries_past_current_term_unaffected : @@ -223,7 +224,7 @@ Section TermSanityProof. log d = log (nwState net (pDst p)) -> (forall m, In m ms -> ~ is_append_entries (snd m)) -> no_entries_past_current_term {| nwPackets := ps'; nwState := st' |}. - Proof using. + Proof using. intros. unfold no_entries_past_current_term in *. intuition. - unfold no_entries_past_current_term_host in *. intros. simpl in *. find_higher_order_rewrite. @@ -315,9 +316,9 @@ Section TermSanityProof. Proof using. intros. unfold handleAppendEntriesReply, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try solve [break_exists; congruence]; - in_crush; eauto using removeAfterIndex_in. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition auto; try solve [break_exists; congruence]; + in_crush_tac (intuition (auto with arith)); eauto using removeAfterIndex_in. Qed. Lemma no_entries_past_current_term_append_entries_reply : @@ -337,9 +338,9 @@ Section TermSanityProof. Proof using. intros. unfold handleRequestVote, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition; try solve [break_exists; congruence]; - in_crush; eauto using removeAfterIndex_in. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition auto; try solve [break_exists; congruence]; + in_crush_tac (intuition auto); eauto using removeAfterIndex_in. Qed. Lemma no_entries_past_current_term_request_vote : @@ -358,8 +359,8 @@ Section TermSanityProof. Proof using. intros. unfold handleRequestVoteReply, advanceCurrentTerm in *. - repeat break_match; try find_inversion; subst; simpl in *; intuition; - do_bool; intuition. + repeat break_match; try find_inversion; subst; simpl in *; intuition auto; + do_bool; intuition (auto with arith). Qed. Lemma no_entries_past_current_term_request_vote_reply : diff --git a/theories/RaftProofs/TermsAndIndicesFromOneLogProof.v b/theories/RaftProofs/TermsAndIndicesFromOneLogProof.v index a249ed5..a689436 100644 --- a/theories/RaftProofs/TermsAndIndicesFromOneLogProof.v +++ b/theories/RaftProofs/TermsAndIndicesFromOneLogProof.v @@ -46,7 +46,7 @@ Section TermsAndIndicesFromOneLog. + break_exists. intuition. unfold terms_and_indices_from_one_log, terms_and_indices_from_one in *. intros. repeat find_rewrite. simpl in *. break_or_hyp. - * intuition. find_apply_lem_hyp current_term_gt_zero_invariant. find_rewrite. + * intuition (try lia). find_apply_lem_hyp current_term_gt_zero_invariant. find_rewrite. eapply_prop current_term_gt_zero. congruence. * eauto. - eapply taifol_no_append_entries; pose handleClientRequest_no_append_entries; eauto. diff --git a/theories/RaftProofs/TransitiveCommitProof.v b/theories/RaftProofs/TransitiveCommitProof.v index 4eb0879..71a76ad 100644 --- a/theories/RaftProofs/TransitiveCommitProof.v +++ b/theories/RaftProofs/TransitiveCommitProof.v @@ -19,7 +19,7 @@ Section TransitiveCommit. unfold transitive_commit, committed. intros. break_exists_name h'; exists h'. break_exists_name e''; exists e''. - intuition; eauto. + intuition (try lia); eauto. eapply (entries_match_invariant net h h'); eauto. Qed. diff --git a/theories/RaftProofs/VotedForMoreUpToDateProof.v b/theories/RaftProofs/VotedForMoreUpToDateProof.v index a762731..b2ab058 100644 --- a/theories/RaftProofs/VotedForMoreUpToDateProof.v +++ b/theories/RaftProofs/VotedForMoreUpToDateProof.v @@ -67,7 +67,7 @@ Section VotedForMoreUpToDate. eapply_prop_hyp requestVote_maxIndex_maxTerm pBody. conclude_using eauto. all:eauto. intuition; subst. - eexists; intuition; eauto. + eexists; intuition (auto with datatypes); eauto. - find_eapply_lem_hyp update_elections_data_request_vote_votedFor; eauto. intuition; repeat find_rewrite. + eapply_prop_hyp RaftState.votedFor RaftState.votedFor; eauto. @@ -78,7 +78,7 @@ Section VotedForMoreUpToDate. eapply_prop_hyp requestVote_maxIndex_maxTerm pBody. conclude_using eauto. all:eauto. intuition; subst. - eexists; intuition; eauto. + eexists; intuition (auto with datatypes); eauto. Qed. Lemma votedFor_moreUpToDate_request_vote_reply : diff --git a/theories/RaftProofs/VotesLeCurrentTermProof.v b/theories/RaftProofs/VotesLeCurrentTermProof.v index 71c7896..ab2fcf1 100644 --- a/theories/RaftProofs/VotesLeCurrentTermProof.v +++ b/theories/RaftProofs/VotesLeCurrentTermProof.v @@ -65,7 +65,7 @@ Section VotesLeCurrentTerm. unfold refined_raft_net_invariant_request_vote, votes_le_currentTerm. start_proof. find_eapply_lem_hyp votes_update_elections_data_request_vote; eauto. - intuition. + intuition (try lia). find_apply_hyp_hyp. eauto using Nat.le_trans, handleRequestVote_currentTerm. Qed. diff --git a/theories/RaftProofs/VotesWithLogTermSanityProof.v b/theories/RaftProofs/VotesWithLogTermSanityProof.v index 3d4b59c..581d5af 100644 --- a/theories/RaftProofs/VotesWithLogTermSanityProof.v +++ b/theories/RaftProofs/VotesWithLogTermSanityProof.v @@ -48,7 +48,7 @@ Section VotesWithLogTermSanity. ]. Ltac solve_currentTerm lem := - find_apply_lem_hyp lem; solve [intuition]. + find_apply_lem_hyp lem; solve [intuition lia]. Lemma votesWithLog_term_sanity_invariant : forall net,