Mefresa.Dec.FunctionalSpec
Writting a decision procedure requires to have computational
versions of some of the involved predicates. In this module
we define such functions and prove them correct, i.e., they
return true (the one in boolean) whenever the predicates evaluates to
True (the one in Prop), and false for False.
Function not_in_bool id lc : bool :=
match lc with
nil => true
| Component id' _ _ _ _ _ _ :: r =>
if (id == id')%id then false else not_in_bool id r
end.
Lemma not_in_bool_correctness:
forall id lc, not_in_bool id lc = true <-> not_in_l id lc.
Proof.
split; intro.
Case "Function Entails Predicate".
functional induction not_in_bool id lc; auto; try congruence.
assert (not_in_l id r); auto.
clear IHb.
apply NotInStep with (a:=Component id' _x _x0 _x1 _x2 _x3 _x4 ) (r:=r); auto.
simpl.
replace (id' == id) with (id == id'); auto.
apply beq_ident_symmetry; auto.
Case "Predicate Entails Function".
induction lc; auto.
inversion H; inversion H0; subst.
clear H0.
unfold not_in_bool.
destruct a0. simpl in *.
replace (id == i) with (i == id).
rewrite H1. auto.
apply beq_ident_symmetry; auto.
Qed.
Hint Resolve not_in_bool_correctness.
Function dec_unique_ids (lc:list component) :=
match lc with
nil => true
| Component id _ _ _ _ _ _ :: r =>
if (beq_bool (not_in_bool id r) false) then false else dec_unique_ids r
end.
Lemma dec_unique_ids_correctness:
forall lc,
dec_unique_ids lc = true <-> unique_ids lc.
Proof.
split; intro.
Case "Function Entails Predicate".
functional induction dec_unique_ids lc; auto; try congruence.
assert (unique_ids r); auto.
clear IHb.
apply Unique_Step with (c:=Component id _x _x0 _x1 _x2 _x3 _x4) (r:=r); auto.
simpl.
assert ((not_in_bool id r) = true).
destruct ((not_in_bool id r)); auto.
clear e0.
apply not_in_bool_correctness; auto.
Case "Predicate Entails Function".
induction lc; auto.
inversion H; inversion H0; subst.
clear H0.
unfold dec_unique_ids.
destruct c; simpl in *.
replace (not_in_bool i r) with true; simpl; auto.
symmetry.
apply not_in_bool_correctness; auto.
Qed.
Hint Resolve dec_unique_ids_correctness.
Function not_in_l_pairs_bool id v li : bool :=
match li with
nil => true
| Interface id' sig p v' ro f ct cd :: r =>
if (id' == id) && (v' == v)%vis then false else not_in_l_pairs_bool id v r
end.
Lemma not_in_l_pairs_bool_correctness:
forall id v li, not_in_l_pairs_bool id v li = true <-> not_in_l_pairs id v li.
Proof.
split; intro.
Case "Function entails Predicate".
functional induction not_in_l_pairs_bool id v li.
SCase "1/3".
apply NotInPair_Nil; auto.
SCase "2/3".
congruence.
SCase "3/3".
intuition.
apply NotInPairStep with (int:=Interface id' sig p v' ro f ct cd) (r:=r); auto.
Case "Predicate entails Function".
induction li.
SCase "Empty interfaces".
refl.
SCase "At least one interface".
assert (not_in_l_pairs_bool id v li = true).
apply IHli.
inversion H; inversion H0; auto.
clear IHli.
inversion H; inversion H1; subst. clear H1.
unfold not_in_l_pairs_bool.
destruct int; simpl in *.
rewrite H2; auto.
Qed.
Hint Resolve not_in_l_pairs_bool_correctness.
Function dec_interfaces li : bool :=
match li with
nil => true
| Interface id sig p v ro f ct cd :: r =>
if (beq_bool (not_in_l_pairs_bool id v r) false) then false else dec_interfaces r
end.
Lemma dec_interfaces_correctness:
forall li,
dec_interfaces li = true <-> well_formed_interfaces li.
Proof.
intros.
split; intro.
Case "Function entails Predicate".
functional induction dec_interfaces li; auto.
SCase "1/2".
congruence.
SCase "2/2".
apply WellFormedInterfaces_Step with
(i:=Interface id sig p v ro f ct cd) (r:=r); auto.
apply UniquePairs_Step with (int:=Interface id sig p v ro f ct cd) (r:=r); auto.
SSCase "1/2".
simpl.
assert (not_in_l_pairs_bool id v r = true).
destruct (not_in_l_pairs_bool id v r); auto.
apply not_in_l_pairs_bool_correctness; auto.
SSCase "2/2".
intuition.
inversion H0; subst; auto.
apply UniquePairs_Base; auto.
Case "Predicate entails Function".
induction li; simpl; auto.
inversion H; inversion H0; subst. clear H0.
destruct i.
intuition.
rewrite H0.
assert ((not_in_l_pairs_bool i v r) = true).
apply not_in_l_pairs_bool_correctness.
inversion H1; inversion H3; subst; simpl in *; auto.
rewrite H3; refl.
Qed.
Hint Resolve dec_interfaces_correctness.
The above functions and proofs establish the required functional counterparts
for the decidability of interfaces' well_formedness. For instance, as of now
we could extract a certified OCaml program that would decide on the
well-formedness of interfaces as so:
Recursive Extraction dec_interfaces.
Into Bindings
Function normal_binding_bool
(idC1 idI1 idC2 idI2 : ident) (lc : list component) : bool :=
match lc [idC1] with
| Some c1 =>
match lc [idC2] with
| Some c2 =>
match ((c1 ->interfaces)%comp [idI1, External])%int with
| Some i =>
match ((c2 ->interfaces)%comp [idI2, External])%int with
| Some i' => ((i ->role)%int == Client)%role &&
((i' ->role)%int == Server)%role
| None => false
end
| None => false
end
| None => false
end
| None => false
end.
Function import_binding_bool
(idI idC idI' : ident) (lc : list component) (li : list interface) : bool :=
match lc [idC] with
| Some c' =>
match (li [idI, Internal])%int with
| Some i =>
match ((c' ->interfaces)%comp [idI', External])%int with
| Some i' => ((i ->role)%int == Server)%role &&
((i' ->role)%int == Client)%role
| None => false
end
| None => false
end
| None => false
end.
Function export_binding_bool
(idI idC idI' : ident) (lc : list component) (li : list interface) : bool :=
match lc [idC] with
| Some c' =>
match (li [idI, Internal])%int with
| Some i =>
match ((c' ->interfaces)%comp [idI', External])%int with
| Some i' => ((i ->role)%int == Client)%role &&
((i' ->role)%int == Server)%role
| None => false
end
| None => false
end
| None => false
end.
Function valid_binding_bool
(b : binding) (lc : list component) (li : list interface) : bool :=
match b with
| Normal _ idC1 idI1 idC2 idI2 => normal_binding_bool idC1 idI1 idC2 idI2 lc
| Export _ idI idC idI' => export_binding_bool idI idC idI' lc li
| Import _ idI idC idI' => import_binding_bool idI idC idI' lc li
end.
Require Import Coq.Bool.Bool.
Lemma valid_bindings_correctness:
forall b lc li,
valid_binding_bool b lc li = true <-> valid_binding b lc li.
Proof.
split; intro.
Case "Function Entails Predicate". Focus.
destruct b; simpl in *.
SCase "Normal Binding". Focus.
functional induction normal_binding_bool i i0 i1 i2 lc;
unfold normal_binding;
try (rewrite e; rewrite e0; try rewrite e1; try rewrite e2);
try congruence.
rewrite andb_true_iff in H; destruct H.
rewrite role_bool_prop in H;
rewrite role_bool_prop in H0; auto.
SCase "Export Binding".
functional induction export_binding_bool i i0 i1 lc li;
unfold export_binding;
try (rewrite e; rewrite e0; try rewrite e1; try rewrite e2);
try congruence.
rewrite andb_true_iff in H; destruct H.
rewrite role_bool_prop in H;
rewrite role_bool_prop in H0; auto.
SCase "import Binding".
functional induction import_binding_bool i i0 i1 lc li;
unfold import_binding;
try (rewrite e; rewrite e0; try rewrite e1; try rewrite e2);
try congruence.
rewrite andb_true_iff in H; destruct H.
rewrite role_bool_prop in H;
rewrite role_bool_prop in H0; auto.
Case "Predicate Entails Function".
destruct b; simpl in *.
SCase "Normal Binding".
functional induction normal_binding i i0 i1 i2 lc li;
unfold normal_binding_bool;
try (rewrite e; rewrite e0; try rewrite e1; try rewrite e2).
destruct H.
rewrite andb_true_iff.
split; rewrite role_bool_prop; auto.
inversion H. inversion H.
SCase "Export Binding".
functional induction export_binding i i0 i1 lc li;
unfold export_binding_bool;
try (rewrite e; rewrite e0; try rewrite e1; try rewrite e2).
inversion H.
destruct H.
rewrite andb_true_iff.
split; rewrite role_bool_prop; auto.
inversion H.
SCase "Import Binding".
functional induction import_binding i i0 i1 lc li;
unfold import_binding_bool;
try (rewrite e; rewrite e0; try rewrite e1; try rewrite e2).
inversion H.
destruct H.
rewrite andb_true_iff.
split; rewrite role_bool_prop; auto.
inversion H.
Qed.
Hint Resolve valid_bindings_correctness.
Function dec_bindings (lb:list binding)
(lc:list component)
(li:list interface) : bool :=
match lb with
nil => true
| b :: r => (valid_binding_bool b lc li) && dec_bindings r lc li
end.
Lemma dec_bindings_correctness:
forall lb lc li,
dec_bindings lb lc li = true <-> well_formed_bindings lb lc li.
Proof.
split; intro.
Case "Function Entails Predicate".
functional induction dec_bindings lb lc li; auto.
rewrite andb_true_iff in H; destruct H.
assert (well_formed_bindings r lc li); auto.
clear IHb.
intro; intro.
destruct H2; subst.
SCase "1/2".
apply valid_bindings_correctness; auto.
SCase "2/2".
apply H1; auto.
Case "Predicate Entails Function".
induction lb;auto.
assert (dec_bindings lb lc li = true).
apply IHlb.
intro; intros.
apply H.
right; auto.
unfold dec_bindings.
rewrite andb_true_iff; split; auto.
apply valid_bindings_correctness.
apply H.
left; auto.
Qed.
In the same way we did it for the interfaces we also made the
required steps for the bindings elements. Extracting a certified
OCaml program would be achieved as follows:
Recursive Extraction dec_bindings.