Commit 4e84eec9 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

tree reconstruction: proof in progress

parent 50f6b5b3
......@@ -36,6 +36,18 @@ theory Tree
forall t1 t2: tree, d1 d2: int.
depths d1 t1 = depths d2 t2 -> d1 = d2 && t1 = t2
lemma depths_prefix:
forall t: tree, d1 d2: int, s1 s2: list int.
depths d1 t ++ s1 = depths d2 t ++ s2 -> d1 = d2
lemma depths_prefix_simple:
forall t: tree, d1 d2: int.
depths d1 t = depths d2 t -> d1 = d2
lemma depths_subtree:
forall t1 t2: tree, d1 d2: int, s1: list int.
depths d1 t1 ++ s1 = depths d2 t2 -> d1 >= d2
end
module TreeReconstruction
......@@ -137,19 +149,39 @@ module ZipperBased
forall f1 f2: list (int, tree).
forest_depths (f1 ++ f2) = forest_depths f1 ++ forest_depths f2
exception Failure
predicate greedy (d1: int) (t1: tree) (l: list (int, tree)) =
forall d: int. d < d1 -> forall t: tree, s: list int.
depths d t ++ s <> forest_depths (Cons (d1, t1) l)
(*
predicate inv (left: list (int, tree)) = match left with
| Nil -> true
| Cons (d, _) Nil -> d <> 0
| Cons (d1, _) ((Cons (d2, _) _) as left') -> d1 <> d2 /\ inv left'
end
*)
inductive g (l: list (int, tree)) =
| Gnil: g Nil
| Gone: forall d: int, t: tree. g (Cons (d, t) Nil)
| Gtwo: forall d: int, t: tree, l: list (int, tree).
greedy d t l -> g l -> g (Cons (d, t) l)
lemma g_append:
forall l1 l2: list (int, tree). g (l1 ++ l2) -> g l1
lemma g_tail:
forall l: list (int, tree), d: int, t: tree.
g (reverse (Cons (d, t) l)) -> g (reverse l)
lemma right_nil:
forall l: list (int, tree). length l >= 2 -> g l ->
forall t: tree. forest_depths l <> depths 0 t
lemma main_lemma:
forall l: list (int, tree), d1 d2: int, t1 t2: tree. d1 <> d2 ->
g (reverse (Cons (d1, t1) l)) ->
g (reverse (Cons (d2, t2) (Cons (d1, t1) l)))
exception Failure
let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree
variant { (length left + length right, length right) } with lex =
{ (* inv left *) }
(* variant { (length left + length right, length right) } with lex *) =
{ g (reverse left) /\
match left with Cons (d, t) Nil -> d <> 0 \/ right <> Nil
| _ -> true end }
match left, right with
| _, Nil ->
raise Failure
......
(* 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 *)
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))).
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree .
(* Why3 assumption *)
Set Implicit Arguments.
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))
end.
Unset Implicit Arguments.
Axiom depths_head : forall (t:tree) (d:Z), match (depths d
t) with
| (Cons x _) => (d <= x)%Z
| 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)).
Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
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_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
t) = (depths d2 t)) -> (d1 = d2).
Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
(* Why3 goal *)
Theorem 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.
induction t1; simpl.
z.
intros t2 d1 d2 s1.
rewrite <- Append_assoc.
intro h.
assert (d2 <= d1+1)%Z by z.
assert (d2 = d1+1 \/ d2 < d1+1)%Z by omega.
destruct H0.
subst d2.
replace (depths (d1+1) t2)%Z with (infix_plpl (depths (d1+1) t2) Nil)%Z in h.
assert (t1_1 = t2) by z.
z.
z.
z.
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.
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))).
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree .
(* Why3 assumption *)
Set Implicit Arguments.
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))
end.
Unset Implicit Arguments.
Axiom depths_head : forall (t:tree) (d:Z), match (depths d
t) with
| (Cons x _) => (d <= x)%Z
| 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)).
Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
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_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
t) = (depths d2 t)) -> (d1 = d2).
(* 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) (x2, y2))
| Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x,
y2)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint reverse (a:Type)(l:(list a)) {struct l}: (list a) :=
match l with
| Nil => (Nil :(list a))
| (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil :(list a))))
end.
Unset Implicit Arguments.
Axiom reverse_append : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1)
(Cons x l2))).
Axiom reverse_reverse : forall (a:Type), forall (l:(list a)),
((reverse (reverse l)) = l).
Axiom Reverse_length : forall (a:Type), forall (l:(list a)),
((length (reverse l)) = (length l)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint forest_depths(f:(list (Z* tree)%type)) {struct f}: (list Z) :=
match f with
| Nil => (Nil :(list Z))
| (Cons (d, t) r) => (infix_plpl (depths d t) (forest_depths r))
end.
Unset Implicit Arguments.
Axiom forest_depths_append : forall (f1:(list (Z* tree)%type)) (f2:(list (Z*
tree)%type)), ((forest_depths (infix_plpl f1
f2)) = (infix_plpl (forest_depths f1) (forest_depths f2))).
(* Why3 assumption *)
Definition greedy(d1:Z) (t1:tree) (l:(list (Z* tree)%type)): Prop :=
forall (d:Z), (d < d1)%Z -> forall (t:tree) (s:(list Z)),
~ ((infix_plpl (depths d t) s) = (forest_depths (Cons (d1, t1) l))).
(* Why3 assumption *)
Inductive g : (list (Z* tree)%type) -> Prop :=
| Gnil : (g (Nil :(list (Z* tree)%type)))
| Gone : forall (d:Z) (t:tree), (g (Cons (d, t) (Nil :(list (Z*
tree)%type))))
| Gtwo : forall (d:Z) (t:tree) (l:(list (Z* tree)%type)), (greedy d t l) ->
((g l) -> (g (Cons (d, t) l))).
Axiom g_tail : forall (l:(list (Z* tree)%type)) (d:Z) (t:tree),
(g (reverse (Cons (d, t) l))) -> (g (reverse l)).
Axiom main_lemma : forall (l:(list (Z* tree)%type)) (d1:Z) (d2:Z) (t1:tree)
(t2:tree), (~ (d1 = d2)) -> ((g (reverse (Cons (d1, t1) l))) ->
(g (reverse (Cons (d2, t2) (Cons (d1, t1) l))))).
Require Import Why3. Ltac z := why3 "z3-3".
(* Why3 goal *)
Theorem WP_parameter_tc : forall (left1:(list (Z* tree)%type)),
forall (right1:(list (Z* tree)%type)), ((g (reverse left1)) /\
match left1 with
| (Cons (d, t) Nil) => (~ (d = 0%Z)) \/ ~ (right1 = (Nil :(list (Z*
tree)%type)))
| _ => True
end) ->
match right1 with
| (Cons x x1) => True
| Nil => forall (t:tree), ~ ((depths 0%Z
t) = (forest_depths (infix_plpl (reverse left1) right1)))
end.
intuition.
destruct right1; auto; simpl.
replace (infix_plpl (reverse left1) Nil) with (reverse left1) by z.
destruct left1; simpl.
z.
inversion H0.
z.
z.
unfold greedy in H2.
z.
destruct left1; simpl.
z.
z.
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.
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))).
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree .
(* Why3 assumption *)
Set Implicit Arguments.
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))
end.
Unset Implicit Arguments.
Axiom depths_head : forall (t:tree) (d:Z), match (depths d
t) with
| (Cons x _) => (d <= x)%Z
| 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)).
Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
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_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
t) = (depths d2 t)) -> (d1 = d2).
(* 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) (x2, y2))
| Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x,
y2)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint reverse (a:Type