Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_5757.v Sprache: Coq

Original von: Coq^©

(* Check that resolved status of evars follows "restrict" *)

Axiom H : forall (v : nat), Some 0 = Some v -> True.
Lemma L : True.
eapply H with _;
match goal with
  | |- Some 0 = Some ?v => change (Some (0+0) = Some v)
end.
Abort.

(* The original example *)

Set Default Proof Using "Type".

Module heap_lang.

Inductive expr :=
  | InjR (e : expr).

Inductive val :=
  | InjRV (v : val).

Bind Scope val_scope with val.

Fixpoint of_val (v : val) : expr :=
  match v with
  | InjRV v => InjR (of_val v)
  end.

Fixpoint to_val (e : expr) : option val := None.

End heap_lang.
Export heap_lang.

Module W.
Inductive expr :=
  | Val (v : val)
  (* Sums *)
  | InjR (e : expr).

Fixpoint to_expr (e : expr) : heap_lang.expr :=
  match e with
  | Val v => of_val v
  | InjR e => heap_lang.InjR (to_expr e)
  end.

End W.

Section Tests.

  Context (iProp: Type).
  Context (WPre: expr -> Prop).

  Context (tac_wp_alloc :
             forall (e : expr) (v : val),
               to_val e = Some v -> WPre e).

  Lemma push_atomic_spec (x: val) :
    WPre (InjR (of_val x)).
  Proof.
(* This works. *)
eapply tac_wp_alloc with _.
match goal with
  | |- to_val ?e = Some ?v =>
    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
end.
Undo. Undo.
(* This is fixed *)
eapply tac_wp_alloc with _;
match goal with
  | |- to_val ?e = Some ?v =>
    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
end.
Abort.
End Tests.

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