Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix deprecations of intuition auto with star #102

Merged
merged 1 commit into from
Nov 4, 2023
Merged

fix deprecations of intuition auto with star #102

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 21 additions & 16 deletions theories/Raft/DecompositionWithPostState.v
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
Loading