Commit 2a7a689f authored by MARCHE Claude's avatar MARCHE Claude

fix unplayed Coq proof in nightly bench

parent 8a6c1483
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
(* Why3 assumption *)
Inductive list (a:Type) :=
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
Parameter map : forall (a:Type) (b:Type), Type.
Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
Type.
Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {b:Type}, (map a b) -> a -> b.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {b:Type}, (map a b) -> a -> b -> (map a b).
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
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_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
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)).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, 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 {a:Type} {b:Type}, b -> (map a b).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {b:Type}, forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vint : BuiltIn.int -> value
| Vbool : bool -> value .
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
......@@ -49,15 +62,22 @@ Inductive operator :=
| Ominus : operator
| Omult : operator
| Ole : operator .
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
Parameter mident : Type.
Axiom mident_WhyType : WhyType mident.
Existing Instance mident_WhyType.
(* Why3 assumption *)
Inductive ident :=
| mk_ident : Z -> ident .
| mk_ident : BuiltIn.int -> ident .
Axiom ident_WhyType : WhyType ident.
Existing Instance ident_WhyType.
(* Why3 assumption *)
Definition ident_index(v:ident): Z := match v with
Definition ident_index(v:ident): BuiltIn.int :=
match v with
| (mk_ident x) => x
end.
......@@ -69,13 +89,18 @@ Inductive term_node :=
| Tvar : ident -> term_node
| Tderef : mident -> term_node
| Tbin : term -> operator -> term -> term_node .
Axiom term_node_WhyType : WhyType term_node.
Existing Instance term_node_WhyType.
(* Why3 assumption *)
Inductive term :=
| mk_term : term_node -> Z -> term .
| mk_term : term_node -> BuiltIn.int -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Definition term_maxvar(v:term): Z := match v with
Definition term_maxvar(v:term): BuiltIn.int :=
match v with
| (mk_term x x1) => x1
end.
......@@ -129,6 +154,8 @@ Inductive fmla :=
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla .
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
(* Why3 assumption *)
Inductive expr :=
......@@ -142,12 +169,14 @@ Inductive expr :=
| Eif : expr -> expr -> expr -> expr
| Eassert : fmla -> expr
| Ewhile : expr -> fmla -> expr -> expr .
Axiom expr_WhyType : WhyType expr.
Existing Instance expr_WhyType.
(* Why3 assumption *)
Definition type_value(v:value): datatype :=
match v with
| Vvoid => TYunit
| (Vint int1) => TYint
| (Vint int) => TYint
| (Vbool bool1) => TYbool
end.
......@@ -178,19 +207,20 @@ 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
datatype)%type)) (v:value) (m:BuiltIn.int), (type_term sigma pi
(mk_term (Tvalue v) m) (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) (m:BuiltIn.int) (ty:datatype),
((get_vartype v pi) = ty) -> (type_term sigma pi (mk_term (Tvar v) m)
ty)
| Type_deref : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (v:mident) (m:Z) (ty:datatype), ((get sigma
datatype)%type)) (v:mident) (m:BuiltIn.int) (ty:datatype), ((get sigma
v) = ty) -> (type_term sigma pi (mk_term (Tderef v) m) ty)
| Type_bin : forall (sigma:(map mident datatype)) (pi:(list (ident*
datatype)%type)) (t1:term) (t2:term) (op:operator) (m:Z) (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))).
datatype)%type)) (t1:term) (t2:term) (op:operator) (m:BuiltIn.int)
(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))).
(* Why3 assumption *)
Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
......@@ -320,8 +350,8 @@ Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
| (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2)
| (Flet x t f1) => (eval_fmla sigma (Cons (x, (eval_term sigma pi t)) pi)
f1)
| (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma (Cons (x,
(Vint n)) pi) f1)
| (Fforall x TYint f1) => forall (n:BuiltIn.int), (eval_fmla sigma (Cons (
x, (Vint n)) pi) f1)
| (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma (Cons (x,
(Vbool b)) pi) f1)
| (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1)
......
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