Commit 5d4ee871 authored by Amin Timany's avatar Amin Timany
Browse files

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents 011cd852 0e49878b
......@@ -6,11 +6,11 @@ buildjob:
script:
- coqc -v
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'grep Axiom build-log.txt && exit 1'
- 'fgrep Axiom build-log.txt && exit 1'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- make validate
only:
- master
- jh_simplified_resources
artifacts:
paths:
- build-time.txt
In this changelog, we document "large-ish" changes to Iris that affect even the
way the logic is used on paper. We also mention some significant changes in the
Coq development, but not every API-breaking change is listed. Changes marked
[#] still need to be ported to the Iris Documentation LaTeX file.
[#] still need to be ported to the Iris Documentation LaTeX file(s).
## Iris 2.0
## Iris 3.0
* [#] View shifts are radically simplified to just internalize frame-preserving
updates. Weakestpre is defined inside the logic, and invariants and view
shifts with masks are also coded up inside Iris. Adequacy of weakestpre
is proven in the logic.
* [#] With invariants and the physical state being handled in the logic, there
is no longer any reason to demand the CMRA unit to be discrete.
* [#] The language can now fork off multiple threads at once.
This version accompanies the final ICFP paper.
## Iris 2.0
* [# algebra] Make the core of an RA or CMRA a partial function.
* [heap_lang] No longer use dependent types for expressions. Instead, values
carry a proof of closedness. Substitution, closedness and value-ness proofs
are performed by computation after reflecting into a term langauge that knows
about values and closed expressions.
* [program_logic/language] The language does not define its own "atomic"
predicate. Instead, atomicity is defined as reducing in one step to a value.
* [program_logic] Due to a lack of maintenance and usefulness, lifting lemmas
for Hoare triples are removed.
## Iris 2.0-rc2
This version matches the final ICFP paper.
* [algebra] Make the core of an RA or CMRA a partial function.
* [program_logic/lifting] Lifting lemmas no longer round-trip through a
user-chosen predicate to define the configurations we can reduce to; they
directly relate to the operational semantics. This is equivalent and
much simpler to read.
## Iris 2.0-rc1
......
# Makefile originally taken from coq-club
%: Makefile.coq
%: Makefile.coq phony
+make -f Makefile.coq $@
all: Makefile.coq
......@@ -17,4 +17,6 @@ _CoqProject: ;
Makefile: ;
.PHONY: all clean
phony: ;
.PHONY: all clean phony
Tactic overview
===============
Many of the tactics below apply to more goals than described in this document
since the behavior of these tactics can be tuned via instances of the type
classes in the file `proofmode/classes`. Most notable, many of the tactics can
be applied when the to be introduced or to be eliminated connective appears
under a later, a primitive view shift, or in the conclusion of a weakest
precondition connective.
Applying hypotheses and lemmas
------------------------------
- `iExact "H"` : finish the goal if the conclusion matches the hypothesis `H`
- `iAssumption` : finish the goal if the conclusion matches any hypothesis
- `iApply trm` : match the conclusion of the current goal against the
conclusion of `tetrmrm` and generates goals for the premises of `trm`. See
- `iApply pm_trm` : match the conclusion of the current goal against the
conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
proof mode terms below.
Context management
......@@ -23,9 +30,10 @@ Context management
`x1 ... xn` into universal quantifiers. The symbol `★` can be used to revert
the entire spatial context.
- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
- `iSpecialize trm` : instantiate universal quantifiers and eliminate
implications/wands of a hypothesis `trm`. See proof mode terms below.
- `iPoseProof trm as "H"` : put `trm` into the context as a new hypothesis `H`.
- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
- `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
`H`.
- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
put `P` in the context of the original goal. The specialization pattern
`spat` specifies which hypotheses will be consumed by proving `P` and the
......@@ -52,17 +60,21 @@ Elimination of logical connectives
----------------------------------
- `iExFalso` : Ex falso sequitur quod libet.
- `iDestruct trm as (x1 ... xn) "spat1 ... spatn"` : elimination of existential
quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
object level connectives using the proof mode introduction patterns
`ipat1 ... ipatn`.
- `iDestruct trm as %cpat` : elimination of a pure hypothesis using the Coq
- `iDestruct pm_trm as (x1 ... xn) "spat1 ... spatn"` : elimination of
existential quantifiers using Coq introduction patterns `x1 ... xn` and
elimination of object level connectives using the proof mode introduction
patterns `ipat1 ... ipatn`.
- `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
introduction pattern `cpat`.
Separating logic specific tactics
---------------------------------
- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal.
- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. The
symbol `★` can be used to frame as much of the spatial context as possible,
and the symbol `#` can be used to repeatedly frame as much of the persistent
context as possible. When without arguments, it attempts to frame all spatial
hypotheses.
- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
`H : P1 ★ P2`.
......@@ -75,20 +87,20 @@ The later modality
Rewriting
---------
- `iRewrite trm` : rewrite an equality in the conclusion.
- `iRewrite trm in "H"` : rewrite an equality in the hypothesis `H`.
- `iRewrite pm_trm` : rewrite an equality in the conclusion.
- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
Iris
----
- `iPvsIntro` : introduction of a primitive view shift. Generates a goal if
the masks are not syntactically equal.
- `iPvs trm as (x1 ... xn) "ipat"` : runs a primitive view shift `trm`.
- `iVsIntro` : introduction of a raw or primitive view shift.
- `iVs pm_trm as (x1 ... xn) "ipat"` : run a raw or primitive view shift
`pm_trm` (if the goal permits, i.e. it is a raw or primitive view shift, or
a weakest precondition).
- `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
- `iInv> N as (x1 ... xn) "ipat"` : open the invariant `N` and establish that
it is timeless so no laters have to be added.
- `iTimeless "H"` : strip a later of a timeless hypotheses `H` in case the
conclusion is a primitive view shifts or weakest precondition.
- `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal
permits, i.e. it is a later, True now, raw or primitive view shift, or a
weakest precondition).
Miscellaneous
-------------
......@@ -111,20 +123,24 @@ introduction patterns:
- `?` : create an anonymous hypothesis.
- `_` : remove the hypothesis.
- `$` : frame the hypothesis in the goal.
- `# ipat` : move the hypothesis to the persistent context.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `[ipat ipat]` : (separating) conjunction elimination.
- `[ipat|ipat]` : disjunction elimination.
- `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `# ipat` : move the hypothesis to the persistent context.
- `> ipat` : remove a later of a timeless hypothesis (if the goal permits).
- `==> ipat` : run a view shift (if the goal permits).
Apart from this, there are the following introduction patterns that can only
appear at the top level:
- `!` : introduce a box (provided that the spatial context is empty).
- `>` : introduce a later (which strips laters from all hypotheses).
- `{H1 ... Hn}` : clear `H1 ... Hn`.
- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
previous pattern, e.g., `{$H1 H2 $H3}`).
- `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an always modality (given that the spatial context is empty).
- `!>` : introduce a later (which strips laters from all hypotheses).
- `!==>` : introduce a view shift.
- `/=` : perform `simpl`.
- `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands.
......@@ -135,7 +151,7 @@ For example, given:
You can write
iIntros (x) "% ! $ [[] | #[HQ HR]] /= >".
iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
which results in:
......@@ -161,7 +177,7 @@ so called specification patterns to express this splitting:
- `[H1 ... Hn]` : generate a goal with the spatial hypotheses `H1 ... Hn` and
all persistent hypotheses. The hypotheses `H1 ... Hn` will be consumed.
- `[-H1 ... Hn]` : negated form of the above pattern
- `=>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is a primitive view shift, in which case the view shift will be kept in the
goal of the premise too.
- `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
......@@ -186,7 +202,7 @@ Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
take both hypotheses and lemmas, and allow one to instantiate universal
quantifiers and implications/wands of these hypotheses/lemmas on the fly.
The syntax for the arguments, called _proof mode terms_, of these tactics is:
The syntax for the arguments of these tactics, called _proof mode terms_, is:
(H $! t1 ... tn with "spat1 .. spatn")
......
......@@ -66,25 +66,25 @@ program_logic/model.v
program_logic/adequacy.v
program_logic/lifting.v
program_logic/invariants.v
program_logic/viewshifts.v
program_logic/wsat.v
program_logic/ownership.v
program_logic/weakestpre.v
program_logic/weakestpre_fix.v
program_logic/pviewshifts.v
program_logic/resources.v
program_logic/hoare.v
program_logic/viewshifts.v
program_logic/language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_lifting.v
program_logic/ghost_ownership.v
program_logic/global_functor.v
program_logic/saved_prop.v
program_logic/auth.v
program_logic/sts.v
program_logic/namespaces.v
program_logic/boxes.v
program_logic/counter_examples.v
program_logic/iris.v
program_logic/thread_local.v
program_logic/cancelable_invariants.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
......@@ -96,20 +96,24 @@ heap_lang/lib/spawn.v
heap_lang/lib/par.v
heap_lang/lib/assert.v
heap_lang/lib/lock.v
heap_lang/lib/spin_lock.v
heap_lang/lib/ticket_lock.v
heap_lang/lib/counter.v
heap_lang/lib/barrier/barrier.v
heap_lang/lib/barrier/specification.v
heap_lang/lib/barrier/protocol.v
heap_lang/lib/barrier/proof.v
heap_lang/proofmode.v
heap_lang/adequacy.v
tests/atomic.v
tests/heap_lang.v
tests/program_logic.v
tests/one_shot.v
tests/joining_existentials.v
tests/proofmode.v
tests/barrier_client.v
tests/list_reverse.v
tests/tree_sum.v
tests/counter.v
proofmode/coq_tactics.v
proofmode/pviewshifts.v
proofmode/environments.v
......@@ -120,5 +124,5 @@ proofmode/notation.v
proofmode/invariants.v
proofmode/weakestpre.v
proofmode/ghost_ownership.v
proofmode/sts.v
proofmode/classes.v
proofmode/class_instances.v
......@@ -108,7 +108,7 @@ Proof.
symmetry; apply dist_le with n; try apply Hx; auto.
- intros x. apply agree_idemp.
- by intros n x y [(?&?&?) ?].
- intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
- intros n x y1 y2 Hval Hx; exists x, x; simpl; split.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
......
......@@ -134,10 +134,10 @@ Proof.
naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
- intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend n (authoritative x) (authoritative y1)
(authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
(authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
as (b&?&?&?); auto using auth_own_validN.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
as (b1&b2&?&?&?); auto using auth_own_validN.
by exists (Auth ea1 b1), (Auth ea2 b2).
Qed.
Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
......@@ -156,7 +156,6 @@ Proof.
split; simpl.
- apply (@ucmra_unit_valid A).
- by intros x; constructor; rewrite /= left_id.
- apply _.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure authUR :=
......@@ -191,11 +190,17 @@ Proof.
exists bf2. rewrite -assoc.
apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
Qed.
Lemma auth_update_no_frame a b : a ~l~> b @ Some a a ~~> b b.
Proof.
intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
by apply auth_update.
Qed.
Lemma auth_update_no_frag af b : ~l~> b @ Some af af ~~> (b af) b.
Proof.
intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ ( _)).
by apply auth_update.
Qed.
End cmra.
Arguments authR : clear implicits.
......@@ -235,6 +240,28 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Program Definition authRF (F : urFunctor) : rFunctor := {|
rFunctor_car A B := authR (urFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
apply auth_map_ext=>y; apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply urFunctor_compose.
Qed.
Instance authRF_contractive F :
urFunctorContractive F rFunctorContractive (authRF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
Qed.
Program Definition authURF (F : urFunctor) : urFunctor := {|
urFunctor_car A B := authUR (urFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
......
......@@ -53,7 +53,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
mixin_cmra_validN_op_l n x y : {n} (x y) {n} x;
mixin_cmra_extend n x y1 y2 :
{n} x x {n} y1 y2
{ z | x z.1 z.2 z.1 {n} y1 z.2 {n} y2 }
z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2
}.
(** Bundeled version *)
......@@ -120,7 +120,7 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Lemma cmra_extend n x y1 y2 :
{n} x x {n} y1 y2
{ z | x z.1 z.2 z.1 {n} y1 z.2 {n} y2 }.
z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
End cmra_mixin.
......@@ -153,7 +153,6 @@ Arguments core' _ _ _ /.
Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
mixin_ucmra_unit_valid : ;
mixin_ucmra_unit_left_id : LeftId () ();
mixin_ucmra_unit_timeless : Timeless ;
mixin_ucmra_pcore_unit : pcore Some
}.
......@@ -201,8 +200,6 @@ Section ucmra_mixin.
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_left_id : LeftId () (@op A _).
Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_timeless : Timeless ( : A).
Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
Lemma ucmra_pcore_unit : pcore (:A) Some .
Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
......@@ -324,7 +321,7 @@ Proof. by apply cmra_pcore_dup' with x. Qed.
(** ** Exclusive elements *)
Lemma exclusiveN_l n x `{!Exclusive x} y : {n} (x y) False.
Proof. intros ?%cmra_validN_le%exclusive0_l; auto with arith. Qed.
Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
Lemma exclusiveN_r n x `{!Exclusive x} y : {n} (y x) False.
Proof. rewrite comm. by apply exclusiveN_l. Qed.
Lemma exclusive_l x `{!Exclusive x} y : (x y) False.
......@@ -332,7 +329,7 @@ Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
Lemma exclusive_r x `{!Exclusive x} y : (y x) False.
Proof. rewrite comm. by apply exclusive_l. Qed.
Lemma exclusiveN_opM n x `{!Exclusive x} my : {n} (x ? my) my = None.
Proof. destruct my. move=> /(exclusiveN_l _ x) []. done. Qed.
Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
(** ** Order *)
Lemma cmra_included_includedN n x y : x y x {n} y.
......@@ -472,16 +469,16 @@ End total_core.
Lemma cmra_timeless_included_l x y : Timeless x {0} y x {0} y x y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy (timeless x z).
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y x {0} y x {n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
Lemma cmra_timeless_included_r x y : Timeless y x {0} y x y.
Proof. intros ? [x' ?]. exists x'. by apply (timeless y). Qed.
Lemma cmra_op_timeless x1 x2 :
(x1 x2) Timeless x1 Timeless x2 Timeless (x1 x2).
Proof.
intros ??? z Hz.
destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
{ rewrite -?Hz. by apply cmra_valid_validN. }
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed.
......@@ -504,8 +501,6 @@ Section ucmra.
Context {A : ucmraT}.
Implicit Types x y z : A.
Global Instance ucmra_unit_inhabited : Inhabited A := populate .
Lemma ucmra_unit_validN n : {n} (:A).
Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
Lemma ucmra_unit_leastN n x : {n} x.
......@@ -542,7 +537,7 @@ Section cmra_total.
Context (validN_op_l : n (x y : A), {n} (x y) {n} x).
Context (extend : n (x y1 y2 : A),
{n} x x {n} y1 y2
{ z | x z.1 z.2 z.1 {n} y1 z.2 {n} y2 }).
z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2).
Lemma cmra_total_mixin : CMRAMixin A.
Proof.
split; auto.
......@@ -692,7 +687,7 @@ Section discrete.
Proof.
destruct ra_mix; split; try done.
- intros x; split; first done. by move=> /(_ 0).
- intros n x y1 y2 ??; by exists (y1,y2).
- intros n x y1 y2 ??; by exists y1, y2.
Qed.
End discrete.
......@@ -883,9 +878,9 @@ Section prod.
exists (z1,z2). by rewrite prod_included prod_pcore_Some.
- intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
- intros n x y1 y2 [??] [??]; simpl in *.
destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
by exists ((z1.1,z2.1),(z1.2,z2.2)).
destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z11&z12&?&?&?); auto.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
by exists (z11,z21), (z12,z22).
Qed.
Canonical Structure prodR :=
CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
......@@ -924,7 +919,6 @@ Section prod_unit.
split.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- by intros ? [??]; split; apply (timeless _).
- rewrite prod_pcore_Some'; split; apply (persistent _).
Qed.
Canonical Structure prodUR :=
......@@ -1050,13 +1044,12 @@ Section option.
eauto using cmra_validN_op_l.
- intros n mx my1 my2.
destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
try (by exfalso; inversion Hx'; auto).
+ destruct (cmra_extend n x y1 y2) as ([z1 z2]&?&?&?); auto.
{ by inversion_clear Hx'. }
by exists (Some z1, Some z2); repeat constructor.
+ by exists (Some x,None); inversion Hx'; repeat constructor.
+ by exists (None,Some x); inversion Hx'; repeat constructor.
+ exists (None,None); repeat constructor.
inversion_clear Hx'; auto.
+ destruct (cmra_extend n x y1 y2) as (z1&z2&?&?&?); auto.
by exists (Some z1), (Some z2); repeat constructor.
+ by exists (Some x), None; repeat constructor.
+ by exists None, (Some x); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
Canonical Structure optionR :=
CMRAT (option A) option_cofe_mixin option_cmra_mixin.
......@@ -1066,7 +1059,7 @@ Section option.
Instance option_empty : Empty (option A) := None.
Lemma option_ucmra_mixin : UCMRAMixin optionR.
Proof. split. done. by intros []. by inversion_clear 1. done. Qed.
Proof. split. done. by intros []. done. Qed.
Canonical Structure optionUR :=
UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
......
......@@ -188,12 +188,21 @@ Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
Section fixpoint.
Context {A : cofeT} `{Inhabited A} (f : A A) `{!Contractive f}.
Lemma fixpoint_unfold : fixpoint f f (fixpoint f).
Proof.
apply equiv_dist=>n.
rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Qed.
Lemma fixpoint_unique (x : A) : x f x x fixpoint f.
Proof.
rewrite !equiv_dist=> Hx n. induction n as [|n IH]; simpl in *.
- rewrite Hx fixpoint_unfold; eauto using contractive_0.
- rewrite Hx fixpoint_unfold. apply (contractive_S _), IH.
Qed.
Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
( z, f z {n} g z) fixpoint f {n} fixpoint g.
Proof.
......@@ -208,6 +217,8 @@ Section fixpoint.
End fixpoint.
(** Function space *)
(* We make [cofe_fun] a definition so that we can register it as a canonical
structure. *)
Definition cofe_fun (A : Type) (B : cofeT) := A B.
Section cofe_fun.
......@@ -673,8 +684,6 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Next {_} _.
Arguments later_car {_} _.
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Proof. by destruct x. Qed.
Section later.
Context {A : cofeT}.
......
......@@ -106,17 +106,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
Lemma gg_gg {k i i1 i2 j} : (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
Proof.
assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1.
intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1.
induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
[by rewrite coerce_id|by rewrite g_coerce IH].
Qed.
Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
Lemma ff_ff {k i i1 i2 j} : (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof.
assert (i = i1 + i2) by lia; simplify_eq/=.
intros ? <- x. assert (i = i1 + i2) as -> by lia.
induction i1 as [|i1 IH]; simplify_eq/=;
[by rewrite coerce_id|by rewrite coerce_f IH].
Qed.
......
......@@ -209,15 +209,13 @@ Proof.
exists (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinl) in Hx'.
destruct (cmra_extend n a a1 a2) as ([z1 z2]&?&?&?); auto.
exists (Cinl z1, Cinl z2). by repeat constructor.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinr) in Hx'.
destruct (cmra_extend n b b1 b2) as ([z1 z2]&?&?&?); auto.
exists (Cinr z1, Cinr z2). by repeat constructor.
+ by exists (CsumBot, CsumBot); destruct y1, y2; inversion_clear Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); auto.
exists (Cinl z1), (Cinl z2). by repeat constructor.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); auto.
exists (Cinr z1), (Cinr z2). by repeat constructor.
+ by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
Qed.
Canonical Structure csumR :=
CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.
......
......@@ -167,10 +167,10 @@ Proof.
- intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
- intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
destruct (dra_core_mono x z) as (z'&Hz').
unshelve eexists (Validity z' (px py pz) _);