 ### vstte12_tree_reconstruction: split a Coq proof into several lemmas

parent 67408c7e
 ... ... @@ -231,6 +231,14 @@ module ZipperBased forest_depths ((d1,t1) :: l) <> depths d t + s whenever d < d1 (see the corresponding Coq file) *) lemma depths_length: forall t d. length (depths d t) >= 1 lemma forest_depths_length: forall l. length (forest_depths l) >= 0 lemma g_tail: forall l1 l2: list (int, tree). g (l1 ++ l2) -> g l2 lemma key_lemma : forall t l d d1 t1 s. d < d1 -> 1 <= length l -> g (reverse (Cons (d1, t1) l)) -> not (forest_depths (Cons (d1, t1) l) = (depths d t) ++ s) lemma right_nil: forall l: list (int, tree). length l >= 2 -> g l -> forall t: tree, d: int. ... ...
 ... ... @@ -94,121 +94,6 @@ Require Import Why3. Ltac z := why3 "Z3,4.4.1," timelimit 5; admit. Ltac ae := why3 "Alt-Ergo,2.0.0,"; admit. Lemma depths_length: forall t d, (Length.length (depths d t) >= 1)%Z. induction t; simpl. intro; omega. z. Admitted. Lemma forest_depths_length: forall l, (Length.length (forest_depths l) >= 0)%Z. induction l; simpl. omega. destruct a. z. Admitted. Lemma g_tail : forall (l1:(list (Z* tree)%type)) (l2:(list (Z* tree)%type)), (g (app l1 l2)) -> (g l2). induction l1; simpl; auto. ae. Admitted. Theorem key_lemma : forall t l d d1 t1 s, (d < d1)%Z -> (1 <= Length.length l)%Z -> g (List.rev (cons (d1, t1) l)) -> ~ (forest_depths (cons (d1, t1) l) = app (depths d t) s). induction t; simpl. (* t = Leaf *) intros. generalize (depths_head t1 d1). destruct (depths d1 t1); intuition. simpl in H3. injection H3. intros; omega. (* t = Node _ _ *) rename t1 into left, IHt1 into IHleft, t2 into right, IHt2 into IHright. destruct l. (* l = Nil *) z. (* l = Cons _ *) destruct p as (d2, t2). intros d d1 t1 s hdd1 hlen hg. assert (hg2: g (app (List.rev l) (cons (d2, t2) nil))) by z. assert (hg12: g (app (cons (d2, t2) nil) (cons (d1, t1) nil))) by z. inversion hg12. subst. clear H5. assert (ineq: (d1 <> d2)) by z. intros eq. assert (case: (d2 < d1 \/ d1 < d2)%Z) by omega. destruct case as [case|case]. (* d2 < d1 *) assert (L0: (forall t2 d1 d2, greedy d1 d2 t2 -> d2 < d1 -> match depths d2 t2 with cons x _ => x < d1 | Nil => False end)%Z). induction t0. ae. simpl. clear IHt0_2. intros d0 d3 (diseq, gr) lt. assert (d0 <> d3+1)%Z by z. assert (d3+1 < d0)%Z by z. generalize (IHt0_1 d0 (d3+1)%Z gr H0). destruct (depths (d3 + 1) t0_1). intuition. simpl; auto. assert (L1: forall t d1 t1 l s d, (d < d1)%Z -> app (depths d1 t1) l = app (depths d t) s -> match l with cons x _ => (x >= d1)%Z | Nil => True end). clear L0 case eq ineq H1 hg12 hg2 hg hlen hdd1. clear s t1 d1 d l t2 d2 IHright IHleft right left. induction t; simpl. intros. generalize (depths_head t1 d1). destruct (depths d1 t1). intuition. destruct l; auto. ae. intros. assert (case2: (d+1 = d1 \/ d+1 < d1)%Z) by omega. destruct case2. rewrite H1 in *. assert (l = app (depths d1 t2) s) by z. generalize (depths_head t2 d1). subst l. destruct (depths d1 t2). intuition. simpl. ae. clear IHt2. apply (IHt1 d1 t0 l (app (depths (d+1) t2) s) (d+1))%Z; auto. z. generalize eq. pose (l0 := (app (depths d2 t2) (forest_depths l))). generalize (depths_head t2 d2). generalize (L0 t2 d1 d2 H1 case); clear L0. generalize (L1 (Node left right) d1 t1 l0 s d hdd1 eq). subst l0. destruct (depths d2 t2). intuition. simpl. intros; omega. (* d1 < d2 *) assert (case2: (d+1 = d1 \/ d+1 < d1)%Z) by omega. destruct case2. (* d+1 = d1 *) rewrite H in *. assert (t1 = left) by z. subst t1. assert (forest_depths (cons (d2, t2) l) = app (depths d1 right) s) by z. clear eq. destruct l. (* l = Nil => contradiction *) simpl in H0. assert (d1 >= d2)%Z by z. omega. (* l = Cons _ _ *) clear IHleft. apply (IHright (cons p l) d1 d2 t2 s); auto. ae. (* d+1 < d1 *) clear IHright. apply (IHleft (cons (d2, t2) l) (d+1) d1 t1 (app (depths (d+1) right) s))%Z; auto. z. Admitted. (* Why3 goal *) Theorem right_nil : forall (l:(list (Z* tree)%type)), (2%Z <= (list.Length.length l))%Z -> ... ...
 (* 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. Require list.Reverse. (* 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 *) Fixpoint forest_depths (f:(list (Z* tree)%type)) {struct f}: (list Z) := match f with | Init.Datatypes.nil => Init.Datatypes.nil | (Init.Datatypes.cons (d, t) r) => (Init.Datatypes.app (depths d t) (forest_depths r)) end. Axiom forest_depths_append : forall (f1:(list (Z* tree)%type)) (f2:(list (Z* tree)%type)), ((forest_depths (Init.Datatypes.app f1 f2)) = (Init.Datatypes.app (forest_depths f1) (forest_depths f2))). (* Why3 assumption *) 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. (* Why3 assumption *) Inductive g: (list (Z* tree)%type) -> Prop := | Gnil : g Init.Datatypes.nil | Gone : forall (d:Z) (t:tree), g (Init.Datatypes.cons (d, t) Init.Datatypes.nil) | Gtwo : forall (d1:Z) (d2:Z) (t1:tree) (t2:tree) (l:(list (Z* tree)%type)), (greedy d1 d2 t2) -> (g (Init.Datatypes.cons (d1, t1) l)) -> g (Init.Datatypes.cons (d2, t2) (Init.Datatypes.cons (d1, t1) l)). Axiom g_append : forall (l1:(list (Z* tree)%type)) (l2:(list (Z* tree)%type)), (g (Init.Datatypes.app l1 l2)) -> g l1. Axiom depths_length : forall (t:tree) (d:Z), (1%Z <= (list.Length.length (depths d t)))%Z. Axiom forest_depths_length : forall (l:(list (Z* tree)%type)), (0%Z <= (list.Length.length (forest_depths l)))%Z. Axiom g_tail : forall (l1:(list (Z* tree)%type)) (l2:(list (Z* tree)%type)), (g (Init.Datatypes.app l1 l2)) -> g l2. Require Import Why3. Ltac z := why3 "Z3,4.4.0," timelimit 5; admit. Ltac ae := why3 "Alt-Ergo,2.0.0,"; admit. (* Why3 goal *) Theorem key_lemma : forall (t:tree) (l:(list (Z* tree)%type)) (d:Z) (d1:Z) (t1:tree) (s:(list Z)), (d < d1)%Z -> (1%Z <= (list.Length.length l))%Z -> (g (Lists.List.rev (Init.Datatypes.cons (d1, t1) l))) -> ~ ((forest_depths (Init.Datatypes.cons (d1, t1) l)) = (Init.Datatypes.app (depths d t) s)). Proof. induction t; simpl. (* t = Leaf *) intros. generalize (depths_head t1 d1). destruct (depths d1 t1); intuition. simpl in H3. injection H3. intros; omega. (* t = Node _ _ *) rename t1 into left, IHt1 into IHleft, t2 into right, IHt2 into IHright. destruct l. (* l = Nil *) z. (* l = Cons _ *) destruct p as (d2, t2). intros d d1 t1 s hdd1 hlen hg. assert (hg2: g (app (List.rev l) (cons (d2, t2) nil))) by z. assert (hg12: g (app (cons (d2, t2) nil) (cons (d1, t1) nil))) by z. inversion hg12. subst. clear H5. assert (ineq: (d1 <> d2)) by z. intros eq. assert (case: (d2 < d1 \/ d1 < d2)%Z) by omega. destruct case as [case|case]. (* d2 < d1 *) assert (L0: (forall t2 d1 d2, greedy d1 d2 t2 -> d2 < d1 -> match depths d2 t2 with cons x _ => x < d1 | Nil => False end)%Z). induction t0. ae. simpl. clear IHt0_2. intros d0 d3 (diseq, gr) lt. assert (d0 <> d3+1)%Z by z. assert (d3+1 < d0)%Z by z. generalize (IHt0_1 d0 (d3+1)%Z gr H0). destruct (depths (d3 + 1) t0_1). intuition. simpl; auto. assert (L1: forall t d1 t1 l s d, (d < d1)%Z -> app (depths d1 t1) l = app (depths d t) s -> match l with cons x _ => (x >= d1)%Z | Nil => True end). clear L0 case eq ineq H1 hg12 hg2 hg hlen hdd1. clear s t1 d1 d l t2 d2 IHright IHleft right left. induction t; simpl. intros. generalize (depths_head t1 d1). destruct (depths d1 t1). intuition. destruct l; auto. ae. intros. assert (case2: (d+1 = d1 \/ d+1 < d1)%Z) by omega. destruct case2. rewrite H1 in *. assert (l = app (depths d1 t2) s) by z. generalize (depths_head t2 d1). subst l. destruct (depths d1 t2). intuition. simpl. ae. clear IHt2. apply (IHt1 d1 t0 l (app (depths (d+1) t2) s) (d+1))%Z; auto. z. generalize eq. pose (l0 := (app (depths d2 t2) (forest_depths l))). generalize (depths_head t2 d2). generalize (L0 t2 d1 d2 H1 case); clear L0. generalize (L1 (Node left right) d1 t1 l0 s d hdd1 eq). subst l0. destruct (depths d2 t2). intuition. simpl. intros; omega. (* d1 < d2 *) assert (case2: (d+1 = d1 \/ d+1 < d1)%Z) by omega. destruct case2. (* d+1 = d1 *) rewrite H in *. assert (t1 = left) by z. subst t1. assert (forest_depths (cons (d2, t2) l) = app (depths d1 right) s) by z. clear eq. destruct l. (* l = Nil => contradiction *) simpl in H0. assert (d1 >= d2)%Z by z. omega. (* l = Cons _ _ *) clear IHleft. apply (IHright (cons p l) d1 d2 t2 s); auto. ae. (* d+1 < d1 *) clear IHright. apply (IHleft (cons (d2, t2) l) (d+1) d1 t1 (app (depths (d+1) right) s))%Z; auto. z. Admitted.
 ... ... @@ -3,11 +3,12 @@ "http://why3.lri.fr/why3session.dtd"> ... ... @@ -93,7 +94,7 @@ ... ... @@ -104,11 +105,35 @@ ... ... @@ -131,13 +156,13 @@ ... ... @@ -167,13 +192,13 @@ ... ...
No preview for this file type
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment