Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 56540862 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

example residuals: replace a Coq proof by induction_pr/E-prover

parent c5b302be
......@@ -11,10 +11,6 @@ Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
......@@ -66,6 +62,7 @@ Theorem WP_parameter_residual : forall (r:regexp) (c:char),
(forall (w:(list char)), (mem w o) <-> (mem (Init.Datatypes.cons c w)
x)) -> forall (w:(list char)), (mem w (Concat o r)) <-> (mem
(Init.Datatypes.cons c w) r).
(* Why3 intros r c x h1 o h2 w. *)
intros r c x h1 o h2 w.
subst.
intuition.
......
......@@ -11,10 +11,6 @@ Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
......@@ -67,6 +63,7 @@ Theorem WP_parameter_residual : forall (r:regexp) (c:char), forall (x:regexp)
forall (o:regexp), (forall (w:(list char)), (mem w o) <-> (mem
(Init.Datatypes.cons c w) x)) -> forall (w:(list char)), (mem w (Concat o
x1)) <-> (mem (Init.Datatypes.cons c w) r)).
(* Why3 intros r c x x1 h1 result h2 h3 o h4 w. *)
intros r c x x1 h1 result h2 h3 o h4 w.
subst.
intuition.
......
(* This file is generated by Why3's Coq 8.4 driver *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -30,25 +30,27 @@ Existing Instance regexp_WhyType.
Definition word := (list char).
(* Why3 assumption *)
Inductive mem : (list char) -> regexp -> Prop :=
| mem_eps : (mem nil Epsilon)
| mem_char : forall (c:char), (mem (cons c nil) (Char c))
Inductive mem: (list char) -> regexp -> Prop :=
| mem_eps : (mem Init.Datatypes.nil Epsilon)
| mem_char : forall (c:char), (mem
(Init.Datatypes.cons c Init.Datatypes.nil) (Char c))
| mem_altl : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem w r1) ->
(mem w (Alt r1 r2))
| mem_altr : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem w r2) ->
(mem w (Alt r1 r2))
| mem_concat : forall (w1:(list char)) (w2:(list char)) (r1:regexp)
(r2:regexp), (mem w1 r1) -> ((mem w2 r2) -> (mem (List.app w1 w2)
(Concat r1 r2)))
| mems1 : forall (r:regexp), (mem nil (Star r))
(r2:regexp), (mem w1 r1) -> ((mem w2 r2) -> (mem
(Init.Datatypes.app w1 w2) (Concat r1 r2)))
| mems1 : forall (r:regexp), (mem Init.Datatypes.nil (Star r))
| mems2 : forall (w1:(list char)) (w2:(list char)) (r:regexp), (mem w1
r) -> ((mem w2 (Star r)) -> (mem (List.app w1 w2) (Star r))).
r) -> ((mem w2 (Star r)) -> (mem (Init.Datatypes.app w1 w2) (Star r))).
(* Why3 goal *)
Theorem inversion_mem_star_gen : forall (c:char) (w:(list char)) (r:regexp)
(w':(list char)) (r':regexp), ((w' = (cons c w)) /\ (r' = (Star r))) ->
((mem w' r') -> exists w1:(list char), exists w2:(list char),
(w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 r'))).
(w':(list char)) (r':regexp), ((w' = (Init.Datatypes.cons c w)) /\
(r' = (Star r))) -> ((mem w' r') -> exists w1:(list char),
exists w2:(list char), (w = (Init.Datatypes.app w1 w2)) /\ ((mem
(Init.Datatypes.cons c w1) r) /\ (mem w2 r'))).
(* Why3 intros c w r w' r' (h1,h2) h3. *)
intros c w r w' r' (h1,h2) h3.
induction h3; try (discriminate h2).
......
......@@ -2,13 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../residual.mlw" expanded="true">
<theory name="Residuals" sum="d48e75533177265727aa3bb0ee9e4495" expanded="true">
<theory name="Residuals" sum="bb1ad89a4746c41bbd1cbc8ac17769db" expanded="true">
<goal name="WP_parameter accepts_epsilon" expl="VC for accepts_epsilon">
<transf name="split_goal_wp">
<goal name="WP_parameter accepts_epsilon.1" expl="1. postcondition">
......@@ -45,7 +47,7 @@
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.10.2" expl="2. VC for accepts_epsilon">
<proof prover="0" timelimit="60" memlimit="4000"><result status="valid" time="5.83" steps="10703"/></proof>
<proof prover="0" timelimit="60" memlimit="4000"><result status="valid" time="7.82" steps="10703"/></proof>
</goal>
</transf>
</goal>
......@@ -58,13 +60,36 @@
</transf>
</goal>
<goal name="inversion_mem_star_gen">
<proof prover="3" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.85"/></proof>
<proof prover="5" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.70"/></proof>
<transf name="induction_pr">
<goal name="inversion_mem_star_gen.1" expl="1.">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="inversion_mem_star_gen.2" expl="2.">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="inversion_mem_star_gen.3" expl="3.">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="inversion_mem_star_gen.4" expl="4.">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="inversion_mem_star_gen.5" expl="5.">
<proof prover="4"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="inversion_mem_star_gen.6" expl="6.">
<proof prover="4"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="inversion_mem_star_gen.7" expl="7.">
<proof prover="6"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
</goal>
<goal name="inversion_mem_star">
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter residual" expl="VC for residual">
<transf name="split_goal_wp">
<goal name="WP_parameter residual" expl="VC for residual" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter residual.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="89"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -80,7 +105,7 @@
<goal name="WP_parameter residual.4" expl="4. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="51"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.35"/></proof>
<proof prover="2"><result status="valid" time="0.52"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.5" expl="5. variant decrease">
......@@ -106,7 +131,7 @@
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter residual.9" expl="9. postcondition">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_1.v"><result status="valid" time="0.97"/></proof>
<proof prover="5" edited="residual_Residuals_WP_parameter_residual_1.v"><result status="valid" time="0.63"/></proof>
</goal>
<goal name="WP_parameter residual.10" expl="10. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="54"/></proof>
......@@ -114,17 +139,17 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.11" expl="11. postcondition">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_3.v"><result status="valid" time="0.92"/></proof>
<goal name="WP_parameter residual.11" expl="11. postcondition" expanded="true">
<proof prover="5" edited="residual_Residuals_WP_parameter_residual_3.v"><result status="valid" time="0.71"/></proof>
</goal>
<goal name="WP_parameter residual.12" expl="12. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="52"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.77"/></proof>
<proof prover="2"><result status="valid" time="1.62"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.13" expl="13. postcondition">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_2.v"><result status="valid" time="0.84"/></proof>
<goal name="WP_parameter residual.13" expl="13. postcondition" expanded="true">
<proof prover="5" edited="residual_Residuals_WP_parameter_residual_2.v"><result status="valid" time="0.50"/></proof>
</goal>
</transf>
</goal>
......@@ -142,7 +167,7 @@
</transf>
</goal>
</theory>
<theory name="Test" sum="11830df98e6b35d65e46c34ae64f02ca" expanded="true">
<theory name="Test" sum="11830df98e6b35d65e46c34ae64f02ca">
<goal name="WP_parameter test_astar" expl="VC for test_astar">
<transf name="split_goal_wp">
</transf>
......
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