Learn side-conditions in the continuation.

examples/binary_search.c

@@ -51,7 +51,7 @@ bool compare_int(void *x, void *y) {
 [[rc::requires("[alloc_initialized]")]]
 [[rc::tactics("all: try by repeat constructor; lia.")]]
 [[rc::tactics("all: try by apply _.")]]
-[[rc::tactics("all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H0 3%nat) => //; lia.")]]
+[[rc::tactics("all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H3 3%nat) => //; lia.")]]
 void test() {
   size_t *ptrs[5];
   ptrs[0] = alloc(sizeof(size_t));

examples/btree.c

@@ -45,18 +45,19 @@ void free_btree(btree_t* t){
 [[rc::ensures("{¬ k ∈ l → StronglySorted (<) (take s l ++ k :: drop s l)}")]]
 [[rc::ensures("own p : array<{it_layout i32}, {(l `at_type` int i32) ++ "
                         "replicate (sz - n)%nat (uninit i32 : type)}>")]]
-[[rc::tactics("destruct (decide (i = s)); by naive_solver lia.")]]
+[[rc::tactics(//FIXME
+  "destruct (decide (i = s)); last eapply H0 => //; by naive_solver lia.")]]
 [[rc::tactics(// FIXME
-  "move: (elem_of_list_lookup_1 _ _ H14) => [i Hi]. "
+  "move: (elem_of_list_lookup_1 _ _ H16) => [i Hi]. "
   "destruct (decide (y = k)); [ done | exfalso ]. "
   "assert (k < y) as Hky by lia. "
   "assert (i < s)%nat as Hle by by eapply StronglySorted_lookup_index_lt. "
   "assert (i < s) as His  by lia. assert (k < k) by by eapply H0. by lia.")]]
 [[rc::tactics(// FIXME
   "apply StronglySorted_insert_drop_take; last done. "
-  "* move => z Hz. destruct (l !! z) eqn:?; naive_solver lia. "
-  "* move: (elem_of_list_lookup_2 l s y H7) => Hy. rewrite H7 /=. "
-  "  assert (k ≠ y); [ by set_solver | by lia ].")]]
+  "* move => z Hz. destruct (l !! z) eqn:? => //=. eapply H0 => //; lia. "
+  "* move: (elem_of_list_lookup_2 l s y H9) => Hy. rewrite H9 /=. "
+  "assert (k ≠ y); [ by set_solver | by lia ].")]]
 [[rc::tactics(// FIXME
   "assert (s = length l) as -> by lia. assert (k < k); last by lia. "
   "move: (elem_of_list_lookup_1 _ _ H7) => [i Hi]. "
@@ -87,9 +88,9 @@ int key_index(int* ar, int n, int k){
 [[rc::tactics("apply: (btree_invariant_in_range_child H2); naive_solver lia.")]]
 [[rc::tactics("rewrite H1; apply: (btree_invariant_lookup_child H2); by naive_solver.")]]
 [[rc::tactics("do 2 rewrite list_insert_id //; by destruct y0.")]]
-[[rc::tactics("assert (k ∉ x0) as Hx1. { move => /H7 Hk. apply lookup_lt_Some in Hk. lia. } "
+[[rc::tactics("assert (k ∉ x0) as Hx1. { move => /H8 Hk. apply lookup_lt_Some in Hk. lia. } "
               "apply: (btree_invariant_in_range_child H2); by naive_solver.")]]
-[[rc::tactics("assert (k ∉ x0) as Hx1. { move => /H7 Hk. apply lookup_lt_Some in Hk. lia. } "
+[[rc::tactics("assert (k ∉ x0) as Hx1. { move => /H8 Hk. apply lookup_lt_Some in Hk. lia. } "
               "rewrite H1. apply: (btree_invariant_lookup_child H2); by naive_solver.")]]
 [[rc::tactics("rewrite list_insert_id //; by destruct y.")]]
 bool btree_member(btree_t* t, int k){

examples/proofs/binary_search/generated_proof_test.v

@@ -28,7 +28,7 @@ Section proof_test.
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: try by repeat constructor; lia.
     all: try by apply _.
-    all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H0 3%nat) => //; lia.
+    all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H3 3%nat) => //; lia.
     all: print_sidecondition_goal "test".
   Qed.
 End proof_test.

examples/proofs/btree/generated_proof_btree_member.v

@@ -46,8 +46,8 @@ Section proof_btree_member.
     + apply: (btree_invariant_in_range_child H2); naive_solver lia.
     + rewrite H1; apply: (btree_invariant_lookup_child H2); by naive_solver.
     + do 2 rewrite list_insert_id //; by destruct y0.
-    + assert (k ∉ x0) as Hx1. { move => /H7 Hk. apply lookup_lt_Some in Hk. lia. } apply: (btree_invariant_in_range_child H2); by naive_solver.
-    + assert (k ∉ x0) as Hx1. { move => /H7 Hk. apply lookup_lt_Some in Hk. lia. } rewrite H1. apply: (btree_invariant_lookup_child H2); by naive_solver.
+    + assert (k ∉ x0) as Hx1. { move => /H8 Hk. apply lookup_lt_Some in Hk. lia. } apply: (btree_invariant_in_range_child H2); by naive_solver.
+    + assert (k ∉ x0) as Hx1. { move => /H8 Hk. apply lookup_lt_Some in Hk. lia. } rewrite H1. apply: (btree_invariant_lookup_child H2); by naive_solver.
     + rewrite list_insert_id //; by destruct y.
     all: print_sidecondition_goal "btree_member".
   Qed.

examples/proofs/btree/generated_proof_key_index.v

@@ -34,9 +34,9 @@ Section proof_key_index.
     - repeat liRStep; liShow.
       all: print_typesystem_goal "key_index" "#1".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    + destruct (decide (i = s)); by naive_solver lia.
-    + move: (elem_of_list_lookup_1 _ _ H14) => [i Hi]. destruct (decide (y = k)); [ done | exfalso ]. assert (k < y) as Hky by lia. assert (i < s)%nat as Hle by by eapply StronglySorted_lookup_index_lt. assert (i < s) as His  by lia. assert (k < k) by by eapply H0. by lia.
-    + apply StronglySorted_insert_drop_take; last done. * move => z Hz. destruct (l !! z) eqn:?; naive_solver lia. * move: (elem_of_list_lookup_2 l s y H7) => Hy. rewrite H7 /=.   assert (k ≠ y); [ by set_solver | by lia ].
+    + destruct (decide (i = s)); last eapply H0 => //; by naive_solver lia.
+    + move: (elem_of_list_lookup_1 _ _ H16) => [i Hi]. destruct (decide (y = k)); [ done | exfalso ]. assert (k < y) as Hky by lia. assert (i < s)%nat as Hle by by eapply StronglySorted_lookup_index_lt. assert (i < s) as His  by lia. assert (k < k) by by eapply H0. by lia.
+    + apply StronglySorted_insert_drop_take; last done. * move => z Hz. destruct (l !! z) eqn:? => //=. eapply H0 => //; lia. * move: (elem_of_list_lookup_2 l s y H9) => Hy. rewrite H9 /=. assert (k ≠ y); [ by set_solver | by lia ].
     + assert (s = length l) as -> by lia. assert (k < k); last by lia. move: (elem_of_list_lookup_1 _ _ H7) => [i Hi]. move: (lookup_lt_Some _ _ _ Hi) => Hlt. naive_solver lia.
     + assert (s = length l) as -> by lia. rewrite drop_all. apply StronglySorted_app; [ .. | done | by do 2 constructor ]. move => x y Hx Hy. assert (y = k) as -> by set_solver. move: (elem_of_list_lookup_1 _ _ Hx) => [i Hi]. move: (lookup_lt_Some _ _ _ Hi) => Hlt. naive_solver lia.
     all: print_sidecondition_goal "key_index".

theories/lithium/interpreter.v

@@ -14,6 +14,10 @@ Definition EVAR_ID {A} (x : A) : A := x.
 Arguments EVAR_ID : simpl never.
 
 (** * Lemmas used by tactics *)
+
+Lemma tac_and_learn {P T: Prop}: P → (P → T) → P ∧ T.
+Proof. naive_solver. Qed.
+
 Section coq_tactics.
   Context {Σ : gFunctors}.
 
@@ -645,7 +649,8 @@ Ltac liSideCond :=
         | _ => fail "could not simplify goal with evar"
         end
       ]
-    | _ => split; [ first [ fast_done | shelve ] | ]
+    (* Non-trivila side-conditions are added to the context for the continuation. *)
+    | _ => first [ split; [ fast_done | ] | apply tac_and_learn; [ shelve | ] ]
     end ] end
   | _ => fail "do_side_cond: unknown goal"
   end.