Require Import NaturalDeduction. Require Import Hoare. Require Import Lemmas. Inductive Tree := | leaf : nat -> Tree | node : nat -> Tree -> Tree -> Tree. Definition isLeaf (t : Tree) : bool := match t with | leaf _ => true | node _ _ _ => false end. Definition left (t : Tree) : Tree := match t with | leaf _ => leaf 0 | node _ t1 _ => t1 end. Definition right (t : Tree) : Tree := match t with | leaf _ => leaf 0 | node _ _ t2 => t2 end. Fixpoint size (t : Tree) : nat := match t with | leaf _ => 1 | node _ t1 t2 => 1 + size t1 + size t2 end. Lemma isLeaf_True : forall t, isLeaf t = true <-> exists n, t = leaf n. Proof. Forall_Intro. split. Impl_Intro. induction t0. Exists_Intro with n. trivial. simpl in H. inversion H. Impl_Intro. Exists_Elim in H. rewrite H0. trivial. Qed. Lemma isLeaf_False : forall t, isLeaf t = false <-> exists n t1 t2, t = node n t1 t2. Proof. Forall_Intro. split. Impl_Intro. induction t0. simpl in H. inversion H. Exists_Intro with n. Exists_Intro with t0_1. Exists_Intro with t0_2. trivial. Impl_Intro. Exists_Elim in H. Exists_Elim in H0. Exists_Elim in H1. rewrite H2. trivial. Qed. Inductive Stack := | empty : Stack | push : Tree -> Stack -> Stack. Definition peek (s : Stack) : Tree := match s with | empty => leaf 0 | push t _ => t end. Definition pop (s : Stack) : Stack := match s with | empty => empty | push _ s => s end. Definition isEmpty (s : Stack) : bool := match s with | empty => true | push _ _ => false end. Fixpoint sizes (s : Stack) : nat := match s with | empty => 0 | push t s' => size t + sizes s' end. Lemma isEmpty_True : forall s, isEmpty s = true <-> s = empty. Proof. Forall_Intro. split. Impl_Intro. induction s. trivial. simpl in H. inversion H. Impl_Intro. rewrite H. trivial. Qed. Lemma isEmpty_False : forall s, isEmpty s = false <-> exists t s', s = push t s'. Proof. Forall_Intro. split. Impl_Intro. induction s. simpl in H. inversion H. Exists_Intro with t0. Exists_Intro with s. trivial. Impl_Intro. Exists_Elim in H. Exists_Elim in H0. rewrite H1. trivial. Qed. Lemma Lab11 (t t' : Tree) (s : Stack) (n : nat): {{ True }} n ::= 0;; s ::= push t empty;; While negb (isEmpty s) Do t' ::= peek s;; s ::= pop s;; n ::= n+1;; If (isLeaf t') Then Skip Else s ::= push (left t') s;; s ::= push (right t') s Fi Od {{ n = size t }}. Proof. Hoare_while_tactic with (n + sizes s = size t). (* Prop 1 *) Impl_Intro. simpl. rewrite add_0_r. trivial. (* Prop 2 *) Impl_Intro. bool2Prop in H. And_Elim_all in H. And_Intro. (* True case *) Impl_Intro. apply isEmpty_False in H0. Exists_Elim in H0. Exists_Elim in H2. rewrite H3. simpl. rewrite H3 in H1. simpl in H1. apply isLeaf_True in H1. Exists_Elim in H1. rewrite H3 in H. rewrite H4 in H. simpl in H. rewrite <- add_assoc. assumption. (* False case *) Impl_Intro. apply isEmpty_False in H0. Exists_Elim in H0. Exists_Elim in H2. rewrite H3. simpl. rewrite H3 in H. simpl in H. rewrite H3 in H1. simpl in H1. apply isLeaf_False in H1. Exists_Elim in H1. Exists_Elim in H4. Exists_Elim in H5. rewrite H6 in H. simpl in H. rewrite H6. simpl. rewrite (add_assoc (size x3)). rewrite (add_comm (size x3)). rewrite <- add_assoc. assumption. (* Prop 3 *) Impl_Intro. bool2Prop in H. And_Elim_all in H. apply isEmpty_True in H0. rewrite H0 in H. simpl in H. rewrite add_0_r in H. assumption. Qed.