Commit 5d307f08 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

tree reconstruction: all proofs in theory Tree

parent b8f565b6
......@@ -33,10 +33,6 @@ theory Tree
forall t1 t2: tree, d: int, s1 s2: list int.
depths d t1 ++ s1 = depths d t2 ++ s2 -> t1 = t2 && s1 = s2
lemma depths_unique2:
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
......@@ -49,6 +45,10 @@ theory Tree
forall t1 t2: tree, d1 d2: int, s1: list int.
depths d1 t1 ++ s1 = depths d2 t2 -> d1 >= d2
lemma depths_unique2:
forall t1 t2: tree, d1 d2: int.
depths d1 t1 = depths d2 t2 -> d1 = d2 && t1 = t2
end
module TreeReconstruction
......
(* 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)).
Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
(* Why3 goal *)
Theorem 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).
induction t; simpl.
z.
z.
Qed.
......@@ -87,45 +87,27 @@ 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.
Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
(* Why3 goal *)
Theorem depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z),
((depths d1 t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
induction t1; simpl.
induction t2; simpl.
intuition.
injection H; auto.
intros d1 d2; generalize (depths_head t2_1 (d2+1)%Z).
destruct ((depths (d2 + 1) t2_1)); simpl; intuition.
generalize (depths_head t2_2 (d2+1)%Z).
generalize H0.
destruct ((depths (d2 + 1) t2_2)); simpl; intuition.
injection H0.
destruct l; simpl; intuition.
discriminate H3.
discriminate H3.
generalize H0.
generalize (depths_head t2_2 (d2+1)%Z).
destruct ((depths (d2 + 1) t2_2)); simpl; intuition.
injection H0.
destruct l; simpl; intuition.
discriminate H3.
discriminate H3.
(* t1 = Node t1_1 t1_2 *)
induction t2; simpl.
(* t2 = Leaf *)
intros d1 d2.
generalize (depths_head t1_1 (d1+1)%Z).
destruct ((depths (d1 + 1) t1_1)); simpl.
intuition.
generalize (depths_head t1_2 (d1+1)%Z).
destruct ((depths (d1 + 1) t1_2)); simpl.
intuition.
intros _ _.
destruct l; simpl.
intros h. discriminate h.
intros h. discriminate h.
(* t2 = Node ... *)
intros t1 t2 d1 d2 h.
assert (depths d1 t1 = infix_plpl (depths d1 t1) Nil) by z.
assert (d1 >= d2)%Z by z.
assert (depths d2 t2 = infix_plpl (depths d2 t2) Nil) by z.
assert (d1 = d2) by z.
z.
Qed.
......@@ -245,14 +245,25 @@ assert (case: (d2 < d1 \/ d2=d1)%Z) by omega. destruct case. 2: auto.
*)
Admitted.
(*
Lemma key_lemma_greedy:
forall l d t t1 t2 d1 d2, d1 <> d2 ->
greedy d t (infix_plpl l (Cons (d1, t1) Nil)) ->
g d t (infix_plpl l (Cons (d1, t1) Nil)) ->
match t2 with
| (Node l2 _) => g (infix_plpl l (Cons (d1, t1) (Cons ((d2 + 1%Z)%Z, l2))))
| Leaf => True end ->
greedy d t (infix_plpl l (Cons (d1, t1) (Cons (d2, t2) Nil))).
induction l; simpl.
unfold greedy; simpl.
intros d t t1 t2 d1 d2 ineq.
do 2 rewrite Append_l_nil.
(* l = Nil *)
admit.
(* l = Cons _ _ *)
unfold greedy; simpl.
intros.
destruct a.
z.
(*
z.
unfold greedy; simpl.
......@@ -260,6 +271,7 @@ intros. z.
Qed.
*)
Admitted.
*)
(* Why3 goal *)
Theorem main_lemma : forall (l:(list (Z* tree)%type)) (d1:Z) (d2:Z) (t1:tree)
......@@ -288,11 +300,15 @@ destruct a.
inversion H0.
z.
apply Gtwo.
(* greedy *)
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.
(* g *)
apply IHl; auto.
destruct t2; auto.
inversion H1; z.
Qed.
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