From 62b42c494f3403d4d7038b283e73e38fafbbe18e Mon Sep 17 00:00:00 2001 From: TeodorescuIoan Date: Mon, 3 Apr 2023 09:18:11 +0300 Subject: [PATCH 1/2] Add annotations --- searchAndDestroy.sh | 23 ++++++ theories/VLSM/Core/AnnotatedVLSM.v | 2 + theories/VLSM/Core/ByzantineTraces.v | 6 +- .../ByzantineTraces/FixedSetByzantineTraces.v | 45 ++++++------ .../ByzantineTraces/LimitedByzantineTraces.v | 17 ++--- theories/VLSM/Core/Composition.v | 34 ++++----- theories/VLSM/Core/ELMO/BaseELMO.v | 6 +- theories/VLSM/Core/ELMO/ELMO.v | 42 +++++------ theories/VLSM/Core/ELMO/UMO.v | 14 ++-- theories/VLSM/Core/Equivocation.v | 70 +++++++++---------- .../Core/Equivocation/FixedSetEquivocation.v | 60 ++++++++-------- theories/VLSM/Core/Equivocation/FullNode.v | 6 +- .../Equivocation/LimitedMessageEquivocation.v | 18 ++--- .../Equivocation/MinimalEquivocationTrace.v | 22 +++--- .../Equivocation/MsgDepFixedSetEquivocation.v | 32 +++++---- .../Equivocation/MsgDepLimitedEquivocation.v | 38 +++++----- .../VLSM/Core/Equivocation/NoEquivocation.v | 14 ++-- .../Core/Equivocation/TraceWiseEquivocation.v | 10 +-- .../Core/Equivocation/WitnessedEquivocation.v | 14 ++-- theories/VLSM/Core/EquivocationProjections.v | 36 +++++----- .../Core/Equivocators/EquivocatorReplay.v | 2 + .../VLSM/Core/Equivocators/Equivocators.v | 2 + .../Equivocators/EquivocatorsComposition.v | 4 +- .../EquivocatorsCompositionProjections.v | 10 +-- .../Equivocators/EquivocatorsProjections.v | 2 + .../Core/Equivocators/FixedEquivocation.v | 28 ++++---- .../FixedEquivocationSimulation.v | 14 ++-- .../VLSM/Core/Equivocators/FullReplayTraces.v | 16 +++-- .../LimitedEquivocationSimulation.v | 4 +- .../Equivocators/LimitedStateEquivocation.v | 10 +-- .../Core/Equivocators/MessageProperties.v | 8 ++- .../VLSM/Core/Equivocators/SimulatingFree.v | 8 ++- theories/VLSM/Core/MessageDependencies.v | 48 +++++++------ theories/VLSM/Core/Plans.v | 2 + theories/VLSM/Core/ProjectionTraces.v | 2 + theories/VLSM/Core/ReachableThreshold.v | 10 +-- theories/VLSM/Core/SubProjectionTraces.v | 27 +++---- theories/VLSM/Core/TraceableVLSM.v | 26 +++---- theories/VLSM/Core/VLSM.v | 6 +- theories/VLSM/Core/VLSMProjections.v | 2 + theories/VLSM/Core/Validator.v | 32 +++++---- theories/VLSM/Lib/Ctauto.v | 2 + theories/VLSM/Lib/EquationsExtras.v | 2 + theories/VLSM/Lib/FinExtras.v | 2 + theories/VLSM/Lib/FinFunExtras.v | 2 + theories/VLSM/Lib/FinSetExtras.v | 40 ++++++----- theories/VLSM/Lib/Itauto.v | 2 + theories/VLSM/Lib/ListExtras.v | 2 + theories/VLSM/Lib/ListFinSetExtras.v | 8 ++- theories/VLSM/Lib/ListSetExtras.v | 2 + theories/VLSM/Lib/Measurable.v | 16 +++-- theories/VLSM/Lib/NatExtras.v | 2 + theories/VLSM/Lib/NeList.v | 2 + theories/VLSM/Lib/Preamble.v | 8 ++- theories/VLSM/Lib/RealsExtras.v | 2 + theories/VLSM/Lib/SortedLists.v | 2 + theories/VLSM/Lib/StdppExtras.v | 2 + theories/VLSM/Lib/StdppListFinSet.v | 36 +++++----- theories/VLSM/Lib/StdppListSet.v | 2 + theories/VLSM/Lib/StreamExtras.v | 2 + theories/VLSM/Lib/StreamFilters.v | 4 +- theories/VLSM/Lib/Temporal.v | 2 + theories/VLSM/Lib/TopSort.v | 36 +++++----- theories/VLSM/Lib/TraceClassicalProperties.v | 1 + theories/VLSM/Lib/TraceProperties.v | 1 + theories/VLSM/Lib/Traces.v | 1 + 66 files changed, 549 insertions(+), 404 deletions(-) create mode 100755 searchAndDestroy.sh diff --git a/searchAndDestroy.sh b/searchAndDestroy.sh new file mode 100755 index 00000000..d609e7a1 --- /dev/null +++ b/searchAndDestroy.sh @@ -0,0 +1,23 @@ +for file in `find theories/VLSM/Core/ELMO/ -maxdepth 1 -name 'UMO.v'`; do + fline=`cat $file | head -n1` + if [[ $fline == 'Set Default Proof Using "Type".' ]]; then + echo $file + echo "already parsed" + else + echo $file + echo -e "Set Default Proof Using \"Type\".\n$(cat $file)" > $file + OUTPUT=`make "${file}o" 2>&1 1>/dev/null` + while [[ `echo $OUTPUT | wc -w` > 0 ]]; do + echo "try again" + ADD="Proof using "`echo -e $OUTPUT | grep -o -E "but not declared: [, _[:alnum:]]*\." | sed 's/but not declared: //'` + LINE=`echo $OUTPUT | grep "line.*characters.*" | cut -d' ' -f4 | cut -d',' -f1` + PLINE=`cat $file | head -n $LINE | grep -n "Proof\." | tail -n -1 | cut -d':' -f1` + echo $PLINE + cat $file | head -n $PLINE | tail -n -1 + sed -i "${PLINE}s/Proof\./${ADD}/" $file + cat $file | head -n $PLINE | tail -n -1 + OUTPUT=`make "${file}o" 2>&1 1>/dev/null` + done + fi +done + diff --git a/theories/VLSM/Core/AnnotatedVLSM.v b/theories/VLSM/Core/AnnotatedVLSM.v index f8d05b97..c47349e0 100644 --- a/theories/VLSM/Core/AnnotatedVLSM.v +++ b/theories/VLSM/Core/AnnotatedVLSM.v @@ -3,6 +3,8 @@ From stdpp Require Import prelude. From VLSM.Lib Require Import ListExtras. From VLSM.Core Require Import VLSM VLSMProjections Validator Composition. +Set Default Proof Using "Type". + (** * State-annotated VLSMs This module describes the VLSM obtained by augmenting the states of an existing diff --git a/theories/VLSM/Core/ByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces.v index 6943ef2e..97a3f005 100644 --- a/theories/VLSM/Core/ByzantineTraces.v +++ b/theories/VLSM/Core/ByzantineTraces.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble. From VLSM.Core Require Import VLSM VLSMProjections Composition ProjectionTraces Validator. +Set Default Proof Using "Type". + (** * VLSM Byzantine Traces In this section, we introduce two definitions of Byzantine traces, @@ -359,7 +361,7 @@ Context *) Lemma validator_pre_loaded_with_all_messages_incl : VLSM_incl PreLoadedX X. -Proof. +Proof using Hvalidator. apply VLSM_incl_finite_traces_characterization. intros. split; [| by apply H]. @@ -395,7 +397,7 @@ Lemma composite_validator_byzantine_traces_are_not_byzantine (tr : vTrace X) (Hbyz : byzantine_trace_prop X tr) : valid_trace_prop X tr. -Proof. +Proof using Hvalidator. apply validator_pre_loaded_with_all_messages_incl. apply alt_pre_loaded_with_all_messages_incl. by apply byzantine_alt_byzantine_iff in Hbyz. diff --git a/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v index e12a82ea..fd69ee02 100644 --- a/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v +++ b/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v @@ -1,3 +1,4 @@ +Set Default Proof Using "Type". From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude finite. From Coq Require Import FunctionalExtensionality. @@ -94,7 +95,7 @@ Definition fixed_byzantine_IM : index -> VLSM message := Lemma fixed_byzantine_IM_no_initial_messages : forall i m, ~ vinitial_message_prop (fixed_byzantine_IM i) m. -Proof. +Proof using no_initial_messages_in_IM. unfold fixed_byzantine_IM, update_IM. simpl. intros i m Hm. by case_decide; [| destruct (no_initial_messages_in_IM i m)]. @@ -102,7 +103,7 @@ Qed. Lemma fixed_byzantine_IM_preserves_channel_authentication : channel_authentication_prop fixed_byzantine_IM A sender. -Proof. +Proof using can_emit_signed. unfold fixed_byzantine_IM, update_IM. simpl. intros i m Hm. case_decide; [| by apply can_emit_signed]. @@ -122,7 +123,7 @@ Definition message_as_byzantine_label (i : index) (Hi : i ∈ byzantine) : composite_label fixed_byzantine_IM. -Proof. +Proof using H6 H4 H3 H2 H1 H0. exists i. unfold fixed_byzantine_IM, update_IM. simpl. @@ -272,7 +273,7 @@ Definition pre_loaded_fixed_non_byzantine_vlsm : VLSM message := Lemma non_byzantine_nodes_same : forall sub_i, sub_IM fixed_byzantine_IM (elements non_byzantine) sub_i = sub_IM IM (elements non_byzantine) sub_i. -Proof. +Proof using H6 H3 H. intro sub_i. destruct_dec_sig sub_i i Hi Heqsub_i. subst. @@ -284,7 +285,7 @@ Qed. Lemma non_byzantine_nodes_same_sym : forall sub_i, sub_IM IM (elements non_byzantine) sub_i = sub_IM fixed_byzantine_IM (elements non_byzantine) sub_i. -Proof. +Proof using H6 H3 H. by intro; symmetry; apply non_byzantine_nodes_same. Qed. @@ -331,7 +332,7 @@ Lemma fixed_non_byzantine_projection_valid_no_equivocations (sub_IM fixed_byzantine_IM (elements non_byzantine)) fixed_set_signed_message l (s, om). -Proof. +Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety. intros l s om Hv. apply (sub_IM_no_equivocation_preservation fixed_byzantine_IM (elements non_byzantine) @@ -354,7 +355,7 @@ Qed. Lemma fixed_non_byzantine_pre_loaded_incl : VLSM_incl fixed_non_byzantine_projection pre_loaded_fixed_non_byzantine_vlsm'. -Proof. +Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety. apply basic_VLSM_incl. - by intro; intros; apply fixed_non_byzantine_projection_initial_state_preservation. - intros l s m (Hs & _ & Hv) HsY _. @@ -377,7 +378,7 @@ Lemma pre_loaded_fixed_non_byzantine_vlsm_lift_valid non_byzantine_not_equivocating_constraint) (lift_sub_label fixed_byzantine_IM (elements non_byzantine)) (lift_sub_state fixed_byzantine_IM (elements non_byzantine)). -Proof. +Proof using can_emit_signed Hsender_safety. intros (sub_i, li) s om (HsX & HomX & Hv & Hc & _) HsY HomY. destruct_dec_sig sub_i i Hi Heqsub_i; subst. split; [by apply lift_sub_valid |]. @@ -406,7 +407,7 @@ Lemma pre_loaded_fixed_non_byzantine_vlsm_lift_initial_message (composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint) (lift_sub_state fixed_byzantine_IM (elements non_byzantine)). -Proof. +Proof using no_initial_messages_in_IM. intros l s m Hv HsY HmX. destruct HmX as [[sub_i [[im Him] Heqm]] | Hseeded]. - exfalso. clear -no_initial_messages_in_IM Him. @@ -461,7 +462,7 @@ Lemma pre_loaded_fixed_non_byzantine_vlsm_lift : (composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint) (lift_sub_label fixed_byzantine_IM (elements non_byzantine)) (lift_sub_state fixed_byzantine_IM (elements non_byzantine)). -Proof. +Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety. apply basic_VLSM_embedding. - by intro; intros; apply pre_loaded_fixed_non_byzantine_vlsm_lift_valid. - by intro; intros * []; rapply lift_sub_transition. @@ -471,7 +472,7 @@ Qed. Lemma pre_loaded_fixed_non_byzantine_incl : VLSM_incl pre_loaded_fixed_non_byzantine_vlsm' fixed_non_byzantine_projection. -Proof. +Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety. apply basic_VLSM_incl; cbn. - by intro; intros; apply fixed_non_byzantine_projection_initial_state_preservation. - by intros l s m Hv _ Him; apply initial_message_is_valid. @@ -487,7 +488,7 @@ Qed. Lemma fixed_non_byzantine_pre_loaded_eq : VLSM_eq fixed_non_byzantine_projection pre_loaded_fixed_non_byzantine_vlsm'. -Proof. +Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety. apply VLSM_eq_incl_iff. split. - by apply fixed_non_byzantine_pre_loaded_incl. - by apply pre_loaded_fixed_non_byzantine_incl. @@ -551,7 +552,7 @@ Lemma fixed_non_equivocating_incl_sub_non_equivocating (pre_induced_sub_projection IM (elements selection_complement) (sub_IM_not_equivocating_constraint IM (elements selection_complement) A sender)). -Proof. +Proof using can_emit_signed Hsender_safety H6 H3 H. apply induced_sub_projection_constraint_subsumption_incl. intros l (s, om) Hv. apply (fixed_strong_equivocation_subsumption IM selection) @@ -580,7 +581,7 @@ Qed. Lemma fixed_non_equivocating_incl_fixed_non_byzantine : VLSM_incl FixedNonEquivocating PreNonByzantine. -Proof. +Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety H6 H3. apply basic_VLSM_incl. - intros s (sX & <- & Hinitial) sub_i. by apply Hinitial. @@ -622,7 +623,7 @@ Qed. Corollary fixed_equivocating_traces_are_byzantine is tr : finite_valid_trace Fixed is tr -> fixed_byzantine_trace_alt_prop IM selection A sender is tr. -Proof. +Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety H6 H3. intro Htr. apply (VLSM_incl_finite_valid_trace fixed_non_equivocating_incl_fixed_non_byzantine). specialize @@ -646,7 +647,7 @@ Lemma fixed_non_byzantine_vlsm_lift_valid : weak_embedding_valid_preservation PreNonByzantine Fixed (lift_sub_label IM (elements selection_complement)) (lift_sub_state IM (elements selection_complement)). -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm. intros l s om Hv HsY HomY. split. - by apply lift_sub_valid, Hv. @@ -727,7 +728,7 @@ Lemma fixed_non_byzantine_vlsm_lift_from_initial : VLSM_embedding PreNonByzantine Fixed (lift_sub_label IM (elements selection_complement)) (lift_sub_state IM (elements selection_complement)). -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull Hfixed_non_byzantine_vlsm_lift_initial_message H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm. apply basic_VLSM_embedding. - by intro; intros; apply fixed_non_byzantine_vlsm_lift_valid. - by intro; intros * []; rapply lift_sub_transition. @@ -737,7 +738,7 @@ Qed. Lemma fixed_non_byzantine_incl_fixed_non_equivocating_from_initial : VLSM_incl PreNonByzantine FixedNonEquivocating. -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull Hfixed_non_byzantine_vlsm_lift_initial_message H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm. apply basic_VLSM_incl. - intro; intros. exists (lift_sub_state IM (elements selection_complement) s). @@ -759,7 +760,7 @@ Qed. Lemma fixed_non_byzantine_eq_fixed_non_equivocating_from_initial : VLSM_eq PreNonByzantine FixedNonEquivocating. -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull Hfixed_non_byzantine_vlsm_lift_initial_message H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm. apply VLSM_eq_incl_iff. split. - by apply fixed_non_byzantine_incl_fixed_non_equivocating_from_initial. @@ -777,7 +778,7 @@ Context Lemma validator_fixed_non_byzantine_vlsm_lift_initial_message : weak_embedding_initial_message_preservation PreNonByzantine Fixed (lift_sub_state IM (elements selection_complement)). -Proof. +Proof using Hvalidator H6 H3. intros l s m Hv HsY HmX. destruct HmX as [[sub_i [[im Him] Heqm]] | Hseeded]. - simpl in Heqm. subst. @@ -800,7 +801,7 @@ Qed. *) Lemma validator_fixed_non_byzantine_eq_fixed_non_equivocating : VLSM_eq PreNonByzantine FixedNonEquivocating. -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hvalidator Hsender_safety Hfull H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm. apply fixed_non_byzantine_eq_fixed_non_equivocating_from_initial. by apply validator_fixed_non_byzantine_vlsm_lift_initial_message. Qed. @@ -824,7 +825,7 @@ Lemma validator_fixed_byzantine_traces_equivocation_char bis btr composite_state_sub_projection IM (elements selection_complement) bis /\ finite_trace_sub_projection IM (elements selection_complement) etr = finite_trace_sub_projection IM (elements selection_complement) btr. -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hvalidator Hsender_safety Hfull H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm. unfold fixed_byzantine_trace_alt_prop. split; intros Htr. - apply fixed_non_equivocating_traces_char. diff --git a/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v index b7abed9a..27789d0f 100644 --- a/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v +++ b/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v @@ -1,3 +1,4 @@ +Set Default Proof Using "Type". From stdpp Require Import prelude finite. From Coq Require Import FunctionalExtensionality Reals. From VLSM.Lib Require Import Preamble FinSetExtras ListFinSetExtras. @@ -108,7 +109,7 @@ Lemma limited_PreNonByzantine_valid_state_lift_not_heavy s (Hs : valid_state_prop PreNonByzantine s) (sX := lift_sub_state IM (elements non_byzantine) s) : tracewise_not_heavy sX. -Proof. +Proof using Inj0 Hlimit H6 H3. cut (tracewise_equivocating_validators sX ⊆ byzantine_vs). { intro Hincl. @@ -177,7 +178,7 @@ Lemma limited_PreNonByzantine_lift_valid : weak_embedding_valid_preservation PreNonByzantine Limited (lift_sub_label IM (elements non_byzantine)) (lift_sub_state IM (elements non_byzantine)). -Proof. +Proof using Inj0 Hlimit H6 H3. intros l s om Hv HsY HomY. repeat split; [by apply lift_sub_valid, Hv |]. hnf. @@ -200,7 +201,7 @@ Lemma limited_PreNonByzantine_vlsm_lift : VLSM_embedding PreNonByzantine Limited (lift_sub_label IM (elements non_byzantine)) (lift_sub_state IM (elements non_byzantine)). -Proof. +Proof using Inj0 Hvalidator Hlimit H6 H3. apply basic_VLSM_embedding; intros ? *. - by intros; apply limited_PreNonByzantine_lift_valid. - by intros * []; rapply lift_sub_transition. @@ -233,7 +234,7 @@ Lemma validator_fixed_limited_non_byzantine_traces_are_limited_non_equivocating composite_state_sub_projection IM (elements not_byzantine) bs /\ finite_trace_sub_projection IM (elements not_byzantine) tr = finite_trace_sub_projection IM (elements not_byzantine) btr. -Proof. +Proof using Inj0 Hvalidator H6 H3. intros [Hlimit Hfixed]. eexists _, _; split. - by apply (VLSM_embedding_finite_valid_trace @@ -263,7 +264,7 @@ Lemma validator_limited_non_byzantine_traces_are_limited_non_equivocating s tr composite_state_sub_projection IM (elements selection_complement) bs /\ finite_trace_sub_projection IM (elements selection_complement) tr = finite_trace_sub_projection IM (elements selection_complement) btr. -Proof. +Proof using Inj0 Hvalidator H6 H3. intros [byzantine Hlimited]. apply proj1 in Hlimited as Hlimit. apply validator_fixed_limited_non_byzantine_traces_are_limited_non_equivocating @@ -333,7 +334,7 @@ Lemma lift_pre_loaded_fixed_non_byzantine_valid_transition_to_limited (Build_annotated_state (free_composite_vlsm IM) Cv (lift_sub_state IM (elements non_byzantine) sub_sf) ann', oom). -Proof. +Proof using Hvalidator H17 H15 H14 EqDecision1. destruct sub_l as [sub_i li]; destruct_dec_sig sub_i i Hi Heqsub_i; subst. repeat split; cbn. - done. @@ -389,7 +390,7 @@ Lemma lift_fixed_byzantine_traces_to_limited (finite_trace_sub_projection IM (elements non_byzantine) tr))) : finite_valid_trace Limited bs btr /\ state_annotation (@finite_trace_last _ (type Limited) bs btr) ⊆ byzantine_vs. -Proof. +Proof using message_dependencies Inj0 Hvalidator Hfull H6 H3 H28 H27 H25 H24 H20 H17 H15 H14 FullMessageDependencies0 EqDecision2 EqDecision1. subst non_byzantine. induction Hbyzantine using finite_valid_trace_rev_ind; [repeat split |]. - constructor; apply initial_state_is_valid. @@ -474,7 +475,7 @@ Lemma msg_dep_validator_limited_non_equivocating_byzantine_traces_are_limited_no finite_trace_sub_projection IM (elements selection_complement) (pre_VLSM_embedding_finite_trace_project (type Limited) (composite_type IM) Datatypes.id original_state btr). -Proof. +Proof using no_initial_messages_in_IM message_dependencies Inj0 Hvalidator Hfull Hchannel H6 H3 H28 H27 H25 H24 H20 H18 H17 H15 H14 FullMessageDependencies0 EqDecision2 EqDecision1. split. - intros (byzantine & Hlimited & Hbyzantine). apply lift_fixed_byzantine_traces_to_limited in Hbyzantine diff --git a/theories/VLSM/Core/Composition.v b/theories/VLSM/Core/Composition.v index 042f83f8..a7a9d4ea 100644 --- a/theories/VLSM/Core/Composition.v +++ b/theories/VLSM/Core/Composition.v @@ -4,6 +4,8 @@ From Coq Require Import Streams FunctionalExtensionality Eqdep_dec. From VLSM.Lib Require Import Preamble ListExtras. From VLSM.Core Require Import VLSM Plans VLSMProjections. +Set Default Proof Using "Type". + (** * VLSM Composition This module provides Coq definitions for composite VLSMs and their projections @@ -1105,7 +1107,7 @@ Context Lemma composite_decidable_initial_message (Hdec_init : forall i, vdecidable_initial_messages_prop (IM i)) : decidable_initial_messages_prop (composite_vlsm_machine IM constraint). -Proof. +Proof using H. intro m. simpl. unfold composite_initial_message_prop. apply (Decision_iff @@ -1411,39 +1413,39 @@ Context {message : Type} Lemma empty_composition_no_index (i : index) : False. -Proof. +Proof using Hempty_index H EqDecision0. by specialize (elem_of_enum i); rewrite Hempty_index; apply not_elem_of_nil. Qed. Lemma empty_composition_single_state (s : composite_state IM) : s = (proj1_sig (composite_s0 IM)). -Proof. +Proof using Hempty_index H EqDecision0. by extensionality i; elim (empty_composition_no_index i). Qed. Lemma empty_composition_no_label (l : composite_label IM) : False. -Proof. +Proof using Hempty_index H EqDecision0. by destruct l as [i _]; elim (empty_composition_no_index i). Qed. Lemma empty_composition_no_initial_message : forall m, ~ composite_initial_message_prop IM m. -Proof. +Proof using Hempty_index H EqDecision0. by intros m [i _]; elim (empty_composition_no_index i). Qed. Lemma empty_composition_no_emit : forall m, ~ can_emit X m. -Proof. +Proof using Hempty_index H. by intros m [s' [l _]]; elim (empty_composition_no_label l). Qed. Lemma empty_composition_no_valid_message : forall m, ~ valid_message_prop X m. -Proof. +Proof using Hempty_index H. intros m Hm. apply emitted_messages_are_valid_iff in Hm as [Hinit | Hemit]. - by elim (empty_composition_no_initial_message _ Hinit). @@ -1454,13 +1456,13 @@ Lemma pre_loaded_empty_composition_no_emit (seed : message -> Prop) (PreX := pre_loaded_vlsm X seed) : forall m, ~ can_emit PreX m. -Proof. +Proof using Hempty_index H. by intros m [s' [l _]]; elim (empty_composition_no_label l). Qed. Lemma pre_loaded_with_all_empty_composition_no_emit : forall m, ~ can_emit (pre_loaded_with_all_messages_vlsm X) m. -Proof. +Proof using Hempty_index H. by intros m [s' [l _]]; elim (empty_composition_no_label l). Qed. @@ -1510,7 +1512,7 @@ Lemma same_IM_embedding (pre_loaded_vlsm (composite_vlsm IM2 constraint2) seed) same_IM_label_rew same_IM_state_rew. -Proof. +Proof using constraint_projection. apply basic_VLSM_embedding; intros l **. - destruct Hv as [Hs [Hom [Hv Hc]]]. apply constraint_projection in Hc; cycle 1. @@ -1666,7 +1668,7 @@ Context Lemma not_CompositeValidTransitionNext_initial : forall s2, composite_initial_state_prop IM s2 -> forall s1, ~ CompositeValidTransitionNext IM s1 s2. -Proof. +Proof using H. intros s2 Hs2 s1 [* Hs1]. apply composite_valid_transition_projection, proj1, valid_transition_next in Hs1; cbn in Hs1. by contradict Hs1; apply not_ValidTransitionNext_initial, Hs2. @@ -1678,7 +1680,7 @@ Lemma composite_quasi_unique_transition_to_state : forall [l2 s2 iom2 oom2], CompositeValidTransition IM l2 s2 iom2 s oom2 -> projT1 l1 = projT1 l2 -> l1 = l2 /\ s1 = s2 /\ iom1 = iom2 /\ oom1 = oom2. -Proof. +Proof using H. intros ? [i li1] * Ht1 [_i li2] * Ht2 [=]; subst _i. apply composite_valid_transition_projection in Ht1, Ht2; cbn in Ht1, Ht2. destruct Ht1 as [Ht1 Heq_s], Ht2 as [Ht2 Heqs]. @@ -1696,7 +1698,7 @@ Lemma CompositeValidTransition_reflects_rechability : CompositeValidTransition IM l s1 iom s2 oom -> valid_state_prop RFree s2 -> input_valid_transition RFree l (s1, iom) (s2, oom). -Proof. +Proof using H. intros * Hnext Hs2; revert l s1 iom oom Hnext. induction Hs2 using valid_state_prop_ind; intros * Hnext. - apply composite_valid_transition_next in Hnext. @@ -1744,20 +1746,20 @@ Qed. Lemma CompositeValidTransitionNext_reflects_rechability : forall s1 s2, CompositeValidTransitionNext IM s1 s2 -> valid_state_prop RFree s2 -> valid_state_prop RFree s1. -Proof. +Proof using H. by intros s1 s2 []; eapply CompositeValidTransition_reflects_rechability. Qed. Lemma composite_valid_transition_future_reflects_rechability : forall s1 s2, composite_valid_transition_future IM s1 s2 -> valid_state_prop RFree s2 -> valid_state_prop RFree s1. -Proof. by apply tc_reflect, CompositeValidTransitionNext_reflects_rechability. Qed. +Proof using H. by apply tc_reflect, CompositeValidTransitionNext_reflects_rechability. Qed. Lemma composite_valid_transitions_from_to_reflects_reachability : forall s s' tr, CompositeValidTransitionsFromTo IM s s' tr -> valid_state_prop RFree s' -> finite_valid_trace_from_to RFree s s' tr. -Proof. +Proof using H. induction 1; intros; [by constructor |]. assert (Hitem : input_valid_transition RFree (l item) (s', input item) (destination item, output item)) diff --git a/theories/VLSM/Core/ELMO/BaseELMO.v b/theories/VLSM/Core/ELMO/BaseELMO.v index 2cd77b5e..4cb116c8 100644 --- a/theories/VLSM/Core/ELMO/BaseELMO.v +++ b/theories/VLSM/Core/ELMO/BaseELMO.v @@ -4,6 +4,8 @@ From VLSM.Lib Require Import EquationsExtras. From VLSM.Lib Require Import Preamble StdppExtras. From VLSM.Core Require Import VLSM MessageDependencies. +Set Default Proof Using "Type". + (** * Basic Definitions and Lemmas for UMO, MO and ELMO This module contains basic definitions and lemmas needed for the UMO, MO and @@ -77,7 +79,7 @@ Proof. by intros x y; unfold Decision; decide equality. Defined. #[local] Lemma State_eq_dec : forall x y : State, {x = y} + {x <> y} with Observation_eq_dec : forall x y : Observation, {x = y} + {x <> y} with Message_eq_dec : forall x y : Message, {x = y} + {x <> y}. -Proof. +Proof using EqDecision0. - intros x y; decide equality. + by apply EqDecision0. + by decide equality. @@ -696,7 +698,7 @@ Definition ELMO_A (a : Address) : index := hd inhabitant (filter (fun i => idx i = a) (enum index)). Lemma ELMO_A_inv : forall i, ELMO_A (idx i) = i. -Proof. +Proof using Inj0. intro i; unfold ELMO_A; cbn. replace (filter _ _) with [i]; [done |]. generalize (enum index), (NoDup_enum index) as Hnodup, (elem_of_enum i) as Hi. diff --git a/theories/VLSM/Core/ELMO/ELMO.v b/theories/VLSM/Core/ELMO/ELMO.v index 31549ac8..0db2eb61 100644 --- a/theories/VLSM/Core/ELMO/ELMO.v +++ b/theories/VLSM/Core/ELMO/ELMO.v @@ -7,6 +7,8 @@ From VLSM.Core Require Import Validator ProjectionTraces MessageDependencies. From VLSM.Core Require Import TraceableVLSM MinimalEquivocationTrace. From VLSM.Core Require Import BaseELMO UMO MO. +Set Default Proof Using "Type". + Create HintDb ELMO_hints. #[local] Hint Resolve submseteq_tail_l : ELMO_hints. @@ -204,7 +206,7 @@ Proof. Qed. #[export] Instance local_equivocators_full_obs_dec : RelDecision local_equivocators_full_obs. -Proof. +Proof using EqDecision0. intros ol a. induction ol using addObservation'_rec. - by right; inversion 1. @@ -326,7 +328,7 @@ Definition ELMOComponent (i : index) : VLSM Message := #[export] Instance ComputableSentMessages_ELMOComponent (i : index) : ComputableSentMessages (ELMOComponent i). -Proof. +Proof using Inj0. constructor 1 with sentMessages; constructor. - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil. - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *. @@ -340,7 +342,7 @@ Defined. #[export] Instance ComputableReceivedMessages_ELMOComponent (i : index) : ComputableReceivedMessages (ELMOComponent i). -Proof. +Proof using Inj0. constructor 1 with receivedMessages; constructor. - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil. - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *. @@ -588,7 +590,7 @@ Lemma local_equivocators_simple_addObservation : adr (state (message ob)) = a /\ message ob ∉ messages s /\ exists m, m ∈ messages s /\ incomparable (message ob) m. -Proof. +Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca. intros s ob a []. apply elem_of_messages_addObservation in les_obs_m1 as [-> | Hm1], les_obs_m2 as [-> | Hm2]. - by destruct les_incomparable as [? []]; constructor. @@ -606,7 +608,7 @@ Lemma local_equivocators_simple_add_Send (s : State) : UMO_reachable no_self_equiv s -> forall a, local_equivocators_simple (s <+> MkObservation Send (MkMessage s)) a -> local_equivocators_simple s a. -Proof. +Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca. intros Hs a Ha. apply local_equivocators_simple_addObservation in Ha as [| (<- & _ & m & Hm & Hincomp)]; [done |]; cbn in *. @@ -621,7 +623,7 @@ Qed. Lemma local_equivocators_simple_no_self (s : State) : UMO_reachable no_self_equiv s -> ~ local_equivocators_simple s (adr s). -Proof. +Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca. intros Hs; induction Hs as [| | ? ? Hno_self_eqv]. - by destruct 1; inversion les_obs_m1. - by contradict IHHs; apply local_equivocators_simple_add_Send in IHHs. @@ -665,7 +667,7 @@ Lemma local_equivocators_simple_add_Receive (s : State) (msg : Message) : local_equivocators_simple s i \/ adr (state msg) = i /\ i <> adr s /\ exists m, m ∈ messages s /\ incomparable msg m. -Proof. +Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca. intros Hs Hno_equiv a Ha. assert (a <> adr (s <+> MkObservation Receive msg)) by (contradict Ha; subst; apply local_equivocators_simple_no_self; constructor; done). @@ -743,7 +745,7 @@ Qed. Lemma local_equivocators_simple_iff_full (s : State) : UMO_reachable no_self_equiv s -> forall a, local_equivocators_simple s a <-> local_equivocators_full s a. -Proof. +Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca. intros Hs a; split. - induction Hs. + by destruct 1; inversion les_obs_m1. @@ -782,7 +784,7 @@ Qed. Lemma local_equivocators_iff_full (s : State) : UMO_reachable (fun s m => full_node s m /\ no_self_equiv s m) s -> forall a, local_equivocators s a <-> local_equivocators_full s a. -Proof. +Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca. intros Hs a. by rewrite local_equivocators_iff_simple; [apply local_equivocators_simple_iff_full |]; @@ -871,7 +873,7 @@ Lemma equivocation_limit_recv_ok_msg_ok (s : State) (m : Message) : UMO_reachable no_self_equiv (state m) -> local_equivocation_limit_ok (s <+> MkObservation Receive m) -> local_equivocation_limit_ok (state m). -Proof. +Proof using i Ri Ei. intros Hfull Hno_self Hs Hms Hs'. eapply Rle_trans; [| done]. apply incl_equivocating_validators_equivocation_fault, filter_subprop; cbn; intros a Ha. @@ -998,7 +1000,7 @@ Lemma reachable_received_messages_reachable (s : State) : forall i', adr (state m) = idx i' -> ram_state_prop (ELMOComponent i') (state m). -Proof. +Proof using Inj0. intros Hs m Hm. destruct (decide (adr (state m) = adr s)). { @@ -1067,7 +1069,7 @@ Lemma receivable_messages_reachable (ms s : State) i' : ram_state_prop Ei s -> ELMO_recv_valid s (MkMessage ms) -> ram_state_prop (ELMOComponent i') ms. -Proof. +Proof using Inj0. intros Heq Hram Hrv. change ms with (state (MkMessage ms)). apply reachable_received_messages_reachable @@ -1119,7 +1121,7 @@ Lemma ELMOComponent_receivedMessages_of_ram_trace [s s' tr] (Htr : finite_valid_trace_from_to Ri s s' tr) : forall item, item ∈ tr -> forall m, (field_selector input) m item -> m ∈ receivedMessages s'. -Proof. +Proof using Inj0. induction Htr using finite_valid_trace_from_to_rev_ind; [by inversion 1 |]. intros item Hitem m Hm. change (has_been_received Ei sf m). @@ -1132,7 +1134,7 @@ Lemma ELMOComponent_sentMessages_of_ram_trace [s s' tr] (Htr : finite_valid_trace_from_to Ri s s' tr) : forall item, item ∈ tr -> forall m, (field_selector output) m item -> m ∈ sentMessages s'. -Proof. +Proof using Inj0. induction Htr using finite_valid_trace_from_to_rev_ind; [by inversion 1 |]. intros item Hitem m Hm. change (has_been_sent Ei sf m). @@ -1158,7 +1160,7 @@ Lemma ELMOComponent_messages_of_ram_trace [s s' tr] (Htr : finite_valid_trace_from_to Ri s s' tr) : forall item, item ∈ tr -> forall m, item_sends_or_receives m item -> m ∈ messages s'. -Proof. +Proof using Inj0. intros ? ? ? [|]; apply elem_of_messages. - by right; eapply ELMOComponent_receivedMessages_of_ram_trace. - by left; eapply ELMOComponent_sentMessages_of_ram_trace. @@ -1552,7 +1554,7 @@ Qed. Lemma ELMO_channel_authentication_prop : channel_authentication_prop ELMOComponent (ELMO_A idx) Message_sender. -Proof. +Proof using Inj0. intros i m ((s, []) & [] & s' & [(Hs & _ & Hv) Ht]); inversion Hv; subst; inversion Ht; subst. unfold channel_authenticated_message; cbn; f_equal. @@ -2003,7 +2005,7 @@ Lemma ELMO_update_state_with_initial ELMO_equivocating_validators (state_update ELMOComponent s i si) ⊆ ELMO_equivocating_validators s ∪ {[ idx i ]}. -Proof. +Proof using H8. assert (Hincl : VLSM_incl ELMOProtocol ReachELMO) by apply constraint_preloaded_free_incl. assert (Htr_min := ELMO_state_to_minimal_equivocation_trace_valid _ Hs). cbn in Htr_min; destruct (ELMO_state_to_minimal_equivocation_trace _ _) @@ -2110,7 +2112,7 @@ Lemma ELMO_valid_states_only_receive_valid_messages : forall (i : index) (l : Label) (s' : vstate ELMOProtocol) (m : Message), ELMOProtocolValidTransition i l s s' m -> valid_message_prop ELMOProtocol m. -Proof. +Proof using H8. intros s Hs i l s' m Hvalid. inversion Hvalid as [? ? ? ? Hreceive | ? ? ? ? Hsend]; subst; cycle 1. { @@ -2815,7 +2817,7 @@ Lemma reflecting_composite_for_reachable_component let s' := state_update ELMOComponent s i s_prev in valid_state_prop ELMOProtocol s' /\ ELMOProtocolValidTransition i l s' s m. -Proof. +Proof using H8. induction Hreachable using valid_state_prop_ind; [| destruct IHHreachable as (sigma & <- & Hsigma & Hreflects & Hsend & Hall), l; cycle 1]. - unfold initial_state_prop in Hs; cbn in Hs. @@ -3011,7 +3013,7 @@ Qed. Theorem ELMOComponents_validating : forall i : index, component_projection_validator_prop ELMOComponent ELMO_global_constraint i. -Proof. +Proof using H8. intros i li si om Hvti. apply input_valid_transition_iff in Hvti as [[si' om'] Hvti]. pose (Hvti' := Hvti); destruct Hvti' as [(_ & _ & Hvi) Hti]. diff --git a/theories/VLSM/Core/ELMO/UMO.v b/theories/VLSM/Core/ELMO/UMO.v index 481a06ad..52331dc6 100644 --- a/theories/VLSM/Core/ELMO/UMO.v +++ b/theories/VLSM/Core/ELMO/UMO.v @@ -5,6 +5,8 @@ From VLSM.Lib Require Import Preamble StdppExtras StdppListSet. From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation ProjectionTraces. From VLSM.Core Require Import BaseELMO. +Set Default Proof Using "Type". + (** * UMO Protocol Definitions and Properties This module contains definitions and properties of UMO components and @@ -105,7 +107,7 @@ Qed. #[export] Instance HasBeenSentCapability_UMOComponent (i : Address) : HasBeenSentCapability (UMOComponent i). -Proof. +Proof using EqDecision0. apply Build_HasBeenSentCapability with (fun s m => m ∈ sentMessages s) ; [by intros s m; typeclasses eauto |]. split. @@ -121,7 +123,7 @@ Defined. #[export] Instance HasBeenReceivedCapability_UMOComponent (i : Address) : HasBeenReceivedCapability (UMOComponent i). -Proof. +Proof using EqDecision0. eapply Build_HasBeenReceivedCapability with (fun s m => m ∈ receivedMessages s) ; [intros s m; typeclasses eauto | split]. - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil. @@ -1399,7 +1401,7 @@ End sec_UMOComponent_lemmas. Proof. by intros x y []; constructor. Defined. #[export] Instance sent_comparable_dec : RelDecision sent_comparable. -Proof. +Proof using EqDecision0. intros m1 m2. destruct (decide (adr (state m1) = adr (state m2))); [| by right; destruct 1; apply n; firstorder congruence]. @@ -1599,7 +1601,7 @@ Lemma finite_valid_trace_from_to_UMO_state2trace_UMO : forall us : UMO_state, valid_state_prop UMO us -> finite_valid_trace_init_to UMO (``(vs0 UMO)) us (UMO_state2trace us). -Proof. +Proof using EqDecision0. intros us Hvsp. apply all_pre_traces_to_valid_state_are_valid; [typeclasses eauto | done |]. apply finite_valid_trace_from_to_UMO_state2trace_RUMO. @@ -1661,7 +1663,7 @@ Lemma elem_of_UMO_sentMessages : forall (us : UMO_state) (m : Message) (i : index), valid_state_prop RUMO us -> idx i = adr (state m) -> m ∈ UMO_sentMessages us <-> m ∈ sentMessages (us i). -Proof. +Proof using Inj0. intros us m i Hvsp Hidx. assert (Hall : forall i, i ∉ enum index -> us i = MkState [] (idx i)) by (intros j Hin; contradict Hin; apply elem_of_enum). @@ -1704,7 +1706,7 @@ Lemma UMO_sentMessages_characterization : <-> let s' := state m <+> MkObservation Send m in state_suffix s' (us i) \/ s' = us i. -Proof. +Proof using Inj0. intros us m i Hvsp Hidx. rewrite elem_of_UMO_sentMessages by done. rewrite <- sentMessages_characterization; [done |]. diff --git a/theories/VLSM/Core/Equivocation.v b/theories/VLSM/Core/Equivocation.v index d30eb58e..291d55f5 100644 --- a/theories/VLSM/Core/Equivocation.v +++ b/theories/VLSM/Core/Equivocation.v @@ -6,6 +6,8 @@ From VLSM.Lib Require Import ListSetExtras Measurable. From VLSM.Core Require Import VLSM VLSMProjections Composition ProjectionTraces Validator. From VLSM.Core Require Export ReachableThreshold. +Set Default Proof Using "Type". + (** * VLSM Equivocation Definitions This module is dedicated to building the vocabulary for discussing equivocation. @@ -881,7 +883,7 @@ Lemma prove_all_have_message_from_stepwise : (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s) (m : message), all_traces_have_message_prop vlsm selector oracle s m. -Proof. +Proof using oracle_props. intros s Hproto m. unfold all_traces_have_message_prop. split. @@ -898,7 +900,7 @@ Lemma prove_none_have_message_from_stepwise : (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s) (m : message), no_traces_have_message_prop vlsm selector (fun s m => ~ oracle s m) s m. -Proof. +Proof using oracle_props. intros s Hproto m. split. - intros H_not_holds start tr Htr. @@ -916,7 +918,7 @@ Lemma selected_messages_consistency_prop_from_stepwise (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s) (m : message) : selected_messages_consistency_prop vlsm selector s m. -Proof. +Proof using oracle_props. split; [| by apply consistency_from_valid_state_proj2]. intro Hsome. destruct (decide (oracle s m)) as [Hsm | Hsm]. @@ -931,7 +933,7 @@ Lemma in_futures_preserving_oracle_from_stepwise : (Hfutures : in_futures (pre_loaded_with_all_messages_vlsm vlsm) s1 s2) (m : message), oracle s1 m -> oracle s2 m. -Proof. +Proof using selector oracle_props. intros s1 s2 [tr Htr] m Hs1m. by eapply oracle_partial_trace_update; [| | right]. Qed. @@ -963,7 +965,7 @@ Context Lemma oracle_no_inits_from_trace : forall (s : vstate vlsm), initial_state_prop (VLSMMachine := vmachine vlsm) s -> forall m, ~ oracle s m. -Proof. +Proof using selector Horacle_all_have. intros s Hinit m Horacle. assert (Hproto : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s) by (apply initial_state_is_valid; done). @@ -979,7 +981,7 @@ Lemma examine_one_trace : forall m, oracle s m <-> trace_has_message selector m tr. -Proof. +Proof using oracle_dec Horacle_all_have Hnot_oracle_none_have. intros is s tr Htr m. assert (valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s) by (apply valid_trace_last_pstate in Htr; done). @@ -1002,7 +1004,7 @@ Lemma oracle_step_property_from_trace : forall msg, oracle s' msg <-> (selector msg {| l := l; input := im; destination := s'; output := om |} \/ oracle s msg). -Proof. +Proof using oracle_dec Horacle_all_have Hnot_oracle_none_have. intros l s im s' om Htrans msg. rename Htrans into Htrans'. pose proof Htrans' as [[Hproto_s [Hproto_m Hvalid]] Htrans]. @@ -1019,7 +1021,7 @@ Proof. Qed. Lemma stepwise_props_from_trace : oracle_stepwise_props selector oracle. -Proof. +Proof using oracle_dec Horacle_all_have Hnot_oracle_none_have. constructor. - by apply oracle_no_inits_from_trace. - by apply oracle_step_property_from_trace. @@ -1493,7 +1495,7 @@ Qed. Lemma com_computable_oracle : computable_messages_oracle vlsm directly_observed_messages_set item_sends_or_receives. -Proof. +Proof using EqDecision0. constructor; intros. - setoid_rewrite directly_observed_messages_set_iff. + by apply has_been_directly_observed_stepwise_props. @@ -1633,7 +1635,7 @@ Context . Definition composite_message_selector : message -> composite_transition_item IM -> Prop. -Proof. +Proof using message_selectors. intros msg [[i li] input s output]. apply (message_selectors i msg). exact {| l := li; input := input; destination := s i; output := output |}. @@ -1646,7 +1648,7 @@ Lemma composite_stepwise_props (constraint : composite_label IM -> composite_state IM * option message -> Prop) (X := composite_vlsm IM constraint) : oracle_stepwise_props (vlsm := X) composite_message_selector composite_oracle. -Proof. +Proof using stepwise_props. split. - (* initial states not claim *) intros s Hs m [i Horacle]. @@ -1693,7 +1695,7 @@ Lemma oracle_component_selected_previously in_futures X (destination item) s /\ projT1 (l item) = i /\ composite_message_selector m item. -Proof. +Proof using stepwise_props. apply valid_state_has_trace in Hs as (is & tr & Htr). eapply VLSM_incl_finite_valid_trace_init_to in Htr as Hpre_tr ; [| by apply constraint_preloaded_free_incl]. @@ -1735,7 +1737,7 @@ Definition composite_has_been_sent (** [composite_has_been_sent] is decidable. *) Lemma composite_has_been_sent_dec : RelDecision composite_has_been_sent. -Proof. +Proof using H EqDecision0. intros s m. apply (Decision_iff (P := List.Exists (fun i => has_been_sent (IM i) (s i) m) (enum index))). - by rewrite Exists_finite. @@ -1768,7 +1770,7 @@ Lemma composite_proper_sent (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) s) (m : message) : has_been_sent_prop (free_composite_vlsm IM) composite_has_been_sent s m. -Proof. +Proof using H. specialize (proper_sent (free_composite_vlsm IM)) as Hproper_sent. by apply Hproper_sent. Qed. @@ -1787,7 +1789,7 @@ Definition composite_has_been_received (** [composite_has_been_received] is decidable. *) Lemma composite_has_been_received_dec : RelDecision composite_has_been_received. -Proof. +Proof using H EqDecision0. intros s m. apply (Decision_iff (P := List.Exists (fun i => has_been_received (IM i) (s i) m) (enum index))). - by rewrite Exists_finite. @@ -1858,7 +1860,7 @@ Definition composite_has_been_directly_observed (** [composite_has_been_directly_observed] is decidable. *) Lemma composite_has_been_directly_observed_dec : RelDecision composite_has_been_directly_observed. -Proof. +Proof using H EqDecision0. intros s m. apply (Decision_iff (P := List.Exists (fun i => has_been_directly_observed (IM i) (s i) m) (enum index))). @@ -1882,7 +1884,7 @@ Definition composite_HasBeenDirectlyObservedCapability_from_stepwise (constraint : composite_label IM -> composite_state IM * option message -> Prop) (X := composite_vlsm IM constraint) : HasBeenDirectlyObservedCapability X. -Proof. +Proof using H1 H0 H. exists composite_has_been_directly_observed. - by apply composite_has_been_directly_observed_dec. - by apply (composite_has_been_directly_observed_stepwise_props constraint). @@ -1938,7 +1940,7 @@ Definition sender_safety_alt_prop : Prop := Lemma sender_safety_alt_iff : sender_safety_prop <-> sender_safety_alt_prop. -Proof. +Proof using EqDecision0. split; intros Hsender_safety m; intros. - specialize (Hsender_safety m v Hsender). destruct (decide (i = A v)); [done |]. @@ -2149,7 +2151,6 @@ Lemma sent_component_sent_previously projT1 (l item) = i /\ output item = Some m. Proof. - clear -Hs Horacle. specialize (oracle_component_selected_previously (fun i => has_been_sent_stepwise_props (IM i)) @@ -2172,7 +2173,6 @@ Lemma received_component_received_previously projT1 (l item) = i /\ input item = Some m. Proof. - clear -Hs Horacle. specialize (oracle_component_selected_previously (fun i => has_been_received_stepwise_props (IM i)) @@ -2213,7 +2213,7 @@ Lemma messages_sent_from_component_of_valid_state_are_valid (m : message) (Hsent : has_been_sent (IM i) (s i) m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H0 IM index message. by apply (sent_valid X s); [| exists i]. Qed. @@ -2227,7 +2227,7 @@ Lemma preloaded_messages_sent_from_component_of_valid_state_are_valid (m : message) (Hsent : has_been_sent (IM i) (s i) m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H0 IM index message. by eapply sent_valid; [| exists i]. Qed. @@ -2240,7 +2240,7 @@ Lemma messages_received_from_component_of_valid_state_are_valid (m : message) (Hreceived : has_been_received (IM i) (s i) m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H1 IM index message. by eapply received_valid; [| exists i]. Qed. @@ -2254,7 +2254,7 @@ Lemma preloaded_messages_received_from_component_of_valid_state_are_valid (m : message) (Hreceived : has_been_received (IM i) (s i) m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H1 IM index message. by eapply received_valid; [| exists i]. Qed. @@ -2266,7 +2266,7 @@ Lemma composite_sent_valid (m : message) (Hsent : composite_has_been_sent s m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H0 IM index message. destruct Hsent as [i Hsent]. by apply messages_sent_from_component_of_valid_state_are_valid with s i. Qed. @@ -2280,7 +2280,7 @@ Lemma preloaded_composite_sent_valid (m : message) (Hsent : composite_has_been_sent s m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H0 IM index message. destruct Hsent as [i Hsent]. by apply preloaded_messages_sent_from_component_of_valid_state_are_valid with s i. Qed. @@ -2293,7 +2293,7 @@ Lemma composite_received_valid (m : message) (Hreceived : composite_has_been_received s m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H1 IM index message. destruct Hreceived as [i Hreceived]. by apply messages_received_from_component_of_valid_state_are_valid with s i. Qed. @@ -2307,7 +2307,7 @@ Lemma preloaded_composite_received_valid (m : message) (Hreceived : composite_has_been_received s m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H1 IM index message. destruct Hreceived as [i Hreceived]. by apply preloaded_messages_received_from_component_of_valid_state_are_valid with s i. Qed. @@ -2320,7 +2320,7 @@ Lemma composite_directly_observed_valid (m : message) (Hobserved : composite_has_been_directly_observed s m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H0 H1 IM index message. destruct Hobserved as [i Hobserved]. apply (has_been_directly_observed_sent_received_iff (IM i)) in Hobserved. - destruct Hobserved as [Hreceived | Hsent]. @@ -2338,7 +2338,7 @@ Lemma preloaded_composite_directly_observed_valid (m : message) (Hobserved : composite_has_been_directly_observed s m) : valid_message_prop X m. -Proof. +Proof using EqDecision0 Free H H0 H1 IM index message. destruct Hobserved as [i Hobserved]. apply (has_been_directly_observed_sent_received_iff (IM i)) in Hobserved. - destruct Hobserved as [Hreceived | Hsent]. @@ -2632,7 +2632,7 @@ Context Lemma input_valid_transition_received_not_resent l s m s' om' (Ht : input_valid_transition (pre_loaded_with_all_messages_vlsm X) l (s, Some m) (s', om')) : om' <> Some m. -Proof. +Proof using H H0 Hno_resend X message. destruct om' as [m' |]; [| by congruence]. intro Heq. inversion Heq. subst m'. clear Heq. destruct (Hno_resend _ _ _ _ _ Ht) as [_ Hnbr_m]. @@ -2653,7 +2653,7 @@ Lemma lift_preloaded_trace_to_seeded (is : state) (Htr : finite_valid_trace PreX is tr) : finite_valid_trace (pre_loaded_vlsm X P) is tr. -Proof. +Proof using EqDecision0 H H0 Hno_resend PreX X message. unfold trace_received_not_sent_before_or_after_invariant in Htrm. split; [| by apply Htr]. induction Htr using finite_valid_trace_rev_ind; intros. @@ -2707,7 +2707,7 @@ Lemma lift_preloaded_state_to_seeded (Hequiv_s : state_received_not_sent_invariant s P) (Hs : valid_state_prop PreX s) : valid_state_prop (pre_loaded_vlsm X P) s. -Proof. +Proof using EqDecision0 H H0 Hno_resend PreX X message. apply valid_state_has_trace in Hs as Htr. destruct Htr as [is [tr Htr]]. specialize (lift_preloaded_trace_to_seeded P tr) as Hlift. @@ -2725,7 +2725,7 @@ Lemma lift_generated_to_seeded (m : message) (Hgen : can_produce PreX s m) : can_produce (pre_loaded_vlsm X P) s m. -Proof. +Proof using EqDecision0 H H0 Hno_resend PreX X message. apply non_empty_valid_trace_from_can_produce. apply non_empty_valid_trace_from_can_produce in Hgen. destruct Hgen as [is [tr [item [Htr Hgen]]]]. @@ -2798,7 +2798,7 @@ Lemma all_pre_traces_to_valid_state_are_valid is tr (Htr : finite_valid_trace_init_to PreX is s tr) : finite_valid_trace_init_to X is s tr. -Proof. +Proof using EqDecision0 H H0 IM PreX X constraint index message. apply pre_traces_with_valid_inputs_are_valid in Htr; [done |]. apply valid_trace_last_pstate in Htr as Hspre. intros. diff --git a/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v b/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v index 4f5abd30..8cc5b9df 100644 --- a/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v +++ b/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v @@ -5,6 +5,8 @@ From VLSM.Lib Require Import Preamble. From VLSM.Core Require Import VLSM VLSMProjections Composition Validator ProjectionTraces. From VLSM.Core Require Import SubProjectionTraces Equivocation Equivocation.NoEquivocation. +Set Default Proof Using "Type". + (** * Fixed Set Equivocation In this section we define fixed equivocation for the regular composition. @@ -115,7 +117,7 @@ Definition sent_by_non_equivocating s m := exists i, i ∉ elements equivocating /\ has_been_sent (IM i) (s i) m. #[export] Instance sent_by_non_equivocating_dec : RelDecision sent_by_non_equivocating. -Proof. +Proof using H7 EqDecision0. intros s m. apply @Decision_iff with (P := Exists (fun i => has_been_sent (IM i) (s i) m) (filter (fun i => i ∉ elements equivocating) (enum index))). @@ -136,7 +138,7 @@ Qed. Lemma sent_by_non_equivocating_are_directly_observed s m (Hsent : sent_by_non_equivocating s m) : composite_has_been_directly_observed IM s m. -Proof. +Proof using EqDecision0. apply composite_has_been_directly_observed_sent_received_iff; left. by apply sent_by_non_equivocating_are_sent. Qed. @@ -241,7 +243,7 @@ Lemma fixed_equivocation_index_incl_subsumption : forall s m, fixed_equivocation IM indices1 s m -> fixed_equivocation IM indices2 s m. -Proof. +Proof using Hincl. intros s m [Hobs | Hemit]; [by left |]. right. specialize @@ -254,7 +256,7 @@ Lemma fixed_equivocation_constraint_index_incl_subsumption : strong_constraint_subsumption IM (fixed_equivocation_constraint IM indices1) (fixed_equivocation_constraint IM indices2). -Proof. +Proof using Hincl. intros l (s, [m |]); [| done]. by apply fixed_equivocation_index_incl_subsumption. Qed. @@ -263,7 +265,7 @@ Lemma fixed_equivocation_vlsm_composition_index_incl : VLSM_incl (fixed_equivocation_vlsm_composition IM indices1) (fixed_equivocation_vlsm_composition IM indices2). -Proof. +Proof using Hincl. apply constraint_subsumption_incl. apply preloaded_constraint_subsumption_stronger. apply strong_constraint_subsumption_strongest. @@ -399,7 +401,7 @@ Context l m (Hv : input_valid Fixed l (s, Some m)) : strong_fixed_equivocation IM equivocators base_s m. -Proof. +Proof using Hobs_s_protocol. destruct Hv as [_ [_ [_ [Hobs | Hemit]]]]. - by apply Hobs_s_protocol. - right. @@ -424,7 +426,7 @@ Qed. (composite_label_sub_projection IM (elements equivocators) l e) (composite_state_sub_projection IM (elements equivocators) s, iom) (composite_state_sub_projection IM (elements equivocators) sf, oom). -Proof. +Proof using Hobs_s_protocol. destruct l as (i, li). simpl in *. repeat split. - done. @@ -453,7 +455,7 @@ Qed. l iom om (Ht : input_valid_transition Fixed l (s, iom) (sf, Some om)) : strong_fixed_equivocation IM equivocators base_s om. -Proof. +Proof using Hobs_s_protocol. destruct (decide (projT1 l ∈ elements equivocators)). - apply (fixed_input_valid_transition_sub_projection_helper Hs_pr _ e) in Ht. @@ -495,7 +497,7 @@ Lemma fixed_finite_valid_trace_sub_projection_helper (finite_trace_sub_projection IM (elements equivocators) tr) /\ forall m, composite_has_been_directly_observed IM s m -> strong_fixed_equivocation IM equivocators base_s m. -Proof. +Proof using H7. induction Htr using finite_valid_trace_init_to_rev_ind. - split. + apply finite_valid_trace_from_to_empty. @@ -559,7 +561,7 @@ Lemma fixed_finite_valid_trace_sub_projection is f tr (composite_state_sub_projection IM (elements equivocators) is) (composite_state_sub_projection IM (elements equivocators) f) (finite_trace_sub_projection IM (elements equivocators) tr). -Proof. +Proof using H7. apply fixed_finite_valid_trace_sub_projection_helper with (base_s := f) in Htr as Htr_pr. - split; [by apply Htr_pr |]. apply proj2 in Htr. @@ -578,7 +580,7 @@ Lemma fixed_directly_observed_has_strong_fixed_equivocation f m (Hobs : composite_has_been_directly_observed IM f m) : strong_fixed_equivocation IM equivocators f m. -Proof. +Proof using H7. apply (VLSM_incl_valid_state Fixed_incl_Preloaded) in Hf as Hfuture. apply in_futures_refl in Hfuture. apply valid_state_has_trace in Hf as [is [tr Htr]]. @@ -591,7 +593,7 @@ Lemma fixed_valid_state_sub_projection s f : valid_state_prop (equivocators_composition_for_sent IM equivocators f) (composite_state_sub_projection IM (elements equivocators) s). -Proof. +Proof using H7. destruct Hsf as [tr Htr]. apply finite_valid_trace_from_to_complete_left in Htr as [is [trs [Htr Hs]]]. apply fixed_finite_valid_trace_sub_projection in Htr as Hpr_tr. @@ -610,7 +612,7 @@ Lemma fixed_input_has_strong_fixed_equivocation l s m (Ht : input_valid Fixed l (s, Some m)) : strong_fixed_equivocation IM equivocators s m. -Proof. +Proof using H7. apply fixed_input_has_strong_fixed_equivocation_helper with (base_s := s) in Ht ; [done |]. by apply fixed_directly_observed_has_strong_fixed_equivocation, Ht. @@ -624,7 +626,7 @@ Lemma fixed_output_has_strong_fixed_equivocation l s iom sf om (Ht : input_valid_transition Fixed l (s, iom) (sf, Some om)) : strong_fixed_equivocation IM equivocators sf om. -Proof. +Proof using H7. apply input_valid_transition_origin in Ht as Hs. apply fixed_output_has_strong_fixed_equivocation_helper with s sf l iom. - intros m Hobs. apply in_futures_preserves_strong_fixed_equivocation with s. @@ -679,7 +681,7 @@ Lemma Equivocators_Fixed_Strong_incl base_s : VLSM_incl (equivocators_composition_for_directly_observed IM equivocators base_s) (equivocators_composition_for_sent IM equivocators base_s). -Proof. +Proof using H7. apply basic_VLSM_incl. - by intros s Hincl. - intros l s m Hv HsY [Hinit | Hobs] @@ -695,7 +697,7 @@ Lemma Equivocators_Fixed_Strong_eq base_s : VLSM_eq (equivocators_composition_for_directly_observed IM equivocators base_s) (equivocators_composition_for_sent IM equivocators base_s). -Proof. +Proof using H7. apply VLSM_eq_incl_iff. split. - by apply Equivocators_Fixed_Strong_incl. - by apply Equivocators_Strong_Fixed_incl. @@ -709,7 +711,7 @@ Lemma fixed_strong_equivocation_subsumption : input_valid_constraint_subsumption IM (fixed_equivocation_constraint IM equivocators) (strong_fixed_equivocation_constraint IM equivocators). -Proof. +Proof using H7. intros l (s, om) Hv. destruct om as [m |]; [| done]. apply proj1 in Hv as Hs. @@ -717,12 +719,12 @@ Proof. Qed. Lemma Fixed_incl_StrongFixed : VLSM_incl Fixed StrongFixed. -Proof. +Proof using H7. apply constraint_subsumption_incl. apply fixed_strong_equivocation_subsumption. Qed. Lemma Fixed_eq_StrongFixed : VLSM_eq Fixed StrongFixed. -Proof. +Proof using H7. apply VLSM_eq_incl_iff. split. - by apply Fixed_incl_StrongFixed. - by apply StrongFixed_incl_Fixed. @@ -878,7 +880,7 @@ Context Lemma fixed_equivocator_lifting_initial_state : weak_projection_initial_state_preservation EquivPreloadedBase Fixed (lift_sub_state_to IM (elements equivocators) base_s). -Proof. +Proof using Hbase_s H7. intros eqv_is Heqv_is. apply (VLSM_incl_valid_state (StrongFixed_incl_Fixed IM equivocators)). apply (VLSM_projection_valid_state (remove_equivocating_transitions_fixed_projection _ Heqv_is)). @@ -925,7 +927,7 @@ Lemma EquivPreloadedBase_Fixed_weak_embedding forall i m, i ∈ equivocators -> ~ vinitial_message_prop (IM i) m) : VLSM_weak_embedding EquivPreloadedBase Fixed (lift_sub_label IM (elements equivocators)) (lift_sub_state_to IM (elements equivocators) base_s). -Proof. +Proof using Hbase_s H7 H6 H4 H3 H2 H1 H0. apply basic_VLSM_weak_embedding. - intros l s om Hv HsY HomY. split. + destruct Hv as [_ [_ [Hv _]]]; revert Hv; destruct l as (i, li). @@ -985,7 +987,7 @@ Context Lemma strong_fixed_equivocation_no_equivocators : forall s m, strong_fixed_equivocation IM (@empty Ci _) s m <-> composite_has_been_sent IM s m. -Proof. +Proof using H6 H4 H3 H2 H1 H. intros s m. split. - intros [Hsent | Hemit]. @@ -1002,7 +1004,7 @@ Lemma strong_fixed_equivocation_constraint_no_equivocators : forall l som, strong_fixed_equivocation_constraint IM (@empty Ci _) l som <-> composite_no_equivocations IM l som. -Proof. +Proof using H6 H4 H3 H2 H1 H. intros. destruct som as (s, [m |]); [| done]. simpl. @@ -1014,7 +1016,7 @@ Qed. Lemma strong_fixed_equivocation_vlsm_composition_no_equivocators : VLSM_eq (strong_fixed_equivocation_vlsm_composition IM (@empty Ci _)) (composite_vlsm IM (composite_no_equivocations IM)). -Proof. +Proof using H6 H4 H3 H2 H1 H. apply VLSM_eq_incl_iff. split. - apply constraint_subsumption_incl. @@ -1032,7 +1034,7 @@ Qed. Lemma fixed_equivocation_vlsm_composition_no_equivocators : VLSM_eq (fixed_equivocation_vlsm_composition IM (@empty Ci _)) (composite_vlsm IM (composite_no_equivocations IM)). -Proof. +Proof using H7 H6 H4 H3 H2 H1 H. eapply VLSM_eq_trans. - by apply Fixed_eq_StrongFixed. - by apply strong_fixed_equivocation_vlsm_composition_no_equivocators. @@ -1070,7 +1072,7 @@ Lemma lift_strong_fixed_non_equivocating : VLSM_embedding StrongFixedNonEquivocating StrongFixed (lift_sub_label IM (elements non_equivocators)) (lift_sub_state IM (elements non_equivocators)). -Proof. +Proof using H6 H3 H EqDecision0. apply induced_sub_projection_lift. intros s1 s2 Heq l om. destruct om as [m |]; [| by itauto]. @@ -1107,7 +1109,7 @@ Lemma lift_fixed_non_equivocating : VLSM_embedding FixedNonEquivocating Fixed (lift_sub_label IM (elements non_equivocators)) (lift_sub_state IM (elements non_equivocators)). -Proof. +Proof using H6 H3 H EqDecision0. constructor. intros sX trX Htr. apply @@ -1124,7 +1126,7 @@ Lemma fixed_non_equivocating_projection_friendliness : projection_friendly_prop (induced_sub_projection_is_projection IM (elements non_equivocators) (fixed_equivocation_constraint IM equivocators)). -Proof. +Proof using H6 H3 H EqDecision0. apply induced_sub_projection_friendliness. by apply lift_fixed_non_equivocating. Qed. @@ -1140,7 +1142,7 @@ Lemma fixed_non_equivocating_traces_char is tr finite_valid_trace Fixed eis etr /\ composite_state_sub_projection IM (elements non_equivocators) eis = is /\ finite_trace_sub_projection IM (elements non_equivocators) etr = tr. -Proof. +Proof using H6 H3 H EqDecision0. apply (projection_friendly_trace_char (induced_sub_projection_is_projection _ _ _)). by apply fixed_non_equivocating_projection_friendliness. Qed. diff --git a/theories/VLSM/Core/Equivocation/FullNode.v b/theories/VLSM/Core/Equivocation/FullNode.v index 3bc1f81a..a1ac3fed 100644 --- a/theories/VLSM/Core/Equivocation/FullNode.v +++ b/theories/VLSM/Core/Equivocation/FullNode.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From VLSM.Core Require Import VLSM VLSMProjections Composition. From VLSM.Core Require Import Equivocation. +Set Default Proof Using "Type". + Section sec_full_node_constraint. Context @@ -95,7 +97,7 @@ Lemma node_generated_without_further_equivocation_weaken (m : message) (Hsmi : node_generated_without_further_equivocation s m i) : node_generated_without_further_equivocation_alt s m i. -Proof. +Proof using EqDecision0. destruct Hsmi as [si [Hsim Hsi]]. apply can_emit_iff. exists si. revert Hsim. @@ -112,7 +114,7 @@ Lemma full_node_condition_for_admissible_equivocators_subsumption : preloaded_constraint_subsumption IM full_node_condition_for_admissible_equivocators full_node_condition_for_admissible_equivocators_alt. -Proof. +Proof using EqDecision0. intros l (s, [m |]) [Hs [_ [_ Hc]]]; [| done]. destruct Hc as [Hno_equiv | Hfull]; [by left |]. right. diff --git a/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v b/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v index 829a8d1d..f604bcce 100644 --- a/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v +++ b/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v @@ -8,6 +8,8 @@ From VLSM.Core Require Import Equivocation.FixedSetEquivocation. From VLSM.Core Require Import Equivocation.TraceWiseEquivocation. From VLSM.Core Require Import Equivocation.WitnessedEquivocation. +Set Default Proof Using "Type". + (** * VLSM Limited Message Equivocation In this section we define the notion of limited (message-based) equivocation. @@ -64,7 +66,7 @@ Definition limited_equivocation_composite_vlsm : VLSM message := Lemma limited_equivocation_valid_state s : valid_state_prop limited_equivocation_composite_vlsm s -> LimitedEquivocationProp s. -Proof. +Proof using Hno_initial_equivocation H7 H6 H4 H3 H2 H1 H0 EqDecision1. intros Hs; apply valid_state_prop_iff in Hs as [[[is His] ->] | (l & [s' om'] & om & [(_ & _ & _ & Hv) Ht])]; simpl. - exists ∅. @@ -210,7 +212,7 @@ Context Lemma StrongFixed_valid_state_not_heavy s (Hs : valid_state_prop StrongFixed s) : tracewise_not_heavy s. -Proof. +Proof using Inj0 Hsender_safety Hlimited H7 H6 H4 H3 H. cut (tracewise_equivocating_validators s ⊆ eqv_validators). { intro Hincl; unfold tracewise_not_heavy, not_heavy. @@ -249,7 +251,7 @@ Proof. Qed. Lemma StrongFixed_incl_Limited : VLSM_incl StrongFixed Limited. -Proof. +Proof using Inj0 Hsender_safety Hlimited H7 H6 H4 H3 H. apply constraint_subsumption_incl. intros [i li] [s om] Hpv. unfold limited_equivocation_constraint. @@ -259,7 +261,7 @@ Proof. Qed. Lemma Fixed_incl_Limited : VLSM_incl Fixed Limited. -Proof. +Proof using Inj0 Hsender_safety Hlimited H7 H6 H4 H3 H. specialize (Fixed_eq_StrongFixed IM equivocators) as Heq. apply VLSM_eq_proj1 in Heq. @@ -318,7 +320,7 @@ Context Lemma traces_exhibiting_limited_equivocation_are_valid (Hsender_safety : sender_safety_alt_prop IM A sender) : forall s tr, fixed_limited_equivocation_prop s tr -> finite_valid_trace Limited s tr. -Proof. +Proof using Inj0 H7 H6 H4 H3 H. intros s tr [equivocators [Hlimited Htr]]. eapply VLSM_incl_finite_valid_trace; [| done]. by eapply Fixed_incl_Limited. @@ -343,7 +345,7 @@ Lemma traces_exhibiting_limited_equivocation_are_valid_rev finite_valid_trace_init_to (free_composite_vlsm IM) is s tr -> tracewise_not_heavy s -> fixed_limited_equivocation_prop is tr. -Proof. +Proof using H7 H6 H4 H3 H. intros is s tr Hstrong Htr Hnot_heavy. exists (equivocating_validators s). split; cycle 1. @@ -365,7 +367,7 @@ Lemma limited_traces_exhibiting_limited_equivocation_are_valid_rev (can_emit_signed : channel_authentication_prop IM A sender) : forall s tr, strong_trace_witnessing_equivocation_prop IM threshold A sender s tr (Cv := Cv) -> finite_valid_trace Limited s tr -> fixed_limited_equivocation_prop s tr. -Proof. +Proof using H7 H6 H4 H3 H. intros s tr Hstrong Htr. eapply traces_exhibiting_limited_equivocation_are_valid_rev; [done.. | |]. - apply valid_trace_add_default_last. @@ -390,7 +392,7 @@ Lemma limited_valid_state_has_trace_exhibiting_limited_equivocation (can_emit_signed : channel_authentication_prop IM A sender) : forall s, valid_state_prop Limited s -> exists is tr, finite_trace_last is tr = s /\ fixed_limited_equivocation_prop is tr. -Proof. +Proof using H7 H6 H4 H3 H. intros s Hs. assert (Hfree_s : valid_state_prop (free_composite_vlsm IM) s) by (revert Hs; apply VLSM_incl_valid_state, constraint_free_incl). diff --git a/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v b/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v index d6cd0e88..b1d374ff 100644 --- a/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v +++ b/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v @@ -3,6 +3,8 @@ From VLSM.Lib Require Import Preamble ListExtras StdppListSet StdppExtras NatExt From VLSM.Core Require Import VLSM Composition. From VLSM.Core Require Import Equivocation MessageDependencies TraceableVLSM. +Set Default Proof Using "Type". + (** * Minimally-equivocating traces In this module we define a [choice_function], [minimal_equivocation_choice], @@ -99,7 +101,7 @@ Lemma not_CompositeNthSentNotObserved_is_observed : ts !! n = Some (item, s) -> forall m, output item = Some m -> CompositeHasBeenObserved IM message_dependencies s m. -Proof. +Proof using full_message_dependencies H11 H EqDecision1. intros * Hnobs **. destruct (decide (CompositeHasBeenObserved IM message_dependencies s m)); [done |]. by contradict Hnobs; econstructor. @@ -115,7 +117,7 @@ Definition composite_latest_sent_not_observed_prop #[local] Instance composite_latest_sent_not_observed_dec s' : RelDecision (composite_latest_sent_not_observed_prop s'). -Proof. +Proof using full_message_dependencies H11 H. intros i n. destruct (composite_state_destructor IM state_destructor s' i !! n) as [[item s] |] eqn: Hdestruct; @@ -194,7 +196,7 @@ Qed. #[local] Instance latest_composite_observed_before_send_irreflexive s' : Irreflexive (latest_composite_observed_before_send s'). -Proof. +Proof using Irreflexive0. intros a (s_i & item_i & m_i & s_j & item_j & m_j & [Hdestruct Houtput H_destruct H_output Hrel]). rewrite Hdestruct in H_destruct; inversion H_destruct; subst; clear H_destruct. rewrite Houtput in H_output; inversion H_output; subst. @@ -210,7 +212,7 @@ Lemma composite_latest_sent_observed_in_before_send head (composite_state_destructor IM state_destructor s' j) = Some (item_j, s_j) -> output item_j = Some m_j -> latest_composite_observed_before_send s' i j. -Proof. +Proof using validator state_size sender full_message_dependencies Hchannel H13 H12 H11 A. intros Hs' Hdestruct_j Houtput_j. eapply composite_state_destructor_head_reachable in Hdestruct_j as Htj; [| done..]. destruct Hij as [Hdestruct_i Houtput_i Hobs]. @@ -273,7 +275,7 @@ Lemma traceable_vlsm_initial_state_dec : forall (i : index) (si : vstate (IM i)), valid_state_prop (pre_loaded_with_all_messages_vlsm (IM i)) si -> Decision (vinitial_state_prop (IM i) si). -Proof. +Proof using state_size state_destructor H13. intros; destruct (decide (state_destructor i si = nil)). - by left; apply tv_state_destructor_initial. - by right; contradict n; apply tv_state_destructor_initial. @@ -456,7 +458,7 @@ Lemma all_latest_composite_observed_before_send_one_step forall isj, is' !! j = Some isj -> forall isi, is' !! (S j) = Some isi -> latest_composite_observed_before_send s isi isj. -Proof. +Proof using validator state_size sender full_message_dependencies Hchannel H13 H12 H11 A. intros Hall j isj Hisj isi Hisi. eapply ForAllSuffix2_lookup in Hisj as Hobs_j; [| done..]. destruct Hobs_j as (s_isi & item_isi & m_isi & Hobs_j). @@ -483,7 +485,7 @@ Lemma all_latest_composite_observed_before_send forall isi, is' !! i = Some isi -> forall isj, is' !! j = Some isj -> latest_composite_observed_before_send s isi isj. -Proof. +Proof using validator state_size sender full_message_dependencies Hchannel H13 H12 H11 A. intros Hall i j Hij; unfold gt, lt in Hij; remember (S j) as k. revert j Heqk; induction Hij; intros j -> isi Hisi isj Hisj. - by eapply all_latest_composite_observed_before_send_one_step. @@ -530,7 +532,7 @@ Lemma at_least_one_send_not_previously_observed find_not_send_decomposition s' is = None -> find_sent_not_observed_decomposition s' is = None -> False. -Proof. +Proof using validator sender Irreflexive0 Hchannel H12 A. intros Hinitial Hnot_send Hsent_not_obs. assert (Hall_sent_observed : forall x : index, x ∈ is -> @@ -592,7 +594,7 @@ Lemma minimal_equivocation_choice_monotone : forall v : validator, msg_dep_is_globally_equivocating IM message_dependencies sender s v -> msg_dep_is_globally_equivocating IM message_dependencies sender s' v. -Proof. +Proof using Irreflexive0 Hchannel H12 A. intros is Hnodup s' Hs' Hnis i Hi n Hchoice s item Hdestruct v [m []]. eapply composite_state_destructor_lookup_reachable in Hdestruct as Ht; [| typeclasses eauto | done]. @@ -692,7 +694,7 @@ Lemma state_to_minimal_equivocation_trace_equivocation_monotonic : (finite_trace_last is pre) v -> msg_dep_is_globally_equivocating IM message_dependencies sender (destination item) v. -Proof. +Proof using Irreflexive0 Hchannel H12 A. intros. eapply composite_state_to_trace_P_monotonic with (P := fun s => msg_dep_is_globally_equivocating IM message_dependencies sender s v); diff --git a/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v b/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v index 55bf69d8..07c5c6e7 100644 --- a/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v +++ b/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v @@ -4,6 +4,8 @@ From VLSM.Lib Require Import Preamble. From VLSM.Core Require Import VLSM MessageDependencies VLSMProjections Composition Equivocation. From VLSM.Core Require Import Equivocation.FixedSetEquivocation ProjectionTraces SubProjectionTraces. +Set Default Proof Using "Type". + Section sec_msg_dep_fixed_set_equivocation. Context @@ -48,7 +50,7 @@ Lemma messages_with_valid_dependences_can_be_emitted s dm (Hdm_i : dm_i ∈ equivocators) (Hemitted : can_emit (pre_loaded_with_all_messages_vlsm (IM dm_i)) dm) : can_emit (equivocators_composition_for_sent IM equivocators s) dm. -Proof. +Proof using Irreflexive0 H9 H8 H18 H17 H14 H12 H11 H10. eapply sub_valid_preloaded_lifts_can_be_emitted, message_dependencies_are_sufficient. - by apply elem_of_elements, Hdm_i. - by apply Hdepm. @@ -73,7 +75,7 @@ Lemma dependencies_are_valid s m forall dm, msg_dep_rel message_dependencies dm m -> valid_message_prop (equivocators_composition_for_sent IM equivocators s) dm. -Proof. +Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10. induction m as [m Hind] using (well_founded_ind Hmsg_dep_happens_before_wf). intros Heqv dm Hdm. apply emitted_messages_are_valid_iff. @@ -93,7 +95,7 @@ Lemma msg_dep_strong_fixed_equivocation_subsumption s m (Hmsg_dep_happens_before_wf : well_founded (msg_dep_happens_before message_dependencies)) : msg_dep_fixed_set_equivocation s m -> strong_fixed_equivocation IM equivocators s m. -Proof. +Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10. intros [Hsent | [[i [Hi Hemit]] Heqv]]; [by left |]. cut (forall dm, msg_dep_rel message_dependencies dm m -> valid_message_prop (equivocators_composition_for_sent IM equivocators s) dm) @@ -108,7 +110,7 @@ Lemma msg_dep_strong_fixed_equivocation_constraint_subsumption : strong_constraint_subsumption IM msg_dep_fixed_set_equivocation_constraint (strong_fixed_equivocation_constraint IM equivocators). -Proof. +Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10. intros l [s [m |]] Hc; [| done]. by apply msg_dep_strong_fixed_equivocation_subsumption. Qed. @@ -172,7 +174,7 @@ Lemma sent_by_non_equivocating_msg_dep_rel_strong_fixed_equivocation forall dm m, msg_dep_rel message_dependencies dm m -> sent_by_non_equivocating IM equivocators s m -> strong_fixed_equivocation IM equivocators s dm. -Proof. +Proof using Irreflexive0 H18 H17. intros s Hs dm m Hdm (i & Hni & Hsent). apply (messages_sent_from_component_produced_previously IM Hs) in Hsent as (destination & Hfutures & Hproduce). @@ -206,7 +208,7 @@ Lemma msg_dep_rel_reflects_strong_fixed_equivocation forall dm m, msg_dep_rel message_dependencies dm m -> strong_fixed_equivocation IM equivocators s m -> strong_fixed_equivocation IM equivocators s dm. -Proof. +Proof using Irreflexive0 H18 H17. intros s Hs dm m Hdm [Hsent | Hemit]. - by eapply sent_by_non_equivocating_msg_dep_rel_strong_fixed_equivocation. - cut (valid_message_prop (equivocators_composition_for_sent IM equivocators s) dm). @@ -235,7 +237,7 @@ Lemma strong_fixed_equivocation_msg_dep_constraint_subsumption : input_valid_constraint_subsumption IM (strong_fixed_equivocation_constraint IM equivocators) msg_dep_fixed_set_equivocation_constraint. -Proof. +Proof using Irreflexive0 H18 H17. intros l [s [m |]] (Hs & _ & _ & Hc); [| done]. cut (dependencies_with_non_equivocating_senders_were_sent s m). { @@ -259,7 +261,7 @@ Lemma msg_dep_strong_fixed_equivocation_incl : VLSM_incl (composite_vlsm IM msg_dep_fixed_set_equivocation_constraint) (composite_vlsm IM (strong_fixed_equivocation_constraint IM equivocators)). -Proof. +Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10. apply constraint_subsumption_incl. apply preloaded_constraint_subsumption_stronger. apply strong_constraint_subsumption_strongest. @@ -271,7 +273,7 @@ Lemma strong_msg_dep_fixed_equivocation_incl : VLSM_incl (composite_vlsm IM (strong_fixed_equivocation_constraint IM equivocators)) (composite_vlsm IM msg_dep_fixed_set_equivocation_constraint). -Proof. +Proof using Irreflexive0 H18 H17. apply constraint_subsumption_incl. by apply strong_fixed_equivocation_msg_dep_constraint_subsumption. Qed. @@ -282,7 +284,7 @@ Lemma msg_dep_strong_fixed_equivocation_eq : VLSM_eq (composite_vlsm IM msg_dep_fixed_set_equivocation_constraint) (composite_vlsm IM (strong_fixed_equivocation_constraint IM equivocators)). -Proof. +Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10. apply VLSM_eq_incl_iff; split. - by apply msg_dep_strong_fixed_equivocation_incl. - by apply strong_msg_dep_fixed_equivocation_incl. @@ -323,7 +325,7 @@ Lemma msg_dep_full_node_fixed_set_equivocation_constraint_subsumption : strong_constraint_subsumption IM (msg_dep_fixed_set_equivocation_constraint IM message_dependencies equivocators) full_node_fixed_set_equivocation_constraint. -Proof. +Proof using H6 H4 H3 H2 H1 H0 EqDecision0. intros l [s [m |]]; [| done] ; intros [Hsent | [[i [Hi Hemit]] Hdeps]]; [by left | right]. apply Hchannel in Hemit; cbv in Hemit |- *. @@ -345,7 +347,7 @@ Lemma fixed_full_node_equivocation_incl : VLSM_incl (composite_vlsm IM (fixed_equivocation_constraint IM equivocators)) (composite_vlsm IM full_node_fixed_set_equivocation_constraint). -Proof. +Proof using no_initial_messages_in_IM message_dependencies Irreflexive0 H9 H7 H6 H4 H3 H2 H18 H16 H15 H14 H13 H12 H11 H10 H1 H0 EqDecision1 Cm. eapply VLSM_incl_trans. - by apply Fixed_incl_StrongFixed. - eapply VLSM_incl_trans. @@ -363,7 +365,7 @@ Lemma full_node_fixed_equivocation_constraint_subsumption : input_valid_constraint_subsumption IM full_node_fixed_set_equivocation_constraint (fixed_equivocation_constraint IM equivocators). -Proof. +Proof using no_initial_messages_in_IM Irreflexive0 H6 H4 H3 H2 H18 H1 H0. intros l [s [m |]] (_ & Hm & Hv & Hc); [| itauto] ; destruct Hc as [Hsent | Heqv]; [left | right]. - by revert Hsent; apply sent_by_non_equivocating_are_directly_observed. @@ -406,7 +408,7 @@ Lemma full_node_fixed_equivocation_incl : VLSM_incl (composite_vlsm IM full_node_fixed_set_equivocation_constraint) (composite_vlsm IM (fixed_equivocation_constraint IM equivocators)). -Proof. +Proof using no_initial_messages_in_IM Irreflexive0 H6 H4 H3 H2 H18 H1 H0. apply constraint_subsumption_incl. by apply full_node_fixed_equivocation_constraint_subsumption. Qed. @@ -417,7 +419,7 @@ Lemma full_node_fixed_equivocation_eq : VLSM_eq (composite_vlsm IM full_node_fixed_set_equivocation_constraint) (composite_vlsm IM (fixed_equivocation_constraint IM equivocators)). -Proof. +Proof using no_initial_messages_in_IM Irreflexive0 H7 H6 H4 H3 H2 H18 H1 H0. apply VLSM_eq_incl_iff; split. - apply full_node_fixed_equivocation_incl; [done |]. by apply channel_authentication_sender_safety. diff --git a/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v b/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v index 61200887..3758d36c 100644 --- a/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v +++ b/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v @@ -10,6 +10,8 @@ From VLSM.Core Require Import Equivocation.LimitedMessageEquivocation. From VLSM.Core Require Import Equivocation.MsgDepFixedSetEquivocation. From VLSM.Core Require Import Equivocation.TraceWiseEquivocation. +Set Default Proof Using "Type". + (** To allow capturing the two models of limited equivocation described in the sections below, we first define a notion of limited equivocation parameterized @@ -72,7 +74,7 @@ Definition coeqv_annotate_trace_with_equivocators := Lemma coeqv_limited_equivocation_transition_state_annotation_incl [l s iom s' oom] : vtransition coeqv_limited_equivocation_vlsm l (s, iom) = (s', oom) -> state_annotation s ⊆ state_annotation s'. -Proof. +Proof using H7 H5 H4 EqDecision1. cbn; unfold annotated_transition; destruct (vtransition _ _ _) as (_s', _om'). inversion 1; cbn. by destruct iom as [m |]; [apply union_subseteq_l |]. @@ -81,7 +83,7 @@ Qed. Lemma coeqv_limited_equivocation_state_annotation_nodup s : valid_state_prop coeqv_limited_equivocation_vlsm s -> NoDup (elements (state_annotation s)). -Proof. +Proof using H7 H5 H4 H0 EqDecision1. induction 1 using valid_state_prop_ind. - by destruct s, Hs as [_ ->]; cbn in *; apply NoDup_elements. - destruct Ht as [_ Ht]; cbn in Ht. @@ -92,7 +94,7 @@ Qed. Lemma coeqv_limited_equivocation_state_not_heavy s : valid_state_prop coeqv_limited_equivocation_vlsm s -> (sum_weights (state_annotation s) <= threshold)%R. -Proof. +Proof using H8 H7 H5 H4 H0 EqDecision1. induction 1 using valid_state_prop_ind. - destruct s, Hs as [_ ->]; cbn in *. rewrite sum_weights_empty; [| done]. @@ -235,7 +237,7 @@ Context Lemma full_node_msg_dep_coequivocating_senders s m i li (Hvalid : input_valid (pre_loaded_with_all_messages_vlsm (IM i)) li (s i, Some m)) : msg_dep_coequivocating_senders IM full_message_dependencies sender s m ≡@{Cv} ∅. -Proof. +Proof using message_dependencies Hfull H6 H4 H3 H19 H17 H16 H15 H14 H FullMessageDependencies0 EqDecision2 EqDecision0. intro; split; intro Hx; [| by contradict Hx; apply not_elem_of_empty]. exfalso; contradict Hx. unfold msg_dep_coequivocating_senders. @@ -273,7 +275,7 @@ Lemma full_node_msg_dep_composite_transition_message_equivocators msg_dep_composite_transition_message_equivocators IM full_message_dependencies sender (existT i li) (s, om). -Proof. +Proof using message_dependencies Hfull H6 H4 H3 H19 H17 H15 H14 H FullMessageDependencies0 EqDecision2 EqDecision0. destruct om as [m |]; cbn; [| done]. apply sets.union_proper; [done |]. unfold coeqv_message_equivocators, msg_dep_coequivocating_senders. @@ -288,7 +290,7 @@ Lemma msg_dep_full_node_valid_iff (Hvi : input_valid (pre_loaded_with_all_messages_vlsm (IM (projT1 l))) (projT2 l) (original_state s (projT1 l), om)) : vvalid Limited l (s, om) <-> vvalid FullNodeLimited l (s, om). -Proof. +Proof using message_dependencies Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0. cbn; unfold annotated_valid, coeqv_limited_equivocation_constraint; destruct l as [i li]. replace (sum_weights _) with (sum_weights @@ -304,7 +306,7 @@ Lemma msg_dep_full_node_transition_iff (Hvi : input_valid (pre_loaded_with_all_messages_vlsm (IM (projT1 l))) (projT2 l) (original_state s (projT1 l), om)) : vtransition Limited l (s, om) = vtransition FullNodeLimited l (s, om). -Proof. +Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0. cbn; unfold annotated_transition; destruct (vtransition _ _ _) as (s', om'), l as (i, li). do 2 f_equal. @@ -315,7 +317,7 @@ Qed. Lemma msg_dep_full_node_limited_equivocation_vlsm_incl : VLSM_incl Limited FullNodeLimited. -Proof. +Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0. apply basic_VLSM_incl. - by intros s Hs. - by intros _ _ m _ _ Hinit; apply initial_message_is_valid. @@ -329,7 +331,7 @@ Qed. Lemma full_node_msg_dep_limited_equivocation_vlsm_incl : VLSM_incl FullNodeLimited Limited. -Proof. +Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0. apply basic_VLSM_incl. - by intros s Hs. - by intros _ _ m _ _ Hinit; apply initial_message_is_valid. @@ -343,7 +345,7 @@ Qed. Lemma full_node_msg_dep_limited_equivocation_vlsm_eq : VLSM_eq FullNodeLimited Limited. -Proof. +Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0. apply VLSM_eq_incl_iff; split. - by apply full_node_msg_dep_limited_equivocation_vlsm_incl. - by apply msg_dep_full_node_limited_equivocation_vlsm_incl. @@ -385,7 +387,7 @@ Lemma equivocating_messages_are_equivocator_emitted v ∈ msg_dep_message_equivocators IM full_message_dependencies sender s im (Cv := Cv) /\ can_emit (pre_loaded_vlsm (IM (A v)) (fun dm => msg_dep_rel message_dependencies dm im)) im. -Proof. +Proof using Hchannel H26 H24 H23 H18 FullMessageDependencies0 EqDecision2. eapply (VLSM_incl_can_emit (vlsm_incl_pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))) in Him. apply can_emit_composite_project in Him as [j Him]. @@ -410,7 +412,7 @@ Lemma equivocating_messages_dependencies_are_directly_observed_or_equivocator_em composite_has_been_directly_observed IM s dm \/ exists v_i, v_i ∈ msg_dep_message_equivocators IM full_message_dependencies sender s im (Cv := Cv) /\ can_emit (pre_loaded_with_all_messages_vlsm (IM (A v_i))) dm. -Proof. +Proof using no_initial_messages_in_IM Hchannel H26 H24 H23 H18 FullMessageDependencies0 EqDecision2. intros dm Hdm. destruct (decide (composite_has_been_directly_observed IM s dm)) as [Hobs | Hnobs] ; [by left | right]. @@ -444,7 +446,7 @@ Lemma message_equivocators_can_emit (s : vstate Limited) im (original_state s) im)) (original_state s)) im. -Proof. +Proof using no_initial_messages_in_IM message_dependencies Hsender_safety Hchannel H8 H6 H4 H3 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1. eapply VLSM_embedding_can_emit. - unshelve apply equivocators_composition_for_directly_observed_index_incl_embedding with (indices1 := fin_sets.set_map A (msg_dep_message_equivocators IM (Cv := Cv) @@ -487,7 +489,7 @@ Lemma msg_dep_fixed_limited_equivocation_witnessed (pre_VLSM_embedding_finite_trace_project (type Limited) (composite_type IM) Datatypes.id original_state tr). -Proof. +Proof using no_initial_messages_in_IM message_dependencies Hsender_safety Hchannel H8 H6 H4 H3 H27 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1. repeat split; [.. | by apply Htr]. - by eapply coeqv_limited_equivocation_state_not_heavy, finite_valid_trace_last_pstate, Htr. @@ -581,7 +583,7 @@ Corollary msg_dep_fixed_limited_equivocation is tr (pre_VLSM_embedding_finite_trace_project (type Limited) (composite_type IM) Datatypes.id original_state tr) (Ci := Ci) (Cv := Cv). -Proof. +Proof using no_initial_messages_in_IM message_dependencies Hsender_safety Hchannel H8 H6 H4 H3 H27 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1. intro Htr. exists (state_annotation (finite_trace_last is tr)). by apply msg_dep_fixed_limited_equivocation_witnessed. @@ -614,7 +616,7 @@ Lemma fixed_transition_preserves_annotation_equivocators (msg_dep_composite_transition_message_equivocators IM full_message_dependencies sender) {| original_state := is; state_annotation := empty_set |} tr), iom) ⊆ eqv_validators. -Proof. +Proof using no_initial_messages_in_IM message_dependencies Inj0 Hsender_safety Hchannel H8 H6 H4 H3 H26 H24 H23 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1. destruct iom as [im |]; [| done]. apply ListFinSetExtras.set_union_subseteq_iff; split; [done | cbn]. rewrite annotate_trace_from_last_original_state; cbn. @@ -672,7 +674,7 @@ Lemma msg_dep_limited_fixed_equivocation finite_valid_trace Limited {| original_state := is; state_annotation := ` inhabitant |} (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender is tr). -Proof. +Proof using no_initial_messages_in_IM message_dependencies Inj0 Hsender_safety Hchannel H8 H6 H4 H3 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1. intros (equivocators & Hlimited & Htr). split; [| by split; [apply Htr |]]. apply valid_trace_add_default_last in Htr. @@ -733,7 +735,7 @@ Lemma annotated_limited_incl_constrained_limited Limited (tracewise_limited_equivocation_vlsm_composition IM threshold A sender (Cv := Cv)) Datatypes.id original_state. -Proof. +Proof using no_initial_messages_in_IM message_dependencies Inj0 Hsender_safety Hchannel H8 H6 H5 H4 H3 H2 H18 H15 H13 H12 H1 H0 H FullMessageDependencies0 EqDecision1 Ci. constructor; intros sX trX HtrX. eapply @traces_exhibiting_limited_equivocation_are_valid; [done.. | |]. - by apply Hsender_safety. diff --git a/theories/VLSM/Core/Equivocation/NoEquivocation.v b/theories/VLSM/Core/Equivocation/NoEquivocation.v index 3b89a5d7..71dfd06d 100644 --- a/theories/VLSM/Core/Equivocation/NoEquivocation.v +++ b/theories/VLSM/Core/Equivocation/NoEquivocation.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble. From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation. +Set Default Proof Using "Type". + (** * VLSM No Equivocation Composition Constraints *) Section sec_no_equivocations. @@ -84,7 +86,7 @@ Lemma directly_observed_were_sent_preserved l s im s' om : input_valid_transition X l (s, im) (s', om) -> directly_observed_were_sent s -> directly_observed_were_sent s'. -Proof. +Proof using Henforced. intros Hptrans Hprev msg Hobs. specialize (Hprev msg). apply preloaded_weaken_input_valid_transition in Hptrans. @@ -105,7 +107,7 @@ Qed. Lemma directly_observed_were_sent_invariant s: valid_state_prop X s -> directly_observed_were_sent s. -Proof. +Proof using Henforced. intro Hproto. induction Hproto using valid_state_prop_ind. - by apply directly_observed_were_sent_initial. @@ -122,7 +124,7 @@ Lemma no_equivocations_preloaded_traces (is : state) (tr : list transition_item) : finite_valid_trace (pre_loaded_with_all_messages_vlsm X) is tr -> finite_valid_trace X is tr. -Proof. +Proof using Henforced H0 H. intro Htr. induction Htr using finite_valid_trace_rev_ind. - split; [| done]. @@ -142,7 +144,7 @@ Qed. Lemma preloaded_incl_no_equivocations : VLSM_incl (pre_loaded_with_all_messages_vlsm X) X. -Proof. +Proof using Henforced H0 H. specialize no_equivocations_preloaded_traces. clear -X. destruct X as [T [S M]]. by apply VLSM_incl_finite_traces_characterization. @@ -150,7 +152,7 @@ Qed. Lemma preloaded_eq_no_equivocations : VLSM_eq (pre_loaded_with_all_messages_vlsm X) X. -Proof. +Proof using Henforced H0 H. specialize preloaded_incl_no_equivocations. specialize (vlsm_incl_pre_loaded_with_all_messages_vlsm X). clear -X. destruct X as [T [S M]]. @@ -215,7 +217,7 @@ Definition composite_directly_observed_were_sent (s : state) : Prop := Lemma composite_directly_observed_were_sent_invariant s : valid_state_prop X s -> composite_directly_observed_were_sent s. -Proof. +Proof using Hsubsumed H. intros Hs m. rewrite composite_has_been_directly_observed_sent_received_iff. intros Hobs. diff --git a/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v b/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v index c721c158..3d577ff4 100644 --- a/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v +++ b/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v @@ -6,6 +6,8 @@ From VLSM.Core Require Import VLSM Composition ProjectionTraces. From VLSM.Core Require Import Equivocation. From VLSM.Lib Require Import Preamble StdppExtras. +Set Default Proof Using "Type". + (** * VLSM Trace-wise Equivocation In this section we define a more precise notion of message equivocation, @@ -46,7 +48,7 @@ Definition item_equivocating_in_trace := from_option (fun m => ~ trace_has_message (field_selector output) m tr) False (input item). #[local] Instance item_equivocating_in_trace_dec : RelDecision item_equivocating_in_trace. -Proof. +Proof using EqDecision0. intros item tr. destruct item. destruct input as [m |]; [| by right; itauto]. unfold item_equivocating_in_trace, trace_has_message, field_selector; cbn. @@ -126,7 +128,7 @@ Qed. Lemma equivocating_senders_in_trace_prefix prefix suffix : equivocating_senders_in_trace prefix ⊆ equivocating_senders_in_trace (prefix ++ suffix). -Proof. +Proof using PreFree EqDecision1. intros v. rewrite !elem_of_equivocating_senders_in_trace. intros [m [Hm Heqv]]. exists m. split; [done |]. @@ -226,7 +228,7 @@ Lemma transition_is_equivocating_tracewise_char : is_equivocating_tracewise_no_has_been_sent s' v -> is_equivocating_tracewise_no_has_been_sent s v \/ option_bind _ _ sender om = Some v. -Proof. +Proof using EqDecision4. destruct (decide (option_bind _ _ sender om = Some v)) ; [by intro; right |]. intros Heqv. left. intros is tr [Htr Hinit]. @@ -249,7 +251,7 @@ Lemma transition_receiving_no_sender_reflects_is_equivocating_tracewise (Hno_sender : option_bind _ _ sender om = None) (v : validator) : is_equivocating_tracewise_no_has_been_sent s' v -> is_equivocating_tracewise_no_has_been_sent s v. -Proof. +Proof using EqDecision4. intro Hs'. by destruct (transition_is_equivocating_tracewise_char _ _ _ _ _ Ht v Hs'); [| congruence]. Qed. diff --git a/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v b/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v index faf5343c..b3848208 100644 --- a/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v +++ b/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v @@ -5,6 +5,8 @@ From VLSM.Core Require Import VLSM VLSMProjections Composition. From VLSM.Core Require Import SubProjectionTraces MessageDependencies Equivocation. From VLSM.Core Require Import NoEquivocation FixedSetEquivocation TraceWiseEquivocation. +Set Default Proof Using "Type". + (** * Witnessed equivocation Although [is_equivocating_tracewise] provides a very precise notion of @@ -361,7 +363,7 @@ Lemma strong_trace_witnessing_equivocation_prop_extend_eq (Hwitness : trace_witnessing_equivocation_prop is (tr' ++ [item])) (Heq : equivocating_validators s ≡@{Cv} equivocating_validators (destination item)) : strong_trace_witnessing_equivocation_prop is' (tr'' ++ [item]). -Proof. +Proof using H0 H. intros prefix suffix Heq_tr''_item. destruct_list_last suffix suffix' sitem Hsuffix_eq. - rewrite app_nil_r in Heq_tr''_item. @@ -475,7 +477,7 @@ Lemma preloaded_has_strong_trace_witnessing_equivocation_prop s : exists is' tr', finite_valid_trace_init_to PreFree is' s tr' /\ strong_trace_witnessing_equivocation_prop is' tr'. -Proof. +Proof using Hke H0 H. apply is_equivocating_tracewise_witness in Hs. destruct Hs as [is [tr [Htr Hwitness]]]. apply finite_valid_trace_init_to_last in Htr as Hlst. @@ -600,7 +602,7 @@ Lemma free_has_strong_trace_witnessing_equivocation_prop s : exists is' tr', finite_valid_trace_init_to Free is' s tr' /\ strong_trace_witnessing_equivocation_prop is' tr'. -Proof. +Proof using Hke H1 H0 H. apply (VLSM_incl_valid_state (vlsm_incl_pre_loaded_with_all_messages_vlsm Free)) in Hs as Hpre_s. apply preloaded_has_strong_trace_witnessing_equivocation_prop in Hpre_s. @@ -683,7 +685,7 @@ Lemma equivocators_can_emit_free m : can_emit (equivocators_composition_for_directly_observed IM (Ci := Ci) (fin_sets.set_map A (equivocating_validators sf)) s) m. -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H6 H4 H3 H29 H28 H27 H26 H25 H24 H23 H22 H21 H EqDecision3 Cm. apply emitted_messages_are_valid_iff in Hmsg as [(_v & [_im Him] & Heqim) | Hiom] ; [by elim (no_initial_messages_in_IM _v _im) |]. @@ -730,7 +732,7 @@ Lemma strong_witness_has_fixed_equivocation is s tr (Heqv : strong_trace_witnessing_equivocation_prop (Cv := Cv) IM threshold A sender is tr) : finite_valid_trace_init_to (fixed_equivocation_vlsm_composition IM (Ci := Ci) (fin_sets.set_map A (equivocating_validators s))) is s tr. -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H7 H6 H4 H3 H29 H28 H27 H26 H25 H24 H23 H22 H21 H Free_has_sender EqDecision3 Cm. split; [| by apply Htr]. induction Htr using finite_valid_trace_init_to_rev_ind. - eapply (finite_valid_trace_from_to_empty (fixed_equivocation_vlsm_composition IM @@ -814,7 +816,7 @@ Lemma equivocating_validators_fixed_equivocation_characterization valid_state_prop Free s -> valid_state_prop (composite_vlsm IM (equivocating_validators_fixed_equivocation_constraint s)) s. -Proof. +Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H7 H6 H4 H3 H29 H28 H27 H26 H25 H24 H23 H22 H21 H Free_has_sender EqDecision3 Cm. intros s Hs. destruct (free_has_strong_trace_witnessing_equivocation_prop IM threshold A sender _ s Hs) diff --git a/theories/VLSM/Core/EquivocationProjections.v b/theories/VLSM/Core/EquivocationProjections.v index 1d096881..75853c5e 100644 --- a/theories/VLSM/Core/EquivocationProjections.v +++ b/theories/VLSM/Core/EquivocationProjections.v @@ -3,6 +3,8 @@ From VLSM.Lib Require Import Preamble. From VLSM.Core Require Import VLSM Equivocation. From VLSM.Core Require Import Composition VLSMProjections Validator ProjectionTraces. +Set Default Proof Using "Type". + (** * VLSM projections and messages properties In this section we show that messages properties (oracles like [has_been_sent], @@ -45,7 +47,7 @@ Lemma VLSM_projection_oracle_reflect (HstepwiseY : oracle_stepwise_props (vlsm := Y) selectorY oracleY) : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, oracleY (state_project s) m -> oracleX s m. -Proof. +Proof using label_project Hsimul Hselector. intros s Hs m Hm. apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseX _ Hs m). intros isX trX HtrX. @@ -74,7 +76,7 @@ Lemma VLSM_projection_has_been_sent_reflect `{HasBeenSentCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_sent Y (state_project s) m -> has_been_sent X s m. -Proof. +Proof using label_project Hsimul. apply VLSM_projection_oracle_reflect with (field_selector output) (field_selector output). - by intros [] [] **; cbn in *; subst. - by apply (has_been_sent_stepwise_props X). @@ -86,7 +88,7 @@ Lemma VLSM_projection_has_been_received_reflect `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_received Y (state_project s) m -> has_been_received X s m. -Proof. +Proof using label_project Hsimul. apply VLSM_projection_oracle_reflect with (field_selector input) (field_selector input). - by intros [] [] **; cbn in *; subst. - by apply (has_been_received_stepwise_props X). @@ -100,7 +102,7 @@ Lemma VLSM_projection_has_been_directly_observed_reflect `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_directly_observed Y (state_project s) m -> has_been_directly_observed X s m. -Proof. +Proof using label_project Hsimul. apply VLSM_projection_oracle_reflect with item_sends_or_receives item_sends_or_receives. - by intros [] [] **; cbn in *; subst. - by apply has_been_directly_observed_stepwise_props. @@ -135,7 +137,7 @@ Lemma VLSM_weak_embedding_selected_message_exists_in_some_preloaded_traces s m : selected_message_exists_in_some_preloaded_traces X selectorX s m -> selected_message_exists_in_some_preloaded_traces Y selectorY (state_project s) m. -Proof. +Proof using label_project Hsimul Hselector. intros [is [tr [Htr Hm]]]. destruct Htr as [Htr His]. apply (VLSM_weak_embedding_finite_valid_trace_from_to Hsimul) in Htr. @@ -163,7 +165,7 @@ Lemma VLSM_weak_embedding_oracle (HoracleY_dec : RelDecision oracleY) : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, oracleX s m -> oracleY (state_project s) m. -Proof. +Proof using label_project Hsimul Hselector. intros s Hs m Hm. apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseX _ Hs m) in Hm. apply (selected_messages_consistency_prop_from_stepwise _ _ _ _ HstepwiseX HoracleX_dec _ Hs) in Hm. @@ -180,7 +182,7 @@ Lemma VLSM_weak_embedding_has_been_sent `{HasBeenSentCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_sent X s m -> has_been_sent Y (state_project s) m. -Proof. +Proof using label_project Hsimul. apply VLSM_weak_embedding_oracle with (field_selector output) (field_selector output). - by intros [] [] Hin Hout; cbn in *; subst. - by apply (has_been_sent_stepwise_props X). @@ -194,7 +196,7 @@ Lemma VLSM_weak_embedding_has_been_received `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_received X s m -> has_been_received Y (state_project s) m. -Proof. +Proof using label_project Hsimul. apply VLSM_weak_embedding_oracle with (field_selector input) (field_selector input). - by intros [] [] Hin Hout; cbn in *; subst. - by apply (has_been_received_stepwise_props X). @@ -210,7 +212,7 @@ Lemma VLSM_weak_embedding_has_been_directly_observed `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_directly_observed X s m -> has_been_directly_observed Y (state_project s) m. -Proof. +Proof using label_project Hsimul. apply VLSM_weak_embedding_oracle with item_sends_or_receives item_sends_or_receives. - by intros [] [] **; cbn in *; subst. - by apply has_been_directly_observed_stepwise_props. @@ -301,7 +303,7 @@ Lemma VLSM_incl_has_been_sent `{HasBeenSentCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_sent X s m -> has_been_sent Y s m. -Proof. +Proof using Hincl. intros s Hs m Hm. by eapply (@VLSM_embedding_has_been_sent _ X Y _ _ @@ -313,7 +315,7 @@ Lemma VLSM_incl_has_been_received `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_received X s m -> has_been_received Y s m. -Proof. +Proof using Hincl. intros s Hs m Hm. by eapply (@VLSM_embedding_has_been_received _ X Y _ _ @@ -327,7 +329,7 @@ Lemma VLSM_incl_has_been_directly_observed `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_directly_observed X s m -> has_been_directly_observed Y s m. -Proof. +Proof using Hincl. intros s Hs m Hm. by eapply (@VLSM_embedding_has_been_directly_observed _ X Y _ _ @@ -339,7 +341,7 @@ Lemma VLSM_incl_has_been_sent_reflect `{HasBeenSentCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_sent Y s m -> has_been_sent X s m. -Proof. +Proof using Hincl. intros s Hs m Hm. by eapply (@VLSM_embedding_has_been_sent_reflect _ X Y _ _ @@ -351,7 +353,7 @@ Lemma VLSM_incl_has_been_received_reflect `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_received Y s m -> has_been_received X s m. -Proof. +Proof using Hincl. intros s Hs m Hm. by eapply (@VLSM_embedding_has_been_received_reflect _ X Y _ _ @@ -365,7 +367,7 @@ Lemma VLSM_incl_has_been_directly_observed_reflect `{HasBeenReceivedCapability message Y} : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s -> forall m, has_been_directly_observed Y s m -> has_been_directly_observed X s m. -Proof. +Proof using Hincl. intros s Hs m Hm. by eapply (@VLSM_embedding_has_been_directly_observed_reflect _ X Y _ _ @@ -393,7 +395,7 @@ Lemma same_IM_composite_has_been_sent_preservation s1 m (Hs1 : valid_state_prop (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM1)) s1) : composite_has_been_sent IM1 s1 m -> composite_has_been_sent IM2 (same_IM_state_rew Heq s1) m. -Proof. +Proof using H. specialize (same_IM_preloaded_free_embedding IM1 IM2 Heq) as Hproj. intros Hbs1_m. by specialize (VLSM_embedding_has_been_sent Hproj _ Hs1 m Hbs1_m). @@ -424,7 +426,7 @@ Context *) Lemma can_emit_projection : can_emit PreFree m -> can_emit (pre_loaded_with_all_messages_vlsm (IM j)) m. -Proof. +Proof using validator sender Hsender_safety Hj A. destruct (sender m) as [v |] eqn: Hsender; simpl in Hj; [| by congruence]. apply Some_inj in Hj. specialize (Hsender_safety _ _ Hsender). diff --git a/theories/VLSM/Core/Equivocators/EquivocatorReplay.v b/theories/VLSM/Core/Equivocators/EquivocatorReplay.v index 00127558..51e6906d 100644 --- a/theories/VLSM/Core/Equivocators/EquivocatorReplay.v +++ b/theories/VLSM/Core/Equivocators/EquivocatorReplay.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From VLSM.Core Require Import VLSM VLSMProjections Equivocators.Equivocators. From VLSM.Core Require Import Equivocation EquivocationProjections Equivocators.MessageProperties. +Set Default Proof Using "Type". + (** * Equivocator State Append Determines a Projection In this module, we show that we can "append" two equivocator traces by diff --git a/theories/VLSM/Core/Equivocators/Equivocators.v b/theories/VLSM/Core/Equivocators/Equivocators.v index cca51c82..0221cfe0 100644 --- a/theories/VLSM/Core/Equivocators/Equivocators.v +++ b/theories/VLSM/Core/Equivocators/Equivocators.v @@ -4,6 +4,8 @@ From Coq Require Import Eqdep Fin FunctionalExtensionality. From VLSM.Lib Require Import Preamble. From VLSM.Core Require Import VLSM VLSMProjections Composition. +Set Default Proof Using "Type". + (** * VLSM Equivocation An [equivocator_vlsm] for a given [VLSM] <> is a VLSM which starts as a diff --git a/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v b/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v index 1031a513..722a11ba 100644 --- a/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v +++ b/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v @@ -9,6 +9,8 @@ From VLSM.Core Require Import Equivocation.NoEquivocation. From VLSM.Core Require Import Equivocators.Equivocators. From VLSM.Core Require Import Equivocators.MessageProperties. +Set Default Proof Using "Type". + (** * VLSM Equivocator Composition Given a composition <> of VLSMs, we can model equivocator behavior by @@ -302,7 +304,7 @@ Definition not_equivocating_equivocator_descriptors #[export] Instance not_equivocating_equivocator_descriptors_dec : RelDecision not_equivocating_equivocator_descriptors. -Proof. +Proof using H. intros eqv_descriptors s. apply @Decision_iff with (P := Forall (fun eqv => existing_descriptor (IM eqv) (eqv_descriptors eqv) (s eqv)) (enum index)). diff --git a/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v b/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v index 9986096b..1fd09c3a 100644 --- a/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v +++ b/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v @@ -9,6 +9,8 @@ From VLSM.Core Require Import Equivocators.Equivocators Equivocators.Equivocator From VLSM.Core Require Import Equivocators.EquivocatorsComposition. From VLSM.Core Require Import Equivocators.MessageProperties. +Set Default Proof Using "Type". + (** * VLSM Equivocator Composition Projections *) Section sec_equivocators_composition_projections. @@ -1516,7 +1518,7 @@ Qed. Lemma PreFreeE_PreFree_vlsm_partial_projection (final_descriptors : equivocator_descriptors) : VLSM_partial_projection PreFreeE PreFree (equivocators_partial_trace_project final_descriptors). -Proof. +Proof using equivocators_no_equivocations_vlsm H0. split; [by split; apply equivocators_partial_trace_project_extends_left |]. intros s tr sX trX Hpr_tr Htr. destruct (destruct_equivocators_partial_trace_project Hpr_tr) @@ -2105,7 +2107,7 @@ Lemma equivocators_valid_trace_from_project equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\ equivocators_state_project final_descriptors final_state = final_stateX /\ finite_valid_trace_from_to Free isX final_stateX trX. -Proof. +Proof using sub_IM H. apply valid_trace_get_last in Htr as Hfinal_state. apply valid_trace_forget_last in Htr. subst final_state. specialize (VLSM_partial_projection_finite_valid_trace_from @@ -2152,7 +2154,7 @@ Qed. Lemma equivocators_no_equivocations_vlsm_X_vlsm_projection : VLSM_projection equivocators_no_equivocations_vlsm Free (equivocators_total_label_project IM) (equivocators_total_state_project IM). -Proof. +Proof using sub_IM H. constructor; [constructor |]. - intros * Htr. apply PreFreeE_Free_vlsm_projection_type. apply VLSM_incl_finite_valid_trace_from; [| done]. @@ -2182,7 +2184,7 @@ Qed. Lemma preloaded_equivocators_no_equivocations_vlsm_X_vlsm_projection : VLSM_projection PreFreeE PreFree (equivocators_total_label_project IM) (equivocators_total_state_project IM). -Proof. +Proof using H0 H. constructor; [constructor; intros |]. - by apply PreFreeE_Free_vlsm_projection_type. - intros * Htr. diff --git a/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v b/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v index a74f8418..b246bcec 100644 --- a/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v +++ b/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble. From VLSM.Core Require Import VLSM VLSMProjections Equivocators.Equivocators. +Set Default Proof Using "Type". + (** * VLSM Projecting Equivocator Traces *) Section sec_equivocator_vlsm_projections. diff --git a/theories/VLSM/Core/Equivocators/FixedEquivocation.v b/theories/VLSM/Core/Equivocators/FixedEquivocation.v index 14e28393..3e6c9d1e 100644 --- a/theories/VLSM/Core/Equivocators/FixedEquivocation.v +++ b/theories/VLSM/Core/Equivocators/FixedEquivocation.v @@ -10,6 +10,8 @@ From VLSM.Core Require Import Equivocators.MessageProperties. From VLSM.Core Require Import Equivocators.EquivocatorsComposition. From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections. +Set Default Proof Using "Type". + (** * VLSM Equivocators Fixed Equivocation *) Section sec_equivocators_fixed_equivocations_vlsm. @@ -252,7 +254,7 @@ Context (** The [full_node_constraint_alt] is stronger than the [fixed_equivocation_constraint]. *) Lemma fixed_equivocation_constraint_subsumption_alt : strong_constraint_subsumption IM full_node_constraint_alt fixed_equivocation_constraint. -Proof. +Proof using H6 H4 H3 H2 H1 H0. intros l (s, [m |]) Hc ; [| done]. destruct Hc as [Hno_equiv | [i [Hi Hm]]]; [by left |]. unfold node_generated_without_further_equivocation_alt in Hm. @@ -270,7 +272,7 @@ Qed. Lemma fixed_equivocation_constraint_subsumption (Hno_resend : forall i : index, cannot_resend_message_stepwise_prop (IM i)) : preloaded_constraint_subsumption IM full_node_constraint fixed_equivocation_constraint. -Proof. +Proof using H6 H4 H3 H2 H1 H0 EqDecision0. intros l (s, om) Hv. apply fixed_equivocation_constraint_subsumption_alt. by eapply full_node_condition_for_admissible_equivocators_subsumption. @@ -331,7 +333,7 @@ Lemma not_equivocating_equivocator_descriptors_proper_fixed (eqv_descriptors : equivocator_descriptors IM) (Heqv_descriptors : not_equivocating_equivocator_descriptors IM eqv_descriptors s) : proper_fixed_equivocator_descriptors eqv_descriptors s. -Proof. +Proof using H6 H4 H3 H2 H1 H0. apply not_equivocating_equivocator_descriptors_proper in Heqv_descriptors as Hproper. split; [done |]. intros i Hi; rewrite <- elem_of_elements in Hi. @@ -450,7 +452,7 @@ Lemma _equivocators_valid_trace_project equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\ equivocators_state_project IM final_descriptors final_state = final_stateX /\ finite_valid_trace X' isX trX. -Proof. +Proof using X H9 H6 H4 H3 H2 H1 H0. remember (length tr) as len_tr. revert tr Htr Heqlen_tr final_state final_descriptors Hproper. induction len_tr as [len_tr IHlen] using (well_founded_induction Wf_nat.lt_wf); intros. @@ -618,7 +620,7 @@ Lemma free_equivocators_valid_trace_project equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\ equivocators_state_project IM final_descriptors final_state = final_stateX /\ finite_valid_trace (free_composite_vlsm IM) isX trX. -Proof. +Proof using X H9 H6 H4 H3 H2 H1 H0. by apply _equivocators_valid_trace_project. Qed. @@ -639,7 +641,7 @@ Lemma not_equivocating_sent_message_has_been_directly_observed_in_projection (descriptors : equivocator_descriptors IM) (Hdescriptors : proper_fixed_equivocator_descriptors descriptors lst) : has_been_directly_observed Free (equivocators_state_project IM descriptors lst) m. -Proof. +Proof using H6 H4 H3 H2 H1 H0. destruct (free_equivocators_valid_trace_project descriptors is tr Hdescriptors Htr) as [trX [initial_descriptors [_ [Htr_project [Hfinal_state HtrX_Free]]]]]. subst lst. @@ -767,7 +769,7 @@ Lemma equivocators_trace_sub_item_input_is_seeded_or_sub_previously_sent : trace_sub_item_input_is_seeded_or_sub_previously_sent (equivocator_IM IM) (elements equivocating) (composite_has_been_directly_observed IM lst_trX) tr. -Proof. +Proof using H6 H4 H3 H2 H1 H0. intros pre item suf m Heq Hm Hitem. destruct (free_equivocators_valid_trace_project descriptors is tr Hproper Htr) as [trX [initial_descriptors [Hinitial_descriptors [Htr_project [Hfinal_state HtrXFree]]]]]. @@ -912,7 +914,7 @@ Lemma equivocator_vlsm_trace_project_reflect_non_equivocating (Houtput : output item = Some m) (Hno_equiv_item : projT1 (l item) ∉ equivocating) : trace_has_message (field_selector output) m trX. -Proof. +Proof using H6 H4 H3 H2 H1 H0. apply elem_of_list_split in Hitem. destruct Hitem as [pre [suf Heq_tr]]. change (item :: suf) with ([item] ++ suf) in Heq_tr. @@ -984,7 +986,7 @@ Lemma projection_has_not_been_directly_observed_is_equivocating (Hno : ~ composite_has_been_directly_observed IM sX m) : forall item : composite_transition_item (equivocator_IM IM), item ∈ tr -> output item = Some m -> projT1 (l item) ∈ equivocating. -Proof. +Proof using H6 H4 H3 H2 H1 H0. destruct (free_equivocators_valid_trace_project descriptors is tr Hproper Htr) as [trX [initial_descriptors [_ [Htr_project [Hlast_state HtrX]]]]]. intros item Hitem Houtput. @@ -1117,7 +1119,7 @@ Qed. Lemma fixed_equivocation_constraint_has_constraint_has_been_sent_prop : constraint_has_been_sent_prop (fixed_equivocation_constraint IM equivocating). -Proof. +Proof using H6 H4 H3 H2 H1 H0. unfold constraint_has_been_sent_prop. intros. remember (equivocators_state_project _ _ _) as sX. destruct (composite_has_been_directly_observed_dec IM sX m) @@ -1296,7 +1298,7 @@ Theorem fixed_equivocators_valid_trace_project equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\ equivocators_state_project IM final_descriptors final_state = final_stateX /\ finite_valid_trace X isX trX. -Proof. +Proof using H6 H4 H3 H2 H1 H0. apply _equivocators_valid_trace_project; [done | done | done |]; intros. by apply fixed_equivocation_constraint_has_constraint_has_been_sent_prop. Qed. @@ -1304,7 +1306,7 @@ Qed. Lemma fixed_equivocators_vlsm_partial_projection (final_descriptors : equivocator_descriptors IM) : VLSM_partial_projection XE X (equivocators_partial_trace_project IM final_descriptors). -Proof. +Proof using H6 H4 H3 H2 H1 H0 H. split; [split |]. - intros s tr sX trX Hpr_tr s_pre pre Hs_lst Hpre_tr. assert (HPreFree_pre_tr : @@ -1330,7 +1332,7 @@ Qed. Lemma fixed_equivocators_vlsm_projection : VLSM_projection XE X (equivocators_total_label_project IM) (equivocators_total_state_project IM). -Proof. +Proof using H6 H4 H3 H2 H1 H0 H. constructor; [constructor |]; intros sX trX HtrX. - apply PreFreeE_Free_vlsm_projection_type. apply VLSM_incl_finite_valid_trace_from; [| done]. diff --git a/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v b/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v index 09357d3e..1a002552 100644 --- a/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v +++ b/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v @@ -12,6 +12,8 @@ From VLSM.Core Require Import Equivocators.FullReplayTraces. From VLSM.Core Require Import Equivocators.FixedEquivocation. From VLSM.Core Require Import Equivocators.SimulatingFree. +Set Default Proof Using "Type". + (** * VLSM Equivocators Simulating fixed-set equivocation composition In this module we show that the composition of equivocators with no @@ -46,7 +48,7 @@ Context {message : Type} Lemma no_initial_messages_in_sub_IM : forall i m, ~ vinitial_message_prop (sub_IM IM (elements equivocating) i) m. -Proof. +Proof using no_initial_messages_in_IM. intros [i Hi] m Hinit. by apply (no_initial_messages_in_IM i m). Qed. @@ -156,7 +158,7 @@ Lemma fixed_equivocation_replay_has_message s im) : composite_has_been_sent (equivocator_IM IM) (lift_equivocators_sub_state_to IM (elements equivocating) eqv_state_s s) im. -Proof. +Proof using H7. apply non_empty_valid_trace_from_can_produce in Him as (im_eis & im_etr & item & Him_etr & Hlast & Heqs & Him). specialize @@ -190,7 +192,8 @@ Lemma fixed_equivocation_has_replayable_message_prop : replayable_message_prop IM (fun _ : message => False) (strong_fixed_equivocation_constraint IM equivocating) (equivocators_fixed_equivocations_constraint IM (elements equivocating)). -Proof. +Proof using Ci EqDecision0 Free FreeE H5 H7 H8 IM PreFreeE SubFreeE X XE +equivocating index message no_initial_messages_in_IM. specialize (vlsm_is_pre_loaded_with_False XE) as HeqXE. specialize (vlsm_is_pre_loaded_with_False X) as HeqX. specialize (equivocators_fixed_equivocations_vlsm_incl_PreFree IM (elements equivocating)) as HinclE. @@ -269,8 +272,7 @@ Proof. { by apply (VLSM_eq_valid_state HeqXE), (VLSM_eq_valid_state HeqXE). } spec Hreplay. { subst s. - clear -HeqXE Hstate_valid. - intros l s om Hv Hlift_s. + intros l' s om Hv Hlift_s. apply (VLSM_eq_valid_state HeqXE) in Hstate_valid. apply (VLSM_eq_valid_state HeqXE) in Hlift_s. by apply fixed_equivocating_non_equivocating_constraint_lifting. @@ -338,7 +340,7 @@ Lemma fixed_equivocators_finite_valid_trace_init_to_rev equivocators_total_trace_project IM tr = trX /\ finite_valid_trace_init_to XE is s tr /\ finite_trace_last_output trX = finite_trace_last_output tr. -Proof. +Proof using Ci EqDecision0 Free FreeE H5 H7 H8 IM PreFreeE SubFreeE X XE equivocating index message no_initial_messages_in_IM. (* Since the base result works with pre-loaded vlsms, some massaging of the hypothesis and conclusion is done to fit the applied lemma. diff --git a/theories/VLSM/Core/Equivocators/FullReplayTraces.v b/theories/VLSM/Core/Equivocators/FullReplayTraces.v index 3537453a..37e66997 100644 --- a/theories/VLSM/Core/Equivocators/FullReplayTraces.v +++ b/theories/VLSM/Core/Equivocators/FullReplayTraces.v @@ -9,6 +9,8 @@ From VLSM.Core Require Import Equivocators.EquivocatorReplay Equivocators.Messag From VLSM.Core Require Import Equivocators.EquivocatorsComposition. From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections Plans. +Set Default Proof Using "Type". + (** * VLSM Equivocator Full Replay Traces In this section we show that given a trace of equivocators, one can "replay" @@ -503,7 +505,7 @@ Lemma replayed_initial_state_from_valid (His : composite_initial_state_prop sub_equivocator_IM is) : finite_valid_trace_from SeededCE full_replay_state (replayed_initial_state_from full_replay_state is). -Proof. +Proof using Hfull_replay_state Hconstraint_none. cut (forall l, incl l (enum (sub_index equivocating)) -> finite_valid_plan_from SeededCE full_replay_state (map (initial_new_machine_transition_item is) l)). @@ -532,7 +534,7 @@ Qed. Lemma lift_initial_message : forall m, vinitial_message_prop SeededXE m -> valid_message_prop SeededCE m. -Proof. +Proof using Hseed. intros m [Hinit | Hseeded]. - apply initial_message_is_valid. destruct Hinit as [[i Hi] Hinit]. by left; exists i. @@ -543,7 +545,7 @@ Lemma lift_equivocators_sub_weak_projection : VLSM_weak_embedding SeededXE SeededCE (lift_equivocators_sub_label_to full_replay_state) (lift_equivocators_sub_state_to full_replay_state). -Proof. +Proof using Hsubsumption Hseed Hfull_replay_state Hconstraint_none. apply basic_VLSM_weak_embedding; intros ? *. - split. + by apply lift_equivocators_sub_valid, Hv. @@ -560,7 +562,7 @@ Lemma sub_preloaded_replayed_trace_from_valid_equivocating (Htr : finite_valid_trace SeededXE is tr) : finite_valid_trace_from SeededCE full_replay_state (replayed_trace_from full_replay_state is tr). -Proof. +Proof using Hsubsumption Hseed Hfull_replay_state Hconstraint_none. destruct Htr as [Htr His]. apply finite_valid_trace_from_app_iff. split; [by apply replayed_initial_state_from_valid |]. @@ -622,7 +624,7 @@ Context equivocator_IM (free_constraint _) seed (lift_equivocators_sub_label_to full_replay_state l) (lift_equivocators_sub_state_to full_replay_state s, om). -Proof. +Proof using Hfull_replay_state. intros l s om (Hs & _ & _ & Hc1 & _). split; [| done]. destruct om as [m |]; [| done]. @@ -666,7 +668,7 @@ Lemma SeededXE_SeededNoEquiv_weak_embedding : VLSM_weak_embedding SeededXE SeededAllXE (lift_equivocators_sub_label_to full_replay_state) (lift_equivocators_sub_state_to full_replay_state). -Proof. +Proof using Hfull_replay_state. constructor. apply lift_equivocators_sub_weak_projection; intros; [done | | done |]. - by apply sent_are_valid. @@ -679,7 +681,7 @@ Lemma sub_replayed_trace_from_valid_equivocating (Htr : finite_valid_trace SeededXE is tr) : finite_valid_trace_from SeededAllXE full_replay_state (replayed_trace_from full_replay_state is tr). -Proof. +Proof using Hfull_replay_state. unfold composite_no_equivocation_vlsm_with_pre_loaded in SeededAllXE. specialize (sub_preloaded_replayed_trace_from_valid_equivocating (no_equivocations_additional_constraint_with_pre_loaded equivocator_IM (free_constraint _) seed) diff --git a/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v b/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v index 2cdf71c9..8c3c7d55 100644 --- a/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v +++ b/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v @@ -16,6 +16,8 @@ From VLSM.Core Require Import Equivocators.FixedEquivocationSimulation. From VLSM.Core Require Import Equivocators.FixedEquivocation. +Set Default Proof Using "Type". + (** * VLSM Equivocators Simulating limited message equivocation traces In this module we show that the composition of equivocators with no-message @@ -139,7 +141,7 @@ Lemma equivocators_limited_valid_trace_projects_to_annotated_limited_equivocatio Datatypes.id original_state trX /\ finite_valid_trace_init_to XE is s tr /\ finite_trace_last_output trX = finite_trace_last_output tr. -Proof. +Proof using no_initial_messages_in_IM message_dependencies Hchannel H19 H18 H16 H15 H11 FullMessageDependencies0 EqDecision1. apply valid_trace_get_last in HtrX as HeqsX. eapply valid_trace_forget_last, @msg_dep_fixed_limited_equivocation in HtrX; [| done..]. apply limited_equivocators_finite_valid_trace_init_to_rev in HtrX diff --git a/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v b/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v index 3bc95528..e05d2e98 100644 --- a/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v +++ b/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v @@ -12,6 +12,8 @@ From VLSM.Core Require Import Equivocators.EquivocatorsComposition. From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections. From VLSM.Core Require Import Equivocators.FixedEquivocation. +Set Default Proof Using "Type". + (** * VLSM Limited Equivocation *) Definition composite_constraint {index message} (IM : index -> VLSM message) : Type := @@ -283,7 +285,7 @@ Lemma equivocators_limited_valid_trace_projects_to_annotated_limited_equivocatio finite_valid_trace (msg_dep_limited_equivocation_vlsm IM threshold full_message_dependencies sender (Cv := Ci)) {| original_state := isX; state_annotation := ` inhabitant |} (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender isX trX). -Proof. +Proof using no_initial_messages_in_IM message_dependencies Hchannel HMsgDep HFullMsgDep H18 H16 H15 H11 EqDecision1. eapply equivocators_limited_valid_trace_projects_to_fixed_limited_equivocation in Htr as (trX & initial_descriptors & Hinitial_descriptors & Hpr & Hlst_pr & Hpr_limited) ; [| done]. @@ -328,7 +330,7 @@ Lemma limited_equivocators_valid_trace_project equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\ equivocators_state_project final_descriptors final_state = final_stateX /\ finite_valid_trace Limited isX trX. -Proof. +Proof using Hsender_safety H0. specialize (equivocators_limited_valid_trace_projects_to_fixed_limited_equivocation final_descriptors is tr Hproper Htr) @@ -348,7 +350,7 @@ Lemma limited_equivocators_vlsm_partial_projection (final_descriptors : equivocator_descriptors) : VLSM_partial_projection equivocators_limited_equivocations_vlsm Limited (equivocators_partial_trace_project IM final_descriptors). -Proof. +Proof using Hsender_safety H0. split; [split |]. - intros s tr sX trX Hpr_tr s_pre pre Hs_lst Hpre_tr. assert (HPreFree_pre_tr : @@ -377,7 +379,7 @@ Qed. Lemma limited_equivocators_vlsm_projection : VLSM_projection equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM). -Proof. +Proof using Hsender_safety H0. constructor; [constructor |]; intros ? *. - intros HtrX. apply PreFreeE_Free_vlsm_projection_type. revert HtrX. apply VLSM_incl_finite_valid_trace_from. diff --git a/theories/VLSM/Core/Equivocators/MessageProperties.v b/theories/VLSM/Core/Equivocators/MessageProperties.v index 0c69ab34..a96710ef 100644 --- a/theories/VLSM/Core/Equivocators/MessageProperties.v +++ b/theories/VLSM/Core/Equivocators/MessageProperties.v @@ -5,6 +5,8 @@ From VLSM.Lib Require Import ListSetExtras FinExtras. From VLSM.Core Require Import VLSM Equivocation. From VLSM.Core Require Import Equivocators.Equivocators Equivocators.EquivocatorsProjections. +Set Default Proof Using "Type". + (** * VLSM Message Properties *) Section sec_equivocator_vlsm_message_properties. @@ -259,7 +261,7 @@ Definition equivocator_oracle Lemma equivocator_oracle_dec : RelDecision equivocator_oracle. -Proof. +Proof using Hdec. intros s m. eapply (Decision_iff @@ -279,7 +281,7 @@ Qed. Lemma equivocator_oracle_stepwise_props : oracle_stepwise_props (vlsm := equivocator_vlsm) equivocator_selector equivocator_oracle. -Proof. +Proof using Hstepwise Hselector_io. destruct Hstepwise. split; intros. - destruct H as [Hn His]. unfold is_singleton_state in Hn. @@ -543,7 +545,7 @@ Qed. Lemma equivocator_ComputableSentMessages : ComputableSentMessages equivocator_vlsm. -Proof. +Proof using EqDecision0 ComputableSentMessages0. constructor 1 with equivocator_sent_messages_set; constructor; intros. - rewrite <- equivocator_elem_of_sent_messages_set. by eapply equivocator_has_been_sent_stepwise_props. diff --git a/theories/VLSM/Core/Equivocators/SimulatingFree.v b/theories/VLSM/Core/Equivocators/SimulatingFree.v index d4157a13..c755f549 100644 --- a/theories/VLSM/Core/Equivocators/SimulatingFree.v +++ b/theories/VLSM/Core/Equivocators/SimulatingFree.v @@ -8,6 +8,8 @@ From VLSM.Core Require Import Equivocators.EquivocatorsComposition. From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections. From VLSM.Core Require Import Equivocators.FullReplayTraces. +Set Default Proof Using "Type". + (** * Equivocators simulating regular nodes In this module we prove a general simulation result parameterized by @@ -110,7 +112,7 @@ Lemma generalized_equivocators_finite_valid_trace_init_to_rev exists tr, equivocators_total_trace_project IM tr = trX /\ finite_valid_trace_init_to CE is s tr /\ finite_trace_last_output trX = finite_trace_last_output tr. -Proof. +Proof using H. assert (HinclE : VLSM_incl CE PreFreeE) by apply composite_pre_loaded_vlsm_incl_pre_loaded_with_all_messages. induction HtrX using finite_valid_trace_init_to_rev_strong_ind. @@ -312,7 +314,7 @@ Lemma seeded_equivocators_finite_valid_trace_init_to_rev exists tr, equivocators_total_trace_project IM tr = trX /\ finite_valid_trace_init_to SeededXE is s tr /\ finite_trace_last_output trX = finite_trace_last_output tr. -Proof. +Proof using H. apply (generalized_equivocators_finite_valid_trace_init_to_rev IM) ; [.. | done]. @@ -391,7 +393,7 @@ Lemma equivocators_finite_valid_trace_init_to_rev exists tr, equivocators_total_trace_project IM tr = trX /\ finite_valid_trace_init_to XE is s tr /\ finite_trace_last_output trX = finite_trace_last_output tr. -Proof. +Proof using H. specialize (vlsm_is_pre_loaded_with_False Free) as Heq. apply (VLSM_eq_finite_valid_trace_init_to Heq) in HtrX. specialize diff --git a/theories/VLSM/Core/MessageDependencies.v b/theories/VLSM/Core/MessageDependencies.v index 256b2bdc..03db6f4b 100644 --- a/theories/VLSM/Core/MessageDependencies.v +++ b/theories/VLSM/Core/MessageDependencies.v @@ -4,6 +4,8 @@ From VLSM.Lib Require Import Preamble ListExtras ListFinSetExtras. From VLSM.Core Require Import VLSM VLSMProjections Composition ProjectionTraces. From VLSM.Core Require Import SubProjectionTraces Equivocation EquivocationProjections. +Set Default Proof Using "Type". + (** * VLSM Message Dependencies An abstract framework for the full-node condition. @@ -133,7 +135,7 @@ Lemma msg_dep_reflects_validity : forall dm m, msg_dep_rel dm m -> valid_message_prop (pre_loaded_vlsm X P) m -> valid_message_prop (pre_loaded_vlsm X P) dm. -Proof. +Proof using MessageDependencies0 Irreflexive0 HasBeenSentCapability0 HasBeenReceivedCapability0. intros dm m Hdm. rewrite emitted_messages_are_valid_iff, can_emit_iff. intros [Hinit | [s Hproduce]]. @@ -165,7 +167,7 @@ Lemma msg_dep_has_been_sent m (Hsent : has_been_sent X s m) : forall dm, msg_dep_rel dm m -> has_been_directly_observed X s dm. -Proof. +Proof using MessageDependencies0 Irreflexive0. revert m Hsent; induction Hs using valid_state_prop_ind; intro m. - intro Hbs; contradict Hbs. by apply has_been_sent_no_inits. @@ -216,7 +218,7 @@ Lemma msg_dep_full_node_reflects_has_been_directly_observed (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm X) s) : forall dm m, msg_dep_rel dm m -> has_been_directly_observed X s m -> has_been_directly_observed X s dm. -Proof. +Proof using MessageDependencies0 Irreflexive0. intros dm m Hdm [Hsent | Hreceived]. - by eapply msg_dep_has_been_sent. - by eapply full_node_has_been_received. @@ -232,7 +234,7 @@ Lemma msg_dep_full_node_happens_before_reflects_has_been_directly_observed (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm X) s) : forall dm m, msg_dep_happens_before dm m -> has_been_directly_observed X s m -> has_been_directly_observed X s dm. -Proof. +Proof using MessageDependencies0 Irreflexive0. intros dm m Hdm Hobs. eapply msg_dep_happens_before_reflect; [| done ..]. by apply msg_dep_full_node_reflects_has_been_directly_observed. @@ -248,7 +250,7 @@ Lemma msg_dep_full_node_input_valid_happens_before_has_been_directly_observed (Hvalid : input_valid (pre_loaded_with_all_messages_vlsm X) l (s, Some m)) : forall dm, msg_dep_happens_before dm m -> has_been_directly_observed X s dm. -Proof. +Proof using MessageDependencies0 Irreflexive0. intro dm; rewrite msg_dep_happens_before_iff_one; intros [Hdm | (dm' & Hdm' & Hdm)]. - by eapply Hfull; [apply Hvalid |]. - eapply msg_dep_happens_before_reflect; [| done |]. @@ -514,7 +516,7 @@ Context *) #[export] Instance composite_message_dependencies : MessageDependencies (free_composite_vlsm IM) message_dependencies. -Proof. +Proof using H10. split. - intros m s' ((s, iom) & [i li] & Ht) dm Hdm. apply composite_has_been_directly_observed_free_iff. @@ -533,7 +535,7 @@ Lemma msg_dep_reflects_free_validity (X := free_composite_vlsm IM) : forall dm m, msg_dep_rel message_dependencies dm m -> valid_message_prop X m -> valid_message_prop X dm. -Proof. +Proof using Irreflexive0 H9 H8 H7 H10. intros dm m Hdm. rewrite !emitted_messages_are_valid_iff. intros [[i [[im Him] _]] | Hemit] @@ -563,7 +565,7 @@ Lemma msg_dep_reflects_happens_before_free_validity (X := free_composite_vlsm IM) : forall dm m, msg_dep_happens_before message_dependencies dm m -> valid_message_prop X m -> valid_message_prop X dm. -Proof. +Proof using Irreflexive0 H9 H8 H7 H10. by apply msg_dep_happens_before_reflect, msg_dep_reflects_free_validity. Qed. @@ -578,7 +580,7 @@ Lemma msg_dep_happens_before_composite_no_initial_valid_messages_emitted_by_send forall dm, msg_dep_happens_before message_dependencies dm m -> exists v, sender dm = Some v /\ can_emit (pre_loaded_with_all_messages_vlsm (IM (A v))) dm. -Proof. +Proof using Irreflexive0 H9 H8 H7 H10. intros m Hm dm Hdm. cut (valid_message_prop X dm). - by apply composite_no_initial_valid_messages_emitted_by_sender. @@ -778,7 +780,7 @@ Lemma tc_composite_observed_before_send_subsumes_happens_before forall m, can_emit Free m -> forall dm, msg_dep_happens_before message_dependencies dm m -> tc_composite_observed_before_send dm m. -Proof. +Proof using H7. intros m Hm dm Hdm. induction Hdm; [by eapply tc_composite_observed_before_send_subsumes_msg_dep_rel |]. transitivity y; [| by apply IHHdm]. @@ -829,7 +831,7 @@ Definition full_node_is_globally_equivocating Lemma full_node_is_globally_equivocating_stronger s v : full_node_is_globally_equivocating s v -> msg_dep_is_globally_equivocating s v. -Proof. +Proof using EqDecision1. intros [m []]; exists m; constructor; [done | | done]. by constructor 1; apply composite_has_been_directly_observed_sent_received_iff; right. Qed. @@ -923,7 +925,7 @@ Lemma msg_dep_reflects_sub_free_validity : forall dm m, msg_dep_rel message_dependencies dm m -> valid_message_prop (pre_loaded_vlsm X P) m -> valid_message_prop (pre_loaded_vlsm X P) dm. -Proof. +Proof using Irreflexive0 H17 H16 H15. eapply msg_dep_reflects_validity; [| | done]. - by typeclasses eauto. - intros m [sub_i [[im Him] Heqm]]. @@ -969,7 +971,7 @@ Context #[export] Instance msg_dep_happens_before_dec : RelDecision (msg_dep_happens_before message_dependencies). -Proof. +Proof using full_message_dependencies HFullMsgDep. refine (fun m1 m2 => match decide (m1 ∈ full_message_dependencies m2) with @@ -982,7 +984,7 @@ Qed. #[export] Instance msg_dep_happens_before_irrefl : Irreflexive (msg_dep_happens_before message_dependencies). -Proof. +Proof using full_message_dependencies HFullMsgDep. intros m Hm. contradict Hm. rewrite <- full_message_dependencies_happens_before. @@ -995,7 +997,7 @@ Qed. Lemma msg_dep_rel_full_message_dependecies_subset : forall x y : message, msg_dep_rel message_dependencies x y -> full_message_dependencies x ⊆ full_message_dependencies y. -Proof. +Proof using HFullMsgDep. intros; intros z Hz. apply full_message_dependencies_happens_before. transitivity x; [by apply full_message_dependencies_happens_before |]. @@ -1003,7 +1005,7 @@ Proof. Qed. Lemma msg_dep_happens_before_wf : well_founded (msg_dep_happens_before message_dependencies). -Proof. +Proof using full_message_dependencies HFullMsgDep. apply tc_wf_projected with (<) (fun m => length (elements (full_message_dependencies m))); [by typeclasses eauto | | by apply Wf_nat.lt_wf]. intros; unfold lt. @@ -1023,7 +1025,7 @@ Lemma FullMessageDependencies_ind (IHm : forall dm, dm ∈ full_message_dependencies m -> (forall dm0, dm0 ∈ full_message_dependencies dm -> P dm0) -> P dm) : forall dm, dm ∈ full_message_dependencies m -> P dm. -Proof. +Proof using message_dependencies HFullMsgDep H6 H5 H4 H3 H2 H1 H0 EqDecision0. induction m as (m & Hm) using (well_founded_ind msg_dep_happens_before_wf). intros dm Hdm. apply IHm; [done |]. @@ -1111,7 +1113,7 @@ Lemma free_valid_from_valid_dependencies forall dm, dm ∈ full_message_dependencies m -> valid_message_prop (free_composite_vlsm IM) dm) : valid_message_prop (free_composite_vlsm IM) m. -Proof. +Proof using H9 H8 H7 H6 H5 H4 H3 H10 EqDecision1. eapply emitted_messages_are_valid, free_valid_preloaded_lifts_can_be_emitted; [| done]. by intros; apply Hdeps, full_message_dependencies_happens_before, msg_dep_happens_before_iff_one; left. @@ -1125,7 +1127,7 @@ Lemma free_valid_from_all_dependencies_emitable_from_dependencies : forall m, all_dependencies_emittable_from_dependencies_prop m -> valid_message_prop (free_composite_vlsm IM) m. -Proof. +Proof using H9 H7 H6 H5 H4 H3 H10 EqDecision1. intros m Hm. specialize (Hm m) as Hemit; spec Hemit; [left |]. inversion Hemit as [v _ Hemit']; clear Hemit. @@ -1147,7 +1149,7 @@ Qed. Lemma valid_free_validating_is_message_validating : forall i, valid_all_dependencies_emittable_from_dependencies_prop i -> component_message_validator_prop IM (free_constraint IM) i. -Proof. +Proof using H9 H7 H6 H5 H4 H3 H10 EqDecision1. by intros i Hvalidating l s im Hv ; eapply free_valid_from_all_dependencies_emitable_from_dependencies, Hvalidating. Qed. @@ -1165,7 +1167,7 @@ Lemma valid_free_validating_equiv_message_validating (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM) : forall i, component_message_validator_prop IM (free_constraint IM) i <-> valid_all_dependencies_emittable_from_dependencies_prop i. -Proof. +Proof using H. intros i; split; [| apply valid_free_validating_is_message_validating]. intros Hvalidator l s m Hv dm Hdm. specialize (Hvalidator l s m Hv). @@ -1197,7 +1199,7 @@ Context #[export] Instance CompositeHasBeenObserved_dec `{FullMessageDependencies message Cm message_dependencies full_message_dependencies} : RelDecision (CompositeHasBeenObserved IM message_dependencies). -Proof. +Proof using H7 EqDecision1. intros s m. destruct (decide (composite_has_been_directly_observed IM s m)); [by left; constructor |]. @@ -1245,7 +1247,7 @@ Lemma input_valid_transition_preserves_msg_dep_is_globally_equivocating : forall v, A v = j -> msg_dep_is_globally_equivocating IM message_dependencies sender s v -> msg_dep_is_globally_equivocating IM message_dependencies sender (destination item) v. -Proof. +Proof using Hsender_safety Hauth. intros s item Ht j Hsj v Hv [m []]. exists m; constructor; [done | ..]. - by eapply transition_preserves_CompositeHasBeenObserved. diff --git a/theories/VLSM/Core/Plans.v b/theories/VLSM/Core/Plans.v index 1c49cc76..dc33bd24 100644 --- a/theories/VLSM/Core/Plans.v +++ b/theories/VLSM/Core/Plans.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From VLSM.Core Require Import VLSM. +Set Default Proof Using "Type". + (** * VLSM Plans *) Section sec_plans. diff --git a/theories/VLSM/Core/ProjectionTraces.v b/theories/VLSM/Core/ProjectionTraces.v index 36bd196c..225ce90a 100644 --- a/theories/VLSM/Core/ProjectionTraces.v +++ b/theories/VLSM/Core/ProjectionTraces.v @@ -3,6 +3,8 @@ From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble StdppExtras. From VLSM.Core Require Import VLSM Composition VLSMProjections Validator. +Set Default Proof Using "Type". + Section sec_projections. (** * Composite VLSM induced projections diff --git a/theories/VLSM/Core/ReachableThreshold.v b/theories/VLSM/Core/ReachableThreshold.v index d9834458..6fb5b12d 100644 --- a/theories/VLSM/Core/ReachableThreshold.v +++ b/theories/VLSM/Core/ReachableThreshold.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From Coq Require Import Reals Lra. From VLSM.Lib Require Import RealsExtras Measurable ListExtras StdppListSet. +Set Default Proof Using "Type". + (** Given a set of validators and a [threshold] (a positive real number), we say that the threshold is reachable ([rt_reachable]) when there exists a @@ -73,7 +75,7 @@ Lemma pivotal_validator_extension exists v, v ∈ vs /\ (sum_weights (vs ∖ {[ v ]} ∪ vsfix) <= threshold)%R. -Proof. +Proof using H6 H3 H0 EqDecision0. intros vsfix vss Hvsfix Hdisj Hall. destruct (pivotal_validator_extension_list (elements vsfix) (elements vss)) as (vs & Hnd_vs & Hincl & Hvs & v & Hv & Hvs_v); @@ -123,7 +125,7 @@ Lemma validators_pivotal_ind exists v, v ∈ vs /\ (sum_weights (vs ∖ {[ v ]}) <= threshold)%R. -Proof. +Proof using Hrt H6 H3 H2 H0 EqDecision0. intros vss Hvss. destruct (pivotal_validator_extension ∅ vss) as (vs & Hincl & Hvs & v & Hv & Hvs'). @@ -146,7 +148,7 @@ Lemma sufficient_validators_pivotal exists v, v ∈ vs /\ (sum_weights (vs ∖ {[ v ]}) <= threshold)%R. -Proof. +Proof using Hrt H6 H3 H2 H0 EqDecision0. destruct (rt_reachable (1 := Hrt)) as [vs Hweight]. apply (validators_pivotal_ind vs) in Hweight as (vs' & Hincl & Hvs'). by exists vs'. @@ -169,7 +171,7 @@ Definition potentially_pivotal (v : V) : Prop := *) Lemma exists_pivotal_validator : exists v, potentially_pivotal v. -Proof. +Proof using Hrt H6 H4 H3 H2 H1 H0 EqDecision0. destruct sufficient_validators_pivotal as (vs & Hgt & v & Hin & Hlte). exists v, (vs ∖ {[ v ]}); split_and!. - by rewrite elem_of_difference, elem_of_singleton; intros []. diff --git a/theories/VLSM/Core/SubProjectionTraces.v b/theories/VLSM/Core/SubProjectionTraces.v index 9ac57af5..a259ed4f 100644 --- a/theories/VLSM/Core/SubProjectionTraces.v +++ b/theories/VLSM/Core/SubProjectionTraces.v @@ -5,6 +5,8 @@ From VLSM.Lib Require Import Preamble ListExtras StdppListSet StdppExtras StdppL From VLSM.Core Require Import VLSM VLSMProjections ProjectionTraces Composition Validator. From VLSM.Core Require Import Equivocation EquivocationProjections Equivocation.NoEquivocation. +Set Default Proof Using "Type". + (** * VLSM Subcomposition *) Section sec_sub_composition. @@ -603,11 +605,10 @@ Proof. + unfold pre_VLSM_projection_transition_item_project in HitemX. destruct (composite_label_sub_projection_option _); [| by congruence]. by inversion HitemX. - - clear -Hmsg Sub_Free Hlst His IHtr. - destruct iom as [m |]; [| done]. + - destruct iom as [m |]; [| done]. simpl in *. remember {| input := Some m |} as x. - assert (Hx : from_sub_projection x). + assert (Hx' : from_sub_projection x). { unfold from_sub_projection at 1, pre_VLSM_projection_in_projection, composite_label_sub_projection_option. @@ -914,7 +915,7 @@ Qed. Lemma preloaded_lift_sub_state_to_initial_state : weak_projection_initial_state_preservation PreSubFree PreFree (lift_sub_state_to IM equivocators base_s). -Proof. +Proof using EqDecision0 Free Hbase_s IM PreFree PreSubFree SubFree base_s equivocating_IM equivocators index message. apply valid_state_has_trace in Hbase_s as Htr. destruct Htr as [is [tr Htr]]. intros eqv_is Heqv_is. @@ -963,7 +964,7 @@ Qed. Lemma PreSubFree_PreFree_weak_embedding : VLSM_weak_embedding PreSubFree PreFree (lift_sub_label IM equivocators) (lift_sub_state_to IM equivocators base_s). -Proof. +Proof using EqDecision0 Free Hbase_s IM PreFree PreSubFree SubFree base_s equivocating_IM equivocators index message. apply basic_VLSM_weak_embedding. - split; [| done]. by apply lift_sub_to_valid, Hv. @@ -1088,7 +1089,7 @@ Lemma lift_sub_incl_message_initial (m : message) (Hm : composite_initial_message_prop sub_IM1 m) : composite_initial_message_prop sub_IM2 m. -Proof. +Proof using EqDecision0 Hincl IM index indices1 indices2 message sub_IM1 sub_IM2. destruct Hm as [[i Hi] Hm]. unfold sub_IM1, sub_IM in Hm. simpl in Hm. apply bool_decide_spec, Hincl in Hi. @@ -1189,7 +1190,7 @@ Lemma sub_can_emit_sender (P : message -> Prop) sender m = Some v -> can_emit (pre_loaded_vlsm (free_composite_vlsm sub_IM) P) m -> A v ∈ indices. -Proof. +Proof using A EqDecision0 Hsender_safety IM index indices message sender sub_IM validator. intros m v Hsender Hemit. specialize (Hsender_safety m v Hsender). destruct Hemit as [[s om] [[sub_i li] [s' Ht]]]. @@ -1265,7 +1266,7 @@ Qed. Lemma sub_IM_sender_safety : sender_safety_alt_prop sub_IM sub_IM_A sub_IM_sender. -Proof. +Proof using A EqDecision0 Hsender_safety IM index indices message sender sub_IM validator. intros m sub_v Hsender sub_i Hm. destruct_dec_sig sub_v v HAv Heqsub_v. destruct_dec_sig sub_i i Hi Heqsub_i. @@ -1291,7 +1292,7 @@ Lemma sub_IM_has_been_sent_iff_by_sender s (Hv : A v ∈ indices) : composite_has_been_sent sub_IM s m -> has_been_sent (sub_IM (dexist (A v) Hv)) (s (dexist (A v) Hv)) m. -Proof. +Proof using A EqDecision0 H Hsender_safety IM index indices message sender sub_IM sub_index_prop_dec validator. apply valid_state_has_trace in Hs as Htr. destruct Htr as [is [tr Htr]]. assert (Hsub_sender : sub_IM_sender m = Some (dexist v Hv)). @@ -1380,7 +1381,7 @@ Lemma sub_IM_no_equivocation_preservation l (s, om)) : composite_no_equivocations_except_from sub_IM non_sub_index_authenticated_message l (s, om). -Proof. +Proof using A EqDecision0 H Hsender_safety IM can_emit_signed index indices message no_initial_messages_in_IM sender sub_IM validator. destruct om as [m |]; [| done]. destruct Hv as (lX & sX & [_ [=] (_ & Hm & _ & Hc)]). specialize (composite_no_initial_valid_messages_have_sender IM A sender @@ -1589,7 +1590,7 @@ Lemma sub_valid_preloaded_lifts_can_be_emitted valid_message_prop (pre_loaded_vlsm (free_composite_vlsm (sub_IM IM (elements indices))) Q) dm) : forall m, can_emit (pre_loaded_vlsm (IM j) P) m -> can_emit (pre_loaded_vlsm (free_composite_vlsm (sub_IM IM (elements indices))) Q) m. -Proof. +Proof using Ci EqDecision0 H5 Hj IM index indices j message. intros m Hm. eapply VLSM_incl_can_emit. - apply (pre_loaded_vlsm_incl_relaxed _ (fun m => Q m \/ P m)). @@ -1843,7 +1844,7 @@ Context *) Lemma sub_no_indices_no_can_emit (P : message -> Prop) : forall m, ~ can_emit (pre_loaded_vlsm (free_composite_vlsm sub_IM) P) m. -Proof. +Proof using EqDecision0 Hno_indices IM index indices message sub_IM. apply pre_loaded_empty_composition_no_emit, elem_of_empty_nil. by intro sub_i; destruct_dec_sig sub_i i Hi Heqsub_i; subst; inversion Hi. Qed. @@ -1884,7 +1885,7 @@ Context `{forall i : index, HasBeenSentCapability (IM i)} : forall sub_i : sub_index (elements selection_complement), HasBeenSentCapability (sub_IM updated_IM (elements selection_complement) sub_i). -Proof. +Proof using Ci EqDecision0 H H0 H1 H2 H3 H4 H5 H6 H7 IM index message replacement_IM selection selection_complement updated_IM. intros sub_i. unfold sub_IM, updated_IM, update_IM. case_decide as Hi; [| typeclasses eauto]. diff --git a/theories/VLSM/Core/TraceableVLSM.v b/theories/VLSM/Core/TraceableVLSM.v index 6047505f..bbbca9d1 100644 --- a/theories/VLSM/Core/TraceableVLSM.v +++ b/theories/VLSM/Core/TraceableVLSM.v @@ -4,6 +4,8 @@ From VLSM.Lib Require Import EquationsExtras. From VLSM.Lib Require Import Preamble ListSetExtras. From VLSM.Core Require Import VLSM Composition VLSMEmbedding. +Set Default Proof Using "Type". + (** * Traceable VLSMs This section introduces [TraceableVLSM]s, characterized by the fact that from @@ -106,7 +108,7 @@ Lemma tv_state_destructor_size : forall s' : vstate X, valid_state_prop R s' -> forall (s : vstate X) (item : vtransition_item X), (item, s) ∈ state_destructor s' -> state_size s < state_size s'. -Proof. +Proof using TraceableVLSM0. intros. apply transition_monotonicity. erewrite <- tv_state_destructor_destination by done. @@ -223,7 +225,7 @@ Qed. Lemma composite_tv_state_destructor_destination : forall (s' s : composite_state IM) (item : composite_transition_item IM) i, (item, s) ∈ composite_state_destructor s' i -> destination item = s'. -Proof. +Proof using state_size H0. intros *; unfold composite_state_destructor; rewrite elem_of_list_fmap. intros ([itemi si] & [= -> ->] & Hin). cbn; unfold lift_to_composite_state. @@ -235,7 +237,7 @@ Lemma composite_tv_state_destructor_transition : forall (s : composite_state IM) (item : composite_transition_item IM) (i : index), (item, s) ∈ composite_state_destructor s' i -> input_valid_transition_item RFree s item. -Proof. +Proof using state_size H0. intros s' Hs' s item i. unfold composite_state_destructor; rewrite elem_of_list_fmap. intros ([itemi si] & [=-> ->] & Hin). @@ -259,7 +261,7 @@ Lemma composite_tv_state_destructor_state_update : forall (s : composite_state IM) (item : composite_transition_item IM) (i : index), (item, s) ∈ composite_state_destructor s' i -> s' = state_update IM s i (destination item i). -Proof. +Proof using state_size H0. intros s' Hs' s item i Hin. replace s' with (destination item) in * by (eapply composite_tv_state_destructor_destination; done). @@ -275,7 +277,7 @@ Lemma composite_tv_state_destructor_initial : vinitial_state_prop (IM i) (s i) <-> composite_state_destructor s i = []. -Proof. +Proof using state_size H0. unfold composite_state_destructor; split; intros Hinit. - replace (state_destructor i (s i)) with (@nil (vtransition_item (IM i) * vstate (IM i))); [done |]. @@ -291,7 +293,7 @@ Lemma composite_tv_state_destructor_reflects_initiality : forall (i : index) (s : composite_state IM) (item : composite_transition_item IM), (item, s) ∈ composite_state_destructor s' i -> forall j, vinitial_state_prop (IM j) (s' j) -> s j = s' j. -Proof. +Proof using state_size H0. intros s' Hs' i s item Hdestruct. apply composite_tv_state_destructor_state_update in Hdestruct as Heqs'; [| done]. intros j Hinit; destruct (decide (i = j)); subst; [| by state_update_simpl]. @@ -304,7 +306,7 @@ Lemma composite_tv_state_destructor_size : forall (s : composite_state IM) (item : composite_transition_item IM) (i : index), (item, s) ∈ composite_state_destructor s' i -> composite_state_size s < composite_state_size s'. -Proof. +Proof using H0. intros s' Hs' s item i. unfold composite_state_destructor; rewrite elem_of_list_fmap. intros ([itemi si] & [= -> ->] & Hin). @@ -320,7 +322,7 @@ Lemma composite_state_destructor_lookup_reachable : forall s' : composite_state IM, valid_state_prop RFree s' -> forall i n item s, composite_state_destructor s' i !! n = Some (item, s) -> input_valid_transition_item RFree s item. -Proof. +Proof using state_size H0. intros s' Hs' i n item s Hdestruct. by eapply composite_tv_state_destructor_transition, elem_of_list_lookup_2. Qed. @@ -329,7 +331,7 @@ Lemma composite_state_destructor_head_reachable : forall s' : composite_state IM, valid_state_prop RFree s' -> forall i item s, head (composite_state_destructor s' i) = Some (item, s) -> input_valid_transition_item RFree s item. -Proof. +Proof using state_size H0. intros s' Hs' i item s Hdestruct. by eapply composite_tv_state_destructor_transition, head_Some_elem_of. Qed. @@ -386,7 +388,7 @@ Lemma choosing_well_position_exists : (i_n := choose s' Hs' indices), composite_state_destructor s' i_n.1 <> [] -> composite_state_destructor s' i_n.1 !! i_n.2 <> None. -Proof. +Proof using state_size H0. intros choose s' Hs' indices Hchoose i_n Hdestruct. eapply not_eq_None_Some, cw_chosen_position_exists; [done | |]. - by destruct (choose _ _ _). @@ -417,7 +419,7 @@ Lemma composite_tv_state_destructor_preserves_not_in_indices_initial : forall (indices : list index), not_in_indices_initial_prop s' indices -> not_in_indices_initial_prop s indices. -Proof. +Proof using state_size H0. intros s' Hs' * Heq indices Hinits' j Hj. by erewrite composite_tv_state_destructor_reflects_initiality; [apply Hinits' | | eapply elem_of_list_lookup_2 | apply Hinits']. @@ -434,7 +436,7 @@ Lemma set_remove_preserves_not_in_indices_initial : forall (indices : list index), not_in_indices_initial_prop s' indices -> not_in_indices_initial_prop s' (StdppListSet.set_remove i indices). -Proof. +Proof using state_size H0. intros s' Hs' i Hdestruct indices Hinit j Hj. destruct (decide (j ∈ indices)); [| by apply Hinit]. destruct (decide (j = i)); [by subst; apply composite_tv_state_destructor_initial |]. diff --git a/theories/VLSM/Core/VLSM.v b/theories/VLSM/Core/VLSM.v index 896ebb9f..0b361dca 100644 --- a/theories/VLSM/Core/VLSM.v +++ b/theories/VLSM/Core/VLSM.v @@ -3,6 +3,8 @@ From stdpp Require Import prelude. From Coq Require Import Streams. From VLSM.Lib Require Import Preamble ListExtras StreamExtras. +Set Default Proof Using "Type". + (** * VLSM Basics This module provides basic VLSM infrastructure. @@ -2767,7 +2769,7 @@ Proof. by subst. Qed. Lemma same_VLSM_initial_message_preservation m : vinitial_message_prop X1 m -> vinitial_message_prop X2 m. -Proof. by subst. Qed. +Proof using Heq. by subst. Qed. End sec_same_VLSM. @@ -2848,7 +2850,7 @@ Lemma history_unique_trace_to_reachable : forall is s tr, finite_valid_trace_init_to R is s tr -> forall is' tr', finite_valid_trace_init_to R is' s tr' -> is' = is /\ tr' = tr. -Proof. +Proof using H. intros is s tr Htr; induction Htr using finite_valid_trace_init_to_rev_ind; intros is' tr' [Htr' His']. - destruct_list_last tr' tr'' item Heqtr'; [by inversion Htr' | subst]. diff --git a/theories/VLSM/Core/VLSMProjections.v b/theories/VLSM/Core/VLSMProjections.v index ab0e04c7..f5f5233a 100644 --- a/theories/VLSM/Core/VLSMProjections.v +++ b/theories/VLSM/Core/VLSMProjections.v @@ -6,6 +6,8 @@ From VLSM.Core Require Export VLSMPartialProjection VLSMStutteringEmbedding. From VLSM.Core Require Export VLSMTotalProjection VLSMEmbedding. From VLSM.Core Require Export VLSMInclusion VLSMEquality. +Set Default Proof Using "Type". + (** * VLSM Projection Properties *) Section sec_same_VLSM_embedding. diff --git a/theories/VLSM/Core/Validator.v b/theories/VLSM/Core/Validator.v index b11c97e8..36ab83d1 100644 --- a/theories/VLSM/Core/Validator.v +++ b/theories/VLSM/Core/Validator.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From VLSM.Core Require Import VLSM VLSMProjections Composition. +Set Default Proof Using "Type". + (** * VLSM Projection Validators In the sequel we fix VLSMs <> and <> and some <> @@ -300,7 +302,7 @@ Context Lemma projection_induced_valid_message_char : forall om, option_valid_message_prop projection_induced_validator om -> option_valid_message_prop X om. -Proof. +Proof using Htransition_consistency Htransition_Some Hstate_lift Hlabel_lift. intros om [s Hsom]. induction Hsom. - by destruct om as [m |]; [done |]; apply option_valid_message_None. @@ -322,7 +324,7 @@ Context Lemma projection_induced_validator_is_projection : VLSM_projection X pre_projection_induced_validator label_project state_project. -Proof. +Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hlabel_lift. apply basic_VLSM_projection; intro; intros. - by exists lX, s. - specialize (Htransition_Some _ _ H _ _ _ _ H0); cbn. @@ -344,7 +346,7 @@ Lemma induced_validator_transition_item_lift : pre_VLSM_projection_transition_item_project _ _ label_project state_project (pre_VLSM_embedding_transition_item_project _ _ label_lift state_lift item) = Some item. -Proof. +Proof using Hstate_lift Hlabel_lift. destruct item. unfold pre_VLSM_embedding_transition_item_project, pre_VLSM_projection_transition_item_project. @@ -356,7 +358,7 @@ Lemma induced_validator_trace_lift : pre_VLSM_projection_finite_trace_project _ _ label_project state_project (pre_VLSM_embedding_finite_trace_project _ _ label_lift state_lift tr) = tr. -Proof. +Proof using Hstate_lift Hlabel_lift. induction tr; cbn; [done |]. by rewrite induced_validator_transition_item_lift; f_equal. Qed. @@ -423,7 +425,7 @@ Lemma projection_induced_validator_incl (Htransition_consistency2 : induced_validator_transition_consistency_Some X2 TY label_project state_project) : VLSM_incl X1 X2 -> VLSM_incl XY1 XY2. -Proof. +Proof using Hstate_lift Hlabel_lift. pose (Htransition_Some1 := basic_weak_projection_transition_consistency_Some X1 TY _ _ _ _ Hlabel_lift Hstate_lift Htransition_consistency1). @@ -479,7 +481,7 @@ Lemma projection_induced_validator_eq (Htransition_consistency2 : induced_validator_transition_consistency_Some X2 TY label_project state_project) : VLSM_eq X1 X2 -> VLSM_eq XY1 XY2. -Proof. +Proof using Hstate_lift Hlabel_lift. intro Heq; apply VLSM_eq_incl_iff; split. - by apply (projection_induced_validator_incl MX1 MX2); [.. | apply VLSM_eq_proj1]. - by apply (projection_induced_validator_incl MX2 MX1); [.. | apply VLSM_eq_proj2]. @@ -530,7 +532,7 @@ Context Lemma projection_induced_valid_transition_eq : forall l s om, vvalid Xi l (s, om) -> vtransition Xi l (s, om) = vtransition Y l (s, om). -Proof. +Proof using Htransition_consistency Htransition_None Hstate_lift Hproji Hproj Hlabel_lift. intros l s im (lX & sX & [Hlx HsX Hv]); cbn in HsX; subst s. replace (vtransition Y _ _) with (state_project (vtransition X lX (sX, im)).1, (vtransition X lX (sX, im)).2). @@ -543,7 +545,7 @@ Qed. Lemma induced_validator_incl_preloaded_with_all_messages : VLSM_incl Xi PreY. -Proof. +Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift. apply basic_VLSM_incl. - by intros is (s & <- & Hs); apply (VLSM_projection_initial_state Hproj). - by intros l s m Hv HsY HmX; apply initial_message_is_valid. @@ -574,7 +576,7 @@ Definition projection_validator_prop_alt := Lemma validator_alt_free_states_are_projection_states : projection_validator_prop_alt -> forall s, valid_state_prop PreY s -> valid_state_prop Xi s. -Proof. +Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift. intros Hvalidator sY Hs. induction Hs using valid_state_prop_ind. - apply initial_state_is_valid. @@ -598,7 +600,7 @@ Qed. (** Below we show that the two definitions above are actually equivalent. *) Lemma projection_validator_prop_alt_iff : projection_validator_prop_alt <-> projection_validator_prop Y label_project state_project. -Proof. +Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift. split; intros Hvalidator l si om Hvalid. - apply Hvalidator; [by apply Hvalid |]. by apply validator_alt_free_states_are_projection_states; [.. | apply Hvalid]. @@ -612,7 +614,7 @@ Qed. Lemma validator_free_states_are_projection_states : projection_validator_prop Y label_project state_project -> forall s, valid_state_prop PreY s -> valid_state_prop Xi s. -Proof. +Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift. rewrite <- projection_validator_prop_alt_iff by done. by apply validator_alt_free_states_are_projection_states. Qed. @@ -631,7 +633,7 @@ Context *) Lemma pre_loaded_with_all_messages_validator_proj_incl : VLSM_incl PreY Xi. -Proof. +Proof using Hvalidator Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift. (* reduce inclusion to inclusion of finite traces. *) apply VLSM_incl_finite_traces_characterization. intros sY trY HtrY. @@ -661,7 +663,7 @@ Qed. *) Lemma pre_loaded_with_all_messages_validator_proj_eq : VLSM_eq PreY Xi. -Proof. +Proof using Hvalidator Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift. apply VLSM_eq_incl_iff; split. - by apply pre_loaded_with_all_messages_validator_proj_incl. - by apply induced_validator_incl_preloaded_with_all_messages. @@ -973,7 +975,7 @@ Context Lemma pre_loaded_with_all_messages_self_validator_vlsm_incl : VLSM_incl PreX X. -Proof. +Proof using Hvalidator. unfold self_validator_vlsm_prop in Hvalidator. destruct X as (T & M). simpl in *. (* redcuction to inclusion of finite traces. *) @@ -997,7 +999,7 @@ Qed. Lemma pre_loaded_with_all_messages_self_validator_vlsm_eq : VLSM_eq PreX X. -Proof. +Proof using Hvalidator. split. - by apply pre_loaded_with_all_messages_self_validator_vlsm_incl. - pose (vlsm_incl_pre_loaded_with_all_messages_vlsm X) as Hincl. diff --git a/theories/VLSM/Lib/Ctauto.v b/theories/VLSM/Lib/Ctauto.v index 1ec32072..52b74f7b 100644 --- a/theories/VLSM/Lib/Ctauto.v +++ b/theories/VLSM/Lib/Ctauto.v @@ -1,5 +1,7 @@ From Cdcl Require Export Itauto. +Set Default Proof Using "Type". + (** * Classical Itauto tactic *) Ltac gen_conflicts tac := diff --git a/theories/VLSM/Lib/EquationsExtras.v b/theories/VLSM/Lib/EquationsExtras.v index 03d008cc..60fe92a4 100644 --- a/theories/VLSM/Lib/EquationsExtras.v +++ b/theories/VLSM/Lib/EquationsExtras.v @@ -1,5 +1,7 @@ From Equations Require Export Equations. +Set Default Proof Using "Type". + (** * Equations utility definitions The definition of [inspect] is available in Equations as of version 1.3+8.16. diff --git a/theories/VLSM/Lib/FinExtras.v b/theories/VLSM/Lib/FinExtras.v index 3127e53a..5671beb2 100644 --- a/theories/VLSM/Lib/FinExtras.v +++ b/theories/VLSM/Lib/FinExtras.v @@ -1,5 +1,7 @@ From stdpp Require Import prelude. +Set Default Proof Using "Type". + (** * Finite type utility definitions and lemmas *) Fixpoint up_to_n_listing diff --git a/theories/VLSM/Lib/FinFunExtras.v b/theories/VLSM/Lib/FinFunExtras.v index dee9d20c..3d51c30f 100644 --- a/theories/VLSM/Lib/FinFunExtras.v +++ b/theories/VLSM/Lib/FinFunExtras.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude finite. From Coq Require Import FinFun. From VLSM.Lib Require Import Preamble ListExtras StdppExtras. +Set Default Proof Using "Type". + (** * Finite function utility definitions and lemmas *) Lemma listing_from_finite (A : Type) `{finite.Finite A} : Listing (enum A). diff --git a/theories/VLSM/Lib/FinSetExtras.v b/theories/VLSM/Lib/FinSetExtras.v index 67c0fdf7..5a757d7e 100644 --- a/theories/VLSM/Lib/FinSetExtras.v +++ b/theories/VLSM/Lib/FinSetExtras.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble. +Set Default Proof Using "Type". + (** * Finite set utility definitions and lemmas *) Section sec_fin_set. @@ -13,12 +15,12 @@ Section sec_general. Lemma elements_subseteq (X Y : C) : X ⊆ Y -> elements X ⊆ elements Y. -Proof. by set_solver. Qed. +Proof using H6 H4 H3 H2 H1 H0 EqDecision0. by set_solver. Qed. Lemma union_size_ge_size1 (X Y : C) : size (X ∪ Y) >= size X. -Proof. +Proof using H6 H4 H3 H1 H0 H EqDecision0. apply subseteq_size. apply subseteq_union. by set_solver. @@ -27,7 +29,7 @@ Qed. Lemma union_size_ge_size2 (X Y : C) : size (X ∪ Y) >= size Y. -Proof. +Proof using H6 H4 H3 H1 H0 H EqDecision0. apply subseteq_size. apply subseteq_union. by set_solver. @@ -36,7 +38,7 @@ Qed. Lemma union_size_ge_average (X Y : C) : 2 * size (X ∪ Y) >= size X + size Y. -Proof. +Proof using H6 H4 H3 H1 H0 H EqDecision0. specialize (union_size_ge_size1 X Y) as Hx. specialize (union_size_ge_size2 X Y) as Hy. by lia. @@ -45,7 +47,7 @@ Qed. Lemma difference_size_le_self (X Y : C) : size (X ∖ Y) <= size X. -Proof. +Proof using H6 H3 H2 H1 H0 H EqDecision0. apply subseteq_size. apply elem_of_subseteq. intros x Hx. @@ -56,7 +58,7 @@ Qed. Lemma union_size_le_sum (X Y : C) : size (X ∪ Y) <= size X + size Y. -Proof. +Proof using H6 H4 H3 H1 H0 H EqDecision0. specialize (size_union_alt X Y) as Halt. rewrite Halt. specialize (difference_size_le_self Y X). @@ -66,7 +68,7 @@ Qed. Lemma intersection_size1 (X Y : C) : size (X ∩ Y) <= size X. -Proof. +Proof using H6 H4 H2 H1 H0 H EqDecision0. apply (subseteq_size (X ∩ Y) X). by set_solver. Qed. @@ -74,7 +76,7 @@ Qed. Lemma intersection_size2 (X Y : C) : size (X ∩ Y) <= size Y. -Proof. +Proof using H6 H4 H2 H1 H0 H EqDecision0. apply (subseteq_size (X ∩ Y) Y). by set_solver. Qed. @@ -83,7 +85,7 @@ Lemma difference_size_subset (X Y : C) (Hsub : Y ⊆ X) : (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size Y))%Z. -Proof. +Proof using H6 H3 H2 H1 H0 EqDecision0. assert (Htemp : Y ∪ (X ∖ Y) ≡ X). { apply set_equiv_equivalence. @@ -114,14 +116,14 @@ Qed. Lemma difference_with_intersection (X Y : C) : X ∖ Y ≡ X ∖ (X ∩ Y). -Proof. +Proof using H6 H5 H2 H1 H0 EqDecision0. by set_solver. Qed. Lemma difference_size (X Y : C) : (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z. -Proof. +Proof using H6 H2 H1 H0 H EqDecision0. rewrite difference_with_intersection. specialize (difference_size_subset X (X ∩ Y)) as Hdif. by set_solver. @@ -130,7 +132,7 @@ Qed. Lemma difference_size_ge_disjoint_case (X Y : C) : size (X ∖ Y) >= size X - size Y. -Proof. +Proof using H6 H3 H2 H1 H0 H EqDecision0. specialize (difference_size X Y). specialize (intersection_size2 X Y). by lia. @@ -139,7 +141,7 @@ Qed. Lemma list_to_set_size (l : list A) : size (list_to_set l (C := C)) <= length l. -Proof. +Proof using H6 H4 H3 H EqDecision0. induction l; cbn. - by rewrite size_empty; lia. - specialize (union_size_le_sum ({[ a ]}) (list_to_set l)) as Hun_size. @@ -159,7 +161,7 @@ Context Lemma filter_subset (Hsub : X ⊆ Y) : filter P X ⊆ filter P Y. -Proof. +Proof using H6 H4 H3 EqDecision0. intros a HaX. apply elem_of_filter in HaX. apply elem_of_filter. @@ -169,7 +171,7 @@ Qed. Lemma filter_subprop (Hsub : forall a, (P a -> P2 a)) : filter P X ⊆ filter P2 X. -Proof. +Proof using H6 H4 H3 EqDecision0. intros a HaP. apply elem_of_filter in HaP. apply elem_of_filter. @@ -191,7 +193,7 @@ Lemma set_map_subset (X Y : C) (Hsub : X ⊆ Y) : set_map (D := D) f X ⊆ set_map (D := D) f Y. -Proof. +Proof using H6 H4 H3 H2 H14 H13 H12 H11 H1 H0 EqDecision1 EqDecision0. intros a Ha. apply elem_of_map in Ha. apply elem_of_map. @@ -202,7 +204,7 @@ Lemma set_map_size_upper_bound (f : A -> B) (X : C) : size (set_map (D := D) f X) <= size X. -Proof. +Proof using H7 H14 H12 H11 EqDecision1. unfold set_map. remember (f <$> elements X) as fX. set (x := size (list_to_set _)). @@ -215,7 +217,7 @@ Qed. Lemma elem_of_set_map_inj (f : A -> B) `{!Inj (=) (=) f} (a : A) (X : C) : f a ∈@{D} fin_sets.set_map f X <-> a ∈ X. -Proof. +Proof using H6 H4 H3 H2 H14 H13 H12 H11 H1 H0 EqDecision1 EqDecision0. intros; rewrite elem_of_map. split; [| by eexists]. intros (_v & HeqAv & H_v). @@ -224,6 +226,6 @@ Proof. Qed. Lemma set_map_id (X : C) : X ≡ set_map id X. -Proof. by set_solver. Qed. +Proof using H9 H8 H7 H6 H4 H3 H14 H13 H12 H11 H10 EqDecision1 EqDecision0 D B. by set_solver. Qed. End sec_map. diff --git a/theories/VLSM/Lib/Itauto.v b/theories/VLSM/Lib/Itauto.v index 468d0408..ac21ec77 100644 --- a/theories/VLSM/Lib/Itauto.v +++ b/theories/VLSM/Lib/Itauto.v @@ -1,5 +1,7 @@ From Cdcl Require Export Itauto. +Set Default Proof Using "Type". + (** * Constructive Itauto tactic *) Ltac gen_conflicts tac := diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v index d795e9b4..98c05fd2 100644 --- a/theories/VLSM/Lib/ListExtras.v +++ b/theories/VLSM/Lib/ListExtras.v @@ -3,6 +3,8 @@ From stdpp Require Import finite. From Coq Require Import FinFun. From VLSM.Lib Require Import Preamble. +Set Default Proof Using "Type". + (** * Utility lemmas about lists *) (** A list is empty if it has no members. *) diff --git a/theories/VLSM/Lib/ListFinSetExtras.v b/theories/VLSM/Lib/ListFinSetExtras.v index 57f3f021..6695ac41 100644 --- a/theories/VLSM/Lib/ListFinSetExtras.v +++ b/theories/VLSM/Lib/ListFinSetExtras.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble StdppListFinSet. +Set Default Proof Using "Type". + Section sec_defs. Context `{FinSet A C}. @@ -20,11 +22,11 @@ Definition set_diff (x y : set) : set := x ∖ y. Lemma set_union_subseteq_left : forall (s1 s2 : set), s1 ⊆ set_union s1 s2. -Proof. by intros s1 s2 x Hincl; apply set_union_intro; left. Qed. +Proof using H6 H5 H4 H3 H1 H0 EqDecision0. by intros s1 s2 x Hincl; apply set_union_intro; left. Qed. Lemma set_union_subseteq_iff : forall (s1 s2 s : set), set_union s1 s2 ⊆ s <-> s1 ⊆ s /\ s2 ⊆ s. -Proof. +Proof using H6 H5 H4 H3 H1 H0 EqDecision0. intros s1 s2 s. unfold subseteq, set_subseteq_instance, set_subseteq_instance. setoid_rewrite set_union_iff. @@ -37,7 +39,7 @@ Proof. by intros a s1 s2 Ha Hincl; apply Hincl. Qed. Lemma empty_subseteq : forall (s : set), ∅ ⊆ s. -Proof. by intros s x Hin; contradict Hin; apply not_elem_of_empty. Qed. +Proof using H6 H5 H4 H3 H2 H1 EqDecision0. by intros s x Hin; contradict Hin; apply not_elem_of_empty. Qed. #[export] Instance elem_of_dec : RelDecision (@elem_of A C _) := elem_of_dec_slow. diff --git a/theories/VLSM/Lib/ListSetExtras.v b/theories/VLSM/Lib/ListSetExtras.v index 390c4413..d9d97a87 100644 --- a/theories/VLSM/Lib/ListSetExtras.v +++ b/theories/VLSM/Lib/ListSetExtras.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble ListExtras StdppExtras StdppListSet. +Set Default Proof Using "Type". + (** * List set utility definitions and lemmas *) Definition set_eq {A} (s1 s2 : set A) : Prop := diff --git a/theories/VLSM/Lib/Measurable.v b/theories/VLSM/Lib/Measurable.v index 41f3a53f..14b5c25d 100644 --- a/theories/VLSM/Lib/Measurable.v +++ b/theories/VLSM/Lib/Measurable.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From Coq Require Import Reals Lra. From VLSM.Lib Require Import Preamble ListExtras StdppListSet StdppListFinSet. +Set Default Proof Using "Type". + (** * Measure-related definitions and lemmas *) Definition pos_R := {r : R | (r > 0)%R}. @@ -29,7 +31,7 @@ Proof. done. Qed. Lemma sum_weights_empty : forall (l : Cv), l ≡ ∅ -> sum_weights l = 0%R. -Proof. +Proof using H7 H5 H4 H3 H2 EqDecision0. intros l Hl. unfold sum_weights, set_fold; cbn. by apply elements_empty_iff in Hl as ->. @@ -80,7 +82,7 @@ Lemma sum_weights_subseteq_list NoDup vs' -> vs ⊆ vs' -> (sum_weights_list vs <= sum_weights_list vs')%R. -Proof. +Proof using EqDecision0. induction vs; intros vs' Hnodup_vs Hnodup_vs' Hincl; [by apply sum_weights_positive_list |]. pose proof (Hvs' := sum_weights_in_list a vs' Hnodup_vs'). @@ -100,7 +102,7 @@ Lemma sum_weights_subseteq : forall (vs vs' : Cv), vs ⊆ vs' -> (sum_weights vs <= sum_weights vs')%R. -Proof. +Proof using H7 H5 H4 H3 H2 H1 EqDecision0. intros vs vs' Hincl. rewrite !sum_weights_list_rew. apply sum_weights_subseteq_list. @@ -110,7 +112,7 @@ Proof. Qed. Lemma sum_weights_proper : Proper (equiv ==> eq) sum_weights. -Proof. +Proof using H7 H5 H4 H3 H2 H1 EqDecision0. intros x y Hequiv. by apply Rle_antisym; apply sum_weights_subseteq; intro a; apply Hequiv. Qed. @@ -118,7 +120,7 @@ Qed. Lemma sum_weights_in : forall v (vs : Cv), v ∈ vs -> sum_weights vs = (proj1_sig (weight v) + sum_weights (set_remove v vs))%R. -Proof. +Proof using H7 H4 H3 H1 EqDecision0. intros v vs Hv. rewrite sum_weights_list_rew, sum_weights_in_list with (v := v); cycle 1. - by apply NoDup_elements. @@ -159,7 +161,7 @@ Lemma sum_weights_disj_union : forall (vs vs' : Cv), vs ## vs' -> sum_weights (vs ∪ vs') = (sum_weights vs + sum_weights vs')%R. -Proof. +Proof using H7 H5 H4 H2 H1 EqDecision0. intros vs vs' Hdisj. apply elements_disj_union, sum_weights_list_permutation_proper in Hdisj. setoid_rewrite Hdisj. @@ -168,7 +170,7 @@ Qed. Lemma sum_weights_union_empty (vs : Cv) : sum_weights (vs ∪ ∅) = sum_weights vs. -Proof. +Proof using H7 H5 H4 H2 H0 EqDecision0. rewrite sum_weights_disj_union by apply disjoint_empty_r. by rewrite (sum_weights_empty ∅); [lra |]. Qed. diff --git a/theories/VLSM/Lib/NatExtras.v b/theories/VLSM/Lib/NatExtras.v index c1d5ef43..2a308511 100644 --- a/theories/VLSM/Lib/NatExtras.v +++ b/theories/VLSM/Lib/NatExtras.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From VLSM.Lib Require Import EquationsExtras. From VLSM.Lib Require Import Preamble. +Set Default Proof Using "Type". + (** * Natural number utility definitions and lemmas Given a decidable property on naturals and a bound, finds the diff --git a/theories/VLSM/Lib/NeList.v b/theories/VLSM/Lib/NeList.v index 397611f6..eca8cd16 100644 --- a/theories/VLSM/Lib/NeList.v +++ b/theories/VLSM/Lib/NeList.v @@ -1,6 +1,8 @@ From stdpp Require Import prelude. From VLSM.Lib Require Import ListExtras StdppExtras. +Set Default Proof Using "Type". + (** A straight-forward inductive definition of non-empty lists. *) Inductive ne_list (A : Type) : Type := | nel_singl : A -> ne_list A diff --git a/theories/VLSM/Lib/Preamble.v b/theories/VLSM/Lib/Preamble.v index dfd89b02..f78610a4 100644 --- a/theories/VLSM/Lib/Preamble.v +++ b/theories/VLSM/Lib/Preamble.v @@ -3,6 +3,8 @@ Obligation Tactic := idtac. From stdpp Require Import prelude. From Coq Require Import Eqdep_dec. +Set Default Proof Using "Type". + (** * General utility definitions, lemmas, and tactics *) Tactic Notation "spec" hyp(H) := @@ -217,7 +219,7 @@ Proof. by induction n; cbn; [| case_decide]; lia. Qed. #[local] Lemma find_least_among_helper_has_property : forall n, P (find_least_among_helper n). -Proof. by induction n; cbn; [| case_decide]. Qed. +Proof using Hbound. by induction n; cbn; [| case_decide]. Qed. #[local] Lemma find_least_among_helper_minimal : forall n m, @@ -235,7 +237,7 @@ Qed. minimal_among le (fun m => bound - n <= m <= bound /\ P m) (find_least_among_helper n). -Proof. +Proof using Hbound. split; [split |]. - by apply find_least_among_helper_bounded. - by apply find_least_among_helper_has_property. @@ -246,7 +248,7 @@ Qed. Lemma find_least_among_is_minimal : minimal_among le P find_least_among. -Proof. +Proof using Hbound. destruct (find_least_among_helper_is_minimal bound) as [[[_ ?] ?] Hmin']. split; [done |]. intros; apply Hmin'; [| done]. diff --git a/theories/VLSM/Lib/RealsExtras.v b/theories/VLSM/Lib/RealsExtras.v index 372e9992..b364badf 100644 --- a/theories/VLSM/Lib/RealsExtras.v +++ b/theories/VLSM/Lib/RealsExtras.v @@ -1,6 +1,8 @@ From Coq Require Import Reals. From stdpp Require Import prelude. +Set Default Proof Using "Type". + (** * Real number utility definitions and lemmas *) (** Sum a list of real numbers. *) diff --git a/theories/VLSM/Lib/SortedLists.v b/theories/VLSM/Lib/SortedLists.v index ab4a3791..e50e6f18 100644 --- a/theories/VLSM/Lib/SortedLists.v +++ b/theories/VLSM/Lib/SortedLists.v @@ -3,6 +3,8 @@ From stdpp Require Import prelude. From Coq Require Import Sorting. From VLSM.Lib Require Import Preamble ListExtras ListSetExtras. +Set Default Proof Using "Type". + (** * Sorted list utility functions and lemmas *) Fixpoint list_compare {A} (compare : A -> A -> comparison) diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v index a305f3c4..08e03963 100644 --- a/theories/VLSM/Lib/StdppExtras.v +++ b/theories/VLSM/Lib/StdppExtras.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble ListExtras. +Set Default Proof Using "Type". + (** * Std++ Related Results *) Lemma elem_of_take {A : Type} (l : list A) (n : nat) (x : A) : diff --git a/theories/VLSM/Lib/StdppListFinSet.v b/theories/VLSM/Lib/StdppListFinSet.v index 8772468b..2a7851be 100644 --- a/theories/VLSM/Lib/StdppListFinSet.v +++ b/theories/VLSM/Lib/StdppListFinSet.v @@ -1,6 +1,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. +Set Default Proof Using "Type". + (** * Finite set implementation of a list set interface *) Section sec_fst_defs. @@ -21,14 +23,14 @@ Definition set_diff (x y : set) : set := x ∖ y. Lemma set_add_intro1 : forall (a b : A) (x : set), a ∈ x -> a ∈ set_add b x. -Proof. +Proof using H6 H5 H4 H3 H0 EqDecision0. unfold set_add; intros a b x Hab. by apply elem_of_union; right. Qed. Lemma set_add_intro2 : forall (a b : A) (x : set), a = b -> a ∈ set_add b x. -Proof. +Proof using H6 H5 H4 H3 H0 EqDecision0. unfold set_add; intros a b x Hab. by rewrite elem_of_union, elem_of_singleton; left. Qed. @@ -37,21 +39,21 @@ Qed. Lemma set_add_intro : forall (a b : A) (x : set), a = b \/ a ∈ x -> a ∈ set_add b x. -Proof. +Proof using H6 H5 H4 H3 H0 EqDecision0. unfold set_add; intros a b x Hab. by rewrite elem_of_union, elem_of_singleton. Qed. Lemma set_add_elim : forall (a b : A) (x : set), a ∈ set_add b x -> a = b \/ a ∈ x. -Proof. +Proof using H6 H5 H4 H3 H0 EqDecision0. unfold set_add; intros a b x Hab. by rewrite elem_of_union, elem_of_singleton in Hab. Qed. Lemma set_add_not_empty : forall (a : A) (x : set), ¬ set_add a x ≡ ∅. -Proof. +Proof using H6 H5 H4 H3 EqDecision0. unfold set_add; intros a x Hcontra. cut (a ∈@{C} ∅); [by apply not_elem_of_empty |]. by rewrite <- Hcontra, elem_of_union, elem_of_singleton; left. @@ -59,7 +61,7 @@ Qed. Lemma set_add_iff a b l : a ∈ set_add b l <-> a = b \/ a ∈ l. -Proof. +Proof using H6 H5 H4 H3 H0 EqDecision0. split. - by apply set_add_elim. - by apply set_add_intro. @@ -67,14 +69,14 @@ Qed. Lemma set_remove_1 (a b : A) (l : set) : a ∈ set_remove b l -> a ∈ l. -Proof. +Proof using H6 H5 H3 H2 H0 EqDecision0. unfold set_remove; intros Habl. by apply elem_of_difference in Habl as [Hl Hnb]. Qed. Lemma set_remove_2 (a b : A) (l : set) : a ∈ set_remove b l -> a <> b. -Proof. +Proof using H6 H5 H3 H2 H0 EqDecision0. unfold set_remove; intros Habl. rewrite elem_of_difference, elem_of_singleton in Habl. by destruct Habl. @@ -82,14 +84,14 @@ Qed. Lemma set_remove_3 (a b : A) (l : set) : a ∈ l -> a <> b -> a ∈ set_remove b l. -Proof. +Proof using H6 H5 H3 H2 H0 EqDecision0. intros Hl Hnb; unfold set_remove. by rewrite elem_of_difference, elem_of_singleton. Qed. Lemma set_remove_iff (a b : A) (l : set) : a ∈ set_remove b l <-> a ∈ l /\ a <> b. -Proof. +Proof using H6 H5 H3 H2 H0 EqDecision0. split; [split |]. - by eapply set_remove_1. - by eapply set_remove_2. @@ -99,20 +101,20 @@ Qed. Lemma set_union_intro : forall (a : A) (x y : set), a ∈ x \/ a ∈ y -> a ∈ set_union x y. -Proof. +Proof using H6 H5 H4 H3 H1 H0 EqDecision0. by intros; apply elem_of_union. Qed. Lemma set_union_elim : forall (a : A) (x y : set), a ∈ set_union x y -> a ∈ x \/ a ∈ y. -Proof. +Proof using H6 H5 H4 H3 H1 H0 EqDecision0. by intros; apply elem_of_union. Qed. Lemma set_union_iff a l l' : a ∈ set_union l l' <-> a ∈ l \/ a ∈ l'. -Proof. +Proof using H6 H5 H4 H3 H1 H0 EqDecision0. split. - by apply set_union_elim. - by apply set_union_intro. @@ -121,28 +123,28 @@ Qed. Lemma set_diff_intro : forall (a : A) (x y : set), a ∈ x -> a ∉ y -> a ∈ set_diff x y. -Proof. +Proof using H6 H5 H3 H2 H1 H0 EqDecision0. by intros; apply elem_of_difference. Qed. Lemma set_diff_elim1 : forall (a : A) (x y : set), a ∈ set_diff x y -> a ∈ x. -Proof. +Proof using H6 H5 H3 H2 H1 H0 EqDecision0. unfold set_diff; intros a x y Hxy. by apply elem_of_difference in Hxy as [Hx _]. Qed. Lemma set_diff_elim2 : forall (a : A) (x y : set), a ∈ set_diff x y -> a ∉ y. -Proof. +Proof using H6 H5 H3 H2 H1 H0 EqDecision0. unfold set_diff; intros a x y Hxy. by apply elem_of_difference in Hxy as [_ Hny]. Qed. Lemma set_diff_iff a l l' : a ∈ set_diff l l' <-> a ∈ l /\ a ∉ l'. -Proof. +Proof using H6 H5 H3 H2 H1 H0 EqDecision0. split. - by eauto using set_diff_elim1, set_diff_elim2. - by intros []; apply set_diff_intro. diff --git a/theories/VLSM/Lib/StdppListSet.v b/theories/VLSM/Lib/StdppListSet.v index ad3d8129..0f0c9384 100644 --- a/theories/VLSM/Lib/StdppListSet.v +++ b/theories/VLSM/Lib/StdppListSet.v @@ -1,6 +1,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. +Set Default Proof Using "Type". + Section sec_fst_defs. Context `{EqDecision A}. diff --git a/theories/VLSM/Lib/StreamExtras.v b/theories/VLSM/Lib/StreamExtras.v index 775f33b0..34515d2d 100644 --- a/theories/VLSM/Lib/StreamExtras.v +++ b/theories/VLSM/Lib/StreamExtras.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From Coq Require Import Streams Sorted. From VLSM.Lib Require Import Preamble ListExtras StdppExtras SortedLists NeList. +Set Default Proof Using "Type". + (** * Stream utility definitions and lemmas *) Lemma stream_eq_hd_tl {A} (s s' : Stream A) : diff --git a/theories/VLSM/Lib/StreamFilters.v b/theories/VLSM/Lib/StreamFilters.v index d1d629af..f4b110ff 100644 --- a/theories/VLSM/Lib/StreamFilters.v +++ b/theories/VLSM/Lib/StreamFilters.v @@ -2,6 +2,8 @@ From stdpp Require Import prelude. From Coq Require Import Streams Sorted. From VLSM.Lib Require Import Preamble StreamExtras SortedLists ListExtras StdppExtras NeList. +Set Default Proof Using "Type". + (** Given a predicate <

> and a stream <>, a stream of naturals <> determines a [filtering_subsequence] for <

> on <> if it corresponds to @@ -377,7 +379,7 @@ Fixpoint stream_filter_fst_pos (n : nat) {struct Hev} : nat * Stream A. -Proof. +Proof using Pdec. refine (match decide (P (hd s)) with | left p => (n, tl s) diff --git a/theories/VLSM/Lib/Temporal.v b/theories/VLSM/Lib/Temporal.v index 9e01d251..5120be0e 100644 --- a/theories/VLSM/Lib/Temporal.v +++ b/theories/VLSM/Lib/Temporal.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From Coq Require Import Streams Classical. +Set Default Proof Using "Type". + (** * Temporal Logic Predicates and Results *) Set Implicit Arguments. diff --git a/theories/VLSM/Lib/TopSort.v b/theories/VLSM/Lib/TopSort.v index 54bcf69d..d86f86ca 100644 --- a/theories/VLSM/Lib/TopSort.v +++ b/theories/VLSM/Lib/TopSort.v @@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble ListExtras ListSetExtras StdppListSet StdppExtras. +Set Default Proof Using "Type". + (** * Topological sorting implementation This module implements an algorithm producing a linear extension for a @@ -131,7 +133,7 @@ Lemma precedes_irreflexive (a : A) (Ha : P a) : ~ precedes a a. -Proof. +Proof using RelDecision0 Hso. specialize (StrictOrder_Irreflexive (exist P a Ha)). unfold complement; unfold precedes_P; simpl; intro Hirr. by destruct (decide (precedes a a)). @@ -143,7 +145,7 @@ Lemma precedes_asymmetric (Hb : P b) (Hab : precedes a b) : ~ precedes b a. -Proof. +Proof using Hso. intro Hba. exact (StrictOrder_Asymmetric Hso @@ -159,7 +161,7 @@ Lemma precedes_transitive (Hab : precedes a b) (Hbc : precedes b c) : precedes a c. -Proof. +Proof using Hso. exact (RelationClasses.StrictOrder_Transitive (exist P a Ha) (exist P b Hb) (exist P c Hc) @@ -173,7 +175,7 @@ Qed. Lemma count_predecessors_zero (Hl : l <> []) : Exists (fun a => count_predecessors a = 0) l. -Proof. +Proof using P Hso HPl. unfold count_predecessors. induction l; [done |]. inversion_clear HPl as [| ? ? HPa HPl0]. @@ -214,7 +216,7 @@ Lemma min_predecessors_zero (Hl : l = a :: l') (min := min_predecessors l' a) : count_predecessors min = 0. -Proof. +Proof using P Hso HPl. assert (Hl' : l <> []) by (intro H; rewrite Hl in H; inversion H). specialize (count_predecessors_zero Hl'); intro Hx. apply Exists_exists in Hx. destruct Hx as [x [Hinx Hcountx]]. @@ -300,7 +302,7 @@ Lemma topologically_sorted_occurrences_ordering (lb1 lb2 : list A) (Heqb : l = lb1 ++ [b] ++ lb2) : exists (lab : list A), lb1 = la1 ++ a :: lab. -Proof. +Proof using RelDecision0 P Hts Hso Hl. assert (Hpa : P a). { rewrite Forall_forall in Hl. apply Hl. rewrite Heqa, !elem_of_app, elem_of_list_singleton. auto. } specialize (Hts a b Hab lb1 lb2 Heqb). @@ -325,7 +327,7 @@ Corollary top_sort_before (l1 l2 : list A) (Heq : l = l1 ++ [b] ++ l2) : a ∈ l1. -Proof. +Proof using RelDecision0 P Hts Hso Hl. apply elem_of_list_split in Ha. destruct Ha as [la1 [la2 Ha]]. specialize (topologically_sorted_occurrences_ordering a b Hab la1 la2 Ha l1 l2 Heq). @@ -343,7 +345,7 @@ Corollary top_sort_precedes (Ha : a ∈ l) (Hb : b ∈ l) : exists l1 l2 l3, l = l1 ++ [a] ++ l2 ++ [b] ++ l3. -Proof. +Proof using RelDecision0 P Hts Hso Hl. apply elem_of_list_split in Hb. destruct Hb as [l12 [l3 Hb']]. specialize (top_sort_before a b Hab Ha l12 l3 Hb'). @@ -550,7 +552,7 @@ Context <>, [top_sort] <> is [topologically_sorted]. *) Lemma top_sort_sorted : topologically_sorted precedes (top_sort l). -Proof. +Proof using P Hso Hl. intro a; intros. intro Ha2. assert (Ha : a ∈ l). @@ -638,7 +640,7 @@ Definition topological_sorting set_eq l lts /\ topologically_sorted precedes lts. Corollary top_sort_correct : topological_sorting l (top_sort l). -Proof. +Proof using P Hso Hl. split. - by apply top_sort_set_eq. - by apply top_sort_sorted. @@ -652,7 +654,7 @@ Lemma maximal_element_in (a : A) (Hmax : get_maximal_element = Some a) : a ∈ l. -Proof. +Proof using P Hso Hl. unfold get_maximal_element in Hmax. assert (exists l', l' ++ [a] = top_sort l). { @@ -681,7 +683,7 @@ Lemma get_maximal_element_correct (Hina : a ∈ l) (Hmax : get_maximal_element = Some max) : ~ precedes max a. -Proof. +Proof using P Hso Hl. specialize top_sort_correct as [Hseteq Htop]. unfold topologically_sorted in Htop. intros contra. @@ -721,7 +723,7 @@ Qed. Lemma get_maximal_element_some (Hne : l <> []) : exists a, get_maximal_element = Some a. -Proof. +Proof using P Hl. unfold get_maximal_element. destruct l; cbn; [by congruence |]. exists (List.last @@ -762,14 +764,14 @@ Corollary simple_topologically_sorted_precedes_closed_remove_last (Hinit : l = init ++ [final]) (Hpc : precedes_closed precedes l) : precedes_closed precedes init. -Proof. +Proof using StrictOrder0. by eapply topologically_sorted_precedes_closed_remove_last; [typeclasses eauto | apply Forall_True | ..]. Qed. Corollary simple_top_sort_correct : forall l, topological_sorting precedes l (top_sort precedes l). -Proof. +Proof using StrictOrder0. by intro; eapply top_sort_correct; [typeclasses eauto | apply Forall_True]. Qed. @@ -777,7 +779,7 @@ Corollary simple_maximal_element_in l (a : A) (Hmax : get_maximal_element precedes l = Some a) : a ∈ l. -Proof. +Proof using StrictOrder0. by eapply maximal_element_in; [typeclasses eauto | apply Forall_True |]. Qed. @@ -786,7 +788,7 @@ Corollary simple_get_maximal_element_correct l (Hina : a ∈ l) (Hmax : get_maximal_element precedes l = Some max) : ~ precedes max a. -Proof. +Proof using StrictOrder0. by eapply get_maximal_element_correct; [typeclasses eauto | apply Forall_True | ..]. Qed. diff --git a/theories/VLSM/Lib/TraceClassicalProperties.v b/theories/VLSM/Lib/TraceClassicalProperties.v index 806a4700..094dd60f 100644 --- a/theories/VLSM/Lib/TraceClassicalProperties.v +++ b/theories/VLSM/Lib/TraceClassicalProperties.v @@ -1,6 +1,7 @@ From Coq Require Import Classical ClassicalEpsilon. From VLSM.Lib Require Import SsrExport Traces TraceProperties. +Set Default Proof Using "Type". Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. diff --git a/theories/VLSM/Lib/TraceProperties.v b/theories/VLSM/Lib/TraceProperties.v index ca9c6f68..4f20c408 100644 --- a/theories/VLSM/Lib/TraceProperties.v +++ b/theories/VLSM/Lib/TraceProperties.v @@ -1,6 +1,7 @@ From Coq Require Import Program.Equality. From VLSM.Lib Require Import SsrExport Traces. +Set Default Proof Using "Type". Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. diff --git a/theories/VLSM/Lib/Traces.v b/theories/VLSM/Lib/Traces.v index 36593d41..8974682a 100644 --- a/theories/VLSM/Lib/Traces.v +++ b/theories/VLSM/Lib/Traces.v @@ -1,5 +1,6 @@ From VLSM.Lib Require Import SsrExport. +Set Default Proof Using "Type". Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. From 4a80a5cdb449023efaaffee3f61d8e45a21d11d9 Mon Sep 17 00:00:00 2001 From: Traian Florin Serbanuta Date: Mon, 3 Apr 2023 13:31:58 +0300 Subject: [PATCH 2/2] Ioan asked me to :-) --- searchAndDestroy.sh | 2 +- theories/VLSM/Core/ELMO/BaseELMO.v | 1 + theories/VLSM/Core/ELMO/ELMO.v | 1 + theories/VLSM/Core/ELMO/MO.v | 5 +++-- 4 files changed, 6 insertions(+), 3 deletions(-) diff --git a/searchAndDestroy.sh b/searchAndDestroy.sh index d609e7a1..b8684358 100755 --- a/searchAndDestroy.sh +++ b/searchAndDestroy.sh @@ -1,4 +1,4 @@ -for file in `find theories/VLSM/Core/ELMO/ -maxdepth 1 -name 'UMO.v'`; do +for file in `find theories/VLSM/Core/ELMO/ -maxdepth 1 -name '*.v'`; do fline=`cat $file | head -n1` if [[ $fline == 'Set Default Proof Using "Type".' ]]; then echo $file diff --git a/theories/VLSM/Core/ELMO/BaseELMO.v b/theories/VLSM/Core/ELMO/BaseELMO.v index 4cb116c8..2e487627 100644 --- a/theories/VLSM/Core/ELMO/BaseELMO.v +++ b/theories/VLSM/Core/ELMO/BaseELMO.v @@ -1,3 +1,4 @@ +Set Default Proof Using "Type". From VLSM.Lib Require Import Itauto. From stdpp Require Import prelude finite. From VLSM.Lib Require Import EquationsExtras. diff --git a/theories/VLSM/Core/ELMO/ELMO.v b/theories/VLSM/Core/ELMO/ELMO.v index 0db2eb61..68ca3d3b 100644 --- a/theories/VLSM/Core/ELMO/ELMO.v +++ b/theories/VLSM/Core/ELMO/ELMO.v @@ -1,3 +1,4 @@ +Set Default Proof Using "Type". From VLSM.Lib Require Import Itauto. From Coq Require Import FunctionalExtensionality Reals. From stdpp Require Import prelude finite. diff --git a/theories/VLSM/Core/ELMO/MO.v b/theories/VLSM/Core/ELMO/MO.v index d4fcba8a..2f310085 100644 --- a/theories/VLSM/Core/ELMO/MO.v +++ b/theories/VLSM/Core/ELMO/MO.v @@ -1,3 +1,4 @@ +Set Default Proof Using "Type". From VLSM.Lib Require Import Itauto. From Coq Require Import FunctionalExtensionality. From stdpp Require Import prelude finite. @@ -713,7 +714,7 @@ Lemma state_suffix_totally_orders_valid_sent_messages : obs1 <*> MkObservation Send m1 <**> obs2 <*> MkObservation Send m2 <**> obs3 -> MO_msg_valid_alt_sends m -> state_suffix (state m1) (state m2) /\ state_suffix (state m2) (state m). -Proof. +Proof using P. intros m m1 m2 obs1 obs2 obs3 Heq Hvalid. red in Hvalid. assert (H2 : @@ -1228,7 +1229,7 @@ Lemma unfold_rec_obs : rec_obs s ob <-> ob ∈ obs s \/ exists m, MkObservation Receive m ∈ obs s /\ rec_obs (state m) ob. -Proof using. clear. (* avoid unneccessary dependence on section variables *) +Proof. clear -Message. (* avoid unneccessary dependence on section variables *) intros s ob; split. - induction 1. + by left; constructor.