Mercurial > cpdt > repo

annotate src/Tactics.v @ 64:739c2818d6e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Co-inductive evaluation example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 30 Sep 2008 17:47:59 -0400
parents 1a664ff9d2d1
children 21bb59c56b98
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 *
adamc@2 3 * This work is licensed under a
adamc@2 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@2 5 * Unported License.
adamc@2 6 * The license text is available at:
adamc@2 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@2 8 *)
adamc@2 9
adamc@2 10 Require Import List.
adamc@2 11
adamc@38 12 Require Omega.
adamc@38 13
adamc@59 14 Set Implicit Arguments.
adamc@59 15
adamc@2 16
adamc@51 17 Ltac inject H := injection H; clear H; intros; subst.
adamc@51 18
adamc@59 19 Ltac appHyps f :=
adamc@50 20 match goal with
adamc@59 21 | [ H : _ |- _ ] => f H
adamc@59 22 end.
adamc@59 23
adamc@59 24 Ltac inList x ls :=
adamc@59 25 match ls with
adamc@59 26 | x => idtac
adamc@59 27 | (?LS, _) => inList x LS
adamc@59 28 end.
adamc@59 29
adamc@59 30 Ltac app f ls :=
adamc@59 31 match ls with
adamc@59 32 | (?LS, ?X) => f X || app f LS || fail 1
adamc@59 33 | _ => f ls
adamc@59 34 end.
adamc@59 35
adamc@59 36 Ltac all f ls :=
adamc@59 37 match ls with
adamc@59 38 | (?LS, ?X) => f X; all f LS
adamc@59 39 | (_, _) => fail 1
adamc@59 40 | _ => f ls
adamc@59 41 end.
adamc@59 42
adamc@59 43 Ltac simplHyp invOne :=
adamc@59 44 match goal with
adamc@59 45 | [ H : ex _ |- _ ] => destruct H
adamc@59 46
adamc@51 47 | [ H : ?F _ = ?F _ |- _ ] => injection H;
adamc@51 48 match goal with
adamc@51 49 | [ |- _ = _ -> _ ] => clear H; intros; subst
adamc@51 50 end
adamc@51 51 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
adamc@51 52 match goal with
adamc@51 53 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst
adamc@51 54 end
adamc@59 55
adamc@59 56 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
adamc@59 57 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
adamc@50 58 end.
adamc@50 59
adamc@2 60 Ltac rewriteHyp :=
adamc@2 61 match goal with
adamc@2 62 | [ H : _ |- _ ] => rewrite H
adamc@2 63 end.
adamc@2 64
adamc@2 65 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
adamc@2 66
adamc@2 67 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
adamc@2 68
adamc@2 69 Hint Rewrite app_ass : cpdt.
adamc@2 70
adamc@59 71 Definition done (T : Type) (x : T) := True.
adamc@2 72
adamc@59 73 Ltac inster e trace :=
adamc@59 74 match type of e with
adamc@59 75 | forall x : _, _ =>
adamc@59 76 match goal with
adamc@59 77 | [ H : _ |- _ ] =>
adamc@59 78 inster (e H) (trace, H)
adamc@59 79 | _ => fail 2
adamc@59 80 end
adamc@59 81 | _ =>
adamc@59 82 match trace with
adamc@59 83 | (_, _) =>
adamc@59 84 match goal with
adamc@59 85 | [ H : done (trace, _) |- _ ] => fail 1
adamc@59 86 | _ =>
adamc@59 87 let T := type of e in
adamc@59 88 match type of T with
adamc@59 89 | Prop =>
adamc@59 90 generalize e; intro;
adamc@59 91 assert (done (trace, tt)); [constructor | idtac]
adamc@59 92 | _ =>
adamc@59 93 all ltac:(fun X =>
adamc@59 94 match goal with
adamc@59 95 | [ H : done (_, X) |- _ ] => fail 1
adamc@59 96 | _ => idtac
adamc@59 97 end) trace;
adamc@59 98 let i := fresh "i" in (pose (i := e);
adamc@59 99 assert (done (trace, i)); [constructor | idtac])
adamc@59 100 end
adamc@59 101 end
adamc@59 102 end
adamc@59 103 end.
adamc@59 104
adamc@59 105 Ltac crush' lemmas invOne :=
adamc@64 106 let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; subst); try congruence
adamc@59 107 in (sintuition; rewriter;
adamc@59 108 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
adamc@59 109 repeat (simplHyp invOne; intuition));
adamc@59 110 sintuition; try omega).
adamc@59 111
adamc@59 112 Ltac crush := crush' tt fail.