Commit ebfefedf by Jean-Christophe Filliâtre

### tree reconstruction: yes!

parent 5d307f08
 ... ... @@ -118,7 +118,6 @@ end (* A variant implementation proposed by Jayadev Misra (and proved correct by Natarajan Shankar using PVS). Given the input list [x1; x2; ...; xn], we first turn it into the list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)]. Then, ... ... @@ -134,6 +133,38 @@ end *) (* Proving termination is quite easy and we do it first (though we could, obviously, do it together with proving correctness) *) module ZipperBasedTermination use import Tree use import int.Lex2 use import list.Length use import list.Reverse exception Failure let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree variant { (length left + length right, length right) } with lex = {} match left, right with | _, Nil -> raise Failure | Nil, Cons (v, t) Nil -> if v = 0 then t else raise Failure | Nil, Cons (v, t) right' -> tc (Cons (v, t) Nil) right' | Cons (v1, t1) left', Cons (v2, t2) right' -> if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right') else tc (Cons (v2, t2) left) right' end {} | Failure -> {} end (* Now soundness and completeness *) module ZipperBased use import Tree ... ... @@ -141,58 +172,86 @@ module ZipperBased use import list.Length use import list.Reverse (* the following function generalizes function [depths] to a forest, that is a list of pairs (depth, tree) *) function forest_depths (f: list (int, tree)) : list int = match f with | Nil -> Nil | Cons (d, t) r -> depths d t ++ forest_depths r end (* an obvious lemma on [forest_depths] *) lemma forest_depths_append: forall f1 f2: list (int, tree). forest_depths (f1 ++ f2) = forest_depths f1 ++ forest_depths f2 predicate only_leaf (l: list (int, tree)) = match l with | Nil -> true | Cons (_, t) r -> t = Leaf /\ only_leaf r end (* to prove completeness, one needs an invariant over the list [left]. The main ingredient is predicate [greedy] below, which states that [d] is distinct from all depths along the left branch of [d1, t1]. *) 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 greedy (d: int) (d1: int) (t1: tree) = d <> d1 /\ match t1 with Leaf -> true | Node l1 _ -> greedy d (d1+1) l1 end (* then we extend it to a list of pairs [(dn,tn); ...; (d2,t2); (d1,t1)] as follows: [greedy d2 d1 t1], [greedy d3 d2 t2], etc. this is inductive predicate [g] *) 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) | Gtwo: forall d1 d2: int, t1 t2: tree, l: list (int, tree). greedy d1 d2 t2 -> g (Cons (d1, t1) l) -> g (Cons (d2, t2) (Cons (d1, t1) l)) (* an easy lemma on [g] *) 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) (* key lemma for completeness: whenever we fail because [right] is empty, we have to prove that there is no solution Note: the proof first generalizes the statement as follows: forest_depths ((d1,t1) :: l) <> depths d t + s whenever d < d1 (see the corresponding Coq file) *) lemma right_nil: forall l: list (int, tree). length l >= 2 -> g l -> forall t: tree. forest_depths l <> depths 0 t forall t: tree, d: int. forest_depths (reverse l) <> depths d t (* key lemma for soundness: preservation of the invariant when we move a tree from [right] to [left] *) lemma main_lemma: forall l: list (int, tree), d1 d2: int, t1 t2: tree. d1 <> d2 -> g (reverse (Cons (d1, t1) l)) -> match t2 with Node l2 _ -> g (reverse (Cons (d2+1, l2) (Cons (d1, t1) l))) | Leaf -> true end -> g (reverse (Cons (d2, t2) (Cons (d1, t1) l))) g (Cons (d1, t1) l) -> match t2 with Node l2 _ -> greedy d1 (d2+1) l2 | Leaf -> true end -> g (Cons (d2, t2) (Cons (d1, t1) l)) (* finally, we need a predicate to state that a forest [l] contains only leaves *) predicate only_leaf (l: list (int, tree)) = match l with | Nil -> true | Cons (_, t) r -> t = Leaf /\ only_leaf r end exception Failure let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree (* variant { (length left + length right, length right) } with lex *) = { g (reverse left) /\ let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree = { (* list [left] satisfies the invariant *) g left /\ (* when [left] has one element, it can't be a solution *) match left with Cons (d1, t1) Nil -> d1 <> 0 \/ right <> Nil | _ -> true end /\ (* apart (possibly) from its head, all elements in [right] are leaves; moreover the left branch of [right]'s head already satisfies invariant [g] when consed to [left] *) match right with | Cons (d2, t2) right' -> only_leaf right' /\ match t2 with Node l2 _ -> g (reverse (Cons (d2+1, l2) left)) match t2 with Node l2 _ -> g (Cons (d2+1, l2) left) | Leaf -> true end | Nil -> true end } ... ... @@ -211,11 +270,18 @@ module ZipperBased | Failure -> { forall t: tree. depths 0 t <> forest_depths (reverse left ++ right) } (* Getting function [build] from [tc] is easy: from the list [x1; x2; ...; xn] we simply build the list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)]. Function [map_leaf] below does this. *) function map_leaf (l: list int) : list (int, tree) = match l with | Nil -> Nil | Cons d r -> Cons (d, Leaf) (map_leaf r) end (* two lemmas on [map_leaf] *) lemma map_leaf_depths: forall l: list int. forest_depths (map_leaf l) = l ... ...
 (* 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_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). 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_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) (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 *) Set Implicit Arguments. Fixpoint only_leaf(l:(list (Z* tree)%type)) {struct l}: Prop := match l with | Nil => True | (Cons (_, t) r) => (t = Leaf) /\ (only_leaf r) end. Unset Implicit Arguments. (* Why3 assumption *) Set Implicit Arguments. Fixpoint greedy(d:Z) (d1:Z) (t1:tree) {struct t1}: Prop := (~ (d = d1)) /\ match t1 with | Leaf => True | (Node l1 _) => (greedy d (d1 + 1%Z)%Z l1) end. Unset Implicit Arguments. (* 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 (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)))). Axiom g_append : forall (l1:(list (Z* tree)%type)) (l2:(list (Z* tree)%type)), (g (infix_plpl l1 l2)) -> (g l1). Axiom right_nil : forall (l:(list (Z* tree)%type)), (2%Z <= (length l))%Z -> ((g l) -> forall (t:tree), ~ ((forest_depths l) = (depths 0%Z t))). Axiom main_lemma : forall (l:(list (Z* tree)%type)) (d1:Z) (d2:Z) (t1:tree) (t2:tree), (~ (d1 = d2)) -> ((g (Cons (d1, t1) l)) -> (match t2 with | (Node l2 _) => (greedy d1 (d2 + 1%Z)%Z l2) | Leaf => True end -> (g (Cons (d2, t2) (Cons (d1, t1) l))))). Require Import Why3. Ltac z := why3 "z3-3" timelimit 5. (* Why3 goal *) Theorem WP_parameter_tc : forall (left1:(list (Z* tree)%type)), forall (right1:(list (Z* tree)%type)), ((g left1) /\ (match left1 with | (Cons (d1, t1) Nil) => (~ (d1 = 0%Z)) \/ ~ (right1 = (Nil :(list (Z* tree)%type))) | _ => True end /\ match right1 with | (Cons (d2, t2) rightqt) => (only_leaf rightqt) /\ match t2 with | (Node l2 _) => (g (Cons ((d2 + 1%Z)%Z, l2) left1)) | Leaf => True end | Nil => 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. rewrite Append_l_nil. destruct left1. z. destruct p; destruct left1. replace (reverse (Cons (z, t) Nil)) with (Cons (z, t) Nil) by z. simpl. rewrite Append_l_nil. intuition. z. Qed.
 ... ... @@ -105,9 +105,6 @@ 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). ... ... @@ -115,6 +112,12 @@ Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list 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_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. ... ... @@ -158,17 +161,31 @@ Axiom forest_depths_append : forall (f1:(list (Z* tree)%type)) (f2:(list (Z* 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))). Set Implicit Arguments. Fixpoint only_leaf(l:(list (Z* tree)%type)) {struct l}: Prop := match l with | Nil => True | (Cons (_, t) r) => (t = Leaf) /\ (only_leaf r) end. Unset Implicit Arguments. (* Why3 assumption *) Set Implicit Arguments. Fixpoint greedy(d:Z) (d1:Z) (t1:tree) {struct t1}: Prop := (~ (d = d1)) /\ match t1 with | Leaf => True | (Node l1 _) => (greedy d (d1 + 1%Z)%Z l1) end. Unset Implicit Arguments. (* 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))). | 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)))). Require Import Why3. Ltac z := why3 "z3-3" timelimit 5. ... ... @@ -183,16 +200,14 @@ replace (Cons a (infix_plpl l1 l2)) inversion 1. z. assert (g l1) by z. destruct l1. z. destruct p. apply Gtwo; auto. red. red in H2. intros d0 hd0 t0 s Heq. generalize (H2 d0 hd0 t0 (infix_plpl s (forest_depths l2))). clear H2 IHl1. simpl in H1. z. simpl. simpl in Heq. z. simpl; auto. Qed.
 ... ... @@ -105,9 +105,6 @@ 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). ... ... @@ -118,6 +115,9 @@ Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1 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_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. ... ... @@ -170,29 +170,33 @@ Fixpoint only_leaf(l:(list (Z* tree)%type)) {struct l}: Prop := Unset Implicit Arguments. (* 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))). Set Implicit Arguments. Fixpoint greedy(d:Z) (d1:Z) (t1:tree) {struct t1}: Prop := (~ (d = d1)) /\ match t1 with | Leaf => True | (Node l1 _) => (greedy d (d1 + 1%Z)%Z l1) end. Unset Implicit Arguments. (* 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))). | 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)))). Axiom g_append : forall (l1:(list (Z* tree)%type)) (l2:(list (Z* tree)%type)), (g (infix_plpl l1 l2)) -> (g l1). Axiom g_tail : forall (l:(list (Z* tree)%type)) (d:Z) (t:tree), (g (reverse (Cons (d, t) l))) -> (g (reverse l)). Axiom right_nil : forall (l:(list (Z* tree)%type)), (2%Z <= (length l))%Z -> ((g l) -> forall (t:tree), ~ ((forest_depths l) = (depths 0%Z t))). ((g l) -> forall (t:tree), ~ ((forest_depths (reverse l)) = (depths 0%Z t))).