|
(* 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.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
