Commit 4be0320e authored by Ralf Jung's avatar Ralf Jung
Browse files

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

parents 12012db9 7a58ae18
...@@ -34,7 +34,7 @@ theories/base_logic/hlist.v ...@@ -34,7 +34,7 @@ theories/base_logic/hlist.v
theories/base_logic/soundness.v theories/base_logic/soundness.v
theories/base_logic/double_negation.v theories/base_logic/double_negation.v
theories/base_logic/deprecated.v theories/base_logic/deprecated.v
theories/base_logic/fix.v theories/base_logic/fixpoint.v
theories/base_logic/lib/iprop.v theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v theories/base_logic/lib/saved_prop.v
......
...@@ -13,5 +13,5 @@ remove: ["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'"] ...@@ -13,5 +13,5 @@ remove: ["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'"]
depends: [ depends: [
"coq" { (>= "8.6.1" & < "8.8~") } "coq" { (>= "8.6.1" & < "8.8~") }
"coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev")) } "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev")) }
"coq-stdpp" { ((= "dev.2017-09-18.1") | (= "dev")) } "coq-stdpp" { ((= "dev.2017-09-18.4") | (= "dev")) }
] ]
...@@ -5,9 +5,9 @@ Import uPred. ...@@ -5,9 +5,9 @@ Import uPred.
(** Least and greatest fixpoint of a monotone function, defined entirely inside (** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *) the logic. *)
Class BIMonoPred {M A} (F : (A uPred M) (A uPred M)) :=
Definition uPred_mono_pred {M A} (F : (A uPred M) (A uPred M)) := bi_mono_pred Φ Ψ : (( x, Φ x - Ψ x) x, F Φ x - F Ψ x)%I.
Φ Ψ, (( x, Φ x Ψ x) x, F Φ x F Ψ x)%I. Arguments bi_mono_pred {_ _ _ _} _ _.
Definition uPred_least_fixpoint {M A} (F : (A uPred M) (A uPred M)) Definition uPred_least_fixpoint {M A} (F : (A uPred M) (A uPred M))
(x : A) : uPred M := (x : A) : uPred M :=
...@@ -18,13 +18,12 @@ Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M ...@@ -18,13 +18,12 @@ Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M
( Φ, ( x, Φ x F Φ x) Φ x)%I. ( Φ, ( x, Φ x F Φ x) Φ x)%I.
Section least. Section least.
Context {M : ucmraT}. Context {M A} (F : (A uPred M) (A uPred M)) `{!BIMonoPred F}.
Context {A} (F : (A uPred M) (A uPred M)) (Hmono : uPred_mono_pred F).
Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x uPred_least_fixpoint F x. Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x uPred_least_fixpoint F x.
Proof. Proof.
iIntros "HF" (Φ) "#Hincl". iIntros "HF" (Φ) "#Hincl".
iApply "Hincl". iApply (Hmono _ Φ); last done. iApply "Hincl". iApply (bi_mono_pred _ Φ); last done.
iIntros "!#" (y) "Hy". iApply "Hy". done. iIntros "!#" (y) "Hy". iApply "Hy". done.
Qed. Qed.
...@@ -32,7 +31,7 @@ Section least. ...@@ -32,7 +31,7 @@ Section least.
uPred_least_fixpoint F x F (uPred_least_fixpoint F) x. uPred_least_fixpoint F x F (uPred_least_fixpoint F) x.
Proof. Proof.
iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy". iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy".
iApply Hmono; last done. iIntros "!#" (z) "?". iApply bi_mono_pred; last done. iIntros "!#" (z) "?".
by iApply least_fixpoint_unfold_2. by iApply least_fixpoint_unfold_2.
Qed. Qed.
...@@ -48,13 +47,13 @@ Section least. ...@@ -48,13 +47,13 @@ Section least.
End least. End least.
Section greatest. Section greatest.
Context {M : ucmraT} {A} (F : (A uPred M) (A uPred M)) (Hmono : uPred_mono_pred F). Context {M A} (F : (A uPred M) (A uPred M)) `{!BIMonoPred F}.
Lemma greatest_fixpoint_unfold_1 x : Lemma greatest_fixpoint_unfold_1 x :
uPred_greatest_fixpoint F x F (uPred_greatest_fixpoint F) x. uPred_greatest_fixpoint F x F (uPred_greatest_fixpoint F) x.
Proof. Proof.
iDestruct 1 as (Φ) "[#Hincl HΦ]". iDestruct 1 as (Φ) "[#Hincl HΦ]".
iApply (Hmono Φ (uPred_greatest_fixpoint F)). iApply (bi_mono_pred Φ (uPred_greatest_fixpoint F)).
- iIntros "!#" (y) "Hy". iExists Φ. auto. - iIntros "!#" (y) "Hy". iExists Φ. auto.
- by iApply "Hincl". - by iApply "Hincl".
Qed. Qed.
...@@ -63,7 +62,7 @@ Section greatest. ...@@ -63,7 +62,7 @@ Section greatest.
F (uPred_greatest_fixpoint F) x uPred_greatest_fixpoint F x. F (uPred_greatest_fixpoint F) x uPred_greatest_fixpoint F x.
Proof. Proof.
iIntros "HF". iExists (F (uPred_greatest_fixpoint F)). iIntros "HF". iExists (F (uPred_greatest_fixpoint F)).
iIntros "{$HF} !#" (y) "Hy". iApply (Hmono with "[] Hy"). iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1. iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed. Qed.
......
...@@ -139,6 +139,84 @@ Proof. ...@@ -139,6 +139,84 @@ Proof.
refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver. refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
Defined. Defined.
Instance base_lit_countable : Countable base_lit.
Proof.
refine (inj_countable' (λ l, match l with
| LitInt n => inl (inl n) | LitBool b => inl (inr b)
| LitUnit => inr (inl ()) | LitLoc l => inr (inr l)
end) (λ l, match l with
| inl (inl n) => LitInt n | inl (inr b) => LitBool b
| inr (inl ()) => LitUnit | inr (inr l) => LitLoc l
end) _); by intros [].
Qed.
Instance un_op_finite : Countable un_op.
Proof.
refine (inj_countable' (λ op, match op with NegOp => 0 | MinusUnOp => 1 end)
(λ n, match n with 0 => NegOp | _ => MinusUnOp end) _); by intros [].
Qed.
Instance bin_op_countable : Countable bin_op.
Proof.
refine (inj_countable' (λ op, match op with
| PlusOp => 0 | MinusOp => 1 | LeOp => 2 | LtOp => 3 | EqOp => 4
end) (λ n, match n with
| 0 => PlusOp | 1 => MinusOp | 2 => LeOp | 3 => LtOp | _ => EqOp
end) _); by intros [].
Qed.
Instance binder_countable : Countable binder.
Proof.
refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
(λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
set (enc := fix go e :=
match e with
| Var x => GenLeaf (inl (inl x))
| Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
| App e1 e2 => GenNode 1 [go e1; go e2]
| Lit l => GenLeaf (inr (inl l))
| UnOp op e => GenNode 2 [GenLeaf (inr (inr (inl op))); go e]
| BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr (inr op))); go e1; go e2]
| If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
| Pair e1 e2 => GenNode 5 [go e1; go e2]
| Fst e => GenNode 6 [go e]
| Snd e => GenNode 7 [go e]
| InjL e => GenNode 8 [go e]
| InjR e => GenNode 9 [go e]
| Case e0 e1 e2 => GenNode 10 [go e0; go e1; go e2]
| Fork e => GenNode 11 [go e]
| Alloc e => GenNode 12 [go e]
| Load e => GenNode 13 [go e]
| Store e1 e2 => GenNode 14 [go e1; go e2]
| CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
end).
set (dec := fix go e :=
match e with
| GenLeaf (inl (inl x)) => Var x
| GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
| GenNode 1 [e1; e2] => App (go e1) (go e2)
| GenLeaf (inr (inl l)) => Lit l
| GenNode 2 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
| GenNode 3 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
| GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
| GenNode 5 [e1; e2] => Pair (go e1) (go e2)
| GenNode 6 [e] => Fst (go e)
| GenNode 7 [e] => Snd (go e)
| GenNode 8 [e] => InjL (go e)
| GenNode 9 [e] => InjR (go e)
| GenNode 10 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
| GenNode 11 [e] => Fork (go e)
| GenNode 12 [e] => Alloc (go e)
| GenNode 13 [e] => Load (go e)
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| _ => Lit LitUnit (* dummy *)
end).
refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
Qed.
Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit). Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit). Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
......
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