vstte12_tree_reconstruction_Harness_VC_harness2_1.v 3.75 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
3 4
Require Import BuiltIn.
Require BuiltIn.
5
Require int.Int.
6 7 8 9
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
10

11
(* Why3 assumption *)
12 13 14
Inductive tree :=
  | Leaf : tree
  | Node : tree -> tree -> tree.
15 16
Axiom tree_WhyType : WhyType tree.
Existing Instance tree_WhyType.
17

18
(* Why3 assumption *)
19
Fixpoint depths (d:Z) (t:tree) {struct t}: (list Z) :=
20
  match t with
21
  | Leaf => (Init.Datatypes.cons d Init.Datatypes.nil)
22 23
  | Node l r =>
      (Init.Datatypes.app (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r))
24 25
  end.

26 27 28
Axiom depths_head :
  forall (t:tree) (d:Z),
  match depths d t with
29 30
  | (Init.Datatypes.cons x _) => (d <= x)%Z
  | Init.Datatypes.nil => False
31 32
  end.

33 34 35 36 37
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).
38

39 40 41 42 43
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).
44

45 46
Axiom depths_prefix_simple :
  forall (t:tree) (d1:Z) (d2:Z), ((depths d1 t) = (depths d2 t)) -> (d1 = d2).
47

48 49 50
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.
51

52 53 54
Axiom depths_unique2 :
  forall (t1:tree) (t2:tree) (d1:Z) (d2:Z),
  ((depths d1 t1) = (depths d2 t2)) -> (d1 = d2) /\ (t1 = t2).
55

56
(* Why3 assumption *)
57
Definition lex (x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type) : Prop :=
58 59 60
  match x1 with
  | (s1, d1) =>
      match x2 with
61 62 63 64 65 66 67 68
      | (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)
69 70 71 72
      end
  end.

Lemma depths_length: 
73
  forall t d, (Length.length (depths d t) >= 1)%Z.
74 75
Proof.
  induction t; simpl; intuition.
76
  rewrite Append.Append_length.
77 78 79 80 81 82
  generalize (IHt1 (d+1))%Z.
  generalize (IHt2 (d+1))%Z.
  omega.
Qed.


83
(* Why3 goal *)
84 85 86 87 88 89 90
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. *)
91

92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
intuition.
destruct result; simpl in H.
discriminate H.
destruct result1; simpl in H.
injection H. intro H1.
destruct result2; simpl in H1.
discriminate H1.
destruct result2_1; simpl in H1.
discriminate H1.
destruct result2_1_1; simpl in H1.
injection H1. intro H2.
destruct result2_1_2; simpl in H2.
discriminate H2.
clear H H1.
generalize (depths_length result2_1_2_1 4).
generalize (depths_length result2_1_2_2 4).
generalize (depths_length result2_2 2).
109
generalize (f_equal Length.length H2).
110
simpl.
111
do 2 (rewrite Append.Append_length).
112 113 114 115 116 117 118
omega.
(* 4 trees, 3 ints *)
clear H.
generalize (depths_length result2_1_1_1 4).
generalize (depths_length result2_1_1_2 4).
generalize (depths_length result2_1_2 3).
generalize (depths_length result2_2 2).
119
generalize (f_equal Length.length H1).
120
simpl.
121
do 3 (rewrite Append.Append_length).
122 123 124 125 126 127 128 129 130 131 132 133
omega.

destruct result1_1; simpl in H.
discriminate H.
destruct result1_1_1; simpl in H.
discriminate H.
(* 5 trees, 4 ints *)
generalize (depths_length result1_1_1_1 4).
generalize (depths_length result1_1_1_2 4).
generalize (depths_length result1_1_2 3).
generalize (depths_length result1_2 2).
generalize (depths_length result2 1).
134
generalize (f_equal Length.length H).
135
simpl.
136
do 4 (rewrite Append.Append_length).
137 138 139 140
omega.

Qed.