From 9870e3e9896b6f5cea968f3c803873060a005bf7 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 5 Nov 2023 08:49:29 +0100 Subject: [PATCH] simplify proofs using conclude and conclude_using tactics --- theories/Raft/CommonTheorems.v | 22 +++++++++---------- theories/RaftProofs/AllEntriesLogProof.v | 4 ++-- .../AppendEntriesRequestLeaderLogsProof.v | 6 ++--- .../RaftProofs/AppliedEntriesMonotonicProof.v | 4 ++-- theories/RaftProofs/InputBeforeOutputProof.v | 4 ++-- .../RaftProofs/LeaderLogsContiguousProof.v | 2 +- .../RaftProofs/LeaderLogsLogMatchingProof.v | 4 ++-- theories/RaftProofs/LogMatchingProof.v | 8 +++---- theories/RaftProofs/LogsLeaderLogsProof.v | 2 +- theories/RaftProofs/OutputCorrectProof.v | 2 +- theories/RaftProofs/OutputGreatestIdProof.v | 2 +- theories/RaftProofs/PrefixWithinTermProof.v | 12 +++++----- .../RaftProofs/StateMachineCorrectProof.v | 2 +- .../RaftProofs/StateMachineSafetyPrimeProof.v | 2 +- theories/RaftProofs/StateMachineSafetyProof.v | 10 ++++----- 15 files changed, 42 insertions(+), 44 deletions(-) diff --git a/theories/Raft/CommonTheorems.v b/theories/Raft/CommonTheorems.v index 850e6c9..6cb6c89 100644 --- a/theories/Raft/CommonTheorems.v +++ b/theories/Raft/CommonTheorems.v @@ -524,7 +524,7 @@ Section CommonTheorems. exists e, In e (findGtIndex entries x) /\ eIndex e = i. Proof using. intros entries x Hsorted; intros. specialize (H i). - conclude H ltac:(lia). + conclude H lia. break_exists. exists x0. intuition. apply findGtIndex_sufficient; auto; lia. Qed. @@ -1170,9 +1170,7 @@ Section CommonTheorems. |- _ ] => specialize (H (eIndex e3)); conclude H - ltac:(split; [eauto| - eapply Nat.le_trans; eauto; apply maxIndex_is_max; eauto]) - + (split; [eauto| eapply Nat.le_trans; eauto; apply maxIndex_is_max; eauto]) end. break_exists. intuition. match goal with @@ -1262,7 +1260,7 @@ Section CommonTheorems. specialize (H (eIndex e)) end. intuition. - conclude_using ltac:(eapply Nat.le_trans; eauto; apply maxIndex_is_max; eauto). + conclude_using (eapply Nat.le_trans; eauto; apply maxIndex_is_max; eauto). break_exists. intuition. match goal with | _: eIndex ?e1 = eIndex ?e2 |- context [ ?e2 ] => @@ -1782,13 +1780,13 @@ Section CommonTheorems. induction l1; intros; simpl in *; intuition. - subst. break_if; do_bool; try lia. eexists; repeat (simpl in *; intuition). - - specialize (H1 e); intuition. conclude H1 ltac:(apply in_app_iff; intuition). + - specialize (H1 e); intuition. conclude H1 (apply in_app_iff; intuition). break_if; do_bool; try lia. eexists; intuition; eauto. simpl in *. intuition. eapply_prop_hyp sorted sorted; eauto. break_exists; intuition. find_rewrite. eauto. Qed. - + Lemma sorted_app_in_1 : forall l1 l2 e, sorted (l1 ++ l2) -> @@ -1822,7 +1820,7 @@ Section CommonTheorems. - break_if; simpl in *; intuition. + eapply_prop_hyp sorted sorted; eauto. break_exists; intuition; find_rewrite; eauto. - + do_bool. specialize (H1 e); conclude H1 ltac:(apply in_app_iff; intuition). + + do_bool. specialize (H1 e); conclude H1 (apply in_app_iff; intuition). lia. Qed. @@ -1875,7 +1873,7 @@ Section CommonTheorems. - exfalso. destruct l'; simpl in *; [lia|]; specialize (H1 e). - conclude_using ltac:(intuition auto with datatypes); + conclude_using (intuition auto with datatypes); lia. Qed. @@ -1891,7 +1889,7 @@ Section CommonTheorems. subst. destruct l'; simpl in *; intuition. - exfalso. specialize (H0 e). intuition lia. - exfalso. specialize (H3 e0). - conclude_using ltac:(intuition auto with datatypes); + conclude_using (intuition auto with datatypes); lia. Qed. @@ -2044,7 +2042,7 @@ Section CommonTheorems. simpl in *. break_match; intuition. subst. simpl in *. unfold contiguous_range_exact_lo in *. - intuition. specialize (H0 e0). conclude_using ltac:(intuition auto with datatypes). + intuition. specialize (H0 e0). conclude_using (intuition auto with datatypes). lia. Qed. @@ -2158,7 +2156,7 @@ Section CommonTheorems. * match goal with | H : _ |- eIndex _ > eIndex ?e => specialize (H e) - end. conclude_using ltac:(intuition auto with datatypes). intuition. + end. conclude_using (intuition auto with datatypes). intuition. + find_apply_lem_hyp cons_contiguous_sorted; eauto. simpl in *. intuition. Qed. diff --git a/theories/RaftProofs/AllEntriesLogProof.v b/theories/RaftProofs/AllEntriesLogProof.v index f82fe71..a9a1791 100644 --- a/theories/RaftProofs/AllEntriesLogProof.v +++ b/theories/RaftProofs/AllEntriesLogProof.v @@ -151,7 +151,7 @@ Ltac all f ls := eIndex e' < eIndex e. Proof using. induction l1; intros; simpl in *; intuition; eauto. - subst. find_insterU. conclude_using ltac:(apply in_app_iff; intuition eauto). + subst. find_insterU. conclude_using (apply in_app_iff; intuition eauto). intuition. Qed. @@ -547,7 +547,7 @@ Ltac all f ls := match goal with | H : forall _, _ < _ <= _ -> _ |- _ => specialize (H (eIndex e)); - conclude_using ltac:(intuition; eapply Nat.le_trans; [eapply maxIndex_is_max; eauto|]; eauto) + conclude_using (intuition; eapply Nat.le_trans; [eapply maxIndex_is_max; eauto|]; eauto) end. break_exists. break_and. match goal with diff --git a/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v b/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v index d976cb5..f96f77c 100644 --- a/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v +++ b/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v @@ -418,7 +418,7 @@ Section AppendEntriesRequestLeaderLogs. induction l1; intros; simpl in *; intuition. - subst. break_if; do_bool; try lia. eexists; repeat (simpl in *; intuition). - - specialize (H1 e); intuition. conclude H1 ltac:(apply in_app_iff; intuition). + - specialize (H1 e); intuition. conclude H1 (apply in_app_iff; intuition). break_if; do_bool; try lia. eexists; intuition; eauto. simpl in *. intuition. eapply_prop_hyp sorted sorted; eauto. break_exists; intuition. @@ -458,7 +458,7 @@ Section AppendEntriesRequestLeaderLogs. - break_if; simpl in *; intuition. + eapply_prop_hyp sorted sorted; eauto. break_exists; intuition; find_rewrite; eauto. - + do_bool. specialize (H1 e); conclude H1 ltac:(apply in_app_iff; intuition). + + do_bool. specialize (H1 e); conclude H1 (apply in_app_iff; intuition). lia. Qed. @@ -529,7 +529,7 @@ Section AppendEntriesRequestLeaderLogs. match goal with | H : forall _ _, In _ _ -> _ |- _ => specialize (H h x0); - conclude H ltac:(unfold deghost in *; + conclude H (unfold deghost in *; repeat (break_match; simpl in *); repeat (simpl in *; find_rewrite); auto) diff --git a/theories/RaftProofs/AppliedEntriesMonotonicProof.v b/theories/RaftProofs/AppliedEntriesMonotonicProof.v index 8298204..7fbab37 100644 --- a/theories/RaftProofs/AppliedEntriesMonotonicProof.v +++ b/theories/RaftProofs/AppliedEntriesMonotonicProof.v @@ -42,7 +42,7 @@ Section AppliedEntriesMonotonicProof. match goal with | H : forall _ _, _ <= _ <= _ -> _ |- _ => specialize (H h i); - conclude H ltac:(intuition; find_apply_lem_hyp maxIndex_is_max; eauto; lia) + conclude H (intuition; find_apply_lem_hyp maxIndex_is_max; eauto; lia) end. break_exists_exists. intuition. apply findAtIndex_intro; eauto using sorted_uniqueIndices. Qed. @@ -368,7 +368,7 @@ Section AppliedEntriesMonotonicProof. find_apply_lem_hyp argmax_elim. intuition. match goal with | H : forall _: name, _ |- _ => - specialize (H h'); conclude H ltac:(eauto using all_fin_all) + specialize (H h'); conclude H (eauto using all_fin_all) end. rewrite_update. simpl in *. update_destruct_hyp; subst; rewrite_update; simpl in *. diff --git a/theories/RaftProofs/InputBeforeOutputProof.v b/theories/RaftProofs/InputBeforeOutputProof.v index 516f8fa..2e2e196 100644 --- a/theories/RaftProofs/InputBeforeOutputProof.v +++ b/theories/RaftProofs/InputBeforeOutputProof.v @@ -97,7 +97,7 @@ Section InputBeforeOutput. find_apply_lem_hyp argmax_elim. intuition. match goal with | H : forall _: name, _ |- _ => - specialize (H h'); conclude H ltac:(eauto using all_fin_all) + specialize (H h'); conclude H (eauto using all_fin_all) end. rewrite_update. simpl in *. update_destruct; subst; rewrite_update; simpl in *. @@ -153,7 +153,7 @@ Section InputBeforeOutput. match goal with | H : forall _ _, _ <= _ <= _ -> _ |- _ => specialize (H h i); - conclude H ltac:(intuition; find_apply_lem_hyp maxIndex_is_max; eauto; lia) + conclude H (intuition; find_apply_lem_hyp maxIndex_is_max; eauto; lia) end. break_exists_exists. intuition. apply findAtIndex_intro; eauto using sorted_uniqueIndices. Qed. diff --git a/theories/RaftProofs/LeaderLogsContiguousProof.v b/theories/RaftProofs/LeaderLogsContiguousProof.v index 1fc20c7..7218c12 100644 --- a/theories/RaftProofs/LeaderLogsContiguousProof.v +++ b/theories/RaftProofs/LeaderLogsContiguousProof.v @@ -109,7 +109,7 @@ Section LeaderLogsContiguous. match goal with | H : forall _ _, _ <= _ <= _ -> _ |- _ => specialize (H h i); - conclude H ltac:(simpl; repeat break_match; simpl in *; repeat find_rewrite; simpl in *;lia) + conclude H (simpl; repeat break_match; simpl in *; repeat find_rewrite; simpl in *;lia) end. break_exists_exists; intuition. simpl in *. diff --git a/theories/RaftProofs/LeaderLogsLogMatchingProof.v b/theories/RaftProofs/LeaderLogsLogMatchingProof.v index 993fcb8..6bd7e0c 100644 --- a/theories/RaftProofs/LeaderLogsLogMatchingProof.v +++ b/theories/RaftProofs/LeaderLogsLogMatchingProof.v @@ -332,8 +332,8 @@ Section LeaderLogsLogMatching. match goal with | [ H : forall _ : packet , _ |- _ ] => do 7 insterU H; - conclude H ltac:(unfold deghost; simpl; eapply in_map_iff; eexists; eauto); - conclude H ltac:(simpl; eauto) + conclude H (unfold deghost; simpl; eapply in_map_iff; eexists; eauto); + conclude H (simpl; eauto) end. rename net into net0. intuition. diff --git a/theories/RaftProofs/LogMatchingProof.v b/theories/RaftProofs/LogMatchingProof.v index 03a691f..9a894ce 100644 --- a/theories/RaftProofs/LogMatchingProof.v +++ b/theories/RaftProofs/LogMatchingProof.v @@ -288,7 +288,7 @@ Section LogMatchingProof. specialize (Hentries leader h e1 e2 x) end. assert (eIndex x <= eIndex e1) by lia. - repeat conclude. intuition. + intuition. } - use_packet_subset_clear; unfold log_matching in *; intuition. + unfold log_matching_nw in *; intuition. use_nw_invariant. @@ -302,7 +302,7 @@ Section LogMatchingProof. | context [ nwState _ ?h ] => specialize (H h i) end; - conclude H ltac:(split; try lia; eapply Nat.le_trans; eauto using findGtIndex_max) + conclude H (split; try lia; eapply Nat.le_trans; eauto using findGtIndex_max) end. break_exists; eexists; @@ -333,7 +333,7 @@ Section LogMatchingProof. _ : eIndex ?e3 <= eIndex _ |- _ ] => specialize (H (eIndex e3)); - conclude H ltac:(split; auto; repeat find_rewrite; + conclude H (split; auto; repeat find_rewrite; eapply Nat.le_trans; eauto; apply maxIndex_is_max; intuition) end. break_exists. intuition. @@ -1410,7 +1410,7 @@ Ltac assert_do_leader := | [ H : forall _, prevLogIndex < _ <= _ -> _ |- _ ] => specialize (H pli); - conclude H ltac:( + conclude H ( split; intuition; eapply Nat.lt_le_incl; eapply Nat.lt_le_trans; eauto; diff --git a/theories/RaftProofs/LogsLeaderLogsProof.v b/theories/RaftProofs/LogsLeaderLogsProof.v index 5053873..386cab4 100644 --- a/theories/RaftProofs/LogsLeaderLogsProof.v +++ b/theories/RaftProofs/LogsLeaderLogsProof.v @@ -371,7 +371,7 @@ Section LogsLeaderLogs. assert (eIndex e = eIndex e') as Heq by (repeat find_rewrite; auto); assert (eIndex e'' <= eIndex e) by lia; eapply leaderLogs_entries_match_invariant in Heq; eauto; - repeat conclude Heq ltac:(eauto; intuition) + repeat conclude Heq (eauto; intuition) end; intuition. - (* old entry *) (* can use host invariant, since we don't change removeAfterIndex *) diff --git a/theories/RaftProofs/OutputCorrectProof.v b/theories/RaftProofs/OutputCorrectProof.v index 5237be9..ce0c7d3 100644 --- a/theories/RaftProofs/OutputCorrectProof.v +++ b/theories/RaftProofs/OutputCorrectProof.v @@ -754,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 ltac:(intuition (auto with arith)). + end. conclude_using (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 4128348..feb3496 100644 --- a/theories/RaftProofs/OutputGreatestIdProof.v +++ b/theories/RaftProofs/OutputGreatestIdProof.v @@ -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 ltac:(intuition (auto with arith)). + end. conclude_using (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/PrefixWithinTermProof.v b/theories/RaftProofs/PrefixWithinTermProof.v index 8c252aa..62596c8 100644 --- a/theories/RaftProofs/PrefixWithinTermProof.v +++ b/theories/RaftProofs/PrefixWithinTermProof.v @@ -43,7 +43,7 @@ Section PrefixWithinTerm. In e (log (snd (nwState net leader))). Proof using lsli rri. intros. pose proof lift_prop leader_sublog_host_invariant. - conclude_using ltac:(apply leader_sublog_invariant_invariant). + conclude_using (apply leader_sublog_invariant_invariant). find_apply_hyp_hyp. match goal with | H : leader_sublog_host_invariant _ |- _ => @@ -78,7 +78,7 @@ Section PrefixWithinTerm. Proof using lsli rri. intros. pose proof lift_prop leader_sublog_nw_invariant. - conclude_using ltac:(apply leader_sublog_invariant_invariant). + conclude_using (apply leader_sublog_invariant_invariant). find_apply_hyp_hyp. find_apply_lem_hyp exists_deghosted_packet. match goal with @@ -1077,9 +1077,9 @@ Section PrefixWithinTerm. In ?e ?es' => specialize (H p t n pli plt es ci p' t' n' pli' plt' es' ci' e e') end. - conclude_using ltac:(repeat find_rewrite; in_crush). + conclude_using (repeat find_rewrite; in_crush). concludes. - conclude_using ltac:(repeat find_rewrite; in_crush_tac (intuition auto)). + conclude_using (repeat find_rewrite; in_crush_tac (intuition auto)). repeat concludes. intuition. * exfalso. match goal with @@ -1099,9 +1099,9 @@ Section PrefixWithinTerm. In ?e (?es' ++ _) => specialize (H p t n pli plt es ci p' t' n' pli' plt' es' ci' e e') end. - conclude_using ltac:(repeat find_rewrite; in_crush). + conclude_using (repeat find_rewrite; in_crush). concludes. - conclude_using ltac:(repeat find_rewrite; in_crush_tac (intuition auto)). + conclude_using (repeat find_rewrite; in_crush_tac (intuition auto)). repeat concludes. intuition (auto with datatypes). + (* use log matching *) break_exists. intuition. diff --git a/theories/RaftProofs/StateMachineCorrectProof.v b/theories/RaftProofs/StateMachineCorrectProof.v index 616383c..0297db9 100644 --- a/theories/RaftProofs/StateMachineCorrectProof.v +++ b/theories/RaftProofs/StateMachineCorrectProof.v @@ -621,7 +621,7 @@ Section StateMachineCorrect. + destruct (clientId_eq_dec (eClient e) (eClient a)). * 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). + conclude_using (now rewrite get_set_same). break_exists_exists. intuition lia. * rewrite log_to_ks'_assoc_set_diff by auto. auto. diff --git a/theories/RaftProofs/StateMachineSafetyPrimeProof.v b/theories/RaftProofs/StateMachineSafetyPrimeProof.v index 302407f..8a7fbad 100644 --- a/theories/RaftProofs/StateMachineSafetyPrimeProof.v +++ b/theories/RaftProofs/StateMachineSafetyPrimeProof.v @@ -209,7 +209,7 @@ Section StateMachineSafety'. intuition. match goal with | H : forall _, _ <= _ -> _ |- _ => - specialize (H e'); conclude H ltac:(lia) + specialize (H e'); conclude H lia end. intuition. eapply rachet; eauto. Qed. diff --git a/theories/RaftProofs/StateMachineSafetyProof.v b/theories/RaftProofs/StateMachineSafetyProof.v index 90dc001..b8fc15a 100644 --- a/theories/RaftProofs/StateMachineSafetyProof.v +++ b/theories/RaftProofs/StateMachineSafetyProof.v @@ -237,7 +237,7 @@ Section StateMachineSafetyProof. Proof using. induction l1; intros; simpl in *; intuition. destruct l2; intuition (auto with arith). simpl in *. - specialize (H0 e). conclude H0 ltac:(intuition (auto with datatypes)). + specialize (H0 e). conclude H0 (intuition (auto with datatypes)). intuition (auto with arith). Qed. @@ -604,7 +604,7 @@ Section StateMachineSafetyProof. repeat clean; match goal with | _ : eIndex ?x' = eIndex ?x, H : context [eIndex ?x'] |- _ => - specialize (H x); conclude H ltac:(apply in_app_iff; auto) + specialize (H x); conclude H (apply in_app_iff; auto) end; intuition lia. - assert (sorted (log d)) by (eauto using lifted_handleAppendEntries_logs_sorted). match goal with @@ -716,7 +716,7 @@ Section StateMachineSafetyProof. repeat clean; match goal with | _ : eIndex ?x' = eIndex ?x, H : context [eIndex ?x'] |- _ => - specialize (H x); conclude H ltac:(apply in_app_iff; auto) + specialize (H x); conclude H (apply in_app_iff; auto) end; intuition lia. Qed. @@ -1991,7 +1991,7 @@ Section StateMachineSafetyProof. unfold log_properties_hold_on_ghost_logs in *. unfold msg_log_property in *. specialize (Hprop (fun l => forall e, In e l -> eIndex e > 0) p). - conclude_using ltac:(intros; eapply lifted_entries_gt_0_invariant; eauto). + conclude_using (intros; eapply lifted_entries_gt_0_invariant; eauto). conclude_using eauto. simpl in *. find_apply_hyp_hyp. lia. @@ -2092,7 +2092,7 @@ Section StateMachineSafetyProof. unfold log_properties_hold_on_ghost_logs in *. unfold msg_log_property in *. specialize (Hprop (fun l => contiguous_range_exact_lo l 0) p). - conclude_using ltac:(intros; eapply lifted_entries_contiguous_invariant; eauto). + conclude_using (intros; eapply lifted_entries_contiguous_invariant; eauto). concludes. simpl in *.