Commit 36a8e008 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

porting example residual

parent 6fc0c80f
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
Require list.Length.
Require int.Int.
Require list.Mem.
Require list.Append.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
Parameter eq: char -> char -> Prop.
Axiom eq_spec : forall (x:char) (y:char), (eq x y) <-> (x = y).
(* Why3 assumption *)
Inductive regexp :=
| Empty : regexp
| Epsilon : regexp
| Char : char -> regexp
| Alt : regexp -> regexp -> regexp
| Concat : regexp -> regexp -> regexp
| Star : regexp -> regexp.
Axiom regexp_WhyType : WhyType regexp.
Existing Instance regexp_WhyType.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
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
(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 (Init.Datatypes.app w1 w2) (Star r))).
Axiom inversion_mem_star_gen : forall (c:char) (w:(list char)) (r:regexp)
(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'))).
Axiom inversion_mem_star : forall (c:char) (w:(list char)) (r:regexp), (mem
(Init.Datatypes.cons c w) (Star r)) -> exists w1:(list char),
exists w2:(list char), (w = (Init.Datatypes.app w1 w2)) /\ ((mem
(Init.Datatypes.cons c w1) r) /\ (mem w2 (Star r))).
(* Why3 goal *)
Theorem VC_residual : forall (r:regexp) (c:char), forall (result:regexp),
(exists x:regexp, (exists x1:regexp, (r = (Concat x x1)) /\ ((mem
Init.Datatypes.nil x) /\ exists o:regexp, (forall (w:(list char)), (mem w
o) <-> (mem (Init.Datatypes.cons c w) x1)) /\ exists o1:regexp,
(forall (w:(list char)), (mem w o1) <-> (mem (Init.Datatypes.cons c w)
x)) /\ (result = (Alt (Concat o1 x1) o))))) -> forall (w:(list char)), (mem
w result) -> (mem (Init.Datatypes.cons c w) r).
intros r c result (x,(x1,(h1,(h2,(o,(h3,(o1,(h4,h5)))))))) w h6.
subst.
inversion h6; subst; clear h6.
inversion H1; subst; clear H1.
replace ((c :: (w1 ++ w2))%list) with (((c :: w1) ++ w2)%list) by auto.
apply mem_concat; auto.
now rewrite <- h4.
replace ((c :: w)%list) with ((nil ++ (c :: w))%list) by auto.
apply mem_concat; auto.
now rewrite <- h3.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
Require list.Length.
Require int.Int.
Require list.Mem.
Require list.Append.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
Parameter eq: char -> char -> Prop.
Axiom eq_spec : forall (x:char) (y:char), (eq x y) <-> (x = y).
(* Why3 assumption *)
Inductive regexp :=
| Empty : regexp
| Epsilon : regexp
| Char : char -> regexp
| Alt : regexp -> regexp -> regexp
| Concat : regexp -> regexp -> regexp
| Star : regexp -> regexp.
Axiom regexp_WhyType : WhyType regexp.
Existing Instance regexp_WhyType.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
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
(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 (Init.Datatypes.app w1 w2) (Star r))).
Axiom inversion_mem_star_gen : forall (c:char) (w:(list char)) (r:regexp)
(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'))).
Axiom inversion_mem_star : forall (c:char) (w:(list char)) (r:regexp), (mem
(Init.Datatypes.cons c w) (Star r)) -> exists w1:(list char),
exists w2:(list char), (w = (Init.Datatypes.app w1 w2)) /\ ((mem
(Init.Datatypes.cons c w1) r) /\ (mem w2 (Star r))).
(* Why3 goal *)
Theorem VC_residual : forall (r:regexp) (c:char), forall (result:regexp),
(exists x:regexp, (exists x1:regexp, (r = (Concat x x1)) /\ ((mem
Init.Datatypes.nil x) /\ exists o:regexp, (forall (w:(list char)), (mem w
o) <-> (mem (Init.Datatypes.cons c w) x1)) /\ exists o1:regexp,
(forall (w:(list char)), (mem w o1) <-> (mem (Init.Datatypes.cons c w)
x)) /\ (result = (Alt (Concat o1 x1) o))))) -> forall (w:(list char)), (mem
(Init.Datatypes.cons c w) r) -> (mem w result).
intros r c result (x,(x1,(h1,(h2,(o,(h3,(o1,(h4,h5)))))))) w h6.
subst.
inversion h6; subst; clear h6.
destruct w1.
simpl in H.
subst w2.
rewrite <- h3 in H3.
now apply mem_altr.
simpl in H.
inversion H; subst; clear H.
apply mem_altl.
apply mem_concat; auto.
now rewrite h4.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
Require list.Length.
Require int.Int.
Require list.Mem.
Require list.Append.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
Parameter eq: char -> char -> Prop.
Axiom eq_spec : forall (x:char) (y:char), (eq x y) <-> (x = y).
(* Why3 assumption *)
Inductive regexp :=
| Empty : regexp
| Epsilon : regexp
| Char : char -> regexp
| Alt : regexp -> regexp -> regexp
| Concat : regexp -> regexp -> regexp
| Star : regexp -> regexp.
Axiom regexp_WhyType : WhyType regexp.
Existing Instance regexp_WhyType.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
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
(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 (Init.Datatypes.app w1 w2) (Star r))).
Axiom inversion_mem_star_gen : forall (c:char) (w:(list char)) (r:regexp)
(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'))).
Axiom inversion_mem_star : forall (c:char) (w:(list char)) (r:regexp), (mem
(Init.Datatypes.cons c w) (Star r)) -> exists w1:(list char),
exists w2:(list char), (w = (Init.Datatypes.app w1 w2)) /\ ((mem
(Init.Datatypes.cons c w1) r) /\ (mem w2 (Star r))).
(* Why3 goal *)
Theorem VC_residual : forall (r:regexp) (c:char), forall (result:regexp),
(exists x:regexp, (exists x1:regexp, (r = (Concat x x1)) /\ ((~ (mem
Init.Datatypes.nil x)) /\ exists o:regexp, (forall (w:(list char)), (mem w
o) <-> (mem (Init.Datatypes.cons c w) x)) /\ (result = (Concat o x1))))) ->
forall (w:(list char)), (mem (Init.Datatypes.cons c w) r) -> (mem w
result).
intros r c result (x,(x1,(h1,(h2,(o,(h3,h4)))))) w h5.
subst.
inversion h5; subst; clear h5.
destruct w1; auto.
now simpl.
simpl in H.
inversion H; subst; clear H.
apply mem_concat; auto.
now rewrite <- h3 in H2.
Qed.
......@@ -2,11 +2,13 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../residual.mlw" expanded="true">
<theory name="Residuals" sum="345b06a8e452e711591978029113ee89" expanded="true">
<theory name="Residuals" sum="f0d76f6b4f252cc41de77f4d2b96cf73" expanded="true">
<goal name="VC accepts_epsilon" expl="VC for accepts_epsilon">
<transf name="split_goal_wp">
<goal name="VC accepts_epsilon.1" expl="1. variant decrease">
......@@ -22,30 +24,15 @@
<proof prover="9"><result status="valid" time="0.01" steps="53"/></proof>
</goal>
<goal name="VC accepts_epsilon.5" expl="5. postcondition">
<proof prover="9"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="VC accepts_epsilon.6" expl="6. postcondition">
<proof prover="9"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC accepts_epsilon.7" expl="7. postcondition">
<proof prover="9"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
<goal name="VC accepts_epsilon.8" expl="8. postcondition">
<proof prover="9"><result status="valid" time="0.02" steps="92"/></proof>
</goal>
<goal name="VC accepts_epsilon.9" expl="9. postcondition">
<transf name="split_goal_wp">
<goal name="VC accepts_epsilon.9.1" expl="1. VC for accepts_epsilon">
<proof prover="10"><result status="valid" time="0.01"/></proof>
<goal name="VC accepts_epsilon.5.1" expl="1. VC for accepts_epsilon">
<proof prover="10"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC accepts_epsilon.9.2" expl="2. VC for accepts_epsilon">
<proof prover="9"><result status="valid" time="0.06" steps="285"/></proof>
<goal name="VC accepts_epsilon.5.2" expl="2. VC for accepts_epsilon">
<proof prover="9"><result status="valid" time="0.05" steps="428"/></proof>
</goal>
</transf>
</goal>
<goal name="VC accepts_epsilon.10" expl="10. postcondition">
<proof prover="9"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="inversion_mem_star_gen">
......@@ -69,7 +56,7 @@
<proof prover="9"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="inversion_mem_star_gen.7" expl="7.">
<proof prover="6" steplimit="1"><result status="valid" time="0.17"/></proof>
<proof prover="6"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
</goal>
......@@ -97,114 +84,59 @@
<proof prover="9"><result status="valid" time="0.01" steps="52"/></proof>
</goal>
<goal name="VC residual.7" expl="7. postcondition">
<proof prover="9"><result status="valid" time="0.03" steps="139"/></proof>
</goal>
<goal name="VC residual.8" expl="8. postcondition">
<proof prover="9"><result status="valid" time="0.04" steps="144"/></proof>
</goal>
<goal name="VC residual.9" expl="9. postcondition">
<proof prover="9"><result status="valid" time="0.07" steps="328"/></proof>
</goal>
<goal name="VC residual.10" expl="10. postcondition">
<proof prover="9"><result status="valid" time="0.07" steps="241"/></proof>
</goal>
<goal name="VC residual.11" expl="11. postcondition">
<transf name="split_goal_wp">
<goal name="VC residual.11.1" expl="1. postcondition">
<transf name="inversion_pr">
<goal name="VC residual.11.1.1" expl="1. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC residual.11.1.2" expl="2. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC residual.11.1.3" expl="3. VC for residual">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="VC residual.11.1.3.1" expl="1. VC for residual">
<transf name="introduce_premises">
<goal name="VC residual.11.1.3.1.1" expl="1. VC for residual">
<proof prover="9"><result status="valid" time="0.15" steps="661"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC residual.11.1.4" expl="4. VC for residual">
<proof prover="6"><result status="valid" time="0.08"/></proof>
<goal name="VC residual.7.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="VC residual.7.1.1" expl="1. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="135"/></proof>
</goal>
<goal name="VC residual.11.1.5" expl="5. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="21"/></proof>
<goal name="VC residual.7.1.2" expl="2. postcondition">
<proof prover="2"><result status="valid" time="0.04" steps="135"/></proof>
</goal>
<goal name="VC residual.11.1.6" expl="6. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="21"/></proof>
<goal name="VC residual.7.1.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.06" steps="215"/></proof>
</goal>
<goal name="VC residual.11.1.7" expl="7. VC for residual">
<proof prover="9"><result status="valid" time="0.02" steps="25"/></proof>
<goal name="VC residual.7.1.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.05" steps="144"/></proof>
</goal>
</transf>
</goal>
<goal name="VC residual.11.2" expl="2. postcondition">
<transf name="inversion_pr">
<goal name="VC residual.11.2.1" expl="1. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC residual.11.2.2" expl="2. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC residual.11.2.3" expl="3. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC residual.11.2.4" expl="4. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC residual.11.2.5" expl="5. VC for residual">
<proof prover="6"><result status="valid" time="0.12"/></proof>
<goal name="VC residual.7.1.5" expl="5. postcondition">
<proof prover="0" edited="residual_Residuals_VC_residual_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC residual.11.2.6" expl="6. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
<goal name="VC residual.7.1.6" expl="6. postcondition">
<proof prover="9" timelimit="1"><result status="valid" time="0.33" steps="1135"/></proof>
</goal>
<goal name="VC residual.11.2.7" expl="7. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="15"/></proof>
<goal name="VC residual.7.1.7" expl="7. postcondition">
<proof prover="9" timelimit="10" memlimit="4000"><result status="valid" time="0.74" steps="1575"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC residual.12" expl="12. postcondition">
<transf name="split_goal_wp">
<goal name="VC residual.12.1" expl="1. postcondition">
<proof prover="9"><result status="valid" time="0.41" steps="1135"/></proof>
</goal>
<goal name="VC residual.12.2" expl="2. postcondition">
<transf name="inversion_pr">
<goal name="VC residual.12.2.1" expl="1. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
<goal name="VC residual.7.2" expl="2. postcondition">
<transf name="split_goal_wp">
<goal name="VC residual.7.2.1" expl="1. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="55"/></proof>
</goal>
<goal name="VC residual.12.2.2" expl="2. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
<goal name="VC residual.7.2.2" expl="2. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="55"/></proof>
</goal>
<goal name="VC residual.12.2.3" expl="3. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="11"/></proof>
<goal name="VC residual.7.2.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="137"/></proof>
</goal>
<goal name="VC residual.12.2.4" expl="4. VC for residual">
<proof prover="9"><result status="valid" time="0.01" steps="11"/></proof>
<goal name="VC residual.7.2.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="74"/></proof>
</goal>
<goal name="VC residual.12.2.5" expl="5. VC for residual">
<proof prover="6"><result status="valid" time="0.15"/></proof>
<goal name="VC residual.7.2.5" expl="5. postcondition">
<proof prover="0" edited="residual_Residuals_VC_residual_2.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="VC residual.12.2.6" expl="6. VC for residual">
<proof prover="9"><result status="valid" time="0.00" steps="11"/></proof>
<goal name="VC residual.7.2.6" expl="6. postcondition">
<proof prover="0" edited="residual_Residuals_VC_residual_3.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="VC residual.12.2.7" expl="7. VC for residual">
<proof prover="9"><result status="valid" time="0.00" steps="13"/></proof>
<goal name="VC residual.7.2.7" expl="7. postcondition">
<proof prover="10"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC residual.13" expl="13. postcondition">
<proof prover="9"><result status="valid" time="0.07" steps="264"/></proof>
</goal>
</transf>
</goal>
<goal name="VC decide_mem" expl="VC for decide_mem">
......@@ -213,10 +145,7 @@
<proof prover="9"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC decide_mem.2" expl="2. postcondition">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC decide_mem.3" expl="3. postcondition">
<proof prover="9"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......
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