Partial firstorder replacement

coq-vlsm.opam

@@ -20,6 +20,7 @@ depends: [
   "coq-stdpp" {>= "1.8.0"}
   "coq-itauto" 
   "coq-equations" 
+  "coq-hammer"
 ]
 
 tags: [

theories/VLSM/Core/Composition.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude finite.
 From Coq Require Import Streams FunctionalExtensionality Eqdep_dec.
@@ -398,6 +399,7 @@ Definition lift_to_composite_finite_trace j
 Definition lift_to_composite_finite_trace_last j
   := VLSM_embedding_finite_trace_last (lift_to_composite_VLSM_embedding j).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma constraint_free_incl
   (constraint : composite_label -> composite_state  * option message -> Prop)
   : VLSM_incl (composite_vlsm constraint) free_composite_vlsm.
@@ -1590,6 +1592,7 @@ Definition composite_valid_transition_item
   (s : composite_state IM) (item : composite_transition_item IM) : Prop :=
   CompositeValidTransition (l item) s (input item) (destination item) (output item).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma composite_valid_transition_reachable_iff l s1 iom s2 oom :
   CompositeValidTransition l s1 iom s2 oom <-> ValidTransition RFree l s1 iom s2 oom.
 Proof. by firstorder. Qed.

theories/VLSM/Core/ELMO/BaseELMO.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude finite.
 From VLSM.Lib Require Import EquationsExtras.
@@ -353,6 +354,7 @@ Proof.
   by split; intros H; decompose [and or ex] H; subst; eauto.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 (**
   When a message belongs to the [sentMessages] of some state, then the state
   contains a corresponding observation which was sent. The converse also holds.
@@ -392,6 +394,7 @@ Proof.
   by destruct (decide (isSend ob)).
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 (**
   When a message belongs to the [receivedMessages] of some state, then the state
   contains a corresponding observation which was received. The converse also holds.
@@ -615,6 +618,7 @@ Proof.
   by apply rec_obs_fn_sizeState.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export] Instance Message_FullMessageDependencies :
   FullMessageDependencies Message_dependencies Message_full_dependencies.
 Proof.

theories/VLSM/Core/ELMO/ELMO.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From Coq Require Import FunctionalExtensionality Reals.
 From stdpp Require Import prelude finite.
@@ -329,6 +330,7 @@ Definition ELMOComponent (i : index) : VLSM Message :=
   vmachine := ELMOComponentMachine i;
 |}.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export]
 Instance ComputableSentMessages_ELMOComponent
   (i : index) : ComputableSentMessages (ELMOComponent i).
@@ -344,6 +346,7 @@ Proof.
       by firstorder congruence.
 Defined.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export]
 Instance ComputableReceivedMessages_ELMOComponent
   (i : index) : ComputableReceivedMessages (ELMOComponent i).
@@ -364,6 +367,7 @@ Instance HasBeenDirectlyObservedCapability_ELMOComponent
   (i : index) : HasBeenDirectlyObservedCapability (ELMOComponent i) :=
     HasBeenDirectlyObservedCapability_from_sent_received (ELMOComponent i).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma ELMO_reachable_view (s : State) i :
   ram_state_prop (ELMOComponent i) s
     <->
@@ -588,6 +592,7 @@ Proof.
     intros; apply elem_of_sentMessages_addObservation; constructor; auto.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma local_equivocators_simple_addObservation :
   forall (s : State) (ob : Observation) (a : Address),
     local_equivocators_simple (s <+> ob) a ->
@@ -1262,6 +1267,7 @@ Proof.
     by apply elem_of_receivedMessages, obs_sizeState in Hobs; cbn in Hobs; lia.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export] Instance MessageDependencies_ELMOComponent :
   MessageDependencies Ei Message_dependencies.
 Proof.

theories/VLSM/Core/ELMO/MO.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From Coq Require Import FunctionalExtensionality.
 From stdpp Require Import prelude finite.
@@ -1223,6 +1224,7 @@ Proof.
       by apply rec_recv.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma unfold_rec_obs :
   forall (s : State) (ob : Observation),
     rec_obs s ob
@@ -1232,7 +1234,7 @@ Proof using. clear. (* avoid unneccessary dependence on section variables *)
   intros s ob; split.
   - induction 1.
     + by left; constructor.
-    + by setoid_rewrite elem_of_addObservation; firstorder.
+    + by setoid_rewrite elem_of_addObservation; qauto.
     + by setoid_rewrite elem_of_addObservation; firstorder.
   - induction s using addObservation_ind.
     + by firstorder using elem_of_nil.

theories/VLSM/Core/ELMO/UMO.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From Coq Require Import FunctionalExtensionality.
 From stdpp Require Import prelude finite.
@@ -114,10 +115,10 @@ Proof.
   - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
     destruct l, im; cbn in *; invert_UMOComponentValid
     ; inversion Ht; subst; clear Ht; cbn.
-    + by rewrite decide_False; cbn; firstorder congruence.
+    + by rewrite decide_False; cbn; qauto; congruence.
     + rewrite decide_True by done; cbn.
       unfold Message; rewrite elem_of_cons.
-      by firstorder congruence.
+      by qauto; congruence.
 Defined.
 
 #[export]
@@ -132,8 +133,8 @@ Proof.
     ; inversion Ht; subst; clear Ht; cbn.
     + rewrite decide_True by done; cbn.
       unfold Message; rewrite elem_of_cons.
-      by firstorder congruence.
-    + by rewrite decide_False; cbn; firstorder congruence.
+      by qauto; congruence.
+    + by rewrite decide_False; cbn; qauto; congruence.
 Defined.
 
 #[export]
@@ -1408,14 +1409,14 @@ Instance sent_comparable_dec : RelDecision sent_comparable.
 Proof.
   intros m1 m2.
   destruct (decide (adr (state m1) = adr (state m2)));
-    [| by right; destruct 1; apply n; firstorder congruence].
+    [| by right; destruct 1; apply n; qauto; congruence].
   destruct (decide (obs (state m1) = obs (state m2)));
     [by left; replace m2 with m1 by (apply eq_Message; done); constructor |].
   destruct (decide (m1 ∈ sentMessages (state m2)));
     [by left; constructor; constructor |].
   destruct (decide (m2 ∈ sentMessages (state m1)));
     [by left; constructor; constructor |].
-  by right; destruct 1; firstorder.
+  by right; destruct 1; qauto.
 Defined.
 
 #[export]

theories/VLSM/Core/Equivocation/NoEquivocation.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation.
@@ -132,7 +133,7 @@ Proof.
     split; [| done].
     rapply extend_right_finite_trace_from; [done |].
     apply finite_valid_trace_last_pstate in IHtr as Hs.
-    cut (option_valid_message_prop X iom); [by firstorder |].
+    cut (option_valid_message_prop X iom); [by hauto|].
     destruct iom as [m |]; [| by apply option_valid_message_None].
     destruct Hx as [Hv _].
     apply Henforced in Hv.

theories/VLSM/Core/VLSM.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From Coq Require Import Streams.
@@ -165,7 +166,7 @@ Lemma trace_has_message_observed_iff m tr
   (Hobserved : trace_has_message item_sends_or_receives m tr)
   : trace_has_message (field_selector input) m tr \/ trace_has_message (field_selector output) m tr.
 Proof.
-  by unfold trace_has_message in *; rewrite !Exists_exists in *; firstorder.
+  by unfold trace_has_message in *; rewrite !Exists_exists in *; qauto.
 Qed.
 
 (** Defines a message received but not sent by within the trace. *)
@@ -790,7 +791,7 @@ Proof.
   split.
   - intros Hm; inversion Hm; subst.
     + by right.
-    + by left; exists (s1, om0), l0; firstorder.
+    + by left; exists (s1, om0), l0; strivial.
   - intros [Hem | Him].
     + by apply option_can_produce_valid.
     + by constructor; apply Him.
@@ -870,7 +871,7 @@ Proof.
   - intro Hps'. destruct Hps' as [om' Hs].
     inversion Hs; subst.
     + by left; exists (exist _ _ Hs0).
-    + by right; exists l0, (s, om), om'; firstorder.
+    + by right; exists l0, (s, om), om'; strivial.
   - intros [[[s His] Heq] | [l [[s om] [om' [[[_om Hps] [[_s Hpm] Hv]] Ht]]]]]; subst.
     + by exists None; apply valid_initial_state_message.
     + by exists om'; apply valid_generated_state_message with s _om _s om l.
@@ -898,7 +899,7 @@ Proof.
   destruct Hs as [om Hs].
   induction Hs.
   - by apply IHinit.
-  - by apply (IHgen s' l0 om om' s); firstorder.
+  - by apply (IHgen s' l0 om om' s); strivial.
 Qed.
 
 (** Valid message characterization. *)
@@ -913,7 +914,7 @@ Proof.
   - intros [s' Hpm'].
     inversion Hpm'; subst.
     + by left; exists (exist _ m' Hom).
-    + by right; exists l0, (s, om), s'; firstorder.
+    + by right; exists l0, (s, om), s'; strivial.
   - intros [[[s His] Heq] | [l [[s om] [s' [[[_om Hps] [[_s Hpm] Hv]] Ht]]]]]; subst.
     + by apply initial_message_is_valid.
     + by exists s'; apply valid_generated_state_message with s _om _s om l.
@@ -1634,7 +1635,7 @@ Proof.
     apply finite_valid_trace_from_to_singleton.
     apply finite_valid_trace_init_to_emit_valid_state_message in Htl1.
     apply finite_valid_trace_init_to_emit_valid_state_message in Htl2.
-    by firstorder.
+    by strivial.
 Qed.
 
 Lemma finite_valid_trace_init_to_add_emit
@@ -1684,7 +1685,7 @@ Proof.
     {
       apply finite_valid_trace_init_to_emit_valid_state_message in Htr1.
       apply finite_valid_trace_init_to_emit_valid_state_message in Htr2.
-      by firstorder.
+      by strivial.
     }
     apply finite_valid_trace_init_to_emit_output in Htr2 as Houtput.
     apply finite_valid_trace_init_to_emit_forget_emit in Htr1.
@@ -1961,7 +1962,7 @@ Proof.
   apply finite_valid_trace_from_to_last in Htrs as Hlast.
   rewrite <- Hlast in Htr.
   apply finite_valid_trace_from_to_forget_last in Htrs.
-  by firstorder using finite_valid_trace_from_app_iff.
+  by strivial using finite_valid_trace_from_app_iff.
 Qed.
 
 (**
@@ -2807,7 +2808,7 @@ Context
 Lemma ValidTransition_preloaded_iff :
   forall l s1 iom s2 oom,
     ValidTransition X l s1 iom s2 oom <-> ValidTransition R l s1 iom s2 oom.
-Proof. by firstorder. Qed.
+Proof. by sauto. Qed.
 
 Lemma ValidTransitionNext_preloaded_iff :
   forall s1 s2, ValidTransitionNext X s1 s2 <-> ValidTransitionNext R s1 s2.
@@ -2824,7 +2825,7 @@ Lemma input_valid_transition_forget_input :
   forall l s1 iom s2 oom,
     input_valid_transition X l (s1, iom) (s2, oom) ->
     ValidTransition X l s1 iom s2 oom.
-Proof. by firstorder. Qed.
+Proof. by hauto. Qed.
 
 End sec_valid_transition_props.
 

theories/VLSM/Core/VLSMProjections/VLSMEquality.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections.VLSMInclusion VLSMProjections.VLSMEmbedding.
@@ -41,6 +42,7 @@ Proof.
   by intros Heq t Hyt; apply Heq.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_incl_iff
   (MX MY : VLSMMachine vtype)
   (X := mk_vlsm MX) (Y := mk_vlsm MY)
@@ -51,6 +53,7 @@ End sec_VLSM_equality.
 
 Notation VLSM_eq X Y := (VLSM_eq_part (machine X) (machine Y)).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_refl
   {message : Type}
   {vtype : VLSMType message}
@@ -61,6 +64,7 @@ Proof.
   by firstorder.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_sym
   {message : Type}
   {vtype : VLSMType message}
@@ -71,6 +75,7 @@ Proof.
   by firstorder.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_trans
   {message : Type}
   {vtype : VLSMType message}

theories/VLSM/Core/VLSMProjections/VLSMInclusion.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections.VLSMEmbedding VLSMProjections.VLSMTotalProjection.
@@ -24,6 +25,7 @@ Definition VLSM_incl_part
     valid_trace_prop X t -> valid_trace_prop Y t.
 #[local] Notation VLSM_incl X Y := (VLSM_incl_part (machine X) (machine Y)).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_incl_refl
   (MX : VLSMMachine vtype)
   (X := mk_vlsm MX)
@@ -32,6 +34,7 @@ Proof.
   by firstorder.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_incl_trans
   (MX MY MZ : VLSMMachine vtype)
   (X := mk_vlsm MX) (Y := mk_vlsm MY) (Z := mk_vlsm MZ)

theories/VLSM/Core/Validator.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections Composition.
@@ -587,7 +588,7 @@ Proof.
         (VLSM_projection_input_valid_transition Hproji); [done |].
       by split; [| apply injective_projections].
     + assert (HivtX : input_valid_transition X lX (sX, om) (vtransition X lX (sX, om)))
-        by firstorder.
+        by strivial.
       destruct (vtransition _ _ _) as (sX', _om').
       eapply (VLSM_projection_input_valid_transition Hproj) in HivtX as [_ Hs']; [| done].
       rewrite HsX in Hs'.

theories/VLSM/Lib/FinSetExtras.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
@@ -195,7 +196,7 @@ Proof.
   intros a Ha.
   apply elem_of_map in Ha.
   apply elem_of_map.
-  by firstorder.
+  by strivial.
 Qed.
 
 Lemma set_map_size_upper_bound

theories/VLSM/Lib/ListExtras.v

@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import finite.
 From Coq Require Import FinFun.
@@ -884,7 +885,7 @@ Lemma nth_error_map
   (n : nat)
   : nth_error (List.map f l) n = option_map f (nth_error l n).
 Proof.
-  by revert n; induction l; intros [| n]; firstorder.
+  by revert n; induction l; intros [| n]; strivial.
 Qed.
 
 Lemma exists_finite
@@ -960,6 +961,7 @@ Proof.
   by destruct (f a); cbn; congruence.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma map_option_nth
   {A B : Type}
   (f : A -> option B)
@@ -1437,8 +1439,8 @@ Proof.
   induction 2; cbn.
   - apply PeanoNat.Nat.add_lt_le_mono; [done |].
     induction l; cbn; [done |].
-    by apply PeanoNat.Nat.add_le_mono; firstorder.
-  - by apply PeanoNat.Nat.add_le_lt_mono; firstorder.
+    by apply PeanoNat.Nat.add_le_mono; qauto.
+  - by apply PeanoNat.Nat.add_le_lt_mono; strivial.
 Qed.
 
 (**