Commit 3a032235 authored by Michael Sammler's avatar Michael Sammler
Browse files

cleanup base.v

parent abf1090a
Pipeline #50497 passed with stage
in 17 minutes and 40 seconds
This diff is collapsed.
......@@ -227,14 +227,14 @@ Proof.
iDestruct "Hl" as "[Hx Hl]". case_bool_decide => //.
iDestruct ("Hsub" with "[Hl]") as "[% [Hl HT]]". {
iApply (big_sepL_impl with "Hl"). iIntros "!>" (???) "?".
repeat case_bool_decide => //; set_solver.
repeat case_decide => //; set_solver.
}
iSplit => //.
have [//|y ?]:= lookup_lt_is_Some_2 l2 i. { lia. }
iDestruct ("HT" with "[//] Hx") as "[Hf $]".
rewrite -{2}(list_insert_id l2 i y) // big_sepL_insert; [|lia]. case_bool_decide => //. iFrame.
iApply (big_sepL_impl with "Hl"). iIntros "!>" (???) "?".
repeat case_bool_decide => //; set_solver.
repeat case_decide => //; set_solver.
Qed.
Global Instance subsume_list_insert_not_in_ig_inst {Σ} A ig i x (l1 l2 : list A) (f : nat A iProp Σ) `{!CanSolve (i ig)} :
SubsumeList A ig (<[i := x]>l1) l2 f :=
......
......@@ -278,7 +278,7 @@ Global Instance simpl_insert_subequiv {A} (l1 l2 : list A) j x1 ig `{!CanSolve (
list_subequiv (j :: ig) l1 l2 l2 !! j = Some x1).
Proof.
unfold CanSolve in *. unfold SimplBothRel.
case_bool_decide; [rewrite subequiv_insert_in_l | rewrite subequiv_insert_ne_l ]; naive_solver.
case_bool_decide; [rewrite list_subequiv_insert_in_l | rewrite list_subequiv_insert_ne_l ]; naive_solver.
Qed.
Global Instance simpl_ig_nil_subequiv {A} (l1 l2 : list A) :
......@@ -290,32 +290,11 @@ Qed.
Global Instance simpl_nil_subequiv {A} (l : list A) ig :
SimplBothRel (list_subequiv ig) [] l (l = []).
Proof. by split; rewrite subequiv_nil_l. Qed.
Lemma lookup_eq_app_r {A} (l1 l2 suffix : list A) (i : nat) :
length l1 = length l2
l1 !! i = l2 !! i (l1 ++ suffix) !! i = (l2 ++ suffix) !! i.
Proof.
move => Hlen. destruct (l1 !! i) as [v|] eqn:HEq.
+ rewrite lookup_app_l; last by eapply lookup_lt_Some.
rewrite lookup_app_l; first by rewrite -HEq.
apply lookup_lt_Some in HEq. by rewrite -Hlen.
+ rewrite lookup_app_r; last by apply lookup_ge_None.
apply lookup_ge_None in HEq. rewrite Hlen in HEq.
apply lookup_ge_None in HEq. rewrite HEq.
split => [_|]//. rewrite lookup_app_r; first by rewrite Hlen.
by apply lookup_ge_None.
Qed.
Proof. by split; rewrite list_subequiv_nil_l. Qed.
Global Instance simpl_app_r_subequiv {A} (l1 l2 suffix : list A) ig :
SimplBothRel (list_subequiv ig) (l1 ++ suffix) (l2 ++ suffix) (list_subequiv ig l1 l2).
Proof.
rewrite /list_subequiv. split => H i; move: (H i) => [Hlen Hlookup].
- rewrite app_length app_length in Hlen. split; first by lia.
move => /Hlookup. apply lookup_eq_app_r. by lia.
- split; first by rewrite app_length app_length Hlen.
move => /Hlookup. apply lookup_eq_app_r. by lia.
Qed.
Proof. apply: list_subequiv_app_r. Qed.
(* The other direction requires `{!Inj (=) (=) f}, but we cannot prove
it if f goes into type. Thus we use the AssumeInj typeclass such that
......@@ -323,11 +302,7 @@ the user can mark functions which are morally injective, but one
cannot prove it. *)
Global Instance simpl_fmap_fmap_subequiv_Unsafe {A B} (l1 l2 : list A) ig (f : A B) `{!AssumeInj (=) (=) f}:
SimplAndUnsafe true (list_subequiv ig (f <$> l1) (f <$> l2)) (λ T, list_subequiv ig l1 l2 T).
Proof.
move => ? [Hs ?]. split => // i. move: (Hs 0%nat) => [Hlen _].
do 2 rewrite fmap_length. split => // ?. rewrite !list_lookup_fmap.
f_equal. move: (Hs i) => [_ ?]. naive_solver.
Qed.
Proof. move => ? [Hs ?]. split => //. by apply: list_subequiv_fmap. Qed.
(* The other direction might not hold if ig contains indices which are
out of bounds, but we don't care about that. *)
......@@ -335,11 +310,14 @@ Global Instance simpl_subequiv_protected {A} (l1 l2 : list A) ig `{!IsProtected
SimplAndUnsafe true (list_subequiv ig l1 l2) (λ T,
foldr (λ i f, (λ l', x, f (<[i:=x]> l'))) (λ l', l2 = l' T) ig l1).
Proof.
(* TODO: add a lemma for list_subequiv such that this unfolding is not necessary anymore. *)
Local Transparent list_subequiv.
unfold list_subequiv, IsProtected in * => T. elim: ig l1 l2.
- move => ??/=. move => [??]. naive_solver.
- move => i ig IH l1 l2/= [x /IH [Hi ?]]. split => // i'.
move: (Hi i') => [<- Hlookup]. rewrite insert_length. split => //.
move => Hi'. rewrite -Hlookup ?list_lookup_insert_ne; set_solver.
Local Opaque list_subequiv.
Qed.
Global Instance simpl_fmap_nil {A B} (l : list A) (f : A B) : SimplBothRel (=) (f <$> l) [] (l = []).
......
......@@ -75,7 +75,7 @@ Proof.
iModIntro. iExists NotStuck, _, (replicate (length thread_mains) (λ _, True%I)), _, _.
iSplitL "Hctx Hf"; last first. 1: iSplitL "Hmains".
- rewrite big_sepL2_fmap_l. iApply big_sepL2_replicate_2. iApply (big_sepL_impl with "Hmains").
- rewrite big_sepL2_fmap_l. iApply big_sepL2_replicate_r; [done|]. iApply (big_sepL_impl with "Hmains").
iIntros "!#" (? main ?); iDestruct 1 as (P) "[Hmain HP]".
iApply (type_call with "[-]"). 2: { by iIntros (??) "??". }
iApply type_val. iApply type_val_context.
......
......@@ -215,24 +215,19 @@ Section programs.
Proof.
move => Hnonneg Hsign Htestbit.
rewrite /elem_of /int_elem_of_it /min_int /max_int.
have ? := bits_per_int_gt_0 it.
destruct (it_signed it).
- rewrite /int_half_modulus.
move ? : (bits_per_int it - 1) => k.
have ? : 0 k.
{ suff : bits_per_int it > 0 by lia. by apply: bits_per_int_gt_0. }
have Hb : n, -2^k n 2^k - 1
l, k l Z.testbit n l = bool_decide (n < 0)
by intros; rewrite -bounded_iff_bits; lia.
have Hb : n, -2^k n 2^k - 1 l, k l Z.testbit n l = bool_decide (n < 0).
{ move => ?. rewrite -Z_bounded_iff_bits; lia. }
move => /Hb Hn1 /Hb Hn2.
apply Hb => l Hl.
by rewrite Htestbit Hsign Hn1 ?Hn2.
- rewrite /int_modulus.
move ? : (bits_per_int it) => k.
have ? : 0 k.
{ suff : bits_per_int it > 0 by lia. by apply: bits_per_int_gt_0. }
have Hb : n, 0 n n 2^k - 1
l, k l Z.testbit n l = bool_decide (n < 0)
by intros; rewrite bool_decide_false -?pos_bounded_iff_bits; lia.
have Hb : n, 0 n n 2^k - 1 l, k l Z.testbit n l = bool_decide (n < 0).
{ move => ??. rewrite bool_decide_false -?Z_bounded_iff_bits_nonneg; lia. }
move => [Hn1 /Hb HN1] [Hn2 /Hb HN2].
have Hn := Hnonneg Hn1 Hn2.
split; first done.
......
Supports Markdown
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