Quellcode-Bibliothek name_mangling.v Sprache: Coq

Set Mangle Names.

(* Check that refine policy of redefining previous names make these names private *)

Goal True -> True.
intro.
Fail exact H.
exact _0.
Abort.

Unset Mangle Names.
Goal True -> True.
intro; exact H.
Abort.

Set Mangle Names.
Set Mangle Names Prefix "baz".
Goal True -> True.
intro.
Fail exact H.
Fail exact _0.
exact baz0.
Abort.

Goal True -> True.
intro; assumption.
Abort.

Goal True -> True.
intro x; exact x.
Abort.

Goal forall x y, x+y=0.
intro x.
refine (fun x => _).
Fail Check x0.
Check x.
Abort.

(* Example from Emilio *)

Goal forall b : False, b = b.
intro b.
refine (let b := I in _).
Fail destruct b0.
Abort.

(* Example from Cyprien *)

Goal True -> True.
Proof.
  refine (fun _ => _).
  Fail exact t.
Abort.

(* Example from Jason *)

Goal False -> False.
intro H.
abstract exact H.
Abort.

(* Variant *)

Goal False -> False.
intro.
Fail abstract exact H.
Abort.

(* Example from Jason *)

Lemma lem1 : False -> False.
intro H.
(* Name H' is from Ltac here, so it preserves the privacy *)
(* But abstract messes everything up *)
let H' := H in abstract exact H'.
Qed.

(* Variant *)

Goal False -> False.
intro.
Fail let H' := H in abstract exact H'.
Abort.

(* Indirectly testing preservation of names by move (derived from Jason) *)

Inductive nat2 := S2 (_ _ : nat2).
Goal forall t : nat2, True.
  intro t.
  let IHt1 := fresh "IHt1" in
  let IHt2 := fresh "IHt2" in
  induction t as [? IHt1 ? IHt2].
  Fail exact IHt1.
Abort.

(* Example on "pose proof" (from Jason) *)

Goal False -> False.
intro; pose proof I as H0.
Fail exact H.
Abort.

(* Testing the approach for which non alpha-renamed quantified names are user-generated *)

Section foo.
Context (b : True).
Goal forall b : False, b = b.
Fail destruct b0.
Abort.

Lemma lem2 : forall b : False, b = b.
now destruct b.
Qed.
End foo.

(* Test stability of "fix" *)

Lemma a : forall n, n = 0.
Proof.
fix a 1.
Check a.
Fail fix a 1.
Abort.

(* Test stability of "induction" *)

Lemma a : forall n : nat, n = n.
Proof.
intro n; induction n as [ | n IHn ].
- auto.
- Check n.
  Check IHn.
Abort.

Inductive I := C : I -> I -> I.

Lemma a : forall n : I, n = n.
Proof.
intro n; induction n as [ n1 IHn1 n2 IHn2 ].
Check n1.
Check n2.
apply f_equal2.
+ apply IHn1.
+ apply IHn2.
Qed.

(* Testing remember *)

Lemma c : 0 = 0.
Proof.
remember 0 as x eqn:Heqx.
Check Heqx.
Abort.

Lemma c : forall Heqx, Heqx -> 0 = 0.
Proof.
intros Heqx X.
remember 0 as x.
Fail Check Heqx0. (* Heqx0 is not canonical *)
Abort.

(* An example by Jason from the discussion for PR #268 *)

Goal nat -> Set -> True.
  intros x y.
  match goal with
  | [ x : _, y : _ |- _ ]
    => let z := fresh "z" in
      rename y into z, x into y;
        let x' := fresh "x" in
        rename z into x'
  end.
  revert y. (* x has been explicitly moved to y *)
  Fail revert x. (* x comes from "fresh" *)
Abort.

Goal nat -> Set -> True.
  intros.
  match goal with
  | [ x : _, y : _ |- _ ]
    => let z := fresh "z" in
      rename y into z, x into y;
        let x' := fresh "x" in
        rename z into x'
  end.
  Fail revert y. (* generated by intros *)
  Fail revert x. (* generated by intros *)
Abort.

quality93%

¤ 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.0.3Bemerkung: ¤

*Bot Zugriff

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.