Skip to content
Snippets Groups Projects
Commit 4d312ec6 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/iInduction_regression_931' into 'master'

Fix `iInduction` regression caused by !931.

Closes #533

See merge request iris/iris!965
parents b9e591f8 d8ad9194
No related branches found
No related tags found
No related merge requests found
......@@ -1769,9 +1769,9 @@ Ltac _iInduction x xs Hs tac IH :=
(* FIXME: We should be able to do this in a more sane way, by concatenating
the spec patterns instead of calling [iRevertIntros] multiple times. *)
_iRevertIntros0 Hs ltac:(fun _ =>
_iRevertIntros xs "∗" ltac:(fun _ =>
_iRevertIntros0 "∗" ltac:(fun _ =>
let Hsx := iHypsContaining x in
_iRevertIntros0 Hsx ltac:(fun _ =>
_iRevertIntros xs Hsx ltac:(fun _ =>
iInductionCore tac as IH
)
)
......
......@@ -903,6 +903,17 @@ Proof.
by iApply "IH".
Qed.
(* From https://gitlab.mpi-sws.org/iris/iris/-/issues/534 *)
Lemma test_iInduction_big_sepL_impl' {A} (Φ Ψ : nat A PROP) (l1 l2 : list A) :
length l1 = length l2
([ list] kx l1, Φ k x) -∗
( k x1 x2, l1 !! k = Some x1 -∗ l2 !! k = Some x2 -∗ Φ k x1 -∗ Ψ k x2) -∗
[ list] kx l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen).
Abort.
Inductive tree := leaf | node (l r: tree).
Check "test_iInduction_multiple_IHs".
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment