Quelle bug_4781.v Sprache: Coq

Ltac force_clear :=
  clear;
  repeat match goal with
         | [ H : _ |- _ ] => clear H
         | [ H := _ |- _ ] => clearbody H
         end.

Class abstract_term {T} (x : T) := by_abstract_term : T.
#[export] Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances.

Goal True.
(* These work: *)
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  pose x.
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let x := (eval cbv iota in (let v : T := x in v)) in
  pose x.
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let x := match constr:(Set) with ?y => constr:(y) end in
  pose x.
(* This fails with an error: *)
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let x := match constr:(x) with ?y => constr:(y) end in
  pose x. (* The command has indeed failed with message:
Error: Variable y should be bound to a term. *)
(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let x := match constr:(x) with ?y => y end in
  pose x.
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let x := (eval cbv iota in x) in
  pose x.
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let x := type of x in
  pose x. (* should succeed *)
  let term := constr:(I) in
  let T := type of term in
  let x := constr:(_ : abstract_term term) in
  let x := type of x in
  pose x. (* should succeed *)

(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time.

Even stranger, consider:*)
  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let y := (eval cbv iota in (let v : T := x in v)) in
  pose y;
    let x' := fresh "x'" in
    pose x as x'.
      let x := (eval cbv delta [x'] in x') in
      pose x;
      let z := (eval cbv iota in x) in
      pose z.

(*This works fine.  But if I change the period to a semicolon, I get:*)

      let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let y := (eval cbv iota in (let v : T := x in v)) in
  pose y;
    let x' := fresh "x'" in
    pose x as x';
      let x := (eval cbv delta [x'] in x') in
      pose x. (* Anomaly: Uncaught exception Not_found. Please report. *)
(* should succeed *)
(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)

  let term := constr:(I) in
  let T := type of term in
  let x := constr:((_ : abstract_term term) : T) in
  let y := (eval cbv iota in (let v : T := x in v)) in
  pose y;
    let x' := fresh "x'" in
    pose x as x';
      let x := (eval cbv delta [x'] in x') in
      let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
      idtac. (* should succeed *)
  exact I.
Qed.

quality99%

¤ Dauer der Verarbeitung: 0.5 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.