better error messages

theories/lithium/interpreter.v

@@ -561,22 +561,22 @@ Ltac liDestructHint :=
        record_destruct_hint hint info
     | DHintDestruct _ (@bool_decide ?P ?b) =>
       let H := fresh "H" in destruct_decide (@bool_decide_reflect P b) as H; revert H; [
-      record_destruct_hint hint (true, info) |
-      record_destruct_hint hint (false, info) ]
+      record_destruct_hint hint (info, true) |
+      record_destruct_hint hint (info, false) ]
     | DHintDestruct _ ?x =>
       tryif (non_trivial_destruct x) then
         case_eq x; repeat liForall;
         lazymatch goal with
         | |- _ = ?res → _ =>
-          record_destruct_hint hint (res, info)
+          record_destruct_hint hint (info, res)
         end
       else (
           idtac
         )
     | @DHintDecide ?P ?b =>
        let H := fresh "H" in destruct_decide (@decide P b) as H; revert H; [
-      record_destruct_hint hint (true, info) |
-      record_destruct_hint hint (false, info) ]
+      record_destruct_hint hint (info, true) |
+      record_destruct_hint hint (info, false) ]
     end
   end; repeat (liForall || liImpl); try by [exfalso; can_solve_tac].
 

theories/lithium/simpl_instances.v

@@ -23,6 +23,10 @@ Global Instance simpl_shelve_hint P:
   SimplImpl true (shelve_hint P) (λ T, P → T).
 Proof. split; naive_solver. Qed.
 
+Global Instance simpl_double_neg_elim_dec P `{!Decision P} :
+  SimplBoth (¬ ¬ P) P.
+Proof. split; destruct (decide P); naive_solver. Qed.
+
 Global Instance simpl_eq_pair A B (x1 x2 : A) (y1 y2 : B):
   SimplAnd ((x1, y1) = (x2, y2)) (λ T, x1 = x2 ∧ y1 = y2 ∧ T).
 Proof. split; naive_solver. Qed.

theories/typing/automation/proof_state.v

@@ -110,8 +110,11 @@ Ltac print_goal :=
         clear H
       end;
    repeat lazymatch reverse goal with
-          | H : CASE_DISTINCTION_INFO ?hint ?info ?l |- _ =>
-            idtac "Case distinction" hint " - " info;
+          | H : CASE_DISTINCTION_INFO ?hint ?i ?l |- _ =>
+            lazymatch i with
+            | (?a, ?b) => idtac "Case distinction" a "->" b
+            | ?a => idtac "Case distinction" a
+            end;
             lazymatch l with
             | ?i :: ?l =>
               lazymatch eval unfold i in i with

theories/typing/int.v

@@ -374,6 +374,11 @@ Section programs.
 End programs.
 Typeclasses Opaque int_inner_type boolean_inner_type.
 
+Notation "'if' p " := (DestructHintIfBool p) (at level 100, only printing).
+Notation "'if' p ≠ 0 " := (DestructHintIfInt p) (at level 100, only printing).
+Notation "'case' n " := (DestructHintSwitchIntCase n) (at level 100, only printing).
+Notation "'default'" := (DestructHintSwitchIntDefault) (at level 100, only printing).
+
 (*** Tests *)
 Section tests.
   Context `{!typeG Σ}.

theories/typing/optional.v

@@ -139,34 +139,39 @@ Section optional.
     λ T, i2p (subsume_optional_val_ty_ref b ty ty' optty v T ot1 ot2).
 
   Inductive destruct_hint_optional :=
-  | DestructHintOptional.
+  | DestructHintOptionalEq (P : Prop)
+  | DestructHintOptionalNe (P : Prop).
 
-  Lemma type_eq_optional_refined v1 v2 ty optty `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} T b  `{!Decision b} :
+  Lemma type_eq_optional_refined v1 v2 ty optty `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} T b :
     opt_pre ty v1 v2 ∧
-    destruct_hint (DHintDecide b) DestructHintOptional
-    (∀ v, (if decide b then v1 ◁ᵥ ty else v1 ◁ᵥ optty) -∗ T v (t2mt ((if decide b then false else true) @ boolean i32)) ) -∗
+    destruct_hint DHintInfo (DestructHintOptionalEq b) (⌜b⌝ -∗ v1 ◁ᵥ ty -∗ T (i2v (Z_of_bool false) i32) (t2mt (false @ boolean i32))) ∧
+    destruct_hint DHintInfo (DestructHintOptionalEq (¬ b)) (⌜¬ b⌝ -∗ v1 ◁ᵥ optty -∗ T (i2v (Z_of_bool true) i32) (t2mt (true @ boolean i32))) -∗
       typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 T.
   Proof.
     unfold destruct_hint. iIntros "HT Hv1 Hv2" (Φ) "HΦ".
-    iDestruct "Hv1" as "[[% Hv1]|[% Hv1]]"; case_decide => //.
-    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool false) => //.
-      iApply (wp_binop_det v'). iSplit. {
+    iDestruct "Hv1" as "[[% Hv1]|[% Hv1]]".
+    - iApply (wp_binop_det (i2v (Z_of_bool false) i32)). iSplit. {
         iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
         iDestruct (opt_bin_op true true with "Hpre Hv1 Hv2 Hctx") as %->.
-        iPureIntro. by split => ?; simpl in *; simplify_eq.
+        iPureIntro. rewrite /i2v.
+        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool false) => //.
+        naive_solver.
       }
-      iDestruct ("HT" with "Hv1") as "HT".
-      iApply "HΦ" => //. by rewrite /ty_own_val/=.
-    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool true) => //.
-      iApply (wp_binop_det v'). iSplit. {
+      iDestruct "HT" as "[_ [HT _]]".
+      iDestruct ("HT" with "[//] Hv1") as "HT".
+      by iApply ("HΦ" with "[] HT").
+    - iApply (wp_binop_det (i2v (Z_of_bool true) i32)). iSplit. {
         iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
         iDestruct (opt_bin_op false true with "Hpre Hv1 Hv2 Hctx") as %->.
-        iPureIntro. by split => ?; simpl in *; simplify_eq.
+        iPureIntro. rewrite /i2v.
+        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool true) => //.
+        naive_solver.
       }
-      iDestruct ("HT" with "Hv1") as "HT".
-      iApply "HΦ" => //. by rewrite /ty_own_val/=.
+      iDestruct "HT" as "[_ [_ HT]]".
+      iDestruct ("HT" with "[//] Hv1") as "HT".
+      by iApply ("HΦ" with "[] HT").
   Qed.
-  Global Instance type_eq_optional_refined_inst v1 v2 ty optty `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} b `{!Decision b} :
+  Global Instance type_eq_optional_refined_inst v1 v2 ty optty `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} b :
     TypedBinOp v1 (v1 ◁ᵥ b @ (optional ty optty))%I v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 :=
     λ T, i2p (type_eq_optional_refined v1 v2 ty optty ot1 ot2 T b).
 
@@ -190,32 +195,36 @@ Section optional.
     TypedBinOp v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 :=
     λ T, i2p (type_eq_optional_neq v1 v2 ty optty ot1 ot2 T).
 
-  Lemma type_neq_optional v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} T b  `{!Decision b} :
+  Lemma type_neq_optional v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} T b :
     opt_pre ty v1 v2 ∧
-    destruct_hint (DHintDecide b) DestructHintOptional
-    (∀ v, (if decide b then v1 ◁ᵥ ty else v1 ◁ᵥ optty) -∗ T v (t2mt ((if decide b then true else false) @ boolean i32)) ) -∗
+    destruct_hint DHintInfo (DestructHintOptionalNe b) (⌜b⌝ -∗ v1 ◁ᵥ ty -∗ T (i2v (Z_of_bool true) i32) (t2mt (true @ boolean i32))) ∧
+    destruct_hint DHintInfo (DestructHintOptionalNe (¬ b)) (⌜¬ b⌝ -∗ v1 ◁ᵥ optty -∗ T (i2v (Z_of_bool false) i32) (t2mt (false @ boolean i32))) -∗
       typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 T.
   Proof.
-    unfold destruct_hint. iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
-    iDestruct "Hv1" as "[[% Hv1]|[% Hv1]]"; case_decide => //.
-    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool true) => //.
-      iApply (wp_binop_det v'). iSplit. {
+    unfold destruct_hint. iIntros "HT Hv1 Hv2" (Φ) "HΦ".
+    iDestruct "Hv1" as "[[% Hv1]|[% Hv1]]".
+    - iApply (wp_binop_det (i2v (Z_of_bool true) i32)). iSplit. {
         iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
         iDestruct (opt_bin_op true false with "Hpre Hv1 Hv2 Hctx") as %->.
-        iPureIntro. by split => ?; simpl in *; simplify_eq.
+        iPureIntro. rewrite /i2v.
+        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool true) => //.
+        naive_solver.
       }
-      iDestruct ("HT" with "Hv1") as "HT".
-      iApply "HΦ" => //. by rewrite /ty_own_val/=.
-    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool false) => //.
-      iApply (wp_binop_det v'). iSplit. {
+      iDestruct "HT" as "[_ [HT _]]".
+      iDestruct ("HT" with "[//] Hv1") as "HT".
+      by iApply ("HΦ" with "[] HT").
+    - iApply (wp_binop_det (i2v (Z_of_bool false) i32)). iSplit. {
         iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
         iDestruct (opt_bin_op false false with "Hpre Hv1 Hv2 Hctx") as %->.
-        iPureIntro. by split => ?; simpl in *; simplify_eq.
+        iPureIntro. rewrite /i2v.
+        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool false) => //.
+        naive_solver.
       }
-      iDestruct ("HT" with "Hv1") as "HT".
-      iApply "HΦ" => //. by rewrite /ty_own_val/=.
+      iDestruct "HT" as "[_ [_ HT]]".
+      iDestruct ("HT" with "[//] Hv1") as "HT".
+      by iApply ("HΦ" with "[] HT").
   Qed.
-  Global Instance type_neq_optional_inst v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} b `{!Decision b} :
+  Global Instance type_neq_optional_inst v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} b :
     TypedBinOp v1 (v1 ◁ᵥ b @ (optional ty optty))%I v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 :=
     λ T, i2p (type_neq_optional v1 v2 ty optty ot1 ot2 T b).
 
@@ -240,6 +249,9 @@ Section optional.
 End optional.
 Typeclasses Opaque optional_type.
 
+Notation "'optional' == ... : P" := (DestructHintOptionalEq P) (at level 100, only printing).
+Notation "'optional' != ... : P" := (DestructHintOptionalNe P) (at level 100, only printing).
+
 Section optionalO.
   Context `{!typeG Σ}.