Commit 784887ff authored by Andrei Paskevich's avatar Andrei Paskevich

repair more session

parent d56bc53c
This diff is collapsed.
......@@ -2,11 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="6" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<file name="../skew_heaps.mlw" expanded="true">
<theory name="Heap" sum="c1911f1af713ae3f21f7eec8f1ca4c26" expanded="true">
<theory name="Heap" sum="c1911f1af713ae3f21f7eec8f1ca4c26">
</theory>
<theory name="SkewHeaps" sum="6a91e994a989db6c2b9e7e80ad197512" expanded="true">
<goal name="WP_parameter root_is_min" expl="VC for root_is_min">
......@@ -27,10 +26,10 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter root_is_min.6" expl="6. postcondition">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter root_is_min.7" expl="7. postcondition">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter root_is_min.8" expl="8. variant decrease">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -39,10 +38,10 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter root_is_min.10" expl="10. postcondition">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter root_is_min.11" expl="11. postcondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......@@ -52,7 +51,7 @@
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter size" expl="VC for size" expanded="true">
<goal name="WP_parameter size" expl="VC for size">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter get_min" expl="VC for get_min">
......@@ -74,7 +73,7 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter merge.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -89,7 +88,7 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.8" expl="8. postcondition">
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="0"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter merge.9" expl="9. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -101,7 +100,7 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.12" expl="12. postcondition">
<proof prover="1"><result status="timeout" time="5.98"/></proof>
<proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter merge.13" expl="13. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -116,7 +115,7 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.17" expl="17. postcondition">
<proof prover="1"><result status="timeout" time="5.99"/></proof>
<proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter merge.18" expl="18. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -168,7 +167,7 @@
</transf>
</goal>
</theory>
<theory name="HeapSort" sum="f7ae733aad5436fe0a747259d57989ba">
<theory name="HeapSort" sum="f7ae733aad5436fe0a747259d57989ba" expanded="true">
<goal name="WP_parameter heapsort" expl="VC for heapsort">
<transf name="split_goal_wp">
<goal name="WP_parameter heapsort.1" expl="1. postcondition">
......@@ -235,13 +234,13 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter heapsort.22" expl="22. assertion">
<proof prover="2"><result status="valid" time="3.32"/></proof>
<proof prover="0"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter heapsort.23" expl="23. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter heapsort.24" expl="24. loop invariant preservation">
<proof prover="0"><result status="valid" time="4.67"/></proof>
<proof prover="0"><result status="valid" time="1.84"/></proof>
</goal>
<goal name="WP_parameter heapsort.25" expl="25. postcondition">
<proof prover="1"><result status="valid" time="0.00"/></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 list.List.
Require list.Length.
Require list.Mem.
Require list.Nth.
Require option.Option.
Require list.NthLength.
Require list.Append.
Require list.NthLengthAppend.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Definition pal {a:Type} {a_WT:WhyType a} (x:(list a)) (n:Z): Prop :=
forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((list.Nth.nth i
x) = (list.Nth.nth ((n - 1%Z)%Z - i)%Z x)).
(* Why3 goal *)
Theorem WP_parameter_palindrome_rec : forall {a:Type} {a_WT:WhyType a},
forall (x:(list a)) (y:(list a)),
((list.Length.length y) <= (list.Length.length x))%Z -> forall (x1:a)
(x2:(list a)), (y = (Init.Datatypes.cons x1 x2)) -> forall (x3:a)
(x4:(list a)), (x2 = (Init.Datatypes.cons x3 x4)) -> forall (x5:a)
(x6:(list a)), (x = (Init.Datatypes.cons x5 x6)) ->
(((list.Length.length x4) <= (list.Length.length x6))%Z -> ((exists i:Z,
((0%Z <= i)%Z /\ (i < (list.Length.length x4))%Z) /\ ~ ((list.Nth.nth i
x6) = (list.Nth.nth (((list.Length.length x4) - 1%Z)%Z - i)%Z x6))) ->
exists i:Z, ((0%Z <= i)%Z /\ (i < (list.Length.length y))%Z) /\
~ ((list.Nth.nth i
x) = (list.Nth.nth (((list.Length.length y) - 1%Z)%Z - i)%Z x)))).
(* Why3 intros a a_WT x y h1 x1 x2 h2 x3 x4 h3 x5 x6 h4 h5 (i,((h6,h7),h8)). *)
intros a a_WT x y h1 x1 x2 h2 x3 x4 h3 x5 x6 h4 hl (i,(hi1,hi2)).
subst.
exists (i+1)%Z; intuition.
unfold Length.length. fold Length.length.
omega.
unfold Length.length in *. fold Length.length in *.
assert (Nth.nth (i+1) (x5 :: x6) = Nth.nth i x6).
unfold Nth.nth; fold Nth.nth.
generalize (Zeq_bool_eq (i+1) 0).
destruct (Zeq_bool (i+1) 0).
intuition.
elimtype False.
omega.
intuition.
replace (i+1-1)%Z with i by omega. auto.
replace (1 + (1 + Length.length x4) - 1 - (i + 1))%Z
with (1 + Length.length x4 - 1 - i)%Z
in H1 by omega.
assert (Nth.nth (1 + Length.length x4 - 1 - i) (x5 :: x6) =
Nth.nth (Length.length x4 - 1 - i) x6).
unfold Nth.nth; fold Nth.nth.
generalize (Zeq_bool_eq (1 + Length.length x4 - 1 - i) 0).
destruct (Zeq_bool (1 + Length.length x4 - 1 - i) 0).
intuition; elimtype False; omega.
intuition.
replace (1 + Length.length x4 - 1 - i - 1)%Z with (Length.length x4 - 1 - i)%Z
by omega; auto.
congruence.
Qed.
......@@ -7,11 +7,11 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../there_and_back_again.mlw" expanded="true">
<theory name="Convolution" sum="0084ef5f9dda6927c0a802becfca201e">
<theory name="Convolution" sum="0084ef5f9dda6927c0a802becfca201e" expanded="true">
<goal name="WP_parameter convolution_rec" expl="VC for convolution_rec">
<transf name="split_goal_wp">
<goal name="WP_parameter convolution_rec.1" expl="1. postcondition">
<proof prover="1" timelimit="120"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter convolution_rec.2" expl="2. variant decrease">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -39,65 +39,64 @@
</goal>
</theory>
<theory name="Palindrome" sum="e8c3059e9bc20f2f24405e97d0118adf" expanded="true">
<goal name="WP_parameter palindrome_rec" expl="VC for palindrome_rec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter palindrome_rec.1" expl="1. postcondition" expanded="true">
<goal name="WP_parameter palindrome_rec" expl="VC for palindrome_rec">
<transf name="split_goal_wp">
<goal name="WP_parameter palindrome_rec.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.2" expl="2. postcondition" expanded="true">
<goal name="WP_parameter palindrome_rec.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.3" expl="3. postcondition" expanded="true">
<goal name="WP_parameter palindrome_rec.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="1.20"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.4" expl="4. postcondition" expanded="true">
<goal name="WP_parameter palindrome_rec.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.5" expl="5. unreachable point" expanded="true">
<proof prover="3"><result status="valid" time="0.13"/></proof>
<goal name="WP_parameter palindrome_rec.5" expl="5. unreachable point">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.6" expl="6. variant decrease" expanded="true">
<goal name="WP_parameter palindrome_rec.6" expl="6. variant decrease">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.7" expl="7. precondition" expanded="true">
<goal name="WP_parameter palindrome_rec.7" expl="7. precondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.8" expl="8. assertion" expanded="true">
<proof prover="0" edited="there_and_back_again_Palindrome_WP_parameter_palindrome_rec_1.v"><result status="unknown" time="1.22"/></proof>
<goal name="WP_parameter palindrome_rec.8" expl="8. assertion">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.9" expl="9. postcondition" expanded="true">
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<goal name="WP_parameter palindrome_rec.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.10" expl="10. postcondition" expanded="true">
<proof prover="2"><result status="timeout" time="4.99"/></proof>
<goal name="WP_parameter palindrome_rec.10" expl="10. postcondition">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.11" expl="11. exceptional postcondition" expanded="true">
<goal name="WP_parameter palindrome_rec.11" expl="11. exceptional postcondition">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.12" expl="12. unreachable point" expanded="true">
<goal name="WP_parameter palindrome_rec.12" expl="12. unreachable point">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.13" expl="13. exceptional postcondition" expanded="true">
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<goal name="WP_parameter palindrome_rec.13" expl="13. exceptional postcondition">
<proof prover="0" edited="there_and_back_again_Palindrome_WP_parameter_palindrome_rec_2.v"><result status="valid" time="1.15"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.14" expl="14. unreachable point" expanded="true">
<goal name="WP_parameter palindrome_rec.14" expl="14. unreachable point">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter palindrome" expl="VC for palindrome" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter palindrome.1" expl="1. precondition" expanded="true">
<goal name="WP_parameter palindrome" expl="VC for palindrome">
<transf name="split_goal_wp">
<goal name="WP_parameter palindrome.1" expl="1. precondition">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter palindrome.2" expl="2. postcondition" expanded="true">
<goal name="WP_parameter palindrome.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter palindrome.3" expl="3. postcondition" expanded="true">
<goal name="WP_parameter palindrome.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
......
......@@ -11,6 +11,10 @@ Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -21,29 +25,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
......@@ -57,33 +63,27 @@ Definition lex (x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop :=
| (s2, d2) => ((list.Length.length s1) < (list.Length.length s2))%Z \/
(((list.Length.length s1) = (list.Length.length s2)) /\ match (s1,
s2) with
| ((cons h1 _), (cons h2 _)) => ((d2 < d1)%Z /\ (d1 <= h1)%Z) /\
(h1 = h2)
| ((Init.Datatypes.cons h1 _), (Init.Datatypes.cons h2 _)) =>
(d2 < d1)%Z /\ ((d1 <= h1)%Z /\ (h1 = h2))
| _ => False
end)
end
end.
(* Why3 goal *)
Theorem WP_parameter_build : forall (s:(list Z)), forall (result:tree)
(result1:(list Z)), (s = (List.app (depths 0%Z result) result1)) ->
match result1 with
| nil => True
| _ => forall (t:tree), ~ ((depths 0%Z t) = s)
end.
(* Why3 intros s result result1 h1. *)
(result1:(list Z)), (s = (Init.Datatypes.app (depths 0%Z
result) result1)) -> ((exists w:Z, (exists w1:(list Z),
(result1 = (Init.Datatypes.cons w w1)))) -> forall (t:tree), ~ ((depths 0%Z
t) = s)).
intros s result result1 h1 (w,(w1,h2)) t.
subst.
intuition.
destruct result1; auto.
intro t.
replace (depths 0 t) with (app (depths 0 t) nil).
intros.
subst s.
generalize (depths_unique _ _ _ _ _ H0).
replace (depths 0 t) with (app (depths 0 t) nil) in H.
generalize (depths_unique _ _ _ _ _ H).
intuition.
discriminate H2.
apply Append.Append_l_nil.
Qed.
......@@ -78,23 +78,21 @@ Theorem WP_parameter_build_rec : forall (d:Z) (s:(list Z)), forall (x:Z)
((forall (t:tree) (s':(list Z)), ~ ((Init.Datatypes.app (depths (d + 1%Z)%Z
t) s') = result1)) -> forall (t:tree) (s':(list Z)),
~ ((Init.Datatypes.app (depths d t) s') = s)))).
(* Why3 intros d s x x1 h1 h2 h3 result result1 h4 h5 t s'. *)
intros d s x x1 h1 h2 h3 result result1 h4 h5 t s'.
subst.
intuition.
destruct s; intuition.
rename z into h. rename s into t.
rename result into l. rename result1 into sl.
destruct t1 as [_|t1 t2].
(* t1 = Leaf *)
simpl in H3.
injection H3.
destruct t as [_|t1 t2].
(* t = Leaf *)
simpl in H.
injection H.
omega.
(* t1 = Node t1 t2 *)
simpl in H3.
rewrite <- Append.Append_assoc in H3.
rewrite H1 in H3.
generalize (depths_unique _ _ _ _ _ H3).
(* t = Node t1 t2 *)
simpl in H.
rewrite <- Append.Append_assoc in H.
rewrite h4 in H.
generalize (depths_unique _ _ _ _ _ H).
intuition.
subst t1.
apply (H2 t2 s'); intuition.
apply (h5 t2 s'); intuition.
Qed.
......@@ -11,6 +11,10 @@ Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -21,29 +25,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
......@@ -57,34 +63,30 @@ Definition lex (x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop :=
| (s2, d2) => ((list.Length.length s1) < (list.Length.length s2))%Z \/
(((list.Length.length s1) = (list.Length.length s2)) /\ match (s1,
s2) with
| ((cons h1 _), (cons h2 _)) => ((d2 < d1)%Z /\ (d1 <= h1)%Z) /\
(h1 = h2)
| ((Init.Datatypes.cons h1 _), (Init.Datatypes.cons h2 _)) =>
(d2 < d1)%Z /\ ((d1 <= h1)%Z /\ (h1 = h2))
| _ => False
end)
end
end.
(* Why3 goal *)
Theorem WP_parameter_build_rec : forall (d:Z) (s:(list Z)),
match s with
| nil => True
| (cons h t) => (~ (h < d)%Z) -> ((~ (h = d)) -> ((forall (t1:tree)
(s':(list Z)), ~ ((List.app (depths (d + 1%Z)%Z t1) s') = s)) ->
forall (t1:tree) (s':(list Z)), ~ ((List.app (depths d t1) s') = s)))
end.
(* Why3 intros d s. *)
Theorem WP_parameter_build_rec : forall (d:Z) (s:(list Z)), forall (x:Z)
(x1:(list Z)), (s = (Init.Datatypes.cons x x1)) -> ((~ (x < d)%Z) ->
((~ (x = d)) -> ((forall (t:tree) (s':(list Z)),
~ ((Init.Datatypes.app (depths (d + 1%Z)%Z t) s') = s)) -> forall (t:tree)
(s':(list Z)), ~ ((Init.Datatypes.app (depths d t) s') = s)))).
intros d s x x1 h1 h2 h3 h4 t s'.
subst.
intuition.
destruct s; intuition.
rename z into h. rename s into t.
destruct t1 as [_|t1 t2].
(* t1 = Leaf *)
simpl in H2.
injection H2.
destruct t as [_|t1 t2].
(* t = Leaf *)
simpl in H.
injection H.
omega.
(* t1 = Node t1 t2 *)
simpl in H2.
rewrite <- Append.Append_assoc in H2.
apply (H1 _ _ H2).
(* t = Node t1 t2 *)
simpl in H.
rewrite <- Append.Append_assoc in H.
apply (h4 _ _ H).
Qed.
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