Commit 9eb50174 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Attempt at an iInduction tactic.

This comment mostly addresses issue #34.

There are still some issues:

- For iLöb we can write `iLöb (x1 .. xn) as "IH"` to revert x1 .. xn
  before performing Löb induction. An analogue notation for iInduction
  results in parsing conflicts.
- The names of the induction hypotheses in the Coq intro pattern are
  ignored. Instead, when using `iInduction x as pat "IH"` the induction
  hypotheses are given fresh names starting with "IH". The problem here
  is that the names in the introduction pattern are idents, whereas the
  induction hypotheses are inserted into the proof mode context, and thus
  need to have strings as names.
parent c208c95d
...@@ -541,6 +541,16 @@ Proof. ...@@ -541,6 +541,16 @@ Proof.
intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l. intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed. Qed.
Lemma tac_revert_ih Δ P Q :
env_spatial_is_nil Δ = true
(of_envs Δ P)
(of_envs Δ P Q)
(of_envs Δ Q).
Proof.
intros ? HP HPQ.
by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R : Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
IntoAssert P Q R IntoAssert P Q R
envs_split lr js Δ = Some (Δ1,Δ2) envs_split lr js Δ = Some (Δ1,Δ2)
......
...@@ -877,12 +877,31 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ...@@ -877,12 +877,31 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) := Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
iDestructCore lem as true (fun H => iPure H as pat). iDestructCore lem as true (fun H => iPure H as pat).
(** * Induction *)
Tactic Notation "iInductionCore" constr(x)
"as" simple_intropattern(pat) constr(IH) :=
let rec fix_ihs :=
lazymatch goal with
| H : coq_tactics.of_envs _ _ |- _ =>
eapply tac_revert_ih;
[env_cbv; reflexivity
|apply H|];
clear H; fix_ihs;
let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
| _ => idtac
end in
induction x as pat; fix_ihs.
Tactic Notation "iInduction" constr(x)
"as" simple_intropattern(pat) constr(IH) :=
iRevertIntros with (iInductionCore x as pat IH).
(** * Löb Induction *)
Tactic Notation "iLöbCore" "as" constr (IH) := Tactic Notation "iLöbCore" "as" constr (IH) :=
eapply tac_löb with _ IH; eapply tac_löb with _ IH;
[reflexivity [reflexivity
|env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|]. |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|].
(** * Löb induction *)
Tactic Notation "iLöb" "as" constr (IH) := Tactic Notation "iLöb" "as" constr (IH) :=
iRevertIntros with (iLöbCore as IH). iRevertIntros with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ")" "as" constr (IH) := Tactic Notation "iLöb" "(" ident(x1) ")" "as" constr (IH) :=
......
Supports Markdown
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