updated proof sessions

parent 43fbb552
......@@ -31,7 +31,6 @@ schorr_waite_via_recursion.mlw
sieve.mlw
sudoku.mlw
sum_of_digits.mlw
there_and_back_again.mlw
topological_sorting.mlw
tortoise_and_hare.mlw
tree_height.mlw
......@@ -47,5 +46,3 @@ vstte10_inverting.mlw
vstte10_search_list.mlw
vstte12_bfs.mlw
vstte12_combinators.mlw
vstte12_ring_buffer.mlw
vstte12_tree_reconstruction.mlw
(* 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.
(* 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)).
Axiom elt : Type.
Parameter elt_WhyType : WhyType elt.
Existing Instance elt_WhyType.
Parameter eq: elt -> elt -> Prop.
Axiom eq_spec : forall (x:elt) (y:elt), (eq x y) <-> (x = y).
(* Why3 goal *)
Theorem VC_palindrome_rec : forall (x:(list elt)) (y:(list elt)),
((list.Length.length y) <= (list.Length.length x))%Z -> forall (x1:elt)
(x2:(list elt)), (y = (Init.Datatypes.cons x1 x2)) -> forall (x3:elt)
(x4:(list elt)), (x2 = (Init.Datatypes.cons x3 x4)) -> forall (x5:elt)
(x6:(list elt)), (x = (Init.Datatypes.cons x5 x6)) -> ((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))).
intros x y h1 x1 x2 h2 x3 x4 h3 x5 x6 h4 (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.
......@@ -21,29 +21,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,8 +59,8 @@ 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
......@@ -76,9 +78,9 @@ Qed.
(* Why3 goal *)
Theorem WP_parameter_harness2 : forall (result:tree), ~ ((depths 0%Z
result) = (cons 1%Z (cons 3%Z (cons 2%Z (cons 2%Z nil))))).
(* Why3 intros result. *)
Theorem VC_harness2 : forall (result:tree), ~ ((depths 0%Z
result) = (Init.Datatypes.cons 1%Z (Init.Datatypes.cons 3%Z (Init.Datatypes.cons 2%Z (Init.Datatypes.cons 2%Z Init.Datatypes.nil))))).
intuition.
destruct result; simpl in H.
discriminate H.
......@@ -128,4 +130,3 @@ omega.
Qed.
......@@ -21,29 +21,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,18 +59,18 @@ 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_harness : forall (result:tree), ((depths 0%Z
result) = (cons 1%Z (cons 3%Z (cons 3%Z (cons 2%Z nil))))) ->
Theorem VC_harness : forall (result:tree), ((depths 0%Z
result) = (Init.Datatypes.cons 1%Z (Init.Datatypes.cons 3%Z (Init.Datatypes.cons 3%Z (Init.Datatypes.cons 2%Z Init.Datatypes.nil))))) ->
(result = (Node Leaf (Node (Node Leaf Leaf) Leaf))).
(* Why3 intros result h1. *)
intuition.
rewrite <- (Append.Append_l_nil (depths 0 result)) in H.
......@@ -79,4 +81,3 @@ generalize (depths_unique _ _ _ _ _ H); intuition.
Qed.
(* 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.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree.
Axiom tree_WhyType : WhyType tree.
Existing Instance tree_WhyType.
(* Why3 assumption *)
Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) :=
match t with
| 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
| (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)), ((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)), ((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)), ((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 lex (x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop :=
match x1 with
| (s1, d1) =>
match x2 with
| (s2, d2) => ((list.Length.length s1) < (list.Length.length s2))%Z \/
(((list.Length.length s1) = (list.Length.length s2)) /\ match (s1,
s2) with
| ((Init.Datatypes.cons h1 _), (Init.Datatypes.cons h2 _)) =>
(d2 < d1)%Z /\ ((d1 <= h1)%Z /\ (h1 = h2))
| _ => False
end)
end
end.
(* Why3 goal *)
Theorem VC_harness : ~ forall (t:tree), ~ ((depths 0%Z
t) = (Init.Datatypes.cons 1%Z (Init.Datatypes.cons 3%Z (Init.Datatypes.cons 3%Z (Init.Datatypes.cons 2%Z Init.Datatypes.nil))))).
intuition.
apply (H (Node Leaf (Node (Node Leaf Leaf) Leaf))).
reflexivity.
Qed.
(* 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.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree.
Axiom tree_WhyType : WhyType tree.
Existing Instance tree_WhyType.
(* Why3 assumption *)
Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) :=
match t with
| 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
| (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)), ((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)), ((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)), ((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 lex (x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop :=
match x1 with
| (s1, d1) =>
match x2 with
| (s2, d2) => ((list.Length.length s1) < (list.Length.length s2))%Z \/
(((list.Length.length s1) = (list.Length.length s2)) /\ match (s1,
s2) with
| ((Init.Datatypes.cons h1 _), (Init.Datatypes.cons h2 _)) =>
(d2 < d1)%Z /\ ((d1 <= h1)%Z /\ (h1 = h2))
| _ => False
end)
end
end.
(* Why3 goal *)
Theorem VC_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 (o:tree) (o1:(list Z)), (s = (Init.Datatypes.app (depths (d + 1%Z)%Z
o) o1)) -> ((forall (t:tree) (s':(list Z)),
~ ((Init.Datatypes.app (depths (d + 1%Z)%Z t) s') = o1)) -> forall (t:tree)
(s':(list Z)), ~ ((Init.Datatypes.app (depths d t) s') = s)))).
(*intros d s x x1 h1 h2 h3 o o1 h4 h5 t s'.*)
intros d s x x1 h1 h2 h3 result result1 h4 h5 t s'.
subst.
intuition.
destruct t as [_|t1 t2].
(* t = Leaf *)
simpl in H.
injection H.
omega.
(* 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 (h5 t2 s'); intuition.
Qed.
(* 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.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree.
Axiom tree_WhyType : WhyType tree.
Existing Instance tree_WhyType.
(* Why3 assumption *)
Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) :=
match t with
| 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
| (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)), ((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)), ((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)), ((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 lex (x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop :=
match x1 with
| (s1, d1) =>
match x2 with
| (s2, d2) => ((list.Length.length s1) < (list.Length.length s2))%Z \/
(((list.Length.length s1) = (list.Length.length s2)) /\ match (s1,
s2) with
| ((Init.Datatypes.cons h1 _), (Init.Datatypes.cons h2 _)) =>
(d2 < d1)%Z /\ ((d1 <= h1)%Z /\ (h1 = h2))
| _ => False
end)
end
end.
(* Why3 goal *)
Theorem VC_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 t as [_|t1 t2].
(* t = Leaf *)
simpl in H.
injection H.
omega.
(* t = Node t1 t2 *)
simpl in H.
rewrite <- Append.Append_assoc in H.
apply (h4 _ _ H).
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* 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