Merge pull request #87 from SkyLabsAI/gmalecha/verify-template-specialization

Remove [untemplate_goal]

Author: gmalecha-at-skylabs

rocq-brick-libstdcpp/proof/lib/tactics.v

@@ -10,23 +10,17 @@ but it works after [untemplate_goal] normalizes the name substitution with [vm_c
 Ltac untemplate_spec G :=
   let y := eval red in G in
   change G with y;
-  rewrite /specify_notation.template_specify/specify_t;
+  rewrite specify_notation.template_specify.unlock/specify_t;
   match goal with
-  |- context [match ?y with _ => _ end] =>
-    let z := eval vm_compute in y in
-    change y with z
+  | |- context [match ?y with _ => _ end] =>
+      let z := eval vm_compute in y in
+      change y with z
   end;
   cbn.
 
-Ltac untemplate_goal :=
-  match goal with
-  |- _ ⊢ ?G =>
-  untemplate_spec G
-  end.
-
 Ltac untemplate_bi :=
   match goal with
-  |- ?S1 ⊣⊢ ?S2 =>
-  untemplate_spec S1;
-  untemplate_spec S2
+  | |- ?S1 ⊣⊢ ?S2 =>
+      untemplate_spec S1;
+      untemplate_spec S2
   end.

rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v

@@ -16,7 +16,6 @@ NES.Begin unique_lock.
 
     Lemma default_ctor_spec_ok : verify[source] "std::unique_lock<std::mutex>::unique_lock()".
     Proof.
-      untemplate_goal.
       verify_spec; go.
     Qed.
 
@@ -32,9 +31,6 @@ NES.Begin unique_lock.
       verify[source]
         "std::unique_lock<std::mutex>::unique_lock(std::mutex&, std::defer_lock_t)".
     Proof.
-      work; iStopProof; untemplate_goal.
-      (* untemplate_spec (lock_defer_ctor_spec "std::mutex" source). *)
-
       verify_spec; go.
       by rewrite cQp.scale_mut (right_id_L 1%Qp Qp.mul).
     Qed.
@@ -46,7 +42,6 @@ NES.Begin unique_lock.
       verify[source]
         "std::unique_lock<std::mutex>::unique_lock(std::mutex&)".
     Proof.
-      work; iStopProof; untemplate_goal.
       verify_spec; go.
       iExists K.
       (* Time Succeed solve [setoid_rewrite cQp.scale_mut; setoid_rewrite (right_id_L 1%Qp Qp.mul); ego with br_erefl]. *)

rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v

@@ -20,7 +20,6 @@ NES.Begin unique_lock.
     Lemma default_ctor_spec_ok :
       verify[source] "std::unique_lock<std::recursive_mutex>::unique_lock()".
     Proof.
-      untemplate_goal.
       verify_spec; go.
     Qed.
 
@@ -36,9 +35,6 @@ NES.Begin unique_lock.
       verify[source]
         "std::unique_lock<std::recursive_mutex>::unique_lock(std::recursive_mutex&, std::defer_lock_t)".
     Proof.
-      work; iStopProof; untemplate_goal.
-      (* untemplate_spec (lock_defer_ctor_spec "std::recursive_mutex" source). *)
-
       verify_spec; go.
       by rewrite cQp.scale_mut (right_id_L 1%Qp Qp.mul).
     Qed.
@@ -51,8 +47,6 @@ NES.Begin unique_lock.
       verify[source]
         "std::unique_lock<std::recursive_mutex>::unique_lock(std::recursive_mutex&)".
     Proof.
-      work; iStopProof; untemplate_goal.
-      (* untemplate_spec (lock_ctor_spec "std::recursive_mutex" source). *)
       verify_spec; go.
       iExists K.
       (* Time Succeed solve [setoid_rewrite cQp.scale_mut; setoid_rewrite (right_id_L 1%Qp Qp.mul); ego with br_erefl]. *)

rocq-brick-libstdcpp/test/memory/test_cpp_proof.v

@@ -10,15 +10,11 @@ NES.Begin memory.
 
     Lemma addressof_ok : __addressof_spec "C" source |-- verify?[source] "std::addressof<C>(C&)".
     Proof.
-      work; iStopProof; untemplate_goal.
-
       verify_spec; go.
     Qed.
 
     Lemma __addressof_ok : verify?[source] "std::__addressof<C>(C&)".
     Proof.
-      work; iStopProof; untemplate_goal.
-
       verify_spec; go.
     Abort.
   End with_cpp.