-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathSemantics.v
122 lines (106 loc) · 4.86 KB
/
Semantics.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
(* *****************************************************************)
(* *)
(* Verified polyhedral AST generation *)
(* *)
(* Nathanaël Courant, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* *****************************************************************)
Require Import List.
Require Import Vpl.Impure.
Require Import Mymap.
Require Import ImpureOperations.
Require Import Misc.
Parameter mem : Type.
(** * Iterating semantics on a list *)
Inductive iter_semantics {A : Type} (P : A -> mem -> mem -> Prop) : list A -> mem -> mem -> Prop :=
| IDone : forall mem, iter_semantics P nil mem mem
| IProgress : forall x l mem1 mem2 mem3,
P x mem1 mem2 -> iter_semantics P l mem2 mem3 ->
iter_semantics P (x :: l) mem1 mem3.
Lemma iter_semantics_map {A : Type} (P Q : A -> mem -> mem -> Prop) :
forall l mem1 mem2,
(forall x mem1 mem2, In x l -> P x mem1 mem2 -> Q x mem1 mem2) ->
iter_semantics P l mem1 mem2 ->
iter_semantics Q l mem1 mem2.
Proof.
intros l mem1 mem2 Himp Hsem.
induction Hsem; econstructor; eauto; [eapply Himp|eapply IHHsem]; eauto.
- simpl; auto.
- intros; apply Himp; simpl; auto.
Qed.
Lemma iter_semantics_mapl :
forall (A B : Type) P (f : A -> B) (l : list A) mem1 mem2,
iter_semantics P (map f l) mem1 mem2 <-> iter_semantics (fun x => P (f x)) l mem1 mem2.
Proof.
intros A B P f. induction l.
- intros; split; simpl; intros H; inversion_clear H; constructor.
- intros; split; simpl; intros H; inversion_clear H; econstructor; eauto; rewrite IHl in *; auto.
Qed.
Lemma iter_semantics_combine :
forall (A B : Type) P (xs : list A) (ys : list B) mem1 mem2,
length xs = length ys -> iter_semantics P xs mem1 mem2 <-> iter_semantics (fun p => P (fst p)) (combine xs ys) mem1 mem2.
Proof.
intros A B P xs ys mem1 mem2 H.
replace xs with (map fst (combine xs ys)) at 1 by (apply map_combine; auto).
rewrite iter_semantics_mapl; reflexivity.
Qed.
Module IterImpureSemantics (Import Imp: FullImpureMonad).
Module ImpOps := ImpureOps Imp.
Import ImpOps.
Lemma iter_semantics_sequence :
forall (A : Type) P (xs : list (imp A)) (ys : list A) mem1 mem2,
mayReturn (sequence xs) ys ->
iter_semantics (fun x mem3 mem4 => WHEN y <- x THEN P y mem3 mem4) xs mem1 mem2 -> iter_semantics P ys mem1 mem2.
Proof.
intros A P. induction xs.
- intros ys mem1 mem2 Hys Hsem; simpl in *. apply mayReturn_pure in Hys; rewrite <- Hys.
inversion_clear Hsem; constructor.
- intros ys mem1 mem2 Hys Hsem; simpl in *.
bind_imp_destruct Hys y Hy.
bind_imp_destruct Hys ys1 Hys1.
apply mayReturn_pure in Hys; rewrite <- Hys in *.
inversion_clear Hsem.
econstructor; [apply H; auto|].
apply IHxs; auto.
Qed.
(* yet another unfortunately needed lemma because of mymap... *)
Lemma iter_semantics_mymapl :
forall (A B : Type) P (f : A -> B) (l : list A) mem1 mem2,
iter_semantics P (mymap f l) mem1 mem2 <-> iter_semantics (fun x => P (f x)) l mem1 mem2.
Proof.
intros A B P f. induction l.
- intros; split; simpl; intros H; inversion_clear H; constructor.
- intros; split; simpl; intros H; inversion_clear H; econstructor; eauto; rewrite IHl in *; auto.
Qed.
Lemma iter_semantics_mapM :
forall (A B : Type) f P (xs : list A) (ys : list B) mem1 mem2,
mayReturn (mapM f xs) ys ->
iter_semantics (fun x mem3 mem4 => WHEN y <- f x THEN P y mem3 mem4) xs mem1 mem2 -> iter_semantics P ys mem1 mem2.
Proof.
intros A B f P xs ys mem1 mem2 Hmap Hsem.
eapply iter_semantics_sequence; [exact Hmap|].
rewrite iter_semantics_mymapl. auto.
Qed.
Lemma iter_semantics_mapM_rev :
forall (A B : Type) P f (xs : list A) (ys : list B) mem1 mem2,
mayReturn (mapM f xs) ys ->
iter_semantics P ys mem1 mem2 ->
iter_semantics (fun '(x, y) mem3 mem4 => mayReturn (f x) y /\ P y mem3 mem4) (combine xs ys) mem1 mem2.
Proof.
intros A B P f. induction xs.
- intros ys mem1 mem2 Hys Hsem; simpl in *. apply mayReturn_pure in Hys; rewrite <- Hys in Hsem.
inversion_clear Hsem; constructor.
- intros ys mem1 mem2 Hys Hsem; simpl in *.
bind_imp_destruct Hys y Hy.
bind_imp_destruct Hys ys1 Hys1.
apply mayReturn_pure in Hys; rewrite <- Hys in *.
inversion_clear Hsem.
econstructor; [eauto|].
apply IHxs; auto.
Qed.
End IterImpureSemantics.