cleanup

theories/lithium/base.v

@@ -63,20 +63,22 @@ Ltac get_head e :=
   | _    => constr:(e)
   end.
 
-(** A version of done that does not exploit False and contradictions. *)
-Ltac done_no_false :=
+(** A version of fast_done that splits conjunctions. *)
+Ltac splitting_fast_done :=
   solve
   [ repeat first
     [ fast_done
-    (* | solve [trivial] *)
     (* All the tactics below will introduce themselves anyway, or make no sense
        for goals of product type. So this is a good place for us to do it. *)
     | progress intros
-    (* | solve [symmetry; trivial] *)
-    (* | solve [apply not_symmetry; trivial] *)
     | split ]
   ].
 
+Ltac assert_is_trivial P :=
+  assert_succeeds (assert (P) as _;[splitting_fast_done|]).
+Ltac assert_is_not_trivial P :=
+  assert_fails (assert (P) as _;[splitting_fast_done|]).
+
 (* Checks that a term is closed using a trick by Jason Gross. *)
 Ltac check_closed t :=
   assert_succeeds (

theories/lithium/infrastructure.v

@@ -22,12 +22,6 @@ Class AssumeInj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
 Global Instance assume_inj_inj A B R S (f : A → B) `{!Inj R S f} : AssumeInj R S f.
 Proof. done. Qed.
 
-(** * Checking if a hyp exists *)
-Ltac check_hyp_not_exists P :=
-  assert_fails (assert (P) as _;[fast_done|]).
-Class CheckHypNotExists (P : Prop) : Prop := check_hyp_not_exists : True.
-Global Hint Extern 1 (CheckHypNotExists ?P) => (check_hyp_not_exists P; change True; fast_done) : typeclass_instances.
-
 (** * Checking if a hyp in the context
   The implementation can be found in interpreter.v *)
 Class CheckOwnInContext {Σ} (P : iProp Σ) : Prop := { check_own_in_context : True }.

theories/lithium/interpreter.v

@@ -593,7 +593,7 @@ Ltac liImpl :=
     lazymatch type of P with
     | Prop => first [
               (* first check if the hyp is trivial *)
-              assert_succeeds (assert (P) as _;[done_no_false|]); intros _
+              assert_is_trivial P; intros _
             |
               progress normalize_goal_impl; simpl
             |
@@ -613,7 +613,7 @@ Ltac liImpl :=
                 | _ = _ =>
                     check_injection_tac;
                     let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi
-                | _ => check_hyp_not_exists P; intros ?; subst
+                | _ => assert_is_not_trivial P; intros ?; subst
                 | _ => move => _
                 end
               end
@@ -724,7 +724,7 @@ Ltac liSideCond :=
     lazymatch P with
     | shelve_hint _ => split; [ unfold shelve_hint; li_shelve_sidecond |]
     | _ => first [
-      split; [done_no_false|] |
+      split; [splitting_fast_done|] |
       progress normalize_goal_and |
     lazymatch P with
     | context [protected _] => first [

theories/lithium/solvers.v

@@ -65,20 +65,22 @@ Proof. naive_solver. Qed.
 
 Ltac normalize_and_simpl_goal_step :=
   first [
-      progress normalize_goal; simpl |
-              lazymatch goal with
-              | |- ∃ _, _ => fail 1 "normalize_and_simpl_goal stop in exist"
-              end
-              |
-              lazymatch goal with
-              | |- _ ∧ _ => idtac
-              | _ => refine (intro_and_True _ _)
-              end;
-              refine (apply_simpl_and _ _ _ _ _);
-              lazymatch goal with
-              | |- true = true → _ => move => _; split_and?
-              end
-              | lazymatch goal with
+      progress normalize_goal; simpl
+    |
+      lazymatch goal with
+      | |- ∃ _, _ => fail 1 "normalize_and_simpl_goal stop in exist"
+      end
+    |
+      lazymatch goal with
+      | |- _ ∧ _ => idtac
+      | _ => refine (intro_and_True _ _)
+      end;
+      refine (apply_simpl_and _ _ _ _ _);
+      lazymatch goal with
+      | |- true = true → _ => move => _; split_and?
+      end
+    |
+      lazymatch goal with
     (* relying on the fact that unification variables cannot contain
        dependent variables to distinguish between dependent and non dependent forall *)
     | |- ?P -> ?Q =>