Mercurial > cpdt > repo

comparison src/Match.v @ 138:59a2110acf64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Uncommented matcher code
author Adam Chlipala <adamc@hcoop.net>
date Sun, 26 Oct 2008 16:45:19 -0400
parents c0bda476b44b
children a9e90bacbd16
comparison
equal deleted inserted replaced
137:c0bda476b44b 138:59a2110acf64
265 The last rule implements modus ponens. The most interesting part is the use of the Ltac-level [let] with a [fresh] expression. [fresh] takes in a name base and returns a fresh hypothesis variable based on that name. We use the new name variable [H] as the name we assign to the result of modus ponens. The use of [generalize] changes our conclusion to be an implication from [Q]. We clear the original hypothesis and move [Q] into the context with name [H]. *) 265 The last rule implements modus ponens. The most interesting part is the use of the Ltac-level [let] with a [fresh] expression. [fresh] takes in a name base and returns a fresh hypothesis variable based on that name. We use the new name variable [H] as the name we assign to the result of modus ponens. The use of [generalize] changes our conclusion to be an implication from [Q]. We clear the original hypothesis and move [Q] into the context with name [H]. *)
266 266
267 Section propositional. 267 Section propositional.
268 Variables P Q R : Prop. 268 Variables P Q R : Prop.
269 269
270 Theorem and_comm : (P \/ Q \/ False) /\ (P -> Q) -> True /\ Q. 270 Theorem propositional : (P \/ Q \/ False) /\ (P -> Q) -> True /\ Q.
271 my_tauto. 271 my_tauto.
272 Qed. 272 Qed.
273 End propositional. 273 End propositional.
274 274
275 (** It was relatively easy to implement modus ponens, because we do not lose information by clearing every implication that we use. If we want to implement a similarly-complete procedure for quantifier instantiation, we need a way to ensure that a particular proposition is not already included among our hypotheses. To do that effectively, we first need to learn a bit more about the semantics of [match]. 275 (** It was relatively easy to implement modus ponens, because we do not lose information by clearing every implication that we use. If we want to implement a similarly-complete procedure for quantifier instantiation, we need a way to ensure that a particular proposition is not already included among our hypotheses. To do that effectively, we first need to learn a bit more about the semantics of [match].
543 ============================ 543 ============================
544 False 544 False
545 ]] *) 545 ]] *)
546 Abort. 546 Abort.
547 547
548
549 (** * Proof Search in Continuation-Passing Style *)
550
551 Definition imp (P1 P2 : Prop) := P1 -> P2.
552
553 Infix "-->" := imp (no associativity, at level 95).
554
555 Ltac imp := unfold imp; firstorder.
556
557 Theorem and_True_prem : forall P Q,
558 (P /\ True --> Q)
559 -> (P --> Q).
560 imp.
561 Qed.
562
563 Theorem and_True_conc : forall P Q,
564 (P --> Q /\ True)
565 -> (P --> Q).
566 imp.
567 Qed.
568
569 Theorem assoc_prem1 : forall P Q R S,
570 (P /\ (Q /\ R) --> S)
571 -> ((P /\ Q) /\ R --> S).
572 imp.
573 Qed.
574
575 Theorem assoc_prem2 : forall P Q R S,
576 (Q /\ (P /\ R) --> S)
577 -> ((P /\ Q) /\ R --> S).
578 imp.
579 Qed.
580
581 Theorem comm_prem : forall P Q R,
582 (P /\ Q --> R)
583 -> (Q /\ P --> R).
584 imp.
585 Qed.
586
587 Theorem assoc_conc1 : forall P Q R S,
588 (S --> P /\ (Q /\ R))
589 -> (S --> (P /\ Q) /\ R).
590 imp.
591 Qed.
592
593 Theorem assoc_conc2 : forall P Q R S,
594 (S --> Q /\ (P /\ R))
595 -> (S --> (P /\ Q) /\ R).
596 imp.
597 Qed.
598
599 Theorem comm_conc : forall P Q R,
600 (R --> P /\ Q)
601 -> (R --> Q /\ P).
602 imp.
603 Qed.
604
605 Ltac search_prem tac :=
606 let rec search P :=
607 tac
608 || (apply and_True_prem; tac)
609 || match P with
610 | ?P1 /\ ?P2 =>
611 (apply assoc_prem1; search P1)
612 || (apply assoc_prem2; search P2)
613 end
614 in match goal with
615 | [ |- ?P /\ _ --> _ ] => search P
616 | [ |- _ /\ ?P --> _ ] => apply comm_prem; search P
617 | [ |- _ --> _ ] => progress (tac || (apply and_True_prem; tac))
618 end.
619
620 Ltac search_conc tac :=
621 let rec search P :=
622 tac
623 || (apply and_True_conc; tac)
624 || match P with
625 | ?P1 /\ ?P2 =>
626 (apply assoc_conc1; search P1)
627 || (apply assoc_conc2; search P2)
628 end
629 in match goal with
630 | [ |- _ --> ?P /\ _ ] => search P
631 | [ |- _ --> _ /\ ?P ] => apply comm_conc; search P
632 | [ |- _ --> _ ] => progress (tac || (apply and_True_conc; tac))
633 end.
634
635 Theorem False_prem : forall P Q,
636 False /\ P --> Q.
637 imp.
638 Qed.
639
640 Theorem True_conc : forall P Q : Prop,
641 (P --> Q)
642 -> (P --> True /\ Q).
643 imp.
644 Qed.
645
646 Theorem Match : forall P Q R : Prop,
647 (Q --> R)
648 -> (P /\ Q --> P /\ R).
649 imp.
650 Qed.
651
652 Theorem ex_prem : forall (T : Type) (P : T -> Prop) (Q R : Prop),
653 (forall x, P x /\ Q --> R)
654 -> (ex P /\ Q --> R).
655 imp.
656 Qed.
657
658 Theorem ex_conc : forall (T : Type) (P : T -> Prop) (Q R : Prop) x,
659 (Q --> P x /\ R)
660 -> (Q --> ex P /\ R).
661 imp.
662 Qed.
663
664 Theorem imp_True : forall P,
665 P --> True.
666 imp.
667 Qed.
668
669 Ltac matcher :=
670 intros;
671 repeat search_prem ltac:(apply False_prem || (apply ex_prem; intro));
672 repeat search_conc ltac:(apply True_conc || eapply ex_conc || search_prem ltac:(apply Match));
673 try apply imp_True.
674
675 Theorem t2 : forall P Q : Prop,
676 Q /\ (P /\ False) /\ P --> P /\ Q.
677 matcher.
678 Qed.
679
680 Theorem t3 : forall P Q R : Prop,
681 P /\ Q --> Q /\ R /\ P.
682 matcher.
683 Abort.
684
685 Theorem t4 : forall (P : nat -> Prop) Q, (exists x, P x /\ Q) --> Q /\ (exists x, P x).
686 matcher.
687 Qed.
688