Quelle goal_selector.v Sprache: Coq

Inductive two : bool -> Prop :=
| Zero : two false
| One : two true.

Ltac dup :=
  let H := fresh in assert (forall (P : Prop), P -> P -> P) as H by (intros; trivial);
  apply H; clear H.

Lemma transform : two false <-> two true.
Proof. split; intros _; constructor. Qed.

Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
Proof.
  do 2 dup.
  - repeat split.
    Fail 7:idtac.
    Fail 2-1:idtac.
    1,2,4-6:idtac.
    2-5:exact One.
    par:exact Zero.
  - repeat split.
    3-6:swap 1 4.
    1-5:swap 1 5.
    1-4:exact One.
    all:exact Zero.
  - repeat split.
    1, 3:exact Zero.
    1, 2, 3, 4: exact One.
  - repeat split.
    all:apply transform.
    2, 4, 6:apply transform.
    all:apply transform.
    1-5:apply transform.
    1-6:exact One.
Qed.

Goal True -> True.
Proof.
  intros y.
  1-1:match goal with y : _ |- _ => let x := y in idtac x end.
  Fail 1-1:let x := y in idtac x.
  1:let x := y in idtac x.
  exact I.
Qed.

Goal True /\ (True /\ True).
Proof.
  dup.
  - split; only 2: (split; exact I).
    exact I.
  - split; only 2: split; exact I.
Qed.

Goal True -> exists (x : Prop), x.
Proof.
  intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
Qed.

Goal Prop.
  refine ?[x].
  [x]: refine _.
  exact True.
Qed.

Goal True /\ True /\ True.
Proof.
  split. 2: split.
  1: refine ?[A].
  2: refine ?[B].
  3: refine ?[C].

  (* Success because all A, B, and C are on the shelf. *)
  [A], [B], [C]: shelve.
  Succeed [A], [B], [C]: exact I.

  (* Fails because C is shelved, but A and B are not. *)
  Unshelve.
  [C]: shelve.
  Fail [A], [C]: exact I.
  Fail [B], [C]: exact I.
  Fail 1, [C]: exact I.
  Fail 1-2, [C]: exact I.
  Fail [C], 2: exact I.
  Fail [C], 1-2: exact I.

  (* Success because A, B and C are unshelved. *)
  Unshelve.
  [A], [B], [C]: exact I.
Qed.

(* Strict focusing! *)
Set Default Goal Selector "!".

Goal True -> True /\ True /\ True.
Proof.
  intro.
  split;only 2:split.
  Fail exact I.
  Fail !:exact I.
  1:exact I.
  - !:exact H.
  - exact I.
Qed.

quality100%

¤ 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.