Commit 3f069634 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'robbert/iAssumption' into 'master'

Make `iAssumption` work on `⊢ ...` premises in the Coq context.

See merge request iris/iris!398
parents a7b4c684 ba3f6ce2
......@@ -78,6 +78,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
`not_stuck_fill``not_stuck_fill_inv`.
- Use the non-`_inv` names (that freed up) for the forwards directions:
`reducible_fill`, `reducible_no_obs_fill`, `irreducible_fill_inv`.
* The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
**Changes in heap_lang:**
......
......@@ -24,7 +24,10 @@ Applying hypotheses and lemmas
------------------------------
- `iExact "H"` : finish the goal if the conclusion matches the hypothesis `H`
- `iAssumption` : finish the goal if the conclusion matches any hypothesis
- `iAssumption` : finish the goal if the conclusion matches any hypothesis in
either the proofmode or the Coq context. Only hypotheses in the Coq context
that are _syntactically_ of the shape `⊢ P` are recognized by this tactic
(this means that assumptions of the shape `P ⊢ Q` are not recognized).
- `iApply pm_trm` : match the conclusion of the current goal against the
conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
proof mode terms below.
......
......@@ -515,8 +515,7 @@ Tactic failure: iExact: "HQ" not found.
The command has indeed failed with message:
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
Tactic failure: iExact: "HP"
not absorbing and the remaining hypotheses not affine.
Tactic failure: iExact: remaining hypotheses not affine and the goal not absorbing.
"iClear_fail"
: string
The command has indeed failed with message:
......@@ -581,13 +580,19 @@ Tactic failure: iApply: cannot apply P.
"iApply_fail_not_affine_1"
: string
The command has indeed failed with message:
Tactic failure: iApply: Q
not absorbing and the remaining hypotheses not affine.
Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
"iApply_fail_not_affine_2"
: string
The command has indeed failed with message:
Tactic failure: iApply: Q
not absorbing and the remaining hypotheses not affine.
Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
"iAssumption_fail_not_affine_1"
: string
The command has indeed failed with message:
Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
"iAssumption_fail_not_affine_2"
: string
The command has indeed failed with message:
Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
"iRevert_wrong_var"
: string
The command has indeed failed with message:
......
......@@ -316,6 +316,12 @@ Proof. iIntros "H". iMod "H". done. Qed.
Lemma test_iAssumption_False P : False - P.
Proof. iIntros "H". done. Qed.
Lemma test_iAssumption_coq_1 P Q : ( Q) <affine> P - Q.
Proof. iIntros (HQ) "_". iAssumption. Qed.
Lemma test_iAssumption_coq_2 P Q : ( Q) <affine> P - Q.
Proof. iIntros (HQ) "_". iAssumption. Qed.
(* Check instantiation and dependent types *)
Lemma test_iSpecialize_dependent_type (P : n, vec nat n PROP) :
( n v, P n v) - n v, P n v.
......@@ -1018,9 +1024,17 @@ Lemma iApply_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.
Check "iApply_fail_not_affine_2".
Lemma iApply_fail_not_affine_1 P Q R : P - R - (R - Q) - Q.
Lemma iApply_fail_not_affine_2 P Q R : P - R - (R - Q) - Q.
Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
Check "iAssumption_fail_not_affine_1".
Lemma iAssumption_fail_not_affine_1 P Q : P - Q - Q.
Proof. iIntros "HP HQ". Fail iAssumption. Abort.
Check "iAssumption_fail_not_affine_2".
Lemma iAssumption_fail_not_affine_2 P Q : ( Q) P - Q.
Proof. iIntros (HQ) "HP". Fail iAssumption. Abort.
Check "iRevert_wrong_var".
Lemma iRevert_wrong_var (k : nat) (Φ : nat PROP) : Φ (S k).
Proof.
......
......@@ -91,6 +91,21 @@ Proof.
- rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Qed.
Lemma tac_assumption_coq Δ P Q :
( P)
FromAssumption true P Q
(if env_spatial_is_nil Δ then TCTrue
else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ)))
envs_entails Δ Q.
Proof.
rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
rewrite envs_entails_eq -(left_id emp%I bi_sep (of_envs Δ)).
rewrite -bi.intuitionistically_emp HP HPQ.
destruct (env_spatial_is_nil _) eqn:?.
- by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
- destruct H; by rewrite sep_elim_l.
Qed.
Lemma tac_rename Δ i j p P Q :
envs_lookup i Δ = Some (p,P)
match envs_simple_replace i p (Esnoc Enil j P) Δ with
......
......@@ -243,7 +243,7 @@ Tactic Notation "iExact" constr(H) :=
fail "iExact:" H ":" P "does not match goal"
|pm_reduce; iSolveTC ||
let H := pretty_ident H in
fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
fail "iExact: remaining hypotheses not affine and the goal not absorbing"].
Tactic Notation "iAssumptionCore" :=
let rec find Γ i P :=
......@@ -261,6 +261,17 @@ Tactic Notation "iAssumptionCore" :=
is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
end.
Tactic Notation "iAssumptionCoq" :=
let Hass := fresh in
match goal with
| H : ⊢ ?P |- envs_entails _ ?Q =>
pose proof (_ : FromAssumption true P Q) as Hass;
notypeclasses refine (tac_assumption_coq _ P _ H _ _);
[exact Hass
|pm_reduce; iSolveTC ||
fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
end.
Tactic Notation "iAssumption" :=
let Hass := fresh in
let rec find p Γ Q :=
......@@ -269,9 +280,9 @@ Tactic Notation "iAssumption" :=
[pose proof (_ : FromAssumption p P Q) as Hass;
eapply (tac_assumption _ j p P);
[pm_reflexivity
|apply Hass
|exact Hass
|pm_reduce; iSolveTC ||
fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
|assert (P = False%I) as Hass by reflexivity;
apply (tac_false_destruct _ j p P);
[pm_reflexivity
......@@ -280,7 +291,9 @@ Tactic Notation "iAssumption" :=
end in
lazymatch goal with
| |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
first [find true Γp Q | find false Γs Q
first [find true Γp Q
|find false Γs Q
|iAssumptionCoq
|fail "iAssumption:" Q "not found"]
end.
......@@ -1142,7 +1155,7 @@ Local Ltac iApplyHypExact H :=
|pm_reduce; iSolveTC]
|lazymatch iTypeOf H with
| Some (_,?Q) =>
fail 2 "iApply:" Q "not absorbing and the remaining hypotheses not affine"
fail 2 "iApply: remaining hypotheses not affine and the goal not absorbing"
end].
Local Ltac iApplyHypLoop H :=
first
......
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