Merge pull request #103 from uwplse/update-conclude

simplify proofs using conclude and conclude_using tactics

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.

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

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)

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 *.

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.

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 *.

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.

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;

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 *)

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 *.

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 *.

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.

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.

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.

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 *.