From 0f5095243b91499b64e267686e76b939a812277d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 25 Oct 2016 15:49:39 +0200
Subject: [PATCH] Uses of iInduction.
---
perm_incl.v | 12 ++++++------
type_incl.v | 13 ++++++-------
2 files changed, 12 insertions(+), 13 deletions(-)
diff --git a/perm_incl.v b/perm_incl.v
index 528852a1..83e7be59 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -203,12 +203,12 @@ Section props.
destruct v as [[[|l|]|]|];
iIntros "H"; try iDestruct "H" as "[]";
iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
- simpl. iVsIntro. iRevert "H".
- change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 2.
- (* TODO : use iInduction, but we need to do it under generalization of O. *)
- induction (combine_offs tyl 0) as [|[ty offs] ll IH]. by auto.
- iIntros (i) "H". rewrite big_sepL_cons /=. iDestruct "H" as "[H0 H]".
- setoid_rewrite <-Nat.add_succ_comm. iDestruct (IH with "[] H") as "$". done.
+ simpl. iVsIntro.
+ change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat).
+ generalize O at 2; intro i.
+ iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH" forall (i). by auto.
+ rewrite big_sepL_cons /=. iDestruct "H" as "[H0 H]".
+ setoid_rewrite <-Nat.add_succ_comm. iDestruct ("IH" $! (S i) with "H") as "$".
iExists _. iSplit. done. admit.
(* FIXME : namespaces problem. *)
Admitted.
diff --git a/type_incl.v b/type_incl.v
index 322ec330..7566f247 100644
--- a/type_incl.v
+++ b/type_incl.v
@@ -108,12 +108,11 @@ Section ty_incl.
iVs (Himpl with "Hρ") as "#Himpl". iIntros "!==>!#*H".
iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit.
by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H").
- - rewrite /Π /=. iRevert "Hρ". generalize O.
- change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O.
- (* TODO : use iInduction, but we need to do it under generalization of O. *)
- induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
- + iIntros (i offs) "_!==>!#*_/=". rewrite big_sepL_nil. eauto.
- + iIntros (i offs) "#Hρ". iVs (IH with "[] []") as "#Hqimpl". by iClear "Hρ". done.
+ - rewrite /Π /=. iRevert "Hρ". generalize O; intros offs.
+ change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O; intros i.
+ iInduction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA] "IH" forall (i offs).
+ + iIntros "_!==>!#*_/=". rewrite big_sepL_nil. eauto.
+ + iIntros "#Hρ". iVs ("IH" $! _ _ with "[]") as "#Hqimpl"; try done.
iVs (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!==>!#*".
rewrite !big_sepL_cons. iIntros "[Hh Hq]".
setoid_rewrite <-Nat.add_succ_comm.
@@ -137,7 +136,7 @@ Section ty_incl.
admit.
Admitted.
- (* TODO *)
+ (* TODO, depends on [ty_incl_prod_cons_l] *)
Lemma ty_incl_prod_flatten ρ tyl1 tyl2 tyl3 :
ty_incl ρ (Π(tyl1 ++ Π tyl2 :: tyl3))
(Π(tyl1 ++ tyl2 ++ tyl3)).
--
GitLab