Quelle bug_17487_2.v Sprache: Coq

(* Potpourri of inconsistencies between intros [] and destruct and fringe behaviours w.r.t. dependent metas *)

Goal forall (f : nat -> bool), True.
Proof.
intros [].
+ match goal with [ |- nat ] => exact 0 end.
+ match goal with [ |- True ] => exact I end.
+ match goal with [ |- True ] => exact I end.
Qed.

Goal forall (f : nat -> bool), True.
Proof.
intros f; destruct f.
+ match goal with [ |- nat ] => exact 0 end.
+ match goal with [ |- True ] => exact I end.
+ match goal with [ |- True ] => exact I end.
Qed.

Goal forall (f : nat -> bool), f = f.
Proof.
Fail intros [].
Abort.

Goal forall (f : nat -> bool), f = f.
Proof.
intros f; destruct f.
+ match goal with [ |- nat ] => exact 0 end.
+ match goal with [ |- f = f ] => reflexivity end.
+ match goal with [ |- f = f ] => reflexivity end.
Qed.

Goal forall (f : forall n : nat, 0 = n), True.
Proof.
Fail intros [].
Abort.

Goal forall (f : forall n : nat, 0 = n), True.
Proof.
Fail intros f; destruct f.
Abort.

Goal forall (f : forall n : nat, 0 = n), f = f.
Proof.
Fail intros [].
Abort.

Goal forall (f : forall n : nat, 0 = n), f = f.
Proof.
Fail intros f; destruct f.
Abort.

Goal forall (f : forall n : nat, n = 0), True.
Proof.
Fail intros [].
Abort.

Goal forall (f : forall n : nat, n = 0), True.
Proof.
Fail intros f; destruct f.
Abort.

quality98%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.