Commit 6ffbc360 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

suite preuves

parent bcbf9ac4
......@@ -216,7 +216,6 @@ function eval_bin (x:value) (op:operator) (y:value) : value =
| _,_ -> Vvoid
end
function eval_term (sigma:env) (pi:stack) (t:term) : value =
match t with
| Tvalue v -> v
......@@ -632,6 +631,7 @@ end
theory WP
use import ImpExpr
use import bool.Bool
use set.Set
......@@ -755,13 +755,18 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
| _ -> false
end
lemma decide_value:
lemma unique_type_expr :
forall e:expr, sigmat: type_env, pit:type_stack, ty1 ty2:datatype.
type_expr sigmat pit e ty1 ->
type_expr sigmat pit e ty2 -> ty1 = ty2
lemma decide_value :
forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v
lemma bool_value:
forall e:expr, sigmat: type_env, pit:type_stack.
type_expr sigmat pit e TYbool -> is_value e ->
(e = Evalue (Vbool Bool.False)) \/ (e = Evalue (Vbool Bool.True))
(e = Evalue (Vbool False)) \/ (e = Evalue (Vbool True))
lemma progress:
forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla.
......
......@@ -718,6 +718,11 @@ Definition is_value(e:expr): Prop :=
| _ => False
end.
Axiom unique_type_expr : forall (e:expr) (sigmat:(map mident datatype))
(pit:(list (ident* datatype)%type)) (ty1:datatype) (ty2:datatype),
(type_expr sigmat pit e ty1) -> ((type_expr sigmat pit e ty2) ->
(ty1 = ty2)).
Axiom decide_value : forall (e:expr), (~ (is_value e)) \/ exists v:value,
(e = (Evalue v)).
......@@ -727,6 +732,18 @@ Theorem bool_value : forall (e:expr) (sigmat:(map mident datatype))
((is_value e) -> ((e = (Evalue (Vbool false))) \/
(e = (Evalue (Vbool true))))).
intros e sigmat pit h1 h2.
destruct (decide_value e).
(* e is not a value *)
tauto.
(* e is not a value *)
elim H; clear H h2; intros v H.
subst e.
assert (h : type_expr sigmat pit (Evalue v) (type_value v)).
apply Type_evalue.
assert (TYbool = (type_value v)).
apply unique_type_expr with (Evalue v) sigmat pit; auto.
assert (h3: v = (Vbool false) \/ v = (Vbool true)).
admit.
Qed.
......
......@@ -756,14 +756,15 @@ intros h4; clear IHe1 IHe2.
assert (h: type_fmla typ_sigma (Cons (result, ty1) typ_pi) q').
eapply Type_let.
constructor; auto.
generalize (h4 h h3 H); clear h4.
admit.
admit.
(*generalize (h4 h h3 H); clear h4.
intro h4.
destruct h4 as (sigma' & pi' & e' & h5 ).
exists sigma'.
exists pi'.
exists (Ebin e' o e2).
apply one_step_bin_ctxt1; auto.
apply one_step_bin_ctxt1; auto.*)
(* case 1.2: e1 is a value *)
elim H; clear H; intros v He1_v.
......
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