Commit fbe40b7d authored by charguer's avatar charguer
Browse files

cleanup

parent 1ea81078
......@@ -7,6 +7,8 @@ Require TLC.LibSet.
Generalizable Variables A B.
(* TODO: local setup *)
Ltac auto_typeclass :=
match goal with |- Inhab _ => typeclass end.
......@@ -14,6 +16,14 @@ Ltac auto_star ::=
try solve [ jauto_set; solve [ eauto | congruence | math | auto_typeclass ] ].
(* TODO: update TLC *)
Lemma lengthZ_zero_eq_eq_nil : forall A (l:list A),
(LibListZ.length l = 0) = (l = nil).
Proof using.
intros. unfolds length. rewrite <- LibList.length_zero_eq_eq_nil. math.
Qed.
Lemma index_update_inv : forall A `{Inhab B} (L:map A B) (a x:A) (b:B),
index L a ->
index (L[a:=b]) x ->
......@@ -23,6 +33,7 @@ Proof using.
rewrite* dom_update_at_index in Ix.
Qed.
(* TODO: update CFML *)
Module ArrayMap.
......@@ -38,10 +49,6 @@ Definition conseq_dom A (n:int) (M:map int A) : Prop :=
Parameter ArrayMap_conseq_dom : forall A (M:map int A) p,
p ~> ArrayMap M ==+> Hexists n, \[conseq_dom n M].
(*******************************************************************)
(** Properties of conseq *)
Lemma conseq_dom_index_eq : forall A n (L:map int A),
conseq_dom n L ->
index n = index L. (* i.e. [index L x <> index n x] *)
......@@ -153,8 +160,7 @@ Hint Extern 1 (RegisterSpec Array_ml.init) => Provide init_spec.
End ArrayMap.
(* TODO: id outside domain *)
(* TODO: update TLC *)
Module LibMaps.
Section Map.
......@@ -206,6 +212,7 @@ End Map.
End LibMaps.
(* TODO: update CFML *)
Module RefGroupSpecs.
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec_group.
......
......@@ -3,17 +3,11 @@ Require Import CFML.CFLib.
Require Import Stdlib.
Require Import MutableQueue_ml.
Require Import TLC.LibListZ.
Require Import CFMLAdditions.
Implicit Types n : int.
Implicit Types q : loc.
(* TODO: update TLC *)
Lemma length_zero_eq_eq_nil : forall A (l:list A),
(LibListZ.length l = 0) = (l = nil).
Proof using.
intros. unfolds length. rewrite <-LibList.length_zero_eq_eq_nil. math.
Qed.
(*******************************************************************)
(** Representation Predicate *)
......@@ -105,7 +99,7 @@ Lemma is_empty_spec : forall A (L:list A) q,
POST (fun b => \[b = isTrue (L = nil)]).
Proof using.
xcf. xopen q. xpull ;=> f b n (I1&I2). xapps. xclose* q. xrets.
subst n. rewrite* length_zero_eq_eq_nil.
subst n. rewrite lengthZ_zero_eq_eq_nil. tauto.
Unshelve. solve_type.
Qed.
......@@ -169,8 +163,7 @@ Proof using.
intros. applys (rm HR).
xlet (fun b => \[b = isTrue (L1 <> nil)] \* q1 ~> Queue L1 \* q2 ~> Queue L2).
{ xapps. xrets. rew_isTrue*. }
intros ->.
xif.
intros ->. xif.
{ destruct L1 as [|x L1']; tryfalse.
xseq. { xapps*. intros L1'' E. inverts E. xapps. }
show IH. xpull.
......
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