Commit a7099c04 authored by MARCHE Claude's avatar MARCHE Claude

missing coq proofs

parent 7d9f7da3
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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
| Flet : term -> fmla -> fmla
| Fforall : fmla -> fmla .
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Inductive datatype :=
| Tint : datatype
| Tbool : datatype .
Inductive value :=
| Vint : Z -> value
| Vbool : bool -> value .
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
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 := (list value).
Definition ref_env := (map Z value).
Inductive state :=
| mk_state : (list 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): (list 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.
Inductive get_env : Z -> (list value) -> value -> Prop :=
| Get_first : forall (x:value) (l:(list value)), (get_env 0%Z (Cons x l) x)
| Get_next : forall (i:Z) (x:value) (r:value) (l:(list value)),
(0%Z < i)%Z -> ((get_env (i - 1%Z)%Z l r) -> (get_env i (Cons x l) x)).
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_env 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) (f:fmla), (forall (n:Z),
(eval_fmla (mk_state (Cons (Vint n) (var_env1 s)) (ref_env1 s)) f
true)) -> (eval_fmla s (Fforall f) true).
Inductive stmt :=
| Sskip : stmt
| Sassign : Z -> term -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : term -> stmt -> stmt -> stmt
| Swhile : term -> 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) (i:stmt), (eval_term s e
(Vbool true)) -> (one_step s (Swhile e i) s (Sseq i (Swhile e i)))
| one_step_while_false : forall (s:state) (e:term) (i:stmt), (eval_term s e
(Vbool false)) -> (one_step s (Swhile e i) s Sskip).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem If42 : forall (s1:state) (s2:state) (i:stmt),
(one_step (mk_state (Cons (Vint 42%Z) (Nil:(list value))) (const(
(Vint 0%Z)):(map Z value))) (Sif (Tbin (Tvar 0%Z) Ole (Tconst 7%Z))
(Sassign 0%Z (Tconst 13%Z)) (Sassign 0%Z (Tconst 42%Z))) s1 i) ->
((one_step s1 i s2 Sskip) -> ((get (ref_env1 s2) 0%Z) = (Vint 42%Z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros s1 s2 i H1 H2.
inversion H1; subst; clear H1.
inversion H7; subst; clear H7.
inversion H4; subst; clear H4.
inversion H6; subst; clear H6.
inversion H1; subst; clear H1.
red in H8.
intuition.
discriminate.
red in H8.
intuition.
discriminate.
inversion H2; subst; clear H2.
simpl.
inversion H4; subst; clear H4.
now apply Select_eq.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
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
| Flet : term -> fmla -> fmla
| Fforall : fmla -> fmla .
Inductive value :=
| Vint : Z -> value
| Vbool : bool -> value .
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Inductive state :=
| mk_state : (list value) -> (list value) -> state .
Definition ref_env(u:state): (list value) :=
match u with
| (mk_state _ ref_env1) => ref_env1
end.
Definition var_env(u:state): (list value) :=
match u with
| (mk_state var_env1 _) => var_env1
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))
end
| (_, _) => False
end.
Inductive get_env : Z -> (list value) -> value -> Prop :=
| Get_first : forall (x:value) (l:(list value)), (get_env 0%Z (Cons x l) x)
| Get_next : forall (i:Z) (x:value) (r:value) (l:(list value)),
(0%Z < i)%Z -> ((get_env (i - 1%Z)%Z l r) -> (get_env i (Cons x l) x)).
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_env i (var_env s)
res) -> (eval_term s (Tvar i) res)
| eval_deref : forall (s:state) (i:Z) (res:value), (get_env i (ref_env 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))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Test55 : (eval_term (mk_state (Cons (Vint 42%Z) (Nil:(list value)))
(Nil:(list value))) (Tbin (Tvar 0%Z) Oplus (Tconst 13%Z)) (Vint 55%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)
apply eval_bin1 with (r1:=Vint 42) (r2:=Vint 13).
constructor.
constructor.
constructor.
constructor.
Qed.
(* DO NOT EDIT BELOW *)
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