Commit 8e0f218c authored by MARCHE Claude's avatar MARCHE Claude

hoare logic: rules for assert

parent 69a8b5e8
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Inductive datatype :=
| Tint : datatype
| Tbool : datatype .
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator .
Definition ident := Z.
Inductive term :=
| Tconst : Z -> term
| Tvar : Z -> term
| Tderef : Z -> term
| Tbin : term -> operator -> term -> term .
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Fforall : Z -> datatype -> fmla -> fmla .
Inductive value :=
| Vint : Z -> value
| Vbool : bool -> value .
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : 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) = b1).
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).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition var_env := (map Z value).
Definition ref_env := (map Z value).
Inductive state :=
| mk_state : (map Z value) -> (map Z value) -> state .
Definition ref_env1(u:state): (map Z value) :=
match u with
| (mk_state _ ref_env2) => ref_env2
end.
Definition var_env1(u:state): (map Z value) :=
match u with
| (mk_state var_env2 _) => var_env2
end.
Definition eval_bin(x:value) (op:operator) (y:value) (res:value): Prop :=
match (x,
y) with
| ((Vint x1), (Vint y1)) =>
match op with
| Oplus => (res = (Vint (x1 + y1)%Z))
| Ominus => (res = (Vint (x1 - y1)%Z))
| Omult => (res = (Vint (x1 * y1)%Z))
| Ole => ((x1 <= y1)%Z -> (res = (Vbool true))) /\ ((~ (x1 <= y1)%Z) ->
(res = (Vbool false)))
end
| (_, _) => False
end.
Definition get_refenv(i:Z) (e:(map Z value)) (r:value): Prop := ((get e
i) = r).
Inductive eval_term : state -> term -> value -> Prop :=
| eval_const : forall (s:state) (n:Z), (eval_term s (Tconst n) (Vint n))
| eval_var : forall (s:state) (i:Z) (res:value), (get_refenv i (var_env1 s)
res) -> (eval_term s (Tvar i) res)
| eval_deref : forall (s:state) (i:Z) (res:value), (get_refenv i
(ref_env1 s) res) -> (eval_term s (Tderef i) res)
| eval_bin1 : forall (s:state) (op:operator) (t1:term) (t2:term) (r1:value)
(r2:value) (r:value), (eval_term s t1 r1) -> ((eval_term s t2 r2) ->
((eval_bin r1 op r2 r) -> (eval_term s (Tbin t1 op t2) r))).
Inductive eval_fmla : state -> fmla -> bool -> Prop :=
| eval_term1 : forall (s:state) (t:term) (b:bool), (eval_term s t
(Vbool b)) -> (eval_fmla s (Fterm t) b)
| eval_and : forall (s:state) (f1:fmla) (f2:fmla) (b1:bool) (b2:bool),
(eval_fmla s f1 b1) -> ((eval_fmla s f2 b2) -> (eval_fmla s (Fand f1
f2) (andb b1 b2)))
| eval_not : forall (s:state) (f:fmla) (b:bool), (eval_fmla s f b) ->
(eval_fmla s (Fnot f) (negb b))
| eval_impl : forall (s:state) (f1:fmla) (f2:fmla) (b1:bool) (b2:bool),
(eval_fmla s f1 b1) -> ((eval_fmla s f2 b2) -> (eval_fmla s
(Fimplies f1 f2) (implb b1 b2)))
| eval_forall_int_true : forall (s:state) (x:Z) (f:fmla), (forall (n:Z),
(eval_fmla (mk_state (set (var_env1 s) x (Vint n)) (ref_env1 s)) f
true)) -> (eval_fmla s (Fforall x Tint f) true).
Parameter subst_term: term -> Z -> term -> term.
Axiom subst_term_def : forall (e:term) (x:Z) (t:term),
match e with
| (Tconst _) => ((subst_term e x t) = e)
| (Tvar _) => ((subst_term e x t) = e)
| (Tderef y) => ((x = y) -> ((subst_term e x t) = t)) /\ ((~ (x = y)) ->
((subst_term e x t) = e))
| (Tbin e1 op e2) => ((subst_term e x t) = (Tbin (subst_term e1 x t) op
(subst_term e2 x t)))
end.
Axiom eval_subst_term : forall (s:state) (e:term) (x:Z) (t:term) (r:value)
(v:value), (eval_term s t r) -> ((eval_term s (subst_term e x t) v) <->
(eval_term (mk_state (var_env1 s) (set (ref_env1 s) x r)) e v)).
Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:Z) (t:term) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (subst_term e x t))
| (Fand f1 f2) => (Fand (subst f1 x t) (subst f2 x t))
| (Fnot f1) => (Fnot (subst f1 x t))
| (Fimplies f1 f2) => (Fimplies (subst f1 x t) (subst f2 x t))
| (Fforall y ty f1) => (Fforall y ty (subst f1 x t))
end.
Unset Implicit Arguments.
Axiom eval_subst : forall (s:state) (f:fmla) (x:Z) (t:term) (r:value)
(b:bool), (eval_fmla s (subst f x t) b) <->
(eval_fmla (mk_state (var_env1 s) (set (ref_env1 s) x r)) f b).
Inductive stmt :=
| Sskip : stmt
| Sassign : Z -> term -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : term -> stmt -> stmt -> stmt
| Swhile : term -> fmla -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Inductive one_step : state -> stmt -> state -> stmt -> Prop :=
| one_step_assign : forall (s:state) (x:Z) (e:term) (r:value), (eval_term s
e r) -> (one_step s (Sassign x e) (mk_state (var_env1 s)
(set (ref_env1 s) x r)) Sskip)
| one_step_seq : forall (s:state) (sqt:state) (i1:stmt) (i1qt:stmt)
(i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1 i2) sqt
(Sseq i1qt i2))
| one_step_seq_skip : forall (s:state) (i:stmt), (one_step s (Sseq Sskip i)
s i)
| one_step_if_true : forall (s:state) (e:term) (i1:stmt) (i2:stmt),
(eval_term s e (Vbool true)) -> (one_step s (Sif e i1 i2) s i1)
| one_step_if_false : forall (s:state) (e:term) (i1:stmt) (i2:stmt),
(eval_term s e (Vbool false)) -> (one_step s (Sif e i1 i2) s i2)
| one_step_while_true : forall (s:state) (e:term) (inv:fmla) (i:stmt),
(eval_fmla s inv true) -> ((eval_term s e (Vbool true)) -> (one_step s
(Swhile e inv i) s (Sseq i (Swhile e inv i))))
| one_step_while_false : forall (s:state) (e:term) (inv:fmla) (i:stmt),
(eval_fmla s inv true) -> ((eval_term s e (Vbool false)) -> (one_step s
(Swhile e inv i) s Sskip)).
Inductive many_steps : state -> stmt -> state -> stmt -> Z -> Prop :=
| many_steps_refl : forall (s:state) (i:stmt), (many_steps s i s i 0%Z)
| many_steps_trans : forall (s1:state) (s2:state) (s3:state) (i1:stmt)
(i2:stmt) (i3:stmt) (n:Z), (one_step s1 i1 s2 i2) -> ((many_steps s2 i2
s3 i3 n) -> (many_steps s1 i1 s3 i3 (n + 1%Z)%Z)).
Axiom steps_non_neg : forall (s1:state) (s2:state) (i1:stmt) (i2:stmt) (n:Z),
(many_steps s1 i1 s2 i2 n) -> (0%Z <= n)%Z.
Axiom many_steps_seq : forall (s1:state) (s3:state) (i1:stmt) (i2:stmt)
(n:Z), (many_steps s1 (Sseq i1 i2) s3 Sskip n) -> exists s2:state,
exists n1:Z, exists n2:Z, (many_steps s1 i1 s2 Sskip n1) /\ ((many_steps s2
i2 s3 Sskip n2) /\ (n = ((1%Z + n1)%Z + n2)%Z)).
Definition valid_fmla(p:fmla): Prop := forall (s:state), (eval_fmla s p
true).
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:state),
(eval_fmla s p true) -> forall (sqt:state) (n:Z), (many_steps s i sqt Sskip
n) -> (eval_fmla sqt q true).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (e:term), (valid_triple (subst q x
e) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt i qqt))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_wp : forall (i:stmt), forall (q:fmla),
match i with
| Sskip => True
| (Sseq i1 i2) => True
| (Sassign x e) => True
| (Sif e i1 i2) => forall (result:fmla), (valid_triple result i1 q) ->
forall (result1:fmla), (valid_triple result1 i2 q) ->
(valid_triple (Fand (Fimplies (Fterm e) result)
(Fimplies (Fnot (Fterm e)) result1)) i q)
| (Swhile e inv i1) => True
end.
(* YOU MAY EDIT THE PROOF BELOW *)
destruct i; auto.
intros q r1 H1 r2 H2.
apply if_rule.
split.
apply consequence_rule with (2:= H1).
Focus 2.
red.
intro.
apply eval_impl.
simpl.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -299,6 +299,10 @@ lemma assert_rule:
forall f p:fmla. valid_fmla (Fimplies p f) ->
valid_triple p (Sassert f) p
lemma assert_rule_ext:
forall f p:fmla.
valid_triple (Fimplies f p) (Sassert f) p
lemma while_rule:
forall e:term, inv:fmla, i:stmt.
valid_triple (Fand (Fterm e) inv) i inv ->
......@@ -335,15 +339,15 @@ module WP
| Sseq i1 i2 -> wp i1 (wp i2 q)
| Sassign x e ->
(*
let id = fresh ? in Flet id e (subst q x (Tvar id))
let id = fresh (vars q) in Flet id e (subst q x (Tvar id))
*)
subst q x e
| Sif e i1 i2 ->
Fand (Fimplies (Fterm e) (wp i1 q))
(Fimplies (Fnot (Fterm e)) (wp i2 q))
| Sassert f ->
(* Fimplies f q (* liberal wp, no termination requires *)*)
Fand f q
Fimplies f q (* liberal wp, no termination requires *)
(* Fand f q *) (* strict wp, termination required *)
| Swhile e inv i ->
Fand inv
((*Fforall*) (Fand
......
......@@ -292,9 +292,23 @@
<result status="valid" time="0.49"/>
</proof>
</goal>
<goal
name="assert_rule_ext"
sum="6ef422accb858e96de2d1c57b650517d"
proved="true"
expanded="false"
shape="avalid_tripleaFimpliesV0V1aSassertV0V1F">
<proof
prover="coq"
timelimit="5"
edited="wp_total_Imp_assert_rule_ext_1.v"
obsolete="false">
<result status="valid" time="0.64"/>
</proof>
</goal>
<goal
name="while_rule"
sum="bec5834960c3c86b3f9f99cc18738d22"
sum="9415c44e0de53e2b8ab66c98e1aad735"
proved="true"
expanded="false"
shape="avalid_tripleV1aSwhileV0V1V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
......@@ -303,12 +317,12 @@
timelimit="5"
edited="wp_total_Imp_while_rule_1.v"
obsolete="false">
<result status="valid" time="0.89"/>
<result status="valid" time="0.75"/>
</proof>
</goal>
<goal
name="while_rule_ext"
sum="8794717fd4ea98f868bff9bef70ba2e9"
sum="b0e30a2a5ef7cc94e42779e850a6e322"
proved="true"
expanded="false"
shape="avalid_tripleV2aSwhileV0V1V3aFandaFnotaFtermV0V2Iavalid_tripleaFandaFtermV0V2V3V2Iavalid_fmlaaFimpliesV2V1F">
......@@ -317,12 +331,12 @@
timelimit="5"
edited="wp_total_Imp_while_rule_ext_1.v"
obsolete="false">
<result status="valid" time="0.68"/>
<result status="valid" time="0.92"/>
</proof>
</goal>
<goal
name="consequence_rule"
sum="6d2f7c295257b282b3949c9e1578b827"
sum="22eda61fc378d4aff202e97861225890"
proved="true"
expanded="false"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
......@@ -331,14 +345,14 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.99"/>
<result status="valid" time="1.13"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
</theory>
......@@ -349,15 +363,15 @@
<goal
name="WP_parameter wp"
expl="parameter wp"
sum="f45f813e5159661bb5111be4d54b8790"
sum="fcf6c0443719c76bb3dd7ad8e2f3d53e"
proved="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V11aFimpliesaFnotaFtermV8V12V0V1Iavalid_tripleV12V10V1FIavalid_tripleV11V9V1FaSassertVavalid_tripleaFandV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FFF">
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V11aFimpliesaFnotaFtermV8V12V0V1Iavalid_tripleV12V10V1FIavalid_tripleV11V9V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FFF">
<proof
prover="coq"
timelimit="5"
edited="wp_total_WP_WP_WP_parameter_wp_2.v"
obsolete="false">
obsolete="true">
<result status="unknown" time="0.66"/>
</proof>
<transf
......@@ -367,7 +381,7 @@
<goal
name="WP_parameter wp.1"
expl="parameter wp"
sum="681cb4de3c5050ec5b11c56595edba80"
sum="e39ef2792789f35bc7b90f25ed79b298"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
......@@ -376,13 +390,13 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
name="WP_parameter wp.2"
expl="parameter wp"
sum="9323fd1e9b4f9bd9e199ad0082179385"
sum="35730568229c8ac688137a37e2315371"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
......@@ -391,13 +405,13 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
name="WP_parameter wp.3"
expl="parameter wp"
sum="78deb10676cae77d7398c31af63dcad8"
sum="f2d2133eb159207f51a4abc3674e7ac4"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSassertVtaSwhileVVVtFF">
......@@ -412,7 +426,7 @@
<goal
name="WP_parameter wp.4"
expl="parameter wp"
sum="1d98f58ccafb8e25b250d710e3a291d0"
sum="95a4085929243ddade16b291fe90bb0f"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V9aFimpliesaFnotaFtermV6V10V0V1Iavalid_tripleV10V8V1FIavalid_tripleV9V7V1FaSassertVtaSwhileVVVtFF">
......@@ -420,14 +434,14 @@
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="5.07"/>
</proof>
<proof
......@@ -435,28 +449,49 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.78"/>
<result status="valid" time="0.66"/>
</proof>
</goal>
<goal
name="WP_parameter wp.5"
expl="parameter wp"
sum="be14bc25a605358d0b402de18e4435bd"
sum="452220572080dad57c9a7e32b60ffdcb"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFandV9V1V0V1aSwhileVVVtFF">
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtFF">
<proof
prover="coq"
timelimit="5"
edited="wp_total_WP_WP_WP_parameter_wp_3.v"
obsolete="true">
<result status="unknown" time="0.44"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.44"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
name="WP_parameter wp.6"
expl="parameter wp"
sum="ec411b6472a60f81d2c3076de8bba26e"
sum="457c7d860257e025ced48c9fdd71eee2"
proved="false"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1V0V1Iavalid_tripleV13V12V11FFF">
......@@ -464,21 +499,21 @@
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="5.07"/>
</proof>
</goal>
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Inductive datatype :=
| Tint : datatype
| Tbool : datatype .
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator .
Definition ident := Z.
Inductive term :=
| Tconst : Z -> term
| Tvar : Z -> term
| Tderef : Z -> term
| Tbin : term -> operator -> term -> term .
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla .
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Inductive value :=
| Vint : Z -> value
| Vbool : bool -> value .
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : 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) = b1).
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).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition env := (map Z value).