iRevert implementation and Qq

Stream: iris-lean

[Oliver Soeser]

I have submitted PR #74 implementing the irevert tactic. However, I ran into some issues using Qq in this part of my code:

      let f ← getFVarId hyp
      let (some ldecl) := ((← getLCtx).find? f) | throwError "unknown identifier"

      let bibase := mkAppN (mkConst ``BI.toBIBase [u]) #[prop, bi]

      let φ := ldecl.type
      let (_, mvarId) ← mvar.revert #[f]
      mvarId.withContext do
        if ← Meta.isProp φ then
          let p := mkAppN (mkConst ``BI.pure [u]) #[prop, bibase, φ]

          let m ← mkFreshExprSyntheticOpaqueMVar <|
            IrisGoal.toExpr { u, prop, bi, hyps, goal := mkAppN (mkConst ``wand [u]) #[prop, bibase, p, goal], .. }

          let pf := mkAppN (mkConst ``pure_revert [u]) #[prop, bi, e, goal, φ, m]

          mvarId.assign pf
          replaceMainGoal [m.mvarId!]
        else
          let v ← Meta.getLevel φ
          let Φ ← mapForallTelescope' (λ t _ => do
            let (some ig) := parseIrisGoal? t | throwError "not in proof mode"
            return ig.goal
          ) (Expr.mvar mvarId)
          let m ← mkFreshExprSyntheticOpaqueMVar <|
            IrisGoal.toExpr { u, prop, bi, hyps, goal := mkAppN (mkConst ``BI.forall [u, v]) #[prop, bibase, φ, Φ], ..}

          let pf := mkAppN (mkConst ``forall_revert [u, v]) #[prop, φ, bi, e, Φ, m]

          mvarId.assign pf
          replaceMainGoal [m.mvarId!]

Whenever I tried using Qq instead of the cumbersome notation used above, I got cryptic errors like

unquoteExpr: match ldecl with
| LocalDecl.cdecl index fvarId userName t bi kind => t
| LocalDecl.ldecl index fvarId userName t value nonDep kind => t : Expr

so I had to build expressions in the less convenient manner. I realise that this is not ideal since Qq is used across iris-lean for tasks like these. If anyone has an idea how this could be remedied or is able to submit a PR to my fork with a Qq based implementation it would be greatly appreciated.

[Mario Carneiro]

do you have a MWE of a bad Qq version?

[Mario Carneiro]

the problem is most likely using let where you should use have to construct a Qq value using non-Qq functions

[Oliver Soeser]

Thanks! That was indeed the issue

[Oliver Soeser]

What is the difference between have and let with regards to Qq?

[Mario Carneiro]

Qq tries to introspect lets when constructing the embedded proof context, and it gets confused when it finds something defined using unapproved functions

[Mario Carneiro]

this is probably a Qq bug