Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Naming.v Sprache: Coq

Original von: Coq^©

(* This file checks the compatibility of naming strategy *)
(* This does not mean that the given naming strategy is good *)

Parameter x2:nat.
Definition foo y := forall x x3 x4 S, x + S = x3 + x4 + y.
Section A.
Variable x3:nat.
Goal forall x x1 x2 x3:nat,
  (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3.
Show.
intros.
Show.

(* Remark: in V8.2, this used to be printed

  x3 : nat
  ============================
   forall x x1 x4 x5 : nat,
   (forall x0 x6 : nat, x0 + x1 = x4 + x6) -> x + x1 = x4 + x5

before intro and

  x3 : nat
  x : nat
  x1 : nat
  x4 : nat
  x0 : nat
  H : forall x x3 : nat, x + x1 = x4 + x3
  ============================
   x + x1 = x4 + x0

after. From V8.3, the quantified hypotheses are printed the sames as
they would be intro. However the hypothesis H remains printed
differently to avoid using the same name in autonomous but nested
subterms *)

Abort.

Goal forall x x1 x2 x3:nat,
  (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) ->
   x+x1 = x2+x3 -> foo (S x).
Show.
unfold foo.
Show.
do 4 intro. (* --> x, x1, x4, x0, ... *)
Show.
do 2 intro.
Show.
do 4 intro.
Show.

(* Remark: in V8.2, this used to be printed

  x3 : nat
  ============================
   forall x x1 x4 x5 : nat,
   (forall x0 x6 : nat,
    x0 + x1 = x4 + x6 ->
    forall x7 x8 x9 S0 : nat, x7 + S0 = x8 + x9 + (S x0 + x1)) ->
   x + x1 = x4 + x5 -> forall x0 x6 x7 S0 : nat, x0 + S0 = x6 + x7 + S x

before the intros and

  x3 : nat
  x : nat
  x1 : nat
  x4 : nat
  x0 : nat
  H : forall x x3 : nat,
      x + x1 = x4 + x3 ->
      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
  H0 : x + x1 = x4 + x0
  x5 : nat
  x6 : nat
  x7 : nat
  S : nat
  ============================
   x5 + S = x6 + x7 + Datatypes.S x

after (note the x5/x0 and the S0/S) *)

Abort.

(* Check naming in hypotheses *)

Goal forall a, (a = 0 -> forall a, a = 0) -> a = 0.
intros.
Show.
apply H with (a:=a). (* test compliance with printing *)
Abort.

End A.

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.