Commit 1aba9415 authored by Ralf Jung's avatar Ralf Jung

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

parents bbc9820d c031da7d
Pipeline #1592 passed with stage
......@@ -8,8 +8,8 @@ Local Arguments cmra_validN _ _ !_ /.
Local Arguments cmra_valid _ !_ /.
Inductive csum (A B : Type) :=
| Cinl : A -> csum A B
| Cinr : B -> csum A B
| Cinl : A csum A B
| Cinr : B csum A B
| CsumBot : csum A B.
Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _.
......@@ -22,13 +22,13 @@ Implicit Types b : B.
(* Cofe *)
Inductive csum_equiv : Equiv (csum A B) :=
| Cinl_equiv a a' : a a' -> Cinl a Cinl a'
| Cinlr_equiv b b' : b b' -> Cinr b Cinr b'
| Cinl_equiv a a' : a a' Cinl a Cinl a'
| Cinlr_equiv b b' : b b' Cinr b Cinr b'
| CsumBot_equiv : CsumBot CsumBot.
Existing Instance csum_equiv.
Inductive csum_dist : Dist (csum A B) :=
| Cinl_dist n a a' : a {n} a' -> Cinl a {n} Cinl a'
| Cinlr_dist n b b' : b {n} b' -> Cinr b {n} Cinr b'
| Cinl_dist n a a' : a {n} a' Cinl a {n} Cinl a'
| Cinlr_dist n b b' : b {n} b' Cinr b {n} Cinr b'
| CsumBot_dist n : CsumBot {n} CsumBot.
Existing Instance csum_dist.
......
......@@ -25,7 +25,7 @@ Proof.
+ apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
by rewrite -(exist_intro (hcons x xs)).
- apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
by rewrite -(exist_intro x).
by rewrite -(exist_intro x) IH.
Qed.
Lemma hforall_forall {As B} (f : himpl As B) (Φ : B uPred M) :
......@@ -33,7 +33,7 @@ Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
Proof.
apply (anti_symm _).
- apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
by rewrite (forall_elim x).
by rewrite (forall_elim x) IH.
- induction As as [|A As IH]; simpl.
+ by rewrite (forall_elim hnil) .
+ apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
......
......@@ -77,11 +77,11 @@ Proof.
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
wp_match. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; simplify_eq/=.
+ iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame; eauto. }
wp_case. wp_let. iPvsIntro. by iApply "Hv".
wp_match. by iApply "Hv".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed.
End proof.
......
......@@ -99,3 +99,17 @@ Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200) : val_scope.
Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
(** Notations for option *)
Notation NONE := (InjL #()).
Notation SOME x := (InjR x).
Notation NONEV := (InjLV #()).
Notation SOMEV x := (InjRV x).
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200) : expr_scope.
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 | 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
......@@ -148,7 +148,7 @@ Tactic Notation "wp_store" :=
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity
|wp_finish]
|wp_finish; try wp_seq]
| _ => fail "wp_store: not a 'wp'"
end.
......
......@@ -92,16 +92,16 @@ Tactic Notation "wp_if" :=
| _ => fail "wp_if: not a 'wp'"
end.
Tactic Notation "wp_case" :=
Tactic Notation "wp_match" :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Case _ _ _ =>
wp_bind K;
etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
wp_finish
end) || fail "wp_case: cannot find 'Case' in" e
| _ => fail "wp_case: not a 'wp'"
etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]];
simpl_subst; wp_finish
end) || fail "wp_match: cannot find 'Match' in" e
| _ => fail "wp_match: not a 'wp'"
end.
Tactic Notation "wp_focus" open_constr(efoc) :=
......
From iris.prelude Require Import base.
From iris.prelude Require Import tactics.
(* Not using [list Type] in order to avoid universe inconsistencies *)
Inductive tlist := tnil : tlist | tcons : Type tlist tlist.
......@@ -7,22 +7,53 @@ Inductive hlist : tlist → Type :=
| hnil : hlist tnil
| hcons {A As} : A hlist As hlist (tcons A As).
Fixpoint tapp (As Bs : tlist) : tlist :=
match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
match xs with hnil => ys | hcons _ _ x xs => hcons x (happ xs ys) end.
Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
match xs with hnil => () | hcons _ _ x _ => x end.
Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
match xs with hnil => () | hcons _ _ _ xs => xs end.
Fixpoint hheads {As Bs} : hlist (tapp As Bs) hlist As :=
match As with
| tnil => λ _, hnil
| tcons A As => λ xs, hcons (hhead xs) (hheads (htail xs))
end.
Fixpoint htails {As Bs} : hlist (tapp As Bs) hlist Bs :=
match As with
| tnil => id
| tcons A As => λ xs, htails (htail xs)
end.
Fixpoint himpl (As : tlist) (B : Type) : Type :=
match As with tnil => B | tcons A As => A himpl As B end.
Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
Definition hinit {B} (y : B) : himpl tnil B := y.
Definition hlam {A As B} (f : A himpl As B) : himpl (tcons A As) B := f.
Arguments hlam _ _ _ _ _/.
Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go As xs :=
match xs in hlist As return himpl As B B with
| hnil => λ f, f
| hcons A As x xs => λ f, go As xs (f x)
end) _ xs f.
Coercion happly : himpl >-> Funclass.
Coercion hcurry : himpl >-> Funclass.
Fixpoint huncurry {As B} : (hlist As B) himpl As B :=
match As with
| tnil => λ f, f hnil
| tcons x xs => λ f, hlam (λ x, huncurry (f hcons x))
end.
Lemma hcurry_uncurry {As B} (f : hlist As B) xs : huncurry f xs = f xs.
Proof. by induction xs as [|A As x xs IH]; simpl; rewrite ?IH. Qed.
Fixpoint hcompose {As B C} (f : B C) {struct As} : himpl As B himpl As C :=
match As with
| tnil => f
| tcons A As => λ g x, hcompose f (g x)
| tcons A As => λ g, hlam (λ x, hcompose f (g x))
end.
Definition hinit {B} (y : B) : himpl tnil B := y.
Definition hlam {A As B} (f : A himpl As B) : himpl (tcons A As) B := f.
......@@ -11,7 +11,6 @@ Declare Reduction env_cbv := cbv [
bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
string_eq_dec string_rec string_rect (* strings *)
himpl happly
env_persistent env_spatial envs_persistent
envs_lookup envs_lookup_delete envs_delete envs_app
envs_simple_replace envs_replace envs_split envs_clear_spatial].
......@@ -35,6 +34,11 @@ Tactic Notation "iTypeOf" constr(H) tactic(tac):=
| Some (?p,?P) => tac p P
end.
Ltac iMatchGoal tac :=
match goal with
| |- context[ environments.Esnoc _ ?x ?P ] => tac x P
end.
(** * Start a proof *)
Tactic Notation "iProof" :=
lazymatch goal with
......@@ -135,7 +139,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
[env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
|apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type"
|env_cbv; reflexivity|]
|cbn [himpl hcurry]; reflexivity|]
end.
Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
......@@ -790,6 +794,10 @@ Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
iRewriteCore true t in H.
Ltac iSimplifyEq := repeat (
iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end)
|| simplify_eq/=).
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ _) => by iPureIntro.
Hint Extern 0 (of_envs _ _) => iAssumption.
......
......@@ -45,7 +45,7 @@ Section client.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done.
iFrame "Hh". iSplitL "Hy Hs".
- (* The original thread, the sender. *)
wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
- (* The two spawned threads, the waiters. *)
iSplitL; [|by iIntros {_ _} "_ >"].
......
......@@ -27,7 +27,7 @@ Section LiftingTests.
nclose N E heap_ctx N WP heap_e @ E {{ v, v = #2 }}.
Proof.
iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
Qed.
Definition heap_e2 : expr [] :=
......@@ -39,7 +39,7 @@ Section LiftingTests.
Proof.
iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
wp_alloc l. wp_let. wp_alloc l'. wp_let.
wp_load. wp_op. wp_store. wp_seq. wp_load. done.
wp_load. wp_op. wp_store. wp_load. done.
Qed.
Definition FindPred : val :=
......
......@@ -71,15 +71,15 @@ Proof.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
wp_let. iPvsIntro. iIntros "!". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
{ wp_case. wp_seq. by iPvsIntro. }
wp_case. wp_let. wp_focus (! _)%E.
{ wp_match. by iPvsIntro. }
wp_match. wp_focus (! _)%E.
iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
wp_load.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
iSplitL "Hl"; [iRight; by eauto|].
wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
Qed.
Lemma hoare_one_shot (Φ : val iProp) :
......
......@@ -40,13 +40,13 @@ Lemma sum_loop_wp `{!heapG Σ} heapN v t l (n : Z) (Φ : val → iPropG heap_lan
WP sum_loop v #l {{ Φ }}.
Proof.
iIntros "(#Hh & Hl & Ht & HΦ)".
iLöb {v t l n Φ} as "IH". wp_rec. wp_let.
iLöb {v t l n Φ} as "IH". wp_rec; wp_let.
destruct t as [n'|tl tr]; simpl in *.
- iDestruct "Ht" as "%"; subst.
wp_case. wp_let. wp_load. wp_op. wp_store.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "Hl").
- iDestruct "Ht" as {ll lr vl vr} "(% & Hll & Htl & Hlr & Htr)"; subst.
wp_case. wp_let. wp_proj. wp_load.
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "Hl Htl".
wp_seq. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htr"). iIntros "Hl Htr".
......
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