Commit df3b860b authored by MARCHE Claude's avatar MARCHE Claude

Hoare logic: if rule

parent bb243268
...@@ -163,10 +163,14 @@ lemma many_steps_seq: ...@@ -163,10 +163,14 @@ lemma many_steps_seq:
type fmla = type fmla =
| Fterm expr | Fterm expr
| Fand fmla fmla
| Fnot fmla
predicate eval_fmla (s:state) (f:fmla) = predicate eval_fmla (s:state) (f:fmla) =
match f with match f with
| Fterm e -> eval_expr s e <> 0 | Fterm e -> eval_expr s e <> 0
| Fand f1 f2 -> eval_fmla s f1 /\ eval_fmla s f2
| Fnot f -> not (eval_fmla s f)
end end
(* substitution *) (* substitution *)
...@@ -186,11 +190,13 @@ lemma eval_subst_expr: ...@@ -186,11 +190,13 @@ lemma eval_subst_expr:
function subst (f:fmla) (x:ident) (t:expr) : fmla = function subst (f:fmla) (x:ident) (t:expr) : fmla =
match f with match f with
| Fterm e -> Fterm (subst_expr e x t) | Fterm e -> Fterm (subst_expr e x t)
| Fand f1 f2 -> Fand (subst f1 x t) (subst f2 x t)
| Fnot f -> Fnot (subst f x t)
end end
lemma eval_subst: lemma eval_subst:
forall s:state, f:fmla, x:ident, t:expr. forall s:state, f:fmla, x:ident, t:expr.
eval_fmla s (subst f x t) -> eval_fmla (IdMap.set s x (eval_expr s t)) f eval_fmla s (subst f x t) <-> eval_fmla (IdMap.set s x (eval_expr s t)) f
(* Hoare triples *) (* Hoare triples *)
...@@ -201,6 +207,9 @@ predicate valid_triple (p:fmla) (i:stmt) (q:fmla) = ...@@ -201,6 +207,9 @@ predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
(* Hoare logic rules *) (* Hoare logic rules *)
lemma skip_rule:
forall q:fmla. valid_triple q Sskip q
lemma assign_rule: lemma assign_rule:
forall q:fmla, x:ident, e:expr. forall q:fmla, x:ident, e:expr.
valid_triple (subst q x e) (Sassign x e) q valid_triple (subst q x e) (Sassign x e) q
...@@ -210,6 +219,12 @@ lemma seq_rule: ...@@ -210,6 +219,12 @@ lemma seq_rule:
valid_triple p i1 r /\ valid_triple r i2 q -> valid_triple p i1 r /\ valid_triple r i2 q ->
valid_triple p (Sseq i1 i2) q valid_triple p (Sseq i1 i2) q
lemma if_rule:
forall e:expr, p q:fmla, i1 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
end end
......
...@@ -4,9 +4,14 @@ Require Import ZArith. ...@@ -4,9 +4,14 @@ Require Import ZArith.
Require Import Rbase. Require Import Rbase.
Parameter ident : Type. Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident. Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
Inductive operator := Inductive operator :=
| Oplus : operator | Oplus : operator
| Ominus : operator | Ominus : operator
...@@ -110,12 +115,18 @@ Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt) ...@@ -110,12 +115,18 @@ Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip). Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip).
Inductive fmla := Inductive fmla :=
| Fterm : expr -> fmla . | Fterm : expr -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla .
Definition eval_fmla(s:(map ident Z)) (f:fmla): Prop := Set Implicit Arguments.
Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
match f with match f with
| (Fterm e) => ~ ((eval_expr s e) = 0%Z) | (Fterm e) => ~ ((eval_expr s e) = 0%Z)
| (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
| (Fnot f1) => ~ (eval_fmla s f1)
end. end.
Unset Implicit Arguments.
Parameter subst_expr: expr -> ident -> expr -> expr. Parameter subst_expr: expr -> ident -> expr -> expr.
...@@ -133,18 +144,24 @@ Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr), ...@@ -133,18 +144,24 @@ Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t)) ((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
e)). e)).
Definition subst(f:fmla) (x:ident) (t:expr): fmla := Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
match f with match f with
| (Fterm e) => (Fterm (subst_expr e x t)) | (Fterm e) => (Fterm (subst_expr e x t))
| (Fand f1 f2) => (Fand (subst f1 x t) (subst f2 x t))
| (Fnot f1) => (Fnot (subst f1 x t))
end. end.
Unset Implicit Arguments.
Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr), Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
(eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f). (eval_fmla s (subst f x t)) <-> (eval_fmla (set s x (eval_expr s t)) f).
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:(map Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:(map
ident Z)), (eval_fmla s p) -> forall (sqt:(map ident Z)), (many_steps s i ident Z)), (eval_fmla s p) -> forall (sqt:(map ident Z)), (many_steps s i
sqt Sskip) -> (eval_fmla sqt q). sqt Sskip) -> (eval_fmla sqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
(* YOU MAY EDIT THE CONTEXT BELOW *) (* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *)
...@@ -160,7 +177,7 @@ inversion H; subst. ...@@ -160,7 +177,7 @@ inversion H; subst.
inversion H0; subst. inversion H0; subst.
(* normal case *) (* normal case *)
clear H Hred H0. clear H Hred H0.
apply eval_subst; auto. rewrite <- eval_subst; auto.
(* absurd case *) (* absurd case *)
inversion H1. inversion H1.
......
...@@ -4,9 +4,14 @@ Require Import ZArith. ...@@ -4,9 +4,14 @@ Require Import ZArith.
Require Import Rbase. Require Import Rbase.
Parameter ident : Type. Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident. Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
Inductive operator := Inductive operator :=
| Oplus : operator | Oplus : operator
| Ominus : operator | Ominus : operator
...@@ -100,17 +105,28 @@ Inductive many_steps : (map ident Z) -> stmt -> (map ident Z) ...@@ -100,17 +105,28 @@ Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) -> ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)). ((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
Axiom many_steps_seq_rec : forall (s1:(map ident Z)) (s3:(map ident Z))
(i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map ident Z),
(many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip)).
Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt) Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
(i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) -> exists s2:(map ident (i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) -> exists s2:(map ident
Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip). Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip).
Inductive fmla := Inductive fmla :=
| Fterm : expr -> fmla . | Fterm : expr -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla .
Definition eval_fmla(s:(map ident Z)) (f:fmla): Prop := Set Implicit Arguments.
Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
match f with match f with
| (Fterm e) => ~ ((eval_expr s e) = 0%Z) | (Fterm e) => ~ ((eval_expr s e) = 0%Z)
| (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
| (Fnot f1) => ~ (eval_fmla s f1)
end. end.
Unset Implicit Arguments.
Parameter subst_expr: expr -> ident -> expr -> expr. Parameter subst_expr: expr -> ident -> expr -> expr.
...@@ -128,21 +144,37 @@ Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr), ...@@ -128,21 +144,37 @@ Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t)) ((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
e)). e)).
Definition subst(f:fmla) (x:ident) (t:expr): fmla := Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
match f with match f with
| (Fterm e) => (Fterm (subst_expr e x t)) | (Fterm e) => (Fterm (subst_expr e x t))
| (Fand f1 f2) => (Fand (subst f1 x t) (subst f2 x t))
| (Fnot f1) => (Fnot (subst f1 x t))
end. end.
Unset Implicit Arguments.
(* YOU MAY EDIT THE CONTEXT BELOW *) (* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *)
Theorem eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr), Theorem eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
(eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f). (eval_fmla s (subst f x t)) <-> (eval_fmla (set s x (eval_expr s t)) f).
(* YOU MAY EDIT THE PROOF BELOW *) (* YOU MAY EDIT THE PROOF BELOW *)
induction f; unfold eval_fmla, subst in *. induction f.
intros x t H. unfold eval_fmla, subst in *.
rewrite <- eval_subst_expr; auto. intros x t.
rewrite <- eval_subst_expr; tauto.
simpl.
intros x t.
rewrite IHf1.
rewrite IHf2.
tauto.
simpl.
intros x t.
rewrite IHf.
tauto.
Qed. Qed.
(* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *)
......
...@@ -326,21 +326,35 @@ ...@@ -326,21 +326,35 @@
</goal> </goal>
<goal <goal
name="eval_subst" name="eval_subst"
sum="75fe9028dd520dcb211e6cde21feb1a6" sum="41c9426526820307330065d8ac78c17c"
proved="true" proved="true"
expanded="false" expanded="false"
shape="aeval_fmlaasetV0V2aeval_exprV0V3V1Iaeval_fmlaV0asubstV1V2V3F"> shape="aeval_fmlaasetV0V2aeval_exprV0V3V1qaeval_fmlaV0asubstV1V2V3F">
<proof <proof
prover="coq" prover="coq"
timelimit="5" timelimit="5"
edited="imp_Imp_eval_subst_2.v" edited="imp_Imp_eval_subst_2.v"
obsolete="false"> obsolete="false">
<result status="valid" time="0.66"/> <result status="valid" time="0.53"/>
</proof>
</goal>
<goal
name="skip_rule"
sum="dfcd50b4105bd2ae7cd329453fdbc909"
proved="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
<proof
prover="coq"
timelimit="3"
edited="imp_Imp_skip_rule_1.v"
obsolete="false">
<result status="valid" time="0.67"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="assign_rule" name="assign_rule"
sum="12f9657b1c525075d56bcf69c77110b1" sum="d492b0a1117c6083520f1a99f602c05b"
proved="true" proved="true"
expanded="false" expanded="false"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F"> shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
...@@ -349,12 +363,12 @@ ...@@ -349,12 +363,12 @@
timelimit="5" timelimit="5"
edited="imp_Imp_assign_rule_1.v" edited="imp_Imp_assign_rule_1.v"
obsolete="false"> obsolete="false">
<result status="valid" time="0.74"/> <result status="valid" time="0.55"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="seq_rule" name="seq_rule"
sum="298c63994d40d9ae8da8b97a6309eed1" sum="a5e519277ce236964d153818a92437e6"
proved="true" proved="true"
expanded="false" expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F"> shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
...@@ -363,7 +377,7 @@ ...@@ -363,7 +377,7 @@
timelimit="3" timelimit="3"
edited="imp_Imp_seq_rule_2.v" edited="imp_Imp_seq_rule_2.v"
obsolete="false"> obsolete="false">
<result status="valid" time="0.54"/> <result status="valid" time="0.51"/>
</proof> </proof>
<proof <proof
prover="z3" prover="z3"
...@@ -373,6 +387,20 @@ ...@@ -373,6 +387,20 @@
<result status="valid" time="0.07"/> <result status="valid" time="0.07"/>
</proof> </proof>
</goal> </goal>
<goal
name="if_rule"
sum="72ad5869a02dbc44921cf038f2f2959e"
proved="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
<proof
prover="coq"
timelimit="3"
edited="imp_Imp_if_rule_1.v"
obsolete="false">
<result status="valid" time="0.51"/>
</proof>
</goal>
</theory> </theory>
</file> </file>
</why3session> </why3session>
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