Quelle strategy.v Sprache: Coq

Notation aid := (@id) (only parsing).
Notation idn := id (only parsing).
Ltac unfold_id := unfold id.

Fixpoint fact (n : nat)
  := match n with
     | 0 => 1
     | S n => (S n) * fact n
     end.

Opaque id.
Goal id (fact 100) = fact 100.
  Strategy expand [id].
  Time Timeout 5 reflexivity. (* should be instant *)
  (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Timeout 5 Defined.
(* Finished transaction in 0.001 secs (0.u,0.s) (successful) *)

Goal True.
  let x := smart_global:(id) in unfold x.
  let x := smart_global:(aid) in unfold x.
  let x := smart_global:(idn) in unfold x.
Abort.

Goal id 0 = 0.
  Opaque id.
  assert_fails unfold_id.
  Transparent id.
  assert_succeeds unfold_id.
  Opaque id.
  Strategy 0 [id].
  assert_succeeds unfold_id.
  Strategy 1 [id].
  assert_succeeds unfold_id.
  Strategy -1 [id].
  assert_succeeds unfold_id.
  Strategy opaque [id].
  assert_fails unfold_id.
  Strategy transparent [id].
  assert_succeeds unfold_id.
  Opaque id.
  Strategy expand [id].
  assert_succeeds unfold_id.
  reflexivity.
Qed.
Goal id 0 = 0.
  Opaque aid.
  assert_fails unfold_id.
  Transparent aid.
  assert_succeeds unfold_id.
  Opaque aid.
  Strategy 0 [aid].
  assert_succeeds unfold_id.
  Strategy 1 [aid].
  assert_succeeds unfold_id.
  Strategy -1 [aid].
  assert_succeeds unfold_id.
  Strategy opaque [aid].
  assert_fails unfold_id.
  Strategy transparent [aid].
  assert_succeeds unfold_id.
  Opaque aid.
  Strategy expand [aid].
  assert_succeeds unfold_id.
  reflexivity.
Qed.
Goal id 0 = 0.
  Opaque idn.
  assert_fails unfold_id.
  Transparent idn.
  assert_succeeds unfold_id.
  Opaque idn.
  Strategy 0 [idn].
  assert_succeeds unfold_id.
  Strategy 1 [idn].
  assert_succeeds unfold_id.
  Strategy -1 [idn].
  assert_succeeds unfold_id.
  Strategy opaque [idn].
  assert_fails unfold_id.
  Strategy transparent [idn].
  assert_succeeds unfold_id.
  Opaque idn.
  Strategy expand [idn].
  assert_succeeds unfold_id.
  reflexivity.
Qed.

quality94%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.