Farewell refactorings (#384)

* Fix bullets in the proof of sum_weights_subseteq_list.

* Refactor count_predecessors_zero.

* Refactor equivocators_transition_item_project_preserves_equivocating_indices.

* Refactor the proof of generalized_equivocators_finite_valid_trace_init_to_rev.

theories/Core/Equivocators/EquivocatorsCompositionProjections.v

@@ -59,14 +59,14 @@ Definition equivocators_transition_item_project
 Lemma equivocators_transition_item_project_preserves_equivocating_indices
   (descriptors : equivocator_descriptors IM)
   (item : composite_transition_item (equivocator_IM IM))
-  oitem idescriptors
-  s
+  (oitem : option (composite_transition_item IM))
+  (idescriptors : equivocator_descriptors IM)
+  (s : composite_state (equivocator_IM IM))
   (Hdescriptors : proper_equivocator_descriptors IM descriptors (destination item))
   (Ht : composite_transition (equivocator_IM IM) (l item) (s, input item) =
-          (destination item, output item))
+    (destination item, output item))
   (Hv : composite_valid (equivocator_IM IM) (l item) (s, input item))
-  (Hpr : equivocators_transition_item_project descriptors item = Some (oitem, idescriptors))
-  :
+  (Hpr : equivocators_transition_item_project descriptors item = Some (oitem, idescriptors)) :
     set_union
       (equivocating_indices IM (enum index) s)
       (newmachine_descriptors_list IM (enum index) idescriptors)
@@ -75,43 +75,33 @@ Lemma equivocators_transition_item_project_preserves_equivocating_indices
       (equivocating_indices IM (enum index) (destination item))
       (newmachine_descriptors_list IM (enum index) descriptors).
 Proof.
-  unfold equivocators_transition_item_project
-    , composite_transition_item_projection
-    , composite_transition_item_projection_from_eq  in Hpr; simpl in Hpr.
+  unfold equivocators_transition_item_project,
+    composite_transition_item_projection,
+    composite_transition_item_projection_from_eq in Hpr; cbn in Hpr.
   unfold eq_rect_r, eq_rect in Hpr; simpl in Hpr.
-  match type of Hpr with
-    (match ?exp with _ => _ end = _)
-    => destruct exp as [(oitemx, deqv') |] eqn: Hitem_pr; [| by congruence]
-  end.
-  simpl in Ht.
-  destruct item. simpl in *. destruct l as (i, li). simpl in *.
-  match type of Ht with
-  | (let '(si', om') := ?t in _) = _ => destruct t as [si' om] eqn: Htei
-  end.
+  case_match eqn: Hitem_pr; [| by congruence].
+  destruct p as [oitemx deqv'].
+  destruct item; cbn in *; destruct l as [i li]; cbn in *.
+  move Ht at bottom; case_match.
   inversion Ht; subst; clear Ht.
   replace idescriptors with (equivocator_descriptors_update IM descriptors i deqv')
     by (destruct oitemx; congruence); clear oitem Hpr.
-  intros eqv Heqv. apply set_union_iff in Heqv. apply set_union_iff.
-  destruct (decide (eqv = i)).
-  - subst i.
-    unfold equivocating_indices in *.
-    unfold newmachine_descriptors_list in *.
-    rewrite! elem_of_list_filter in *.
+  intros eqv Heqv.
+  rewrite set_union_iff in Heqv |- *.
+  destruct (decide (eqv = i)) as [<- |].
+  - unfold equivocating_indices, newmachine_descriptors_list in *.
+    rewrite! elem_of_list_filter in Heqv |- *.
     specialize (Hdescriptors eqv).
     state_update_simpl.
-    cut (is_equivocating_state (IM eqv) si' \/  is_newmachine_descriptor (IM eqv) (descriptors eqv));
+    cut (is_equivocating_state (IM eqv) e \/  is_newmachine_descriptor (IM eqv) (descriptors eqv));
       [by itauto |].
     eapply (equivocator_transition_item_project_preserves_equivocating_indices)
       in Hitem_pr; [done.. |].
     by itauto.
-  - destruct Heqv as [Heqv | Heqv]
-    ; apply elem_of_list_filter in Heqv as [Heqv Hin].
-    + left.
-      apply elem_of_list_filter.
-      by state_update_simpl.
-    + right.
-      apply elem_of_list_filter.
-      by state_update_simpl.
+  - unfold equivocating_indices, newmachine_descriptors_list in Heqv |- *.
+    rewrite !elem_of_list_filter in Heqv |- *.
+    state_update_simpl.
+    by itauto.
 Qed.
 
 (**

theories/Core/Equivocators/SimulatingFree.v

@@ -110,53 +110,46 @@ Lemma generalized_equivocators_finite_valid_trace_init_to_rev
     finite_valid_trace_init_to CE is s tr /\
     finite_trace_last_output trX = finite_trace_last_output tr.
 Proof.
-  assert (HinclE : VLSM_incl CE (preloaded_with_all_messages_vlsm FreeE))
-    by apply constrained_preloaded_vlsm_incl_preloaded_with_all_messages.
   induction HtrX using finite_valid_trace_init_to_rev_strong_ind.
   - specialize (lift_initial_to_equivocators_state IM _ His) as Hs.
     remember (lift_to_equivocators_state IM is) as s.
-    cut (equivocators_state_project IM (zero_descriptor IM) s = is).
-    { intro Hproject.
-      exists s. split; [done |].
-      exists s. split; [done |].
-      exists []. split; [done |]. do 2 (split; [| done]).
-      constructor.
-      by apply initial_state_is_valid.
-    }
-    by apply functional_extensionality_dep_good; subst.
-  - destruct IHHtrX1 as [eqv_state_is [Hstate_start_project [eqv_state_s
-      [Hstate_final_project [eqv_state_tr [Hstate_project [Hstate_trace _]]]]]]].
-    destruct IHHtrX2 as [eqv_msg_is [Hmsg_start_project [eqv_msg_s [_
-      [eqv_msg_tr [Hmsg_project [Hmsg_trace Hfinal_msg]]]]]]].
-    exists eqv_state_is. split; [done |].
-    apply valid_trace_last_pstate in Hstate_trace as Hstate_valid.
+    assert (Hproject : equivocators_state_project IM (zero_descriptor IM) s = is)
+      by (apply functional_extensionality_dep_good; subst; done).
+    exists s; split; [done |].
+    exists s; split; [done |].
+    exists []; split; [done |].
+    do 2 (split; [| done]).
+    constructor.
+    by apply initial_state_is_valid.
+  - destruct IHHtrX1 as (eqv_state_is & Hstate_start_project & eqv_state_s
+      & Hstate_final_project & eqv_state_tr & Hstate_project & Hstate_trace & _).
+    destruct IHHtrX2 as (eqv_msg_is & Hmsg_start_project & eqv_msg_s & _
+      & eqv_msg_tr & Hmsg_project & Hmsg_trace & Hfinal_msg).
+    exists eqv_state_is; split; [done |].
     destruct Ht as [[Hs [Hiom [Hv Hc]]] Ht].
+    apply valid_trace_last_pstate in Hstate_trace as Hstate_valid.
     specialize
       (Hreplayable _ _ _ HtrX1 _ Hstate_valid Hstate_final_project _ _ _ Hmsg_trace iom)
       as Hreplay.
     spec Hreplay.
-    { clear -Heqiom Hfinal_msg.
+    {
+      clear -Heqiom Hfinal_msg.
       destruct iom as [im |]; [| done].
       unfold empty_initial_message_or_final_output in Heqiom.
-      destruct_list_last iom_tr iom_tr' item Heqiom_tr.
-      - by right.
-      - left. simpl in *. rewrite <- Hfinal_msg.
-        by rewrite finite_trace_last_output_is_last.
+      destruct_list_last iom_tr iom_tr' item Heqiom_tr; [by right | left].
+      by cbn; rewrite <- Hfinal_msg, finite_trace_last_output_is_last.
     }
-    specialize (Hreplay _ Hc)
-      as [emsg_tr [es [Hmsg_trace_full_replay [Hemsg_tr_pr [Hes_pr Hbs_iom]]]]].
+    destruct (Hreplay _ Hc)
+      as (emsg_tr & es & Hmsg_trace_full_replay & Hemsg_tr_pr & Hes_pr & Hbs_iom).
     intros .
     specialize
       (finite_valid_trace_from_to_app CE  _ _ _ _ _ (proj1 Hstate_trace) Hmsg_trace_full_replay)
       as Happ.
     specialize
       (extend_right_finite_trace_from_to CE Happ) as Happ_extend.
-    destruct l as (eqv, li).
-    pose
-      (@existT _ (fun i : index => label (equivocator_IM IM i)) eqv (ContinueWith 0 li))
-      as el.
-    destruct (transition CE el (es, iom))
-      as (es', om') eqn: Hesom'.
+    destruct l as [eqv li].
+    pose (el := @existT _ (fun i : index => label (equivocator_IM IM i)) eqv (ContinueWith 0 li)).
+    destruct (transition CE el (es, iom)) as [es' om'] eqn: Hesom'.
     specialize (Happ_extend  el iom es' om').
     apply valid_trace_get_last in Happ as Heqes.
     assert (Hes_pr_i : forall i, equivocators_total_state_project IM es i = s i)
@@ -169,54 +162,41 @@ Proof.
     cbn in Hesom', Hes_pr_eqv.
     rewrite Hes_pr_eqv in Hesom'.
     cbn in Ht.
-    destruct (transition _ _ _) as (si', _om) eqn: Hteqv.
-    inversion Ht. subst sf _om. clear Ht.
-    inversion Hesom'. subst es' om'. clear Hesom'.
-    match type of Happ_extend with
-    | ?H -> _ => cut H
+    destruct (transition _ _ _) as [si' _om] eqn: Hteqv.
+    inversion Ht; subst sf _om; clear Ht.
+    inversion Hesom'; subst es' om'; clear Hesom'.
+    spec Happ_extend.
+    {
+      apply valid_trace_last_pstate in Happ.
+      repeat split; [done | .. | done]; cycle 1.
+      - by subst el; cbn; rewrite equivocator_state_project_zero, Hes_pr_eqv.
+      - by apply Hsubsumption.
+      - destruct iom as [im |]; [| by apply option_valid_message_None].
+        destruct Hbs_iom as [Hbs_iom | Hseeded].
+        + by apply (preloaded_composite_sent_valid (equivocator_IM IM) _ _ _ Happ _ Hbs_iom).
+        + by apply initial_message_is_valid.
+    }
+    match goal with
+    |- ?H /\ _ => assert (Hproject : H)
     end.
-    { intro Hivt.
-      specialize (Happ_extend Hivt).
-      match goal with
-      |- ?H /\ _ => assert (Hproject : H)
-      end.
-      { apply functional_extensionality_dep.
-        intro i.
-        unfold equivocators_total_state_project at 1.
-        unfold equivocators_state_project.
-        by destruct (decide (i = eqv)); subst; state_update_simpl; [| apply Hes_pr_i].
-      }
-      split; [done |].
-      eexists; split; [| split; [split; [done |] |]].
-      - apply valid_trace_forget_last in Happ_extend.
-        apply (VLSM_incl_finite_valid_trace_from HinclE) in Happ_extend.
-        rewrite (equivocators_total_trace_project_app IM)
-          by (eexists; done).
-        apply valid_trace_forget_last in Happ.
-        apply (VLSM_incl_finite_valid_trace_from HinclE) in Happ.
-        rewrite (equivocators_total_trace_project_app IM)
-          by (eexists; done).
-        rewrite Hemsg_tr_pr.
-        rewrite app_nil_r.
-        rewrite Hstate_project.
-        f_equal.
-        subst el.
-        unfold equivocators_total_trace_project.
-        cbn. unfold equivocators_transition_item_project.
-        by cbn; rewrite !equivocator_state_project_zero, decide_True
-        ; cbn; repeat f_equal.
-      - by apply Hstate_trace.
-      - by rewrite! finite_trace_last_output_is_last.
+    {
+      apply functional_extensionality_dep; intro i; cbn.
+      by destruct (decide (i = eqv)); subst; state_update_simpl; [| apply Hes_pr_i].
     }
-    clear Happ_extend.
-    apply valid_trace_last_pstate in Happ.
-    repeat split; [done | .. | done].
-    + destruct iom as [im |]; [| by apply option_valid_message_None].
-      destruct Hbs_iom as [Hbs_iom | Hseeded].
-      * by apply (preloaded_composite_sent_valid (equivocator_IM IM) _ _ _ Happ _ Hbs_iom).
-      * by apply initial_message_is_valid.
-    + by subst el; cbn; rewrite equivocator_state_project_zero, Hes_pr_eqv.
-    + by apply Hsubsumption.
+    split; [done |].
+    eexists; split; [| split; [split; [done |] |]]; cycle 1.
+    + by apply Hstate_trace.
+    + by rewrite !finite_trace_last_output_is_last.
+    + apply valid_trace_forget_last in Happ_extend.
+      assert (HinclE : VLSM_incl CE (preloaded_with_all_messages_vlsm FreeE))
+        by (apply constrained_preloaded_vlsm_incl_preloaded_with_all_messages).
+      apply (VLSM_incl_finite_valid_trace_from HinclE) in Happ_extend.
+      rewrite (equivocators_total_trace_project_app IM)
+        by (eexists; done).
+      apply valid_trace_forget_last, (VLSM_incl_finite_valid_trace_from HinclE) in Happ.
+      rewrite (equivocators_total_trace_project_app IM)
+        by (eexists; done).
+      by rewrite Hemsg_tr_pr, app_nil_r, Hstate_project, <- Hproject.
 Qed.
 
 End sec_generalized_constraints.

theories/Lib/Measurable.v

@@ -100,8 +100,8 @@ Proof.
   intros v Hv.
   apply StdppListSet.set_remove_iff; [done |].
   split.
-  + by apply Hincl; right.
-  + by intros ->.
+  - by apply Hincl; right.
+  - by intros ->.
 Qed.
 
 Lemma sum_weights_subseteq

theories/Lib/TopSort.v

@@ -173,37 +173,28 @@ Qed.
   If <<precedes>> is a [StrictOrder] on <<l>>, then there must exist an
   element of <<l>> with no predecessors in <<l>>.
 *)
-Lemma count_predecessors_zero
-  (Hl : l <> [])
-  : Exists (fun a => count_predecessors a = 0) l.
+Lemma count_predecessors_zero :
+  l <> [] ->
+  Exists (fun a => count_predecessors a = 0) l.
 Proof.
   unfold count_predecessors.
-  induction l; [done |].
+  induction l; [done |]; intros _.
   inversion_clear HPl as [| ? ? HPa HPl0].
-  specialize (IHl0 HPl0).
   apply Exists_cons.
   rewrite filter_cons.
-  destruct (decide (precedes a a)); [by contradict p; apply precedes_irreflexive |].
-  assert ({ l0=[] }+{l0 <> [] }) by (destruct l0; clear; [left | right]; congruence).
-  destruct H as [? | Hl0]; [subst l0 |]; [by left |].
-  specialize (IHl0 Hl0).
-  apply Exists_exists in IHl0.
-  destruct IHl0 as [x [Hin Hlen]].
-  destruct (decide (precedes a x)).
+  rewrite decide_False; [| by apply precedes_irreflexive].
+  destruct l0 as [| h t]; [by left |].
+  apply Exists_exists in IHl0 as (x & Hin & Hlen); [| done..].
+  destruct (decide (precedes a x)); cycle 1.
+  - right.
+    apply Exists_exists; exists x.
+    by rewrite filter_cons, decide_False.
   - left.
-    specialize (Forall_forall P l0); intros [Hall _].
-    specialize (Hall HPl0 x Hin).
-    match goal with |- ?X = 0  => cut (X <= 0) end; [by lia |].
-    rewrite <- Hlen; clear Hlen.
-    apply filter_length_fn.
-    revert HPl0.
-    intro.
-    apply (Forall_impl P); [done |].
-    intros.
-    by apply precedes_transitive with a.
-  - right. apply Exists_exists. exists x.
-    rewrite filter_cons.
-    by destruct (decide (precedes a x)).
+    apply Nat.le_antisymm; [| by lia].
+    rewrite <- Hlen.
+    apply filter_length_fn, (Forall_impl P); intros; [done |].
+    apply precedes_transitive with a; only 1-2, 4-5: done.
+    by eapply Forall_forall in HPl0.
 Qed.
 
 (**