gallery: simplified proofs using induction

parent 08d1a75c
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Axiom set : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) -> (mem x s2).
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set
a))).
Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
(empty :(set a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
s)))%Z).
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set1: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set1 m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set1 m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
Parameter v: (set vertex).
Parameter g_succ: vertex -> (set vertex).
Axiom G_succ_sound : forall (x:vertex), (subset (g_succ x) v).
Parameter weight: vertex -> vertex -> Z.
Axiom Weight_nonneg : forall (x:vertex) (y:vertex), (0%Z <= (weight x y))%Z.
(* Why3 assumption *)
Definition min(m:vertex) (q:(set vertex)) (d:(map vertex Z)): Prop := (mem m
q) /\ forall (x:vertex), (mem x q) -> ((get d m) <= (get d x))%Z.
(* Why3 assumption *)
Inductive path : vertex -> vertex -> Z -> Prop :=
| Path_nil : forall (x:vertex), (path x x 0%Z)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex), forall (d:Z),
(path x y d) -> ((mem z (g_succ y)) -> (path x z (d + (weight y z))%Z)).
Axiom Length_nonneg : forall (x:vertex) (y:vertex), forall (d:Z), (path x y
d) -> (0%Z <= d)%Z.
(* Why3 assumption *)
Definition shortest_path(x:vertex) (y:vertex) (d:Z): Prop := (path x y d) /\
forall (d':Z), (path x y d') -> (d <= d')%Z.
Axiom Path_inversion : forall (src:vertex) (v1:vertex), forall (d:Z),
(path src v1 d) -> (((v1 = src) /\ (d = 0%Z)) \/ exists v':vertex,
(path src v' (d - (weight v' v1))%Z) /\ (mem v1 (g_succ v'))).
Axiom Path_shortest_path : forall (src:vertex) (v1:vertex), forall (d:Z),
(path src v1 d) -> exists d':Z, (shortest_path src v1 d') /\ (d' <= d)%Z.
Axiom Main_lemma : forall (src:vertex) (v1:vertex), forall (d:Z), (path src
v1 d) -> ((~ (shortest_path src v1 d)) -> exists v':vertex, exists d':Z,
(shortest_path src v' d') /\ ((mem v1 (g_succ v')) /\ ((d' + (weight v'
v1))%Z < d)%Z)).
Require Import Why3. Ltac ae := why3 "alt-ergo".
(* Why3 goal *)
Theorem Completeness_lemma : forall (s:(set vertex)), (forall (v1:vertex),
(mem v1 s) -> forall (w:vertex), (mem w (g_succ v1)) -> (mem w s)) ->
forall (src:vertex), (mem src s) -> forall (dst:vertex), forall (d:Z),
(path src dst d) -> (mem dst s).
intros s h1 src h2 dst d h3.
induction h3; trivial.
ae.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Axiom set : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) -> (mem x s2).
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set
a))).
Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
(empty :(set a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
s)))%Z).
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set1: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set1 m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set1 m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
Parameter v: (set vertex).
Parameter g_succ: vertex -> (set vertex).
Axiom G_succ_sound : forall (x:vertex), (subset (g_succ x) v).
Parameter weight: vertex -> vertex -> Z.
Axiom Weight_nonneg : forall (x:vertex) (y:vertex), (0%Z <= (weight x y))%Z.
(* Why3 assumption *)
Definition min(m:vertex) (q:(set vertex)) (d:(map vertex Z)): Prop := (mem m
q) /\ forall (x:vertex), (mem x q) -> ((get d m) <= (get d x))%Z.
(* Why3 assumption *)
Inductive path : vertex -> vertex -> Z -> Prop :=
| Path_nil : forall (x:vertex), (path x x 0%Z)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex), forall (d:Z),
(path x y d) -> ((mem z (g_succ y)) -> (path x z (d + (weight y z))%Z)).
(* Why3 goal *)
Theorem Length_nonneg : forall (x:vertex) (y:vertex), forall (d:Z), (path x y
d) -> (0%Z <= d)%Z.
induction 1; try omega.
generalize (Weight_nonneg y z); omega.
Qed.
......@@ -3,13 +3,15 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="15" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="30" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC3" version="2.2" timelimit="15" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<file name="../dijkstra.mlw" expanded="true">
<theory name="DijkstraShortestPath" sum="189655dd1069a89e93126ccf56986f6e" expanded="true">
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<file name="../dijkstra.mlw">
<theory name="DijkstraShortestPath" sum="afa04af5de17123ae1f4e1a114b65d61">
<goal name="WP_parameter relax" expl="VC for relax">
<transf name="split_goal_wp">
<goal name="WP_parameter relax.1" expl="1. postcondition">
......@@ -27,22 +29,36 @@
</transf>
</goal>
<goal name="Length_nonneg">
<proof prover="1" edited="dijkstra_DijkstraShortestPath_Length_nonneg_1.v"><result status="valid" time="1.07"/></proof>
<transf name="induction_pr">
<goal name="Length_nonneg.1" expl="1.">
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Length_nonneg.2" expl="2.">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="Path_inversion">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Path_shortest_path">
<proof prover="1" edited="dijkstra_DijkstraShortestPath_Path_shortest_path_1.v"><result status="valid" time="1.26"/></proof>
<proof prover="1" timelimit="5" edited="dijkstra_DijkstraShortestPath_Path_shortest_path_1.v"><result status="valid" time="1.26"/></proof>
</goal>
<goal name="Main_lemma">
<proof prover="3"><result status="valid" time="1.72"/></proof>
</goal>
<goal name="Completeness_lemma">
<proof prover="1" edited="dijkstra_DijkstraShortestPath_Completeness_lemma_1.v"><result status="valid" time="1.17"/></proof>
<transf name="induction_pr">
<goal name="Completeness_lemma.1" expl="1.">
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Completeness_lemma.2" expl="2.">
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code" expl="VC for shortest_path_code" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter shortest_path_code" expl="VC for shortest_path_code">
<transf name="split_goal_wp">
<goal name="WP_parameter shortest_path_code.1" expl="1. loop invariant init">
<proof prover="2"><result status="valid" time="0.20"/></proof>
<proof prover="5"><result status="valid" time="0.14"/></proof>
......@@ -136,7 +152,7 @@
<proof prover="3"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.7" expl="7.">
<proof prover="1" timelimit="30" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="12.63"/></proof>
<proof prover="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="12.63"/></proof>
</goal>
</transf>
</goal>
......@@ -170,8 +186,8 @@
<goal name="WP_parameter shortest_path_code.16" expl="16. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.17" expl="17. loop invariant preservation" expanded="true">
<proof prover="1" timelimit="30" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="2.40"/></proof>
<goal name="WP_parameter shortest_path_code.17" expl="17. loop invariant preservation">
<proof prover="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="2.40"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.18" expl="18. loop variant decrease">
<proof prover="3"><result status="valid" time="0.07"/></proof>
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist nil nil 0%Z)
| dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (cons a w1) w2 (n + 1%Z)%Z)
| dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist w1 (cons a w2) (n + 1%Z)%Z)
| dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (cons a w1) (cons a w2) n).
(* Why3 assumption *)
Definition min_dist (w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
(* Why3 assumption *)
Fixpoint last_char (a:char) (u:(list char)) {struct u}: char :=
match u with
| nil => a
| (cons c u') => (last_char c u')
end.
(* Why3 assumption *)
Fixpoint but_last (a:char) (u:(list char)) {struct u}: (list char) :=
match u with
| nil => nil
| (cons c u') => (cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((List.app (but_last a u) (cons (last_char a u) nil)) = (cons a u)).
Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
exists b:char, ((List.app v (cons b nil)) = (cons a u)) /\
((list.Length.length v) = (list.Length.length u)).
Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z)
(a:char), (dist w1 w'2 m) -> forall (w2:(list char)),
(w'2 = (cons a w2)) -> exists u1:(list char), exists v1:(list char),
exists k:Z, (w1 = (List.app u1 v1)) /\ ((dist v1 w2 k) /\
((k + (list.Length.length u1))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> (dist w2 w1 n).
Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
(a:char), (dist (cons a w1) w2 m) -> exists u2:(list char),
exists v2:(list char), exists k:Z, (w2 = (List.app u2 v2)) /\ ((dist w1 v2
k) /\ ((k + (list.Length.length u2))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_concat_left : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist (List.app u v) w
((list.Length.length u) + n)%Z).
Axiom dist_concat_right : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist v (List.app u w)
((list.Length.length u) + n)%Z).
Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
(n:Z), (min_dist w1 w2 n) -> (min_dist (cons a w1) (cons a w2) n).
Axiom min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char)
(b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (cons a w1) w2 p) ->
((min_dist w1 (cons b w2) m) -> (min_dist (cons a w1) (cons b w2)
((Zmin m p) + 1%Z)%Z))).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w nil
n) -> (min_dist (cons a w) nil (n + 1%Z)%Z).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist nil w
(list.Length.length w)).
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter suffix: (@array char char_WhyType) -> Z -> (list char).
Axiom suffix_nil : forall (a:(@array char char_WhyType)), ((suffix a
(length a)) = nil).
Axiom suffix_cons : forall (a:(@array char char_WhyType)) (i:Z),
((0%Z <= i)%Z /\ (i < (length a))%Z) -> ((suffix a i) = (cons (get a