Commit a4500c76 authored by MARCHE Claude's avatar MARCHE Claude

Fixed simple mistakes in nightly bench

parent f1ec0759
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter set : forall (a:Type), Type.
(* Why3 assumption *)
Definition rel (a:Type) (b:Type) := (set (a* b)%type).
(* Why3 goal *)
Theorem t : True.
trivial.
Qed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="hoare_logic/imp/why3session.xml">
name="examples/hoare_logic/imp/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -36,13 +36,13 @@
expanded="true">
<theory
name="Imp"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="2" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="ident_eq_dec"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="8" loccnumb="6" loccnume="18"
sum="1d2fa1307a90cfa4436e58ca8c4baa8b"
proved="true"
......@@ -75,7 +75,7 @@
</goal>
<goal
name="check_skip"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="32" loccnumb="6" loccnume="16"
sum="f37d9a038124492ded7dcc13c243bca4"
proved="true"
......@@ -100,7 +100,7 @@
</goal>
<goal
name="Test13"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="59" loccnumb="7" loccnume="13"
sum="79514e82972fcb9fb181a42bdd168a5d"
proved="true"
......@@ -149,7 +149,7 @@
</goal>
<goal
name="Test42"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="63" loccnumb="7" loccnume="13"
sum="2233d910dd871f7629fbd14fe21880a0"
proved="true"
......@@ -198,7 +198,7 @@
</goal>
<goal
name="Test55"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="68" loccnumb="7" loccnume="13"
sum="81f3d89dbb17dd5616d61c746363e319"
proved="true"
......@@ -223,7 +223,7 @@
</goal>
<goal
name="Ass42"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="112" loccnumb="7" loccnume="12"
sum="d79dafb4b123bd6d405249e2aeae999f"
proved="true"
......@@ -248,7 +248,7 @@
</goal>
<goal
name="If42"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="119" loccnumb="7" loccnume="11"
sum="2cf4b33a87e77dc3113cb2270027977a"
proved="true"
......@@ -265,7 +265,7 @@
</goal>
<goal
name="progress"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="131" loccnumb="8" loccnume="16"
sum="e135ae75103f2c596782b1e202f4ddb9"
proved="true"
......@@ -283,10 +283,10 @@
</goal>
<goal
name="many_steps_seq_rec"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="148" loccnumb="6" loccnume="24"
sum="aeea567425648bcdc8f7b73f26164f74"
proved="false"
proved="true"
expanded="true"
shape="amany_stepsV6V5V1aSskipAamany_stepsV0V4V6aSskipEIainfix =V2aSseqV4V5FIainfix =V3aSskipIamany_stepsV0V2V1V3F">
<proof
......@@ -294,14 +294,14 @@
timelimit="3"
memlimit="0"
edited="imp_Imp_many_steps_seq_rec_1.v"
obsolete="true"
archived="false"><undone/>
obsolete="false"
archived="false">
<result status="valid" time="0.49"/>
</proof>
</goal>
<goal
name="many_steps_seq"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="155" loccnumb="6" loccnume="20"
sum="2c0574f92883e7d75abeab91219a5f5b"
proved="true"
......@@ -334,7 +334,7 @@
</goal>
<goal
name="eval_subst_expr"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="185" loccnumb="6" loccnume="21"
sum="10a08076cbde9ff3d47f3756599d4269"
proved="true"
......@@ -352,7 +352,7 @@
</goal>
<goal
name="eval_subst"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="197" loccnumb="6" loccnume="16"
sum="9ed41003e65c3b0d6e018246af7e1910"
proved="true"
......@@ -370,7 +370,7 @@
</goal>
<goal
name="skip_rule"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="210" loccnumb="6" loccnume="15"
sum="86491dec98ad2def2cf841b1953670b7"
proved="true"
......@@ -388,7 +388,7 @@
</goal>
<goal
name="assign_rule"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="213" loccnumb="6" loccnume="17"
sum="6aa1e2def89b26b124b052e7f456e1e6"
proved="true"
......@@ -406,7 +406,7 @@
</goal>
<goal
name="seq_rule"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="217" loccnumb="6" loccnume="14"
sum="edb979d62451e4d773f12b17ae4d29e1"
proved="true"
......@@ -432,7 +432,7 @@
</goal>
<goal
name="if_rule"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="222" loccnumb="6" loccnume="13"
sum="a7f2179c110652afa53bf980838b7b3c"
proved="true"
......@@ -450,7 +450,7 @@
</goal>
<goal
name="while_rule_rec"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="238" loccnumb="6" loccnume="20"
sum="568be4c208959ba07400c93bf7827c92"
proved="false"
......@@ -468,7 +468,7 @@
</goal>
<goal
name="while_rule"
locfile="hoare_logic/imp/../imp.why"
locfile="examples/hoare_logic/imp/../imp.why"
loclnum="246" loccnumb="6" loccnume="16"
sum="42400857028ab4b823953cc85e3146df"
proved="true"
......
......@@ -18,7 +18,9 @@ type value = Vvoid | Vint int | Vbool bool
type operator = Oplus | Ominus | Omult | Ole
type ident = int
type refident
type refident
lemma eq_refident_dec : forall x y:refident. x=y \/ x <>y
constant result : ident = (-1)
......
This diff is collapsed.
......@@ -35,6 +35,9 @@ Definition ident := Z.
Parameter refident : Type.
Axiom eq_refident_dec : forall (x:refident) (y:refident), (x = y) \/
~ (x = y).
(* Why3 assumption *)
Inductive term :=
| Tvalue : value -> term
......@@ -199,13 +202,13 @@ rewrite (subst_term_def (Tvar z) x v'); auto.
generalize (subst_term_def (Tderef r) x v').
intros (h1,h2).
case (Z_eq_dec x r).
case (eq_refident_dec x r).
intro; subst r; rewrite h1; simpl; auto.
rewrite Select_eq; auto.
intro; rewrite h2; simpl; auto.
rewrite Select_neq; auto.
rewrite (subst_term_def (Tbin e1 o e2) r v'); simpl; auto.
rewrite (subst_term_def (Tbin e1 o e2) x v'); simpl; auto.
elim H; intros.
rewrite IHe1; auto.
rewrite IHe2; auto.
......
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