Commit e98e4ccc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Always revert the whole spatial context for iInduction.

Otherwise, the tactic will fail subsequently. Besides, it was inconsistent
w.r.t. the iLöb tactic, which was already doing this.
parent 4f9deccf
...@@ -1212,7 +1212,7 @@ Tactic Notation "iInductionCore" constr(x) ...@@ -1212,7 +1212,7 @@ Tactic Notation "iInductionCore" constr(x)
lazymatch goal with lazymatch goal with
| H : coq_tactics.of_envs _ _ |- _ => | H : coq_tactics.of_envs _ _ |- _ =>
eapply tac_revert_ih; eapply tac_revert_ih;
[reflexivity || fail "iInduction: spatial context not empty" [reflexivity || fail "iInduction: spatial context not empty, this should not happen"
|apply H|]; |apply H|];
clear H; fix_ihs; clear H; fix_ihs;
let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')] let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
...@@ -1251,41 +1251,50 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) ...@@ -1251,41 +1251,50 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" constr(Hs) := "forall" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros Hs with (iInductionCore x as pat IH). iRevertIntros Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ")" constr(Hs) := "forall" "(" ident(x1) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1) Hs with (iInductionCore x as pat IH). iRevertIntros(x1) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ")" constr(Hs) := "forall" "(" ident(x1) ident(x2) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2) Hs with (iInductionCore x as pat IH). iRevertIntros(x1 x2) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) := "forall" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3) Hs with (iInductionCore x as pat IH). iRevertIntros(x1 x2 x3) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" constr(Hs) := "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4) Hs with (iInductionCore x as pat IH). iRevertIntros(x1 x2 x3 x4) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")" "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")"
constr(Hs) := constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5) Hs with (iInductionCore x as aat IH). iRevertIntros(x1 x2 x3 x4 x5) Hs with (iInductionCore x as aat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ")" "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ")"
constr(Hs) := constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5 x6) Hs with (iInductionCore x as pat IH). iRevertIntros(x1 x2 x3 x4 x5 x6) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
ident(x7) ")" constr(Hs) := ident(x7) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5 x6 x7) Hs with (iInductionCore x as pat IH). iRevertIntros(x1 x2 x3 x4 x5 x6 x7) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
ident(x7) ident(x8) ")" constr(Hs) := ident(x7) ident(x8) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iInductionCore x as pat IH). iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iInductionCore x as pat IH).
(** * Löb Induction *) (** * Löb Induction *)
Tactic Notation "iLöbCore" "as" constr (IH) := Tactic Notation "iLöbCore" "as" constr (IH) :=
iStartProof; iStartProof;
eapply tac_löb with _ IH; eapply tac_löb with _ IH;
[reflexivity || fail "iLöb: persistent context not empty" [reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|env_reflexivity || fail "iLöb:" IH "not fresh"|]. |env_reflexivity || fail "iLöb:" IH "not fresh"|].
Tactic Notation "iLöb" "as" constr (IH) := Tactic Notation "iLöb" "as" constr (IH) :=
......
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