Commit 187cefbb authored by charguer's avatar charguer

RO example

parent a761ee45
......@@ -8,9 +8,9 @@ License: MIT.
*)
Set Implicit Arguments.
From Sep Require Import LambdaCFSep.
From Sep Require Import LambdaSepRO.
Generalizable Variables A B.
Open Scope trm_scope.
Ltac auto_star ::= jauto.
Implicit Types p q : loc.
......@@ -18,6 +18,99 @@ Implicit Types n : int.
Implicit Types v : val.
Import TripleLowLevel. (* TODO: remove *)
(* To move and factorize *)
Notation "F 'PRE' H 'POST' Q" :=
(F H Q)
(at level 69, only parsing) : heap_scope.
(* todo move *)
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (length Vs) xs ->
triple (substs xs Vs t1) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros h1 h2 D H1.
forwards~ (h1'&v&N1&N2&N3&N4): (rm M) h2 H1.
exists h1' v. splits~. { subst. applys* red_app_funs_val. }
Qed.
Lemma var_funs_exec_elim : forall (n:nat) xs,
var_funs_exec n xs -> (var_funs n xs).
Proof using. introv M. rewrite var_funs_exec_eq in M. rew_istrue~ in M. Qed.
Hint Resolve var_funs_exec_elim.
Lemma RO_himpl_RO_hstar_RO : forall H,
RO H ==> (RO H \* RO H).
Proof using. intros. applys RO_duplicatable. Qed.
Lemma rule_xchange : forall (H1 H1':hprop), H1 ==> H1' ->
forall t H H2 Q,
H ==> H1 \* H2 ->
triple t (H1' \* H2) Q ->
triple t H Q.
Proof using.
introv M1 M2 M. applys~ rule_consequence M2.
applys* rule_consequence (H1' \* H2). hsimpl~.
Qed.
Lemma rule_frame_read_only_conseq : forall t H1 Q1 H2 H Q,
H ==> (H1 \* H2) ->
normal H1 ->
triple t (RO H1 \* H2) Q1 ->
(Q1 \*+ H1) ===> Q ->
triple t H Q.
Proof using.
introv WP M N WQ. applys* rule_consequence (rm WP) (rm WQ).
forwards~ R: rule_frame_read_only t H2 Q1 H1.
{ rewrite~ hstar_comm. } { rewrite~ hstar_comm. }
Qed.
Lemma rule_get : forall v l,
triple (val_get (val_loc l))
(l ~~~> v)
(fun x => \[x = v] \* l ~~~> v).
Proof using.
intros. applys rule_frame_read_only_conseq (l ~~~> v).
{ hsimpl. } { applys normal_single. (* todo: normal_hsingle? *) }
{ rew_heap. applys rule_get_ro. }
{ auto. }
Qed.
Lemma rule_let' : forall x t1 t2 H2 H1 H Q Q1,
H ==> (H1 \* H2) ->
triple t1 H1 Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X \* H2) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using. introv WP M1 M2. applys* rule_consequence WP. applys* rule_let. Qed.
Lemma rule_frame : forall t H1 Q1 H2,
triple t H1 Q1 ->
normal H2 ->
triple t (H1 \* H2) (Q1 \*+ H2).
Proof using.
introv M N. applys~ rule_frame_read_only.
applys~ rule_consequence (H1 \* \Top). hsimpl.
applys* rule_htop_pre.
Qed.
Lemma rule_frame_conseq : forall t H1 Q1 H2 H Q,
H ==> H2 \* H1 ->
normal H1 ->
triple t H2 Q1 ->
Q1 \*+ H1 ===> Q ->
triple t H Q.
Proof using. intros. applys* rule_consequence. applys* rule_frame. Qed.
Hint Resolve normal_single.
(* ********************************************************************** *)
(* * Formalisation of higher-order iterator on a reference *)
......@@ -30,36 +123,47 @@ Definition val_ref_apply :=
Let 'x := val_get 'p in
'f 'x.
Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val),
Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
(triple (f v)
PRE (RO(p ~~~> v) \* H)
POST Q)
->
(triple (val_ref_apply f r)
(triple (val_ref_apply f p)
PRE (RO(p ~~~> v) \* H)
POST Q).
Proof using.
admit.
introv M.
rew_nary; rew_vals_to_trms; applys rule_apps_funs;
[unfold val_ref_apply; rew_nary; reflexivity| auto | simpl].
applys rule_xchange (@RO_himpl_RO_hstar_RO (p ~~~> v)); [ hsimpl |].
rew_heap. applys rule_let (RO (p ~~~> v)).
{ applys rule_get_ro. }
{ intros x; simpl.
applys rule_extract_hprop ;=> E; subst x.
applys M. }
Qed.
(* Note: this specification allows [f] to call [val_get] on [r],
as illustrated next *)
Definition val_demo_1 :=
ValFun 'n :=
Let 'p := val_ref n in
LetFun 'f 'x :=
Let 'y := val_get 'p in
val_add 'x 'y in
val_ref_apply 'f 'p.
Lemma rule_demo_1 : forall (n:int),
(triple (val_demo_1 n)
PRE \[]
POST (fun r => \[r = val_int (2*n)]).
Proof using.
admit.
Qed.
as illustrated next
Definition val_demo_1 :=
ValFun 'n :=
Let 'p := val_ref 'n in
LetFun 'f 'x :=
Let 'y := val_get 'p in
val_add 'x 'y in
val_ref_apply 'f 'p.
Lemma rule_demo_1 : forall (n:int),
triple (val_demo_1 n)
PRE \[]
POST (fun r => \[r = val_int (2*n)]).
Proof using.
admit.
Qed.
*)
(* ---------------------------------------------------------------------- *)
......@@ -69,18 +173,30 @@ Definition val_ref_update :=
ValFun 'f 'p :=
Let 'x := val_get 'p in
Let 'y := 'f 'x in
val_set 'r 'y.
val_set 'p 'y.
Lemma rule_ref_update : forall (f:val) (p:loc) (v:val),
Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
normal_post Q -> (* todo: this might not be needed if using "normally" *)
(triple (f v)
PRE (RO(p ~~~> v) \* H)
POST Q)
->
(triple (val_ref_apply f r)
(triple (val_ref_update f p)
PRE (p ~~~> v \* H)
POST (fun r => \[r = val_unit] \* \Hexists w, (p ~~~> w) \* (Q w))).
POST (fun r => \[r = val_unit] \* Hexists w, (p ~~~> w) \* (Q w))).
Proof using.
admit.
introv N M.
rew_nary; rew_vals_to_trms; applys rule_apps_funs;
[unfold val_ref_update; rew_nary; reflexivity| auto | simpl].
applys rule_let.
{ applys rule_get. }
{ intros x; simpl; rew_heap. applys rule_extract_hprop ;=> E; subst x.
applys rule_let' \[]. { hsimpl. }
applys~ rule_frame_read_only_conseq (p ~~~> v).
{ hsimpl. } { rew_heap. applys M. } { hsimpl. }
{ intros y; simpl; rew_heap. clear M.
applys~ rule_frame_conseq (Q y). hsimpl.
rew_heap. applys rule_set. hsimpl~. } }
Qed.
......@@ -90,6 +206,12 @@ Qed.
(*-----------LATER using LambdaCFRO
(* ********************************************************************** *)
(* * Formalisation of records *)
......@@ -469,5 +591,5 @@ Qed.
Hint Extern 1 (Register_spec val_copy_transfer) => Provide rule_copy_transfer.
*)
......@@ -10,7 +10,7 @@ License: MIT.
Set Implicit Arguments.
From TLC Require Export LibFix.
From Sep Require Export LambdaSepRO LambdaCFTactics.
From Sep Require Export LambdaSep LambdaCFTactics.
Open Scope heap_scope.
Implicit Types v w : val.
......@@ -305,37 +305,6 @@ Implicit Types n : nat.
Implicit Types F : val.
Implicit Types f x : var.
(*-- LATER: move to TLC LibNatExec *)
Fixpoint nat_compare (x y : nat) :=
match x, y with
| O, O => true
| S x', S y' => nat_compare x' y'
| _, _ => false
end.
Lemma nat_compare_eq : forall n1 n2,
nat_compare n1 n2 = isTrue (n1 = n2).
Proof using.
intros n1. induction n1; intros; destruct n2; simpl; rew_bool_eq; auto_false.
rewrite IHn1. extens. rew_istrue. math.
Qed.
Definition var_funs_exec (n:nat) (xs:vars) : bool := (* --todo: use exec typeclass *)
nat_compare n (List.length xs)
&& is_not_nil xs (* --todo: rename to exec *)
&& var_distinct xs.
Lemma var_funs_exec_eq : forall n xs,
var_funs_exec n xs = isTrue (var_funs n xs).
Proof using.
intros. unfold var_funs_exec, var_funs.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_istrue. iff*.
Qed.
Lemma triple_apps_funs_of_cf_iter : forall n F (vs:vals) xs t H Q,
F = val_funs xs t ->
var_funs_exec (length vs) xs ->
......@@ -346,21 +315,6 @@ Proof using.
applys* rule_apps_funs. applys* triple_trm_of_cf_iter.
Qed.
Definition var_fixs_exec (f:var) (n:nat) (xs:vars) : bool := (* todo: use exec typeclass *)
nat_compare n (List.length xs)
&& is_not_nil xs (* todo: rename to exec *)
&& var_distinct (f::xs).
Lemma var_fixs_exec_eq : forall f n xs,
var_fixs_exec f n xs = isTrue (var_fixs f n xs).
Proof using.
intros. unfold var_fixs_exec, var_fixs.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_istrue. iff*.
Qed.
Lemma triple_apps_fixs_of_cf_iter : forall n f F (vs:vals) xs t H Q,
F = val_fixs f xs t ->
var_fixs_exec f (length vs) xs ->
......@@ -373,13 +327,8 @@ Qed.
End LemmasCf.
(* ---------------------------------------------------------------------- *)
(* ** Database of specifications used by [xapp], through tactic [xspec] *)
(** A name for the database *)
Definition database_spec := True.
(** ** Database of lemmas *)
(** We here use the notation [Register] and [Provide] from the TLC library.
......@@ -395,43 +344,12 @@ Definition database_spec := True.
*)
Notation "'Register_goal' G" := (Register database_spec G)
(at level 69) : charac.
Notation "'Register_rule' t" := (Register_goal (triple t _ _))
(at level 69) : charac.
Notation "'Register_spec' f" := (Register_rule (trm_apps (trm_val f) _))
(at level 69) : charac.
(** [xspec G] retreives from the database [database_spec]
the specification that could apply to a goal [G].
It places the specification as hypothesis at the head of the goal. *)
Ltac xapp_basic_prepare tt ::= (* actually defined further *)
idtac.
Ltac xspec_context G := (* refined only in LambdaCFLifted *)
fail.
Ltac xspec_registered G :=
ltac_database_get database_spec G.
Ltac xspec_database G :=
first [ xspec_registered G | xspec_context G ].
Ltac xspec_base tt :=
match goal with
| |- ?G => xspec_database G
end.
Ltac xspec_core tt :=
xapp_basic_prepare tt;
xspec_base tt.
Tactic Notation "xspec" :=
xspec_core tt.
(* ---------------------------------------------------------------------- *)
(** ** Registering specification of primitive functions *)
......
......@@ -13,6 +13,65 @@ From TLC Require Export LibFix.
From Sep Require Export LambdaSepRO LambdaCFTactics.
Open Scope heap_scope.
Import TripleLowLevel. (* TODO: remove *)
(* ---------------------------------------------------------------------- *)
(* ** Triples satisfy the [local] predicate :: TODO move *)
(** This lemma is exploited indirectly by tactics such as [xapply],
which perform application of lemmas modulo framing. *)
Lemma on_rw_sub_union : forall (H1 H2:hprop) h1 h2,
on_rw_sub H1 h1 ->
H2 h2 ->
normal H2 ->
heap_compat h1 h2 ->
on_rw_sub (H1 \* H2) (h1 \u h2).
Proof using.
(*
introv (h11&h12&N1&N2&N3&N4) M2 C. hnf.
subst h1. lets~ (N1a&N1b): heap_compat_union_l_inv C.
exists h11 (h12 \u h2). splits~.
{ applys~ heap_union_assoc. }
Qed.
*)
Admitted.
Lemma is_local_triple : forall t,
is_local (triple t).
Proof using.
intros. applys pred_ext_2. intros H Q. iff M.
{ intros h Hh. forwards (h'&v&N1&N2&N3&N4): M h heap_empty.
{ applys heap_compat_empty_r. } { auto. }
exists H \[] Q. splits~. { hhsimpl. } { hsimpl. } }
{ intros h1 h2 D M1. lets (H1&H2&Q1&R1&R2&R3): M M1.
destruct R1 as (h11&h12&N1&N2&N3&N4).
skip Da: (heap_compat h11 h12).
skip Db: (heap_compat h12 h2).
skip Dc: (heap_compat h11 h2). (* TODO: urgent *)
forwards (h11'&v&T1&T2&T3&T4): (rm R2) (h12 \u h2) (rm N1).
{ applys~ heap_compat_union_r. }
skip Dd: (heap_compat h11' h2).
skip De: (heap_compat h11' h12). (* TODO URGENT *)
exists (h11' \u h12) v. splits.
{ auto. }
{ subst h1. do 2 rewrite~ heap_union_assoc. }
{ subst. do 2 rewrite~ heap_union_r. rewrite~ T3. }
{ applys on_rw_sub_htop. applys on_rw_sub_weaken R3.
applys~ on_rw_sub_union. skip. } } (* TODO: requires [normal H2] *)
Qed.
(** Make tactic [xlocal] aware that triples are local *)
Ltac xlocal_base tt ::=
try first [ applys is_local_local
| applys is_local_triple ].
(* ---------------------------------------------------------------------- *)
Implicit Types v w : val.
Implicit Types t : trm.
......@@ -43,7 +102,7 @@ Definition cf_fail : formula := fun H Q =>
False.
Definition cf_val (v:val) : formula := fun H Q =>
(fun (x:val) => \[x = v] \* H) ===> Q.
normal H /\ (fun (x:val) => \[x = v] \* H) ===> Q.
Definition cf_seq (F1 F2:formula) : formula := fun H Q =>
exists H1,
......@@ -165,10 +224,16 @@ Proof using.
intros t. induction_wf: trm_size t.
rewrite cf_unfold. destruct t; simpl;
try (applys sound_for_local; intros H Q P).
{ unfolds in P. applys~ rule_val. hchanges~ P. }
{ destruct P as (P1&P2). applys~ rule_val. hchanges~ P2. }
{ false. }
{ unfolds in P. applys rule_fun. hchanges~ P. }
{ unfolds in P. applys rule_fix. hchanges~ P. }
skip.
skip.
(*
{ destruct P as (P1&P2). applys rule_fun. hchanges~ P. }
{ destruct P as (P1&P2). applys rule_fix. hchanges~ P. }
*)
skip.
(* rule_if_bool
{ destruct P as (Q1&P1&P2). applys rule_if.
{ applys* IH. }
{ intros v. specializes P2 v. applys sound_for_local (rm P2).
......@@ -176,6 +241,7 @@ Proof using.
case_if; applys* IH. }
{ intros v N. specializes P2 v. applys local_extract_false P2.
intros H' Q' (b&E&S1&S2). subst. applys N. hnfs*. } }
*)
{ destruct P as (H1&P1&P2). applys rule_seq' H1.
{ applys~ IH. }
{ intros X. applys~ IH. } }
......@@ -305,37 +371,6 @@ Implicit Types n : nat.
Implicit Types F : val.
Implicit Types f x : var.
(*-- LATER: move to TLC LibNatExec *)
Fixpoint nat_compare (x y : nat) :=
match x, y with
| O, O => true
| S x', S y' => nat_compare x' y'
| _, _ => false
end.
Lemma nat_compare_eq : forall n1 n2,
nat_compare n1 n2 = isTrue (n1 = n2).
Proof using.
intros n1. induction n1; intros; destruct n2; simpl; rew_bool_eq; auto_false.
rewrite IHn1. extens. rew_istrue. math.
Qed.
Definition var_funs_exec (n:nat) (xs:vars) : bool := (* --todo: use exec typeclass *)
nat_compare n (List.length xs)
&& is_not_nil xs (* --todo: rename to exec *)
&& var_distinct xs.
Lemma var_funs_exec_eq : forall n xs,
var_funs_exec n xs = isTrue (var_funs n xs).
Proof using.
intros. unfold var_funs_exec, var_funs.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_istrue. iff*.
Qed.
Lemma triple_apps_funs_of_cf_iter : forall n F (vs:vals) xs t H Q,
F = val_funs xs t ->
var_funs_exec (length vs) xs ->
......@@ -346,21 +381,6 @@ Proof using.
applys* rule_apps_funs. applys* triple_trm_of_cf_iter.
Qed.
Definition var_fixs_exec (f:var) (n:nat) (xs:vars) : bool := (* todo: use exec typeclass *)
nat_compare n (List.length xs)
&& is_not_nil xs (* todo: rename to exec *)
&& var_distinct (f::xs).
Lemma var_fixs_exec_eq : forall f n xs,
var_fixs_exec f n xs = isTrue (var_fixs f n xs).
Proof using.
intros. unfold var_fixs_exec, var_fixs.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_istrue. iff*.
Qed.
Lemma triple_apps_fixs_of_cf_iter : forall n f F (vs:vals) xs t H Q,
F = val_fixs f xs t ->
var_fixs_exec f (length vs) xs ->
......@@ -395,43 +415,12 @@ Definition database_spec := True.
*)
Notation "'Register_goal' G" := (Register database_spec G)
(at level 69) : charac.
Notation "'Register_rule' t" := (Register_goal (triple t _ _))
(at level 69) : charac.
Notation "'Register_spec' f" := (Register_rule (trm_apps (trm_val f) _))
(at level 69) : charac.
(** [xspec G] retreives from the database [database_spec]
the specification that could apply to a goal [G].
It places the specification as hypothesis at the head of the goal. *)
Ltac xapp_basic_prepare tt ::= (* actually defined further *)
idtac.
Ltac xspec_context G := (* refined only in LambdaCFLifted *)
fail.
Ltac xspec_registered G :=
ltac_database_get database_spec G.
Ltac xspec_database G :=
first [ xspec_registered G | xspec_context G ].
Ltac xspec_base tt :=
match goal with
| |- ?G => xspec_database G
end.
Ltac xspec_core tt :=
xapp_basic_prepare tt;
xspec_base tt.
Tactic Notation "xspec" :=
xspec_core tt.
(* ---------------------------------------------------------------------- *)
(** ** Registering specification of primitive functions *)
......@@ -439,11 +428,13 @@ Tactic Notation "xspec" :=
Hint Extern 1 (Register_spec (val_prim val_ref)) => Provide rule_ref.
Hint Extern 1 (Register_spec (val_prim val_get)) => Provide rule_get.
Hint Extern 1 (Register_spec (val_prim val_set)) => Provide rule_set.
Hint Extern 1 (Register_spec (val_prim val_add)) => Provide rule_add.
(*
Hint Extern 1 (Register_spec (val_prim val_alloc)) => Provide rule_alloc.
Hint Extern 1 (Register_spec (val_prim val_eq)) => Provide rule_eq.
Hint Extern 1 (Register_spec (val_prim val_add)) => Provide rule_add.
Hint Extern 1 (Register_spec (val_prim val_sub)) => Provide rule_sub.
Hint Extern 1 (Register_spec (val_prim val_ptr_add)) => Provide rule_ptr_add.
*)
(* ********************************************************************** *)
......
......@@ -12,6 +12,46 @@ Set Implicit Arguments.
From Sep Require Export LambdaSemantics.
(* ---------------------------------------------------------------------- *)
(* ** Database of specifications used by [xapp], through tactic [xspec] *)
(** A name for the database *)
Definition database_spec := True.
Notation "'Register_goal' G" := (Register database_spec G)
(at level 69) : charac.
(** [xspec G] retreives from the database [database_spec]
the specification that could apply to a goal [G].
It places the specification as hypothesis at the head of the goal. *)
Ltac xapp_basic_prepare tt :=
fail "not instantiated".
Ltac xspec_context G := (* refined only in LambdaCFLifted *)
fail "not instantiated".
Ltac xspec_registered G :=
ltac_database_get database_spec G.
Ltac xspec_database G :=
first [ xspec_registered G | xspec_context G ].
Ltac xspec_base tt :=
match goal with
| |- ?G => xspec_database G
end.
Ltac xspec_core tt :=
xapp_basic_prepare tt;
xspec_base tt.
Tactic Notation "xspec" :=
xspec_core tt.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xcf] *)
......@@ -130,8 +170,6 @@ Ltac xapps_let_cont tt :=
fail "not instantiated".
Ltac xapp_template xlet_tactic xapp_tactic xlet_cont :=
fail "not instantiated".
Ltac xapp_basic_prepare tt :=
fail "not instantiated".
Ltac xapp_with_args E cont_xapply :=
fail "not instantiated".
Ltac xapp_basic E cont_post tt :=
......
......@@ -673,6 +673,52 @@ Definition val_fixs (f:var) (xs:vars) (t:trm) : val :=
end.
(* ---------------------------------------------------------------------- *)
(** Nonempty list of distinct variables *)
Definition var_funs (n:nat) (xs:vars) : Prop :=
var_distinct xs
/\ length xs = n
/\ xs <> nil.
(** Computable version of the above definition *)
Definition var_funs_exec (n:nat) (xs:vars) : bool := (* --todo: use exec typeclass *)
nat_compare n (List.length xs)
&& is_not_nil xs (* --todo: rename to exec *)
&& var_distinct xs.
Lemma var_funs_exec_eq : forall n xs,
var_funs_exec n xs = isTrue (var_funs n xs).
Proof using.
intros. unfold var_funs_exec, var_funs.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_istrue. iff*.
Qed.
Definition var_fixs (f:var) (n:nat) (xs:vars) : Prop :=
var_distinct (f::xs)
/\ length xs = n
/\ xs <> nil.
Definition var_fixs_exec (f:var) (n:nat) (xs:vars) : bool := (* todo: use exec typeclass *)
nat_compare n (List.length xs)
&& is_not_nil xs (* todo: rename to exec *)
&& var_distinct (f::xs).
Lemma var_fixs_exec_eq : forall f n xs,
var_fixs_exec f n xs = isTrue (var_fixs f n xs).
Proof using.
intros. unfold var_fixs_exec, var_fixs.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_istrue. iff*.
Qed.
(* ---------------------------------------------------------------------- *)
(** Properties of n-ary functions *)
......@@ -692,11 +738,6 @@ Proof using.
{ case_if. rewrite~ IHxs'. }
Qed.
Definition var_funs (n:nat) (xs:vars) : Prop :=
var_distinct xs
/\ length xs = n
/\ xs <> nil.
Lemma red_app_funs_val_ind : forall xs vs m1 m2 tf t r,
red m1 tf m1 (val_funs xs t) ->
red m1 (substs xs vs t) m2 r ->
......@@ -747,11 +788,6 @@ Proof using.
{ simpls. do 2 case_if in N. rewrite~ subst_trm_funs. }
Qed.
Definition var_fixs (f:var) (n:nat) (xs:vars) : Prop :=
var_distinct (f::xs)
/\ length xs = n
/\ xs <> nil.
Lemma red_app_fixs_val : forall xs vs m1 m2 vf f t r,
vf = val_fixs f xs t ->
red m1 (subst f vf (substs xs vs t)) m2 r ->
......@@ -979,3 +1015,4 @@ Ltac var_neq :=
[ false | apply E ] ] end.
Hint Extern 1 (?x <> ?y) => var_neq.
......@@ -21,9 +21,7 @@ Open Scope fmap_scope.
Arguments exist [A] [P].