Commit 86de92cf authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Elimination of pure facts using Coq introduction patterns for iAssert.

parent d6dc89b4
...@@ -40,8 +40,10 @@ Context management ...@@ -40,8 +40,10 @@ Context management
`H`. `H`.
- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and - `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
put `P` in the context of the original goal. The specialization pattern put `P` in the context of the original goal. The specialization pattern
`spat` specifies which hypotheses will be consumed by proving `P` and the `spat` specifies which hypotheses will be consumed by proving `P`. The
introduction pattern `ipat` specifies how to eliminate `P`. introduction pattern `ipat` specifies how to eliminate `P`.
- `iAssert P with "spat" as %cpat` : assert `P` and eliminate it using the Coq
introduction pattern `cpat`.
Introduction of logical connectives Introduction of logical connectives
----------------------------------- -----------------------------------
......
...@@ -833,7 +833,7 @@ Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) ...@@ -833,7 +833,7 @@ Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ltac:(iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 )). ltac:(iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 )).
(** * Assert *) (** * Assert *)
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) := Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) :=
let H := iFresh in let H := iFresh in
let Hs := spec_pat.parse Hs in let Hs := spec_pat.parse Hs in
lazymatch Hs with lazymatch Hs with
...@@ -842,7 +842,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) := ...@@ -842,7 +842,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
[env_cbv; reflexivity [env_cbv; reflexivity
|(*goal*) |(*goal*)
|apply _ || fail "iAssert:" Q "not persistent" |apply _ || fail "iAssert:" Q "not persistent"
|iDestructHyp H as pat] |tac H]
| [SGoal ?k ?lr ?Hs] => | [SGoal ?k ?lr ?Hs] =>
eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *) eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
[match k with [match k with
...@@ -851,13 +851,21 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) := ...@@ -851,13 +851,21 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
end end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found" |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity| |env_cbv; reflexivity|
|iDestructHyp H as pat] |tac H]
| ?pat => fail "iAssert: invalid pattern" pat | ?pat => fail "iAssert: invalid pattern" pat
end. end.
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssertCore Q with Hs as (fun H => iDestructHyp H as pat).
Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) := Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
iAssert Q with "[]" as pat. iAssert Q with "[]" as pat.
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs)
"as" "%" simple_intropattern(pat) :=
iAssertCore Q with Hs as (fun H => iPure H as pat).
Tactic Notation "iAssert" open_constr(Q) "as" "%" simple_intropattern(pat) :=
iAssert Q with "[]" as %pat.
(** * Rewrite *) (** * Rewrite *)
Local Ltac iRewriteFindPred := Local Ltac iRewriteFindPred :=
match goal with match goal with
......
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