derive more adequacy results

theories/examples/refinements/refinement.v

@@ -851,3 +851,44 @@ Section adequacy.
     Qed.
 
 End adequacy.
+
+Definition heapΣ SI : gFunctors SI := #[invΣ SI; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
+Instance subG_heapPreG {SI} {Σ: gFunctors SI} : subG (heapΣ SI) Σ → heapPreG Σ.
+Proof. solve_inG. Qed.
+
+Definition refΣ SI := #[heapΣ SI; na_invΣ; #[GFunctor (constRF (authR (cfgUR SI)))]; fmlistΣ (cfg heap_lang); na_invΣ; #[GFunctor (constRF (authR (natA SI)))]].
+
+Instance subG_refΣ_rheapPreG {SI} {Σ: gFunctors SI} : subG (refΣ SI) Σ → rheapPreG Σ.
+Proof.
+  intros ?. split; solve_inG.
+Qed.
+
+Instance subG_refΣ_na_invG Σ : subG (refΣ ordI) Σ → na_invG Σ.
+Proof. solve_inG. Qed.
+
+Instance subG_refΣ_source_natG Σ : subG (refΣ ordI) Σ → inG Σ (authR (natA ordI)).
+Proof. solve_inG. Qed.
+
+Section adequacy_ordinals_closed.
+  Context `{C: Classical} {Σ: gFunctors ordI} `{Hsub: !subG (refΣ ordI) Σ}.
+
+  Theorem heap_lang_ref_adequacy_closed (φ: val → val → Prop) (s t: expr) σ σ_src:
+    (∀ `{!rheapG Σ} `{!seqG Σ} `{!auth_sourceG Σ (natA ordI)}, src s ⊢ SEQ t ⟨⟨ v, ∃ v': val, src v' ∗ ⌜φ v v'⌝ ⟩⟩) →
+    (∀ σ' v, rtc erased_step ([t], σ) ([Val v], σ') → ∃ v': val, ∃ σ_src' ts, rtc erased_step ([s], σ_src) (Val v' :: ts, σ_src') ∧ φ v v') ∧
+    (sn erased_step ([s], σ_src) → sn erased_step ([t], σ)).
+  Proof using Hsub C.
+    apply heap_lang_ref_adequacy.
+  Qed.
+End adequacy_ordinals_closed.
+
+From Coq.Logic Require Import Classical_Prop.
+
+Theorem heap_lang_ref_adequacy_fully_closed (φ: val → val → Prop) (s t: expr) σ σ_src:
+  (∀ `{!rheapG (refΣ ordI)} `{!seqG (refΣ ordI)} `{!auth_sourceG (refΣ ordI) (natA ordI)}, src s ⊢ SEQ t ⟨⟨ v, ∃ v': val, src v' ∗ ⌜φ v v'⌝ ⟩⟩) →
+  (∀ σ' v, rtc erased_step ([t], σ) ([Val v], σ') → ∃ v': val, ∃ σ_src' ts, rtc erased_step ([s], σ_src) (Val v' :: ts, σ_src') ∧ φ v v') ∧
+  (sn erased_step ([s], σ_src) → sn erased_step ([t], σ)).
+Proof.
+  assert (Classical).
+  { intros P. apply classic. }
+  apply heap_lang_ref_adequacy_closed.
+Qed.
\ No newline at end of file

theories/examples/termination/adequacy.v

@@ -62,6 +62,32 @@ Section adequacy_ord.
   Proof using C Σ Hpre Hna Htc.
     apply heap_lang_ref_adequacy.
   Qed.
-  Print Assumptions heap_lang_ref_adequacy_ord.
 
 End adequacy_ord.
+
+
+Definition heapΣ SI : gFunctors SI := #[invΣ SI; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
+Instance subG_heapPreG {SI} {Σ: gFunctors SI} : subG (heapΣ SI) Σ → heapPreG Σ.
+Proof. solve_inG. Qed.
+
+Definition tcΣ SI: gFunctors SI := #[GFunctor (constRF (authR (ordA SI)))].
+Local Instance subG_tcΣ {SI} {Σ: gFunctors SI} : subG (tcΣ SI) Σ → inG Σ (authR (ordA SI)).
+Proof. solve_inG. Qed.
+
+Definition termΣ SI := #[heapΣ SI; na_invΣ; tcΣ SI].
+
+From Coq.Logic Require Import Classical_Prop.
+
+Theorem heap_lang_ref_adequacy_closed (e: expr) σ:
+  (∀ `{heapG ordI (termΣ ordI)} `{!seqG (termΣ ordI)} `{!auth_sourceG (termΣ ordI) (ordA ordI)},
+    True ⊢ (∃ α, $α -∗ SEQ e ⟨⟨ v, True ⟩⟩)%I
+  ) →
+  sn erased_step ([e], σ).
+Proof.
+  assert (Classical).
+  { intros P. apply classic. }
+
+  apply heap_lang_ref_adequacy.
+Qed.
+
+Print Assumptions heap_lang_ref_adequacy_closed.
\ No newline at end of file

theories/examples/termination/logrel.v

@@ -850,7 +850,7 @@ From iris.examples.termination Require Import adequacy.
 Section adequacy.
 
   Context {SI} `{C: Classical}  {Σ: gFunctors SI} {Hlarge: LargeIndex SI}.
-  Context `{Hpre: !heapPreG Σ} `{Hna: !na_invG Σ} `{Htc: !inG Σ (authR (ordA SI))}.
+  Context `{Hpre: !heapPreG Σ} `{Hna: !na_invG Σ} `{Htc: !inG Σ (authR (ordA SI))} `{Tok: !inG Σ (exclR (unitO SI))}.
 
   Theorem simple_logrel_adequacy (e: expr) σ A:
     (∀ `{heapG SI Σ} `{!seqG Σ} `{!auth_sourceG Σ (ordA SI)},
@@ -890,7 +890,7 @@ End adequacy.
 
 Section ordinals.
   Context `{C: Classical}  {Σ: gFunctors ordI}.
-  Context `{Hpre: !heapPreG Σ} `{Hna: !na_invG Σ} `{Htc: !inG Σ (authR (ordA ordI))}.
+  Context `{Hpre: !heapPreG Σ} `{Hna: !na_invG Σ} `{Htc: !inG Σ (authR (ordA ordI))} `{Tok: !inG Σ (exclR (unitO ordI))}.
 
   Theorem simple_logrel_adequacy_ord (e: expr) σ A:
     (∀ `{heapG ordI Σ} `{!seqG Σ} `{!auth_sourceG Σ (ordA ordI)},
@@ -928,3 +928,33 @@ Section ordinals.
 
 End ordinals.
 
+
+Definition logrelΣ := #[termΣ ordI; GFunctor (constRF (exclR (unitO ordI)))].
+Instance subG_logrelΣ_tok {Σ: gFunctors ordI} : subG (logrelΣ) Σ → inG Σ (exclR (unitO ordI)).
+Proof. solve_inG. Qed.
+
+From Coq.Logic Require Import Classical_Prop.
+
+Theorem simple_logrel_adequacy_closed (e: expr) σ A:
+(∀ `{heapG ordI logrelΣ} `{!seqG logrelΣ} `{!auth_sourceG logrelΣ (ordA ordI)},
+  ltyped ∅ e A
+) →
+sn erased_step ([e], σ).
+Proof.
+  assert (Classical).
+  { intros P. apply classic. }
+  unshelve eapply simple_logrel_adequacy_ord.
+  apply subG_tcΣ. apply _.
+Qed.
+
+Theorem logrel_adequacy_closed (e: expr) σ A:
+(∀ `{heapG ordI logrelΣ} `{!seqG logrelΣ} `{!auth_sourceG logrelΣ (ordA ordI)},
+  lptyped ∅ ∅ e A
+) →
+sn erased_step ([e], σ).
+Proof.
+  assert (Classical).
+  { intros P. apply classic. }
+  unshelve eapply logrel_adequacy_ord.
+  apply subG_tcΣ. apply _.
+Qed.
\ No newline at end of file