(* 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 ■ □ ⊑ *)