pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising before class

Browse source
This commit is contained in:
Adam Chlipala 2020-04-14 15:48:36 -04:00
parent 2efec7b61d
commit d74a0ebb42
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
Connecting.v
View file

@ -110,7 +110,7 @@ Proof.
intros; apply (shatter_word a). intros; apply (shatter_word a).
Qed. Qed.
Hint Resolve shatter_word_0. Hint Resolve shatter_word_0 : core.
Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Logic.Eqdep_dec.
@ -314,7 +314,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
t. t.
Qed. Qed.
Hint Resolve split_empty_bwd'. Hint Resolve split_empty_bwd' : core.
Theorem extra_lift : forall (P : Prop) p, Theorem extra_lift : forall (P : Prop) p,
P P
@ -457,7 +457,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
unfold star, himp in *; simp; eauto 7. unfold star, himp in *; simp; eauto 7.
Qed. Qed.
Hint Constructors hoare_triple. Hint Constructors hoare_triple : core.
Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
hoare_triple P (Bind c1 c2) Q hoare_triple P (Bind c1 c2) Q
@ -658,7 +658,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
unfold ptsto; reflexivity. unfold ptsto; reflexivity.
Qed. Qed.
Hint Constructors step. Hint Constructors step : core.
Lemma progress : forall {result} (c : cmd result) P Q, Lemma progress : forall {result} (c : cmd result) P Q,
hoare_triple P c Q hoare_triple P c Q
@ -1384,7 +1384,7 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
next_data <- next_data <-
(data <- Read p; (data <- Read p;
next <- Read (p ^+ ^1); next <- Read (p ^+ ^1);
Return (next, data)); Return (next, r ^+ data));
Return (Again next_data))) Return (Again next_data)))
(fun pr => Return (snd pr)). (fun pr => Return (snd pr)).
@ -1398,7 +1398,8 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
Definition summer_compiled := Eval simpl in proj1_sig translate_summer. Definition summer_compiled := Eval simpl in proj1_sig translate_summer.
(* We restate the program to accommodate limitations in the tactics! *) (* We restate our original example program to accommodate limitations
* in the tactics! *)
Definition reverse_alt p := Definition reverse_alt p :=
pr <- for pr := (p, ^0) loop pr <- for pr := (p, ^0) loop
let (p, r) := pr in let (p, r) := pr in
@ -2731,7 +2732,7 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
equality. equality.
Qed. Qed.
Hint Constructors eval DE.step. Hint Constructors eval DE.step : core.
Lemma translate_exp_sound' : forall V v e, Lemma translate_exp_sound' : forall V v e,
translate_exp V v e translate_exp V v e
@ -2750,7 +2751,7 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
induct 1; simplify; eauto. induct 1; simplify; eauto.
Qed. Qed.
Hint Resolve translate_exp_sound translate_exp_sound'. Hint Resolve translate_exp_sound translate_exp_sound' : core.
Lemma not_stuck_loop : forall V (c : cmd (wrd * wrd)) s, Lemma not_stuck_loop : forall V (c : cmd (wrd * wrd)) s,
translate (rt := TwoWords) translate_loop_body V c s translate (rt := TwoWords) translate_loop_body V c s
@ -3351,5 +3352,4 @@ Module MixedEmbedded32.
Definition incrementer_exported := Eval compute in DE.stmtS incrementer_compiled. Definition incrementer_exported := Eval compute in DE.stmtS incrementer_compiled.
Definition summer_exported := Eval compute in DE.stmtS summer_compiled. Definition summer_exported := Eval compute in DE.stmtS summer_compiled.
Definition reverse_alt_exported := Eval compute in DE.stmtS reverse_alt_compiled. Definition reverse_alt_exported := Eval compute in DE.stmtS reverse_alt_compiled.
End MixedEmbedded32. End MixedEmbedded32.