Certified Programming with Dependent Types: src/MoreDep.v comparison

comparison src/MoreDep.v @ 95:7804f9d5249f

Correctness of insertion

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 07 Oct 2008 21:49:35 -0400
parents	affdf00759d8
children	b78a55b30f4a

comparison

equal deleted inserted replaced

-:affdf00759d8
+:7804f9d5249f
 Inductive rbtree : color -> nat -> Set :=
 | Leaf : rbtree Black 0
 | RedNode : forall n, rbtree Black n -> nat-> rbtree Black n -> rbtree Red n
 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
+Require Import Max Min.
+Section depth.
+Variable f : nat -> nat -> nat.
+Fixpoint depth c n (t : rbtree c n) {struct t} : nat :=
+match t with
+| Leaf => 0
+| RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
+| BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
+end.
+End depth.
+Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
+induction t; crush;
+match goal with
+| [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
+end; crush.
+Qed.
+Lemma depth_max' : forall c n (t : rbtree c n), match c with
+| Red => depth max t <= 2 * n + 1
+| Black => depth max t <= 2 * n
+end.
+induction t; crush;
+match goal with
+| [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
+end; crush.
+destruct c1; crush.
+destruct c2; crush.
+Qed.
+Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
+intros; generalize (depth_max' t); destruct c; crush.
+Qed.
+Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
+intros; generalize (depth_min t); generalize (depth_max t); crush.
+Qed.
 Inductive rtree : nat -> Set :=
 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
 Notation "{< x >}" := (existT _ _ x).
 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
 | RedNode _ a x b => fun c d => {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
 | t1' => fun t2 =>
 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
 | RedNode _ b x c => fun a d => {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
-| b => fun a t => {<BlackNode a data b>}
+| b => fun a t => {<BlackNode (RedNode a y b) data t>}
 end t1'
 end t2
 end.
 Definition balance2 n (a : rtree n) (data : nat) c2 :=
 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
 | RedNode _ b y c => fun d a => {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
 | t1' => fun t2 =>
 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
 | RedNode _ c z' d => fun b a => {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
-| b => fun t a => {<BlackNode a data b>}
+| b => fun a t => {<BlackNode t data (RedNode a z b)>}
 end t1'
 end t2
 end.
+Section present.
+Variable x : nat.
+Fixpoint present c n (t : rbtree c n) {struct t} : Prop :=
+match t with
+| Leaf => False
+| RedNode _ a y b => present a \/ x = y \/ present b
+| BlackNode _ _ _ a y b => present a \/ x = y \/ present b
+end.
+Definition rpresent n (t : rtree n) : Prop :=
+match t with
+| RedNode' _ _ _ a y b => present a \/ x = y \/ present b
+end.
+End present.
 Section insert.
 Variable x : nat.
 Definition insResult c n :=
 Implicit Arguments makeBlack [c n].
 Definition insert c n (t : rbtree c n) : insertResult c n :=
 makeBlack (ins t).
-Fixpoint present c n (t : rbtree c n) {struct t} : bool :=
+Record rbtree' : Set := Rbtree' {
-match t with
+rtC : color;
-| Leaf => false
+rtN : nat;
-| RedNode _ a y b =>
+rtT : rbtree rtC rtN
-if eq_nat_dec x y
+}.
-then true
-else if le_lt_dec x y
+Section present.
-then present a
+Variable z : nat.
-else present b
-| BlackNode _ _ _ a y b =>
+Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
-if eq_nat_dec x y
+present z (projT2 (balance1 a y b))
-then true
+<-> rpresent z a \/ z = y \/ present z b.
-else if le_lt_dec x y
+destruct a; crush;
-then present a
+repeat match goal with
-else present b
+| [ H : context[match ?T with
-end.
+| Leaf => _
+| RedNode _ _ _ _ => _
-Definition rpresent n (t : rtree n) : bool :=
+| BlackNode _ _ _ _ _ _ => _
-match t with
+end] |- _ ] => pose T; dep_destruct T; crush
-| RedNode' _ _ _ a y b =>
+| [ |- context[match ?T with
-if eq_nat_dec x y
+| Leaf => _
-then true
+| RedNode _ _ _ _ => _
-else if le_lt_dec x y
+| BlackNode _ _ _ _ _ _ => _
-then present a
+end] ] => pose T; dep_destruct T; crush
-else present b
+end.
-end.
+Qed.
+Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
+present z (projT2 (balance2 a y b))
+<-> rpresent z a \/ z = y \/ present z b.
+destruct a; crush;
+repeat match goal with
+| [ H : context[match ?T with
+| Leaf => _
+| RedNode _ _ _ _ => _
+| BlackNode _ _ _ _ _ _ => _
+end] |- _ ] => pose T; dep_destruct T; crush
+| [ |- context[match ?T with
+| Leaf => _
+| RedNode _ _ _ _ => _
+| BlackNode _ _ _ _ _ _ => _
+end] ] => pose T; dep_destruct T; crush
+end.
+Qed.
+Definition present_insResult c n :=
+match c return (rbtree c n -> insResult c n -> Prop) with
+| Red => fun t r => rpresent z r <-> z = x \/ present z t
+| Black => fun t r => present z (projT2 r) <-> z = x \/ present z t
+end.
+Theorem present_ins : forall c n (t : rbtree c n),
+present_insResult t (ins t).
+induction t; crush;
+repeat (match goal with
+| [ H : context[if ?E then _ else _] |- _ ] => destruct E
+| [ |- context[if ?E then _ else _] ] => destruct E
+| [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] => destruct C
+end; crush);
+try match goal with
+| [ H : context[balance1 ?A ?B ?C] |- _ ] =>
+generalize (present_balance1 A B C)
+end;
+try match goal with
+| [ H : context[balance2 ?A ?B ?C] |- _ ] =>
+generalize (present_balance2 A B C)
+end;
+try match goal with
+| [ |- context[balance1 ?A ?B ?C] ] =>
+generalize (present_balance1 A B C)
+end;
+try match goal with
+| [ |- context[balance2 ?A ?B ?C] ] =>
+generalize (present_balance2 A B C)
+end;
+intuition;
+match goal with
+| [ z : nat, x : nat |- _ ] =>
+match goal with
+| [ H : z = x |- _ ] => rewrite H in *; clear H
+end
+end;
+tauto.
+Qed.
+Theorem present_insert_Red : forall n (t : rbtree Red n),
+present z (insert t)
+<-> (z = x \/ present z t).
+unfold insert; inversion t;
+generalize (present_ins t); simpl;
+dep_destruct (ins t); tauto.
+Qed.
+Theorem present_insert_Black : forall n (t : rbtree Black n),
+present z (projT2 (insert t))
+<-> (z = x \/ present z t).
+unfold insert; inversion t;
+generalize (present_ins t); simpl;
+dep_destruct (ins t); tauto.
+Qed.
+End present.
 End insert.
-Require Import Max Min.
-Section depth.
-Variable f : nat -> nat -> nat.
-Fixpoint depth c n (t : rbtree c n) {struct t} : nat :=
-match t with
-| Leaf => 0
-| RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
-| BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
-end.
-End depth.
-Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
-induction t; crush;
-match goal with
-| [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
-end; crush.
-Qed.
-Lemma depth_max' : forall c n (t : rbtree c n), match c with
-| Red => depth max t <= 2 * n + 1
-| Black => depth max t <= 2 * n
-end.
-induction t; crush;
-match goal with
-| [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
-end; crush.
-destruct c1; crush.
-destruct c2; crush.
-Qed.
-Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
-intros; generalize (depth_max' t); destruct c; crush.
-Qed.
-Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
-intros; generalize (depth_min t); generalize (depth_max t); crush.
-Qed.
 (** * A Certified Regular Expression Matcher *)
 (** Another interesting example is regular expressions with dependent types that express which predicates over strings particular regexps implement.  We can then assign a dependent type to a regular expression matching function, guaranteeing that it always decides the string property that we expect it to decide.

Mercurial > cpdt > repo

comparison src/MoreDep.v @ 95:7804f9d5249f