Require Export List. Require Export Arith. (*Defining well-parenthesized expressions, take 1*) (*We consider the following type of characters:*) Inductive par : Set := open | close. (* We represent character strings using the type list par. An expression is well-parenthesized when: it is the empty list, it is a well-parenthesized expression between parentheses, it is the concatenation of two well-parenthesized expressions. Define the inductive property wp:list par -> Prop that corresponds to this informal definition. You can use the function app given in the module List to concatenate two lists. Prove the following three properties: *) Inductive wp:list par -> Prop := | wp_nil : wp nil (*mot vide*) | wp_nest: forall l:list par, wp l -> wp (open::(app l (close::nil))) (* open w close *) | wp_concat: forall l1 l2:list par, wp l1 -> wp l2 -> wp (l1 ++ l2). (* w1 w2 *) Example wp_oc : wp (cons open (cons close nil)) (*[open; close]*). Proof. apply (wp_nest nil). apply wp_nil. Qed. Lemma wp_o_head_c : forall l1 l2:list par, wp l1 -> wp l2 -> wp (cons open (app l1 (cons close l2))). Proof. intros. assert (wp (((open::l1) ++ (close::nil))++l2)) as G. apply wp_concat. simpl. apply wp_nest. assumption. assumption. simpl in G. rewrite <- app_assoc in G. simpl in G. assumption. Qed. Lemma wp_o_tail_c : forall l1 l2:list par, wp l1 -> wp l2 -> wp (app l1 (cons open (app l2 (cons close nil)))). Proof. intros. apply (wp_concat). assumption. apply wp_nest. assumption. Qed. (*Generating well-parenthesized expressions, take 1 We consider a type of binary trees without labels and a function that maps any tree to a list of characters. Show that this function always builds a well-parenthesized expression: *) Inductive bin : Set := L: bin | N : bin -> bin -> bin. Fixpoint bin_to_string (t:bin) : list par := match t with | L => nil | N u v => cons open (app (bin_to_string u) (cons close (bin_to_string v))) end. Lemma bin_to_string_correct: forall t:bin, wp(bin_to_string t). Proof. intros. induction t. simpl. apply wp_nil. simpl. apply wp_o_head_c;assumption. Qed. (*Generating well-parenthesized expressions, take 2 Prove that the following function also returns a well-parenthesized expression:*) Fixpoint bin_to_string' (t:bin) : list par := match t with | L => nil | N u v => app (bin_to_string' u) (cons open (app (bin_to_string' v)(cons close nil))) end. Lemma bin_to_string'_correct: forall t:bin, wp(bin_to_string' t). Proof. intros. induction t. simpl; apply wp_nil. simpl; apply wp_o_tail_c; assumption. Qed. (*Defining well-parenthesized expressions, take 2 Here is a second definition of well-parenthesized expressions. Prove that it is equivalent to the previous one:*) Inductive wp' : list par -> Prop := | wp'_nil : wp' nil | wp'_cons : forall l1 l2:list par, wp' l1 -> wp' l2 -> wp' (cons open (app l1 (cons close l2))). Lemma wp'_concat: forall l1 l2 : list par, wp' l1 -> wp' l2 -> wp' (l1++l2). Proof. intros. induction H. simpl; assumption. simpl. rewrite <- app_assoc. simpl. constructor; assumption. Qed. Lemma wp_wp': forall l:list par, wp l -> wp' l. Proof. intros. induction H. apply wp'_nil. apply wp'_cons. assumption. apply wp'_nil. apply wp'_concat; assumption. Qed. Lemma wp'_wp: forall l:list par, wp' l -> wp l. Proof. intros. induction H. apply wp_nil. apply wp_o_head_c; assumption. Qed. (* Defining well-parenthesized expressions, take 3 Here is a third definition. Prove that it is equivalent to the previous ones:*) Inductive wp'' : list par -> Prop := | wp''_nil : wp'' nil | wp''_cons : forall l1 l2:list par, wp'' l1 -> wp'' l2 -> wp'' (app l1 (cons open (app l2 (cons close nil)))). (* Recognizing well-parenthesized expressions (completeness) Here is a function that recognizes well-parenthesized expressions by counting the opening parentheses that are not yet closed:*) Fixpoint recognize (n:nat)(l:list par){struct l} : bool := match l with nil => match n with O => true | _ => false end | cons open l' => recognize (S n) l' | cons close l' => match n with O => false | S n' => recognize n' l' end end. (* Prove the following theorem:*) Theorem recognize_complete_aux : forall l:list par, wp l -> forall (n:nat)(l':list par), recognize n (app l l') = recognize n l'. Proof. intros l H. induction H. trivial. intros. simpl. SearchAbout app. rewrite <- app_assoc. simpl. rewrite IHwp. simpl. reflexivity. intros. rewrite <- app_assoc. rewrite IHwp1. rewrite IHwp2. reflexivity. Qed. (* Conclude with the following main theorem:*) Theorem recognize_complete : forall l:list par, wp l -> recognize 0 l = true. Proof. intros. rewrite app_nil_end with (l:=l). apply recognize_complete_aux. assumption. Qed. (*Recognizing well-parenthesized expressions (soundness) This exercise is rather hard. Prove that the recognize function only accepts well-parenthesized expressions, More precisely*) Fixpoint ln (n:nat) : list par := match n with | 0 => nil | S n' => open:: (ln n') end. Lemma ln_open : forall l: list par, forall n:nat, (ln(S n))++l = (ln n)++(open::l). Proof. intros. induction n. simpl;reflexivity. simpl. rewrite <- IHn. simpl. reflexivity. Qed. Lemma recognize_ln: forall l:list par, forall n: nat, recognize n l =true-> forall n1 n2: nat, n=n1+n2 -> recognize n1 (ln n2++l)=true. Proof. intros l n. generalize dependent l. induction n. intros. destruct n1; destruct n2; try(simpl in H0; inversion H0). simpl; assumption. intros. destruct n1; destruct n2; try(simpl in H0; inversion H0). rewrite ln_open. apply IHn. simpl; assumption. simpl; assumption. rewrite plus_0_r in H2. rewrite <- H2; simpl; assumption. rewrite ln_open. apply IHn. simpl. assumption. simpl. rewrite <- plus_n_Sm in H2;assumption. Qed. Lemma list_decomp: forall A:Type, forall l1 l2 l1' l2' :list A, l1++l2=l1'++l2' -> exists l', l1 = l1'++l' \/ l2 = l'++l2'. Proof. intros A l1 l2. induction l1. intros. simpl in H. exists l1'; right; assumption. intros. destruct l1'. simpl. exists (a::l1). left. reflexivity. simpl in H. inversion H. apply IHl1 in H2. inversion H2. inversion H0; simpl; exists x; [left|right]; rewrite H3; reflexivity. Qed. Lemma wp_insert : forall l: list par, wp l -> forall l1 l2 l3:list par, l = l1++l3 -> wp l2 -> wp(l1++l2++l3). Proof. intros l H; induction H. intros. destruct l1; destruct l3; simpl in H; try(inversion H). SearchAbout (_++nil). simpl. rewrite app_nil_r. assumption. intros. assert (close::(rev l)++open::nil = rev l3++ rev l1) as H0_rev. SearchAbout rev. rewrite <- rev_app_distr. rewrite <- H0. simpl. SearchRewrite (rev (_ ++ _::nil)). rewrite rev_unit. simpl; reflexivity. destruct l1. simpl in H0; simpl. constructor. assumption. rewrite <- H0. constructor. assumption. SearchAbout rev. assert(l3 = rev(rev l3)) as RRl3. rewrite rev_involutive. reflexivity. rewrite RRl3 in H0. rewrite RRl3. destruct (rev l3). simpl in H0. rewrite app_nil_r in H0. rewrite <- H0. rewrite app_nil_r. constructor. constructor; assumption. assumption. simpl in H0; simpl in H0_rev. inversion H0; inversion H0_rev. simpl. rewrite app_assoc. rewrite app_assoc. constructor. rewrite <- app_assoc. apply IHwp. rewrite app_assoc in H4. apply app_inj_tail in H4. inversion H4; assumption. assumption. intros. remember H1 as Eq. clear HeqEq. apply list_decomp in H1. Admitted. Lemma recognize_sound_aux: forall l: list par, forall n: nat, recognize n l =true-> wp(ln n++l). Proof. Admitted. Theorem recognize_sound : forall l:list par, recognize 0 l = true -> wp l. Proof. Admitted. (*hint: we suggest proving that if recognize n l is true then the string app ln l is well-parenthesized, where ln is the string made of n opening parentheses. Several lemmas about list concatenation are needed. Parsing well-parenthesized expressions We consider the following parsing function:*) Fixpoint parse (s:list bin)(t:bin)(l:list par){struct l} : option bin := match l with | nil => match s with nil => Some t | _ => None end | cons open l' => parse (cons t s) L l' | cons close l' => match s with | cons t' s' => parse s' (N t' t) l' | _ => None end end. (*Prove that this parser is correct and complete:*) Theorem parse_complete : forall l:list par, wp l -> parse nil L l <> None. Proof. Admitted. Theorem parse_invert: forall (l:list par)(t:bin), parse nil L l = Some t -> bin_to_string' t = l. Proof. Admitted. Theorem parse_sound: forall (l:list par)(t:bin), parse nil L l = Some t -> wp l. Proof. Admitted. (* Inductive presentation of parsing The following inductive definition gives the description of a parsing function for well-parenthesized expressions. Intuitively, ``parse_rel l1 l2 t'' reads as ``parsing the string l1 leaves l2 as suffix and builds the tree t.''*) Inductive parse_rel : list par -> list par -> bin -> Prop := | parse_node : forall (l1 l2 l3:list par)(t1 t2:bin), parse_rel l1 (cons close l2) t1 -> parse_rel l2 l3 t2 -> parse_rel (cons open l1) l3 (N t1 t2) | parse_leaf_nil : parse_rel nil nil L | parse_leaf_close : forall l:list par, parse_rel (cons close l)(cons close l) L. (* Prove the following lemmas:*) Lemma parse_rel_sound_aux : forall (l1 l2:list par)(t:bin), parse_rel l1 l2 t -> l1 = app (bin_to_string t) l2. Proof. Admitted. Lemma parse_rel_sound : forall l:list par, (exists t:bin, parse_rel l nil t)-> wp l. Proof. Admitted.