feat: iinduction

Iris/Iris/ProofMode/Classes.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Michael Sammler, Alvin Tang
+Authors: Lars König, Michael Sammler, Yunsong Yang, Alvin Tang
 -/
 module
 
@@ -208,18 +208,27 @@ class IntoLaterN {PROP} [BI PROP] (only_head : Bool) (n : Nat) (P : PROP) (Q : o
 export IntoLaterN (into_laterN)
 
 /-- `CombineSepAs` combines two propositions `P` and `Q` into `R` -/
-@[ipm_class]
+@[ipm_class, rocq_alias CombineSepAs]
 class CombineSepAs [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_as : P ∗ Q ⊢ R
 export CombineSepAs (combine_sep_as)
 
 /-- `CombineSepGives` combines two propositions `P` and `Q` for a proposition
     with the `<pers>` modality -/
-@[ipm_class]
+@[ipm_class, rocq_alias CombineSepGives]
 class CombineSepGives [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_gives : P ∗ Q ⊢ <pers> R
 export CombineSepGives (combine_sep_gives)
 
+/-
+  `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
+  hypothesis `Q` under an intuitionistic BI context `□ P`.
+-/
+@[ipm_class, rocq_alias IntoIH]
+class IntoIH [BI PROP] (φ : Prop) (P : PROP) (Q : outParam PROP) where
+  into_ih : φ → □ P ⊢ Q
+export IntoIH (into_ih)
+
 #rocq_ignore elim_inv_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore elim_modal_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore from_and_tc_opaque "No tc_opaque in Lean"

Iris/Iris/ProofMode/Expr.lean

@@ -189,6 +189,12 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} :
   | _, .hyp _ _ ivar p _ _ => if isTrue p then [ivar] else []
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticIVarIds ++ rhs.intuitionisticIVarIds
 
+partial def Hyps.intuitionisticProps {u prop bi} :
+    ∀ {s}, @Hyps u prop bi s → List Q($prop)
+  | _, .emp _ => []
+  | _, .hyp tm _ _ p _ _ => if isTrue p then [tm] else []
+  | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticProps ++ rhs.intuitionisticProps
+
 variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
   | _, .emp _ => none
@@ -484,6 +490,11 @@ structure IrisGoal where
 
 def isIrisGoal (expr : Expr) : Bool := isAppOfArity expr ``Entails' 4
 
+partial def isIrisGoalWithForalls (expr : Expr) : Bool :=
+  match expr.consumeMData with
+  | .forallE _ _ e _ => isIrisGoalWithForalls e
+  | e => isIrisGoal e
+
 def parseIrisGoal? (expr : Expr) : Option IrisGoal := do
   -- remove top-level metadata when matching on the goal
   let expr := expr.consumeMData

Iris/Iris/ProofMode/Instances.lean

@@ -7,6 +7,7 @@ module
 
 public import Iris.BI
 public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ClassesMake
 public import Iris.ProofMode.ModalityInstances
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
@@ -917,3 +918,69 @@ instance combineSepGives_persistently [BI PROP] (Q1 Q2 P : PROP)
     [h : CombineSepGives Q1 Q2 P] :
     CombineSepGives iprop(<pers> Q1) iprop(<pers> Q2) iprop(<pers> P) where
   combine_sep_gives := persistently_sep_2.trans (persistently_mono h.combine_sep_gives)
+
+@[rocq_alias into_ih_entails]
+instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (P ⊢ Q) P Q where
+  into_ih := λ hpq => intuitionistically_elim.trans hpq
+
+@[rocq_alias into_ih_forall]
+instance (priority := default - 2) intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP)
+    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
+    IntoIH (∀ x, φ x) P (BI.forall Φ) where
+  into_ih := by
+    intro hφ
+    apply forall_intro
+    intro x
+    exact (h x).into_ih (hφ x)
+
+@[rocq_alias into_ih_impl]
+instance (priority := default - 1) intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
+    [h1 : MakeAffinely iprop(⌜φ⌝) P]
+    [h2 : IntoIH ψ Δ Q] :
+    IntoIH (φ → ψ) Δ iprop(P -∗ Q) where
+  into_ih := by
+    intro hImp
+    apply wand_intro
+    refine (sep_mono_r h1.make_affinely.mpr).trans ?_
+    refine persistent_and_affinely_sep_r.2.trans ?_
+    exact pure_elim_r (fun hφ => h2.into_ih (hImp hφ))
+
+/-- Support for induction principles whose IH is guarded by `List.Forall`, e.g.
+    `∀ l, Forall P l → P (Tree l)` arising from nested inductive types like
+    `inductive ntree := Tree : List ntree → ntree`. -/
+@[rocq_alias into_ih_Forall]
+instance intoIH_listForall [BI PROP] (φ : α → Bool) (l : List α) (P : PROP) (Φ : α → PROP)
+    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
+    IntoIH (l.all φ) P (bigSepL (fun _ a => iprop(□ Φ a)) l) where
+  into_ih := by
+    intro h1
+    induction l generalizing Φ with
+    | nil =>
+      simp [affine]
+    | cons x xs ih =>
+      simp [List.all, bigSepL] at h1 ⊢
+      rcases h1 with ⟨hx, hxs⟩
+      apply intuitionistically_sep_idem.mpr.trans
+      refine sep_mono ?_ ?_
+      · exact intuitionistically_intro' ((h x).into_ih hx)
+      · apply ih
+        apply (List.all_eq_true.mpr)
+        apply hxs
+
+/-- Support for induction principles whose IH is guarded by `List.Forall₂`, e.g.
+    arising from mutual inductive types relating two lists element-wise. -/
+@[rocq_alias into_ih_Forall2]
+instance intoIH_listForall₂ [BI PROP] (φ : α → β → Prop) (l1 : List α) (l2 : List β)
+    (P : PROP) (Φ : α → β → PROP)
+    [h : ∀ x1 x2, IntoIH (φ x1 x2) P (Φ x1 x2)] :
+    IntoIH (List.Forall₂ φ l1 l2) P (bigSepL2 (fun _ x1 x2 => iprop(□ Φ x1 x2)) l1 l2) where
+  into_ih := by
+    intro h
+    induction h with
+    | nil => simp [bigSepL2, affine]
+    | cons x xs ih =>
+      simp [bigSepL2] at ⊢
+      apply intuitionistically_sep_idem.mpr.trans
+      refine sep_mono ?_ ?_
+      · exact intuitionistically_intro' ((h _ _).into_ih x)
+      · exact ih

Iris/Iris/ProofMode/Tactics.lean

@@ -12,6 +12,7 @@ public meta import Iris.ProofMode.Tactics.ExFalso
 public meta import Iris.ProofMode.Tactics.Exists
 public meta import Iris.ProofMode.Tactics.Frame
 public meta import Iris.ProofMode.Tactics.Have
+public meta import Iris.ProofMode.Tactics.Induction
 public meta import Iris.ProofMode.Tactics.Intro
 public meta import Iris.ProofMode.Tactics.LeftRight
 public meta import Iris.ProofMode.Tactics.Loeb