Commit 7a0c2004 authored by charguer's avatar charguer

progress

parent 743686f0
TLCBuffer
TLCbuffer
Fmap
LambdaSemantics
SepFunctor
......
......@@ -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. }
......
......@@ -32,6 +32,10 @@ include $(TLC)/Makefile.coq
# Exporting the self-contained archive.
.PHONY: export
demo:
echo ${V}
export:
./export.sh
......
......@@ -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].
(* ---------------------------------------------------------------------- *)
......
......@@ -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');
......
......@@ -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 *)
......
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