Quelle bug_5757.v Sprache: 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.

quality99%

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