(* This is a proof of the eb_write function in the edit module (file [edit.c]). *) Section ProofWrite. (* The type of Runes is abstract to the edit buffer, so I leave it as a parameter to this proof. *) Variable Rune: Type. (* Runes can be of different types *) Inductive Rtype := Space | Newline | Regular. Variable rclass: Rune -> Rtype. (* Some helper to classify runes *) Definition risspace r := match rclass r with | Space => true | _ => false end. Definition risnl r := match rclass r with | Newline => true | _ => false end. (* Buffers need only to be abstracted as the C function [buf_get], as defined in [buf.c]. We also need to know about the limbo part. *) Record Buf: Type := mkBuf { buf_get: nat -> Rune ; buf_limbo: nat ; SPEC_limbo: forall n, n >= buf_limbo -> rclass (buf_get n) = Newline }. Require Import Bool. Require Import Arith. Require Import Omega. Require Import Recdef. Require Import List. Definition nat_eq (a b: nat) := if eq_nat_dec a b then true else false. Notation "a == b" := (nat_eq a b) (at level 70). Notation "a >=? b" := (ge_dec a b) (at level 70). Notation "! a" := (negb a) (at level 65, right associativity). Definition putrune (r: Rune) rem := cons r rem. Section WithBuffer. Context (eb: Buf). (* [eb] is the buffer [eb_write] must output *) Inductive State: Type := Munching | Spitting. Inductive Vars := V (state: State) (munchb: nat) (munche: nat) (nl: nat). Fixpoint steps state p fuel := let W s m := match state with Spitting => s | Munching => m end in match fuel with | 0 => W 1 0 | S fuel' => match rclass (buf_get eb p) with | Regular => S (W 0 1 + steps Spitting (1+ p) fuel') | _ => S (W 1 0 + steps Munching (1+ p) fuel') end end. Definition M (vars: Vars) := let (state, munchb, munche, _) := vars in let p := match state with Munching => munche | Spitting => munchb end in steps state p (buf_limbo eb - p). Function wloop (vars: Vars) {measure M vars} := let (state, munchb, munche, nl) := vars in if munche >=? buf_limbo eb then nil else (* switch (state) { *) match state with | (* case *) Munching => let r := buf_get eb munche in (* if (r == ' ' || r == '\t' || r == '\n') { *) if risspace r || risnl r then let nl' := if risnl r then nl + 1 else nl in wloop (V Munching munchb (1+ munche) (* munche++; *) nl') (* nl += (r == '\n'); *) (* } /* end of if */ *) else (* for (; munchb < munche; munchb++) { *) let fix forloop munchb nl memb := match memb with S memb' => (* loop body *) let r := buf_get eb munchb in (* if ((r == ' ' || r == '\t') && nl) { *) if risspace r && !(nl == 0) then forloop (1+ munchb) nl memb' (* continue; *) (* } /* end of if */ *) else let nl' := if risnl r then nl - 1 else nl in putrune r (* putrune(r, fp); *) (forloop (1+ munchb) nl' memb') (* /* implicit continue */ *) (* } /* end of the for loop */ *) | 0 => nil end in app (forloop munchb nl (munche - munchb)) (wloop (V Spitting (* state = Spitting *) munche munche 0)) (* assert(nl == 0); *) (* continue; *) | (* case *) Spitting => let r := buf_get eb munchb in (* if (r == ' ' || r == '\t' || r == '\n') { *) if risspace r || risnl r then wloop (V Munching (* state = Munching; *) munchb munchb (* munche = munchb; *) 0) (* assert(nl == 0); *) (* } /* end of if */ *) else putrune r (* putrune(r, fp); *) (wloop (V Spitting (1+ munchb) (* munchb++; *) munche nl)) (* continue; *) (* } /* end of switch */ *) end. (* The termination proof follows the function definition. We simply have to prove that each recursive call makes the [steps] function decrease on the new state. *) (* Termination *) Proof. Ltac term_tac := repeat match goal with | [ H: ~ ?a >= ?b |- context[ steps _ _ (?b - ?a) ]] => (* Using a < b we prove (∃fuel, b - a = 1+ fuel). *) destruct (NPeano.Nat.zero_or_succ (b - a)) as [? | Hfuel]; [omega|]; destruct Hfuel as [fuel ?]; replace (b - a) with (S fuel); replace (b - S a) with fuel by omega | [ |- context[ steps _ ?x (S _) ]] => (* One fuel unit is available! Make progress using simpl. *) simpl; destruct (rclass (buf_get eb x)) | [ |- _ ] => (omega || discriminate) end. Ltac t := unfold risspace, risnl; intros; simpl. (* Each bullet corrsponds to a 'continue' in the C program. *) + t. term_tac. + t. term_tac. + t. destruct (munchb >=? buf_limbo eb); [|term_tac]. replace (buf_limbo eb - munchb) with 0 by omega. simpl. omega. + t. destruct (munchb >=? buf_limbo eb); [|term_tac]. rewrite SPEC_limbo in * by assumption. discriminate. Qed. End WithBuffer. (* Extract a chunk of text from a buffer. *) Fixpoint eb_chunk eb p len := match len with | 0 => nil | S len' => buf_get eb p :: eb_chunk eb (1+ p) len' end. (* Lemma to split an [eb_chunk] call into two. *) Lemma eb_chunk_app: forall l1 l2 len p eb (LEN: len = l1 + l2), eb_chunk eb p len = eb_chunk eb p l1 ++ eb_chunk eb (l1 + p) l2. Proof. induction l1 as [|l1 IND]; simpl; intros. + congruence. + subst. simpl. apply f_equal. replace (S (l1 + p)) with (l1 + S p) by omega. apply IND. reflexivity. Qed. (* We will use these two predicates on runes quite often so I abbreviate them into symbols here. *) Notation "□ r" := (* signify an invisible rune *) (rclass r = Newline \/ rclass r = Space) (at level 65, only parsing). Notation "■ r" := (* signify a solid rune *) (rclass r = Regular) (at level 65, only parsing). (* A rune is either solid or white *) Lemma solid_white_dec: forall r, { ■ r } + { □ r }. Proof. intros; destruct (rclass r); eauto. Qed. (* The different kinds of chunks we can encounter in a buffer. *) Definition solid str := forall r, In r str -> ■ r. Definition white str := forall r, In r str -> □ r. Definition space str := forall r, In r str -> rclass r = Space. (* Lemmas to add in the default Coq automation. *) Lemma solid_: (forall r s, solid (r :: s) -> solid s) /\ (forall r s, solid (r :: s) -> ■ r). Proof. unfold solid; intuition. Qed. Lemma white_: (forall r s, white (r :: s) -> □ r) /\ (forall r s, white (r :: s) -> white s). Proof. unfold white; intuition. Qed. Lemma space_: (forall r s, space (r :: s) -> rclass r = Space) /\ (forall r s, space (r :: s) -> space s). Proof. unfold space; intuition. Qed. Hint Resolve (proj1 solid_) (proj2 solid_) (proj1 white_) (proj2 white_) (proj1 space_) (proj2 space_). (* White is detected by the test we use in the C program. *) Lemma white_test: forall r, □ r -> risspace r || risnl r = true. Proof with (destruct (rclass r); congruence). unfold risspace, risnl, orb; intros ? [?|?]... Qed. Lemma solid_test: forall r, ■ r -> risspace r || risnl r = false. Proof with (destruct (rclass r); congruence). unfold risspace, risnl, orb; intros... Qed. (* First behavior lemma. The state machine when started on a solid buffer chunk in the [Spitting] state will output the buffer chunk as is and continue with the rest of the buffer remaining in the [Spitting] state. The proof structure is a simple induction on the length of the block considered. *) Lemma beh_solid: forall eb len p chunk (CHUNK: eb_chunk eb p len = chunk) (SOLID_CHUNK: solid chunk) nl q (Q: q <= p), wloop eb (V Spitting p q nl) = chunk ++ wloop eb (V Spitting (len + p) q nl). Proof. induction len. + simpl. intros. subst. reflexivity. + simpl. intros. subst. rewrite wloop_equation. destruct (q >=? buf_limbo eb). - absurd (rclass (buf_get eb p) = Regular); eauto. rewrite SPEC_limbo by omega; congruence. - rewrite solid_test by eauto. unfold putrune. simpl app. apply f_equal. replace (S (len + p)) with (len + (S p)) by omega. apply IHlen; (omega || congruence || eauto). Qed. (* Counts the number of lines in a string. *) Fixpoint cl str := match str with | r :: str' => if risnl r then cl str' + 1 else cl str' | nil => 0 end. (* Second behavior lemma. *) Lemma beh_white: forall eb len q chunk (CHUNK: eb_chunk eb q len = chunk) (WHITE_CHUNK: white chunk) nl p, wloop eb (V Munching p q nl) = wloop eb (V Munching p (len + q) (cl chunk + nl)). Proof. induction len. + simpl. intros. subst. reflexivity. + simpl. intros. subst. rewrite wloop_equation. destruct (q >=? buf_limbo eb) as [?|_]. - rewrite wloop_equation. destruct (S (len + q) >=? buf_limbo eb); (omega || reflexivity). - rewrite white_test by eauto. replace (S (len + q)) with (len + (1 + q)) by omega. simpl. destruct (risnl (buf_get eb q)). rewrite <- plus_assoc, plus_comm. eauto using IHlen. eauto using IHlen. Qed. Fixpoint out_white str nl := match str with | r :: str' => if risnl r then r :: out_white str' (nl-1) else if nl >=? 1 then out_white str' nl else r :: out_white str' 0 | nil => nil end. (* Third (and most complex) behavior lemma. Here we specify what happens then a chunk of white ends. The behavior can be summarized precisely using the above [out_white] function. *) Lemma beh_white_solid: forall eb p q chunk (CHUNK: eb_chunk eb p (q-p) = chunk) nl (NL_CHUNK: cl chunk = nl) (WHITE_CHUNK: white chunk) (SOLID_AFTER: ■ buf_get eb q), wloop eb (V Munching p q nl) = out_white chunk nl ++ wloop eb (V Spitting q q 0). Proof. intros until q. set (n := q - p). generalize (eq_refl n). unfold n at 2. generalize n. clear n. intros n N. intros. rewrite wloop_equation. destruct (q >=? buf_limbo eb) as [?|_]. { absurd (rclass (buf_get eb q) = Regular). rewrite SPEC_limbo by assumption; congruence. assumption. } rewrite solid_test by assumption. replace (q - p) with n by congruence. revert q p N chunk CHUNK nl NL_CHUNK WHITE_CHUNK SOLID_AFTER. induction n as [|n HIND]; simpl; intros. + subst. reflexivity. + case_eq (risspace (buf_get eb p)); intro SPACE. unfold nat_eq. destruct (eq_nat_dec nl 0) as [NLZ|NLNZ]. (* nl = 0, p points to a space *) - rewrite <- CHUNK, NLZ. simpl. cut (risnl (buf_get eb p) = false). intro NONL. rewrite NONL. simpl. apply f_equal, HIND; (subst; omega || reflexivity || eauto). simpl in NLZ. rewrite NONL in NLZ. assumption. assert (□ buf_get eb p) by (subst; eauto). unfold risnl, risspace in *; destruct (rclass (buf_get eb p)); congruence. (* nl <> 0, p points to a space *) - rewrite <- CHUNK. simpl. cut (risnl (buf_get eb p) = false). intro NONL. rewrite NONL. simpl. destruct (nl >=? 1) as [_|?]; [|omega]. apply HIND; (subst; omega || reflexivity || eauto). simpl. rewrite NONL. reflexivity. assert (□ buf_get eb p) by (subst; eauto). unfold risnl, risspace in *; destruct (rclass (buf_get eb p)); congruence. (* p points to a a newline *) - rewrite <- CHUNK. simpl. cut (risnl (buf_get eb p) = true). intro NL. rewrite NL. simpl. apply f_equal, HIND; (subst; omega || reflexivity || eauto). simpl. rewrite NL. omega. assert (□ buf_get eb p) by (subst; eauto). unfold risnl, risspace in *; intuition; destruct (rclass (buf_get eb p)); congruence. Qed. (* Fourth behavior lemma. *) Lemma beh_solid_white: forall eb p q (Q: p <= q) (WHITE_AFTER: □ buf_get eb q), wloop eb (V Spitting q p 0) = wloop eb (V Munching q q 0). Proof. intros. rewrite wloop_equation. destruct (p >=? buf_limbo eb). + rewrite wloop_equation. destruct (q >=? buf_limbo eb); [|omega]. reflexivity. + rewrite white_test by assumption. reflexivity. Qed. Inductive same_visual: list Rune -> list Rune -> Prop := | sv_eos: forall s, white s -> (* An empty string has the same visual as a whitey one. *) same_visual nil s | sv_eol: forall s1 s2 nl sp, space sp -> rclass nl = Newline -> same_visual s1 s2 -> (* The spaces just before a newline can never be seen, they have no impact on the visual aspect. *) same_visual (nl :: s1) (sp ++ nl :: s2) | sv_sam: forall s1 s2 r, same_visual s1 s2 -> (* In any cases, adding the same rune to two strings with the same visual yields the same visual. *) same_visual (r :: s1) (r :: s2). Notation "a ⊑ b" := (same_visual a b) (at level 70). (* This lemma drives the chunk consumption for proofs on the wloop function. These proofs go chunk by chunk such that each chunk corresponds to a part of the input consumed in a certain state. The blocks' size must be non-zero to make progress. *) Lemma next_chunk: forall eb p, exists len, let chunk := eb_chunk eb p len in white chunk /\ len + p >= buf_limbo eb \/ white chunk /\ ■ buf_get eb (len + p) /\ 0 < len \/ solid chunk /\ □ buf_get eb (len + p) /\ 0 < len. Proof. (* induction on the distance to limbo *) intros. set (n := buf_limbo eb - p). generalize (eq_refl n). unfold n at 2. generalize n. clear n. intro n. revert n p. induction n as [|n IND]. (* n = 0 is easy, we are on the last block *) { exists 0. left. simpl. unfold white, In; intuition. } (* inductive step, we either merge the extra char to an existing block or create a block of length 1 *) intros. refine (_ (IND (S p) _)); try omega. clear IND. intros [sufflen IND]. destruct IND as [ [WHITE ATLIMBO] | [ [WHITE [SOLID_AFTER LENNZ]] | [SOLID [WHITE_AFTER LENNZ]] ] ]. (* the next block is the last of the buffer *) + destruct (solid_white_dec (buf_get eb p)) as [S|F]. - exists 1. right. right. split; [|split]. unfold solid. simpl. intuition; congruence. destruct sufflen. rewrite SPEC_limbo by omega. eauto. eauto. omega. - exists (1+ sufflen). left. split. unfold white; intros r [?|REST]. congruence. eauto. omega. (* the next block is white *) + destruct (solid_white_dec (buf_get eb p)) as [s|f]. - exists 1. right. right. split; [|split]. unfold solid. simpl. intuition; congruence. destruct sufflen as [|sufflen]; [omega|]. eauto. omega. - exists (1+ sufflen). right. left. split; [|split]. unfold white; intros r [?|REST]. congruence. eauto. replace (1 + sufflen + p) with (sufflen + S p) by omega. assumption. omega. (* the next block is solid *) + destruct (solid_white_dec (buf_get eb p)) as [s|f]. - exists (1+ sufflen). right. right. split; [|split]. unfold solid. simpl. intuition; congruence. replace (1 + sufflen + p) with (sufflen + S p) by omega. assumption. omega. - exists 1. right. left. split; [|split]. unfold white. simpl. intuition; subst; eauto. destruct sufflen as [|sufflen]; [omega|]. eauto. omega. Qed. Lemma out_white_rec: forall (P: list Rune -> list Rune -> Prop), forall f (WHITE: white f) (BASE: forall a (SP: space a), P a a) (REC: forall sp nl a b (IND: P a b) (SP: space sp) (NL: rclass nl = Newline), P (sp ++ nl :: a) (nl :: b)), P f (out_white f (cl f)). Proof. intros P f. pose (n := cl f). generalize (eq_refl n). unfold n at 1. generalize n. clear n. intro n. revert f. induction n as [|n IND]; intros; rewrite H. + assert (B: out_white f 0 = f /\ space f). - clear REC BASE. induction f. unfold space. simpl. split; [reflexivity|intros ?[]]. assert (A: □ a) by eauto. simpl in *. unfold risnl in *. destruct A as [A|A]; rewrite A in *. omega. split. apply f_equal. apply IHf; eauto. unfold space. intros r [?|IN]. subst. assumption. apply IHf; eauto. - rewrite (proj1 B). apply BASE, B. + cut (exists sp nl rem, f = sp ++ nl :: rem /\ space sp /\ rclass nl = Newline /\ cl rem = n /\ white rem ). - intros [sp [nl [rem [? HF]]]]; subst. replace (out_white (sp ++ nl :: rem) (S n)) with (nl :: out_white rem n). * eapply REC; try eapply HF. replace n with (cl rem) by (apply HF). apply IND; eauto; eapply HF. * clear H WHITE. revert sp nl rem HF. clear. induction sp; intros nl rem [SPACE [NL ?]]; simpl. unfold risnl. replace (rclass nl) with Newline by congruence. replace (n - 0) with n by omega. reflexivity. unfold risnl. replace (rclass a) with Space by (symmetry; eauto). apply IHsp. unfold space in *; intuition. - revert f H WHITE. clear. induction f; simpl. intro. congruence. unfold risnl. case_eq (rclass a); intro CLASS; intros. * refine (_ (IHf H _)); eauto. clear IHf. intros [sp [nl [rem IND]]]. exists (a :: sp). exists nl. exists rem. simpl; intuition; (congruence || eauto). unfold space, In; intuition; congruence. * exists nil. exists a. exists f. unfold space, white, In; intuition. * assert (A: □ a) by eauto. destruct A; congruence. Qed. Lemma wloop_rec: forall (P: list Rune -> list Rune -> Prop), forall eb len p (LEN: len = buf_limbo eb - p) st (BASE: forall a (FL: white a), P a nil) (REC1: forall sp r a b (IND: P a (r :: b)) (SP: space sp) (RSOL: ■ r), P (sp ++ a) (sp ++ r :: b)) (REC2: forall sp nl a b (IND: P a b) (SP: space sp) (NL: rclass nl = Newline) (BNIL: b <> nil), P (sp ++ nl :: a) (nl :: b)) (REC3: forall sl a b (IND: P a b) (SL: solid sl), P (sl ++ a) (sl ++ b)), P (eb_chunk eb p len) (wloop eb (V st p p 0)). Proof. induction len as [n IND] using lt_wf_rec. intros. subst. refine (_ (next_chunk eb p)). intros [len [e | [f | s]]]. (* base case, we are on the last white chunk *) + replace (wloop eb (V st p p 0)) with (wloop eb (V Munching p p 0)). - erewrite beh_white; try (eapply e || reflexivity). rewrite wloop_equation. destruct (len + p >=? buf_limbo eb) as [_|?]; [|omega]. apply BASE. destruct (p >=? buf_limbo eb). replace (buf_limbo eb - p) with 0 by omega. unfold white, In; simpl; intuition. destruct e as [WHITE LEN]. rewrite ( eb_chunk_app (buf_limbo eb - p) (len + p - buf_limbo eb) ) in WHITE by omega. unfold white. intros. apply WHITE, in_or_app. left. assumption. - symmetry. destruct st; [reflexivity|]. case_eq (p >=? buf_limbo eb); intros cmp CMP. * rewrite wloop_equation, wloop_equation, CMP. reflexivity. * rewrite wloop_equation, CMP. rewrite white_test. reflexivity. destruct len as [|len]. left. apply SPEC_limbo. omega. apply (proj1 e). left. reflexivity. (* non empty white chunk followed by a solid rune *) + cut (~ len + p >= buf_limbo eb). intro LIMBO. refine (_ (IND (buf_limbo eb - _) _ (len + p) _ Spitting)); try reflexivity. clear IND. intro IND. replace (wloop eb (V st p p 0)) with (wloop eb (V Munching p p 0)). - erewrite beh_white; try (eapply f || reflexivity). erewrite beh_white_solid; try (eapply f). erewrite (eb_chunk_app len _ (buf_limbo eb - p)). rewrite plus_0_r. assert (STEP: wloop eb (V Spitting (len + p) (len + p) 0) = buf_get eb (len + p) :: wloop eb (V Spitting (S len + p) (len + p) 0) ). { destruct len as [|len]; [omega|]. rewrite wloop_equation. destruct (S len + p >=? buf_limbo eb); [omega|]. rewrite solid_test by (apply f). reflexivity. } rewrite STEP. apply out_white_rec. apply f. intros. apply REC1. rewrite <- STEP. apply IND; eauto. apply SP. apply f. intros. rewrite <- app_assoc. apply REC2; eauto. intro ABS. generalize (app_eq_nil _ _ ABS). intros [_?]. congruence. omega. replace (len + p - p) with len by omega. reflexivity. rewrite plus_0_r. reflexivity. - destruct st; [reflexivity|]. destruct len as [|len]; [omega|]. symmetry. rewrite wloop_equation. destruct (p >=? buf_limbo eb) as [?|_]; [omega|]. rewrite white_test. reflexivity. apply (proj1 f). left. reflexivity. - omega. - intro. rewrite SPEC_limbo in f by assumption. destruct f as [? [? ?]]; congruence. (* non empty solid chunk followed by a white rune *) + cut (len + p <= buf_limbo eb). intro LIMBO. refine (_ (IND (buf_limbo eb - _) _ (len + p) _ Munching)); try reflexivity. clear IND. intro IND. replace (wloop eb (V st p p 0)) with (wloop eb (V Spitting p p 0)). - erewrite beh_solid; try (eapply s || reflexivity). erewrite (eb_chunk_app _ _ (buf_limbo eb - p)). rewrite beh_solid_white. apply REC3. apply IND; eauto. apply s. omega. apply s. omega. - destruct st; [|reflexivity]. cut (■ buf_get eb p). intro SOLID. symmetry. rewrite wloop_equation. destruct (p >=? buf_limbo eb) as [?|_]. { absurd (■ buf_get eb p); [|assumption]. rewrite SPEC_limbo by assumption. congruence. } rewrite solid_test by assumption. replace (p - p) with 0 by omega. reflexivity. destruct len as [|len]; [omega|]. apply (proj1 s). left. reflexivity. - omega. - destruct s as [s [_ l]]. destruct len as [|len]; [omega|clear l]. rewrite (eb_chunk_app len 1) in s. cut (~ len + p >= buf_limbo eb). intro. omega. intro. cut (■ buf_get eb (len + p)). intro SOLID. rewrite SPEC_limbo in SOLID by assumption. congruence. apply s, in_or_app. right. left. reflexivity. omega. Qed. (* Definition and decidability of normal forms. *) Fixpoint normal ty str := match str with | r :: str' => match rclass r with | Newline => ty <> Space /\ normal Newline str' | ty' => normal ty' str' end | nil => ty = Regular end. Lemma normal_Regular: forall str ty, normal ty str -> normal Regular str. Proof. induction str; simpl; intros. reflexivity. destruct (rclass a); (now intuition || congruence). Qed. Lemma normal_same_visual: forall s1 s2 (SV: s1 ⊑ s2) (NORM: normal Regular s2), s1 = s2. Proof. induction 1; intros. + destruct s as [|a s]; [reflexivity|]. cut ( forall s, white s -> ~ normal Space s /\ ~ normal Newline s ). intro A. generalize (H a (or_introl eq_refl)). simpl in NORM. destruct (rclass a). - absurd (normal Space s); [|apply NORM]. apply A. unfold white in *; intuition. - absurd (normal Newline s); [|apply NORM]. apply A. unfold white in *; intuition. - intros [?|?]; congruence. - clear. induction s; simpl. * intros. split; congruence. * intro H. generalize (H a (or_introl eq_refl)). unfold white in *. destruct (rclass a). intros _. split; apply IHs; intuition. intros _. split. intros [? _]; congruence. intros [_ X]; revert X. apply IHs; intuition. intros [?|?]; congruence. + destruct sp; simpl in NORM. - rewrite IHSV. reflexivity. eapply normal_Regular. rewrite H0 in NORM. apply NORM. - replace (rclass r) with Space in NORM. assert (SPACE: space sp). { unfold space in *; intuition. } cut False. intros []. revert nl NORM SPACE H0. clear. induction sp. * simpl. intros. rewrite H0 in NORM. destruct NORM as [? _]; congruence. * simpl. intros. replace (rclass a) with Space in NORM. apply (IHsp nl); unfold space in *; intuition. symmetry. eauto. * symmetry. eauto. + apply f_equal, IHSV, (normal_Regular _ (rclass r)). simpl in NORM. destruct (rclass r); intuition. Qed. Lemma partial_write_same_visual: forall eb len st p (LEN: len = buf_limbo eb - p), wloop eb (V st p p 0) ⊑ eb_chunk eb p len. Proof. intros ? ? ? ? ?. pattern (eb_chunk eb p len). pattern (wloop eb (V st p p 0)). apply wloop_rec; eauto; clear. + intros. constructor. assumption. + intros. induction sp. assumption. simpl; apply sv_sam, IHsp; eauto. + intros. apply sv_eol; eauto. + intros. induction sl. assumption. simpl. apply sv_sam. eauto. Qed. Lemma partial_write_normal: forall len p eb (LEN: len = buf_limbo eb - p) st, normal Regular (wloop eb (V st p p 0)). Proof. intros ? ? ? ? ?. pattern (eb_chunk eb p len). pattern (wloop eb (V st p p 0)). apply wloop_rec; eauto; clear. + intros. reflexivity. + intros. cut (normal Space (sp ++ r :: b)). apply normal_Regular. induction sp as [|s sp]; simpl. - simpl in *. rewrite RSOL in *. assumption. - assert (SPA: rclass s = Space) by eauto. rewrite SPA. eauto. + intros. simpl. rewrite NL. split; [congruence|]. destruct b; [congruence|]. simpl in *. destruct (rclass r); intuition; congruence. + intros. induction sl as [|r sl]. assumption. simpl. replace (rclass r) with Regular. apply IHsl. eauto. symmetry. eauto. Qed. Theorem printing_while_loop_is_correct: forall eb, let output := wloop eb (V Munching 0 0 0) in output ⊑ eb_chunk eb 0 (buf_limbo eb) /\ forall x, x ⊑ output -> x = output. Proof. simpl. split. apply partial_write_same_visual. omega. intros. eauto using normal_same_visual, partial_write_normal. Qed. Print Assumptions printing_while_loop_is_correct. End ProofWrite. (* symbols used ■ □ ⊑ *)