Dyck words example completed (thanks to Martin)

parent 87fe8329
(** Checking that a word is a Dyck word
Authors: Martin Clochard (École Normale Supérieure)
Jean-Christophe Filliâtre (CNRS)
*)
theory Dyck
use export list.List
......@@ -19,12 +25,6 @@ theory Dyck
lemma dyck_word_first:
forall w: word. dyck w ->
match w with Nil -> true | Cons c _ -> c = L end
(*(* Concatenation of dyck words is a dyck word. *)
lemma dyck_concat : forall w1 w2:word. dyck w1 -> dyck w2 -> dyck (w1 ++ w2)
lemma dyck_decomp:
forall w1 w2: word. dyck (w1 ++ w2) -> dyck w1 -> dyck w2*)
end
......@@ -38,10 +38,10 @@ module Check
(* A fall of a word is a decomposition p ++ s with p a dyck word
and s a word not starting by L. *)
predicate fall (p s:word) = dyck p /\
predicate fall (p s: word) = dyck p /\
match s with Cons L _ -> false | _ -> true end
let rec lemma same_prefix (p s s2:word) : unit
let rec lemma same_prefix (p s s2: word) : unit
requires { p ++ s = p ++ s2 }
ensures { s = s2 }
variant { p }
......@@ -49,27 +49,31 @@ module Check
(* Compute the fall decomposition, if it exists. As a side-effect,
prove its unicity. *)
let rec is_dyck_rec (ghost p:ref word) (w: word) : word
let rec is_dyck_rec (ghost p: ref word) (w: word) : word
ensures { w = !p ++ result && fall !p result &&
(forall p2 s: word. w = p2 ++ s /\ fall p2 s -> p2 = !p && s = result) }
writes { p }
raises { Failure -> (forall p s:word. w = p ++ s -> not fall p s) }
raises { Failure -> forall p s: word. w = p ++ s -> not fall p s }
variant { length w }
=
match w with
| Cons L w0 -> let ghost p0 = ref Nil in
| Cons L w0 ->
let ghost p0 = ref Nil in
match is_dyck_rec p0 w0 with
| Cons _ w1 -> assert { forall p s p1 p2:word.
dyck p /\ w = p ++ s /\ dyck p1 /\ dyck p2 /\
p = Cons L (p1 ++ Cons R p2) ->
w0 = p1 ++ (Cons R (p2 ++ s)) && p1 = !p0 && w1 = p2 ++ s };
| Cons _ w1 ->
assert { forall p s p1 p2: word.
dyck p /\ w = p ++ s /\ dyck p1 /\ dyck p2 /\
p = Cons L (p1 ++ Cons R p2) ->
w0 = p1 ++ (Cons R (p2 ++ s)) && p1 = !p0 && w1 = p2 ++ s };
let ghost p1 = ref Nil in
let w = is_dyck_rec p1 w1 in
p := Cons L (!p0 ++ Cons R !p1);
w
| _ -> raise Failure
| _ ->
raise Failure
end
| _ -> p := Nil; w
| _ ->
p := Nil; w
end
let is_dyck (w: word) : bool
......
......@@ -37,7 +37,7 @@
shape="CtaNilainfix =V1aLaConsVwV0IadyckV0F">
<proof
prover="0"
timelimit="5"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
......@@ -48,13 +48,13 @@
<theory
name="Check"
locfile="../dyck.mlw"
loclnum="31" loccnumb="7" loccnume="12"
loclnum="25" loccnumb="7" loccnume="12"
verified="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter same_prefix"
locfile="../dyck.mlw"
loclnum="44" loccnumb="16" loccnume="27"
loclnum="38" loccnumb="16" loccnume="27"
expl="VC for same_prefix"
sum="dcb14e08e8ab6eb15dd9cb50d01a00e3"
proved="true"
......@@ -76,22 +76,22 @@
<goal
name="WP_parameter is_dyck_rec"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="VC for is_dyck_rec"
sum="aa0df784a36bf5978f98ef8738357366"
proved="true"
expanded="false"
expanded="true"
shape="CNCfaConsaLwtwV3AadyckV2Iainfix =V0ainfix ++V2V3FINCfaConsaLwtwV5AadyckV4Iainfix =V1ainfix ++V4V5FACNCfaConsaLwtwV10AadyckV9Iainfix =V0ainfix ++V9V10FINCfaConsaLwtwV12AadyckV11Iainfix =V8ainfix ++V11V12FAainfix =V17V14Aainfix =V16V15ICfaConsaLwtwV17AadyckV16Aainfix =V0ainfix ++V16V17FACfaConsaLwtwV14AadyckV15Aainfix =V0ainfix ++V15V14Iainfix =V15aConsaLainfix ++V6aConsaRV13FIainfix =V19V14Aainfix =V18V13ICfaConsaLwtwV19AadyckV18Aainfix =V8ainfix ++V18V19FACfaConsaLwtwV14AadyckV13Aainfix =V8ainfix ++V13V14FFAainfix &lt;alengthV8alengthV0Aainfix &lt;=c0alengthV0Aainfix =V8ainfix ++V23V21Aainfix =V22V6Aainfix =V1ainfix ++V22aConsaRainfix ++V23V21Iainfix =V20aConsaLainfix ++V22aConsaRV23AadyckV23AadyckV22Aainfix =V0ainfix ++V20V21AadyckV20FaConswVNCfaConsaLwtwV25AadyckV24Iainfix =V0ainfix ++V24V25FwV7Iainfix =V27V7Aainfix =V26V6ICfaConsaLwtwV27AadyckV26Aainfix =V1ainfix ++V26V27FACfaConsaLwtwV7AadyckV6Aainfix =V1ainfix ++V6V7FFAainfix &lt;alengthV1alengthV0Aainfix &lt;=c0alengthV0aConsaLVainfix =V30V0Aainfix =V29V28ICfaConsaLwtwV30AadyckV29Aainfix =V0ainfix ++V29V30FACfaConsaLwtwV0AadyckV28Aainfix =V0ainfix ++V28V0Iainfix =V28aNilFwV0F">
<label
name="expl:VC for is_dyck_rec"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter is_dyck_rec.1"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="1. variant decrease"
sum="8d59955d0cdfa70927e377f831339388"
proved="true"
......@@ -111,7 +111,7 @@
<goal
name="WP_parameter is_dyck_rec.2"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="2. assertion"
sum="44b912b899b7205df34db3c68fbbd659"
proved="true"
......@@ -126,7 +126,7 @@
<goal
name="WP_parameter is_dyck_rec.2.1"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="1. assertion"
sum="9461cee86e8dd1c4d009f897b5423676"
proved="true"
......@@ -146,7 +146,7 @@
<goal
name="WP_parameter is_dyck_rec.2.2"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="2. assertion"
sum="1031183809e838e2083b2a3c7b10a1a7"
proved="true"
......@@ -166,7 +166,7 @@
<goal
name="WP_parameter is_dyck_rec.2.3"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="3. assertion"
sum="fd41447065433779408f31182f8004cc"
proved="true"
......@@ -188,7 +188,7 @@
<goal
name="WP_parameter is_dyck_rec.3"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="3. variant decrease"
sum="f64a473b39d7b6c94ffeb2d5ed9a38a5"
proved="true"
......@@ -208,7 +208,7 @@
<goal
name="WP_parameter is_dyck_rec.4"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="4. postcondition"
sum="a4a91515fb10492def2aa51e162aabec"
proved="true"
......@@ -223,7 +223,7 @@
<goal
name="WP_parameter is_dyck_rec.4.1"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="1."
sum="f6357b93bd6cb9b67ae3eaf768e71765"
proved="true"
......@@ -243,7 +243,7 @@
<goal
name="WP_parameter is_dyck_rec.4.2"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="2."
sum="0d01ea738ccfa434c229d408824839be"
proved="true"
......@@ -263,7 +263,7 @@
<goal
name="WP_parameter is_dyck_rec.4.3"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="3."
sum="7b6c7777254aa03e368c88ab594b9d76"
proved="true"
......@@ -283,7 +283,7 @@
<goal
name="WP_parameter is_dyck_rec.4.4"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="4."
sum="df9ab1962df417b17dff9774acb19a37"
proved="true"
......@@ -303,7 +303,7 @@
<goal
name="WP_parameter is_dyck_rec.4.5"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="5."
sum="4d7cce234f9316c0043fc707a30cad44"
proved="true"
......@@ -325,7 +325,7 @@
<goal
name="WP_parameter is_dyck_rec.5"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="5. exceptional postcondition"
sum="3fa156323d7a0af9730c4a575c886d6a"
proved="true"
......@@ -339,17 +339,17 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.40"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="WP_parameter is_dyck_rec.6"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="6. exceptional postcondition"
sum="b244c068ac534114b7446b80a646d385"
proved="true"
expanded="false"
expanded="true"
shape="exceptional postconditionCCtaConswVNCfaConsaLwtwV6AadyckV5Iainfix =V0ainfix ++V5V6FwV3Iainfix =V8V3Aainfix =V7V2ICfaConsaLwtwV8AadyckV7Aainfix =V1ainfix ++V7V8FACfaConsaLwtwV3AadyckV2Aainfix =V1ainfix ++V2V3FFaConsaLVtwV0F">
<label
name="expl:VC for is_dyck_rec"/>
......@@ -359,13 +359,13 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.84"/>
<result status="valid" time="0.73"/>
</proof>
</goal>
<goal
name="WP_parameter is_dyck_rec.7"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="7. exceptional postcondition"
sum="d328ca41623634dd81d4a44e60f48de0"
proved="true"
......@@ -385,7 +385,7 @@
<goal
name="WP_parameter is_dyck_rec.8"
locfile="../dyck.mlw"
loclnum="52" loccnumb="10" loccnume="21"
loclnum="46" loccnumb="10" loccnume="21"
expl="8. postcondition"
sum="1ac2a9e2e8fdcbba9737253c9e5543cd"
proved="true"
......@@ -407,22 +407,22 @@
<goal
name="WP_parameter is_dyck"
locfile="../dyck.mlw"
loclnum="75" loccnumb="6" loccnume="13"
loclnum="73" loccnumb="6" loccnume="13"
expl="VC for is_dyck"
sum="830c3c98dc4b022a03c03137f89c804e"
proved="true"
expanded="false"
expanded="true"
shape="NadyckV0INCfaConsaLwtwV2AadyckV1Iainfix =V0ainfix ++V1V2FACadyckV0aNilNadyckV0wV4Iainfix =V6V4Aainfix =V5V3ICfaConsaLwtwV6AadyckV5Aainfix =V0ainfix ++V5V6FACfaConsaLwtwV4AadyckV3Aainfix =V0ainfix ++V3V4FFF">
<label
name="expl:VC for is_dyck"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter is_dyck.1"
locfile="../dyck.mlw"
loclnum="75" loccnumb="6" loccnume="13"
loclnum="73" loccnumb="6" loccnume="13"
expl="1. postcondition"
sum="2c36f7905682ba526cdf6307072a527b"
proved="true"
......@@ -442,31 +442,724 @@
<goal
name="WP_parameter is_dyck.2"
locfile="../dyck.mlw"
loclnum="75" loccnumb="6" loccnume="13"
loclnum="73" loccnumb="6" loccnume="13"
expl="2. postcondition"
sum="eb92aff55628b8eea351095a10b269d8"
proved="true"
expanded="false"
expanded="true"
shape="postconditionCtaNilNadyckV0wV2Iainfix =V4V2Aainfix =V3V1ICfaConsaLwtwV4AadyckV3Aainfix =V0ainfix ++V3V4FACfaConsaLwtwV2AadyckV1Aainfix =V0ainfix ++V1V2FFF">
<label
name="expl:VC for is_dyck"/>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.64"/>
</proof>
<metas
proved="true"
expanded="true">
<ts_pos
name="real"
arity="0"
id="2"
ip_theory="BuiltIn">
<ip_library
name="why3"/>
<ip_qualid
name="real"/>
</ts_pos>
<ts_pos
name="bool"
arity="0"
id="3"
ip_theory="Bool">
<ip_library
name="why3"/>
<ip_qualid
name="bool"/>
</ts_pos>
<ts_pos
name="tuple0"
arity="0"
id="20"
ip_theory="Tuple0">
<ip_library
name="why3"/>
<ip_qualid
name="tuple0"/>
</ts_pos>
<ts_pos
name="unit"
arity="0"
id="21"
ip_theory="Unit">
<ip_library
name="why3"/>
<ip_qualid
name="unit"/>
</ts_pos>
<ts_pos
name="word"
arity="0"
id="4278"
ip_theory="Dyck">
<ip_qualid
name="word"/>
</ts_pos>
<ts_pos
name="ref"
arity="1"
id="4300"
ip_theory="Ref">
<ip_library
name="ref"/>
<ip_qualid
name="ref"/>
</ts_pos>
<ls_pos
name="infix ="
id="10"
ip_theory="BuiltIn">
<ip_library
name="why3"/>
<ip_qualid
name="infix ="/>
</ls_pos>
<ls_pos
name="zero"
id="159"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="zero"/>
</ls_pos>
<ls_pos
name="one"
id="160"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="one"/>
</ls_pos>
<ls_pos
name="infix &lt;"
id="161"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="infix &lt;"/>
</ls_pos>
<ls_pos
name="infix &gt;"
id="164"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="infix &gt;"/>
</ls_pos>
<ls_pos
name="infix &lt;="
id="173"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="infix &lt;="/>
</ls_pos>
<ls_pos
name="infix +"
id="1253"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="infix +"/>
</ls_pos>
<ls_pos
name="prefix -"
id="1254"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="prefix -"/>
</ls_pos>
<ls_pos
name="infix *"
id="1255"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="infix *"/>
</ls_pos>
<ls_pos
name="infix -"
id="1303"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="infix -"/>
</ls_pos>
<ls_pos
name="infix &gt;="
id="1323"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="infix &gt;="/>
</ls_pos>
<ls_pos
name="length"
id="2183"
ip_theory="Length">
<ip_library
name="list"/>
<ip_qualid
name="length"/>
</ls_pos>
<ls_pos
name="prefix !"
id="4306"
ip_theory="Ref">
<ip_library
name="ref"/>
<ip_qualid
name="prefix !"/>
</ls_pos>
<ls_pos
name="fall"
id="4449"
ip_theory="Check">
<ip_qualid
name="fall"/>
</ls_pos>
<pr_pos
name="Assoc"
id="1256"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CommutativeGroup"/>
<ip_qualid
name="Assoc"/>
</pr_pos>
<pr_pos
name="Unit_def_l"
id="1263"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CommutativeGroup"/>
<ip_qualid
name="Unit_def_l"/>
</pr_pos>
<pr_pos
name="Unit_def_r"
id="1266"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CommutativeGroup"/>
<ip_qualid
name="Unit_def_r"/>
</pr_pos>
<pr_pos
name="Inv_def_l"
id="1269"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CommutativeGroup"/>
<ip_qualid
name="Inv_def_l"/>
</pr_pos>
<pr_pos
name="Inv_def_r"
id="1272"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CommutativeGroup"/>
<ip_qualid
name="Inv_def_r"/>
</pr_pos>
<pr_pos
name="Comm"
id="1275"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CommutativeGroup"/>
<ip_qualid
name="Comm"/>
<ip_qualid
name="Comm"/>
</pr_pos>
<pr_pos
name="Assoc"
id="1280"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Assoc"/>
<ip_qualid
name="Assoc"/>
</pr_pos>
<pr_pos
name="Mul_distr_l"
id="1287"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Mul_distr_l"/>
</pr_pos>
<pr_pos
name="Mul_distr_r"
id="1294"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Mul_distr_r"/>
</pr_pos>
<pr_pos
name="Comm"
id="1312"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Comm"/>
<ip_qualid
name="Comm"/>
</pr_pos>
<pr_pos
name="Unitary"
id="1317"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Unitary"/>
</pr_pos>
<pr_pos
name="NonTrivialRing"
id="1320"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="NonTrivialRing"/>
</pr_pos>
<pr_pos
name="Refl"
id="1332"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Refl"/>
</pr_pos>
<pr_pos
name="Trans"
id="1335"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Trans"/>
</pr_pos>
<pr_pos
name="Antisymm"
id="1342"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Antisymm"/>
</pr_pos>
<pr_pos
name="Total"
id="1347"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="Total"/>
</pr_pos>
<pr_pos
name="ZeroLessOne"
id="1352"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="ZeroLessOne"/>
</pr_pos>
<pr_pos
name="CompatOrderAdd"
id="1353"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CompatOrderAdd"/>
</pr_pos>
<pr_pos
name="CompatOrderMult"
id="1360"
ip_theory="Int">
<ip_library
name="int"/>
<ip_qualid
name="CompatOrderMult"/>
</pr_pos>
<pr_pos
name="Length_nonnegative"
id="2193"
ip_theory="Length">
<ip_library
name="list"/>
<ip_qualid
name="Length_nonnegative"/>
</pr_pos>
<pr_pos
name="Length_nil"
id="2196"
ip_theory="Length">
<ip_library
name="list"/>
<ip_qualid
name="Length_nil"/>
</pr_pos>
<pr_pos
name="Append_length"
id="3694"
ip_theory="Append">
<ip_library
name="list"/>
<ip_qualid
name="Append_length"/>
</pr_pos>
<pr_pos
name="mem_append"
id="3699"
ip_theory="Append">
<ip_library
name="list"/>
<ip_qualid
name="mem_append"/>
</pr_pos>
<pr_pos
name="mem_decomp"
id="3706"
ip_theory="Append">
<ip_library
name="list"/>
<ip_qualid
name="mem_decomp"/>
</pr_pos>
<pr_pos
name="dyck_word_first"
id="4288"
ip_theory="Dyck">
<ip_qualid
name="dyck_word_first"/>
</pr_pos>
<pr_pos
name="same_prefix"
id="4563"
ip_theory="Check">
<ip_qualid
name="same_prefix"/>
</pr_pos>
<meta
name="remove_logic">