From a7099c04ee0b9c91f1bf271045afa5cd1689ba4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Claude=20March=C3=A9?= Date: Thu, 27 Oct 2011 12:35:38 +0200 Subject: [PATCH] missing coq proofs --- examples/hoare_logic/wp/wp_Imp_If42_1.v | 198 ++++++++++++++++++++++ examples/hoare_logic/wp/wp_Imp_Test55_2.v | 91 ++++++++++ 2 files changed, 289 insertions(+) create mode 100644 examples/hoare_logic/wp/wp_Imp_If42_1.v create mode 100644 examples/hoare_logic/wp/wp_Imp_Test55_2.v diff --git a/examples/hoare_logic/wp/wp_Imp_If42_1.v b/examples/hoare_logic/wp/wp_Imp_If42_1.v new file mode 100644 index 000000000..89897a52e --- /dev/null +++ b/examples/hoare_logic/wp/wp_Imp_If42_1.v @@ -0,0 +1,198 @@ +(* 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 *) + + diff --git a/examples/hoare_logic/wp/wp_Imp_Test55_2.v b/examples/hoare_logic/wp/wp_Imp_Test55_2.v new file mode 100644 index 000000000..603c9fbcd --- /dev/null +++ b/examples/hoare_logic/wp/wp_Imp_Test55_2.v @@ -0,0 +1,91 @@ +(* 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 *) + + -- 2.24.1