Commit b12acb40 authored by MARCHE Claude's avatar MARCHE Claude

example tree reconstruction: remove a few Coq proofs

parent ae62fcce
......@@ -9,7 +9,7 @@
lists from Why3's standard library.
*)
theory Tree
module Tree
use export int.Int
use export list.List
......@@ -29,9 +29,22 @@ theory Tree
forall t: tree, d: int.
match depths d t with Cons x _ -> x >= d | Nil -> false end
lemma depths_unique:
forall t1 t2: tree, d: int, s1 s2: list int.
depths d t1 ++ s1 = depths d t2 ++ s2 -> t1 = t2 && s1 = s2
let rec lemma depths_unique (t1 t2: tree) (d: int) (s1 s2: list int)
requires { depths d t1 ++ s1 = depths d t2 ++ s2 }
variant { t1 }
ensures { t1 = t2 && s1 = s2 }
= let d' = d+1 in
match t1,t2 with
| Leaf,Leaf -> ()
| Node t11 t12, Node t21 t22 ->
depths_unique t11 t21 d' (depths d' t12 ++ s1) (depths d' t22 ++ s2);
depths_unique t12 t22 d' s1 s2
| Leaf, (Node t _) | (Node t _), Leaf ->
match depths d' t with
| Nil -> absurd
| Cons x _ -> assert { x >= d' }
end
end
lemma depths_prefix:
forall t: tree, d1 d2: int, s1 s2: list int.
......@@ -41,9 +54,16 @@ theory Tree
forall t: tree, d1 d2: int.
depths d1 t = depths d2 t -> d1 = d2
lemma depths_subtree:
forall t1 "induction" t2: tree, d1 d2: int, s1: list int.
depths d1 t1 ++ s1 = depths d2 t2 -> d1 >= d2
let rec lemma depths_subtree (t1 t2: tree) (d1 d2:int) (s1:list int)
requires { depths d1 t1 ++ s1 = depths d2 t2 }
variant { t1 }
ensures { d1 >= d2 }
= assert { depths d2 t2 = depths d2 t2 ++ Nil };
match t1 with
| Leaf -> ()
| Node t3 t4 ->
depths_subtree t3 t2 (d1+1) d2 (depths (d1+1) t4 ++ s1)
end
lemma depths_unique2:
forall t1 t2: tree, d1 d2: int.
......
(* 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.
(* 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 => (cons d nil)
| (Node l r) => (List.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
| (cons x _) => (d <= x)%Z
| nil => False
end.
(* Why3 goal *)
Theorem depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z))
(s2:(list Z)), ((List.app (depths d t1) s1) = (List.app (depths d
t2) s2)) -> ((t1 = t2) /\ (s1 = s2)).
(* Why3 intros t1 t2 d s1 s2 h1. *)
induction t1.
simpl; intros.
induction t2.
simpl in H.
injection H; intuition.
simpl in *.
generalize (depths_head t2_1 (d+1)%Z).
generalize H; clear H.
destruct ((depths (d + 1) t2_1)); simpl in *.
intuition.
intros h; injection h.
intros; apply False_ind; omega.
(* t1 = Node *)
induction t2; simpl.
(* t2 = Leaf *)
intros.
generalize (depths_head t1_1 (d+1)%Z).
generalize H; clear H.
destruct ((depths (d + 1) t1_1)); simpl in *.
intuition.
intros h; injection h.
intros; apply False_ind; omega.
(* t2 = Node *)
intros.
do 2 (rewrite <- Append.Append_assoc in H).
generalize (IHt1_1 t2_1 (d+1) _ _ H)%Z. clear IHt1_1.
intros (eq1, H1).
generalize (IHt1_2 t2_2 (d+1) _ _ H1)%Z. clear IHt1_2.
intuition.
apply f_equal2; auto.
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