Get rid of the useless Axiom.

theories/mask_core/calculus.v

@@ -54,7 +54,8 @@ Proof.
 Qed.
 
 Definition ranges_monotone (l : list range) : Prop :=
-  Sorted range_lt l.
+  (* Trick to make this proof-irrelevant. *)
+  Is_true (bool_decide (Sorted range_lt l)).
 
 (* a signature describes the field layout of a bit vector *)
 Record signature := {
@@ -67,9 +68,25 @@ Record signature := {
   (* total bits *)
   sig_bits : nat;
   sig_max_range_bounded : ∃ r, last sig_ranges = Some r ∧
-    offset r + width r ≤ sig_bits
+    bool_decide (offset r + width r ≤ sig_bits)
 }.
 
+Global Instance signature_eq_dec_inst : EqDecision signature.
+Proof.
+  move => [s1_len s1_ranges s1_mon s1_bits s1_max].
+  move => [s2_len s2_ranges s2_mon s2_bits s2_max].
+  destruct (decide (s1_len = s2_len)) as [->|]; last first.
+  { right. move => ?. simplify_eq. }
+  destruct (decide (s1_ranges = s2_ranges)) as [->|]; last first.
+  { right. move => ?. simplify_eq. }
+  destruct (decide (s1_bits = s2_bits)) as [->|]; last first.
+  { right. move => ?. simplify_eq. }
+  left.
+  move: s1_max s2_max. move => [r1 [Hr1_1 Hr1_2]] [r2 [Hr2_1 Hr2_2]].
+  assert (r1 = r2) by naive_solver. simplify_eq.
+  f_equal; last do 2 f_equal; apply: proof_irrel.
+Qed.
+
 Definition field_width (σ : signature) f : nat :=
   width (σ.(sig_ranges) !!! f).
 Arguments field_width _ !_ /.
@@ -92,7 +109,10 @@ Lemma sig_ranges_bounded σ f :
 Proof.
 Admitted.
 
-Ltac solve_ranges_monotone := by repeat econstructor.
+Ltac solve_ranges_monotone :=
+  apply bool_decide_pack;
+  repeat (constructor; [|constructor; rewrite /range_lt /=; lia]);
+  constructor.
 Ltac sig_max_range_bounded := eexists; split; [done | simpl; lia].
 
 Module example.
@@ -104,13 +124,6 @@ Module example.
   Next Obligation. sig_max_range_bounded. Qed.
 End example.
 
-(* This is reasonable, because in practice signature is more like a nominal type,
-   which means we can directly know if two signatures are eq by checking if their names are eq,
-   and the record signature is more like a definition of that nominal type *)
-Axiom signature_eq_dec : EqDecision signature.
-
-Global Instance signature_eq_dec_inst : EqDecision signature := signature_eq_dec.
-
 (* Terms representing RefinedC bit field constructors. *)
 Inductive tm : Type :=
   | bf_val (n : Z)

theories/mask_core/safety.v

@@ -67,7 +67,7 @@ Ltac auto_inv :=
   | [ H : _ ## _ ∨ ⊢ _ : _ |- _ ] => destruct H as [H|H]
   (* sigma type: val *)
   | [ H : existT ?σ _ = existT ?σ _ |- _ ] =>
-    apply Eqdep_dec.inj_pair2_eq_dec in H; [subst | by apply signature_eq_dec]
+    apply Eqdep_dec.inj_pair2_eq_dec in H; [subst | by apply signature_eq_dec_inst]
   (* typing rules with premises: expand or contradiction *)
   | [ H : ⊢ bf_val _ : _  |- _ ] => invert H
   | [ H : ⊢ bf_mask _ : _  |- _ ] => invert H