Commit 8f96c0ed authored by MARCHE Claude's avatar MARCHE Claude

Sessions: last updates for coq 8.5

parent 25554264
......@@ -2,28 +2,24 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../flag2.mlw" expanded="true">
<theory name="Flag" sum="886d4458ce409913c292403e0ff44758" expanded="true">
<goal name="nb_occ_split">
<proof prover="0" edited="flag2_WP_Flag_nb_occ_split_1.v"><result status="valid" time="1.28"/></proof>
<proof prover="3" edited="flag2_WP_Flag_nb_occ_split_1.v"><result status="valid" time="1.28"/></proof>
</goal>
<goal name="nb_occ_ext">
<proof prover="0" edited="flag2_Flag_nb_occ_ext_1.v"><result status="valid" time="0.90"/></proof>
<proof prover="3" edited="flag2_Flag_nb_occ_ext_1.v"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="nb_occ_store_outside_up">
<proof prover="0" edited="flag2_WP_Flag_nb_occ_store_outside_up_1.v"><result status="valid" time="1.11"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="nb_occ_store_outside_down">
<proof prover="0" edited="flag2_WP_Flag_nb_occ_store_outside_down_1.v"><result status="valid" time="1.09"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
......@@ -34,7 +30,7 @@
<proof prover="8"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="nb_occ_store_eq_neq">
<proof prover="0" timelimit="10" edited="flag2_WP_Flag_nb_occ_store_eq_neq_1.v"><result status="valid" time="4.04"/></proof>
<proof prover="3" timelimit="10" edited="flag2_WP_Flag_nb_occ_store_eq_neq_1.v"><result status="valid" time="1.65"/></proof>
</goal>
<goal name="nb_occ_store_neq_eq">
<proof prover="7"><result status="valid" time="0.14"/></proof>
......@@ -102,15 +98,11 @@
</goal>
<goal name="WP_parameter dutch_flag.9" expl="9. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.03" steps="23"/></proof>
</goal>
<goal name="WP_parameter dutch_flag.10" expl="10. loop variant decrease">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
......@@ -136,15 +128,11 @@
</goal>
<goal name="WP_parameter dutch_flag.15" expl="15. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter dutch_flag.16" expl="16. loop variant decrease">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
......@@ -170,15 +158,11 @@
</goal>
<goal name="WP_parameter dutch_flag.21" expl="21. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter dutch_flag.22" expl="22. loop variant decrease">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
......@@ -188,7 +172,6 @@
</goal>
<goal name="WP_parameter dutch_flag.24" expl="24. postcondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
......
(* 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.
Require int.Int.
Require option.Option.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Nth.
Require option.Option.
Require list.NthLength.
Require list.Append.
Require list.NthLengthAppend.
......@@ -17,90 +17,84 @@ Require list.NthLengthAppend.
Definition unit := unit.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> 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]].
Implicit Arguments mk_array [[a]].
(* 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
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
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 :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): 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 :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (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))).
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Inductive buffer
(a:Type) {a_WT:WhyType a} :=
| mk_buffer : Z -> Z -> (@array a a_WT) -> (list a) -> buffer a.
(a:Type) :=
| mk_buffer : Z -> Z -> (array a) -> (list a) -> buffer a.
Axiom buffer_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (buffer a).
Existing Instance buffer_WhyType.
Implicit Arguments mk_buffer [[a] [a_WT]].
Implicit Arguments mk_buffer [[a]].
(* Why3 assumption *)
Definition sequence {a:Type} {a_WT:WhyType a} (v:(@buffer
a a_WT)): (list a) := match v with
Definition sequence {a:Type} {a_WT:WhyType a} (v:(buffer a)): (list a) :=
match v with
| (mk_buffer x x1 x2 x3) => x3
end.
(* Why3 assumption *)
Definition data {a:Type} {a_WT:WhyType a} (v:(@buffer a a_WT)): (@array
a a_WT) := match v with
Definition data {a:Type} {a_WT:WhyType a} (v:(buffer a)): (array a) :=
match v with
| (mk_buffer x x1 x2 x3) => x2
end.
(* Why3 assumption *)
Definition len {a:Type} {a_WT:WhyType a} (v:(@buffer a a_WT)): Z :=
Definition len {a:Type} {a_WT:WhyType a} (v:(buffer a)): Z :=
match v with
| (mk_buffer x x1 x2 x3) => x1
end.
(* Why3 assumption *)
Definition first {a:Type} {a_WT:WhyType a} (v:(@buffer a a_WT)): Z :=
Definition first {a:Type} {a_WT:WhyType a} (v:(buffer a)): Z :=
match v with
| (mk_buffer x x1 x2 x3) => x
end.
(* Why3 assumption *)
Definition size {a:Type} {a_WT:WhyType a} (b:(@buffer a a_WT)): Z :=
Definition size {a:Type} {a_WT:WhyType a} (b:(buffer a)): Z :=
(length (data b)).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 3; admit.
(* Why3 goal *)
Theorem WP_parameter_head : forall {a:Type} {a_WT:WhyType a}, forall (b:Z)
(b1:Z) (b2:Z) (b3:(@map.Map.map Z _ a a_WT)) (b4:(list a)),
(((((0%Z <= b)%Z /\ (b < b2)%Z) /\ (((0%Z <= b1)%Z /\ (b1 <= b2)%Z) /\
(b1:Z) (b2:Z) (b3:(map.Map.map Z a)) (b4:(list a)), (((((0%Z <= b)%Z /\
(b < b2)%Z) /\ (((0%Z <= b1)%Z /\ (b1 <= b2)%Z) /\
((b1 = (list.Length.length b4)) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < b1)%Z) -> ((((b + i)%Z < b2)%Z -> ((list.Nth.nth i
b4) = (Some (map.Map.get b3 (b + i)%Z)))) /\
b4) = (Init.Datatypes.Some (map.Map.get b3 (b + i)%Z)))) /\
((0%Z <= ((b + i)%Z - b2)%Z)%Z -> ((list.Nth.nth i
b4) = (Some (map.Map.get b3 ((b + i)%Z - b2)%Z)))))))) /\ (0%Z <= b2)%Z) /\
(0%Z < b1)%Z) -> (((0%Z <= b)%Z /\ (b < b2)%Z) ->
b4) = (Init.Datatypes.Some (map.Map.get b3 ((b + i)%Z - b2)%Z)))))))) /\
(0%Z <= b2)%Z) /\ (0%Z < b1)%Z) -> (((0%Z <= b)%Z /\ (b < b2)%Z) ->
match b4 with
| nil => False
| (cons x _) => ((map.Map.get b3 b) = x)
| Init.Datatypes.nil => False
| (Init.Datatypes.cons x _) => ((map.Map.get b3 b) = x)
end).
(* Why3 intros a a_WT b b1 b2 b3 b4 ((((h1,h2),((h3,h4),(h5,h6))),h7),h8)
(h9,h10). *)
......@@ -112,6 +106,5 @@ omega.
intuition.
generalize (h2d 0%Z). clear h2d.
ae.
Qed.
Admitted.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require option.Option.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Nth.
Require list.NthLength.
Require list.Append.
Require list.NthLengthAppend.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Inductive buffer
(a:Type) :=
| mk_buffer : Z -> Z -> (array a) -> (list a) -> buffer a.
Axiom buffer_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (buffer a).
Existing Instance buffer_WhyType.
Implicit Arguments mk_buffer [[a]].
(* Why3 assumption *)
Definition sequence {a:Type} {a_WT:WhyType a} (v:(buffer a)): (list a) :=
match v with
| (mk_buffer x x1 x2 x3) => x3
end.
(* Why3 assumption *)
Definition data {a:Type} {a_WT:WhyType a} (v:(buffer a)): (array a) :=
match v with
| (mk_buffer x x1 x2 x3) => x2
end.
(* Why3 assumption *)
Definition len {a:Type} {a_WT:WhyType a} (v:(buffer a)): Z :=
match v with
| (mk_buffer x x1 x2 x3) => x1
end.
(* Why3 assumption *)
Definition first {a:Type} {a_WT:WhyType a} (v:(buffer a)): Z :=
match v with
| (mk_buffer x x1 x2 x3) => x
end.
(* Why3 assumption *)
Definition size {a:Type} {a_WT:WhyType a} (b:(buffer a)): Z :=
(length (data b)).
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 5; admit.
(* Why3 goal *)
Theorem WP_parameter_pop : forall {a:Type} {a_WT:WhyType a}, forall (b:Z)
(b1:Z) (b2:Z) (b3:(map.Map.map Z a)) (b4:(list a)), (((((0%Z <= b)%Z /\
(b < b2)%Z) /\ (((0%Z <= b1)%Z /\ (b1 <= b2)%Z) /\
((b1 = (list.Length.length b4)) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < b1)%Z) -> ((((b + i)%Z < b2)%Z -> ((list.Nth.nth i
b4) = (Init.Datatypes.Some (map.Map.get b3 (b + i)%Z)))) /\
((0%Z <= ((b + i)%Z - b2)%Z)%Z -> ((list.Nth.nth i
b4) = (Init.Datatypes.Some (map.Map.get b3 ((b + i)%Z - b2)%Z)))))))) /\
(0%Z <= b2)%Z) /\ (0%Z < b1)%Z) -> forall (x:a) (x1:(list a)),
(b4 = (Init.Datatypes.cons x x1)) -> forall (rho:(list a)), (rho = x1) ->
(((0%Z <= b)%Z /\ (b < b2)%Z) -> forall (rho1:Z), (rho1 = (b1 - 1%Z)%Z) ->
forall (rho2:Z), (rho2 = (b + 1%Z)%Z) -> ((~ (rho2 = b2)) ->
((((0%Z <= rho2)%Z /\ (rho2 < b2)%Z) /\ (((0%Z <= rho1)%Z /\
(rho1 <= b2)%Z) /\ ((rho1 = (list.Length.length rho)) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < rho1)%Z) -> ((((rho2 + i)%Z < b2)%Z ->
((list.Nth.nth i rho) = (Init.Datatypes.Some (map.Map.get b3
(rho2 + i)%Z)))) /\ ((0%Z <= ((rho2 + i)%Z - b2)%Z)%Z -> ((list.Nth.nth i
rho) = (Init.Datatypes.Some (map.Map.get b3
((rho2 + i)%Z - b2)%Z)))))))) -> forall (x2:a) (x3:(list a)),
(b4 = (Init.Datatypes.cons x2 x3)) -> ((map.Map.get b3 b) = x2)))).
(* Why3 intros a a_WT b b1 b2 b3 b4 ((((h1,h2),((h3,h4),(h5,h6))),h7),h8) x
x1 h9 rho h10 (h11,h12) rho1 h13 rho2 h14 h15
((h16,h17),((h18,h19),(h20,h21))) x2 x3 h22. *)
intros a a_WT b b1 b2 b3 b4 ((((h1,h2),((h3,h4),(h5,h6))),h7),h8) x x1 h9 rho
h10 (h11,h12) rho1 h13 rho2 h14 h15 ((h16,h17),((h18,h19),(h20,h21))) x2 x3
h22.
generalize (h6 0)%Z.
ae.
Admitted.
......@@ -22,29 +22,31 @@ Existing Instance tree_WhyType.
(* Why3 assumption *)
Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) :=
match t with
| Leaf => (cons d nil)
| (Node l r) => (List.app (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r))
| Leaf => (Init.Datatypes.cons d Init.Datatypes.nil)
| (Node l r) => (Init.Datatypes.app (depths (d + 1%Z)%Z
l) (depths (d + 1%Z)%Z r))
end.
Axiom depths_head : forall (t:tree) (d:Z), match (depths d
t) with
| (cons x _) => (d <= x)%Z
| nil => False
| (Init.Datatypes.cons x _) => (d <= x)%Z
| Init.Datatypes.nil => False
end.
Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z))
(s2:(list Z)), ((List.app (depths d t1) s1) = (List.app (depths d
t2) s2)) -> ((t1 = t2) /\ (s1 = s2)).
(s2:(list Z)), ((Init.Datatypes.app (depths d
t1) s1) = (Init.Datatypes.app (depths d t2) s2)) -> ((t1 = t2) /\
(s1 = s2)).
Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z))
(s2:(list Z)), ((List.app (depths d1 t) s1) = (List.app (depths d2
t) s2)) -> (d1 = d2).
(s2:(list Z)), ((Init.Datatypes.app (depths d1
t) s1) = (Init.Datatypes.app (depths d2 t) s2)) -> (d1 = d2).
Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
t) = (depths d2 t)) -> (d1 = d2).
Axiom depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z)
(s1:(list Z)), ((List.app (depths d1 t1) s1) = (depths d2 t2)) ->
(s1:(list Z)), ((Init.Datatypes.app (depths d1 t1) s1) = (depths d2 t2)) ->
(d2 <= d1)%Z.
Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
......@@ -53,13 +55,14 @@ Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
(* Why3 assumption *)
Fixpoint forest_depths (f:(list (Z* tree)%type)) {struct f}: (list Z) :=
match f with
| nil => nil
| (cons (d, t) r) => (List.app (depths d t) (forest_depths r))
| Init.Datatypes.nil => Init.Datatypes.nil
| (Init.Datatypes.cons (d, t) r) => (Init.Datatypes.app (depths d
t) (forest_depths r))
end.
Axiom forest_depths_append : forall (f1:(list (Z* tree)%type)) (f2:(list (Z*
tree)%type)),
((forest_depths (List.app f1 f2)) = (List.app (forest_depths f1) (forest_depths f2))).
((forest_depths (Init.Datatypes.app f1 f2)) = (Init.Datatypes.app (forest_depths f1) (forest_depths f2))).
(* Why3 assumption *)
Fixpoint greedy (d:Z) (d1:Z) (t1:tree) {struct t1}: Prop := (~ (d = d1)) /\
......@@ -69,18 +72,21 @@ Fixpoint greedy (d:Z) (d1:Z) (t1:tree) {struct t1}: Prop := (~ (d = d1)) /\
end.
(* Why3 assumption *)
Inductive g : (list (Z* tree)%type) -> Prop :=
| Gnil : (g nil)
| Gone : forall (d:Z) (t:tree), (g (cons (d, t) nil))
Inductive g: (list (Z* tree)%type) -> Prop :=
| Gnil : (g Init.Datatypes.nil)
| Gone : forall (d:Z) (t:tree), (g (Init.Datatypes.cons (d,
t) Init.Datatypes.nil))
| Gtwo : forall (d1:Z) (d2:Z) (t1:tree) (t2:tree) (l:(list (Z*
tree)%type)), (greedy d1 d2 t2) -> ((g (cons (d1, t1) l)) -> (g (cons (
d2, t2) (cons (d1, t1) l)))).
tree)%type)), (greedy d1 d2 t2) -> ((g (Init.Datatypes.cons (d1,
t1) l)) -> (g (Init.Datatypes.cons (d2, t2) (Init.Datatypes.cons (d1,
t1) l)))).
Require Import Why3. Ltac z := why3 "z3" timelimit 5.
Require Import Why3.
Ltac z := why3 "Z3,4.4.0," timelimit 5;admit.
(* Why3 goal *)
Theorem g_append : forall (l1:(list (Z* tree)%type)) (l2:(list (Z*
tree)%type)), (g (List.app l1 l2)) -> (g l1).
tree)%type)), (g (Init.Datatypes.app l1 l2)) -> (g l1).
(* Why3 intros l1 l2 h1. *)
induction l1; simpl.
z.
......@@ -95,6 +101,5 @@ destruct p.
apply Gtwo; auto.
simpl in H1.
z.
Qed.
Admitted.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.Reverse.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Unset Implicit Arguments.
Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil :(list a))) = l).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Unset Implicit Arguments.
Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree .
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree.
Axiom tree_WhyType : WhyType tree.
Existing Instance tree_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) :=
Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) :=
match t with
| Leaf => (Cons d (Nil :(list Z)))
| (Node l r) => (infix_plpl (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r))
| Leaf => (Init.Datatypes.cons d Init.Datatypes.nil)
| (Node l r) => (Init.Datatypes.app (depths (d + 1%Z)%Z
l) (depths (d + 1%Z)%Z r))
end.
Unset Implicit Arguments.
Axiom depths_head : forall (t:tree) (d:Z), match (depths d
t) with
| (Cons x _) => (d <= x)%Z
| Nil => False
| (Init.Datatypes.cons x _) => (d <= x)%Z
| Init.Datatypes.nil => False
end.
Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z))
(s2:(list Z)), ((infix_plpl (depths d t1) s1) = (infix_plpl (depths d t2)
s2)) -> ((t1 = t2) /\ (s1 = s2)).
(s2:(list Z)), ((Init.Datatypes.app (depths d
t1) s1) = (Init.Datatypes.app (depths d t2) s2)) -> ((t1 = t2) /\
(s1 = s2)).
Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list
Z)), ((infix_plpl (depths d1 t) s1) = (infix_plpl (depths d2 t) s2)) ->
(d1 = d2).
Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z))
(s2:(list Z)), ((Init.Datatypes.app (depths d1
t) s1) = (Init.Datatypes.app (depths d2 t) s2)) -> (d1 = d2).
Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
t) = (depths d2 t)) -> (d1 = d2).
Axiom depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z) (s1:(list
Z)), ((infix_plpl (depths d1 t1) s1) = (depths d2 t2)) -> (d2 <= d1)%Z.
Axiom depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z)
(s1:(list Z)), ((Init.Datatypes.app (depths d1 t1) s1) = (depths d2 t2)) ->
(d2 <= d1)%Z.
Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
(* Why3 assumption *)
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
(* Why3 assumption *)
Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop :=
| Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1,
y1