Remove "simpl" uses and refactor a BoundedN def

theories/Automation.v

@@ -48,7 +48,7 @@ Local Ltac perm_simplify_once :=
   aux.
 
 Local Ltac perm_simplify_round :=
-  simpl;
+  cbn;
   repeat appify;
   (* Change into [] ++ l ++ [] *)
   match goal with
@@ -57,7 +57,7 @@ Local Ltac perm_simplify_round :=
                                 rewrite <- (app_nil_r l1), <- (app_nil_r l2)
   end;
   repeat perm_simplify_once;
-  simpl;
+  cbn;
   repeat rewrite <- app_assoc;
   repeat rewrite app_nil_r;
   repeat
@@ -67,7 +67,7 @@ Local Ltac perm_simplify_round :=
 
 Ltac perm_simplify :=
   repeat perm_simplify_round;
-  simpl;
+  cbn;
   try apply Permutation_refl.
 
 Ltac destruct_match :=

theories/BoundedN.v

@@ -56,21 +56,14 @@ Module BoundedN.
     if (z <? 0)%Z then None else of_N (Z.to_N z).
 
   Definition of_Z_const (bound : N) (z : Z) :=
-    let ofz := @of_Z bound z in
-    match ofz return (match ofz with
-                      | Some _ => BoundedN bound
-                      | None => unit
-                      end) with
-    | Some x => x
-    | None => tt
-    end.
+    unpack_option (@of_Z bound z).
 
   Lemma to_N_inj {bound : N} {a b : BoundedN bound} :
     to_N a = to_N b -> a = b.
   Proof.
     intros eq.
     destruct a, b.
-    simpl in *.
+    cbn in *.
     subst.
     f_equal.
     apply UIP_dec.
@@ -115,7 +108,7 @@ Module BoundedN.
   Lemma of_to_N {bound : N} (n : BoundedN bound) :
     of_N (to_N n) = Some n.
   Proof.
-    destruct n as [n prf]; simpl.
+    destruct n as [n prf]; cbn.
     unfold of_N.
     replace (of_N_compare n) with (Some prf); auto.
     unfold of_N_compare.
@@ -185,7 +178,7 @@ Module BoundedN.
   Proof.
     induction xs as [|x xs IH].
     - split; intros H; inversion H.
-    - simpl.
+    - cbn.
       destruct (of_nat x) eqn:of_nat_x; split; intros H.
       + destruct H.
         * subst.
@@ -226,7 +219,7 @@ Module BoundedN.
     Proof.
       unfold decode_bounded, encode_bounded.
       rewrite decode_encode.
-      simpl.
+      cbn.
       apply of_to_N.
     Qed.
 
@@ -247,11 +240,11 @@ Module BoundedN.
     pose proof (in_seq (N.to_nat bound) 0) as in_seq'.
     pose proof (fun n => proj1 (in_seq' n)) as in_seq; clear in_seq'.
     induction nodup; try constructor.
-    simpl.
+    cbn.
     pose proof (in_seq x) as x_bound.
     specialize (x_bound (or_introl eq_refl)).
     destruct x_bound as [useless x_bound]; clear useless.
-    simpl in x_bound.
+    cbn in x_bound.
     destruct (of_nat x) eqn:ofnatx. all: cycle 1.
     apply of_nat_none in ofnatx.
     lia.
@@ -275,7 +268,7 @@ Module BoundedN.
     apply in_seq.
     unfold to_nat.
     destruct t as [t lt].
-    simpl.
+    cbn.
     change ((bound ?= t) = Gt) with (bound > t) in lt.
     lia.
   Qed.

theories/Congress.v

@@ -100,7 +100,7 @@ Global Program Instance setup_serializable : Serializable Setup :=
        Some (build_setup rules); |}.
 Next Obligation.
   intros x.
-  simpl.
+  cbn.
   rewrite deserialize_serialize.
   reflexivity.
 Qed.
@@ -178,7 +178,7 @@ Global Program Instance msg_serializable : Serializable Msg :=
 Next Obligation.
   intros msg.
   unfold serialize_msg, deserialize_msg.
-  destruct msg; repeat (simpl; rewrite deserialize_serialize); reflexivity.
+  destruct msg; repeat (cbn; rewrite deserialize_serialize); reflexivity.
 Qed.
 
 Definition serialize_state (s : State) : SerializedValue :=
@@ -193,7 +193,7 @@ Global Program Instance state_serializable : Serializable State :=
   {| serialize := serialize_state; deserialize := deserialize_state; |}.
 Next Obligation.
   unfold serialize_state, deserialize_state.
-  destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
+  destruct x; repeat (cbn; rewrite deserialize_serialize); reflexivity.
 Qed.
 
 End Serialization.

theories/Congress_Buggy.v

@@ -101,7 +101,7 @@ Global Program Instance setup_serializable : Serializable Setup :=
        Some (build_setup rules); |}.
 Next Obligation.
   intros x.
-  simpl.
+  cbn.
   rewrite deserialize_serialize.
   reflexivity.
 Qed.
@@ -181,7 +181,7 @@ Global Program Instance msg_serializable : Serializable Msg :=
 Next Obligation.
   intros msg.
   unfold serialize_msg, deserialize_msg.
-  destruct msg; repeat (simpl; rewrite deserialize_serialize); reflexivity.
+  destruct msg; repeat (cbn; rewrite deserialize_serialize); reflexivity.
 Qed.
 
 Definition serialize_state (s : State) : SerializedValue :=
@@ -196,7 +196,7 @@ Global Program Instance state_serializable : Serializable State :=
   {| serialize := serialize_state; deserialize := deserialize_state; |}.
 Next Obligation.
   unfold serialize_state, deserialize_state.
-  destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
+  destruct x; repeat (cbn; rewrite deserialize_serialize); reflexivity.
 Qed.
 
 End Serialization.

theories/Extras.v

@@ -60,7 +60,7 @@ Lemma sumnat_app
 Proof.
   revert ys.
   induction xs as [| x xs IH]; intros ys; auto.
-  simpl.
+  cbn.
   rewrite IH.
   lia.
 Qed.
@@ -92,7 +92,7 @@ Lemma sumZ_app
 Proof.
   revert ys.
   induction xs as [| x xs IH]; intros ys; auto.
-  simpl.
+  cbn.
   rewrite IH.
   lia.
 Qed.
@@ -167,7 +167,7 @@ Proof.
   revert start.
   induction len1 as [| len1 IH]; intros start.
   - now rewrite Nat.add_0_r.
-  - simpl.
+  - cbn.
     rewrite IH.
     f_equal; f_equal; f_equal.
     lia.
@@ -179,7 +179,7 @@ Proof.
   replace (S len) with (len + 1)%nat by lia.
   rewrite (seq_app start len 1).
   rewrite sumZ_app.
-  simpl.
+  cbn.
   lia.
 Qed.
 

theories/LocalBlockchain.v

@@ -252,8 +252,8 @@ Section ExecuteActions.
       + inversion sent; subst;
           now apply set_contract_state_equiv, transfer_balance_equiv.
     - (* no contract at destination, so msg should be empty *)
-      destruct (address_is_contract to) eqn:addr_format; simpl in *; try congruence.
-      destruct msg; simpl in *; try congruence.
+      destruct (address_is_contract to) eqn:addr_format; cbn in *; try congruence.
+      destruct msg; cbn in *; try congruence.
       assert (new_acts = []) by congruence; subst new_acts.
       apply (eval_transfer from to amount); auto.
       inversion sent; subst; now apply transfer_balance_equiv.
@@ -454,8 +454,8 @@ Proof.
   destruct lcopt as [lc|] eqn:exec; [|exact None].
   subst lcopt.
   cbn -[execute_actions] in exec.
-  destruct (validate_header _) eqn:validate; [|simpl in *; congruence].
-  destruct (validate_actions _) eqn:validate_actions; [|simpl in *; congruence].
+  destruct (validate_header _) eqn:validate; [|cbn in *; congruence].
+  destruct (validate_actions _) eqn:validate_actions; [|cbn in *; congruence].
   destruct_units.
   destruct lcb as [prev_lc_end prev_lcb_trace].
   refine (Some {| lcb_lc := lc; lcb_trace := _ |}).