diff --git a/model/FILES b/model/FILES index 7665a40e7e66ab846172f6fdde411dea8e27b423..353a8bcc59bd981412a5dedee58df7ff0768c867 100644 --- a/model/FILES +++ b/model/FILES @@ -1,4 +1,4 @@ -TLCBuffer +TLCbuffer Fmap LambdaSemantics SepFunctor diff --git a/model/Fmap.v b/model/Fmap.v index 01276f7e5c8dea855259ec8a248ff48575e0e327..05babaa52e5b4293f84dc49d469fe336a5d5098c 100644 --- a/model/Fmap.v +++ b/model/Fmap.v @@ -46,7 +46,7 @@ Definition map_union (A B : Type) (f1 f2 : map A B) : map A B := (** Finite domain of a partial function *) Definition map_finite (A B : Type) (f : map A B) := - exists (L : list A), forall (x:A), f x <> None -> Mem x L. + exists (L : list A), forall (x:A), f x <> None -> mem x L. (** Disjointness of domain of two partial functions *) @@ -97,8 +97,8 @@ Lemma map_union_finite : forall f1 f2, map_finite (map_union f1 f2). Proof using. introv [L1 F1] [L2 F2]. exists (L1 ++ L2). introv M. - specializes F1 x. specializes F2 x. unfold map_union in M. - apply Mem_app_or. destruct~ (f1 x). + specializes F1 x. specializes F2 x. unfold map_union in M. + apply mem_app. destruct~ (f1 x). Qed. End MapOps. @@ -114,7 +114,7 @@ Inductive fmap (A B : Type) : Type := fmap_make { fmap_data :> map A B; fmap_finite : map_finite fmap_data }. -Implicit Arguments fmap_make [A B]. +Arguments fmap_make [A] [B]. (* ---------------------------------------------------------------------- *) @@ -126,7 +126,7 @@ Program Definition fmap_empty (A B : Type) : fmap A B := fmap_make (fun l => None) _. Next Obligation. exists (@nil A). auto_false. Qed. -Implicit Arguments fmap_empty [[A] [B]]. +Arguments fmap_empty {A} {B}. (** Singleton fmap *) @@ -160,7 +160,7 @@ Definition fmap_update A B (h:fmap A B) (x:A) (v:B) := (** Inhabited type [fmap] *) Global Instance Inhab_fmap A B : Inhab (fmap A B). -Proof using. intros. applys prove_Inhab (@fmap_empty A B). Qed. +Proof using. intros. applys Inhab_of_val (@fmap_empty A B). Qed. (** Compatible fmaps *) @@ -312,8 +312,8 @@ Lemma fmap_union_eq_empty_inv_l : forall h1 h2, Proof using. intros (f1&F1) (f2&F2) M. inverts M as M. applys fmap_make_eq. intros l. - unfolds map_union. - lets: func_same_1 l M. + unfolds map_union. + lets: fun_eq_1 l M. cases (f1 l); auto_false. Qed. @@ -324,7 +324,7 @@ Proof using. intros (f1&F1) (f2&F2) M. inverts M as M. applys fmap_make_eq. intros l. unfolds map_union. - lets: func_same_1 l M. + lets: fun_eq_1 l M. cases (f1 l); auto_false. Qed. @@ -541,9 +541,9 @@ Qed. End FmapProp. -Implicit Arguments fmap_union_assoc [A B]. -Implicit Arguments fmap_union_comm_of_disjoint [A B]. -Implicit Arguments fmap_union_comm_of_agree [A B]. +Arguments fmap_union_assoc [A] [B]. +Arguments fmap_union_comm_of_disjoint [A] [B]. +Arguments fmap_union_comm_of_agree [A] [B]. (* ********************************************************************** *) @@ -791,24 +791,24 @@ Definition loc_fresh_gen (L : list nat) := (1 + fold_right plus O L)%nat. Lemma loc_fresh_ind : forall l L, - Mem l L -> + mem l L -> (l < loc_fresh_gen L)%nat. Proof using. intros l L. unfold loc_fresh_gen. - induction L; introv M; inverts M; rew_list. + induction L; introv M; inverts M; rew_listx. { math. } { forwards~: IHL. math. } Qed. Lemma loc_fresh_nat_ge : forall (L:list nat), - exists (l:nat), forall (i:nat), ~ Mem (l+i)%nat L. + exists (l:nat), forall (i:nat), ~ mem (l+i)%nat L. Proof using. intros L. exists (loc_fresh_gen L). intros i M. lets: loc_fresh_ind M. math. Qed. Lemma loc_fresh_nat : forall (L:list nat), - exists (l:nat), ~ Mem l L. + exists (l:nat), ~ mem l L. Proof using. intros L. forwards (l&P): loc_fresh_nat_ge L. exists l. intros M. applys (P 0%nat). applys_eq M 2. math. @@ -829,8 +829,8 @@ Proof using. unfold fmap_disjoint, map_disjoint. simpl. lets (l&F): (loc_fresh_nat (null::L)). exists l. split. - { intros l'. case_if~. - { right. applys not_not_elim. intros H. applys F. + { intros l'. case_if~. (* --TODO: fix subst *) + { subst. right. applys not_not_inv. intros H. applys F. constructor. applys~ M. } } { intro_subst. applys~ F. } Qed. @@ -847,8 +847,8 @@ Proof using. { rewrite fmap_conseq_succ. destruct (IHk (S l)%nat) as [E|?]. { intros i N. applys F (S i). applys_eq N 2. math. } - { simpl. unfold map_union. case_if~. - { right. applys not_not_elim. intros H. applys F 0%nat. + { simpl. unfold map_union. case_if~. (* --TODO: fix subst *) + { subst. right. applys not_not_inv. intros H. applys F 0%nat. constructor. math_rewrite (l'+0 = l')%nat. applys~ M. } } { auto. } } } { intro_subst. applys~ F 0%nat. rew_nat. auto. } diff --git a/model/Makefile b/model/Makefile index ad748477b4153283c1ae3ff5b8c679fd6ca4d241..111309637efbe982f683ae9c05185a7bac6f9937 100644 --- a/model/Makefile +++ b/model/Makefile @@ -32,6 +32,10 @@ include \$(TLC)/Makefile.coq # Exporting the self-contained archive. .PHONY: export +demo: + echo \${V} + + export: ./export.sh diff --git a/model/SepFunctor.v b/model/SepFunctor.v index 9caa380b713d8ab0d4bfcd9c45d24de7a1eda9f2..8128fc98d40bc7c7c9e8254f229737535f7da6ba 100644 --- a/model/SepFunctor.v +++ b/model/SepFunctor.v @@ -39,7 +39,7 @@ Lemma hprop_extens : forall A (H1 H2:A->Prop), (forall h, H1 h <-> H2 h) -> (H1 = H2). Proof using. - introv M. applys func_ext_1. intros h. applys* prop_ext. + introv M. applys fun_ext_1. intros h. applys* prop_ext. Qed. @@ -49,14 +49,20 @@ Qed. (* ---------------------------------------------------------------------- *) (* ** Definition of entailment *) +(* --TODO: define [himpl] to mean [pred_incl] and [pimpl] to mean [rel_incl'] *) + (** TLC defines [pred_le P Q] as [forall x, P x -> Q x]. *) -Notation "P ==> Q" := (pred_le P Q) +Notation "P ==> Q" := (pred_incl P Q) (at level 55, right associativity) : heap_scope. -(** TLC defines [rel_le P Q] as [forall x y, P x y -> Q x y]. *) +(* [rel_incl'] is like TLC's [rel_incl] but defined in terms of [pred_incl] + so that after [intros r] we get an entailment. *) + +Definition rel_incl' A B (P Q:A->B->Prop) := + forall r, pred_incl (P r) (Q r). -Notation "P ===> Q" := (rel_le P Q) +Notation "P ===> Q" := (rel_incl' P Q) (at level 55, right associativity) : heap_scope. Open Scope heap_scope. @@ -69,7 +75,7 @@ Section HimplProp. Variable A : Type. Implicit Types H : A -> Prop. -Hint Unfold pred_le. +Hint Unfold pred_incl. (** Entailment is reflexive, symmetric, transitive *) @@ -77,7 +83,7 @@ Lemma himpl_refl : forall H, H ==> H. Proof using. intros h. auto. Qed. -Lemma himpl_trans : forall H1 H2 H3, +Lemma himpl_trans : forall H2 H1 H3, (H1 ==> H2) -> (H2 ==> H3) -> (H1 ==> H3). @@ -87,7 +93,7 @@ Lemma himpl_antisym : forall H1 H2, (H1 ==> H2) -> (H2 ==> H1) -> (H1 = H2). -Proof using. introv M1 M2. applys prop_ext_1. intros h. iff*. Qed. +Proof using. introv M1 M2. applys pred_ext_1. intros h. iff*. Qed. (** Paragraphe of the definition, used by tactics *) @@ -111,11 +117,20 @@ Proof. intros. subst. applys~ himpl_refl. Qed. End HimplProp. -Implicit Arguments himpl_of_eq [A H1 H2]. -Implicit Arguments himpl_of_eq_sym [A H1 H2]. -Implicit Arguments himpl_antisym [A H1 H2]. +Arguments himpl_of_eq [A] [H1] [H2]. +Arguments himpl_of_eq_sym [A] [H1] [H2]. +Arguments himpl_antisym [A] [H1] [H2]. + +Hint Resolve himpl_refl. + +(** Reflexivity for postconditions *) + +Lemma refl_rel_incl' : forall A B (Q:A->B->Prop), + Q ===> Q. +Proof using. apply refl_rel_incl. Qed. + +Hint Resolve refl_rel_incl'. -Hint Resolve himpl_refl rel_le_refl. (* ********************************************************************** *) @@ -271,9 +286,11 @@ Implicit Types P : Prop. (* ---------------------------------------------------------------------- *) (* ** Additional notation for entailment *) +Delimit Scope heap_scope with heap. + (** [H1 ==+> H2] is short for [H1 ==> H1 \* H2] *) -Notation "H1 ==+> H2" := (H1 ==> H1 \* H2) +Notation "H1 ==+> H2" := (H1%heap ==> H1%heap \* H2%heap) (at level 55) : heap_scope. @@ -309,7 +326,7 @@ Open Scope heap_scope. (* ** Properties of [hprop] *) Global Instance hinhab : Inhab hprop. -Proof using. intros. apply (prove_Inhab hempty). Qed. +Proof using. intros. apply (Inhab_of_val hempty). Qed. (* ---------------------------------------------------------------------- *) @@ -318,7 +335,7 @@ Proof using. intros. apply (prove_Inhab hempty). Qed. Lemma hstar_hempty_r : forall H, H \* \[] = H. Proof using. - applys neutral_r_from_comm_neutral_l. + applys neutral_r_of_comm_neutral_l. applys~ hstar_comm. applys~ hstar_hempty_l. Qed. @@ -352,7 +369,7 @@ Qed. Lemma hempty_eq_hpure_true : \[] = \[True]. Proof using. - applys prop_ext_1. intros h. iff M. + applys pred_ext_1. intros h. iff M. { applys* hpure_intro. } { forwards*: hpure_inv M. } Qed. @@ -360,7 +377,7 @@ Qed. Lemma hfalse_hstar_any : forall H, \[False] \* H = \[False]. Proof using. - intros. applys prop_ext_1. intros h. rewrite hstar_pure. iff M. + intros. applys pred_ext_1. intros h. rewrite hstar_pure. iff M. { false*. } { lets: hpure_inv M. false*. } Qed. @@ -468,7 +485,7 @@ Proof using. applys M. rewrite~ hstar_hempty_l. Qed. -Implicit Arguments rule_extract_hprop_from_extract_hexists [T]. +Arguments rule_extract_hprop_from_extract_hexists [T]. (* ---------------------------------------------------------------------- *) diff --git a/model/SepTactics.v b/model/SepTactics.v index 02c1f7a38336c1e06217db731c34b3de3dfba745..fddf6117fcbcb1bbbf1928026a232474a3327772 100644 --- a/model/SepTactics.v +++ b/model/SepTactics.v @@ -61,7 +61,7 @@ Local Transparent repr. Lemma star_post_empty : forall B (Q:B->hprop), Q \*+ \[] = Q. -Proof using. extens. intros. rewrite~ hstar_hempty_r. Qed. +Proof using. extens. intros. rewrite* hstar_hempty_r. Qed. Hint Rewrite hstar_hempty_l hstar_hempty_r hstar_assoc star_post_empty : rew_heap. @@ -243,9 +243,9 @@ Qed. Ltac hpull_prepare tt := match goal with - | |- @rel_le unit _ _ _ => let t := fresh "_tt" in intros t; destruct t - | |- @rel_le _ _ _ _ => let r := fresh "r" in intros r - | |- pred_le _ _ => idtac + | |- @rel_incl' unit _ _ _ => let t := fresh "_tt" in intros t; destruct t + | |- @rel_incl' _ _ _ _ => let r := fresh "r" in intros r + | |- pred_incl _ _ => idtac | _ => fail 1 "not a goal for hpull" end. @@ -730,12 +730,12 @@ Ltac check_arg_true v := Ltac hcancel_prepare tt := match goal with - | |- @rel_le _ _ _ ?Q' => is_evar Q'; apply rel_le_refl - | |- @rel_le unit _ ?Q ?Q' => let t := fresh "_tt" in intros t; destruct t + | |- @rel_incl' _ _ _ ?Q' => is_evar Q'; apply refl_rel_incl' + | |- @rel_incl' unit _ ?Q ?Q' => let t := fresh "_tt" in intros t; destruct t | |- eq _ _ => applys himpl_antisym - | |- @rel_le _ _ _ _ => let r := fresh "r" in intros r - | |- pred_le _ ?H' => is_evar H'; apply himpl_refl - | |- pred_le _ _ => idtac + | |- @rel_incl' _ _ _ _ => let r := fresh "r" in intros r + | |- pred_incl _ ?H' => is_evar H'; apply himpl_refl + | |- pred_incl _ _ => idtac end. Ltac hcancel_setup tt := @@ -747,7 +747,7 @@ Ltac hcancel_setup tt := Ltac hcancel_cleanup tt := try apply hcancel_stop; try apply hcancel_stop; - try apply pred_le_refl; + try apply himpl_refl; try hcancel_hint_remove tt; try remove_empty_heaps_right tt; try remove_empty_heaps_left tt; @@ -1085,8 +1085,8 @@ Lemma hchange_lemma : forall H1 H1' H H' H2, (H1' \* H2 ==> H') -> (H ==> H'). Proof using. - intros. applys* (@pred_le_trans heap) (H1 \* H2). - applys* (@pred_le_trans heap) (H1' \* H2). hsimpl~. + intros. applys* (@himpl_trans heap) (H1 \* H2). + applys* (@himpl_trans heap) (H1' \* H2). hsimpl~. Qed. Ltac hchange_apply L cont1 cont2 := @@ -1267,7 +1267,7 @@ Lemma is_local_intro : forall F, (forall H Q, F H Q <-> local F H Q) -> is_local F. Proof using. - intros. unfold is_local. apply func_ext_2. + intros. unfold is_local. apply fun_ext_2. intros. applys prop_ext. applys H. Qed. @@ -1611,7 +1611,7 @@ Tactic Notation "xpulls" "*" := xpulls; auto_star. Ltac xapply_core H cont1 cont2 := forwards_nounfold_then H ltac:(fun K => match xpostcondition_is_evar tt with - | true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try apply rel_le_refl ] + | true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try apply himpl_refl ] | false => eapply local_frame_htop; [ xlocal | sapply K | cont1 tt | cont2 tt ] end). @@ -1847,7 +1847,7 @@ Tactic Notation "xunfold" "*" constr(E) := xunfold E; auto_star. Ltac xunfold_arg_at_core E n := let E := get_head E in (* to get rid of typeclasses arguments *) - let n := nat_from_number n in + let n := number_to_nat n in change repr with repr'; let h := fresh "temp" in set (h := repr'); diff --git a/model/TLCbuffer.v b/model/TLCbuffer.v index c5a364b570454d79d33a98eed09c07f2a8546d7e..e067eafef6e6733fd617e21a1337bfe9c7617069 100644 --- a/model/TLCbuffer.v +++ b/model/TLCbuffer.v @@ -10,7 +10,8 @@ License: MIT. Set Implicit Arguments. -Require Import LibTactics LibLogic. +Require Import LibTactics LibLogic LibList. +Require LibListZ. Generalizable Variables A B. @@ -61,11 +62,6 @@ Hint Rewrite nat_zero_plus nat_plus_zero nat_plus_succ -(*----------------------*) -(* Hint for LibListZ *) - -Hint Rewrite length_map index_map_eq : rew_arr. - (*----------------------*) (* ListExec *) @@ -83,8 +79,7 @@ Definition is_not_nil A (l:list A) : bool := Lemma is_not_nil_eq : forall A (l:list A), is_not_nil l = isTrue (l <> nil). Proof. - intros. destruct l; simpl; fold_bool; fold_prop; (* TODO: update *) - auto_false. + intros. destruct l; simpl; rew_bool_eq; auto_false. Qed. Lemma List_length_eq : forall A (l:list A), @@ -93,7 +88,7 @@ Proof using. intros. induction l; simpl; rew_list; auto. Qed. Lemma List_app_eq : forall A (L1 L2:list A), - List.app L1 L2 = LibList.append L1 L2. + List.app L1 L2 = LibList.app L1 L2. Proof using. intros. induction L1; simpl; rew_list; congruence. Qed. @@ -108,7 +103,7 @@ Qed. Lemma List_map_eq : forall A B (f:A->B) (L:list A), List.map f L = LibList.map f L. Proof using. - intros. induction L; simpl; rew_list; congruence. + intros. induction L; simpl; rew_listx; congruence. Qed. Lemma List_combine_eq : forall A B (L1:list A) (L2:list B), @@ -124,6 +119,13 @@ Qed. (* todo: reformulate without arguments *) + +(*----------------------*) +(* Hint for LibListZ *) + +Hint Rewrite LibListZ.length_map LibListZ.index_map_eq : rew_arr. + + (*----------------------*) (* Tactics *)