Commit dbb2d606 authored by MARCHE Claude's avatar MARCHE Claude

fix abstract_effect_monotonic

parent b0ba03aa
......@@ -722,9 +722,11 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
eval_fmla sigma pi f
axiom abstract_effects_monotonic :
forall s:stmt, f:fmla.
forall sigma:env, pi:stack. eval_fmla sigma pi f ->
forall sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s f)
forall s:stmt, p q:fmla.
valid_fmla (Fimplies p q) ->
forall sigma:env, pi:stack.
eval_fmla sigma pi (abstract_effects s p) ->
eval_fmla sigma pi (abstract_effects s q)
function wp (s:stmt) (q:fmla) : fmla =
match s with
......
......@@ -14,6 +14,53 @@ Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
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 map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
......@@ -68,6 +115,9 @@ Axiom mident : Type.
Parameter mident_WhyType : WhyType mident.
Existing Instance mident_WhyType.
Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/
~ (m1 = m2).
(* Why3 assumption *)
Inductive ident :=
| mk_ident : Z -> ident .
......@@ -79,67 +129,26 @@ Definition ident_index(v:ident): Z := match v with
| (mk_ident x) => x
end.
Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2).
(* Why3 assumption *)
Inductive term_node :=
| Tvalue : value -> term_node
| Tvar : ident -> term_node
| Tderef : mident -> term_node
| Tbin : term -> operator -> term -> term_node
with term :=
| mk_term : term_node -> Z -> term .
Inductive term :=
| Tvalue : value -> term
| Tvar : ident -> term
| Tderef : mident -> term
| Tbin : term -> operator -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
Axiom term_node_WhyType : WhyType term_node.
Existing Instance term_node_WhyType.
(* Why3 assumption *)
Definition term_maxvar(v:term): Z := match v with
| (mk_term x x1) => x1
end.
(* Why3 assumption *)
Definition term_node1(v:term): term_node :=
match v with
| (mk_term x x1) => x
end.
(* Why3 assumption *)
Fixpoint var_occurs_in_term(x:ident) (t:term) {struct t}: Prop :=
match t with
| (mk_term (Tvalue _) _) => False
| (mk_term (Tvar i) _) => (x = i)
| (mk_term (Tderef _) _) => False
| (mk_term (Tbin t1 _ t2) _) => (var_occurs_in_term x t1) \/
(var_occurs_in_term x t2)
| (Tvalue _) => False
| (Tvar i) => (x = i)
| (Tderef _) => False
| (Tbin t1 _ t2) => (var_occurs_in_term x t1) \/ (var_occurs_in_term x t2)
end.
(* Why3 assumption *)
Definition term_inv(t:term): Prop := forall (x:ident), (var_occurs_in_term x
t) -> ((ident_index x) <= (term_maxvar t))%Z.
(* Why3 assumption *)
Definition mk_tvalue(v:value): term := (mk_term (Tvalue v) (-1%Z)%Z).
Axiom mk_tvalue_inv : forall (v:value), (term_inv (mk_tvalue v)).
(* Why3 assumption *)
Definition mk_tvar(i:ident): term := (mk_term (Tvar i) (ident_index i)).
Axiom mk_tvar_inv : forall (i:ident), (term_inv (mk_tvar i)).
(* Why3 assumption *)
Definition mk_tderef(r:mident): term := (mk_term (Tderef r) (-1%Z)%Z).
Axiom mk_tderef_inv : forall (r:mident), (term_inv (mk_tderef r)).
(* Why3 assumption *)
Definition mk_tbin(t1:term) (o:operator) (t2:term): term := (mk_term (Tbin t1
o t2) (Zmax (term_maxvar t1) (term_maxvar t2))).
Axiom mk_tbin_inv : forall (t1:term) (t2:term) (o:operator),
((term_inv t1) /\ (term_inv t2)) -> (term_inv (mk_tbin t1 o t2)).
(* Why3 assumption *)
Inductive fmla :=
| Fterm : term -> fmla
......@@ -162,6 +171,8 @@ Inductive stmt :=
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
(* Why3 assumption *)
Definition type_value(v:value): datatype :=
match v with
......@@ -197,19 +208,19 @@ Definition type_env := (map mident datatype).
Inductive type_term : (map mident datatype) -> (list (ident* datatype)%type)
-> term -> datatype -> Prop :=
| Type_value : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (v:value) (m:Z), (type_term sigma pi
(mk_term (Tvalue v) m) (type_value v))
datatype)%type)) (v:value), (type_term sigma pi (Tvalue v)
(type_value v))
| Type_var : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (v:ident) (m:Z) (ty:datatype), ((get_vartype v
pi) = ty) -> (type_term sigma pi (mk_term (Tvar v) m) ty)
datatype)%type)) (v:ident) (ty:datatype), ((get_vartype v pi) = ty) ->
(type_term sigma pi (Tvar v) ty)
| Type_deref : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (v:mident) (m:Z) (ty:datatype), ((get sigma
v) = ty) -> (type_term sigma pi (mk_term (Tderef v) m) ty)
datatype)%type)) (v:mident) (ty:datatype), ((get sigma v) = ty) ->
(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) (m:Z) (ty1:datatype)
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 (mk_term (Tbin t1 op t2) m) ty))).
(type_term sigma pi (Tbin t1 op t2) ty))).
(* Why3 assumption *)
Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
......@@ -305,13 +316,40 @@ Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
(t:term) {struct t}: value :=
match t with
| (mk_term (Tvalue v) _) => v
| (mk_term (Tvar id) _) => (get_stack id pi)
| (mk_term (Tderef id) _) => (get sigma id)
| (mk_term (Tbin t1 op t2) _) => (eval_bin (eval_term sigma pi t1) op
(eval_term sigma pi t2))
| (Tvalue v) => v
| (Tvar id) => (get_stack id pi)
| (Tderef id) => (get sigma id)
| (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
pi t2))
end.
(* 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).
(* Why3 assumption *)
Definition existe_compatible(ty:datatype) (v:value): Prop :=
match ty 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))).
(* Why3 assumption *)
Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
(f:fmla) {struct f}: Prop :=
......@@ -333,41 +371,31 @@ Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
match t with
| (mk_term ((Tvalue _)|(Tvar _)) _) => ((msubst_term t r v) = t)
| (mk_term (Tderef x) _) => ((r = x) -> ((msubst_term t r
v) = (mk_tvar v))) /\ ((~ (r = x)) -> ((msubst_term t r v) = t))
| (mk_term (Tbin t1 op t2) _) => ((msubst_term t r
v) = (mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v)))
| ((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.
Parameter subst_term: term -> ident -> ident -> term.
Axiom subst_term_def : forall (t:term) (r:ident) (v:ident),
match t with
| (mk_term ((Tvalue _)|(Tderef _)) _) => ((subst_term t r v) = t)
| (mk_term (Tvar x) _) => ((r = x) -> ((subst_term t r
v) = (mk_tvar v))) /\ ((~ (r = x)) -> ((subst_term t r v) = t))
| (mk_term (Tbin t1 op t2) _) => ((subst_term t r
v) = (mk_tbin (subst_term t1 r v) op (subst_term t2 r v)))
| ((Tvalue _)|(Tderef _)) => ((subst_term t r v) = t)
| (Tvar x) => ((r = x) -> ((subst_term t r v) = (Tvar v))) /\
((~ (r = x)) -> ((subst_term t r v) = t))
| (Tbin t1 op t2) => ((subst_term t r v) = (Tbin (subst_term t1 r v) op
(subst_term t2 r v)))
end.
(* Why3 assumption *)
Definition fresh_in_term(id:ident) (t:term): Prop :=
((term_maxvar t) < (ident_index id))%Z.
Definition fresh_in_term(id:ident) (t:term): Prop := ~ (var_occurs_in_term id
t).
Axiom eval_msubst_term : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (e:term) (x:mident) (v:ident), (fresh_in_term v e) ->
((eval_term sigma pi (msubst_term e x v)) = (eval_term (set sigma x
(get_stack v pi)) pi e)).
Axiom eval_subst_term : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (e:term) (x:ident) (v:ident), (fresh_in_term v e) ->
((eval_term sigma pi (subst_term e x v)) = (eval_term sigma (Cons (x,
(get_stack v pi)) pi) e)).
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 fresh_in_binop : forall (t:term) (t':term) (op:operator) (v:ident),
(fresh_in_term v (Tbin t op t')) -> ((fresh_in_term v t) /\
(fresh_in_term v t')).
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (f:fmla) {struct f}: Prop :=
......@@ -403,55 +431,57 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
Axiom subst_fresh_term : forall (t:term) (x:ident) (v:ident),
(fresh_in_term x t) -> ((subst_term t x v) = t).
Axiom subst_fresh : forall (f:fmla) (x:ident) (v:ident), (fresh_in_fmla x
f) -> ((subst f x v) = f).
Axiom let_subst : forall (t:term) (f:fmla) (x:ident) (id':ident) (id:mident),
((msubst (Flet x t f) id id') = (Flet x (msubst_term t id id') (msubst f id
id'))).
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
(get_stack v pi)) pi e)).
Axiom eval_msubst : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:mident) (v:ident), (fresh_in_fmla v f) ->
((eval_fmla sigma pi (msubst f x v)) <-> (eval_fmla (set sigma x
(get_stack v pi)) pi f)).
Axiom eval_subst : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:ident) (v:ident), (fresh_in_fmla v f) ->
((eval_fmla sigma pi (subst f x v)) <-> (eval_fmla sigma (Cons (x,
(get_stack v pi)) pi) f)).
Axiom eval_swap_term : forall (t:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
(id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_term sigma
(infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi))) t) = (eval_term sigma
(infix_plpl l (Cons (id2, v2) (Cons (id1, v1) pi))) t)).
Axiom eval_swap : forall (f:fmla) (sigma:(map mident value)) (pi:(list
Axiom eval_swap_term_2 : forall (t:term) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id1:ident) (id2:ident) (v1:value) (v2:value),
(~ (id1 = id2)) -> ((eval_fmla sigma (Cons (id1, v1) (Cons (id2, v2) pi))
f) <-> (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi)) f)).
(~ (id1 = id2)) -> ((eval_term sigma (Cons (id1, v1) (Cons (id2, v2) pi))
t) = (eval_term sigma (Cons (id2, v2) (Cons (id1, v1) pi)) t)).
Axiom eval_same_var : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id:ident) (v1:value) (v2:value), (eval_fmla sigma
(Cons (id, v1) (Cons (id, v2) pi)) f) <-> (eval_fmla sigma (Cons (id, v1)
pi) f).
Axiom eval_swap : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
(id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_fmla sigma
(infix_plpl l (Cons (id1, v1) (Cons (id2, v2) pi))) f) <-> (eval_fmla sigma
(infix_plpl l (Cons (id2, v2) (Cons (id1, v1) 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)).
Axiom eval_swap_2 : forall (f:fmla) (id1:ident) (id2:ident) (v1:value)
(v2:value), (~ (id1 = id2)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma (Cons (id1, v1) (Cons (id2, v2)
pi)) f) <-> (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi)) f).
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).
(* Why3 assumption *)
Definition valid_fmla(p:fmla): Prop := forall (sigma:(map mident value))
(pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
Axiom let_equiv : forall (id:ident) (id':ident) (t:term) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(fresh_in_fmla id' f) -> ((eval_fmla sigma pi (Flet id' t (subst f id
id'))) -> (eval_fmla sigma pi (Flet id t f))).
Axiom let_equiv2 : forall (id:ident) (id':ident) (t:term) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(fresh_in_fmla id' f) -> ((eval_fmla sigma pi (Flet id' t (subst f id
id'))) -> (eval_fmla sigma pi (Flet id t f))).
Axiom let_implies : forall (id:ident) (t:term) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> (valid_fmla (Fimplies (Flet id t p) (Flet id
t q))).
(* Why3 assumption *)
Fixpoint fresh_in_stmt(id:ident) (s:stmt) {struct s}: Prop :=
match s with
......@@ -492,7 +522,7 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
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_falsee : forall (sigma:(map mident value)) (pi:(list
| 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)
......@@ -524,11 +554,13 @@ Axiom many_steps_seq : forall (sigma1:(map mident value)) (sigma3:(map mident
pi2 Sskip n1) /\ ((many_steps sigma2 pi2 s2 sigma3 pi3 Sskip n2) /\
(n = ((1%Z + n1)%Z + n2)%Z)).
Axiom one_step_change_free : forall (s:stmt) (s':stmt) (sigma:(map mident
value)) (sigma':(map mident value)) (pi:(list (ident* value)%type))
(pi':(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_stmt id
s) -> ((one_step sigma (Cons (id, v) pi) s sigma' pi' s') ->
(one_step sigma pi s sigma' pi' s')).
Axiom type_preservation : forall (s1:stmt) (s2:stmt) (sigma1:(map mident
value)) (sigma2:(map mident value)) (pi1:(list (ident* value)%type))
(pi2:(list (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list
(ident* datatype)%type)), ((type_stmt sigmat pit s1) /\
((compatible_env sigma1 sigmat pi1 pit) /\ (one_step sigma1 pi1 s1 sigma2
pi2 s2))) -> ((type_stmt sigmat pit s2) /\ (compatible_env sigma2 sigmat
pi2 pit)).
(* Why3 assumption *)
Definition valid_triple(p:fmla) (s:stmt) (q:fmla): Prop := forall (sigma:(map
......
......@@ -14,6 +14,53 @@ Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
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 map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
......@@ -68,6 +115,9 @@ Axiom mident : Type.
Parameter mident_WhyType : WhyType mident.
Existing Instance mident_WhyType.
Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/
~ (m1 = m2).
(* Why3 assumption *)
Inductive ident :=
| mk_ident : Z -> ident .
......@@ -79,67 +129,26 @@ Definition ident_index(v:ident): Z := match v with
| (mk_ident x) => x
end.
Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2).
(* Why3 assumption *)
Inductive term_node :=
| Tvalue : value -> term_node
| Tvar : ident -> term_node
| Tderef : mident -> term_node
| Tbin : term -> operator -> term -> term_node
with term :=
| mk_term : term_node -> Z -> term .
Inductive term :=
| Tvalue : value -> term
| Tvar : ident -> term
| Tderef : mident -> term
| Tbin : term -> operator -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
Axiom term_node_WhyType : WhyType term_node.
Existing Instance term_node_WhyType.
(* Why3 assumption *)
Definition term_maxvar(v:term): Z := match v with
| (mk_term x x1) => x1
end.
(* Why3 assumption *)
Definition term_node1(v:term): term_node :=
match v with
| (mk_term x x1) => x
end.