Commit 8a3bd004 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'fix-intro-forall' into 'master'

Fix iIntros on forall

Closes #307

See merge request iris/iris!424
parents 37262a82 a14f0fa3
......@@ -77,6 +77,17 @@
--------------------------------------∗
Q
"test_iIntros_forall_pure"
: string
1 subgoal
PROP : sbi
Ψ : nat → PROP
a : nat
============================
--------------------------------------∗
Ψ a → Ψ a
The command has indeed failed with message:
No applicable tactic.
The command has indeed failed with message:
......
......@@ -119,6 +119,15 @@ Proof. iIntros "-#HQ". done. Qed.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ φ P φ ψ P.
Proof. iIntros (??) "H". auto. Qed.
Check "test_iIntros_forall_pure".
Lemma test_iIntros_forall_pure (Ψ: nat PROP) :
x : nat, Ψ x Ψ x.
Proof.
iIntros "%".
(* should be a trivial implication now *)
Show. auto.
Qed.
Lemma test_iIntros_pure_not : @{PROP} ¬False .
Proof. by iIntros (?). Qed.
......@@ -1088,6 +1097,7 @@ Ltac ltac_tactics.string_to_ident_hook ::=
make_string_to_ident_hook ltac:(fun s => lazymatch s with
| "HP2" => ident:(HP2)
| "H" => ident:(H)
| "y" => ident:(y)
| _ => fail 100 s
end).
......@@ -1102,6 +1112,10 @@ Proof.
exact (Himpl HP2).
Qed.
Lemma test_iIntros_forall_pure_named (Ψ: nat PROP) :
( x : nat, Ψ x) x : nat, Ψ x.
Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed.
Check "test_not_fresh".
Lemma test_not_fresh P1 (P2: Prop) (H:P2) :
P1 P2 - P1 P2.
......
......@@ -1525,7 +1525,9 @@ Ltac iIntros_go pats startproof :=
| false => idtac
end
(* Optimizations to avoid generating fresh names *)
| IPure :: ?pats => iIntro (?); iIntros_go pats startproof
| IPure (IGallinaNamed ?s) :: ?pats => let i := string_to_ident s in
iIntro (i); iIntros_go pats startproof
| IPure IGallinaAnon :: ?pats => iIntro (?); iIntros_go pats startproof
| IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IDrop :: ?pats => iIntro _; iIntros_go pats startproof
| IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof
......
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