pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-03-19 19:12:29 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Connecting: failure is not an option

Browse source
This commit is contained in:
Adam Chlipala 2018-04-29 21:24:49 -04:00
parent 82db018daf
commit ba72a971dc
1 changed files with 2 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
Connecting.v
View file

@ -178,8 +178,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
| Bind {result result'} (c1 : cmd result') (c2 : result' -> cmd result) : cmd result | Bind {result result'} (c1 : cmd result') (c2 : result' -> cmd result) : cmd result
| Read (a : wrd) : cmd wrd | Read (a : wrd) : cmd wrd
| Write (a v : wrd) : cmd unit | Write (a v : wrd) : cmd unit
| Loop {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) : cmd acc | Loop {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) : cmd acc.
| Fail {result} : cmd result.
(* We're leaving out allocation and deallocation, to avoid distraction from (* We're leaving out allocation and deallocation, to avoid distraction from
* the main point of the examples to follow. *) * the main point of the examples to follow. *)
@ -397,8 +396,6 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
| HtLoop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) I, | HtLoop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) I,
(forall acc, hoare_triple (I (Again acc)) (body acc) I) (forall acc, hoare_triple (I (Again acc)) (body acc) I)
-> hoare_triple (I (Again init)) (Loop init body) (fun r => I (Done r)) -> hoare_triple (I (Again init)) (Loop init body) (fun r => I (Done r))
| HtFail : forall {result},
hoare_triple (fun _ => False) (Fail (result := result)) (fun _ _ => False)
| HtRead : forall a R, | HtRead : forall a R,
hoare_triple (exists v, a |-> v * R v)%sep (Read a) (fun r => a |-> r * R r)%sep hoare_triple (exists v, a |-> v * R v)%sep (Read a) (fun r => a |-> r * R r)%sep
@ -501,15 +498,6 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
unfold star in *; simp; eauto 7. unfold star in *; simp; eauto 7.
Qed. Qed.
Lemma invert_Fail : forall result P Q,
hoare_triple P (Fail (result := result)) Q
-> forall h, P h -> False.
Proof.
induct 1; propositional; eauto.
unfold star in *; simp; eauto.
Qed.
(* Now that we proved enough basic facts, let's hide the definitions of all (* Now that we proved enough basic facts, let's hide the definitions of all
* these predicates, so that we reason about them only through automation. *) * these predicates, so that we reason about them only through automation. *)
Opaque heq himp lift star exis ptsto. Opaque heq himp lift star exis ptsto.
@ -847,8 +835,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
Ltac step0 := basic || eapply HtBind || (eapply use_lemma; [ basic | cancel; auto ]) Ltac step0 := basic || eapply HtBind || (eapply use_lemma; [ basic | cancel; auto ])
|| (eapply use_lemma; [ eapply HtRead' | solve [ cancel; auto ] ]) || (eapply use_lemma; [ eapply HtRead' | solve [ cancel; auto ] ])
|| (eapply HtRead''; solve [ cancel ]) || (eapply HtRead''; solve [ cancel ])
|| (eapply HtStrengthen; [ eapply use_lemma; [ basic | cancel; auto ] | ]) || (eapply HtStrengthen; [ eapply use_lemma; [ basic | cancel; auto ] | ]).
|| (eapply HtConsequence; [ apply HtFail | .. ]).
Ltac step := step0; simp. Ltac step := step0; simp.
Ltac ht := simp; repeat step. Ltac ht := simp; repeat step.
Ltac conseq := simplify; eapply HtConsequence. Ltac conseq := simplify; eapply HtConsequence.