Commit adeceeea authored by MARCHE Claude's avatar MARCHE Claude

preuve sem5 encore plus courtes

parent 6666b646
......@@ -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').
......@@ -282,13 +282,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 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(x:ident) (t:term) {struct t}: Prop :=
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 *)
......@@ -303,28 +325,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
......@@ -350,11 +350,7 @@ Theorem eval_msubst : forall (f:fmla),
| (Fforall i d f1) => True
end.
destruct f; auto.
simpl.
intros.
destruct H0 as (h1 & h2 & h3).
rewrite eval_msubst_term in H1; auto.
ae.
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').
......@@ -282,13 +282,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 *)
......@@ -303,28 +325,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
......@@ -335,6 +335,9 @@ Axiom eval_msubst : forall (f:fmla) (sigma:(map mident value)) (pi:(list
((eval_fmla sigma pi (msubst f x v)) <-> (eval_fmla (set sigma x
(get_stack v pi)) pi f)).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem eval_swap_term : forall (t:term),
match t with
......@@ -348,46 +351,16 @@ Theorem eval_swap_term : forall (t:term),
| (Tderef m) => True
| (Tbin t1 o t2) => True
end.
destruct t;auto.
intros.
simpl.
intros; simpl.
induction l.
(* l = Nil *)
simpl.
destruct (ident_decide i id1).
subst.
pattern (get_stack id1 (Cons (id1, v1) (Cons (id2, v2) pi)));
rewrite get_stack_eq.
rewrite get_stack_neq; auto.
rewrite get_stack_eq; auto.
(* i <> id1 *)
destruct (ident_decide i id2).
(* i = id2 *)
subst.
pattern (get_stack id2 (Cons (id2, v2) (Cons (id1, v1) pi)));
rewrite get_stack_eq.
rewrite get_stack_neq; auto.
rewrite get_stack_eq; auto.
(* i <> id2 *)
rewrite get_stack_neq; auto.
rewrite get_stack_neq; auto.
rewrite get_stack_neq; auto.
rewrite get_stack_neq; auto.
ae.
(* Cons *)
simpl.
destruct a.
destruct (ident_decide i0 i).
(* i = i0 *)
subst.
pattern (get_stack i
(Cons (i, v) (infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi)))));
rewrite get_stack_eq; auto.
rewrite get_stack_eq; auto.
(* i <> i0 *)
rewrite get_stack_neq; auto.
rewrite get_stack_neq; auto.
destruct (ident_decide i0 i); ae.
Qed.
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