 ### tree reconstruction: more invariant

parent 4e84eec9
 ... ... @@ -23,7 +23,8 @@ theory Tree | Node l r -> depths (d+1) l ++ depths (d+1) r end (* two lemmas on depths *) (* lemmas on depths *) lemma depths_head: forall t: tree, d: int. match depths d t with Cons x _ -> x >= d | Nil -> false end ... ... @@ -149,6 +150,11 @@ module ZipperBased 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 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) ... ... @@ -173,6 +179,8 @@ module ZipperBased 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))) exception Failure ... ... @@ -180,8 +188,14 @@ module ZipperBased let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree (* 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 with Cons (d1, t1) Nil -> d1 <> 0 \/ right <> Nil | _ -> true end /\ match right with | Cons (d2, t2) right' -> only_leaf right' /\ match t2 with Node l2 _ -> g (reverse (Cons (d2+1, l2) left)) | Leaf -> true end | Nil -> true end } match left, right with | _, Nil -> raise Failure ... ... @@ -205,6 +219,9 @@ module ZipperBased lemma map_leaf_depths: forall l: list int. forest_depths (map_leaf l) = l lemma map_leaf_only_leaf: forall l: list int. only_leaf (map_leaf l) let build (s: list int) = {} tc Nil (map_leaf s) ... ...
 ... ... @@ -160,6 +160,15 @@ 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 *) Definition greedy(d1:Z) (t1:tree) (l:(list (Z* tree)%type)): Prop := forall (d:Z), (d < d1)%Z -> forall (t:tree) (s:(list Z)), ... ... @@ -185,27 +194,54 @@ Axiom right_nil : forall (l:(list (Z* tree)%type)), (2%Z <= (length l))%Z -> Require Import Why3. Ltac z := why3 "z3-3" timelimit 5. Lemma key_lemma: forall d d1, (d < d1)%Z -> forall t t1 t2 s d2, forall t t1 t2 s d2 d d1, (d < d1)%Z -> match t2 with Leaf => True | Node left2 _ => g (Cons (d1, t1) (Cons ((d2+1)%Z, left2) Nil)) end -> infix_plpl (depths d1 t1) (depths d2 t2) = infix_plpl (depths d t) s -> d = (d1-1)%Z /\ d1=d2. d = (d1-1)%Z /\ d2 = d1. induction t; simpl. destruct t1; simpl. injection 1. intros; omega. intros t2 s d2. rewrite <- Append_assoc. (* d >= d1+1 -> contradiction *) admit. (* t = Leaf *) intros. assert (d >= d1)%Z. clear H. generalize H1; clear H1. generalize (depths d2 t2). generalize d1. induction t1; simpl. z. (* intros t0 t3 s d2. z. omega. (* t = Node t1 t2 *) rename t1 into left, t2 into right. intros t1 t2 s d2 d d1 ineq. rewrite <- Append_assoc. assert (d+1 < d1 \/ d=d1-1)%Z by omega. destruct H0. intros eq. (* generalize (IHt1 t0 t3 _ _ eq); intuition. intro eq. assert (case: (d+1 < d1 \/ d=d1-1)%Z) by omega. destruct case. (* d+1 < d1, by iH *) generalize (IHt1 t1 t2 (infix_plpl (depths (d + 1) right) s) d2 (d+1) d1 H eq)%Z. intuition. subst. replace (infix_plpl (depths d2 t1) (depths d2 t2)) with (depths (d2-1) (Node t1 t2))%Z in eq. rewrite H0 in eq. assert (Node t1 t2 = left) by z. rewrite H0 in eq. replace (depths (d2 - 1) left) with (infix_plpl (depths (d2 - 1) left) Nil) in eq by z. z. omega. simpl. replace (d2 - 1 + 1)%Z with d2; z. (* d+1 = d1 *) intuition. replace (d+1)%Z with d1 in eq by z. assert (t1 = left) by z. subst. assert (depths d2 t2 = infix_plpl (depths d1 right) s) by z. assert (d2 <= d1)%Z by z. assert (case: (d2 < d1 \/ d2=d1)%Z) by omega. destruct case. 2: auto. *) Admitted. ... ... @@ -228,12 +264,15 @@ Admitted. (* Why3 goal *) Theorem 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))))). (match t2 with | (Node l2 _) => (g (reverse (Cons ((d2 + 1%Z)%Z, l2) (Cons (d1, t1) l)))) | Leaf => True end -> (g (reverse (Cons (d2, t2) (Cons (d1, t1) l)))))). simpl. intro l; generalize (reverse l). clear l. induction l; simpl. (* length = 2 *) intros d1 d2 t1 t2 ineq _. intros d1 d2 t1 t2 ineq _ ht2. apply Gtwo. red; intros. simpl. ... ... @@ -253,7 +292,7 @@ replace (infix_plpl (infix_plpl l (Cons (d1, t1) Nil)) (Cons (d2, t2) Nil)) with (infix_plpl l (Cons (d1, t1) (Cons (d2, t2) Nil))) by z. apply key_lemma_greedy; auto. 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). 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. (* 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 *) 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_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))). 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))) -> (match t2 with | (Node l2 _) => (g (reverse (Cons ((d2 + 1%Z)%Z, l2) (Cons (d1, t1) l)))) | Leaf => True end -> (g (reverse (Cons (d2, t2) (Cons (d1, t1) l)))))). (* Why3 assumption *) Set Implicit Arguments. Fixpoint map_leaf(l:(list Z)) {struct l}: (list (Z* tree)%type) := match l with | Nil => (Nil :(list (Z* tree)%type)) | (Cons d r) => (Cons (d, Leaf) (map_leaf r)) end. Unset Implicit Arguments. Axiom map_leaf_depths : forall (l:(list Z)), ((forest_depths (map_leaf l)) = l). (* Why3 goal *) Theorem map_leaf_only_leaf : forall (l:(list Z)), (only_leaf (map_leaf l)). induction l; simpl; auto. Qed.
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!