Commit 5a327729 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

wp4: proof update

parent 63ca4c96
This diff is collapsed.
......@@ -33,11 +33,13 @@ Inductive operator :=
(* Why3 assumption *)
Definition ident := Z.
Parameter refident : Type.
(* Why3 assumption *)
Inductive term :=
| Tvalue : value -> term
| Tvar : Z -> term
| Tderef : Z -> term
| Tderef : refident -> term
| Tbin : term -> operator -> term -> term .
(* Why3 assumption *)
......@@ -65,16 +67,16 @@ Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Definition env := (map Z value).
Definition env := (map refident value).
(* Why3 assumption *)
Inductive list (a:Type) :=
......@@ -112,9 +114,16 @@ Axiom get_stack_def : forall (i:Z) (pi:(list (Z* value)%type)),
((get_stack i pi) = (get_stack i r)))
end.
Axiom get_stack_eq : forall (x:Z) (v:value) (r:(list (Z* value)%type)),
((get_stack x (Cons (x, v) r)) = v).
Axiom get_stack_neq : forall (x:Z) (i:Z) (v:value) (r:(list (Z*
value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
r)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint eval_term(sigma:(map Z value)) (pi:(list (Z* value)%type))
Fixpoint eval_term(sigma:(map refident value)) (pi:(list (Z* value)%type))
(t:term) {struct t}: value :=
match t with
| (Tvalue v) => v
......@@ -127,7 +136,7 @@ Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint eval_fmla(sigma:(map Z value)) (pi:(list (Z* value)%type))
Fixpoint eval_fmla(sigma:(map refident value)) (pi:(list (Z* value)%type))
(f:fmla) {struct f}: Prop :=
match f with
| (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
......@@ -144,9 +153,9 @@ Fixpoint eval_fmla(sigma:(map Z value)) (pi:(list (Z* value)%type))
end.
Unset Implicit Arguments.
Parameter subst_term: term -> Z -> Z -> term.
Parameter subst_term: term -> refident -> Z -> term.
Axiom subst_term_def : forall (e:term) (r:Z) (v:Z),
Axiom subst_term_def : forall (e:term) (r:refident) (v:Z),
match e with
| ((Tvalue _)|(Tvar _)) => ((subst_term e r v) = e)
| (Tderef x) => ((r = x) -> ((subst_term e r v) = (Tvar v))) /\
......@@ -155,6 +164,17 @@ Axiom subst_term_def : forall (e:term) (r:Z) (v:Z),
(subst_term e2 r v)))
end.
Parameter vsubst_term: term -> Z -> term -> term.
Axiom vsubst_term_def : forall (e:term) (v:Z) (t:term),
match e with
| ((Tvalue _)|(Tderef _)) => ((vsubst_term e v t) = e)
| (Tvar x) => ((v = x) -> ((vsubst_term e v t) = t)) /\ ((~ (v = x)) ->
((vsubst_term e v t) = e))
| (Tbin e1 op e2) => ((vsubst_term e v t) = (Tbin (vsubst_term e1 v t) op
(vsubst_term e2 v t)))
end.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
......@@ -167,19 +187,19 @@ Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
Unset Implicit Arguments.
(* Why3 goal *)
Theorem eval_subst_term : forall (sigma:(map Z value)) (pi:(list (Z*
value)%type)) (e:term) (x:Z) (v:Z), (fresh_in_term v e) ->
Theorem eval_subst_term : forall (sigma:(map refident value)) (pi:(list (Z*
value)%type)) (e:term) (x:refident) (v:Z), (fresh_in_term v e) ->
((eval_term sigma pi (subst_term e x v)) = (eval_term (set sigma x
(get_stack v pi)) pi e)).
induction e; intros r v' H.
induction e; intros x v' H.
rewrite (subst_term_def (Tvalue v) r v'); auto.
rewrite (subst_term_def (Tvalue v) x v'); auto.
rewrite (subst_term_def (Tvar z) r v'); auto.
rewrite (subst_term_def (Tvar z) x v'); auto.
generalize (subst_term_def (Tderef z) r v').
generalize (subst_term_def (Tderef r) x v').
intros (h1,h2).
case (Z_eq_dec r z).
case (Z_eq_dec x r).
intro; subst r; rewrite h1; simpl; auto.
rewrite Select_eq; auto.
intro; rewrite h2; simpl; auto.
......
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