Review PR #354

theories/Core/AnnotatedVLSM.v

@@ -254,8 +254,8 @@ Definition annotated_projection_validator_prop_alt : Prop :=
     annotated_composite_label_project annotated_composite_state_project
     annotated_composite_label_lift annotated_composite_state_lift.
 
-Lemma preloaded_annotated_composite_preloaded_projection
-  : VLSM_projection
+Lemma preloaded_annotated_composite_preloaded_projection :
+  VLSM_projection
     (pre_loaded_with_all_messages_vlsm AnnotatedFree)
     (pre_loaded_with_all_messages_vlsm (IM i))
     annotated_composite_label_project annotated_composite_state_project.
@@ -289,14 +289,14 @@ Proof.
   - by intro; intros; apply any_message_is_valid_in_preloaded.
 Qed.
 
-Lemma annotated_composite_preloaded_projection
-  : VLSM_projection AnnotatedFree (pre_loaded_with_all_messages_vlsm (IM i))
+Lemma annotated_composite_preloaded_projection :
+  VLSM_projection AnnotatedFree (pre_loaded_with_all_messages_vlsm (IM i))
     annotated_composite_label_project annotated_composite_state_project.
 Proof.
   apply @VLSM_incl_projection_trans
-    with (MY := (pre_loaded_with_all_messages_vlsm AnnotatedFree));
-    [| by apply preloaded_annotated_composite_preloaded_projection].
-  by apply (vlsm_incl_pre_loaded_with_all_messages_vlsm AnnotatedFree).
+    with (MY := (pre_loaded_with_all_messages_vlsm AnnotatedFree)).
+  - by apply (vlsm_incl_pre_loaded_with_all_messages_vlsm AnnotatedFree).
+  - by apply preloaded_annotated_composite_preloaded_projection.
 Qed.
 
 Definition annotated_composite_induced_validator : VLSM message

theories/Core/ByzantineTraces/LimitedByzantineTraces.v

@@ -389,11 +389,9 @@ Proof.
   subst non_byzantine.
   induction Hbyzantine using finite_valid_trace_rev_ind.
   - split; [| by apply empty_subseteq].
-    cut (initial_state_prop Limited bs).
-    {
-      by split; [constructor; apply initial_state_is_valid |].
-    }
-    by split; cbn; [apply lift_sub_state_initial |].
+    assert (Hisp : initial_state_prop Limited bs)
+      by (split; cbn; [apply lift_sub_state_initial |]; done).
+    by split; [constructor; apply initial_state_is_valid |].
   - subst s_reset_byzantine bs btr.
     unfold pre_VLSM_embedding_finite_trace_project; rewrite !map_app.
     rewrite @msg_dep_annotate_trace_with_equivocators_app; cbn.
@@ -402,9 +400,9 @@ Proof.
     ; destruct IHHbyzantine as [[Htr0_ann Hsi_ann] Htr0_eqv_byzantine]
     ; cbn in Htr0_eqv_byzantine |- *.
     remember (@finite_trace_last _ (annotated_type (free_composite_vlsm IM) _) _ _)
-     as lst in Htr0_eqv_byzantine at 1 |- * at 1 2 3 4 5 6.
-    assert (Hlsti : original_state lst = lift_sub_state IM (elements (list_to_set (enum index) ∖ byzantine))
-                                          (finite_trace_last si tr0)).
+      as lst in Htr0_eqv_byzantine at 1 |- * at 1 2 3 4 5 6.
+    assert (Hlsti : original_state lst = lift_sub_state IM
+      (elements (list_to_set (enum index) ∖ byzantine)) (finite_trace_last si tr0)).
     {
       subst lst; rewrite msg_dep_annotate_trace_with_equivocators_last_original_state; symmetry.
       apply (pre_VLSM_embedding_finite_trace_last _ _

theories/Core/Composition.v

@@ -657,22 +657,20 @@ Ltac state_update_simpl :=
 *)
 
 (**
-  We call a [composite_state] constrained is it is constrained for the
+  We call a [composite_state] constrained if it is constrained for the
   [free_composite_vlsm].
 *)
 Definition composite_constrained_state_prop
   {message : Type} `{EqDecision index}
   (IM : index -> VLSM message) (s : composite_state IM) : Prop :=
     constrained_state_prop (free_composite_vlsm IM) s.
 
-(**
-  If a composite state is constrained, so are all of its component states.
-*)
+(** If a composite state is constrained, so are all of its component states. *)
 Lemma composite_constrained_state_project
-  message `{EqDecision index} (IM : index -> VLSM message)
+  {message : Type} `{EqDecision index} (IM : index -> VLSM message)
   (s : composite_state IM) i :
-  composite_constrained_state_prop IM s ->
-  constrained_state_prop (IM i) (s i).
+    composite_constrained_state_prop IM s ->
+    constrained_state_prop (IM i) (s i).
 Proof.
   intros [om Hproto].
   induction Hproto; [by apply initial_state_is_valid; cbn |].

theories/Core/Equivocation/MsgDepLimitedEquivocation.v

@@ -121,7 +121,7 @@ Definition coeqv_limited_equivocation_projection_validator_prop_alt : index -> P
   HasBeenSentCapability coeqv_limited_equivocation_vlsm :=
 {
   has_been_sent :=
-    fun (sigma : state coeqv_limited_equivocation_vlsm) (m : message)=>
+    fun (sigma : state coeqv_limited_equivocation_vlsm) (m : message) =>
       composite_has_been_sent IM (original_state sigma) m
 }.
 Next Obligation.
@@ -137,20 +137,19 @@ Proof.
     with  (lY := li) in Ht as Hti; [| by apply (composite_project_label_eq IM)].
   cbn in Hti.
   apply has_been_sent_step_update with (msg := msg) in Hti.
-  destruct Ht as [_ Ht]; cbn in Ht; unfold annotated_transition in Ht.
-  cbn in Ht; destruct transition; inversion Ht; subst; cbn in *; clear Ht.
+  destruct Ht as [_ Ht]; cbn in Ht; unfold annotated_transition in Ht; cbn in Ht.
+  destruct transition; inversion Ht; subst; cbn in *; clear Ht.
   split.
   - intros [i_msg Hmsg].
     destruct (decide (i = i_msg)) as [<- | Hi_msg].
     + cbn in Hmsg; apply Hti in Hmsg as [-> | Hmsg]; [by left |].
       by right; eexists.
     + by right; state_update_simpl; eexists.
-  - cbn in *.
-    intros [-> | Hmsg]; [by eexists; apply Hti; left |].
+  - intros [-> | Hmsg]; [by eexists; apply Hti; left |].
     destruct Hmsg as [i_msg Hmsg].
-    destruct (decide (i = i_msg)) as [<- | Hi_msg];
-      [by eexists; apply Hti; right |].
-    by exists i_msg; state_update_simpl.
+    destruct (decide (i = i_msg)) as [<- | Hi_msg].
+    + by eexists; apply Hti; right.
+    + by exists i_msg; state_update_simpl.
 Qed.
 
 End sec_coequivocating_senders_limited_equivocation.
@@ -782,12 +781,11 @@ Lemma constrained_limited_to_annotated_limited_valid_state
     RelDecision (is_equivocating_tracewise_no_has_been_sent IM A sender)}
   `{!WitnessedEquivocation.WitnessedEquivocationCapability (Cv := Cv) IM threshold A sender}
   (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies) :
-  forall (s : composite_state IM),
-    valid_state_prop
-      (tracewise_limited_equivocation_vlsm_composition IM threshold A sender (Cv := Cv))
-      s ->
-    exists (sigma : state Limited),
-      valid_state_prop Limited sigma /\ original_state sigma = s.
+    forall (s : composite_state IM),
+      valid_state_prop (tracewise_limited_equivocation_vlsm_composition
+        IM threshold A sender (Cv := Cv)) s ->
+      exists (sigma : state Limited),
+        valid_state_prop Limited sigma /\ original_state sigma = s.
 Proof.
   intros s Hs.
   eapply @limited_valid_state_has_trace_exhibiting_limited_equivocation
@@ -803,11 +801,10 @@ Lemma constrained_limited_to_annotated_limited_valid_message
     RelDecision (is_equivocating_tracewise_no_has_been_sent IM A sender)}
   `{!WitnessedEquivocation.WitnessedEquivocationCapability (Cv := Cv) IM threshold A sender}
   (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies) :
-  forall (m : message),
-    valid_message_prop
-      (tracewise_limited_equivocation_vlsm_composition IM threshold A sender (Cv := Cv))
-      m ->
-    valid_message_prop Limited m.
+    forall (m : message),
+      valid_message_prop (tracewise_limited_equivocation_vlsm_composition
+        IM threshold A sender (Cv := Cv)) m ->
+      valid_message_prop Limited m.
 Proof.
   intros msg Hmsg.
   apply emitted_messages_are_valid_iff in Hmsg as [Hmsg | ([s im] & [i li] & s' & Ht)];

theories/Core/MessageDependencies.v

@@ -849,8 +849,9 @@ Proof.
     by rewrite composite_has_been_directly_observed_sent_received_iff; intros [].
   }
   destruct Hobs as [Hobs | m' [i Hobs] Hhb]; [done | exists i].
-  by eapply msg_dep_full_node_happens_before_reflects_has_been_directly_observed;
-    cycle 2; [eapply composite_constrained_state_project |..].
+  eapply msg_dep_full_node_happens_before_reflects_has_been_directly_observed;
+    [done | done | | done..].
+  by eapply composite_constrained_state_project.
 Qed.
 
 Lemma msg_dep_locally_is_globally_equivocating
@@ -1270,26 +1271,26 @@ Definition transition_preserves_global_equivocation
 
 Inductive TraceMonotonicGlobalEquivocation :
   composite_state IM -> list (composite_transition_item IM) -> Prop :=
-| tpge_initial : forall (s : composite_state IM),
-  TraceMonotonicGlobalEquivocation s []
-| tpge_step : forall (s : composite_state IM) (item : composite_transition_item IM)
-    (tr : list (composite_transition_item IM)),
-    transition_preserves_global_equivocation s item ->
-    TraceMonotonicGlobalEquivocation (destination item) tr ->
-    TraceMonotonicGlobalEquivocation s (item :: tr).
+| tpge_initial :
+    forall (s : composite_state IM), TraceMonotonicGlobalEquivocation s []
+| tpge_step :
+    forall (s : composite_state IM) (item : composite_transition_item IM)
+      (tr : list (composite_transition_item IM)),
+      transition_preserves_global_equivocation s item ->
+      TraceMonotonicGlobalEquivocation (destination item) tr ->
+      TraceMonotonicGlobalEquivocation s (item :: tr).
 
 Definition trace_monotonic_global_equivocation
   (s : composite_state IM) (tr : list (composite_transition_item IM)) : Prop :=
-  forall (pre suf : list (composite_transition_item IM))
-    (item : composite_transition_item IM),
-    tr = pre ++ [item] ++ suf ->
-    transition_preserves_global_equivocation (finite_trace_last s pre) item.
+    forall (pre suf : list (composite_transition_item IM)) (item : composite_transition_item IM),
+      tr = pre ++ [item] ++ suf ->
+      transition_preserves_global_equivocation (finite_trace_last s pre) item.
 
 Lemma trace_monotonic_global_equivocation_def_equiv :
   forall (s : composite_state IM) (tr : list (composite_transition_item IM)),
-  trace_monotonic_global_equivocation s tr
-    <->
-  TraceMonotonicGlobalEquivocation s tr.
+    trace_monotonic_global_equivocation s tr
+      <->
+    TraceMonotonicGlobalEquivocation s tr.
 Proof.
   split.
   - remember (length tr) as n; revert s tr Heqn.

theories/Core/VLSM.v

@@ -1459,8 +1459,8 @@ Proof.
     by auto using finite_valid_trace_from_to_extend.
 Qed.
 
-Lemma finite_valid_trace_from_to_snoc
-  (s f : state X) (ls : list transition_item) (item : transition_item):
+Lemma finite_valid_trace_from_to_snoc :
+  forall (s f : state X) (ls : list transition_item) (item : transition_item X),
     finite_valid_trace_from_to s f (ls ++ [item]) <->
     let m := finite_trace_last s ls in
       finite_valid_trace_from_to s m ls /\
@@ -1506,43 +1506,45 @@ Proof.
   by eauto using finite_valid_trace_from_to_last.
 Qed.
 
-Lemma finite_valid_trace_init_to_snoc
-  (si sf : state X) (tr : list transition_item) (item : transition_item):
-  finite_valid_trace_init_to si sf (tr ++ [item]) <->
-  finite_valid_trace_init_to si (finite_trace_last si tr) tr /\
-  input_valid_transition_item (finite_trace_last si tr) item /\
-  destination item = sf.
+Lemma finite_valid_trace_init_to_snoc :
+  forall (si sf : state X) (tr : list transition_item) (item : transition_item X),
+    finite_valid_trace_init_to si sf (tr ++ [item]) <->
+    finite_valid_trace_init_to si (finite_trace_last si tr) tr /\
+    input_valid_transition_item (finite_trace_last si tr) item /\
+    destination item = sf.
 Proof.
-  unfold finite_valid_trace_init_to; rewrite finite_valid_trace_from_to_snoc.
+  unfold finite_valid_trace_init_to; intros.
+  rewrite finite_valid_trace_from_to_snoc.
   by itauto.
 Qed.
 
-Lemma finite_valid_trace_init_to_snoc_rev
-  {si sf : state X} {tr : list transition_item} {item : transition_item}:
-  finite_valid_trace_init_to si sf tr ->
-  input_valid_transition_item sf item ->
-  finite_valid_trace_init_to si (destination item) (tr ++ [item]).
+Lemma finite_valid_trace_init_to_snoc_rev :
+  forall {si sf : state X} {tr : list transition_item} {item : transition_item X},
+    finite_valid_trace_init_to si sf tr ->
+    input_valid_transition_item sf item ->
+    finite_valid_trace_init_to si (destination item) (tr ++ [item]).
 Proof.
-  unfold finite_valid_trace_init_to; rewrite finite_valid_trace_from_to_snoc.
-  intros [Htr Hinit].
+  unfold finite_valid_trace_init_to.
+  intros * [Htr Hinit] Hivt.
+  rewrite finite_valid_trace_from_to_snoc.
   apply finite_valid_trace_from_to_last in Htr as Hsf; subst sf.
   by itauto.
 Qed.
 
-Lemma finite_valid_trace_init_to_prefix
-  {si sf : state X} {pre tr : list transition_item} :
-  finite_valid_trace_init_to si sf tr ->
-  pre `prefix_of` tr ->
-  finite_valid_trace_init_to si (finite_trace_last si pre) pre.
+Lemma finite_valid_trace_init_to_prefix :
+  forall {si sf : state X} {pre tr : list (transition_item X)},
+    finite_valid_trace_init_to si sf tr ->
+    pre `prefix_of` tr ->
+    finite_valid_trace_init_to si (finite_trace_last si pre) pre.
 Proof.
-  intros [] [suf ->]; split; [| done].
+  intros * [] [suf ->]; split; [| done].
   by eapply finite_valid_trace_from_to_app_split.
 Qed.
 
-Lemma finite_valid_trace_init_to_prefix_1
-  {si sf : state X} {pre suf : list transition_item} :
-  finite_valid_trace_init_to si sf (pre ++ suf) ->
-  finite_valid_trace_init_to si (finite_trace_last si pre) pre.
+Lemma finite_valid_trace_init_to_prefix_1 :
+  forall {si sf : state X} {pre suf : list (transition_item X)},
+    finite_valid_trace_init_to si sf (pre ++ suf) ->
+    finite_valid_trace_init_to si (finite_trace_last si pre) pre.
 Proof. by intros; eapply finite_valid_trace_init_to_prefix; [| eexists]. Qed.
 
 Lemma extend_right_finite_trace_from_to

theories/Examples/ELMO/ELMO.v

@@ -49,18 +49,19 @@ Proof.
   - intros v vs Hv Hvs.
     rewrite sum_weights_disj_union, Hvs by set_solver.
     replace (sum_weights (set_map _ ({[v]} ∪ _)))
-      with (sum_weights (set_map (C := listset (Message_validator idx)) (D := listset Address) proj1_sig {[v]} ∪ set_map (D := listset Address) proj1_sig vs))
+      with (sum_weights (set_map (C := listset (Message_validator idx))
+        (D := listset Address) proj1_sig {[v]} ∪ set_map (D := listset Address) proj1_sig vs))
       by (apply sum_weights_proper; rewrite set_map_union; done).
     rewrite sum_weights_disj_union; cycle 1.
     + rewrite set_map_singleton.
-      cut (` v ∉ set_map (D := listset Address) proj1_sig vs); [by set_solver |].
+      cut (`v ∉ set_map (D := listset Address) proj1_sig vs); [by set_solver |].
       contradict Hv.
       apply elem_of_map in Hv as (v' & Hv' & Hv).
       by apply dsig_eq in Hv' as ->.
     + replace (sum_weights (set_map _ {[v]}))
-        with (sum_weights (Cv := listset Address) {[` v]});
-        [by rewrite !sum_weights_singleton |].
-      by apply sum_weights_proper; rewrite set_map_singleton.
+        with (sum_weights (Cv := listset Address) {[` v]}).
+      * by rewrite !sum_weights_singleton.
+      * by apply sum_weights_proper; rewrite set_map_singleton.
 Qed.
 
 Definition immediate_dependency (m1 m2 : Message) : Prop :=
@@ -1410,9 +1411,8 @@ Definition ELMO_global_equivocation :
 Definition ELMO_not_heavy : composite_state ELMO_component -> Prop :=
   not_heavy (1 := ELMO_global_equivocation).
 
-Definition ELMO_equivocating_validators :
-  composite_state ELMO_component -> listset Address :=
-    equivocating_validators (1 := ELMO_global_equivocation).
+Definition ELMO_equivocating_validators : composite_state ELMO_component -> listset Address :=
+  equivocating_validators (1 := ELMO_global_equivocation).
 
 Lemma ELMO_equivocating_validators_are_Message_validators :
   forall (s : composite_state ELMO_component) (a : Address),

theories/Examples/ELMO/MO.v

@@ -1173,7 +1173,7 @@ Proof.
       * by apply pre_composite_free_update_state_with_initial.
     + replace us with (state_update M us i (us i)) at 2 by (state_update_simpl; done).
       apply lift_to_RMO_finite_valid_trace_from_to; [done |].
-      apply (composite_constrained_state_project _ _ us i) in Hvsp as Hvsp'.
+      apply (composite_constrained_state_project _ us i) in Hvsp as Hvsp'.
       apply valid_state_has_trace in Hvsp' as (s & tr & [Hfvt Hinit]).
       replace s with (MkState [] (idx i)) in *; cycle 1.
       * by inversion Hinit; destruct s; cbn in *; subst.

theories/Examples/ELMO/UMO.v

@@ -1679,7 +1679,7 @@ Proof.
       * by apply pre_composite_free_update_state_with_initial.
     + replace us with (state_update U us i (us i)) at 2 by (state_update_simpl; done).
       apply lift_to_RUMO_finite_valid_trace_from_to; [done |].
-      apply (composite_constrained_state_project _ _ us i) in Hvsp as Hvsp'.
+      apply (composite_constrained_state_project _ us i) in Hvsp as Hvsp'.
       apply valid_state_has_trace in Hvsp' as (s & tr & [Hfvt Hinit]).
       replace s with (MkState [] (idx i)) in *; cycle 1.
       * by inversion Hinit; destruct s; cbn in *; subst.