Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 65af15a2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

proofs improved again

parent 38628bc5
......@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Sassert f) sigma pi Sskip)
| one_step_while_true : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi
inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
value)%type)) (cond:term) (inv:fmla) (body:stmt), ((eval_fmla sigma pi
inv) /\ ((eval_term sigma pi cond) = (Vbool true))) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body)))
| one_step_while_false : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
(eval_fmla sigma pi inv) -> (((eval_term sigma pi
cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip)).
((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip).
(* Why3 assumption *)
Inductive many_steps : (map mident value) -> (list (ident* value)%type)
......@@ -230,7 +230,7 @@ Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident
(0%Z <= n)%Z.
(* Why3 assumption *)
Definition reducible(sigma:(map mident value)) (pi:(list (ident*
Definition reductible(sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt): Prop := exists sigma':(map mident value),
exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s
sigma' pi' s').
......@@ -280,9 +280,9 @@ Inductive type_term : (map mident datatype) -> (list (ident* datatype)%type)
(type_term sigma pi (Tderef v) ty)
| Type_bin : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (t1:term) (t2:term) (op:operator) (ty1:datatype)
(ty2:datatype) (ty:datatype), (type_term sigma pi t1 ty1) ->
((type_term sigma pi t2 ty2) -> ((type_operator op ty1 ty2 ty) ->
(type_term sigma pi (Tbin t1 op t2) ty))).
(ty2:datatype) (ty:datatype), ((type_term sigma pi t1 ty1) /\
((type_term sigma pi t2 ty2) /\ (type_operator op ty1 ty2 ty))) ->
(type_term sigma pi (Tbin t1 op t2) ty).
(* Why3 assumption *)
Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
......@@ -291,8 +291,8 @@ Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
datatype)%type)) (t:term), (type_term sigma pi t TYbool) ->
(type_fmla sigma pi (Fterm t))
| Type_conj : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (f1:fmla) (f2:fmla), (type_fmla sigma pi f1) ->
((type_fmla sigma pi f2) -> (type_fmla sigma pi (Fand f1 f2)))
datatype)%type)) (f1:fmla) (f2:fmla), ((type_fmla sigma pi f1) /\
(type_fmla sigma pi f2)) -> (type_fmla sigma pi (Fand f1 f2))
| Type_neg : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (f:fmla), (type_fmla sigma pi f) -> (type_fmla sigma
pi (Fnot f))
......@@ -303,15 +303,9 @@ Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
datatype)%type)) (x:ident) (t:term) (f:fmla) (ty:datatype),
(type_term sigma pi t ty) -> ((type_fmla sigma (Cons (x, ty) pi) f) ->
(type_fmla sigma pi (Flet x t f)))
| Type_forall1 : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYint)
pi) f) -> (type_fmla sigma pi (Fforall x TYint f))
| Type_forall2 : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYbool)
pi) f) -> (type_fmla sigma pi (Fforall x TYbool f))
| Type_forall3 : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYunit)
pi) f) -> (type_fmla sigma pi (Fforall x TYunit f)).
| Type_forall : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla) (ty:datatype), (type_fmla sigma
(Cons (x, ty) pi) f) -> (type_fmla sigma pi (Fforall x ty f)).
(* Why3 assumption *)
Inductive type_stmt : (map mident datatype) -> (list (ident* datatype)%type)
......@@ -333,36 +327,29 @@ Inductive type_stmt : (map mident datatype) -> (list (ident* datatype)%type)
datatype)%type)) (p:fmla), (type_fmla sigma pi p) -> (type_stmt sigma
pi (Sassert p))
| Type_while : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (guard:term) (body:stmt) (inv:fmla), (type_fmla sigma
pi inv) -> ((type_term sigma pi guard TYbool) -> ((type_stmt sigma pi
body) -> (type_stmt sigma pi (Swhile guard inv body)))).
datatype)%type)) (cond:term) (body:stmt) (inv:fmla), (type_fmla sigma
pi inv) -> ((type_term sigma pi cond TYbool) -> ((type_stmt sigma pi
body) -> (type_stmt sigma pi (Swhile cond inv body)))).
(* Why3 assumption *)
Inductive compatible : datatype -> value -> Prop :=
| Compatible_bool : forall (b:bool), (compatible TYbool (Vbool b))
| Compatible_int : forall (n:Z), (compatible TYint (Vint n))
| Compatible_void : (compatible TYunit Vvoid).
Definition compatible_env(sigma:(map mident value)) (sigmat:(map mident
datatype)) (pi:(list (ident* value)%type)) (pit:(list (ident*
datatype)%type)): Prop := (forall (id:mident), ((type_value (get sigma
id)) = (get sigmat id))) /\ forall (id:ident), ((type_value (get_stack id
pi)) = (get_vartype id pit)).
(* Why3 assumption *)
Definition existe_compatible(ty:datatype) (v:value): Prop :=
match ty with
Axiom type_inversion : forall (v:value),
match (type_value v) with
| TYbool => exists b:bool, (v = (Vbool b))
| TYint => exists n:Z, (v = (Vint n))
| TYunit => (v = Vvoid)
end.
(* Why3 assumption *)
Definition compatible_env(sigma:(map mident value)) (sigmat:(map mident
datatype)) (pi:(list (ident* value)%type)) (pit:(list (ident*
datatype)%type)): Prop := (forall (id:mident), (compatible (get sigmat id)
(get sigma id))) /\ forall (id:ident), (compatible (get_vartype id pit)
(get_stack id pi)).
Axiom eval_type_term : forall (t:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident*
datatype)%type)) (ty:datatype), (compatible_env sigma sigmat pi pit) ->
((type_term sigmat pit t ty) -> (existe_compatible ty (eval_term sigma pi
t))).
((type_term sigmat pit t ty) -> ((type_value (eval_term sigma pi
t)) = ty)).
Axiom type_preservation : forall (s1:stmt) (s2:stmt) (sigma1:(map mident
value)) (sigma2:(map mident value)) (pi1:(list (ident* value)%type))
......@@ -419,13 +406,35 @@ 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))).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (x:mident) (v:ident),
match t with
| ((Tvalue _)|(Tvar _)) => ((msubst_term t x v) = t)
| (Tderef y) => ((x = y) -> ((msubst_term t x v) = (Tvar v))) /\
((~ (x = y)) -> ((msubst_term t x v) = t))
| (Tbin t1 op t2) => ((msubst_term t x v) = (Tbin (msubst_term t1 x v) op
(msubst_term t2 x v)))
end.
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (msubst_term e x v))
| (Fand f1 f2) => (Fand (msubst f1 x v) (msubst f2 x v))
| (Fnot f1) => (Fnot (msubst f1 x v))
| (Fimplies f1 f2) => (Fimplies (msubst f1 x v) (msubst f2 x v))
| (Flet y t f1) => (Flet y (msubst_term t x v) (msubst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
(* Why3 assumption *)
Fixpoint fresh_in_term(id:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tvar i) => ~ (id = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
| (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
end.
(* Why3 assumption *)
......@@ -440,28 +449,6 @@ Fixpoint fresh_in_fmla(id:ident) (f:fmla) {struct f}: Prop :=
| (Fforall y ty f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
end.
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
match t with
| ((Tvalue _)|(Tvar _)) => ((msubst_term t r v) = t)
| (Tderef x) => ((r = x) -> ((msubst_term t r v) = (Tvar v))) /\
((~ (r = x)) -> ((msubst_term t r v) = t))
| (Tbin t1 op t2) => ((msubst_term t r v) = (Tbin (msubst_term t1 r v) op
(msubst_term t2 r v)))
end.
(* Why3 assumption *)
Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (msubst_term e x v))
| (Fand f1 f2) => (Fand (msubst f1 x v) (msubst f2 x v))
| (Fnot f1) => (Fnot (msubst f1 x v))
| (Fimplies f1 f2) => (Fimplies (msubst f1 x v) (msubst f2 x v))
| (Flet y t f1) => (Flet y (msubst_term t x v) (msubst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
Axiom eval_msubst_term : forall (e:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:mident) (v:ident), (fresh_in_term v e) ->
((eval_term sigma pi (msubst_term e x v)) = (eval_term (set sigma x
......@@ -488,10 +475,9 @@ Axiom eval_term_change_free : forall (t:term) (sigma:(map mident value))
(pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_term id
t) -> ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
Axiom eval_change_free : forall (f:fmla) (id:ident) (v:value),
(fresh_in_fmla id f) -> forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)), (eval_fmla sigma (Cons (id, v) pi) f) <-> (eval_fmla sigma
pi f).
Axiom eval_change_free : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id:ident) (v:value), (fresh_in_fmla id f) ->
((eval_fmla sigma (Cons (id, v) pi) f) <-> (eval_fmla sigma pi f)).
Parameter fresh_from: fmla -> ident.
......@@ -503,10 +489,16 @@ Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
Axiom abstract_effects_monotonic : forall (s:stmt) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma pi f) -> forall (sigma1:(map mident value)) (pi1:(list
(ident* value)%type)), (eval_fmla sigma1 pi1 (abstract_effects s f)).
Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
(sigma:(map mident value)) (pi:(list (ident* value)%type)),
((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
(abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
q))).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
......@@ -530,6 +522,9 @@ Axiom abstract_effects_writes : forall (sigma:(map mident value)) (pi:(list
Axiom monotonicity : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> (valid_fmla (Fimplies (wp s p) (wp s q))).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem distrib_conj : forall (s:stmt),
match s with
......@@ -544,7 +539,8 @@ Theorem distrib_conj : forall (s:stmt),
| (Swhile t f s1) => True
end.
destruct s; auto.
unfold valid_fmla; simpl.
unfold valid_fmla; simpl; ae.
(*
intros sigma pi p q.
intros.
assert (fresh_in_fmla (fresh_from (Fand p q)) (Fand p q)).
......@@ -570,6 +566,7 @@ apply fresh_from_fmla; auto.
apply fresh_from_fmla; auto.
apply fresh_from_fmla; auto.
apply fresh_from_fmla; auto.
*)
Qed.
......@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Sassert f) sigma pi Sskip)
| one_step_while_true : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi
inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
value)%type)) (cond:term) (inv:fmla) (body:stmt), ((eval_fmla sigma pi
inv) /\ ((eval_term sigma pi cond) = (Vbool true))) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body)))
| one_step_while_false : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
(eval_fmla sigma pi inv) -> (((eval_term sigma pi
cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip)).
((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip).
(* Why3 assumption *)
Inductive many_steps : (map mident value) -> (list (ident* value)%type)
......@@ -280,9 +280,9 @@ Inductive type_term : (map mident datatype) -> (list (ident* datatype)%type)
(type_term sigma pi (Tderef v) ty)
| Type_bin : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (t1:term) (t2:term) (op:operator) (ty1:datatype)
(ty2:datatype) (ty:datatype), (type_term sigma pi t1 ty1) ->
((type_term sigma pi t2 ty2) -> ((type_operator op ty1 ty2 ty) ->
(type_term sigma pi (Tbin t1 op t2) ty))).
(ty2:datatype) (ty:datatype), ((type_term sigma pi t1 ty1) /\
((type_term sigma pi t2 ty2) /\ (type_operator op ty1 ty2 ty))) ->
(type_term sigma pi (Tbin t1 op t2) ty).
(* Why3 assumption *)
Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
......@@ -291,8 +291,8 @@ Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
datatype)%type)) (t:term), (type_term sigma pi t TYbool) ->
(type_fmla sigma pi (Fterm t))
| Type_conj : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (f1:fmla) (f2:fmla), (type_fmla sigma pi f1) ->
((type_fmla sigma pi f2) -> (type_fmla sigma pi (Fand f1 f2)))
datatype)%type)) (f1:fmla) (f2:fmla), ((type_fmla sigma pi f1) /\
(type_fmla sigma pi f2)) -> (type_fmla sigma pi (Fand f1 f2))
| Type_neg : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (f:fmla), (type_fmla sigma pi f) -> (type_fmla sigma
pi (Fnot f))
......@@ -303,15 +303,9 @@ Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
datatype)%type)) (x:ident) (t:term) (f:fmla) (ty:datatype),
(type_term sigma pi t ty) -> ((type_fmla sigma (Cons (x, ty) pi) f) ->
(type_fmla sigma pi (Flet x t f)))
| Type_forall1 : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYint)
pi) f) -> (type_fmla sigma pi (Fforall x TYint f))
| Type_forall2 : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYbool)
pi) f) -> (type_fmla sigma pi (Fforall x TYbool f))
| Type_forall3 : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYunit)
pi) f) -> (type_fmla sigma pi (Fforall x TYunit f)).
| Type_forall : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (x:ident) (f:fmla) (ty:datatype), (type_fmla sigma
(Cons (x, ty) pi) f) -> (type_fmla sigma pi (Fforall x ty f)).
(* Why3 assumption *)
Inductive type_stmt : (map mident datatype) -> (list (ident* datatype)%type)
......@@ -333,16 +327,9 @@ Inductive type_stmt : (map mident datatype) -> (list (ident* datatype)%type)
datatype)%type)) (p:fmla), (type_fmla sigma pi p) -> (type_stmt sigma
pi (Sassert p))
| Type_while : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (guard:term) (body:stmt) (inv:fmla), (type_fmla sigma
pi inv) -> ((type_term sigma pi guard TYbool) -> ((type_stmt sigma pi
body) -> (type_stmt sigma pi (Swhile guard inv body)))).
Axiom type_inversion : forall (v:value),
match (type_value v) with
| TYbool => exists b:bool, (v = (Vbool b))
| TYint => exists n:Z, (v = (Vint n))
| TYunit => (v = Vvoid)
end.
datatype)%type)) (cond:term) (body:stmt) (inv:fmla), (type_fmla sigma
pi inv) -> ((type_term sigma pi cond TYbool) -> ((type_stmt sigma pi
body) -> (type_stmt sigma pi (Swhile cond inv body)))).
(* Why3 assumption *)
Definition compatible_env(sigma:(map mident value)) (sigmat:(map mident
......@@ -351,6 +338,13 @@ Definition compatible_env(sigma:(map mident value)) (sigmat:(map mident
id)) = (get sigmat id))) /\ forall (id:ident), ((type_value (get_stack id
pi)) = (get_vartype id pit)).
Axiom type_inversion : forall (v:value),
match (type_value v) with
| TYbool => exists b:bool, (v = (Vbool b))
| TYint => exists n:Z, (v = (Vint n))
| TYunit => (v = Vvoid)
end.
Axiom eval_type_term : forall (t:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident*
datatype)%type)) (ty:datatype), (compatible_env sigma sigmat pi pit) ->
......@@ -412,13 +406,35 @@ 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))).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (x:mident) (v:ident),
match t with
| ((Tvalue _)|(Tvar _)) => ((msubst_term t x v) = t)
| (Tderef y) => ((x = y) -> ((msubst_term t x v) = (Tvar v))) /\
((~ (x = y)) -> ((msubst_term t x v) = t))
| (Tbin t1 op t2) => ((msubst_term t x v) = (Tbin (msubst_term t1 x v) op
(msubst_term t2 x v)))
end.
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (msubst_term e x v))
| (Fand f1 f2) => (Fand (msubst f1 x v) (msubst f2 x v))
| (Fnot f1) => (Fnot (msubst f1 x v))
| (Fimplies f1 f2) => (Fimplies (msubst f1 x v) (msubst f2 x v))
| (Flet y t f1) => (Flet y (msubst_term t x v) (msubst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
(* Why3 assumption *)
Fixpoint fresh_in_term(id:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tvar i) => ~ (id = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
| (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
end.
(* Why3 assumption *)
......@@ -433,28 +449,6 @@ Fixpoint fresh_in_fmla(id:ident) (f:fmla) {struct f}: Prop :=
| (Fforall y ty f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
end.
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
match t with
| ((Tvalue _)|(Tvar _)) => ((msubst_term t r v) = t)
| (Tderef x) => ((r = x) -> ((msubst_term t r v) = (Tvar v))) /\
((~ (r = x)) -> ((msubst_term t r v) = t))
| (Tbin t1 op t2) => ((msubst_term t r v) = (Tbin (msubst_term t1 r v) op
(msubst_term t2 r v)))
end.
(* Why3 assumption *)
Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (msubst_term e x v))
| (Fand f1 f2) => (Fand (msubst f1 x v) (msubst f2 x v))
| (Fnot f1) => (Fnot (msubst f1 x v))
| (Fimplies f1 f2) => (Fimplies (msubst f1 x v) (msubst f2 x v))
| (Flet y t f1) => (Flet y (msubst_term t x v) (msubst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
Axiom eval_msubst_term : forall (e:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:mident) (v:ident), (fresh_in_term v e) ->
((eval_term sigma pi (msubst_term e x v)) = (eval_term (set sigma x
......@@ -481,10 +475,9 @@ Axiom eval_term_change_free : forall (t:term) (sigma:(map mident value))
(pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_term id
t) -> ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
Axiom eval_change_free : forall (f:fmla) (id:ident) (v:value),
(fresh_in_fmla id f) -> forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)), (eval_fmla sigma (Cons (id, v) pi) f) <-> (eval_fmla sigma
pi f).
Axiom eval_change_free : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id:ident) (v:value), (fresh_in_fmla id f) ->
((eval_fmla sigma (Cons (id, v) pi) f) <-> (eval_fmla sigma pi f)).
Parameter fresh_from: fmla -> ident.
......@@ -496,17 +489,17 @@ Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
(sigma:(map mident value)) (pi:(list (ident* value)%type)),
((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
(abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
q))).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
match s with
......@@ -530,6 +523,7 @@ Axiom monotonicity : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> (valid_fmla (Fimplies (wp s p) (wp s q))).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 5.
(* Why3 goal *)
Theorem distrib_conj : forall (s:stmt),
......@@ -551,18 +545,12 @@ Theorem distrib_conj : forall (s:stmt),
| (Swhile t f s1) => True
end.
destruct s; auto.
intros H1 H2 sigma pi p q (H3 & H4).
simpl in *.
simpl; intros H1 H2 sigma pi p q (H3 & H4).
assert (H: valid_fmla
(Fimplies (Fand (wp s2 p) (wp s2 q)) (wp s2 (Fand p q)))).
unfold valid_fmla ; simpl.
intros sigma' pi' (H5 & H6).
apply H1; auto; clear H1.
unfold valid_fmla ; simpl; ae.
generalize (monotonicity s1 _ _ H).
clear H; intro H.
unfold valid_fmla in H.
simpl in H.
why3 "alt-ergo" timelimit 5.
unfold valid_fmla; simpl; ae.
Qed.
......@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Sassert f) sigma pi Sskip)
| one_step_while_true : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi
inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
value)%type)) (cond:term) (inv:fmla) (body:stmt), ((eval_fmla sigma pi
inv) /\ ((eval_term sigma pi cond) = (Vbool true))) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body)))
| one_step_while_false : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
(eval_fmla sigma pi inv) -> (((eval_term sigma pi
cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip)).
((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip).
(* Why3 assumption *)
Inductive many_steps : (map mident value) -> (list (ident* value)%type)
......@@ -230,7 +230,7 @@ Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident
(0%Z <= n)%Z.
(* Why3 assumption *)
Definition reducible(sigma:(map mident value)) (pi:(list (ident*
Definition reductible(sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt): Prop := exists sigma':(map mident value),
exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s
sigma' pi' s').
......@@ -280,9 +280,9 @@ Inductive type_term : (map mident datatype) -> (list (ident* datatype)%type)
(type_term sigma pi (Tderef v) ty)
| Type_bin : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (t1:term) (t2:term) (op:operator) (ty1:datatype)
(ty2:datatype) (ty:datatype), (type_term sigma pi t1 ty1) ->
((type_term sigma pi t2 ty2) -> ((type_operator op ty1 ty2 ty) ->
(type_term sigma pi (Tbin t1 op t2) ty))).
(ty2:datatype) (ty:datatype), ((type_term sigma pi t1 ty1) /\
((type_term sigma pi t2 ty2) /\ (type_operator op ty1 ty2 ty))) ->
(type_term sigma pi (Tbin t1 op t2) ty).
(* Why3 assumption *)