Commit becd6e2e authored by Robbert Krebbers's avatar Robbert Krebbers

Support `iInduction ... using`; this closes issue #204.

parent af5493d0
......@@ -267,6 +267,15 @@ Proof.
rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega.
Qed.
Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat nat PROP) y :
([ map] x i m, Φ y x) - ([ map] x i m, emp Φ y x).
Proof.
iIntros "Hm". iInduction m as [|i x m] "IH" using map_ind forall(y).
- by rewrite !big_sepM_empty.
- rewrite !big_sepM_insert //. iDestruct "Hm" as "[$ ?]".
by iApply "IH".
Qed.
Lemma test_iIntros_start_proof :
(True : PROP)%I.
Proof.
......
......@@ -1630,7 +1630,7 @@ result in the following actions:
- Introduce the spatial hypotheses and persistent hypotheses involving [x]
- Introduce the proofmode hypotheses [Hs]
*)
Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(IH) :=
Tactic Notation "iInductionCore" tactic(tac) "as" constr(IH) :=
let rec fix_ihs rev_tac :=
lazymatch goal with
| H : context [envs_entails _ _] |- _ =>
......@@ -1646,7 +1646,7 @@ Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(
rev_tac j)
| _ => rev_tac 0%N
end in
induction x as pat; fix_ihs ltac:(fun _ => idtac).
tac; fix_ihs ltac:(fun _ => idtac).
Ltac iHypsContaining x :=
let rec go Γ x Hs :=
......@@ -1672,65 +1672,161 @@ Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) :=
iInductionRevert x "" with (iInductionCore x as pat IH).
iInductionRevert x "" with (iInductionCore (induction x as pat) as IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ")" :=
iInductionRevert x "" with (iRevertIntros(x1) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with (
iRevertIntros(x1) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ")" :=
iInductionRevert x "" with (iRevertIntros(x1 x2) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with
(iRevertIntros(x1 x2) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ")" :=
iInductionRevert x "" with (iRevertIntros(x1 x2 x3) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" :=
iInductionRevert x "" with (iRevertIntros(x1 x2 x3 x4) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")" :=
iInductionRevert x "" with (iRevertIntros(x1 x2 x3 x4 x5) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5) "" with (iInductionCore (induction x as pat) as 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) ")" :=
iInductionRevert x "" with (iRevertIntros(x1 x2 x3 x4 x5 x6) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5 x6) "" with (iInductionCore (induction x as pat) as 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)
ident(x7) ")" :=
iInductionRevert x "" with (iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "" with (iInductionCore (induction x as pat) as 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)
ident(x7) ident(x8) ")" :=
iInductionRevert x "" with (iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "" with (iInductionCore x as pat IH)).
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" constr(Hs) :=
iInductionRevert x Hs with (iInductionCore x as pat IH).
iInductionRevert x Hs with (iInductionCore (induction x as pat) as IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ")" constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ")" constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1 x2) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1 x2) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1 x2 x3) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1 x2 x3 x4) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")"
constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1 x2 x3 x4 x5) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5) "" with (iInductionCore (induction x as pat) as 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) ")"
constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1 x2 x3 x4 x5 x6) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5 x6) "" with (iInductionCore (induction x as pat) as 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)
ident(x7) ")" constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "" with (iInductionCore (induction x as pat) as 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)
ident(x7) ident(x8) ")" constr(Hs) :=
iInductionRevert x Hs with (iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "" with (iInductionCore x as pat IH)).
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "" with (iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) :=
iInductionRevert x "" with (iInductionCore (induction x as pat using u) as IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ")" :=
iInductionRevert x "" with (
iRevertIntros(x1) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ")" :=
iInductionRevert x "" with
(iRevertIntros(x1 x2) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ")" :=
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" :=
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ")" :=
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ")" :=
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5 x6) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ")" :=
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ")" :=
iInductionRevert x "" with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" constr(Hs) :=
iInductionRevert x Hs with (iInductionCore (induction x as pat using u) as IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1 x2) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5 x6) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "" with (iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "" with (iInductionCore (induction x as pat using u) as IH)).
(** * Löb Induction *)
Tactic Notation "iLöbCore" "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