 ### extra

parent edea7903
 Lemma normally_idempotent2 : forall H, normally (normally H) ==> normally H. Proof using. intros. unfold normally at 1. hpull ;=> H1 H2 N1 R. asserts E: (\[] ==> RO H2). (* equivalent to [RO H2 hempty] *) { intros h M. rewrites (hempty_inv (rm M)). (* This is almost true. I think we would need to know that H2 is not [False], i.e. that at least one heap satisfies [RO H2] in order to conclude. We might try to add \[exists h2, RO H2 h2], or equivalently \[ ~ (RO H2 ==> \[False]) ] to the definition. *) admit. } hchange E. hchanges R. Abort. (* It this was true, we would have a proper idempotence result: [(normally (normally H)) = normally H] *) End Normally. Program Definition normally' H h1 := (* alternative *) exists h2, heap_compat h1 h2 /\ h1^r = fmap_empty ... ...
 ... ... @@ -1307,27 +1307,6 @@ Proof using. intros. applys normally_intro. applys normal_normally. Qed. Lemma normally_idempotent2 : forall H, normally (normally H) ==> normally H. Proof using. intros. unfold normally at 1. hpull ;=> H1 H2 N1 R. asserts E: (\[] ==> RO H2). (* equivalent to [RO H2 hempty] *) { intros h M. rewrites (hempty_inv (rm M)). (* This is almost true. I think we would need to know that H2 is not [False], i.e. that at least one heap satisfies [RO H2] in order to conclude. We might try to add \[exists h2, RO H2 h2], or equivalently \[ ~ (RO H2 ==> \[False]) ] to the definition. *) admit. } hchange E. hchanges R. Abort. (* It this was true, we would have a proper idempotence result: [(normally (normally H)) = normally H] *) End Normally. (* ---------------------------------------------------------------------- *) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!