Commit 61e0e3fa by Amin Timany

### Merge branch 'amin/logrel' into 'master'

```Make EqType more realistic

See merge request FP/iris-examples!4```
parents 30b963ae f4fed4c2
Pipeline #7838 passed with stage
in 5 minutes and 46 seconds
 ... @@ -187,7 +187,9 @@ Proof. ... @@ -187,7 +187,9 @@ Proof. Qed. Qed. Definition ctx_refines (Γ : list type) Definition ctx_refines (Γ : list type) (e e' : expr) (τ : type) := ∀ K thp σ v, (e e' : expr) (τ : type) := typed Γ e τ ∧ typed Γ e' τ ∧ ∀ K thp σ v, typed_ctx K Γ τ [] TUnit → typed_ctx K Γ τ [] TUnit → rtc step ([fill_ctx K e], ∅) (of_val v :: thp, σ) → rtc step ([fill_ctx K e], ∅) (of_val v :: thp, σ) → ∃ thp' σ' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ'). ∃ thp' σ' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ'). ... ...
 ... @@ -366,6 +366,6 @@ Theorem counter_ctx_refinement : ... @@ -366,6 +366,6 @@ Theorem counter_ctx_refinement : Proof. Proof. set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (authR cfgUR) ]). set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (authR cfgUR) ]). set (HG := soundness_unary.HeapPreIG Σ _ _). set (HG := soundness_unary.HeapPreIG Σ _ _). eapply (binary_soundness Σ _); auto. eapply (binary_soundness Σ _); auto using FG_counter_type, CG_counter_type. intros. apply FG_CG_counter_refinement. intros. apply FG_CG_counter_refinement. Qed. Qed.