Fixes to abstract_hoare_logic well-foundedness

kth-step · Sep 25, 2023 · 03e4100 · 03e4100
1 parent faea00f
commit 03e4100
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 38 deletions.
diff --git a/src/theory/abstract_hoare_logic/abstract_hoare_logicScript.sml b/src/theory/abstract_hoare_logic/abstract_hoare_logicScript.sml
@@ -28,9 +28,9 @@ val abstract_weak_model_comp_rule_thm = store_thm("abstract_weak_model_comp_rule
     abstract_jgmt m l ls pre post ==>
     abstract_jgmt n l ls pre post``,
 
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 FULL_SIMP_TAC std_ss [abstract_jgmt_def] >>
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 QSPECL_X_ASSUM ``!ms. _`` [`ms`] >>
 QSPECL_X_ASSUM ``!ms. _`` [`ms`] >>
 REV_FULL_SIMP_TAC std_ss [] >>
@@ -80,9 +80,9 @@ val abstract_subset_rule_thm =
     abstract_jgmt m l (ls1 UNION ls2) pre post ==>
     abstract_jgmt m l ls1 pre post``,
 
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 REV_FULL_SIMP_TAC std_ss [abstract_jgmt_def] >>
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 QSPECL_X_ASSUM ``!ms. _`` [`ms`] >>
 METIS_TAC [weak_union_pc_not_in_thm]
 );
@@ -98,9 +98,9 @@ val abstract_seq_rule_thm = store_thm("abstract_seq_rule_thm",
     ) ==>
     abstract_jgmt m l ls2 pre post``,
 
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 SIMP_TAC std_ss [abstract_jgmt_def] >>
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 PAT_X_ASSUM ``abstract_jgmt m l (ls1 UNION ls2) pre post``
               (fn thm => ASSUME_TAC (SIMP_RULE std_ss [abstract_jgmt_def] thm)) >>
 QSPECL_X_ASSUM ``!ms. _`` [`ms`] >>
@@ -128,9 +128,9 @@ val abstract_conj_rule_thm = prove(``
   abstract_jgmt m l ls pre post2 ==>
   abstract_jgmt m l ls pre (\ms. (post1 ms) /\ (post2 ms))``,
 
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 FULL_SIMP_TAC std_ss [abstract_jgmt_def] >>
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 METIS_TAC [weak_unique_thm]
 );
 
@@ -173,20 +173,20 @@ WF_REL_TAC `(\(m, ms, wf_rel, var, l, le, invariant, C1).
               then wf_rel (var ms) (var' ms')
               else F)` >- (
   FULL_SIMP_TAC std_ss [Once relationTheory.WF_DEF] >>
-  REPEAT STRIP_TAC >>
+  rpt strip_tac >>
   Cases_on `?m ms wf_rel var l le invariant C1. B (m,ms,wf_rel,var,l,le,invariant,C1) /\ ~WF wf_rel` >| [
     FULL_SIMP_TAC std_ss [] >>
     Q.EXISTS_TAC `(m,ms,wf_rel,var,l,le,invariant,C1)` >>
     FULL_SIMP_TAC std_ss [] >>
-    REPEAT STRIP_TAC >>
+    rpt strip_tac >>
     PairCases_on `b` >>
     FULL_SIMP_TAC std_ss [] >>
     RW_TAC std_ss [] >>
     FULL_SIMP_TAC std_ss [],
 
     FULL_SIMP_TAC std_ss [] >>
     (* Define B' = {b in B| b.wf_rel = w.wf_rel} *)
-    Q.ABBREV_TAC `get_wf_rel = \loop_fun_st. FST(SND(SND (loop_fun_st:(α, β) bin_model_t #
+    Q.ABBREV_TAC `get_wf_rel = \loop_fun_st. FST(SND(SND (loop_fun_st:(α, β) abstract_model_t #
      α #
      (γ -> γ -> bool) # (α -> γ) # β # (β -> bool) # (α -> bool) # (α -> bool))))` >>
     Q.ABBREV_TAC `B' = \b. (b IN B /\ (get_wf_rel b = get_wf_rel w))` >>
@@ -198,10 +198,10 @@ WF_REL_TAC `(\(m, ms, wf_rel, var, l, le, invariant, C1).
       FULL_SIMP_TAC std_ss [pred_setTheory.IN_ABS, pred_setTheory.IN_APP]
     ) >>
     (* Define A' = {b.var b | b in B'} *)
-    Q.ABBREV_TAC `get_var = \loop_fun_st. FST(SND(SND(SND (loop_fun_st:(α, β) bin_model_t #
+    Q.ABBREV_TAC `get_var = \loop_fun_st. FST(SND(SND(SND (loop_fun_st:(α, β) abstract_model_t #
      α #
      (γ -> γ -> bool) # (α -> γ) # β # (β -> bool) # (α -> bool) # (α -> bool)))))` >>
-    Q.ABBREV_TAC `get_state = \loop_fun_st. FST(SND (loop_fun_st:(α, β) bin_model_t #
+    Q.ABBREV_TAC `get_state = \loop_fun_st. FST(SND (loop_fun_st:(α, β) abstract_model_t #
      α #
      (γ -> γ -> bool) # (α -> γ) # β # (β -> bool) # (α -> bool) # (α -> bool)))` >>
     Q.ABBREV_TAC `A' = IMAGE (\a. ((get_var a) (get_state a))) (\b. b IN B')` >>
@@ -257,15 +257,15 @@ WF_REL_TAC `(\(m, ms, wf_rel, var, l, le, invariant, C1).
       Q.UNABBREV_TAC `B''` >>
       Q.UNABBREV_TAC `B'` >>
       irule SELECT_ELIM_THM >>
-      REPEAT STRIP_TAC >| [
+      rpt strip_tac >| [
         FULL_SIMP_TAC std_ss [pred_setTheory.IN_ABS, pred_setTheory.IN_APP],
 
         FULL_SIMP_TAC std_ss [GSYM pred_setTheory.MEMBER_NOT_EMPTY] >>
         Q.EXISTS_TAC `x'''` >>
         FULL_SIMP_TAC std_ss [pred_setTheory.IN_ABS]
       ],
 
-      REPEAT STRIP_TAC >>
+      rpt strip_tac >>
       PairCases_on `b` >>
       PairCases_on `min_wf` >>
       FULL_SIMP_TAC std_ss [] >>
@@ -296,7 +296,7 @@ WF_REL_TAC `(\(m, ms, wf_rel, var, l, le, invariant, C1).
     ]
   ]
 ) >>
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 FULL_SIMP_TAC std_ss [LET_DEF] >>
 IMP_RES_TAC pred_setTheory.CHOICE_DEF >>
 FULL_SIMP_TAC std_ss [pred_setTheory.CHOICE_DEF] >>
@@ -306,10 +306,10 @@ FULL_SIMP_TAC std_ss [pred_setTheory.IN_ABS]
 
 
 val abstract_loop_jgmt_def = Define `
-  abstract_loop_jgmt m l le invariant C1 wf_rel var =
+  abstract_loop_jgmt m l le invariant C1 wf_rel var <=>
     l NOTIN le /\ WF wf_rel /\
-    (!x. (abstract_jgmt m l ({l} UNION le) (\ms. invariant ms /\ C1 ms /\ (var ms = x))
-         (\ms. (m.pc ms = l) /\ invariant ms /\ (wf_rel (var ms) x))))
+    !x. abstract_jgmt m l ({l} UNION le) (\ms. invariant ms /\ C1 ms /\ var ms = x)
+         (\ms. m.pc ms = l /\ invariant ms /\ wf_rel (var ms) x)
 `;
 
 (* Note that due to loop_fun_ind relating states ms and ms' at loop points,
@@ -405,9 +405,9 @@ Q.SUBGOAL_THEN `l NOTIN le` (fn thm => fs [thm]) >- (
   fs [abstract_loop_jgmt_def, pred_setTheory.IN_SING]
 )
 *)
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 FULL_SIMP_TAC std_ss [] >>
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 (* We first prove that one iteration works *)
 subgoal `(weak_loop_step m ms wf_rel var l le invariant C1) <> {}`  >- (
   SIMP_TAC std_ss [weak_loop_step_def, LET_DEF] >>
@@ -493,22 +493,18 @@ val abstract_loop_rule_thm = store_thm("abstract_loop_rule_thm",
     abstract_jgmt m l le (\ms. invariant ms /\ ~C1 ms) post ==>
     abstract_jgmt m l le invariant post``,
 
-
-metis_tac [abstract_jgmt_def, abstract_loop_rule_tmp_thm]
-(* OLD:
-REPEAT STRIP_TAC >>
+rpt strip_tac >>
 SIMP_TAC std_ss [abstract_jgmt_def] >>
-REPEAT STRIP_TAC >>
-ASSUME_TAC (Q.SPECL [`m`, `ms`, `wf_rel`, `var`, `l`, `le`, `invariant`, `C1`] invariant_rule_tmp_thm) >>
+rpt strip_tac >>
+ASSUME_TAC (Q.SPECL [`m`, `ms`, `wf_rel`, `var`, `l`, `le`, `invariant`, `C1`] abstract_loop_rule_tmp_thm) >>
 FULL_SIMP_TAC std_ss [] >>
 REV_FULL_SIMP_TAC std_ss [] >>
 Cases_on `C1 ms` >- (
   FULL_SIMP_TAC std_ss [] >>
   Q.EXISTS_TAC `ms'`>>
   FULL_SIMP_TAC std_ss []
 ) >>
-FULL_SIMP_TAC std_ss [abstract_jgmt_def] 
-*)
+FULL_SIMP_TAC std_ss [abstract_jgmt_def]
 );
 
 val _ = export_theory();
diff --git a/src/theory/abstract_hoare_logic/abstract_hoare_logic_partialScript.sml b/src/theory/abstract_hoare_logic/abstract_hoare_logic_partialScript.sml
@@ -1,4 +1,4 @@
-open HolKernel boolLib bossLib BasicProvers dep_rewrite;
+open HolKernel boolLib bossLib BasicProvers dep_rewrite prim_recTheory;
 
 open bir_auxiliaryLib;
 
@@ -225,7 +225,7 @@ subgoal `abstract_jgmt m l le (\s'. (^invariant) s' /\ ~(C1 s')) post` >- (
 ) >>
 
 (* 2. Prove loop iteration contract *)
-subgoal `abstract_loop_jgmt m l le (^invariant) C1 (^variant)` >- (
+subgoal `abstract_loop_jgmt m l le (^invariant) C1 $< (^variant)` >- (
  fs [abstract_loop_jgmt_def, abstract_jgmt_def] >>
  rpt strip_tac >>
  subgoal `s <> ms'` >- (
@@ -281,6 +281,7 @@ subgoal `abstract_loop_jgmt m l le (^invariant) C1 (^variant)` >- (
  ]
 ) >>
 
+ASSUME_TAC WF_LESS >>
 imp_res_tac abstract_loop_rule_thm >>
 fs [abstract_jgmt_def] >>
 (* TODO: Should be provable using trs_to_ls m ({l} UNION le) ms n (SUC n_l) = SOME ms' *)

diff --git a/src/theory/abstract_hoare_logic/abstract_simp_hoare_logicScript.sml b/src/theory/abstract_hoare_logic/abstract_simp_hoare_logicScript.sml
@@ -518,12 +518,13 @@ REV_FULL_SIMP_TAC std_ss []
 val abstract_simp_loop_rule_thm = store_thm("abstract_simp_loop_rule_thm",
   ``!m.
     weak_model m ==>
-    !l wl bl invariant C1 var post.
+    !l wl bl invariant C1 wf_rel var post.
+    WF wf_rel ==>
     l NOTIN wl ==> 
     l NOTIN bl ==>
     (!x. abstract_simp_jgmt m invariant l ({l} UNION wl) bl
-      (\ms. C1 ms /\ (var ms = (x:num)))
-      (\ms. (m.pc ms = l) /\ var ms < x /\ var ms >= 0)) ==>
+      (\ms. C1 ms /\ var ms = x)
+      (\ms. m.pc ms = l /\ wf_rel (var ms) x)) ==>
     abstract_simp_jgmt m (\ms. T) l wl bl (\ms. ~(C1 ms) /\ invariant ms) post ==>
     abstract_simp_jgmt m (\ms. T) l wl bl invariant post``,
 
@@ -533,16 +534,17 @@ irule abstract_loop_rule_thm >>
 FULL_SIMP_TAC std_ss [] >>
 Q.EXISTS_TAC `C1` >>
 Q.EXISTS_TAC `var` >>
+Q.EXISTS_TAC `wf_rel` >>
 FULL_SIMP_TAC (std_ss++pred_setLib.PRED_SET_ss)
   [abstract_loop_jgmt_def, Once boolTheory.CONJ_SYM] >>
 STRIP_TAC >>
 QSPECL_X_ASSUM ``!x. _`` [`x`] >>  
 irule abstract_conseq_rule_thm >>
 FULL_SIMP_TAC std_ss [] >>
-Q.EXISTS_TAC `(\ms.
-                m.pc ms NOTIN bl /\ ((m.pc ms = l) /\ var ms < x) /\
-                invariant ms)` >>
-Q.EXISTS_TAC `(\ms. (C1 ms /\ (var ms = x)) /\ invariant ms)` >>
+Q.EXISTS_TAC `\ms.
+                m.pc ms NOTIN bl /\ (m.pc ms = l /\ wf_rel (var ms) x) /\
+                invariant ms` >>
+Q.EXISTS_TAC `\ms. (C1 ms /\ var ms = x) /\ invariant ms` >>
 FULL_SIMP_TAC (std_ss++pred_setLib.PRED_SET_ss) [pred_setTheory.UNION_ASSOC]
 );