Require Import List.
Import ListNotations.
Require Import Relations.
Utilities for proof scripts
Ltac inv H :=
inversion H ;
subst ;
clear H.
Marking cases in proof scripts.
Definition CASE {
A B C:
Type} (
s1:
A) (
t:
B) (
s2:
C) :=
True.
Oracles
The type of oracles, used to deal with non-determinism.
Definition oracle :=
list bool.
Miscellaneous semantics definitions
Reflexive-transitive closure of a stepping relation R.
Inductive run {
A E :
Type} (
R :
A ->
list E ->
A ->
Prop) (
x :
A) :
list E ->
A ->
Prop :=
run_step :
forall t y,
R x t y ->
run R x t y
|
run_refl :
run R x nil x
|
run_trans :
forall y z t1 t2,
run R x t1 y ->
run R y t2 z ->
run R x (
t1++
t2)
z.
Reflexive-transitive closure of a stepping relation R, defined using a more handy induction principle.
Inductive run_right {
A E:
Type} (
R :
A ->
list E ->
A ->
Prop) (
x :
A) :
list E ->
A ->
Prop :=
|
run_right_refl :
run_right R x nil x
|
run_right_step :
forall t1 t2 y z,
forall (
STEP:
R x t1 y)
(
RUN :
run_right R y t2 z),
run_right R x (
t1 ++
t2)
z.
We prove that both predicate of run and run_right coincide.
Lemma run_right_run :
forall A E (
R:
A ->
list E ->
A ->
Prop)
x t y,
run_right R x t y ->
run R x t y.
Proof.
induction 1 ;
intros.
-
apply run_refl.
-
econstructor 3;
eauto.
econstructor;
eauto.
Qed.
Lemma run_right_concat :
forall A E (
R:
A ->
list E ->
A ->
Prop)
x t1 y,
run_right R x t1 y ->
forall z t2,
run_right R y t2 z ->
run_right R x (
t1++
t2)
z.
Proof.
induction 1;
intros.
-
simpl;
auto.
-
eapply IHrun_right in H0;
eauto.
rewrite <-
app_assoc.
econstructor 2 ;
eauto.
Qed.
Lemma run_run_right :
forall A E (
R:
A ->
list E ->
A ->
Prop)
x t y,
run R x t y ->
run_right R x t y.
Proof.
induction 1 ;
intros.
-
replace t with (
t ++ [])
by apply app_nil_r.
eapply run_right_step;
eauto.
econstructor;
eauto.
-
econstructor;
eauto.
-
inv IHrun1.
+
simpl.
auto.
+
rewrite <-
app_assoc.
econstructor 2;
eauto.
eapply run_right_concat with (
y:=
y);
eauto.
Qed.