diff options
Diffstat (limited to 'test-suite/success/ltac.v')
-rw-r--r-- | test-suite/success/ltac.v | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v new file mode 100644 index 00000000..55aa110d --- /dev/null +++ b/test-suite/success/ltac.v @@ -0,0 +1,70 @@ +(* The tactic language *) + +(* Submitted by Pierre Crégut *) +(* Checks substitution of x *) +Tactic Definition f x := Unfold x; Idtac. + +Lemma lem1 : (plus O O) = O. +f plus. +Reflexivity. +Qed. + +(* Submitted by Pierre Crégut *) +(* Check syntactic correctness *) +Recursive Tactic Definition F x := Idtac; (G x) +And G y := Idtac; (F y). + +(* Check that Match Context keeps a closure *) +Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a. + +Lemma lem2 : True. +U. +Qed. + +(* Check that Match giving non-tactic arguments are evaluated at Let-time *) + +Tactic Definition B := + Let y = (Match Context With [ z:? |- ? ] -> z) In + Intro H1; Exact y. + +Lemma lem3 : True -> False -> True -> False. +Intros H H0. +B. (* y is H0 if at let-time, H1 otherwise *) +Qed. + +(* Checks the matching order of hypotheses *) +Tactic Definition Y := Match Context With [ x:?; y:? |- ? ] -> Apply x. +Tactic Definition Z := Match Context With [ y:?; x:? |- ? ] -> Apply x. + +Lemma lem4 : (True->False) -> (False->False) -> False. +Intros H H0. +Z. (* Apply H0 *) +Y. (* Apply H *) +Exact I. +Qed. + +(* Check backtracking *) +Lemma back1 : (0)=(1)->(0)=(0)->(1)=(1)->(0)=(0). +Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Qed. + +Lemma back2 : (0)=(0)->(0)=(1)->(1)=(1)->(0)=(0). +Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Qed. + +Lemma back3 : (0)=(0)->(1)=(1)->(0)=(1)->(0)=(0). +Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Qed. + +(* Check context binding *) +Tactic Definition sym t := Match t With [C[?1=?2]] -> Inst C[?1=?2]. + +Lemma sym : ~(0)=(1)->~(1)=(0). +Intro H. +Let t = (sym (Check H)) In Assert t. +Exact H. +Intro H1. +Apply H. +Symmetry. +Assumption. +Qed. |