Skip to content

Commit

Permalink
Merge pull request #102 from uwplse/fix-intuition-deprec
Browse files Browse the repository at this point in the history
fix deprecations of intuition auto with star
  • Loading branch information
palmskog authored Nov 4, 2023
2 parents 94ff9fa + 29cefdb commit b555033
Show file tree
Hide file tree
Showing 57 changed files with 445 additions and 437 deletions.
37 changes: 21 additions & 16 deletions theories/Raft/DecompositionWithPostState.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
{|
Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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.
Expand All @@ -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
{|
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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 |} ] =>
Expand Down
8 changes: 4 additions & 4 deletions theories/Raft/Linearizability.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down
25 changes: 13 additions & 12 deletions theories/Raft/RaftLinearizableProofs.v
Original file line number Diff line number Diff line change
Expand Up @@ -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' :
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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 :
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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 :
Expand Down Expand Up @@ -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 :
Expand Down
8 changes: 4 additions & 4 deletions theories/Raft/RefinementSpecLemmas.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand All @@ -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)) ->
Expand Down Expand Up @@ -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 :
Expand Down Expand Up @@ -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.
22 changes: 11 additions & 11 deletions theories/Raft/SpecLemmas.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down Expand Up @@ -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 :
Expand Down Expand Up @@ -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' :
Expand All @@ -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 :
Expand Down Expand Up @@ -531,15 +531,15 @@ 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 :
forall st h h' t lli llt st' m,
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.
Expand All @@ -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 :
Expand Down Expand Up @@ -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 :
Expand Down Expand Up @@ -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 :
Expand Down
4 changes: 2 additions & 2 deletions theories/RaftProofs/AllEntriesLeaderSublogProof.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down
Loading

0 comments on commit b555033

Please sign in to comment.