Commit a815ce53 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

rajout lemma appen_nil_l et cons_append

parent 43d448bf
......@@ -408,6 +408,12 @@ theory FreshVariables
use import SemOp
use import list.Append
lemma Cons_append: forall a: 'a, l1 l2: list 'a.
Cons a (l1 ++ l2) = (Cons a l1) ++ l2
lemma Append_nil_l:
forall l: list 'a. Nil ++ l = l
(** substitution of a reference [x] by a logic variable [v]
warning: proper behavior only guaranted if [v] is fresh *)
......@@ -605,7 +611,7 @@ fresh_in_fmla (fresh_from f) f
alors
sigma, pi |= f
*)
axiom abstract_effects_generalize :
axiom abstract_effects_specialize :
forall sigma:env, pi:stack, s:stmt, f:fmla.
eval_fmla sigma pi (abstract_effects s f) ->
eval_fmla sigma pi f
......
......@@ -282,15 +282,22 @@ 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 Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
l2)).
Axiom Append_nil_l : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl (Nil :(list a)) l) = l).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
Axiom msubst_term_def : forall (t:term) (x: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)))
| ((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 *)
......@@ -305,12 +312,12 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
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 *)
......@@ -370,14 +377,9 @@ Theorem eval_change_free : forall (f:fmla),
| (Fforall i d f1) => True
end.
destruct f; auto.
simpl; intros H sigma pi id v (h1 & h2 & h3).
simpl; intros H sigma pi id v (h1 & h2 & h3) h.
rewrite eval_term_change_free; auto.
assert (eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi))) f =
eval_fmla sigma
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi)) f);
auto.
rewrite <- H0; clear H0.
pattern (Cons (i, eval_term sigma pi t) (Cons (id, v) pi)); rewrite <- Append_nil_l.
rewrite eval_swap; auto.
apply H; auto.
Qed.
......
......@@ -282,15 +282,22 @@ 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 Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
l2)).
Axiom Append_nil_l : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl (Nil :(list a)) l) = l).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
Axiom msubst_term_def : forall (t:term) (x: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)))
| ((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 *)
......@@ -305,12 +312,12 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
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 *)
......@@ -369,12 +376,7 @@ Theorem eval_change_free : forall (f:fmla),
destruct f; auto.
simpl; intros H sigma pi id v (h1 & h2 & h3).
rewrite eval_term_change_free; auto.
assert (h : eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi))) f =
eval_fmla sigma
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi)) f);
auto.
rewrite <- h.
pattern (Cons (i, eval_term sigma pi t) (Cons (id, v) pi)); rewrite <- Append_nil_l.
rewrite eval_swap; auto.
apply H; auto.
Qed.
......
......@@ -282,15 +282,22 @@ 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 Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
l2)).
Axiom Append_nil_l : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl (Nil :(list a)) l) = l).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
Axiom msubst_term_def : forall (t:term) (x: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)))
| ((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 *)
......@@ -305,12 +312,12 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
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 *)
......@@ -393,12 +400,7 @@ simpl; apply H; auto.
(* TYbool*)
intro b.
assert (h: eval_fmla sigma (Cons (i, Vbool b) (Cons (id, v) pi)) f); auto.
assert
(eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, Vbool b) (Cons (id, v) pi))) f =
eval_fmla sigma (Cons (i, Vbool b) (Cons (id, v) pi)) f); auto.
rewrite <- H0.
pattern (Cons (i, Vbool b) (Cons (id, v) pi)); rewrite <- Append_nil_l.
rewrite eval_swap; auto.
simpl; apply H; auto.
Qed.
......
......@@ -282,15 +282,22 @@ 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 Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
l2)).
Axiom Append_nil_l : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl (Nil :(list a)) l) = l).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
Axiom msubst_term_def : forall (t:term) (x: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)))
| ((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 *)
......@@ -305,12 +312,12 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
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 *)
......@@ -393,9 +400,7 @@ apply H1.
(* Vbool *)
intro b.
rewrite <- (H _ _ id v); auto.
replace (Cons (id, v) (Cons (i, Vbool b) pi)) with
(infix_plpl (Nil : (list (ident*value)))
(Cons (id, v) (Cons (i, Vbool b) pi))) by auto.
pattern (Cons (id, v) (Cons (i, Vbool b) pi)); rewrite <- Append_nil_l.
rewrite eval_swap; auto.
apply H1.
Qed.
......
......@@ -282,6 +282,13 @@ 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 Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
l2)).
Axiom Append_l_nil1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (x:mident) (v:ident),
......@@ -367,16 +374,13 @@ Theorem eval_swap : forall (f:fmla),
end.
destruct f; auto.
simpl; intros.
assert (h: forall (l1 l2 : list (ident*value)) (a : (ident*value)),
(Cons a (infix_plpl l1 l2)) = (infix_plpl (Cons a l1) l2))
by (simpl; auto).
destruct d.
(* Void *)
ae.
(* Int *)
intros; rewrite h; ae.
intro; rewrite Cons_append; ae.
(* Bool *)
intros; rewrite h; ae.
intro; rewrite Cons_append; ae.
Qed.
......@@ -282,6 +282,13 @@ 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 Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a) (l1:(list
a)) (l2:(list a)), ((Cons a1 (infix_plpl l1 l2)) = (infix_plpl (Cons a1 l1)
l2)).
Axiom Append_l_nil1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (x:mident) (v:ident),
......@@ -367,16 +374,13 @@ Theorem eval_swap : forall (f:fmla),
end.
destruct f; auto.
intros.
assert (h: forall (l1 l2 : list (ident*value)) (a : (ident*value)),
(Cons a (infix_plpl l1 l2)) = (infix_plpl (Cons a l1) l2))
by (simpl; auto).
destruct d; simpl.
(* Void *)
ae.
(* Int *)
intros; rewrite h; ae.
intro; rewrite Cons_append; ae.
(* Bool *)
intros; rewrite h; ae.
intro; rewrite Cons_append; ae.
Qed.
......@@ -539,7 +539,7 @@ Theorem distrib_conj : forall (s:stmt),
| (Swhile t f s1) => True
end.
destruct s; auto.
unfold valid_fmla; simpl; ae.
simpl; ae.
(*
intros sigma pi p q.
intros.
......
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