Mercurial > cpdt > repo

comparison src/MoreDep.v @ 86:fd505bcb5632

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of certified regexp matcher
author Adam Chlipala <adamc@hcoop.net>
date Mon, 06 Oct 2008 14:33:11 -0400
parents 3746a2ded8da
children a0b8b550e265
comparison
equal deleted inserted replaced
85:3746a2ded8da 86:fd505bcb5632
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith Bool List. 11 Require Import Arith Bool List.
12 12
13 Require Import Tactics. 13 Require Import Tactics MoreSpecif.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
340 repeat (match goal with 340 repeat (match goal with
341 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) 341 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
342 | [ |- (if ?E then _ else _) = _ ] => destruct E 342 | [ |- (if ?E then _ else _) = _ ] => destruct E
343 end; crush). 343 end; crush).
344 Qed. 344 Qed.
345
346
347 (** * A Certified Regular Expression Matcher *)
348
349 Require Import Ascii String.
350 Open Scope string_scope.
351
352 Inductive regexp : (string -> Prop) -> Set :=
353 | Char : forall ch : ascii,
354 regexp (fun s => s = String ch "")
355 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
356 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
357
358 Open Scope specif_scope.
359
360 Lemma length_emp : length "" <= 0.
361 crush.
362 Qed.
363
364 Lemma append_emp : forall s, s = "" ++ s.
365 crush.
366 Qed.
367
368 Ltac substring :=
369 crush;
370 repeat match goal with
371 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
372 end.
373
374 Lemma substring_le : forall s n m,
375 length (substring n m s) <= m.
376 induction s; substring.
377 Qed.
378
379 Lemma substring_all : forall s,
380 substring 0 (length s) s = s.
381 induction s; substring.
382 Qed.
383
384 Lemma substring_none : forall s n,
385 substring n 0 s = EmptyString.
386 induction s; substring.
387 Qed.
388
389 Hint Rewrite substring_all substring_none : cpdt.
390
391 Lemma substring_split : forall s m,
392 substring 0 m s ++ substring m (length s - m) s = s.
393 induction s; substring.
394 Qed.
395
396 Lemma length_app1 : forall s1 s2,
397 length s1 <= length (s1 ++ s2).
398 induction s1; crush.
399 Qed.
400
401 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
402
403 Lemma substring_app_fst : forall s2 s1 n,
404 length s1 = n
405 -> substring 0 n (s1 ++ s2) = s1.
406 induction s1; crush.
407 Qed.
408
409 Lemma substring_app_snd : forall s2 s1 n,
410 length s1 = n
411 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
412 Hint Rewrite <- minus_n_O : cpdt.
413
414 induction s1; crush.
415 Qed.
416
417 Hint Rewrite substring_app_fst substring_app_snd using assumption : cpdt.
418
419 Section split.
420 Variables P1 P2 : string -> Prop.
421 Variable P1_dec : forall s, {P1 s} + {~P1 s}.
422 Variable P2_dec : forall s, {P2 s} + {~P2 s}.
423
424 Variable s : string.
425
426 Definition split' (n : nat) : n <= length s
427 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
428 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2}.
429 refine (fix F (n : nat) : n <= length s
430 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
431 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2} :=
432 match n return n <= length s
433 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
434 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2} with
435 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
436 | S n' => fun _ => (P1_dec (substring 0 (S n') s) && P2_dec (substring (S n') (length s - S n') s))
437 || F n' _
438 end); clear F; crush; eauto 7;
439 match goal with
440 | [ _ : length ?S <= 0 |- _ ] => destruct S
441 | [ _ : length ?S' <= S ?N |- _ ] =>
442 generalize (eq_nat_dec (length S') (S N)); destruct 1
443 end; crush.
444 Defined.
445
446 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
447 + {forall s1 s2, s = s1 ++ s2 -> ~P1 s1 \/ ~P2 s2}.
448 refine (Reduce (split' (n := length s) _)); crush; eauto.
449 Defined.
450 End split.
451
452 Implicit Arguments split [P1 P2].
453
454 Lemma app_cong : forall x1 y1 x2 y2,
455 x1 = x2
456 -> y1 = y2
457 -> x1 ++ y1 = x2 ++ y2.
458 congruence.
459 Qed.
460
461 Hint Resolve app_cong.
462
463 Definition matches P (r : regexp P) s : {P s} + { ~P s}.
464 refine (fix F P (r : regexp P) s : {P s} + { ~P s} :=
465 match r with
466 | Char ch => string_dec s (String ch "")
467 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
468 end); crush;
469 match goal with
470 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
471 end;
472 tauto.
473 Defined.
474
475 Example hi := Concat (Char "h"%char) (Char "i"%char).
476 Eval simpl in matches hi "hi".
477 Eval simpl in matches hi "bye".