Commit dd6f44a4 authored by Ralf Jung's avatar Ralf Jung

add some missing timeless instances; fix auth.v eauto usage and argument implicity

On branch master
	modified:   algebra/fin_maps.v
Untracked files:
	heap_lang/heap.v
no changes added to commit (use "git add" and/or "git commit -a")
parent f0b605c5
......@@ -57,6 +57,11 @@ Proof.
[by constructor|by apply lookup_ne].
Qed.
Global Instance map_timeless `{! a : A, Timeless a} (g : gmap K A) : Timeless g.
Proof.
intros m Hm i. apply timeless; eauto with typeclass_instances.
Qed.
Instance map_empty_timeless : Timeless ( : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
......
......@@ -51,6 +51,8 @@ Global Instance None_timeless : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
Global Instance Some_timeless x : Timeless x Timeless (Some x).
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
Global Instance option_timeless `{! a : A, Timeless a} (mx : option A) : Timeless mx.
Proof. destruct mx; auto with typeclass_instances. Qed.
End cofe.
Arguments optionC : clear implicits.
......
......@@ -62,7 +62,7 @@ Section auth.
apply (eq_rewrite b (a a')
(λ x, ■✓x ▷φ x own AuthI γ ( x a))%I).
{ by move=>n ? ? /timeless_iff ->. }
{ apply sep_elim_l', sep_elim_r'. done. (* FIXME why does "eauto using I" not work? *) }
{ by eauto with I. }
rewrite const_equiv // left_id comm.
apply sep_mono; first done.
by rewrite sep_elim_l.
......@@ -84,7 +84,7 @@ Section auth.
step-indices. However, since A is timeless, that should not be
a restriction. *)
Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
`{!LocalUpdate Lv L} N E P (Q : X iPropG Λ Σ) γ a :
L `{!LocalUpdate Lv L} N E P (Q : X iPropG Λ Σ) γ a :
nclose N E
P auth_ctx AuthI γ N φ
P (auth_own AuthI γ a ( a', ■✓(a a') ▷φ (a a') -
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment