Commit 3a75339e authored by Léon Gondelman's avatar Léon Gondelman
Browse files

fixed bug in the definition of denv_wf_len

parent cef2551f
...@@ -40,7 +40,7 @@ Section denv. ...@@ -40,7 +40,7 @@ Section denv.
Fixpoint denv_wf_len (E: known_locs) (m: denv) : bool := Fixpoint denv_wf_len (E: known_locs) (m: denv) : bool :=
match E, m with match E, m with
| _, [] => true | _, [] => true
| _ :: E', _ :: m' => denv_wf_len E m' | _ :: E', _ :: m' => denv_wf_len E' m'
| [], _ => false | [], _ => false
end. end.
...@@ -684,37 +684,77 @@ Section denv_spec. ...@@ -684,37 +684,77 @@ Section denv_spec.
E `prefix_of`E' E `prefix_of`E'
denv_wf_len E' m. denv_wf_len E' m.
Proof. Proof.
revert E. induction m as [| x m']; intros. revert E E'. induction m as [| x m']; intros.
- by destruct E'. - by destruct E'.
- destruct E', E; simplify_eq /=; - destruct E', E;
[ | by apply prefix_nil_not in H1 | | ]; by eauto. [ | by apply prefix_nil_not in H1 | | ]; try by eauto.
simpl. destruct m' ; try done. destruct E'; eauto.
eapply IHm'. done. by eapply prefix_cons_inv_2.
Qed.
Lemma denv_wf_len_mono_r E m1 m2 :
denv_wf_len E (m1 ++ m2)
denv_wf_len E m2.
Proof.
revert m1 m2. induction E; intros m1 m2 Hwf.
- destruct m2; first by naive_solver.
simpl in Hwf. destruct (m1 ++ o :: m2) as [|] eqn:Hyp.
+ destruct m1; by inversion Hyp.
+ done.
- destruct m1; first by naive_solver.
destruct m2; first done.
* simpl in *. eapply IHE with (m1 ++ [o0]).
rewrite -app_assoc. naive_solver.
Qed.
Lemma denv_wf_val_mono_r E m1 m2 :
denv_wf_val E (m1 ++ m2)
denv_wf_val E m2.
Proof.
revert m2. induction m1; intros m2 Hwf.
- naive_solver.
- apply IHm1. simpl in Hwf.
destruct a as [d|]; last done.
destruct d. naive_solver.
Qed. Qed.
Lemma denv_wf_mono E E' m : Lemma denv_wf_mono E E' m :
denv_wf E m E `prefix_of` E' denv_wf E' m. denv_wf E m E `prefix_of` E' denv_wf E' m.
Proof. Proof.
rewrite !andb_True. rewrite !andb_True. revert E E'.
induction m as [|[denv|] ms]; simpl; eauto. induction m as [|[denv|] ms]; eauto.
- intros [_ Hwf] Hpre; split; first done. by destruct E'. - intros E E' [_ Hwf] Hpre; split; first done. by destruct E'.
- destruct denv. intros. destruct_and!. - intros E E' [ Hwf1 Hwf2] Hpre.
split_and. rewrite andb_True. split. split_and.
eapply dval_wf_mono; eauto. + destruct E'.
apply IHms; eauto. * destruct E; simplify_eq; first by naive_solver.
+ split; first done; by destruct E. by apply prefix_nil_not in Hpre.
+ destruct E, E'; simplify_eq /=; try done; * simpl. destruct denv as [ lvl q dv].
first by apply prefix_nil_not in H1. rewrite andb_True. split.
destruct ms; simplify_eq /=; first done. ** simpl in Hwf1. apply andb_True in Hwf1 as [Hwf11 Hwf12].
pose H1. by eapply dval_wf_mono.
apply prefix_cons_inv_1 in p. ** eapply (IHms E (c::E')); last done. split.
apply (denv_wf_len_mono (c::E)). done. *** apply (denv_wf_val_mono_r E
rewrite -p in H1. by rewrite -p. [Some {| denv_level := lvl; denv_frac := q; denv_dval := dv |}]).
- intros. destruct H0 as [Hwg1 He]. naive_solver.
destruct E, E'; try done. *** apply (denv_wf_len_mono_r E
+ by apply prefix_nil_not in H1. [Some {| denv_level := lvl; denv_frac := q; denv_dval := dv |}]).
+ by apply IHms. naive_solver.
+ by eapply denv_wf_len_mono.
- intros E E' [ Hwf1 Hwf2] Hpre.
split_and.
+ destruct E'.
* destruct E; simplify_eq; first by naive_solver.
by apply prefix_nil_not in Hpre.
* simpl. eapply (IHms E (c::E')); last done. split.
** by eapply (denv_wf_val_mono_r E [None]).
** by eapply (denv_wf_len_mono_r E [None]).
+ by eapply denv_wf_len_mono.
Qed. Qed.
Lemma denv_wf_merge_val (E : known_locs) (m1 m2 : denv) : Lemma denv_wf_merge_val (E : known_locs) (m1 m2 : denv) :
denv_wf_val E m1 denv_wf_val E m2 denv_wf_val E (denv_merge m1 m2). denv_wf_val E m1 denv_wf_val E m2 denv_wf_val E (denv_merge m1 m2).
Proof. Proof.
...@@ -762,7 +802,7 @@ Section denv_spec. ...@@ -762,7 +802,7 @@ Section denv_spec.
Lemma denv_wf_len_unlock E m : Lemma denv_wf_len_unlock E m :
denv_wf_len E m denv_wf_len E (denv_unlock m). denv_wf_len E m denv_wf_len E (denv_unlock m).
Proof. Proof.
induction m; destruct E; naive_solver. revert m; induction E; destruct m; try naive_solver.
Qed. Qed.
Lemma denv_wf_unlock E m : Lemma denv_wf_unlock E m :
...@@ -794,10 +834,16 @@ Section denv_spec. ...@@ -794,10 +834,16 @@ Section denv_spec.
eapply IHm; eauto. eapply IHm; eauto.
Qed. Qed.
Lemma denv_delete_full_len i m m' q dv :
denv_delete_full_aux i m = Some (m', q, dv)
length m' = (length m - 1)%nat.
Proof. Admitted.
Lemma denv_delete_full_len_aux_wf E i m m' q dv : Lemma denv_delete_full_len_aux_wf E i m m' q dv :
denv_wf_len E m denv_delete_full_aux i m = Some (m', q, dv) denv_wf_len E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf_len E m'. denv_wf_len E m'.
Proof. Admitted. Proof.
Admitted.
Lemma denv_delete_full_aux_wf E i m m' q dv : Lemma denv_delete_full_aux_wf E i m m' q dv :
denv_wf E m denv_delete_full_aux i m = Some (m', q, dv) denv_wf E m denv_delete_full_aux i m = Some (m', q, dv)
......
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