diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /test-suite/success/paralleltac.v | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/success/paralleltac.v')
-rw-r--r-- | test-suite/success/paralleltac.v | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/test-suite/success/paralleltac.v b/test-suite/success/paralleltac.v new file mode 100644 index 00000000..94ff96ef --- /dev/null +++ b/test-suite/success/paralleltac.v @@ -0,0 +1,46 @@ +Fixpoint fib n := match n with + | O => 1 + | S m => match m with + | O => 1 + | S o => fib o + fib m end end. +Ltac sleep n := + try (assert (fib n = S (fib n)) by reflexivity). +(* Tune that depending on your PC *) +Let time := 18. + +Axiom P : nat -> Prop. +Axiom P_triv : Type -> forall x, P x. +Ltac solve_P := + match goal with |- P (S ?X) => + sleep time; exact (P_triv Type _) + end. + +Lemma test_old x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T1: linear". +Time all: solve_P. +Qed. + +Lemma test_ok x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T2: parallel". +Time par: solve_P. +Qed. + +Lemma test_fail x : P (S x) /\ P x /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T3: linear failure". +Fail Time all: solve_P. +all: apply (P_triv Type). +Qed. + +Lemma test_fail2 x : P (S x) /\ P x /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T4: parallel failure". +Fail Time par: solve_P. +all: apply (P_triv Type). +Qed. |