Commit 763467f9 authored by Asma Tafat's avatar Asma Tafat

eval_swap proof

parent a65e2836
......@@ -9,6 +9,7 @@ use import int.Int
use import int.MinMax
use import bool.Bool
use export list.List
use export list.Append
use map.Map as IdMap
(** types and values *)
......@@ -107,6 +108,7 @@ function get_vartype (i:ident) (pi:type_stack) : datatype =
| Cons (x,ty) r -> if x=i then ty else get_vartype i r
end
type type_env = IdMap.map mident datatype (* map global mutable variables to their type *)
function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i
......@@ -238,7 +240,7 @@ function eval_term (sigma:env) (pi:stack) (t:term) : value =
| Tderef id -> get_env id sigma
| Tbin t1 op t2 ->
eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
end
end
lemma eval_bool_term:
......@@ -293,7 +295,7 @@ lemma fresh_in_binop:
forall t t':term, op:operator, v:ident.
fresh_in_term v (mk_tbin t op t') ->
fresh_in_term v t /\ fresh_in_term v t'
lemma eval_msubst_term:
forall e:term, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_term v e ->
......@@ -373,12 +375,24 @@ lemma eval_same_var:
eval_fmla sigma (Cons (id,v1) (Cons (id,v2) pi)) f <->
eval_fmla sigma (Cons (id,v1) pi) f
lemma eval_swap_term_any:
forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
lemma eval_swap_term:
forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t =
eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t)
lemma eval_swap_any:
forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
lemma eval_swap:
forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
......
......@@ -14,6 +14,53 @@ Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
......@@ -394,6 +441,12 @@ Axiom eval_swap_term : forall (t:term) (sigma:(map mident value)) (pi:(list
(~ (id1 = id2)) -> ((eval_term sigma (Cons (id1, v1) (Cons (id2, v2) pi))
t) = (eval_term sigma (Cons (id2, v2) (Cons (id1, v1) pi)) t)).
Axiom eval_swap_any : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
(id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_fmla sigma
(infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi))) f) <-> (eval_fmla sigma
(infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi))) f)).
(* Why3 goal *)
Theorem eval_swap : forall (f:fmla),
match f with
......@@ -412,16 +465,30 @@ Theorem eval_swap : forall (f:fmla),
| (Fforall i d f1) => True
end.
destruct f; auto.
intros.
intros H sigma pi id1 id2 v1 v2 H1 H2.
simpl in *.
rewrite eval_swap_term; auto.
rewrite eval_swap_term in H2; auto.
destruct (ident_decide i id2).
(* i = id1*)
subst.
apply H in H2; auto.
destruct (ident_decide i id1).
(* i = id1*)
subst.
admit.
(* i <> id1*)
apply H; auto.
simpl in *.
rewrite eval_swap_term in H2; auto.
apply eval_same_var.
eval_same_var_term.
(* i <> id2*)
Qed.
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/programs/arm/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.2pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="z3"
name="Z3 smtv1"
version="2.2"/>
<file
name="../arm.mlw"
verified="false"
expanded="true">
<theory
name="WP M"
verified="false"
expanded="true">
<goal
name="WP_parameter insertion_sort"
expl="parameter insertion_sort"
sum="e4d2f23cb15a5aabb590bc249287e0dc"
proved="false"
expanded="false"
shape="Lamk arrayV0V3Lamk arrayV0V8iainfix <=V5c10Lamk arrayV0V13iainfix <agetV13V11agetV13ainfix -V11c1ainfix <V18V11Aainfix <=c0V11Aainfix <=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix <=V18V5Aainfix <=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V15ainfix +V12c1Fainfix <ainfix -c10V19ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix <=V19c11Aainfix <=c2V19Iainfix =V19ainfix +V5c1FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11FFFAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V6c45Aainfix =V7c9Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5FFFFAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4FFFF">
</goal>
</theory>
<theory
name="WP ARM"
verified="true"
expanded="true">
</theory>
<theory
name="WP InsertionSortExample"
verified="true"
expanded="false">
<goal
name="WP_parameter path_init_l2"
expl="normal postcondition"
sum="c2c5ea2cbb588e6cd95f3653c4f1f8fb"
proved="true"
expanded="false"
shape="ainv_l2V5V0V2Iainfix =V5amixfix [<-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter path_l2_exit"
expl="normal postcondition"
sum="aad12da07e3d91a9a0721b583a6decc3"
proved="true"
expanded="false"
shape="ainfix =V0c9Iainfix =V4aTrueNIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1FFF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment