Commit e65a7c20 authored by Martin Clochard's avatar Martin Clochard

remove some (but not all) instances of coq tactic in example

  vstte12_tree_reconstruction
parent c1fc50f7
......@@ -222,7 +222,7 @@ module ZipperBased
(* an easy lemma on [g] *)
lemma g_append:
forall l1 l2: list (int, tree). g (l1 ++ l2) -> g l1
forall l1 [@induction] l2: list (int, tree). g (l1 ++ l2) -> g l1
(* key lemma for completeness: whenever we fail because [right] is empty,
we have to prove that there is no solution
......
......@@ -8,9 +8,6 @@ Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -22,47 +19,53 @@ Existing Instance tree_WhyType.
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))
| 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
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_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 :
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_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_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)).
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 :=
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)
| (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.
......@@ -78,8 +81,13 @@ Qed.
(* Why3 goal *)
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))))).
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))))).
(* Why3 intros result. *)
intuition.
destruct result; simpl in H.
......
......@@ -8,9 +8,6 @@ Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -22,54 +19,65 @@ Existing Instance tree_WhyType.
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))
| 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
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_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 :
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_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_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)).
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 :=
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)
| (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 (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))))) ->
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.
......
......@@ -8,9 +8,6 @@ Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -22,53 +19,64 @@ Existing Instance tree_WhyType.
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))
| 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
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_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 :
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_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_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)).
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 :=
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)
| (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))))).
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.
......
......@@ -8,9 +8,6 @@ Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -22,57 +19,66 @@ Existing Instance tree_WhyType.
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))
| 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
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_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 :
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_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_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)).
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 :=
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)
| (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)))).
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).
(* Why3 intros d s x x1 h1 h2 h3 o o1 h4 h5 t 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.
......
......@@ -8,9 +8,6 @@ Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -22,56 +19,64 @@ Existing Instance tree_WhyType.
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))
| 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
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_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 :
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_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_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)).
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 :=
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)
| (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)))).
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).
(* Why3 intros d s x x1 h1 h2 h3 h4 t s'. *)
intros d s x x1 h1 h2 h3 h4 t s'.
subst.
intuition.
......
......@@ -9,9 +9,6 @@ Require list.Mem.
Require list.Append.
Require list.Reverse.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
......@@ -22,54 +19,59 @@ 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
Axiom depths_head :
forall (t:tree) (d:Z),
match depths d t with
| (Init.Datatypes.cons x _) => (d <= x)%Z
| Init.Datatypes.nil => False