From 953a1eefbb2a2ed9596f163ce33bbaf7290b66c7 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 6 Aug 2025 10:53:54 +0200 Subject: [PATCH] =?UTF-8?q?feat:=20Implement=20`mrevert=20=E2=88=80`=20(#9?= =?UTF-8?q?755)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements a `mrevert ∀n` tactic that "eta-reduces" the stateful goal and is adjoint to `mintro ∀x1 ... ∀xn`. --- src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean | 2 +- src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean | 4 +- src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean | 60 ++++++++++----- src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean | 74 ++++++++++++++++++- src/Lean/Meta/AppBuilder.lean | 14 ++++ src/Std/Do/SPred/DerivedLaws.lean | 6 +- src/Std/Tactic/Do/Syntax.lean | 14 +++- tests/lean/run/spredProofMode.lean | 7 ++ 8 files changed, 152 insertions(+), 29 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean index e86cab2338..ba81456cf8 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean @@ -26,7 +26,7 @@ def mStart (goal : Expr) : MetaM MStartResult := do return { goal := mgoal } let u ← mkFreshLevelMVar - let σs ← mkFreshExprMVar (σs.mkType u) + let σs ← mkFreshExprMVar (TypeList.mkType u) let P ← mkFreshExprMVar (mkApp (mkConst ``SPred [u]) σs) let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology [u]) goal σs P) let u ← instantiateLevelMVars u diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean index 33a261f244..7f12d595b0 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean @@ -48,7 +48,7 @@ partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] | `(binderIdent| $_) => liftMetaM <| mkFreshUserName `s withLocalDeclD name σ fun s => do addLocalVarInfo ident (← getLCtx) s σ (isBinder := true) - let H := betaRevPreservingHypNames σs' goal.hyps #[s] + let H := pushForallContextIntoHyps σs' (mkApp goal.hyps s) let T := goal.target.betaRev #[s] map do let (a, prf) ← k { u := goal.u, σs:=σs', hyps:=H, target:=T } @@ -58,7 +58,7 @@ partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] def mIntroForallN [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (k : MGoal → m (α × Expr)) : m (α × Expr) := match n with | 0 => k goal - | n+1 => do mIntroForall goal (← liftM (m := MetaM) `(binderIdent| _)) fun g => + | n+1 => do mIntroForall goal (← liftMetaM `(binderIdent| _)) fun g => mIntroForallN g n k macro_rules diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean index ff83c723a5..6457240633 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean @@ -35,12 +35,26 @@ def parseHyp? : Expr → Option Hyp def Hyp.toExpr (hyp : Hyp) : Expr := .mdata ⟨[(nameAnnotation, .ofName hyp.name), (uniqAnnotation, .ofName hyp.uniq)]⟩ hyp.p +def SPred.mkType (u : Level) (σs : Expr) : Expr := + mkApp (mkConst ``SPred [u]) σs + -- set_option pp.all true in -- #check ⌜True⌝ +def SPred.mkPure (u : Level) (σs : Expr) (p : Expr) : Expr := + mkApp3 (mkConst ``SVal.curry [u]) (mkApp (mkConst ``ULift [u, 0]) (.sort .zero)) σs <| + mkLambda `tuple .default (mkApp (mkConst ``SVal.StateTuple [u]) σs) <| + mkApp2 (mkConst ``ULift.up [u, 0]) (.sort .zero) (Expr.liftLooseBVars p 0 1) + +def SPred.isPure? : Expr → Option (Level × Expr × Expr) + | mkApp3 (.const ``SVal.curry [u]) (mkApp (.const ``ULift _) (.sort .zero)) σs <| + .lam _ _ (mkApp2 (.const ``ULift.up _) _ p) _ => some (u, σs, (Expr.lowerLooseBVars p 0 1)) + | _ => none + def emptyHyp (u : Level) (σs : Expr) : Expr := -- ⌜True⌝ standing in for an empty conjunction of hypotheses - mkApp3 (mkConst ``SVal.curry [u]) (mkApp (mkConst ``ULift [u, 0]) (.sort .zero)) σs <| mkLambda `tuple .default (mkApp (mkConst ``SVal.StateTuple [u]) σs) (mkApp2 (mkConst ``ULift.up [u, 0]) (.sort .zero) (mkConst ``True)) -def parseEmptyHyp? : Expr → Option (Level × Expr) - | mkApp3 (.const ``SVal.curry [u]) (mkApp (.const ``ULift _) (.sort .zero)) σs (.lam _ _ (mkApp2 (.const ``ULift.up _) _ (.const ``True _)) _) => some (u, σs) + SPred.mkPure u σs (mkConst ``True) + +def parseEmptyHyp? (e : Expr) : Option (Level × Expr) := match SPred.isPure? e with + | some (u, σs, .const ``True _) => some (u, σs) | _ => none def pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos := @@ -65,12 +79,13 @@ def mkAnd (u : Level) (σs lhs rhs : Expr) : Expr × Expr := let result := mkAnd! u σs lhs rhs (result, mkApp2 (mkConst ``SPred.bientails.refl [u]) σs result) -def σs.mkType (u : Level) : Expr := mkApp (mkConst ``List [.succ u]) (mkSort (.succ u)) -def σs.mkNil (u : Level) : Expr := mkApp (mkConst ``List.nil [.succ u]) (mkSort (.succ u)) +def TypeList.mkType (u : Level) : Expr := mkApp (mkConst ``List [.succ u]) (mkSort (.succ u)) +def TypeList.mkNil (u : Level) : Expr := mkApp (mkConst ``List.nil [.succ u]) (mkSort (.succ u)) +def TypeList.mkCons (u : Level) (hd tl : Expr) : Expr := mkApp3 (mkConst ``List.cons [.succ u]) (mkSort (.succ u)) hd tl def parseAnd? (e : Expr) : Option (Level × Expr × Expr × Expr) := (e.getAppFn.constLevels![0]!, ·) <$> e.app3? ``SPred.and - <|> (0, σs.mkNil 0, ·) <$> e.app2? ``And + <|> (0, TypeList.mkNil 0, ·) <$> e.app2? ``And structure MGoal where u : Level @@ -127,19 +142,30 @@ def getFreshHypName : TSyntax ``binderIdent → CoreM (Name × Syntax) | `(binderIdent| $name:ident) => pure (name.getId, name) | stx => return (← mkFreshUserName `h, stx) -partial def betaRevPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr := - if let some (u, _) := parseEmptyHyp? e then - emptyHyp u σs' - else if let some hyp := parseHyp? e then - { hyp with p := hyp.p.betaRev args }.toExpr - else if let some (u, _σs, lhs, rhs) := parseAnd? e then - -- _σs = σ :: σs' - mkAnd! u σs' (betaRevPreservingHypNames σs' lhs args) (betaRevPreservingHypNames σs' rhs args) - else - e.betaRev args +partial def pushForallContextIntoHyps (σs hyps : Expr) : Expr := go #[] #[] hyps + where + wrap (revLams : Array (Name × Expr × BinderInfo)) (revAppArgs : Array Expr) (body : Expr) : Expr := + revLams.foldr (fun (x, ty, info) e => .lam x ty e info) (body.betaRev revAppArgs) + + go (revLams : Array (Name × Expr × BinderInfo)) (revAppArgs : Array Expr) (e : Expr) : Expr := + if let some (u, _σs) := parseEmptyHyp? e then + emptyHyp u σs + else if let some hyp := parseHyp? e then + { hyp with p := wrap revLams revAppArgs hyp.p }.toExpr + else if let some (u, _σs, lhs, rhs) := parseAnd? e then + mkAnd! u σs (go revLams revAppArgs lhs) (go revLams revAppArgs rhs) + else if let .lam x ty body info := e then + if let some a := revAppArgs.back? then + go revLams revAppArgs.pop (body.instantiate1 a) + else + go (revLams.push (x, ty, info)) revAppArgs body + else if let .app f a := e then + go revLams (revAppArgs.push a) f + else + wrap revLams revAppArgs e def betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr := - betaRevPreservingHypNames σs' e args.reverse + pushForallContextIntoHyps σs' (mkAppN e args) def dropStateList (σs : Expr) (n : Nat) : MetaM Expr := do let mut σs := σs diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean index 987bc7af90..a7b19aab5d 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean @@ -16,7 +16,9 @@ namespace Lean.Elab.Tactic.Do.ProofMode open Std.Do SPred.Tactic open Lean Elab Tactic Meta -partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → MetaM Expr) : MetaM Expr := do +variable {m : Type → Type u} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] + +partial def mRevert (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → m Expr) : m Expr := do let res ← goal.focusHypWithInfo ref let P := goal.hyps let Q := res.restHyps @@ -26,14 +28,78 @@ partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → Met let prf := mkApp7 (mkConst ``Revert.revert [goal.u]) goal.σs P Q H T res.proof prf return prf +/-- +Turn goal + hᵢ : Hᵢ + ⊢ₛ T e₁ ... eₙ +into + hᵢ : fun sₙ ... s₁ => Hᵢ + h : fun sₙ ... s₁ => ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝ + ⊢ₛ T +-/ +partial def mRevertForallN (goal : MGoal) (n : Nat) (hypName : Name) (k : MGoal → m Expr) : m Expr := do + if n = 0 then return ← k goal + let H := goal.hyps + let T := goal.target.consumeMData + let f := T.getAppFn + let args := T.getAppRevArgs + let revertArgs := args[0:n].toArray.reverse + unless revertArgs.size = n do + liftMetaM <| throwError "mrevert: expected {n} excess arguments in {T}, got {revertArgs.size}" + let revertArgsTypes ← liftMetaM <| revertArgs.mapM inferType + + let declInfos ← revertArgsTypes.mapIdxM fun i ty => do + return ((← liftMetaM <| mkFreshUserName `s).appendIndexAfter (i+1), ty) + + -- Build `fun s₁ ... sₙ => H ∧ ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝` + let (H, φ) ← withLocalDeclsDND declInfos fun ss => do + let eqs ← (revertArgs.zip ss).mapM fun (e, s) => mkEq s e + let eqs := eqs.toList + let φ := mkAndN eqs + let φ := SPred.mkPure goal.u goal.σs φ + let uniq ← liftMetaM <| mkFreshUserName hypName + let φ := Hyp.toExpr ⟨hypName, uniq, ← mkLambdaFVars ss φ⟩ + return (← mkLambdaFVars ss H, φ) + + -- Build `⟨rfl, ..., rfl⟩ : e₁ = e₁ ∧ ... ∧ eₙ = eₙ` + let prfs ← liftMetaM <| revertArgs.mapM mkEqRefl + let h ← mkAndIntroN prfs.toList + + -- Push `fun s₁ ... sₙ =>` into the hyps in `H` + let u := goal.u + let σs' := revertArgsTypes.foldr (TypeList.mkCons u) goal.σs + let H ← instantiateMVarsIfMVarApp H + let H := pushForallContextIntoHyps σs' H + let (H, hand) := mkAnd u σs' H φ + + -- Prove `((fun s₁ ... sₙ => H) ∧ (fun s₁ ... sₙ => ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝)) ⊢ₛ T` + let goal' := { u, σs := σs', hyps := H, target := mkAppRev f args[n:] } + let prf ← k goal' + + -- Build the proof for `H ⊢ₛ T e₁ ... eₙ` + let prf := mkApp8 (mkConst ``Revert.and_pure_intro_r [goal.u]) goal.σs (← inferType h) goal.hyps (mkAppN H revertArgs) goal.target h (mkAppN hand revertArgs) (mkAppN prf revertArgs) + -- goal.checkProof prf + return prf + @[builtin_tactic Lean.Parser.Tactic.mrevert] def elabMRevert : Tactic - | `(tactic| mrevert $h) => do + | `(tactic| mrevert $h:ident) => do + let mvar ← getMainGoal + let some goal := parseMGoal? (← mvar.getType) + | throwError "Not in proof mode" + mvar.withContext do + let goals ← IO.mkRef [] + mvar.assign (← mRevert goal h fun newGoal => do + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + goals.modify (m.mvarId! :: ·) + return m) + replaceMainGoal (← goals.get) + | `(tactic| mrevert ∀ $[$n]?) => do let (mvar, goal) ← mStartMVar (← getMainGoal) mvar.withContext do - + let n := ((·.getNat) <$> n).getD 1 let goals ← IO.mkRef [] - mvar.assign (← mRevertStep goal h fun newGoal => do + mvar.assign (← mRevertForallN goal n (← mkFreshUserName `h) fun newGoal => do let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr goals.modify (m.mvarId! :: ·) return m) diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index 09b1116b9c..6b4aa8bfe1 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -716,6 +716,20 @@ def mkIffOfEq (h : Expr) : MetaM Expr := do else mkAppM ``Iff.of_eq #[h] +/-- +Given proofs `hᵢ : pᵢ`, returns a proof for `p₁ ∧ ... ∧ pₙ`. +Roughly, `mkAndIntroN hs : mkAndN (← hs.mapM inferType)`. +-/ +def mkAndIntroN (hs : List Expr) : MetaM Expr := (·.1) <$> go hs + where + go : List Expr → MetaM (Expr × Expr) + | [] => return (mkConst ``True.intro, mkConst ``True) + | [h] => return (h, ← inferType h) + | h :: hs => do + let (h', p') ← go hs + let p ← inferType h + return (mkApp4 (mkConst ``And.intro) p p' h h', mkApp2 (mkConst ``And) p p') + builtin_initialize do registerTraceClass `Meta.appBuilder registerTraceClass `Meta.appBuilder.result (inherited := true) diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean index d423cf56a0..e669128df3 100644 --- a/src/Std/Do/SPred/DerivedLaws.lean +++ b/src/Std/Do/SPred/DerivedLaws.lean @@ -33,6 +33,8 @@ theorem bientails.mpr {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊢ₛ P) := fu /-! # Connectives -/ +theorem and_intro_l (h : P ⊢ₛ Q) : P ⊢ₛ Q ∧ P := and_intro h .rfl +theorem and_intro_r (h : P ⊢ₛ Q) : P ⊢ₛ P ∧ Q := and_intro .rfl h theorem and_elim_l' (h : P ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_l.trans h theorem and_elim_r' (h : Q ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_r.trans h theorem or_intro_l' (h : P ⊢ₛ Q) : P ⊢ₛ Q ∨ R := h.trans or_intro_l @@ -216,6 +218,7 @@ theorem Have.dup {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (hgoal : P theorem Have.have {P H PH T : SPred σs} (hand : P ∧ H ⊣⊢ₛ PH) (hhave : P ⊢ₛ H) (hgoal : PH ⊢ₛ T) : P ⊢ₛ T := (and_intro .rfl hhave).trans (hand.mp.trans hgoal) theorem Have.replace {P H H' PH PH' T : SPred σs} (hfoc : PH ⊣⊢ₛ P ∧ H ) (hand : P ∧ H' ⊣⊢ₛ PH') (hhave : PH ⊢ₛ H') (hgoal : PH' ⊢ₛ T) : PH ⊢ₛ T := (and_intro (hfoc.mp.trans and_elim_l) hhave).trans (hand.mp.trans hgoal) theorem Intro.intro {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T := imp_intro (hand.mp.trans h) +theorem Revert.and_pure_intro_r {φ : Prop} {P P' Q : SPred σs} (h₁ : φ) (hand : P ∧ ⌜φ⌝ ⊣⊢ₛ P') (h₂ : P' ⊢ₛ Q) : P ⊢ₛ Q := (SPred.and_intro_r (SPred.pure_intro h₁)).trans (hand.mp.trans h₂) theorem Pure.thm {P Q T : SPred σs} {φ : Prop} [IsPure Q φ] (h : φ → P ⊢ₛ T) : P ∧ Q ⊢ₛ T := by apply pure_elim · exact and_elim_r.trans IsPure.to_pure.mp @@ -252,7 +255,6 @@ instance (σs) (P : SPred σs) : SimpAnd ⌜True⌝ P P where simp_and := true_a class HasFrame (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop where reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝ -instance (σs) : HasFrame (σs:=σs) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm instance (σs) (P P' Q QP : SPred σs) [HasFrame P Q φ] [SimpAnd Q P' QP]: HasFrame (σs:=σs) spred(P ∧ P') QP φ where reassoc := ((and_congr_l HasFrame.reassoc).trans and_right_comm).trans (and_congr_l SimpAnd.simp_and) instance (σs) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ]: HasFrame (σs:=σs) spred(P ∧ P') PQ φ where reassoc := ((and_congr_r HasFrame.reassoc).trans and_assoc.symm).trans (and_congr_l SimpAnd.simp_and) instance (σs) (P P' : SVal.StateTuple σs → Prop) (Q : SPred σs) [HasFrame spred(SVal.curry (fun t => ⟨P t⟩) ∧ SVal.curry (fun t => ⟨P' t⟩)) Q φ] : HasFrame (σs:=σs) (SVal.curry fun t => ⟨P t ∧ P' t⟩) Q φ where reassoc := and_curry.symm.trans HasFrame.reassoc @@ -281,7 +283,7 @@ instance (σs) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame (σs:=σs) spred(P <| and_congr_r (and_comm.trans pure_and) -- The following instance comes last so that it gets the highest priority. -- It's the most efficient and best solution if valid -instance {φ : Prop} : HasFrame (σs:=[]) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm +instance (σs) : HasFrame (σs:=σs) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm instance {P : SPred []} : HasFrame (σs:=[]) P ⌜True⌝ P.down where reassoc := true_and.symm theorem Frame.frame {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ] diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index dbbea7b40e..c1a9ba58a2 100644 --- a/src/Std/Tactic/Do/Syntax.lean +++ b/src/Std/Tactic/Do/Syntax.lean @@ -75,9 +75,6 @@ syntax (name := mpure) "mpure" colGt ident : tactic macro (name := mpureIntro) "mpure_intro" : tactic => `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro)) -@[inherit_doc Lean.Parser.Tactic.mrevertMacro] -syntax (name := mrevert) "mrevert" colGt ident : tactic - @[inherit_doc Lean.Parser.Tactic.mrenameIMacro] syntax (name := mrenameI) "mrename_i" (ppSpace colGt binderIdent)+ : tactic @@ -224,6 +221,17 @@ macro_rules | `(mintroPat| $pat:mcasesPat) => `(tactic| mintro h; mcases h with $pat) | _ => Macro.throwUnsupported -- presently unreachable +declare_syntax_cat mrevertPat + +syntax ident : mrevertPat +syntax "∀" optional(num) : mrevertPat + +@[inherit_doc Lean.Parser.Tactic.mrevertMacro] +syntax (name := mrevert) "mrevert" (ppSpace colGt mrevertPat)+ : tactic + +macro_rules + | `(tactic| mrevert $pat₁ $pat₂ $pats:mrevertPat*) => `(tactic| mrevert $pat₁; mrevert $pat₂ $pats*) + /-- `mspec_no_simp $spec` first tries to decompose `Bind.bind`s before applying `$spec`. This variant of `mspec_no_simp` does not; `mspec_no_bind $spec` is defined as diff --git a/tests/lean/run/spredProofMode.lean b/tests/lean/run/spredProofMode.lean index 49cbc04ebf..742e198a0c 100644 --- a/tests/lean/run/spredProofMode.lean +++ b/tests/lean/run/spredProofMode.lean @@ -145,6 +145,13 @@ theorem revert (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ R := by mintro HR' mexact HR' +theorem revert_forall (H : SPred σs) (T : SPred (α::β::σs)) + (h : (fun _ _ => H) ∧ (fun s₁ s₂ => ⌜s₁ = e₁ ∧ s₂ = e₂⌝) ⊢ₛ T) : + H ⊢ₛ T e₁ e₂ := by + mintro h + mrevert ∀2 + exact h + namespace constructor theorem and (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by