Commit 1aa50cba authored by Armaël Guéneau's avatar Armaël Guéneau

Fix demo

parent 97978996
......@@ -846,6 +846,7 @@ Proof using.
inverts M4. subst*.
Qed.
(* Used by xgc_credit *)
Lemma credits_le_rest : forall (n m : int), (* todo: move later, inverse hyp *)
n <= m -> exists H', affine H' /\ \$ m ==> \$ n \* H'.
Proof using.
......
......@@ -3901,8 +3901,7 @@ Tactic Notation "xpay_skip" := xpay_fake tt.
between two credit expressions, e.g. [m <= n].
This inequality is used to change [\$n] to [\$m] in the
precondition of the goal.
LATER: add demos for this tactic. *)
*)
Ltac xgc_credit_core HP :=
let H := fresh in
......@@ -3913,14 +3912,14 @@ Ltac xgc_credit_core HP :=
Tactic Notation "xgc_credit" constr(HP) :=
xgc_credit_core HP.
Goal forall m n B (F : ~~B) Q,
Lemma demo_xgc_credit_core : forall m n B (F : ~~B) Q,
m <= n ->
is_local F ->
F (\$m) Q ->
F (\$n) Q.
Proof.
introv H L HH.
xgc_credit_core H.
xgc_credit H.
assumption.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment