Merge remote-tracking branch 'upstream/master' into Imports

Author: alvinylt

.github/workflows/build.yml

@@ -82,7 +82,9 @@ jobs:
           path: Iris/.lake
       - name: Read pinned Rocq commit
         id: rocq-commit
-        run: echo "sha=$(cat scripts/ROCQ_REVISION)" >> "$GITHUB_OUTPUT"
+        run: |
+          sha=$(cat scripts/ROCQ_REVISION)
+          echo "sha=$sha" >> "$GITHUB_OUTPUT"
       - name: Cache Rocq definitions
         uses: actions/cache@v6
         with:

.github/workflows/check-stale.yml

@@ -21,8 +21,9 @@ jobs:
       - name: Resolve Iris-Rocq master to a commit SHA
         id: rocq-commit
         run: |
-          sha=$(curl -fsSL \
-            "https://gitlab.mpi-sws.org/api/v4/projects/iris%2Firis/repository/commits/master" \
+          set -euo pipefail
+          url=$(python3 scripts/check_porting.py --print commit-api-url)
+          sha=$(curl -fsSL "$url" \
             | python3 -c 'import json,sys; print(json.load(sys.stdin)["id"])')
           echo "sha=$sha" >> "$GITHUB_OUTPUT"
 

Iris/Iris/HeapLang/ProofMode.lean

@@ -658,11 +658,11 @@ elab "wp_store" : tactic =>
     let ⟨_, name, vid, _, hyps'', pfSplit⟩ ←
       lookupPointsTo `wp_store mvar hgs hyps' l q(DFrac.own 1) q(false)
 
-    let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v'))
+    let ⟨_, hyps''', pf'''⟩ := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v'))
 
     let pfCont ← finishHeapOp hyps''' hgs s E K q(hl_val(#())) Φ
 
-    mvar.assign q(tac_wp_store (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+    mvar.assign q(tac_wp_store (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit <| $(pf''').mp.trans $pfCont)
 
 elab "wp_xchg" : tactic =>
   runTacticHeapWp `wp_xchg fun mvar {bi, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
@@ -676,11 +676,11 @@ elab "wp_xchg" : tactic =>
     let ⟨v, name, vid, _, hyps'', pfSplit⟩ ←
       lookupPointsTo `wp_xchg mvar hgs hyps' l q(DFrac.own 1) q(false)
 
-    let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v'))
+    let ⟨_, hyps''', pf'''⟩ := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v'))
 
     let pfCont ← finishHeapOp hyps''' hgs s E K v Φ
 
-    mvar.assign q(tac_wp_xchg (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+    mvar.assign q(tac_wp_xchg (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit <| $(pf''').mp.trans $pfCont)
 
 elab "wp_faa" : tactic =>
   runTacticHeapWp `wp_faa fun mvar {bi, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
@@ -703,12 +703,12 @@ elab "wp_faa" : tactic =>
     have pfSplit : Q($eΔ' ⊣⊢ $eΔ'' ∗
       pointsTo $l (DFrac.own 1) (some (Val.lit (BaseLit.int $z1)))) := pfSplit
 
-    let hyps''' := hyps''.add bi name vid q(false)
+    let ⟨_, hyps''', pf'''⟩ := hyps''.add bi name vid q(false)
       q(pointsTo $l (DFrac.own 1) (some (Val.lit (BaseLit.int ($z1 + $z2)))))
 
     let pfCont ← finishHeapOp hyps''' hgs s E K q(Val.lit (BaseLit.int $z1)) Φ
 
-    mvar.assign q(tac_wp_faa (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+    mvar.assign q(tac_wp_faa (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit <| $(pf''').mp.trans $pfCont)
 
 elab "wp_cmpxchg_suc" : tactic =>
   runTacticHeapWp `wp_cmpxchg_suc fun mvar {bi, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
@@ -729,14 +729,14 @@ elab "wp_cmpxchg_suc" : tactic =>
     -- check equality, don't throw hard error to match Rocq behavior
     let pfEq ← iSolveSidecondition q($v = $v1) (failOnUnsolved := false)
 
-    let hyps''' := hyps''.add bi name vid q(false)
+    let ⟨_, hyps''', pf'''⟩ := hyps''.add bi name vid q(false)
       q(pointsTo $l (DFrac.own 1) (some $v2))
 
     let pfCont ← finishHeapOp hyps''' hgs s E K
       q(Val.pair $v (Val.lit (BaseLit.bool true))) Φ
 
     mvar.assign
-      q(tac_wp_cmpXchg_suc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfEq $pfSafe $pfCont)
+      q(tac_wp_cmpXchg_suc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfEq $pfSafe <| $(pf''').mp.trans $pfCont)
 
 elab "wp_cmpxchg_fail" : tactic =>
   runTacticHeapWp `wp_cmpxchg_fail fun mvar {s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
@@ -779,7 +779,7 @@ elab "wp_cmpxchg" " with" colGt ppSpace h1:binderIdent colGt ppSpace h2:binderId
     let ⟨v, name, vid, eΔ'', hyps'', pfSplit⟩ ←
       lookupPointsTo `wp_cmpxchg mvar hgs hyps' l q(DFrac.own 1) q(false)
 
-    let hypsSuc := hyps''.add bi name vid q(false)
+    let ⟨_, hypsSuc, pfEq⟩ := hyps''.add bi name vid q(false)
       q(pointsTo $l (DFrac.own 1) (some $v2))
 
     -- check safety, don't throw hard error to match Rocq behavior
@@ -793,7 +793,7 @@ elab "wp_cmpxchg" " with" colGt ppSpace h1:binderIdent colGt ppSpace h2:binderId
         Qq.withLocalDeclDQ sucName q($v = $v1) fun _h => do
           let pf ← finishHeapOp hypsSuc hgs s E K
             q(Val.pair $v (Val.lit (BaseLit.bool true))) Φ
-          mkLambdaFVars #[_h] pf
+          mkLambdaFVars #[_h] q($(pfEq).mp.trans $pf)
 
     let (failName, _) ← getFreshName h2
     let pfFail : Q($v ≠ $v1 → $eΔ' ⊢
@@ -843,11 +843,11 @@ elab "wp_alloc" colGt ppSpace loc:binderIdent " with" colGt ppSpace hyp:binderId
         Wp.wp (self := wp.def (ι := @HeapLang $hlc $GF $hgs)) $s $E
           (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) (Val.lit (BaseLit.loc l)))) $Φ) ←
       Qq.withLocalDeclDQ locName q(Loc) fun l => do
-        let ⟨_, hyps''⟩ ← hyps'.addWithInfo bi hyp q(false)
+        let ⟨_, _, hyps'', pfEq⟩ ← hyps'.addWithInfo bi hyp q(false)
           q(pointsTo $l (DFrac.own 1) (some $v))
 
         let pf ← finishHeapOp hyps'' hgs s E K q(Val.lit (BaseLit.loc $l)) Φ
-        mkLambdaFVars #[l] pf
+        mkLambdaFVars #[l] q($(pfEq).mp.trans $pf)
 
     mvar.assign q(tac_wp_alloc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfCont)
 

Iris/Iris/HeapLang/Syntax.lean

@@ -7,16 +7,21 @@ module
 
 public import Iris.Std.Infinite
 public import Iris.ProgramLogic.Language
+meta import Iris.Std.RocqPorting
 
 @[expose] public section
 namespace Iris.HeapLang
 
-@[ext]
+@[ext, rocq_alias heap_lang.loc]
 structure Loc where
   mk ::
   n : Int
 deriving Inhabited, Repr, DecidableEq
 
+attribute [rocq_alias heap_lang.Loc.inhabited] instInhabitedLoc
+attribute [rocq_alias heap_lang.Loc.eq_dec] instDecidableEqLoc
+
+@[rocq_alias heap_lang.Loc.infinite]
 instance : InfiniteType Loc where
   enum n := .mk n
   enum_inj n m := by grind
@@ -47,7 +52,7 @@ instance : Zero Loc where
 theorem loc_add_n (l : Loc) n :
   (l + n).n = l.n + n := by simp [HAdd.hAdd]
 
-@[ext]
+@[ext, rocq_alias heap_lang.heap_lang.proph_id]
 structure ProphId where
   mk ::
   n : Nat
@@ -78,6 +83,7 @@ inductive Binder where
   | named (name : String)
 deriving Inhabited, Repr, DecidableEq
 
+@[rocq_alias heap_lang.heap_lang.base_lit]
 inductive BaseLit where
   | int (n : Int)
   | bool (b : Bool)
@@ -87,11 +93,13 @@ inductive BaseLit where
   | prophecy (p : ProphId)
 deriving Inhabited, Repr, DecidableEq
 
+@[rocq_alias heap_lang.heap_lang.un_op]
 inductive UnOp where
   | neg
   | minus
 deriving Inhabited, Repr, DecidableEq
 
+@[rocq_alias heap_lang.heap_lang.bin_op]
 inductive BinOp where
   /- We use "tdiv" and "tmod" instead of "div" and "mod" to
       better match the behavior of 'real' languages:
@@ -104,6 +112,7 @@ inductive BinOp where
 deriving Inhabited, Repr, DecidableEq
 
 mutual
+  @[rocq_alias heap_lang.heap_lang.expr]
   inductive Exp : Type where
     /- values -/
     -- This constructor should not be used directly. Use Exp.ofVal instead.
@@ -138,6 +147,7 @@ mutual
     | newProph
     | resolve (e₀ e₁ e₂ : Exp)
   deriving Inhabited, Repr, DecidableEq
+  @[rocq_alias heap_lang.heap_lang.val]
   inductive Val : Type where
     | lit (l : BaseLit)
     | rec_ (f x : Binder) (e : Exp)

Iris/Iris/ProofMode/Expr.lean

@@ -156,12 +156,13 @@ def Hyps.mkHyp {prop : Q(Type u)} (bi : Q(BI $prop))
     (name : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) (e := q(iprop(□?$p $ty))) : Hyps bi e :=
   .hyp (mkIntuitionisticIf bi p (mkNameAnnotation name ivar ty)) name ivar p ty ⟨⟩
 
--- TODO: should this ensure that adding a hypothesis to emp creates a
--- hyp node instead of a sep node?
 def Hyps.add {prop : Q(Type u)} (bi : Q(BI $prop))
     (name : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
-    : Hyps bi q(iprop($e ∗ □?$p $ty)) :=
-  Hyps.mkSep h (.mkHyp bi name ivar p ty)
+    : (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e')) :=
+  match h with
+  -- Adding a hypothesis to `emp` creates a `.hyp` node instead of a `.sep` node
+  | .emp _ => ⟨_, .mkHyp bi name ivar p ty, q(emp_sep)⟩
+  | _ => ⟨_, .mkSep h (.mkHyp bi name ivar p ty), q(.rfl)⟩
 
 partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) :
     Option ((s : Q($prop)) × Hyps bi s) := do
@@ -552,6 +553,14 @@ def parseIrisGoal? (expr : Expr) : Option IrisGoal := do
   let ⟨e, hyps⟩ ← parseHyps? bi P
   some { u, prop, bi, e, hyps, goal }
 
+/--
+  Parse an Iris entailment (`Entails` rather than `Entails'`).
+-/
+def parseEntails? (expr : Expr) : Option <| Expr × Expr × Expr × Expr :=
+  match expr.consumeMData.appM? ``Entails with
+  | some #[prop, bi, e, goal] => some ⟨prop, bi, e, goal⟩
+  | _ => none
+
 def IrisGoal.toExpr : IrisGoal → Expr
   | { hyps, goal, .. } => q(Entails' $(hyps.tm) $goal)
 
@@ -592,12 +601,12 @@ def Hyps.findWithInfo {u prop bi} (hyps : @Hyps u prop bi s) (name : Ident) : Me
 /-- Hyps.addWithInfo should be used by tactics that introduce a hypothesis based on the name given by the user. -/
 def Hyps.addWithInfo {prop : Q(Type u)} (bi : Q(BI $prop))
     (name : TSyntax ``binderIdent) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
-    : MetaM (IVarId × Hyps bi q(iprop($e ∗ □?$p $ty))) := do
+    : MetaM (IVarId × (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e'))) := do
   let ivar' ← mkFreshIVarId (isTrue p)
   let (nameTo, nameRef) ← getFreshName name
   addHypInfo nameRef nameTo ivar' prop ty (isBinder := true)
-  let hyps := Hyps.add bi nameTo ivar' p ty h
-  return ⟨ivar', hyps⟩
+  let ⟨e', hyps, pf⟩ := Hyps.add bi nameTo ivar' p ty h
+  return ⟨ivar', e', hyps, pf⟩
 
 /--
   Given hypothesis `hyps` representing `e` where every hypothesis exist in the

Iris/Iris/ProofMode/Patterns/CasesPattern.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
+Authors: Lars König, Alvin Tang
 -/
 module
 
@@ -15,50 +15,77 @@ open Lean
 declare_syntax_cat icasesPat
 syntax icasesPatAlts := sepBy1(icasesPat, " | ")
 syntax binderIdent : icasesPat
+/-- Drop the hypothesis. -/
 syntax "-" : icasesPat
+/-- Frame the hypothesis and cancel it against the goal. -/
 syntax "$" : icasesPat
+/--
+  Destruct a (separating) conjunction or existential; an existential variable is
+  bound with `%x` where `x` is the name for it.
+-/
 syntax "⟨" icasesPatAlts,* "⟩" : icasesPat
+/-- Destruct a disjunction, one goal per disjunct. -/
 syntax "(" icasesPatAlts ")" : icasesPat
-syntax "%" binderIdent : icasesPat
+/-- Move the hypothesis to the pure Lean context and give it a name. -/
+syntax "%" rcasesPat : icasesPat
+/-- Move the hypothesis to the intuitionistic context and destruct the proposition. -/
 syntax "#" icasesPat : icasesPat
+/-- Move the hypothesis to the spatial context and destruct the proposition. -/
 syntax "∗" icasesPat : icasesPat
+/-- Eliminate the modality at the top of the hypothesis and destruct the remaining proposition. -/
 syntax ">" icasesPat : icasesPat
 
--- TODO: attach syntax to iCasesPat such that one can use withRef to
--- associate the errors with the right part of the syntax
-inductive iCasesPat
+mutual
+
+inductive iCasesPatCase
   | one (name : TSyntax ``binderIdent)
   | clear
   | frame
   | conjunction (args : List iCasesPat)
   | disjunction (args : List iCasesPat)
-  | pure           (pat : TSyntax ``binderIdent)
+  | pure (pat : TSyntax `rcasesPat)
   | intuitionistic (pat : iCasesPat)
-  | spatial        (pat : iCasesPat)
-  | mod            (pat : iCasesPat)
+  | spatial (pat : iCasesPat)
+  | mod (pat : iCasesPat)
   deriving Repr, Inhabited
 
+structure iCasesPat where
+  ref : Syntax
+  case : iCasesPatCase
+
+end
+
 partial def iCasesPat.parse (pat : TSyntax `icasesPat) : MacroM iCasesPat := do
-  match go ⟨← expandMacros pat⟩ with
+  let stx ← expandMacros pat
+  match go ⟨stx⟩ with
   | none => Macro.throwUnsupported
   | some pat => return pat
 where
-  go : TSyntax `icasesPat → Option iCasesPat
-  | `(icasesPat| $name:binderIdent) => some <| .one name
-  | `(icasesPat| -) => some <| .clear
-  | `(icasesPat| $) => some <| .frame
-  | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList)
-  | `(icasesPat| %$pat:binderIdent) => some <| .pure pat
-  | `(icasesPat| #$pat) => go pat |>.map .intuitionistic
-  | `(icasesPat| ∗$pat) => go pat |>.map .spatial
-  | `(icasesPat| >$pat) => go pat |>.map .mod
-  | `(icasesPat| ($pat)) => goAlts pat
-  | _ => none
-  goAlts : TSyntax ``icasesPatAlts → Option iCasesPat
-  | `(icasesPatAlts| $args|*) =>
-    match args.getElems with
-    | #[arg] => go arg
-    | args   => args.mapM go |>.map (.disjunction ·.toList)
-  | _ => none
+  go (stx : TSyntax `icasesPat) : Option iCasesPat :=
+    match stx.raw with
+    -- delegate: keep the inner pattern's own ref
+    | `(icasesPat| ($pat)) => goAlts pat
+    | _ => (goCase stx).map ({ ref := stx.raw, case := · })
+
+  goCase (stx : TSyntax `icasesPat) : Option iCasesPatCase :=
+    match stx.raw with
+    | `(icasesPat| $name:binderIdent) => some <| .one name
+    | `(icasesPat| -) => some <| .clear
+    | `(icasesPat| $) => some <| .frame
+    | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList)
+    | `(icasesPat| %$pat:rcasesPat) => some <| .pure pat
+    | `(icasesPat| #$pat) => go pat |>.map <| .intuitionistic
+    | `(icasesPat| ∗$pat) => go pat |>.map <| .spatial
+    | `(icasesPat| >$pat) => go pat |>.map <| .mod
+    | _ => none
+
+  goAlts (stx : TSyntax ``icasesPatAlts) : Option iCasesPat :=
+    match stx with
+    | `(icasesPatAlts| $args|*) =>
+      match args.getElems with
+      | #[arg] => go arg
+      | args   => args.mapM go |>.map
+          fun ps => { ref := stx.raw, case := .disjunction ps.toList }
+    | _ => none
 
 end Iris.ProofMode