Commit 855c3724 authored by Dan Frumin's avatar Dan Frumin

Move the lemmas from ds.v out to std++

parent 7032dc7d
-Q theories iris_logrel
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/prelude/ds.v
theories/prelude/base.v
theories/prelude/hax.v
theories/F_mu_ref_conc/binder.v
......
......@@ -7,7 +7,7 @@ Inductive binder := BAnon | BNamed : string → binder.
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
Definition cons_binder (mx : binder) (X : gset string) : gset string :=
Definition cons_binder (mx : binder) (X : stringset) : stringset :=
match mx with BAnon => X | BNamed x => {[x]} X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_eq_dec_eq : EqDecision binder.
......@@ -45,7 +45,7 @@ Instance singleton_binder_set : Singleton binder stringset :=
(** Properties lifts *)
Lemma dom_delete_binder {A} (i : binder) (m : stringmap A) :
dom (gset string) (delete i m) (dom (gset string) m) {[i]}.
dom stringset (delete i m) (dom stringset m) {[i]}.
Proof.
destruct i; cbn-[difference]; eauto.
- set_solver.
......@@ -63,7 +63,7 @@ Lemma dom_insert_binder {A} (m : stringmap A) (i : binder) (x : A) :
dom _ (<[i:=x]> m) = {[i]} dom _ m.
Proof. destruct i; cbn-[union]; unfold_leibniz. set_solver.
apply dom_insert. Qed.
Lemma cons_binder_union (i : binder) (X : gset string) :
Lemma cons_binder_union (i : binder) (X : stringset) :
i :b: X = {[i]} X.
Proof. destruct i; cbn-[union]; eauto. set_solver. Qed.
......
......@@ -66,7 +66,7 @@ Module lang.
Proof. solve_decision. Defined.
(** ** Closed expressions *)
Fixpoint is_closed (X : gset string) (e : expr) : bool :=
Fixpoint is_closed (X : stringset) (e : expr) : bool :=
match e with
| Var x => bool_decide (x X)
| Rec f x e => is_closed (x :b: f :b: X) e
......@@ -83,7 +83,7 @@ Module lang.
| Unpack e e1 => is_closed X e && is_closed X e1
end.
Class Closed (X : gset string) (e : expr) := closed : is_closed X e.
Class Closed (X : stringset) (e : expr) := closed : is_closed X e.
Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
......
......@@ -119,7 +119,7 @@ Ltac of_expr e :=
end
end.
Fixpoint is_closed (X : gset string) (e : expr) : bool :=
Fixpoint is_closed (X : stringset) (e : expr) : bool :=
match e with
| Val _ _ _ => true
| ClosedExpr e _ => true
......
......@@ -111,7 +111,7 @@ Proof.
Qed.
(** ** Properties of [Closed] and [is_closed] *)
Lemma is_closed_weaken (e : expr) : (X Y : gset string),
Lemma is_closed_weaken (e : expr) : (X Y : stringset),
is_closed X e X Y is_closed Y e.
Proof.
induction e; intros X Y HXY HXe; simpl; simpl in HXe, HXY; eauto;
......@@ -166,7 +166,7 @@ Proof.
| [ |- Is_true (?P && ?Q) ] => apply andb_prop_intro; split; eauto
end;
try match goal with
| [ H : X : gset string,
| [ H : X : stringset,
Closed X ?e Closed X es Closed X (subst x es ?e)
|- Is_true (is_closed _ (subst x es ?e)) ] =>
eapply H; eauto; try (eapply Closed_mono; eauto; set_solver)
......
......@@ -166,7 +166,7 @@ Proof.
Qed.
Lemma typed_X_closed Γ τ e :
Γ ⊢ₜ e : τ Closed (dom (gset string) Γ) e.
Γ ⊢ₜ e : τ Closed (dom (stringset) Γ) e.
Proof.
intros H. rewrite /Closed. induction H => /=; simpl in *; auto with f_equal.
- case_bool_decide; auto.
......
......@@ -140,16 +140,16 @@ Section masked.
destruct x as [|x], f as [|f]; cbn-[union difference].
+ set_solver.
+ rewrite difference_empty.
rewrite assoc. rewrite difference_union_id.
rewrite assoc. rewrite difference_union.
set_solver.
+ rewrite difference_empty.
rewrite assoc. rewrite difference_union_id.
rewrite assoc. rewrite difference_union.
set_solver.
+ rewrite ?(right_id union).
rewrite (comm union {[x]} {[f]}) !assoc.
rewrite difference_union_id.
rewrite difference_union.
rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
rewrite difference_union_id.
rewrite difference_union.
set_solver. }
assert (Closed (x :b: f :b: )
(subst_p (delete f (delete x (snd <$> vvs))) e')).
......@@ -159,16 +159,16 @@ Section masked.
destruct x as [|x], f as [|f]; cbn-[union difference].
+ set_solver.
+ rewrite difference_empty.
rewrite assoc. rewrite difference_union_id.
rewrite assoc. rewrite difference_union.
set_solver.
+ rewrite difference_empty.
rewrite assoc. rewrite difference_union_id.
rewrite assoc. rewrite difference_union.
set_solver.
+ rewrite ?(right_id union).
rewrite (comm union {[x]} {[f]}) !assoc.
rewrite difference_union_id.
rewrite difference_union.
rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
rewrite difference_union_id.
rewrite difference_union.
set_solver.
}
iModIntro. value_case'; eauto.
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Export base.
From iris.base_logic Require Import upred.
From iris.program_logic Require Import weakestpre.
From iris.base_logic Require Import invariants.
From iris_logrel.prelude Require Export ds.
From stdpp Require Export strings stringmap gmap mapset fin_maps.
From Autosubst Require Export Autosubst.
Import uPred.
......
(* Data structures properties *)
(* TODO: move this to std++ *)
From stdpp Require Export strings gmap mapset stringmap.
From iris.algebra Require Export base. (* for ssreflect stuff *)
Lemma delete_insert_delete {A} (m : stringmap A) (i : string) (x : A) :
delete i (<[i:=x]> m) = delete i m.
Proof.
apply map_eq=>j.
destruct (decide (i = j)) as [Eij|Nij];
simplify_map_eq; auto.
Qed.
Lemma delete_idem {A} (x : string) (m : stringmap A) :
delete x (delete x m) = delete x m.
Proof.
rewrite delete_notin; first done.
apply lookup_delete.
Qed.
Lemma delete_singleton_ne {A} (i j : string) (x : A) :
j i
delete i {[j := x]} = {[j := x]}.
Proof. intros Hij. apply delete_notin. by apply lookup_singleton_ne. Qed.
Lemma difference_empty_map {K A} `{EqDecision K} `{Countable K} (X : gmap K A) :
X = X.
Proof.
apply map_eq => i.
remember (X !! i) as Z. destruct Z.
- apply lookup_difference_Some. split; eauto.
- apply lookup_difference_None. left; eauto.
Qed.
Lemma singleton_union_difference (X Y : stringset) (x : string) :
{[x]} (X Y) = ({[x]} X) (Y {[x]}).
Proof.
unfold_leibniz. intros y. split; intro Hy.
- apply elem_of_union in Hy. set_solver.
- apply elem_of_difference in Hy. destruct Hy as [Hy1 Hy2].
apply elem_of_union in Hy1.
rewrite elem_of_union. rewrite elem_of_difference.
rewrite elem_of_singleton.
destruct (decide (x = y)); subst; eauto.
assert (y {[x]}). intro K; apply elem_of_singleton in K. auto.
right. destruct Hy1; set_solver.
Qed.
Lemma difference_union_id {A : Type} `{EqDecision A, Countable A} (X Y : gset A):
X Y Y = X Y.
Proof.
unfold_leibniz. intro x.
rewrite !elem_of_union elem_of_difference.
split.
- set_solver.
- destruct (decide (x Y)); set_solver.
Qed.
Lemma difference_empty {A: Type} `{EqDecision A, Countable A} (X : gset A) :
X = X.
Proof.
unfold_leibniz.
rewrite <- (right_id union (X )).
rewrite <- (right_id union X) at 2.
fold_leibniz.
apply difference_union_id.
Qed.
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