diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index ab3eac9bb2..e483587e68 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1790,6 +1790,307 @@ macro (name := bvNormalizeMacro) (priority:=low) "bv_normalize" optConfig : tact Macro.throwError "to use `bv_normalize`, please include `import Std.Tactic.BVDecide`" +/-- +`massumption` is like `assumption`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P Q : SPred σs) : Q ⊢ₛ P → Q := by + mintro _ _ + massumption +``` +-/ +macro (name := massumptionMacro) (priority:=low) "massumption" : tactic => + Macro.throwError "to use `massumption`, please include `import Std.Tactic.Do`" + + +/-- +`mclear` is like `clear`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P Q : SPred σs) : P ⊢ₛ Q → Q := by + mintro HP + mintro HQ + mclear HP + mexact HQ +``` +-/ +macro (name := mclearMacro) (priority:=low) "mclear" : tactic => + Macro.throwError "to use `mclear`, please include `import Std.Tactic.Do`" + + +/-- +`mconstructor` is like `constructor`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by + mintro HQ + mconstructor <;> mexact HQ +``` +-/ +macro (name := mconstructorMacro) (priority:=low) "mconstructor" : tactic => + Macro.throwError "to use `mconstructor`, please include `import Std.Tactic.Do`" + + +/-- +`mexact` is like `exact`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (Q : SPred σs) : Q ⊢ₛ Q := by + mstart + mintro HQ + mexact HQ +``` +-/ +macro (name := mexactMacro) (priority:=low) "mexact" : tactic => + Macro.throwError "to use `mexact`, please include `import Std.Tactic.Do`" + + +/-- +`mexfalso` is like `exfalso`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by + mintro HP + mexfalso + mexact HP +``` +-/ +macro (name := mexfalsoMacro) (priority:=low) "mexfalso" : tactic => + Macro.throwError "to use `mexfalso`, please include `import Std.Tactic.Do`" + + +/-- +`mexists` is like `exists`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by + mintro H + mexists 42 +``` +-/ +macro (name := mexistsMacro) (priority:=low) "mexists" : tactic => + Macro.throwError "to use `mexists`, please include `import Std.Tactic.Do`" + + +/-- +`mframe` infers which hypotheses from the stateful context can be moved into the pure context. +This is useful because pure hypotheses "survive" the next application of modus ponens +(`Std.Do.SPred.mp`) and transitivity (`Std.Do.SPred.entails.trans`). + +It is used as part of the `mspec` tactic. + +```lean +example (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by + mintro _ + mframe + /- `h : p ∧ q ∧ r ∧ s ∧ t` in the pure context -/ + mcases h with hP + mexact h +``` +-/ +macro (name := mframeMacro) (priority:=low) "mframe" : tactic => + Macro.throwError "to use `mframe`, please include `import Std.Tactic.Do`" + + +/-- +`mhave` is like `have`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by + mintro HP HPQ + mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ + mexact HQ +``` +-/ +macro (name := mhaveMacro) (priority:=low) "mhave" : tactic => + Macro.throwError "to use `mhave`, please include `import Std.Tactic.Do`" + + +/-- +`mreplace` is like `replace`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by + mintro HP HPQ + mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ + mexact HPQ +``` +-/ +macro (name := mreplaceMacro) (priority:=low) "mreplace" : tactic => + Macro.throwError "to use `mreplace`, please include `import Std.Tactic.Do`" + + +/-- +`mleft` is like `left`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by + mintro HP + mleft + mexact HP +``` +-/ +macro (name := mleftMacro) (priority:=low) "mleft" : tactic => + Macro.throwError "to use `mleft`, please include `import Std.Tactic.Do`" + + +/-- +`mright` is like `right`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P Q : SPred σs) : P ⊢ₛ Q ∨ P := by + mintro HP + mright + mexact HP +``` +-/ +macro (name := mrightMacro) (priority:=low) "mright" : tactic => + Macro.throwError "to use `mright`, please include `import Std.Tactic.Do`" + + +/-- +`mpure` moves a pure hypothesis from the stateful context into the pure context. +```lean +example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by + mintro Hφ + mpure Hφ + mexact (ψ Hφ) +``` +-/ +macro (name := mpureMacro) (priority:=low) "mpure" : tactic => + Macro.throwError "to use `mpure`, please include `import Std.Tactic.Do`" + + +/-- +`mpure_intro` operates on a stateful `Std.Do.SPred` goal of the form `P ⊢ₛ ⌜φ⌝`. +It leaves the stateful proof mode (thereby discarding `P`), leaving the regular goal `φ`. +```lean +theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by + mpure_intro + exact True.intro +``` +-/ +macro (name := mpureIntroMacro) (priority:=low) "mpure_intro" : tactic => + Macro.throwError "to use `mpure_intro`, please include `import Std.Tactic.Do`" + + +/-- +`mrevert` is like `revert`, but operating on a stateful `Std.Do.SPred` goal. +```lean +example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by + mintro ⟨HP, HQ, HR⟩ + mrevert HR + mrevert HP + mintro HP' + mintro HR' + mexact HR' +``` +-/ +macro (name := mrevertMacro) (priority:=low) "mrevert" : tactic => + Macro.throwError "to use `mrevert`, please include `import Std.Tactic.Do`" + + +/-- +`mspecialize` is like `specialize`, but operating on a stateful `Std.Do.SPred` goal. +It specializes a hypothesis from the stateful context with hypotheses from either the pure +or stateful context or pure terms. +```lean +example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by + mintro HP HPQ + mspecialize HPQ HP + mexact HPQ + +example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by + mintro HQ HΨ + mspecialize HΨ (y + 1) hP HQ + mexact HΨ +``` +-/ +macro (name := mspecializeMacro) (priority:=low) "mspecialize" : tactic => + Macro.throwError "to use `mspecialize`, please include `import Std.Tactic.Do`" + + +/-- +`mspecialize_pure` is like `mspecialize`, but it specializes a hypothesis from the +*pure* context with hypotheses from either the pure or stateful context or pure terms. +```lean +example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by + mintro HQ + mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ + mexact HΨ +``` +-/ +macro (name := mspecializePureMacro) (priority:=low) "mspecialize_pure" : tactic => + Macro.throwError "to use `mspecialize_pure`, please include `import Std.Tactic.Do`" + + +/-- +Start the stateful proof mode of `Std.Do.SPred`. +This will transform a stateful goal of the form `H ⊢ₛ T` into `⊢ₛ H → T` +upon which `mintro` can be used to re-introduce `H` and give it a name. +It is often more convenient to use `mintro` directly, which will +try `mstart` automatically if necessary. +-/ +macro (name := mstartMacro) (priority:=low) "mstart" : tactic => + Macro.throwError "to use `mstart`, please include `import Std.Tactic.Do`" + + +/-- +Stops the stateful proof mode of `Std.Do.SPred`. +This will simply forget all the names given to stateful hypotheses and pretty-print +a bit differently. +-/ +macro (name := mstopMacro) (priority:=low) "mstop" : tactic => + Macro.throwError "to use `mstop`, please include `import Std.Tactic.Do`" + + +/-- +Like `rcases`, but operating on stateful `Std.Do.SPred` goals. +Example: Given a goal `h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R`, +`mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩` will yield two goals: +`(hq : Q, hqr : Q → R) ⊢ₛ R` and `(hr : R) ⊢ₛ R`. + +That is, `mcases h with pat` has the following semantics, based on `pat`: +* `pat=□h'` renames `h` to `h'` in the stateful context, regardless of whether `h` is pure +* `pat=⌜h'⌝` introduces `h' : φ` to the pure local context if `h : ⌜φ⌝` + (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`) +* `pat=h'` is like `pat=⌜h'⌝` if `h` is pure + (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`), otherwise it is like `pat=□h'`. +* `pat=_` renames `h` to an inaccessible name +* `pat=-` discards `h` +* `⟨pat₁, pat₂⟩` matches on conjunctions and existential quantifiers and recurses via + `pat₁` and `pat₂`. +* `⟨pat₁ | pat₂⟩` matches on disjunctions, matching the left alternative via `pat₁` and the right + alternative via `pat₂`. +-/ +macro (name := mcasesMacro) (priority:=low) "mcases" : tactic => + Macro.throwError "to use `mcases`, please include `import Std.Tactic.Do`" + + +/-- +Like `refine`, but operating on stateful `Std.Do.SPred` goals. +```lean +example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by + mintro ⟨HP, HQ, HR⟩ + mrefine ⟨HP, HR⟩ + +example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by + mintro H + mrefine ⟨⌜42⌝, H⟩ +``` +-/ +macro (name := mrefineMacro) (priority:=low) "mrefine" : tactic => + Macro.throwError "to use `mrefine`, please include `import Std.Tactic.Do`" + + +/-- +Like `intro`, but introducing stateful hypotheses into the stateful context of the `Std.Do.SPred` +proof mode. +That is, given a stateful goal `(hᵢ : Hᵢ)* ⊢ₛ P → T`, `mintro h` transforms +into `(hᵢ : Hᵢ)*, (h : P) ⊢ₛ T`. + +Furthermore, `mintro ∀s` is like `intro s`, but preserves the stateful goal. +That is, `mintro ∀s` brings the topmost state variable `s:σ` in scope and transforms +`(hᵢ : Hᵢ)* ⊢ₛ T` (where the entailment is in `Std.Do.SPred (σ::σs)`) into +`(hᵢ : Hᵢ s)* ⊢ₛ T s` (where the entailment is in `Std.Do.SPred σs`). + +Beyond that, `mintro` supports the full syntax of `mcases` patterns +(`mintro pat = (mintro h; mcases h with pat`), and can perform multiple +introductions in sequence. +-/ +macro (name := mintroMacro) (priority:=low) "mintro" : tactic => + Macro.throwError "to use `mintro`, please include `import Std.Tactic.Do`" + end Tactic namespace Attr diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 02d3fda064..e5ed953ecb 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -52,3 +52,4 @@ import Lean.Elab.Tactic.ExposeNames import Lean.Elab.Tactic.SimpArith import Lean.Elab.Tactic.Show import Lean.Elab.Tactic.Lets +import Lean.Elab.Tactic.Do diff --git a/src/Lean/Elab/Tactic/Do.lean b/src/Lean/Elab/Tactic/Do.lean new file mode 100644 index 0000000000..620d690d8e --- /dev/null +++ b/src/Lean/Elab/Tactic/Do.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Lean.Elab.Tactic.Do.ProofMode diff --git a/src/Lean/Elab/Tactic/Do/ProofMode.lean b/src/Lean/Elab/Tactic/Do/ProofMode.lean new file mode 100644 index 0000000000..bb231ebbe8 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Lean.Elab.Tactic.Do.ProofMode.MGoal +import Lean.Elab.Tactic.Do.ProofMode.Display +import Lean.Elab.Tactic.Do.ProofMode.Basic +import Lean.Elab.Tactic.Do.ProofMode.Clear +import Lean.Elab.Tactic.Do.ProofMode.Intro +import Lean.Elab.Tactic.Do.ProofMode.Revert +import Lean.Elab.Tactic.Do.ProofMode.Exact +import Lean.Elab.Tactic.Do.ProofMode.Assumption +import Lean.Elab.Tactic.Do.ProofMode.Pure +import Lean.Elab.Tactic.Do.ProofMode.Frame +import Lean.Elab.Tactic.Do.ProofMode.LeftRight +import Lean.Elab.Tactic.Do.ProofMode.Constructor +import Lean.Elab.Tactic.Do.ProofMode.Specialize +import Lean.Elab.Tactic.Do.ProofMode.Cases +import Lean.Elab.Tactic.Do.ProofMode.Exfalso +import Lean.Elab.Tactic.Do.ProofMode.Have +import Lean.Elab.Tactic.Do.ProofMode.Refine diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean new file mode 100644 index 0000000000..fcf19253af --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.Basic +import Lean.Elab.Tactic.Do.ProofMode.Exact +import Lean.Elab.Tactic.Do.ProofMode.Focus + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +theorem Assumption.assumption_l {σs : List Type} {P Q R : SPred σs} (h : P ⊢ₛ R) : P ∧ Q ⊢ₛ R := + SPred.and_elim_l.trans h +theorem Assumption.assumption_r {σs : List Type} {P Q R : SPred σs} (h : Q ⊢ₛ R) : P ∧ Q ⊢ₛ R := + SPred.and_elim_r.trans h + +partial def MGoal.assumption (goal : MGoal) : OptionT MetaM Expr := do + if let some _ := parseEmptyHyp? goal.hyps then + failure + if let some hyp := parseHyp? goal.hyps then + guard (← isDefEq hyp.p goal.target) + return mkApp2 (mkConst ``SPred.entails.refl) goal.σs hyp.p + if let some (σs, lhs, rhs) := parseAnd? goal.hyps then + -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Display). + mkApp5 (mkConst ``Assumption.assumption_r) σs lhs rhs goal.target <$> assumption { goal with hyps := rhs } + <|> + mkApp5 (mkConst ``Assumption.assumption_l) σs lhs rhs goal.target <$> assumption { goal with hyps := lhs } + else + panic! s!"assumption: hypothesis without proper metadata: {goal.hyps}" + +def MGoal.assumptionPure (goal : MGoal) : OptionT MetaM Expr := do + let φ := mkApp2 (mkConst ``SPred.tautological) goal.σs goal.target + let fvarId ← OptionT.mk (findLocalDeclWithType? φ) + let inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ goal.σs goal.target) + return mkApp6 (mkConst ``Exact.from_tautology) φ goal.σs goal.hyps goal.target inst (.fvar fvarId) + +@[builtin_tactic Lean.Parser.Tactic.massumption] +def elabMAssumption : Tactic | _ => do + let mvar ← getMainGoal + mvar.withContext do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + + let some proof ← liftMetaM <| + goal.assumption <|> goal.assumptionPure + | throwError "hypothesis not found" + mvar.assign proof + replaceMainGoal [] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean new file mode 100644 index 0000000000..558c1f1e09 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean @@ -0,0 +1,60 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Lean.Meta +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab.Tactic Meta + +structure MStartResult where + goal : MGoal + proof? : Option Expr := none + +def mStart (goal : Expr) : MetaM MStartResult := do + -- check if already in proof mode + if let some mgoal := parseMGoal? goal then + return { goal := mgoal } + + let listType := mkApp (mkConst ``List [.succ .zero]) (mkSort (.succ .zero)) + let σs ← mkFreshExprMVar listType + let P ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) + let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology) goal σs P) + let prf := mkApp4 (mkConst ``ProofMode.start_entails) σs P goal inst + let goal : MGoal := { σs, hyps := emptyHyp σs, target := ← instantiateMVars P } + return { goal, proof? := some prf } + +def mStartMVar (mvar : MVarId) : MetaM (MVarId × MGoal) := mvar.withContext do + let goal ← instantiateMVars <| ← mvar.getType + unless ← isProp goal do + throwError "type mismatch\n{← mkHasTypeButIsExpectedMsg (← inferType goal) (mkSort .zero)}" + + let result ← mStart goal + if let some proof := result.proof? then + let subgoal ← + mkFreshExprSyntheticOpaqueMVar result.goal.toExpr (← mvar.getTag) + mvar.assign (mkApp proof subgoal) + return (subgoal.mvarId!, result.goal) + else + return (mvar, result.goal) + +@[builtin_tactic Lean.Parser.Tactic.mstart] +def elabMStart : Tactic | _ => do + let (mvar, _) ← mStartMVar (← getMainGoal) + replaceMainGoal [mvar] + +@[builtin_tactic Lean.Parser.Tactic.mstop] +def elabMStop : Tactic | _ => do + -- parse goal + let mvar ← getMainGoal + mvar.withContext do + let goal ← instantiateMVars <| ← mvar.getType + + -- check if already in proof mode + let some mgoal := parseMGoal? goal | throwError "not in proof mode" + mvar.setType mgoal.strip diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean new file mode 100644 index 0000000000..63286522ef --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean @@ -0,0 +1,233 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.Focus +import Lean.Elab.Tactic.Do.ProofMode.Basic +import Lean.Elab.Tactic.Do.ProofMode.Pure +import Lean.Elab.Tactic.Do.ProofMode.Intro + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do Lean.Parser.Tactic +open Lean Elab Tactic Meta + +initialize registerTraceClass `Meta.Tactic.Do.cases + +theorem SCases.add_goal {σs} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (hgoal : P ⊢ₛ T) : Q ∧ H ⊢ₛ T := + hand.mp.trans hgoal + +theorem SCases.clear {σs} {Q H T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ∧ H ⊢ₛ T := + (SPred.and_mono_r SPred.true_intro).trans hgoal + +theorem SCases.pure {σs} {Q T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ⊢ₛ T := + (SPred.and_intro .rfl SPred.true_intro).trans hgoal + +theorem SCases.and_1 {σs} {Q H₁' H₂' H₁₂' T : SPred σs} (hand : H₁' ∧ H₂' ⊣⊢ₛ H₁₂') (hgoal : Q ∧ H₁₂' ⊢ₛ T) : (Q ∧ H₁') ∧ H₂' ⊢ₛ T := + ((SPred.and_congr_r hand.symm).trans SPred.and_assoc.symm).mpr.trans hgoal + +theorem SCases.and_2 {σs} {Q H₁' H₂ T : SPred σs} (hgoal : (Q ∧ H₁') ∧ H₂ ⊢ₛ T) : (Q ∧ H₂) ∧ H₁' ⊢ₛ T := + SPred.and_right_comm.mp.trans hgoal + +theorem SCases.and_3 {σs} {Q H₁ H₂ H T : SPred σs} (hand : H ⊣⊢ₛ H₁ ∧ H₂) (hgoal : (Q ∧ H₂) ∧ H₁ ⊢ₛ T) : Q ∧ H ⊢ₛ T := + (SPred.and_congr_r hand).mp.trans (SPred.and_assoc.mpr.trans (SPred.and_right_comm.mp.trans hgoal)) + +theorem SCases.exists {σs : List Type} {Q : SPred σs} {ψ : α → SPred σs} {T : SPred σs} + (h : ∀ a, Q ∧ ψ a ⊢ₛ T) : Q ∧ (∃ a, ψ a) ⊢ₛ T := + SPred.imp_elim' (SPred.exists_elim fun a => SPred.imp_intro (SPred.entails.trans SPred.and_symm (h a))) + +class IsAnd {σs : List Type} (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where to_and : P ⊣⊢ₛ Q₁ ∧ Q₂ +instance (σs) (Q₁ Q₂ : SPred σs) : IsAnd (σs:=σs) spred(Q₁ ∧ Q₂) Q₁ Q₂ where to_and := .rfl +instance (σs) : IsAnd (σs:=σs) ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝ where to_and := SPred.pure_and.symm +instance (σs) (P Q₁ Q₂ : σ → SPred σs) [base : ∀ s, IsAnd (P s) (Q₁ s) (Q₂ s)] : IsAnd (σs:=σ::σs) P Q₁ Q₂ where to_and := fun s => (base s).to_and + +-- Given σs and H, produces H₁, H₂ and a proof that H₁ ∧ H₂ ⊣⊢ₛ H. +def synthIsAnd (σs H : Expr) : OptionT MetaM (Expr × Expr × Expr) := do + if let some (_σs, H₁, H₂) := parseAnd? H.consumeMData then + return (H₁, H₂, mkApp2 (mkConst ``SPred.bientails.refl) σs H) + try + let H₁ ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) + let H₂ ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) + let inst ← synthInstance (mkApp4 (mkConst ``IsAnd) σs H H₁ H₂) + return (H₁, H₂, mkApp5 (mkConst ``IsAnd.to_and) σs H H₁ H₂ inst) + catch _ => failure + +-- Produce a proof for Q ∧ H ⊢ₛ T by opening a new goal P ⊢ₛ T, where P ⊣⊢ₛ Q ∧ H. +def mCasesAddGoal (goals : IO.Ref (Array MVarId)) (σs : Expr) (T : Expr) (Q : Expr) (H : Expr) : MetaM (Unit × MGoal × Expr) := do + let (P, hand) := mkAnd σs Q H + -- hand : Q ∧ H ⊣⊢ₛ P + -- Need to produce a proof that P ⊢ₛ T and return res + let goal : MGoal := { σs := σs, hyps := P, target := T } + let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr + goals.modify (·.push m.mvarId!) + let prf := mkApp7 (mkConst ``SCases.add_goal) σs P Q H T hand m + let goal := { goal with hyps := mkAnd! σs Q H } + return ((), goal, prf) + +private def getQH (goal : MGoal) : MetaM (Expr × Expr) := do + let some (_, Q, H) := parseAnd? goal.hyps | throwError m!"Internal error: Hypotheses not a conjunction {goal.hyps}" + return (Q, H) + +-- Pretty much like sPureCore, but for existential quantifiers. +-- This function receives the hypothesis H=(∃ (x : α), ψ x) to destruct. +-- It will provide a proof for Q ∧ H ⊢ₛ T +-- if `k` produces a proof for Q ∧ ψ n ⊢ₛ T that may range over `name : α`. +-- It calls `k` with name. +def mCasesExists (H : Expr) (name : TSyntax ``binderIdent) + (k : Expr /-name:α-/ → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr) := do + let some (α, σs, ψ) := H.consumeMData.app3? ``SPred.exists | throwError "Not an existential quantifier {H}" + let (name, ref) ← getFreshHypName name + withLocalDeclD name α fun x => do + addLocalVarInfo ref (← getLCtx) x α + let (r, goal, prf /- : goal.toExpr -/) ← k x + let (Q, _) ← getQH goal + let u ← getLevel α + let prf := mkApp6 (mkConst ``SCases.exists [u]) α σs Q ψ goal.target (← mkLambdaFVars #[x] prf) + let goal := { goal with hyps := mkAnd! σs Q H } + return (r, goal, prf) + +-- goal is P ⊢ₛ T +-- The caller focuses on hypothesis H, P ⊣⊢ₛ Q ∧ H. +-- scasesCore on H, pat and k builds H ⊢ₛ H' according to pat, then calls k with H' +-- k knows context Q and builds goal Q ∧ H' ⊢ₛ T and a proof of the goal. +-- (k should not also apply H ⊢ₛ H' or unfocus because that does not work with spureCore which needs the see `P'` and not `Q ∧ _`.) +-- then scasesCore builds a proof for Q ∧ H ⊢ₛ T from P' ⊢ₛ T: +-- Q ∧ H ⊢ₛ Q ∧ H' ⊢ₛ P' ⊢ₛ T +-- and finally the caller builds the proof for +-- P ⊢ₛ Q ∧ H ⊢ₛ T +-- by unfocussing. +partial def mCasesCore (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → MetaM (α × MGoal × Expr)): MetaM (α × MGoal × Expr) := + match pat with + | .clear => do + let H' := emptyHyp σs -- H' = ⌜True⌝ + let (a, goal, prf) ← k H' + let (Q, _H) ← getQH goal + -- prf : Q ∧ ⌜True⌝ ⊢ₛ T + -- Then Q ∧ H ⊢ₛ Q ∧ ⌜True⌝ ⊢ₛ T + let prf := mkApp5 (mkConst ``SCases.clear) σs Q H goal.target prf + let goal := { goal with hyps := mkAnd! σs Q H } + return (a, goal, prf) + | .stateful name => do + let (name, ref) ← getFreshHypName name + let uniq ← mkFreshId + let hyp := Hyp.mk name uniq H.consumeMData + addHypInfo ref σs hyp (isBinder := true) + k hyp.toExpr + | .pure name => do + mPureCore σs H name fun _ _hφ => do + -- This case is very similar to the clear case, but we need to + -- return Q ⊢ₛ T, not Q ∧ H ⊢ₛ T. + let H' := emptyHyp σs -- H' = ⌜True⌝ + let (a, goal, prf) ← k H' + let (Q, _H) ← getQH goal + -- prf : Q ∧ ⌜True⌝ ⊢ₛ T + -- Then Q ⊢ₛ Q ∧ ⌜True⌝ ⊢ₛ T + let prf := mkApp4 (mkConst ``SCases.pure) σs Q goal.target prf + let goal := { goal with hyps := Q } + return (a, goal, prf) + -- Now prf : Q ∧ H ⊢ₛ T (where H is ⌜φ⌝). Exactly what is needed. + | .one name => do + try + -- First try to see if H can be introduced as a pure hypothesis + let φ ← mkFreshExprMVar (mkSort .zero) + let _ ← synthInstance (mkApp3 (mkConst ``IsPure) σs H φ) + mCasesCore σs H (.pure name) k + catch _ => + -- Otherwise introduce it as a stateful hypothesis. + mCasesCore σs H (.stateful name) k + | .tuple [] => mCasesCore σs H .clear k + | .tuple [p] => mCasesCore σs H p k + | .tuple (p :: ps) => do + if let some (H₁, H₂, hand) ← synthIsAnd σs H then + -- goal is Q ∧ H ⊢ₛ T, where `hand : H ⊣⊢ₛ H₁ ∧ H₂`. Plan: + -- 1. Recurse on H₁ and H₂. + -- 2. The inner callback sees H₁' and H₂' and calls k on H₁₂', where H₁₂' = mkAnd H₁' H₂' + -- 3. The inner callback receives P' ⊢ₛ T, where (P' ⊣⊢ₛ Q ∧ H₁₂'). + -- 4. The inner callback returns (Q ∧ H₁') ∧ H₂' ⊢ₛ T + -- 5. The outer callback receives (Q ∧ H₁') ∧ H₂ ⊢ₛ T + -- 6. The outer callback reassociates and returns (Q ∧ H₂) ∧ H₁' ⊢ₛ T + -- 7. The top-level receives (Q ∧ H₂) ∧ H₁ ⊢ₛ T + -- 8. Reassociate to Q ∧ (H₁ ∧ H₂) ⊢ₛ T, rebuild Q ∧ H ⊢ₛ T and return it. + let ((a, Q), goal, prf) ← mCasesCore σs H₁ p fun H₁' => do + let ((a, Q), goal, prf) ← mCasesCore σs H₂ (.tuple ps) fun H₂' => do + let (H₁₂', hand') := mkAnd σs H₁' H₂' + let (a, goal, prf) ← k H₁₂' -- (2) + -- (3) prf : Q ∧ H₁₂' ⊢ₛ T + -- (4) refocus to (Q ∧ H₁') ∧ H₂' + let (Q, _H) ← getQH goal + let T := goal.target + let prf := mkApp8 (mkConst ``SCases.and_1) σs Q H₁' H₂' H₁₂' T hand' prf + -- check prf + let QH₁' := mkAnd! σs Q H₁' + let goal := { goal with hyps := mkAnd! σs QH₁' H₂' } + return ((a, Q), goal, prf) + -- (5) prf : (Q ∧ H₁') ∧ H₂ ⊢ₛ T + -- (6) refocus to prf : (Q ∧ H₂) ∧ H₁' ⊢ₛ T + let prf := mkApp6 (mkConst ``SCases.and_2) σs Q H₁' H₂ goal.target prf + let QH₂ := mkAnd! σs Q H₂ + let goal := { goal with hyps := mkAnd! σs QH₂ H₁' } + return ((a, Q), goal, prf) + -- (7) prf : (Q ∧ H₂) ∧ H₁ ⊢ₛ T + -- (8) rearrange to Q ∧ H ⊢ₛ T + let prf := mkApp8 (mkConst ``SCases.and_3) σs Q H₁ H₂ H goal.target hand prf + let goal := { goal with hyps := mkAnd! σs Q H } + return (a, goal, prf) + else if let some (_α, σs, ψ) := H.consumeMData.app3? ``SPred.exists then + let .one n := p + | throwError "cannot further destruct a term after moving it to the Lean context" + -- goal is Q ∧ (∃ x, ψ x) ⊢ₛ T. The plan is pretty similar to sPureCore: + -- 1. Recurse on ψ n where (n : α) is named according to the head pattern p. + -- 2. Receive a proof for Q ∧ ψ n ⊢ₛ T. + -- 3. Build a proof for Q ∧ (∃ x, ψ x) ⊢ₛ T from it (in sCasesExists). + mCasesExists H n fun x => mCasesCore σs (ψ.betaRev #[x]) (.alts ps) k + else throwError "Neither a conjunction nor an existential quantifier {H}" + | .alts [] => throwUnsupportedSyntax + | .alts [p] => mCasesCore σs H p k + | .alts (p :: ps) => do + let some (σs, H₁, H₂) := H.consumeMData.app3? ``SPred.or | throwError "Not a disjunction {H}" + -- goal is Q ∧ (H₁ ∨ H₂) ⊢ₛ T. Plan: + -- 1. Recurse on H₁ and H₂ with the same k. + -- 2. Receive proofs for Q ∧ H₁ ⊢ₛ T and Q ∧ H₂ ⊢ₛ T. + -- 3. Build a proof for Q ∧ (H₁ ∨ H₂) ⊢ₛ T from them. + let (_a, goal₁, prf₁) ← mCasesCore σs H₁ p k + let (a, _goal₂, prf₂) ← mCasesCore σs H₂ (.alts ps) k + let (Q, _H₁) ← getQH goal₁ + let goal := { goal₁ with hyps := mkAnd! σs Q (mkApp3 (mkConst ``SPred.or) σs H₁ H₂) } + let prf := mkApp7 (mkConst ``SPred.and_or_elim_r) σs Q H₁ H₂ goal.target prf₁ prf₂ + return (a, goal, prf) + +private theorem assembled_proof {σs} {P P' Q H H' T : SPred σs} + (hfocus : P ⊣⊢ₛ Q ∧ H) (hcases : H ⊢ₛ H') (hand : Q ∧ H' ⊣⊢ₛ P') (hprf₃ : P' ⊢ₛ T) : P ⊢ₛ T := + hfocus.mp.trans ((SPred.and_mono_r hcases).trans (hand.mp.trans hprf₃)) + +private theorem blah2 {σs} {P Q H R : SPred σs} + (h₁ : P ⊣⊢ₛ Q ∧ H) (h₂ : Q ∧ H ⊢ₛ R) : P ⊢ₛ R := + h₁.mp.trans h₂ + +private theorem blah3 {σs} {P Q H T : SPred σs} + (hand : Q ∧ H ⊣⊢ₛ P) (hgoal : P ⊢ₛ T) : Q ∧ H ⊢ₛ T := + hand.mp.trans hgoal + +@[builtin_tactic Lean.Parser.Tactic.mcases] +def elabMCases : Tactic + | `(tactic| mcases $hyp:ident with $pat:mcasesPat) => do + let pat ← liftMacroM <| MCasesPat.parse pat + let (mvar, goal) ← mStartMVar (← getMainGoal) + mvar.withContext do + + let focus ← goal.focusHypWithInfo hyp + -- goal : P ⊢ₛ T, + -- hfocus : P ⊣⊢ₛ Q ∧ H + let Q := focus.restHyps + let H := focus.focusHyp + let goals ← IO.mkRef #[] + let (_, _new_goal, prf) ← mCasesCore goal.σs H pat (mCasesAddGoal goals goal.σs goal.target Q) + + -- Now prf : Q ∧ H ⊢ₛ T. Prepend hfocus.mp, done. + let prf := focus.rewriteHyps goal prf + -- check prf + mvar.assign prf + replaceMainGoal (← goals.get).toList + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean new file mode 100644 index 0000000000..a35253b1df --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean @@ -0,0 +1,32 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal +import Lean.Elab.Tactic.Do.ProofMode.Focus + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +theorem Clear.clear {σs : List Type} {P P' A Q : SPred σs} + (hfocus : P ⊣⊢ₛ P' ∧ A) (h : P' ⊢ₛ Q) : P ⊢ₛ Q := + hfocus.mp.trans <| (SPred.and_mono_l h).trans SPred.and_elim_l + +@[builtin_tactic Lean.Parser.Tactic.mclear] +def elabMClear : Tactic + | `(tactic| mclear $hyp:ident) => do + let mvar ← getMainGoal + mvar.withContext do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + let res ← goal.focusHypWithInfo hyp + let m ← mkFreshExprSyntheticOpaqueMVar (res.restGoal goal).toExpr + + mvar.assign (mkApp7 (mkConst ``Clear.clear) goal.σs goal.hyps + res.restHyps res.focusHyp goal.target res.proof m) + replaceMainGoal [m.mvarId!] + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean new file mode 100644 index 0000000000..4a6fb1d183 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean @@ -0,0 +1,30 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +def mConstructorCore (mvar : MVarId) : MetaM (MVarId × MVarId) := do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + + let mkApp3 (.const ``SPred.and []) σs L R := goal.target | throwError "target is not SPred.and" + + let leftGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := L}.toExpr + let rightGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := R}.toExpr + mvar.assign (mkApp6 (mkConst ``SPred.and_intro) σs goal.hyps L R leftGoal rightGoal) + return (leftGoal.mvarId!, rightGoal.mvarId!) + +@[builtin_tactic Lean.Parser.Tactic.mconstructor] +def elabMConstructor : Tactic | _ => do + let mvar ← getMainGoal + mvar.withContext do + let (leftGoal, rightGoal) ← mConstructorCore mvar + replaceMainGoal [leftGoal, rightGoal] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Display.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Display.lean new file mode 100644 index 0000000000..4b8239a1c1 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Display.lean @@ -0,0 +1,55 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Lean.Elab.Tactic.Do.ProofMode.MGoal + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Expr Meta PrettyPrinter Delaborator SubExpr + +syntax mgoalHyp := ident " : " term + +syntax mgoalStx := ppDedent(ppLine mgoalHyp)* ppDedent(ppLine "⊢ₛ " term) + +@[app_delab MGoalEntails] +partial def delabMGoal : Delab := do + let expr ← instantiateMVars <| ← getExpr + + -- extract environment + let some goal := parseMGoal? expr | failure + + -- delaborate + let (_, hyps) ← withAppFn ∘ withAppArg <| delabHypotheses goal.σs ({}, #[]) + let target ← SPred.Notation.unpack (← withAppArg <| delab) + + -- build syntax + return ⟨← `(mgoalStx| $hyps.reverse* ⊢ₛ $target:term)⟩ +where + delabHypotheses (σs : Expr) + (acc : NameMap Nat × Array (TSyntax ``mgoalHyp)) : + DelabM (NameMap Nat × Array (TSyntax ``mgoalHyp)) := do + let hyps ← getExpr + if let some _ := parseEmptyHyp? hyps then + return acc + if let some hyp := parseHyp? hyps then + let mut (map, lines) := acc + let (idx, name') := + if let some idx := map.find? hyp.name then + (idx + 1, hyp.name.appendAfter <| if idx == 0 then "✝" else "✝" ++ idx.toSuperscriptString) + else + (0, hyp.name) + let name' := mkIdent name' + let stx ← `(mgoalHyp| $name' : $(← SPred.Notation.unpack (← withMDataExpr <| delab))) + return (map.insert hyp.name idx, lines.push stx) + if (parseAnd? hyps).isSome then + let acc_rhs ← withAppArg <| delabHypotheses σs acc + let acc_lhs ← withAppFn ∘ withAppArg <| delabHypotheses σs acc_rhs + return acc_lhs + else + failure + +@[app_delab HypMarker] +def delabHypMarker : Delab := do SPred.Notation.unpack (← withAppArg delab) diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean new file mode 100644 index 0000000000..3ecd9aca63 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean @@ -0,0 +1,50 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.Basic +import Lean.Elab.Tactic.Do.ProofMode.Focus + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +theorem Exact.assumption {σs : List Type} {P P' A : SPred σs} + (h : P ⊣⊢ₛ P' ∧ A) : P ⊢ₛ A := h.mp.trans SPred.and_elim_r + +theorem Exact.from_tautology {σs : List Type} {P T : SPred σs} [PropAsSPredTautology φ T] (h : φ) : P ⊢ₛ T := + SPred.true_intro.trans (PropAsSPredTautology.iff.mp h) + +def _root_.Lean.Elab.Tactic.Do.ProofMode.MGoal.exact (goal : MGoal) (hyp : Syntax) : OptionT MetaM Expr := do + if goal.findHyp? hyp.getId |>.isNone then failure + let focusRes ← goal.focusHypWithInfo ⟨hyp⟩ + OptionT.mk do + let proof := mkApp5 (mkConst ``Exact.assumption) goal.σs goal.hyps focusRes.restHyps goal.target focusRes.proof + unless ← isDefEq focusRes.focusHyp goal.target do + throwError "mexact tactic failed, hypothesis {hyp} is not definitionally equal to {goal.target}" + return proof + +def _root_.Lean.Elab.Tactic.Do.ProofMode.MGoal.exactPure (goal : MGoal) (hyp : Syntax) : TacticM Expr := do + let φ ← mkFreshExprMVar (mkSort .zero) + let h ← elabTermEnsuringType hyp φ + let P ← mkFreshExprMVar (mkApp (mkConst ``SPred) goal.σs) + let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ goal.σs P) + | throwError "mexact tactic failed, {hyp} is not an SPred tautology" + return mkApp6 (mkConst ``Exact.from_tautology) φ goal.σs goal.hyps goal.target inst h + +@[builtin_tactic Lean.Parser.Tactic.mexact] +def elabMExact : Tactic + | `(tactic| mexact $hyp:term) => do + let mvar ← getMainGoal + mvar.withContext do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + if let some prf ← liftMetaM (goal.exact hyp) then + mvar.assign prf + else + mvar.assign (← goal.exactPure hyp) + replaceMainGoal [] + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean new file mode 100644 index 0000000000..6d4b5391b9 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean @@ -0,0 +1,31 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal +import Lean.Elab.Tactic.Do.ProofMode.Basic + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + + +-- set_option pp.all true in +-- #check ⌜False⌝ +private def falseProp (σs : Expr) : Expr := -- ⌜False⌝ standing in for an empty conjunction of hypotheses + mkApp3 (mkConst ``SVal.curry) (.sort .zero) σs <| mkLambda `escape .default (mkApp (mkConst ``SVal.StateTuple) σs) (mkConst ``False) + +@[builtin_tactic Lean.Parser.Tactic.mexfalso] +def elabMExfalso : Tactic | _ => do + let mvar ← getMainGoal + mvar.withContext do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + let newGoal := { goal with target := falseProp goal.σs } + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + let prf := mkApp4 (mkConst ``SPred.exfalso) goal.σs goal.hyps goal.target m + mvar.assign prf + replaceMainGoal [m.mvarId!] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean new file mode 100644 index 0000000000..0677a45376 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean @@ -0,0 +1,80 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Lean.Elab.Tactic.Do.ProofMode.MGoal +import Lean.Meta + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do ProofMode +open Lean Elab.Tactic Meta + +/-- The result of focussing the context of a goal `goal : MGoal` on a particular hypothesis. +The focussed hypothesis is returned as `focusHyp : Expr`, along with the +residual `restHyps : Expr` and a `proof : Expr` for the property +`goal.hyps ⊣⊢ₛ restHyps ∧ focusHyp`. -/ +structure FocusResult where + focusHyp : Expr + restHyps : Expr + proof : Expr + deriving Inhabited + +theorem focus_this {σs : List Type} {P : SPred σs} : P ⊣⊢ₛ ⌜True⌝ ∧ P := + SPred.true_and.symm + +theorem focus_l {σs : List Type} {P P' Q C R : SPred σs} (h₁ : P ⊣⊢ₛ P' ∧ R) (h₂ : P' ∧ Q ⊣⊢ₛ C) : + P ∧ Q ⊣⊢ₛ C ∧ R := + (SPred.and_congr_l h₁).trans (SPred.and_right_comm.trans (SPred.and_congr_l h₂)) + +theorem focus_r {σs : List Type} {P Q Q' C R : SPred σs} (h₁ : Q ⊣⊢ₛ Q' ∧ R) (h₂ : P ∧ Q' ⊣⊢ₛ C) : + P ∧ Q ⊣⊢ₛ C ∧ R := + (SPred.and_congr_r h₁).trans (SPred.and_assoc.symm.trans (SPred.and_congr_l h₂)) + +partial def focusHyp (σs : Expr) (e : Expr) (name : Name) : Option FocusResult := do + if let some hyp := parseHyp? e then + if hyp.name = name then + return ⟨e, emptyHyp σs, mkApp2 (mkConst ``focus_this) σs e⟩ + else + none + else if let some (σs, lhs, rhs) := parseAnd? e then + try + -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Display). + let ⟨focus, rhs', h₁⟩ ← focusHyp σs rhs name + let ⟨C, h₂⟩ := mkAnd σs lhs rhs' + return ⟨focus, C, mkApp8 (mkConst ``focus_r) σs lhs rhs rhs' C focus h₁ h₂⟩ + catch _ => + let ⟨focus, lhs', h₁⟩ ← focusHyp σs lhs name + let ⟨C, h₂⟩ := mkAnd σs lhs' rhs + return ⟨focus, C, mkApp8 (mkConst ``focus_l) σs lhs lhs' rhs C focus h₁ h₂⟩ + else if let some _ := parseEmptyHyp? e then + none + else + panic! s!"focusHyp: hypothesis without proper metadata: {e}" + +def MGoal.focusHyp (goal : MGoal) (name : Name) : Option FocusResult := + Lean.Elab.Tactic.Do.ProofMode.focusHyp goal.σs goal.hyps name + +def FocusResult.refl (σs : Expr) (restHyps : Expr) (focusHyp : Expr) : FocusResult := + let proof := mkApp2 (mkConst ``SPred.bientails.refl) σs (mkAnd! σs restHyps focusHyp) + { restHyps, focusHyp, proof } + +def FocusResult.restGoal (res : FocusResult) (goal : MGoal) : MGoal := + { goal with hyps := res.restHyps } + +def FocusResult.recombineGoal (res : FocusResult) (goal : MGoal) : MGoal := + { goal with hyps := mkAnd! goal.σs res.restHyps res.focusHyp } + +theorem FocusResult.rewrite_hyps {σs} {P Q R : SPred σs} (hrw : P ⊣⊢ₛ Q) (hgoal : Q ⊢ₛ R) : P ⊢ₛ R := + hrw.mp.trans hgoal + +/-- Turn a proof for `(res.recombineGoal goal).toExpr` into one for `goal.toExpr`. -/ +def FocusResult.rewriteHyps (res : FocusResult) (goal : MGoal) : Expr → Expr := + mkApp6 (mkConst ``rewrite_hyps) goal.σs goal.hyps (mkAnd! goal.σs res.restHyps res.focusHyp) goal.target res.proof + +def MGoal.focusHypWithInfo (goal : MGoal) (name : Ident) : MetaM FocusResult := do + let some res := goal.focusHyp name.getId | throwError "unknown hypothesis '{name}'" + let some hyp := parseHyp? res.focusHyp | throwError "impossible; res.focusHyp not a hypothesis" + addHypInfo name goal.σs hyp + pure res diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean new file mode 100644 index 0000000000..02ae4341c7 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2025 Lars König. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal +import Lean.Elab.Tactic.Do.ProofMode.Focus + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +class SimpAnd {σs : List Type} (P Q : SPred σs) (PQ : outParam (SPred σs)) : Prop where + simp_and : P ∧ Q ⊣⊢ₛ PQ + +instance (σs) (P Q : SPred σs) : SimpAnd P Q (spred(P ∧ Q)) where simp_and := .rfl +instance (σs) (P : SPred σs) : SimpAnd P ⌜True⌝ P where simp_and := SPred.and_true +instance (σs) (P : SPred σs) : SimpAnd ⌜True⌝ P P where simp_and := SPred.true_and + +class HasFrame {σs : List Type} (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop where + reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝ +instance (σs) : HasFrame (σs:=σs) ⌜φ⌝ ⌜True⌝ φ where reassoc := SPred.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 := ((SPred.and_congr_l HasFrame.reassoc).trans SPred.and_right_comm).trans (SPred.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 := ((SPred.and_congr_r HasFrame.reassoc).trans SPred.and_assoc.symm).trans (SPred.and_congr_l SimpAnd.simp_and) +instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(⌜φ⌝ ∧ P) P φ where reassoc := SPred.and_comm +instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(P ∧ ⌜φ⌝) P φ where reassoc := .rfl +instance (σs) (P P' Q Q' QQ : SPred σs) [HasFrame P Q φ] [HasFrame P' Q' ψ] [SimpAnd Q Q' QQ]: HasFrame (σs:=σs) spred(P ∧ P') QQ (φ ∧ ψ) where + reassoc := (SPred.and_congr HasFrame.reassoc HasFrame.reassoc).trans + <| SPred.and_assoc.trans + <| (SPred.and_congr_r + <| SPred.and_assoc.symm.trans + <| (SPred.and_congr_l SPred.and_comm).trans + <| SPred.and_assoc.trans + <| SPred.and_congr_r SPred.pure_and).trans + <| SPred.and_assoc.symm.trans + <| SPred.and_congr_l SimpAnd.simp_and +instance (σs) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame (σs:=σs) spred(⌜φ⌝ ∧ P) Q (φ ∧ ψ) where + reassoc := SPred.and_comm.trans + <| (SPred.and_congr_l HasFrame.reassoc).trans + <| SPred.and_right_comm.trans + <| SPred.and_assoc.trans + <| SPred.and_congr_r SPred.pure_and +instance (σs) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame (σs:=σs) spred(P ∧ ⌜φ⌝) Q (ψ ∧ φ) where + reassoc := (SPred.and_congr_l HasFrame.reassoc).trans + <| SPred.and_right_comm.trans + <| SPred.and_assoc.trans + <| SPred.and_congr_r (SPred.and_comm.trans SPred.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 {P : Prop} : HasFrame (σs:=[]) P ⌜True⌝ P where reassoc := SPred.true_and.symm + +-- #synth ∀ {w x P Q y z}, HasFrame spred(⌜w = 2⌝ ∧ ⌜x = 3⌝ ∧ P ∧ ⌜y = 4⌝ ∧ Q ∧ ⌜z=6⌝) _ _ + +theorem Frame.frame {σs : List Type} {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ] + (h : φ → Q ⊢ₛ T) : P ⊢ₛ T := by + apply SPred.pure_elim + · exact HasFrame.reassoc.mp.trans SPred.and_elim_r + · intro hp + exact HasFrame.reassoc.mp.trans (SPred.and_elim_l' (h hp)) + +/-- If `P'` is a conjunction of unnamed hypotheses that are a subset of the named hypotheses of `P`, +transfer the names of the hypotheses of `P` to the hypotheses of `P'`. -/ +partial def transferHypNames (P P' : Expr) : MetaM Expr := (·.snd) <$> label (collectHyps P) P' + where + collectHyps (P : Expr) (acc : List Hyp := []) : List Hyp := + if let some hyp := parseHyp? P then + hyp :: acc + else if let some (_, L, R) := parseAnd? P then + collectHyps L (collectHyps R acc) + else + acc + + label (Ps : List Hyp) (P' : Expr) : MetaM (List Hyp × Expr) := do + let P' ← instantiateMVarsIfMVarApp P' + if let some _ := parseEmptyHyp? P' then + return (Ps, P') + if let some (σs, L, R) := parseAnd? P' then + let (Ps, L') ← label Ps L + let (Ps, R') ← label Ps R + return (Ps, mkAnd! σs L' R') + else + let mut Ps' := Ps + repeat + -- If we cannot find the hyp, it might be in a nested conjunction. + -- Just pick a default name for it. + let uniq ← mkFreshId + let P :: Ps'' := Ps' | return (Ps, { name := `h, uniq, p := P' : Hyp }.toExpr) + Ps' := Ps'' + if ← isDefEq P.p P' then + return (Ps, { P with p := P' }.toExpr) + unreachable! + +def mFrameCore [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] + (goal : MGoal) (kFail : m (α × Expr)) (kSuccess : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MGoal → m (α × Expr)) : m (α × Expr) := do + let P := goal.hyps + let φ ← mkFreshExprMVar (mkSort .zero) + let P' ← mkFreshExprMVar (mkApp (mkConst ``SPred) goal.σs) + if let some inst ← synthInstance? (mkApp4 (mkConst ``HasFrame) goal.σs P P' φ) then + if ← isDefEq (mkConst ``True) φ then return (← kFail) + -- copy the name of P to P' if it is a named hypothesis + let P' ← transferHypNames P P' + let goal := { goal with hyps := P' } + withLocalDeclD `h φ fun hφ => do + let (a, prf) ← kSuccess φ hφ goal + let prf ← mkLambdaFVars #[hφ] prf + let prf := mkApp7 (mkConst ``Frame.frame) goal.σs P P' goal.target φ inst prf + return (a, prf) + else + kFail + +def mTryFrame [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] + (goal : MGoal) (k : MGoal → m (α × Expr)) : m (α × Expr) := + mFrameCore goal (k goal) (fun _ _ goal => k goal) + +@[builtin_tactic Lean.Parser.Tactic.mframe] +def elabMFrame : Tactic | _ => do + let mvar ← getMainGoal + mvar.withContext do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + let (m, prf) ← mFrameCore goal (fun _ => throwError "Could not infer frame") fun _ _ goal => do + let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr + return (m, m) + mvar.assign prf + replaceMainGoal [m.mvarId!] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean new file mode 100644 index 0000000000..bf6552396a --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.Cases +import Lean.Elab.Tactic.Do.ProofMode.Specialize + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +def Have.dup {σs : List Type} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T := + (SPred.and_intro .rfl (hfoc.mp.trans SPred.and_elim_r)).trans hgoal + +def Have.have {σs : List Type} {P H PH T : SPred σs} (hand : P ∧ H ⊣⊢ₛ PH) (hhave : P ⊢ₛ H) (hgoal : PH ⊢ₛ T) : P ⊢ₛ T := + (SPred.and_intro .rfl hhave).trans (hand.mp.trans hgoal) + +def Have.replace {σs : List Type} {P H H' PH PH' T : SPred σs} (hfoc : PH ⊣⊢ₛ P ∧ H ) (hand : P ∧ H' ⊣⊢ₛ PH') (hhave : PH ⊢ₛ H') (hgoal : PH' ⊢ₛ T) : PH ⊢ₛ T := + (SPred.and_intro (hfoc.mp.trans SPred.and_elim_l) hhave).trans (hand.mp.trans hgoal) + +@[builtin_tactic Lean.Parser.Tactic.mdup] +def elabMDup : Tactic + | `(tactic| mdup $h:ident => $h₂:ident) => do + let (mvar, goal) ← ensureMGoal + mvar.withContext do + let some res := goal.focusHyp h.raw.getId | throwError m!"Hypothesis {h} not found" + let P := goal.hyps + let Q := res.restHyps + let H := res.focusHyp + let uniq ← mkFreshId + let hyp := Hyp.mk h₂.raw.getId uniq H.consumeMData + addHypInfo h goal.σs hyp (isBinder := true) + let H' := hyp.toExpr + let T := goal.target + let newGoal := { goal with hyps := mkAnd! goal.σs P H' } + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + mvar.assign (mkApp7 (mkConst ``Have.dup) goal.σs P Q H T res.proof m) + replaceMainGoal [m.mvarId!] + | _ => throwUnsupportedSyntax + +@[builtin_tactic Lean.Parser.Tactic.mhave] +def elabMHave : Tactic + | `(tactic| mhave $h $[: $ty?]? := $rhs) => do + let (mvar, goal) ← ensureMGoal + mvar.withContext do + -- build goal `P ⊢ₛ T` from `P ⊢ₛ H` and residual goal `P ∧ H ⊢ₛ T` + let P := goal.hyps + let spred := mkApp (mkConst ``SPred) goal.σs + let H ← match ty? with + | some ty => elabTerm ty spred + | _ => mkFreshExprMVar spred + let uniq ← mkFreshId + let hyp := Hyp.mk h.raw.getId uniq H + addHypInfo h goal.σs hyp (isBinder := true) + let H := hyp.toExpr + let T := goal.target + let (PH, hand) := mkAnd goal.σs P H + let haveGoal := { goal with target := H } + let hhave ← elabTermEnsuringType rhs haveGoal.toExpr + let newGoal := { goal with hyps := PH } + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + mvar.assign (mkApp8 (mkConst ``Have.have) goal.σs P H PH T hand hhave m) + replaceMainGoal [m.mvarId!] + | _ => throwUnsupportedSyntax + +@[builtin_tactic Lean.Parser.Tactic.mreplace] +def elabMReplace : Tactic + | `(tactic| mreplace $h $[: $ty?]? := $rhs) => do + let (mvar, goal) ← ensureMGoal + mvar.withContext do + -- build goal `P ⊢ₛ T` from `P ⊢ₛ H` and residual goal `P ∧ H ⊢ₛ T` + let PH := goal.hyps + let some res := goal.focusHyp h.raw.getId | throwError m!"Hypothesis {h} not found" + let P := res.restHyps + let H := res.focusHyp + let spred := mkApp (mkConst ``SPred) goal.σs + let H' ← match ty? with + | some ty => elabTerm ty spred + | _ => mkFreshExprMVar spred + let uniq ← mkFreshId + let hyp := Hyp.mk h.raw.getId uniq H' + addHypInfo h goal.σs hyp (isBinder := true) + let H' := hyp.toExpr + let haveGoal := { goal with target := H' } + let hhave ← elabTermEnsuringType rhs haveGoal.toExpr + let T := goal.target + let (PH', hand) := mkAnd goal.σs P H' + let newGoal := { goal with hyps := PH' } + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + let prf := mkApp (mkApp10 (mkConst ``Have.replace) goal.σs P H H' PH PH' T res.proof hand hhave) m + mvar.assign prf + replaceMainGoal [m.mvarId!] + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean new file mode 100644 index 0000000000..acf5610495 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean @@ -0,0 +1,90 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.Basic +import Lean.Elab.Tactic.Do.ProofMode.Display + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +theorem Intro.intro {σs : List Type} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T := + SPred.imp_intro (hand.mp.trans h) + +partial def mIntro [Monad m] [MonadControlT MetaM m] (goal : MGoal) (ident : TSyntax ``binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr) := + controlAt MetaM fun map => do + let some (σs, H, T) := goal.target.app3? ``SPred.imp | throwError "Target not an implication {goal.target}" + let (name, ref) ← getFreshHypName ident + let uniq ← mkFreshId + let hyp := Hyp.mk name uniq H + addHypInfo ref σs hyp (isBinder := true) + let Q := goal.hyps + let H := hyp.toExpr + let (P, hand) := mkAnd goal.σs goal.hyps H + map do + let (a, prf) ← k { goal with hyps := P, target := T } + let prf := mkApp7 (mkConst ``Intro.intro) σs P Q H T hand prf + return (a, prf) + +-- This is regular MVar.intro, but it takes care not to leave the proof mode by preserving metadata +partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax ``binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr) := + controlAt MetaM fun map => do + let some (_type, σ, σs') := (← whnf goal.σs).app3? ``List.cons | liftMetaM <| throwError "Ambient state list not a cons {goal.σs}" + let name ← match ident with + | `(binderIdent| $name:ident) => pure name.getId + | `(binderIdent| $_) => liftMetaM <| mkFreshUserName `s + withLocalDeclD name σ fun s => do + addLocalVarInfo ident (← getLCtx) s σ (isBinder := true) + let H := betaRevPreservingHypNames σs' goal.hyps #[s] + let T := goal.target.betaRev #[s] + map do + let (a, prf) ← k { σs:=σs', hyps:=H, target:=T } + let prf ← mkLambdaFVars #[s] prf + return (a, mkApp5 (mkConst ``SPred.entails_cons_intro) σ σs' goal.hyps goal.target prf) + +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 => + mIntroForallN g n k + +macro_rules + | `(tactic| mintro $pat₁ $pat₂ $pats:mintroPat*) => `(tactic| mintro $pat₁; mintro $pat₂ $pats*) + | `(tactic| mintro $pat:mintroPat) => do + match pat with + | `(mintroPat| $_:binderIdent) => Macro.throwUnsupported -- handled by an elaborator below + | `(mintroPat| ∀$_:binderIdent) => Macro.throwUnsupported -- handled by an elaborator below + | `(mintroPat| $pat:mcasesPat) => `(tactic| mintro h; mcases h with $pat) + | _ => Macro.throwUnsupported -- presently unreachable + +@[builtin_tactic Lean.Parser.Tactic.mintro] +def elabMIntro : Tactic + | `(tactic| mintro $ident:binderIdent) => do + + let (mvar, goal) ← mStartMVar (← getMainGoal) + mvar.withContext do + + let goals ← IO.mkRef [] + mvar.assign (← Prod.snd <$> mIntro goal ident fun newGoal => do + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + goals.modify (m.mvarId! :: ·) + return ((), m)) + replaceMainGoal (← goals.get) + + | `(tactic| mintro ∀$ident:binderIdent) => do + + let (mvar, goal) ← mStartMVar (← getMainGoal) + mvar.withContext do + + let goals ← IO.mkRef [] + mvar.assign (← Prod.snd <$> mIntroForall goal ident fun newGoal => do + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + goals.modify (m.mvarId! :: ·) + return ((), m)) + replaceMainGoal (← goals.get) + + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean b/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean new file mode 100644 index 0000000000..3a887846bc --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean @@ -0,0 +1,38 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +def mLeftRightCore (right : Bool) (mvar : MVarId) : MetaM MVarId := do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + + let mkApp3 (.const ``SPred.or []) σs L R := goal.target | throwError "target is not SPred.or" + + let (thm, keep) := if right then (``SPred.or_intro_r', R) else (``SPred.or_intro_l', L) + + let newGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := keep}.toExpr + mvar.assign (mkApp5 (mkConst thm) σs goal.hyps L R newGoal) + return newGoal.mvarId! + +@[builtin_tactic Lean.Parser.Tactic.mleft] +def elabMLeft : Tactic | _ => do + let mvar ← getMainGoal + mvar.withContext do + let newGoal ← mLeftRightCore (right := false) mvar + replaceMainGoal [newGoal] + +@[builtin_tactic Lean.Parser.Tactic.mright] +def elabMRight : Tactic | _ => do + let mvar ← getMainGoal + mvar.withContext do + let newGoal ← mLeftRightCore (right := true) mvar + replaceMainGoal [newGoal] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean new file mode 100644 index 0000000000..0d24cb5111 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean @@ -0,0 +1,192 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Do.SPred.DerivedLaws + +import Lean.Meta +open Lean Elab Meta + +namespace Std.Do + +/-- Tautology in `SPred` as a definition. -/ +abbrev SPred.tautological {σs : List Type} (Q : SPred σs) : Prop := ⊢ₛ Q + +class PropAsSPredTautology (φ : Prop) {σs : outParam (List Type)} (P : outParam (SPred σs)) : Prop where + iff : φ ↔ ⊢ₛ P + +instance : PropAsSPredTautology (σs := []) φ φ where + iff := true_imp_iff.symm + +instance : PropAsSPredTautology (P ⊢ₛ Q) spred(P → Q) where + iff := (SPred.entails_true_intro P Q).symm + +instance : PropAsSPredTautology (⊢ₛ P) P where + iff := Iff.rfl + +end Std.Do + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do + +theorem start_entails {φ : Prop} [PropAsSPredTautology φ P] : (⊢ₛ P) → φ := + PropAsSPredTautology.iff.mpr + +theorem elim_entails {φ : Prop} [PropAsSPredTautology φ P] : φ → (⊢ₛ P) := + PropAsSPredTautology.iff.mp + +@[match_pattern] def nameAnnotation := `name +@[match_pattern] def uniqAnnotation := `uniq + +structure Hyp where + name : Name + uniq : Name -- for display purposes only + p : Expr + +def parseHyp? : Expr → Option Hyp + | .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ p => + some ⟨name, uniq, p⟩ -- NB: mdatas are transparent to SubExpr; hence no pos.push + | _ => none + +def Hyp.toExpr (hyp : Hyp) : Expr := + .mdata ⟨[(nameAnnotation, .ofName hyp.name), (uniqAnnotation, .ofName hyp.uniq)]⟩ hyp.p + +/-- An elaborator to create a new named hypothesis for an `MGoal` context. -/ +elab "mk_hyp " name:ident " := " e:term : term <= ty? => do + let e ← Lean.Elab.Term.elabTerm e ty? + let uniq ← mkFreshId + return (Hyp.mk name.getId uniq e).toExpr + +-- set_option pp.all true in +-- #check ⌜True⌝ +def emptyHyp (σs : Expr) : Expr := -- ⌜True⌝ standing in for an empty conjunction of hypotheses + mkApp3 (mkConst ``SVal.curry) (.sort .zero) σs <| mkLambda `escape .default (mkApp (mkConst ``SVal.StateTuple) σs) (mkConst ``True) +def parseEmptyHyp? : Expr → Option Expr + | mkApp3 (.const ``SVal.curry _) (.sort .zero) σs (.lam _ _ (.const ``True _) _) => some σs + | _ => none + +def pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos := + pos.pushNaryArg 3 1 + +def pushRightConjunct (pos : SubExpr.Pos) : SubExpr.Pos := + pos.pushNaryArg 3 2 + +/-- Combine two hypotheses into a conjunction. +Precondition: Neither `lhs` nor `rhs` is empty (`parseEmptyHyp?`). -/ +def mkAnd! (σs lhs rhs : Expr) : Expr := + mkApp3 (mkConst ``SPred.and) σs lhs rhs + +/-- Smart constructor that cancels away empty hypotheses, +along with a proof that `lhs ∧ rhs ⊣⊢ₛ result`. -/ +def mkAnd (σs lhs rhs : Expr) : Expr × Expr := + if let some _ := parseEmptyHyp? lhs then + (rhs, mkApp2 (mkConst ``SPred.true_and) σs rhs) + else if let some _ := parseEmptyHyp? rhs then + (lhs, mkApp2 (mkConst ``SPred.and_true) σs lhs) + else + let result := mkAnd! σs lhs rhs + (result, mkApp2 (mkConst ``SPred.bientails.refl) σs result) + +def σs.mkType : Expr := mkApp (mkConst ``List [.succ .zero]) (mkSort (.succ .zero)) +def σs.mkNil : Expr := mkApp (mkConst ``List.nil [.succ .zero]) (mkSort (.succ .zero)) + +def parseAnd? (e : Expr) : Option (Expr × Expr × Expr) := + e.app3? ``SPred.and <|> (σs.mkNil, ·) <$> e.app2? ``And + +structure MGoal where + σs : Expr -- Q(List Type) + hyps : Expr -- A conjunction of hypotheses in `SPred σs`, each carrying a name and uniq as metadata (`parseHyp?`) + target : Expr -- Q(SPred $σs) + deriving Inhabited + +/-- This is the same as `SPred.entails`. +This constant is used to detect `SPred` proof mode goals. -/ +abbrev MGoalEntails := @SPred.entails + +def parseMGoal? (expr : Expr) : Option MGoal := do + let some (σs, hyps, target) := expr.consumeMData.app3? ``MGoalEntails | none + some { σs, hyps, target } + +open Tactic in +def ensureMGoal : TacticM (MVarId × MGoal) := do + let mvar ← getMainGoal + let goal ← instantiateMVars <| (← mvar.getType) + if let some goal := parseMGoal? goal then + return (mvar, goal) + else + throwError "Not in proof mode" + +def MGoal.strip (goal : MGoal) : Expr := -- omits the .mdata wrapper + mkApp3 (mkConst ``SPred.entails) goal.σs goal.hyps goal.target + +/-- Roundtrips with `parseMGoal?`. -/ +def MGoal.toExpr (goal : MGoal) : Expr := + mkApp3 (mkConst ``MGoalEntails) goal.σs goal.hyps goal.target + +partial def MGoal.findHyp? (goal : MGoal) (name : Name) : Option (SubExpr.Pos × Hyp) := go goal.hyps SubExpr.Pos.root + where + go (e : Expr) (p : SubExpr.Pos) : Option (SubExpr.Pos × Hyp) := do + if let some hyp := parseHyp? e then + if hyp.name = name then + return (p, hyp) + else + none + else if let some (_, lhs, rhs) := parseAnd? e then + -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Display). + go rhs (pushLeftConjunct p) <|> go lhs (pushRightConjunct p) + else if let some _ := parseEmptyHyp? e then + none + else + panic! "MGoal.findHyp?: hypothesis without proper metadata: {e}" + +def MGoal.checkProof (goal : MGoal) (prf : Expr) (suppressWarning : Bool := false) : MetaM Unit := do + check prf + let prf_type ← inferType prf + unless ← isDefEq goal.toExpr prf_type do + throwError "MGoal.checkProof: the proof and its supposed type did not match.\ngoal: {goal.toExpr}\nproof: {prf_type}" + unless suppressWarning do + logWarning m!"stray MGoal.checkProof {prf_type} {goal.toExpr}" + +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 _σs := parseEmptyHyp? e then + emptyHyp σs' + else if let some hyp := parseHyp? e then + { hyp with p := hyp.p.betaRev args }.toExpr + else if let some (_σs, lhs, rhs) := parseAnd? e then + -- _σs = σ :: σs' + mkAnd! σs' (betaRevPreservingHypNames σs' lhs args) (betaRevPreservingHypNames σs' rhs args) + else + e.betaRev args + +def betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr := + betaRevPreservingHypNames σs' e args.reverse + +def dropStateList (σs : Expr) (n : Nat) : MetaM Expr := do + let mut σs := σs + for _ in [:n] do + let some (_type, _σ, σs') := (← whnfR σs).app3? ``List.cons | throwError "Ambient state list not a cons {σs}" + σs := σs' + return σs + +/-- This is only used for display purposes, so that we can render context variables that appear +to have type `A : PROP` even though `PROP` is not a type. -/ +def HypMarker {σs : List Type} (_A : SPred σs) : Prop := True + +def addLocalVarInfo (stx : Syntax) (lctx : LocalContext) + (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do + Elab.withInfoContext' (pure ()) + (fun _ => + return .inl <| .ofTermInfo + { elaborator := .anonymous, lctx, expr, stx, expectedType?, isBinder }) + (return .ofPartialTermInfo { elaborator := .anonymous, lctx, stx, expectedType? }) + +def addHypInfo (stx : Syntax) (σs : Expr) (hyp : Hyp) (isBinder := false) : MetaM Unit := do + let lctx ← getLCtx + let ty := mkApp2 (mkConst ``HypMarker) σs hyp.p + addLocalVarInfo stx (lctx.mkLocalDecl ⟨hyp.uniq⟩ hyp.name ty) (.fvar ⟨hyp.uniq⟩) ty isBinder diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean new file mode 100644 index 0000000000..77d2be5e1b --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean @@ -0,0 +1,71 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal +import Lean.Elab.Tactic.Do.ProofMode.Focus + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +class IsPure {σs : List Type} (P : SPred σs) (φ : outParam Prop) where to_pure : P ⊣⊢ₛ ⌜φ⌝ +instance (σs) : IsPure (σs:=σs) ⌜φ⌝ φ where to_pure := .rfl +instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ → ⌜ψ⌝) (φ → ψ) where to_pure := SPred.pure_imp +instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ ∧ ⌜ψ⌝) (φ ∧ ψ) where to_pure := SPred.pure_and +instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ ∨ ⌜ψ⌝) (φ ∨ ψ) where to_pure := SPred.pure_or +instance (σs) (P : α → Prop) : IsPure (σs:=σs) spred(∃ x, ⌜P x⌝) (∃ x, P x) where to_pure := SPred.pure_exists +instance (σs) (P : α → Prop) : IsPure (σs:=σs) spred(∀ x, ⌜P x⌝) (∀ x, P x) where to_pure := SPred.pure_forall +instance (σs) (P : SPred (σ::σs)) [inst : IsPure P φ] : IsPure (σs:=σs) spred(P s) φ where to_pure := (iff_of_eq SPred.bientails_cons).mp inst.to_pure s +instance (P : Prop) : IsPure (σs:=[]) P P where to_pure := Iff.rfl + +theorem Pure.thm {σs : List Type} {P Q T : SPred σs} {φ : Prop} [IsPure Q φ] + (h : φ → P ⊢ₛ T) : P ∧ Q ⊢ₛ T := by + apply SPred.pure_elim + · exact SPred.and_elim_r.trans IsPure.to_pure.mp + · intro hp + exact SPred.and_elim_l.trans (h hp) + +-- NB: We do not use MVarId.intro because that would mean we require all callers to supply an MVarId. +-- This function only knows about the hypothesis H=⌜φ⌝ to destruct. +-- It will provide a proof for Q ∧ H ⊢ₛ T +-- if `k` produces a proof for Q ⊢ₛ T that may range over a pure proof h : φ. +-- It calls `k` with the φ in H = ⌜φ⌝ and a proof `h : φ` thereof. +def mPureCore (σs : Expr) (hyp : Expr) (name : TSyntax ``binderIdent) + (k : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr) := do + let φ ← mkFreshExprMVar (mkSort .zero) + let inst ← synthInstance (mkApp3 (mkConst ``IsPure) σs hyp φ) + let (name, ref) ← getFreshHypName name + withLocalDeclD name φ fun h => do + addLocalVarInfo ref (← getLCtx) h φ + let (a, goal, prf /- : goal.toExpr -/) ← k φ h + let prf ← mkLambdaFVars #[h] prf + let prf := mkApp7 (mkConst ``Pure.thm) σs goal.hyps hyp goal.target φ inst prf + let goal := { goal with hyps := mkAnd! σs goal.hyps hyp } + return (a, goal, prf) + +@[builtin_tactic Lean.Parser.Tactic.mpure] +def elabMPure : Tactic + | `(tactic| mpure $hyp) => do + let mvar ← getMainGoal + mvar.withContext do + let g ← instantiateMVars <| ← mvar.getType + let some goal := parseMGoal? g | throwError "not in proof mode" + let res ← goal.focusHypWithInfo hyp + let (m, _new_goal, prf) ← mPureCore goal.σs res.focusHyp (← `(binderIdent| $hyp:ident)) fun _ _ => do + let goal := res.restGoal goal + let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr + return (m, goal, m) + let prf := res.rewriteHyps goal prf + mvar.assign prf + replaceMainGoal [m.mvarId!] + | _ => throwUnsupportedSyntax + +/-- A generalization of `SPred.pure_intro` exploiting `IsPure`. -/ +private theorem Pure.intro {σs : List Type} {P Q : SPred σs} {φ : Prop} [IsPure Q φ] (hp : φ) : P ⊢ₛ Q := + (SPred.pure_intro hp).trans IsPure.to_pure.mpr + +macro "mpure_intro" : tactic => `(tactic| apply Pure.intro) diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean new file mode 100644 index 0000000000..eb502b0d21 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean @@ -0,0 +1,78 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.Focus +import Lean.Elab.Tactic.Do.ProofMode.Assumption +import Lean.Elab.Tactic.Do.ProofMode.Exact + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do Lean.Parser.Tactic +open Lean Elab Tactic Meta + +def patAsTerm (pat : MRefinePat) (expected : Option Expr := none) : OptionT TacticM Expr := do + match pat with + | .pure t => elabTerm t expected + | .one name => + if let `(binderIdent| $name:ident) := name then + elabTerm (← `($name)) expected + else failure + | _ => failure + +partial def mRefineCore (goal : MGoal) (pat : MRefinePat) (k : MGoal → TSyntax ``binderIdent → TacticM Expr) : TacticM Expr := do + match pat with + | .stateful name => liftMetaM do + match name with + | `(binderIdent| $name:ident) => do + let some prf ← goal.exact name | throwError "unknown hypothesis '{repr name}'" + return prf + | _ => do + let some prf ← goal.assumption | throwError "could not solve {goal.target} by assumption" + return prf + | .pure t => do + goal.exactPure t + | .one name => + if let `(binderIdent| $_:ident) := name then + mRefineCore goal (.pure ⟨name.raw⟩) k <|> mRefineCore goal (.stateful name) k + else + mRefineCore goal (.stateful name) k + | .hole name => k goal name + | .tuple [] => throwUnsupportedSyntax + | .tuple [p] => mRefineCore goal p k + | .tuple (p::ps) => do + let T ← whnfR goal.target + if let some (σs, T₁, T₂) := parseAnd? T.consumeMData then + let prf₁ ← mRefineCore { goal with target := T₁ } p k + let prf₂ ← mRefineCore { goal with target := T₂ } (.tuple ps) k + return mkApp6 (mkConst ``SPred.and_intro) σs goal.hyps T₁ T₂ prf₁ prf₂ + else if let some (α, σs, ψ) := T.app3? ``SPred.exists then + let some witness ← patAsTerm p (some α) | throwError "pattern does not elaborate to a term to instantiate ψ" + let prf ← mRefineCore { goal with target := ψ.betaRev #[witness] } (.tuple ps) k + let u ← getLevel α + return mkApp6 (mkConst ``SPred.exists_intro' [u]) α σs goal.hyps ψ witness prf + else throwError "Neither a conjunction nor an existential quantifier {goal.target}" + +@[builtin_tactic Lean.Parser.Tactic.mrefine] +def elabMRefine : Tactic + | `(tactic| mrefine $pat:mrefinePat) => do + let pat ← liftMacroM <| MRefinePat.parse pat + let (mvar, goal) ← mStartMVar (← getMainGoal) + mvar.withContext do + + let goals ← IO.mkRef #[] + let prf ← mRefineCore goal pat fun goal name => do + let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr name.raw.getId + goals.modify (·.push m.mvarId!) + return m + mvar.assign prf + replaceMainGoal (← goals.get).toList + | _ => throwUnsupportedSyntax + +macro_rules + | `(tactic| mexists $args,*) => do + let pats ← args.getElems.mapM fun t => `(mrefinePat| ⌜$t⌝) + let pat ← pats.foldrM (fun pat acc => `(mrefinePat| ⟨$pat, $acc⟩)) (← `(mrefinePat| ?_)) + `(tactic| (mrefine $pat; try massumption)) diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean new file mode 100644 index 0000000000..7217e2174f --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean @@ -0,0 +1,40 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.Focus +import Lean.Elab.Tactic.Do.ProofMode.Basic + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +theorem Revert.revert {σs : List Type} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (h : Q ⊢ₛ H → T) : P ⊢ₛ T := + hfoc.mp.trans (SPred.imp_elim h) + +partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → MetaM Expr) : MetaM Expr := do + let res ← goal.focusHypWithInfo ref + let P := goal.hyps + let Q := res.restHyps + let H := res.focusHyp + let T := goal.target + let prf ← k { goal with hyps := Q, target := mkApp3 (mkConst ``SPred.imp) goal.σs H T } + let prf := mkApp7 (mkConst ``Revert.revert) goal.σs P Q H T res.proof prf + return prf + +@[builtin_tactic Lean.Parser.Tactic.mrevert] +def elabMRevert : Tactic + | `(tactic| mrevert $h) => do + let (mvar, goal) ← mStartMVar (← getMainGoal) + mvar.withContext do + + let goals ← IO.mkRef [] + mvar.assign (← mRevertStep goal h fun newGoal => do + let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr + goals.modify (m.mvarId! :: ·) + return m) + replaceMainGoal (← goals.get) + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean new file mode 100644 index 0000000000..627d189329 --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean @@ -0,0 +1,203 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax +import Lean.Elab.Tactic.Do.ProofMode.MGoal +import Lean.Elab.Tactic.Do.ProofMode.Focus +import Lean.Elab.Tactic.Do.ProofMode.Basic +import Lean.Elab.Tactic.Do.ProofMode.Pure + +namespace Lean.Elab.Tactic.Do.ProofMode +open Std.Do +open Lean Elab Tactic Meta + +initialize registerTraceClass `Meta.Tactic.Do.specialize + +theorem Specialize.imp_stateful {P P' Q R : SPred σs} + (hrefocus : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q) : P ∧ (Q → R) ⊢ₛ P ∧ R := by + calc spred(P ∧ (Q → R)) + _ ⊢ₛ (P' ∧ Q) ∧ (Q → R) := SPred.and_intro hrefocus.mp SPred.and_elim_r + _ ⊢ₛ P' ∧ Q ∧ (Q → R) := SPred.and_assoc.mp + _ ⊢ₛ P' ∧ Q ∧ R := SPred.and_mono_r (SPred.and_intro SPred.and_elim_l SPred.imp_elim_r) + _ ⊢ₛ (P' ∧ Q) ∧ R := SPred.and_assoc.mpr + _ ⊢ₛ P ∧ R := SPred.and_mono_l (hrefocus.mpr.trans SPred.and_elim_l) + +theorem Specialize.imp_pure {P Q R : SPred σs} [PropAsSPredTautology φ Q] + (h : φ) : P ∧ (Q → R) ⊢ₛ P ∧ R := by + calc spred(P ∧ (Q → R)) + _ ⊢ₛ P ∧ (Q ∧ (Q → R)) := SPred.and_mono_r (SPred.and_intro (SPred.true_intro.trans (PropAsSPredTautology.iff.mp h)) .rfl) + _ ⊢ₛ P ∧ R := SPred.and_mono_r (SPred.mp SPred.and_elim_r SPred.and_elim_l) + +theorem Specialize.forall {P : SPred σs} {ψ : α → SPred σs} + (a : α) : P ∧ (∀ x, ψ x) ⊢ₛ P ∧ ψ a := SPred.and_mono_r (SPred.forall_elim a) + +theorem Specialize.pure_start {φ : Prop} {H P T : SPred σs} [PropAsSPredTautology φ H] (hpure : φ) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T := + (SPred.and_intro .rfl (SPred.true_intro.trans (PropAsSPredTautology.iff.mp hpure))).trans hgoal + +theorem Specialize.pure_taut {σs} {φ} {P : SPred σs} [IsPure P φ] (h : φ) : ⊢ₛ P := + (SPred.pure_intro h).trans IsPure.to_pure.mpr + +def mSpecializeImpStateful (σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do + guard (arg.raw.isIdent) + let some argRes := focusHyp σs (mkAnd! σs P QR) arg.raw.getId | failure + let some hyp := parseHyp? argRes.focusHyp | failure + addHypInfo arg σs hyp + OptionT.mk do -- no OptionT failure after this point + -- The goal is P ∧ (Q → R) + -- argRes.proof : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q + -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R)) + let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpStateful violated" + let P' := argRes.restHyps + let Q := argRes.focusHyp + let hrefocus := argRes.proof -- P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q + let mkApp3 (.const ``SPred.imp []) σs Q' R := specHyp.p | throwError "Expected implication {QR}" + let proof := mkApp6 (mkConst ``Specialize.imp_stateful) σs P P' Q R hrefocus + -- check proof + trace[Meta.Tactic.Do.specialize] "Statefully specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}" + unless ← isDefEq Q Q' do + throwError "failed to specialize {specHyp.p} with {Q}" + + return ({ specHyp with p := R }.toExpr, proof) + +def mSpecializeImpPure (_σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do + let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpPure violated" + let mkApp3 (.const ``SPred.imp []) σs Q R := specHyp.p | failure + let mut φ ← mkFreshExprMVar (mkSort .zero) + let mut (hφ, mvarIds) ← try + elabTermWithHoles arg.raw φ `specialize (allowNaturalHoles := true) + catch _ => failure + -- We might have hφ : φ and Q = ⌜φ⌝. In this case, convert hφ to a proof of ⊢ₛ ⌜φ⌝, + -- so that we can infer an instance of `PropAsSPredTautology`. + -- NB: PropAsSPredTautology φ ⌜φ⌝ is unfortunately impossible because ⊢ₛ ⌜φ⌝ does not imply φ. + -- Hence this additional (lossy) conversion. + if let some inst ← synthInstance? (mkApp3 (mkConst ``IsPure) σs Q φ) then + hφ := mkApp5 (mkConst ``Specialize.pure_taut) σs φ Q inst hφ + φ := mkApp2 (mkConst ``SPred.tautological) σs Q + + let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ σs Q) + | failure + + OptionT.mk do -- no OptionT failure after this point + -- The goal is P ∧ (Q → R) + -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R)) + pushGoals mvarIds + let proof := mkApp7 (mkConst ``Specialize.imp_pure) σs φ P Q R inst hφ + -- check proof + trace[Meta.Tactic.Do.specialize] "Purely specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}" + -- logInfo m!"proof: {← inferType proof}" + return ({ specHyp with p := R }.toExpr, proof) + +def mSpecializeForall (_σs : Expr) (P : Expr) (Ψ : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do + let some specHyp := parseHyp? Ψ | panic! "Precondition of specializeForall violated" + let mkApp3 (.const ``SPred.forall [u]) α σs αR := specHyp.p | failure + let (a, mvarIds) ← try + elabTermWithHoles arg.raw α `specialize (allowNaturalHoles := true) + catch _ => failure + OptionT.mk do -- no OptionT failure after this point + pushGoals mvarIds + let proof := mkApp5 (mkConst ``Specialize.forall [u]) σs α P αR a + let R := αR.beta #[a] + -- check proof + trace[Meta.Tactic.Do.specialize] "Instantiate {specHyp.p} with {a}. New Goal: {mkAnd! σs P R}" + return ({ specHyp with p := R }.toExpr, proof) + +theorem focus {P P' Q R : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ Q) (hnew : P' ∧ Q ⊢ₛ R) : P ⊢ₛ R := + hfocus.mp.trans hnew + +@[builtin_tactic Lean.Parser.Tactic.mspecialize] +def elabMSpecialize : Tactic + | `(tactic| mspecialize $hyp $args*) => do + let (mvar, goal) ← mStartMVar (← getMainGoal) + mvar.withContext do + + -- Want to prove goal P ⊢ T, where hyp occurs in P. + -- So we + -- 1. focus on hyp (referred to as H): P ⊣⊢ₛ P' ∧ H. Prove P' ∧ H ⊢ₛ T + -- 2. Produce a (transitive chain of) proofs + -- P' ∧ H ⊢ P' ∧ H₁ ⊢ₛ P' ∧ H₂ ⊢ₛ ... + -- One for each arg; end up with goal P' ∧ H' ⊢ₛ T + -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'. + -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain. + let some specFocus := goal.focusHyp hyp.getId | throwError "unknown identifier '{hyp}'" + let σs := goal.σs + let P := specFocus.restHyps + let mut H := specFocus.focusHyp + let some hyp' := parseHyp? H | panic! "Invariant of specialize violated" + addHypInfo hyp σs hyp' + -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar + let mut proof : Expr → Expr := + mkApp7 (mkConst ``focus) σs goal.hyps P H goal.target specFocus.proof + + for arg in args do + let res? ← OptionT.run + (mSpecializeImpStateful σs P H arg + <|> mSpecializeImpPure σs P H arg + <|> mSpecializeForall σs P H arg) + match res? with + | some (H', H2H') => + -- logInfo m!"H: {H}, proof: {← inferType H2H'}" + proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal) + H := H' + | none => + throwError "Could not specialize {H} with {arg}" + + let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr + mvar.assign (proof newMVar) + replaceMainGoal [newMVar.mvarId!] + + | _ => throwUnsupportedSyntax + +@[builtin_tactic Lean.Parser.Tactic.mspecializePure] +def elabMspecializePure : Tactic + | `(tactic| mspecialize_pure $head $args* => $hyp) => do + -- "mspecialize_pure" >> term >> many (ppSpace >> checkColGt "irrelevant" >> termParser (eval_prec max)) >> "as" >> ident + let (mvar, goal) ← mStartMVar (← getMainGoal) + mvar.withContext do + + -- Want to prove goal P ⊢ₛ T. `head` is a pure proof of type `φ` that turns into `⊢ₛ H` via `start_entails`. + -- So we + -- 1. Introduce `head` via `PropAsEntails` as stateful hypothesis named `hyp`, P ∧ (hyp : H) ⊢ₛ T + -- 2. (from here on it's the same as `mspecialize`.) + -- Produce a (transitive chain of) proofs + -- P ∧ H ⊢ P ∧ H₁ ⊢ₛ P ∧ H₂ ⊢ₛ ... + -- One for each arg; end up with goal P ∧ H' ⊢ₛ T + -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'. + -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain. + let σs := goal.σs + let P := goal.hyps + let T := goal.target + let hφ ← elabTerm head none + let φ ← inferType hφ + let H ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) + let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology) φ σs H) + let uniq ← mkFreshId + let mut H := (Hyp.mk hyp.getId uniq (← instantiateMVars H)).toExpr + + let goal : MGoal := { goal with hyps := mkAnd! σs P H } + -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar + let mut proof : Expr → Expr := + mkApp8 (mkConst ``Specialize.pure_start) σs φ H P T inst hφ + + for arg in args do + let res? ← OptionT.run + (mSpecializeImpStateful σs P H ⟨arg⟩ + <|> mSpecializeImpPure σs P H ⟨arg⟩ + <|> mSpecializeForall σs P H ⟨arg⟩) + match res? with + | some (H', H2H') => + -- logInfo m!"H: {H}, proof: {← inferType H2H'}" + proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal) + H := H' + | none => + throwError "Could not specialize {H} with {arg}" + + let some hyp' := parseHyp? H | panic! "Invariant of specialize_pure violated" + addHypInfo hyp σs hyp' + + let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr + mvar.assign (proof newMVar) + replaceMainGoal [newMVar.mvarId!] + | _ => throwUnsupportedSyntax diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index d08ce518d9..6af7909266 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich prelude import Lean.Parser.Term import Lean.Parser.Tactic.Doc +import Std.Tactic.Do.Syntax namespace Lean namespace Parser diff --git a/src/Std.lean b/src/Std.lean index 70238c1772..3e926c0a9c 100644 --- a/src/Std.lean +++ b/src/Std.lean @@ -6,6 +6,7 @@ Authors: Sebastian Ullrich prelude import Std.Classes import Std.Data +import Std.Do import Std.Sat import Std.Sync import Std.Time diff --git a/src/Std/Do.lean b/src/Std/Do.lean new file mode 100644 index 0000000000..3bd6f8ceb5 --- /dev/null +++ b/src/Std/Do.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Std.Do.SPred diff --git a/src/Std/Do/SPred.lean b/src/Std/Do/SPred.lean new file mode 100644 index 0000000000..96327c1b77 --- /dev/null +++ b/src/Std/Do/SPred.lean @@ -0,0 +1,11 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Std.Do.SPred.SVal +import Std.Do.SPred.SPred +import Std.Do.SPred.Notation +import Std.Do.SPred.Laws +import Std.Do.SPred.DerivedLaws diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean new file mode 100644 index 0000000000..c5b28a79de --- /dev/null +++ b/src/Std/Do/SPred/DerivedLaws.lean @@ -0,0 +1,162 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Init.ByCases +import Std.Do.SPred.Laws + +/-! +# Derived laws of `SPred` + +This module contains some laws about `SPred` that are derived from +the laws in `Std.Do.SPred.Laws`. +-/ + +namespace Std.Do.SPred + +variable {σs : List Type} {P P' Q Q' R R' : SPred σs} {φ φ₁ φ₂ : Prop} + +theorem entails.rfl {σs : List Type} {P : SPred σs} : P ⊢ₛ P := entails.refl P + +theorem bientails.rfl {σs : List Type} {P : SPred σs} : P ⊣⊢ₛ P := bientails.refl P +theorem bientails.of_eq {σs : List Type} {P Q : SPred σs} (h : P = Q) : P ⊣⊢ₛ Q := h ▸ .rfl + +theorem bientails.mp {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (P ⊢ₛ Q) := fun h => (bientails.iff.mp h).1 +theorem bientails.mpr {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊢ₛ P) := fun h => (bientails.iff.mp h).2 + +/-! # Connectives -/ + +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 +theorem or_intro_r' (h : P ⊢ₛ R) : P ⊢ₛ Q ∨ R := h.trans or_intro_r +theorem and_symm : P ∧ Q ⊢ₛ Q ∧ P := and_intro and_elim_r and_elim_l +theorem or_symm : P ∨ Q ⊢ₛ Q ∨ P := or_elim or_intro_r or_intro_l +theorem imp_intro' (h : Q ∧ P ⊢ₛ R) : P ⊢ₛ Q → R := imp_intro <| and_symm.trans h +theorem entails.trans' (h₁ : P ⊢ₛ Q) (h₂ : P ∧ Q ⊢ₛ R) : P ⊢ₛ R := (and_intro .rfl h₁).trans h₂ +theorem mp (h₁ : P ⊢ₛ Q → R) (h₂ : P ⊢ₛ Q) : P ⊢ₛ R := entails.trans' h₂ (imp_elim h₁) +theorem imp_elim' (h : Q ⊢ₛ P → R) : P ∧ Q ⊢ₛ R := and_symm.trans <| imp_elim h +theorem imp_elim_l : (P → Q) ∧ P ⊢ₛ Q := imp_elim .rfl +theorem imp_elim_r : P ∧ (P → Q) ⊢ₛ Q := imp_elim' .rfl +theorem false_elim : ⌜False⌝ ⊢ₛ P := pure_elim' False.elim +theorem true_intro : P ⊢ₛ ⌜True⌝ := pure_intro trivial +theorem exists_intro' {σs} {P} {Ψ : α → SPred σs} (a : α) (h : P ⊢ₛ Ψ a) : P ⊢ₛ ∃ a, Ψ a := h.trans (exists_intro a) +theorem and_or_elim_l (hleft : P ∧ R ⊢ₛ T) (hright : Q ∧ R ⊢ₛ T) : (P ∨ Q) ∧ R ⊢ₛ T := imp_elim (or_elim (imp_intro hleft) (imp_intro hright)) +theorem and_or_elim_r (hleft : P ∧ Q ⊢ₛ T) (hright : P ∧ R ⊢ₛ T) : P ∧ (Q ∨ R) ⊢ₛ T := imp_elim' (or_elim (imp_intro (and_symm.trans hleft)) (imp_intro (and_symm.trans hright))) +theorem exfalso (h : P ⊢ₛ ⌜False⌝) : P ⊢ₛ Q := h.trans false_elim + +/-! # Monotonicity and congruence -/ + +theorem and_mono (hp : P ⊢ₛ P') (hq : Q ⊢ₛ Q') : P ∧ Q ⊢ₛ P' ∧ Q' := and_intro (and_elim_l' hp) (and_elim_r' hq) +theorem and_mono_l (h : P ⊢ₛ P') : P ∧ Q ⊢ₛ P' ∧ Q := and_mono h .rfl +theorem and_mono_r (h : Q ⊢ₛ Q') : P ∧ Q ⊢ₛ P ∧ Q' := and_mono .rfl h +theorem and_congr (hp : P ⊣⊢ₛ P') (hq : Q ⊣⊢ₛ Q') : P ∧ Q ⊣⊢ₛ P' ∧ Q' := bientails.iff.mpr ⟨and_mono (bientails.mp hp) (bientails.mp hq), and_mono (bientails.mpr hp) (bientails.mpr hq)⟩ +theorem and_congr_l (hp : P ⊣⊢ₛ P') : P ∧ Q ⊣⊢ₛ P' ∧ Q := and_congr hp .rfl +theorem and_congr_r (hq : Q ⊣⊢ₛ Q') : P ∧ Q ⊣⊢ₛ P ∧ Q' := and_congr .rfl hq +theorem or_mono (hp : P ⊢ₛ P') (hq : Q ⊢ₛ Q') : P ∨ Q ⊢ₛ P' ∨ Q' := or_elim (or_intro_l' hp) (or_intro_r' hq) +theorem or_mono_l (h : P ⊢ₛ P') : P ∨ Q ⊢ₛ P' ∨ Q := or_mono h .rfl +theorem or_mono_r (h : Q ⊢ₛ Q') : P ∨ Q ⊢ₛ P ∨ Q' := or_mono .rfl h +theorem or_congr (hp : P ⊣⊢ₛ P') (hq : Q ⊣⊢ₛ Q') : P ∨ Q ⊣⊢ₛ P' ∨ Q' := bientails.iff.mpr ⟨or_mono (bientails.mp hp) (bientails.mp hq), or_mono (bientails.mpr hp) (bientails.mpr hq)⟩ +theorem or_congr_l (hp : P ⊣⊢ₛ P') : P ∨ Q ⊣⊢ₛ P' ∨ Q := or_congr hp .rfl +theorem or_congr_r (hq : Q ⊣⊢ₛ Q') : P ∨ Q ⊣⊢ₛ P ∨ Q' := or_congr .rfl hq +theorem imp_mono (h1 : Q ⊢ₛ P) (h2 : P' ⊢ₛ Q') : (P → P') ⊢ₛ Q → Q' := imp_intro <| (and_mono_r h1).trans <| (imp_elim .rfl).trans h2 +theorem imp_mono_l (h : P' ⊢ₛ P) : (P → Q) ⊢ₛ (P' → Q) := imp_mono h .rfl +theorem imp_mono_r (h : Q ⊢ₛ Q') : (P → Q) ⊢ₛ (P → Q') := imp_mono .rfl h +theorem imp_congr (h1 : P ⊣⊢ₛ Q) (h2 : P' ⊣⊢ₛ Q') : (P → P') ⊣⊢ₛ (Q → Q') := bientails.iff.mpr ⟨imp_mono h1.mpr h2.mp, imp_mono h1.mp h2.mpr⟩ +theorem imp_congr_l (h : P ⊣⊢ₛ P') : (P → Q) ⊣⊢ₛ (P' → Q) := imp_congr h .rfl +theorem imp_congr_r (h : Q ⊣⊢ₛ Q') : (P → Q) ⊣⊢ₛ (P → Q') := imp_congr .rfl h +theorem forall_mono {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊢ₛ Ψ a) : (∀ a, Φ a) ⊢ₛ ∀ a, Ψ a := forall_intro fun a => (forall_elim a).trans (h a) +theorem forall_congr {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊣⊢ₛ Ψ a) : (∀ a, Φ a) ⊣⊢ₛ ∀ a, Ψ a := bientails.iff.mpr ⟨forall_mono fun a => (h a).mp, forall_mono fun a => (h a).mpr⟩ +theorem exists_mono {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊢ₛ Ψ a) : (∃ a, Φ a) ⊢ₛ ∃ a, Ψ a := exists_elim fun a => (h a).trans (exists_intro a) +theorem exists_congr {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊣⊢ₛ Ψ a) : (∃ a, Φ a) ⊣⊢ₛ ∃ a, Ψ a := bientails.iff.mpr ⟨exists_mono fun a => (h a).mp, exists_mono fun a => (h a).mpr⟩ + +theorem and_imp (hp : P₁ ⊢ₛ P₂) (hq : Q₁ ⊢ₛ Q₂) : (P₁ ∧ Q₁) ⊢ₛ (P₂ ∧ Q₂) := and_intro (and_elim_l' hp) (and_elim_r' hq) +theorem or_imp_left (hleft : P₁ ⊢ₛ P₂) : (P₁ ∨ Q) ⊢ₛ (P₂ ∨ Q) := or_elim (or_intro_l' hleft) or_intro_r +theorem or_imp_right (hright : Q₁ ⊢ₛ Q₂) : (P ∨ Q₁) ⊢ₛ (P ∨ Q₂) := or_elim or_intro_l (or_intro_r' hright) + +/-! # Boolean algebra -/ + +theorem and_self : P ∧ P ⊣⊢ₛ P := bientails.iff.mpr ⟨and_elim_l, and_intro .rfl .rfl⟩ +theorem or_self : P ∨ P ⊣⊢ₛ P := bientails.iff.mpr ⟨or_elim .rfl .rfl, or_intro_l⟩ +theorem and_comm : P ∧ Q ⊣⊢ₛ Q ∧ P := bientails.iff.mpr ⟨and_symm, and_symm⟩ +theorem or_comm : P ∨ Q ⊣⊢ₛ Q ∨ P := bientails.iff.mpr ⟨or_symm, or_symm⟩ +theorem and_assoc : (P ∧ Q) ∧ R ⊣⊢ₛ P ∧ Q ∧ R := bientails.iff.mpr ⟨and_intro (and_elim_l' and_elim_l) (and_mono_l and_elim_r), and_intro (and_mono_r and_elim_l) (and_elim_r' and_elim_r)⟩ +theorem or_assoc : (P ∨ Q) ∨ R ⊣⊢ₛ P ∨ Q ∨ R := bientails.iff.mpr ⟨or_elim (or_mono_r or_intro_l) (or_intro_r' or_intro_r), or_elim (or_intro_l' or_intro_l) (or_mono_l or_intro_r)⟩ +theorem and_eq_right : (P ⊢ₛ Q) ↔ P ⊣⊢ₛ Q ∧ P := Iff.intro (fun h => bientails.iff.mpr ⟨and_intro h .rfl, and_elim_r⟩) (fun h => h.mp.trans and_elim_l) +theorem and_eq_left : (P ⊢ₛ Q) ↔ P ⊣⊢ₛ P ∧ Q := Iff.intro (fun h => bientails.iff.mpr ⟨and_intro .rfl h, and_elim_l⟩) (fun h => h.mp.trans and_elim_r) +theorem or_eq_left : (P ⊢ₛ Q) ↔ Q ⊣⊢ₛ Q ∨ P := Iff.intro (fun h => bientails.iff.mpr ⟨or_intro_l' .rfl, or_elim .rfl h⟩) (fun h => or_intro_r.trans h.mpr) +theorem or_eq_right : (P ⊢ₛ Q) ↔ Q ⊣⊢ₛ P ∨ Q := Iff.intro (fun h => bientails.iff.mpr ⟨or_intro_r' .rfl, or_elim h .rfl⟩) (fun h => or_intro_l.trans h.mpr) + +theorem and_or_left : P ∧ (Q ∨ R) ⊣⊢ₛ (P ∧ Q) ∨ (P ∧ R) := + bientails.iff.mpr ⟨and_or_elim_r or_intro_l or_intro_r, + or_elim (and_intro and_elim_l (or_intro_l' and_elim_r)) (and_intro and_elim_l (or_intro_r' and_elim_r))⟩ +theorem or_and_left : P ∨ (Q ∧ R) ⊣⊢ₛ (P ∨ Q) ∧ (P ∨ R) := + bientails.iff.mpr ⟨or_elim (and_intro or_intro_l or_intro_l) (and_imp or_intro_r or_intro_r), + and_or_elim_l (or_intro_l' and_elim_l) (and_or_elim_r (or_intro_l' and_elim_r) or_intro_r)⟩ +theorem or_and_right : (P ∨ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∨ (Q ∧ R) := and_comm.trans (and_or_left.trans (or_congr and_comm and_comm)) +theorem and_or_right : (P ∧ Q) ∨ R ⊣⊢ₛ (P ∨ R) ∧ (Q ∨ R) := or_comm.trans (or_and_left.trans (and_congr or_comm or_comm)) + +theorem true_and : ⌜True⌝ ∧ P ⊣⊢ₛ P := bientails.iff.mpr ⟨and_elim_r, and_intro (pure_intro trivial) .rfl⟩ +theorem and_true : P ∧ ⌜True⌝ ⊣⊢ₛ P := and_comm.trans true_and +theorem false_and : ⌜False⌝ ∧ P ⊣⊢ₛ ⌜False⌝ := bientails.iff.mpr ⟨and_elim_l, false_elim⟩ +theorem and_false : P ∧ ⌜False⌝ ⊣⊢ₛ ⌜False⌝ := and_comm.trans false_and +theorem true_or : ⌜True⌝ ∨ P ⊣⊢ₛ ⌜True⌝ := bientails.iff.mpr ⟨true_intro, or_intro_l⟩ +theorem or_true : P ∨ ⌜True⌝ ⊣⊢ₛ ⌜True⌝ := or_comm.trans true_or +theorem false_or : ⌜False⌝ ∨ P ⊣⊢ₛ P := bientails.iff.mpr ⟨or_elim false_elim .rfl, or_intro_r⟩ +theorem or_false : P ∨ ⌜False⌝ ⊣⊢ₛ P := or_comm.trans false_or + +theorem true_imp : (⌜True⌝ → P) ⊣⊢ₛ P := bientails.iff.mpr ⟨and_true.mpr.trans imp_elim_l, imp_intro and_elim_l⟩ +theorem imp_self : Q ⊢ₛ P → P := imp_intro and_elim_r +theorem imp_self_simp : (Q ⊢ₛ P → P) ↔ True := iff_true_intro SPred.imp_self +theorem imp_trans : (P → Q) ∧ (Q → R) ⊢ₛ P → R := imp_intro' <| and_assoc.mpr.trans <| (and_mono_l imp_elim_r).trans imp_elim_r +theorem false_imp : (⌜False⌝ → P) ⊣⊢ₛ ⌜True⌝ := bientails.iff.mpr ⟨true_intro, imp_intro <| and_elim_r.trans false_elim⟩ + +/-! # Pure -/ + +theorem pure_elim {φ : Prop} (h1 : Q ⊢ₛ ⌜φ⌝) (h2 : φ → Q ⊢ₛ R) : Q ⊢ₛ R := + and_self.mpr.trans <| imp_elim <| h1.trans <| pure_elim' fun h => + imp_intro' <| and_elim_l.trans (h2 h) + +theorem pure_mono {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) : ⌜φ₁⌝ ⊢ₛ (⌜φ₂⌝ : SPred σs) := pure_elim' <| pure_intro ∘ h +theorem pure_congr {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : ⌜φ₁⌝ ⊣⊢ₛ (⌜φ₂⌝ : SPred σs) := bientails.iff.mpr ⟨pure_mono h.1, pure_mono h.2⟩ + +theorem pure_elim_l {φ : Prop} (h : φ → Q ⊢ₛ R) : ⌜φ⌝ ∧ Q ⊢ₛ R := pure_elim and_elim_l <| and_elim_r' ∘ h +theorem pure_elim_r {φ : Prop} (h : φ → Q ⊢ₛ R) : Q ∧ ⌜φ⌝ ⊢ₛ R := and_comm.mp.trans (pure_elim_l h) +theorem pure_true {φ : Prop} (h : φ) : ⌜φ⌝ ⊣⊢ₛ (⌜True⌝ : SPred σs) := eq_true h ▸ .rfl +theorem pure_and {φ₁ φ₂ : Prop} : ⌜φ₁⌝ ∧ (⌜φ₂⌝ : SPred σs) ⊣⊢ₛ ⌜φ₁ ∧ φ₂⌝ := bientails.iff.mpr ⟨pure_elim and_elim_l fun h => and_elim_r' <| pure_mono <| And.intro h, and_intro (pure_mono And.left) (pure_mono And.right)⟩ +theorem pure_or {φ₁ φ₂ : Prop} : ⌜φ₁⌝ ∨ (⌜φ₂⌝ : SPred σs) ⊣⊢ₛ ⌜φ₁ ∨ φ₂⌝ := bientails.iff.mpr ⟨or_elim (pure_mono Or.inl) (pure_mono Or.inr), pure_elim' (·.elim (or_intro_l' ∘ pure_intro) (or_intro_r' ∘ pure_intro))⟩ +theorem pure_imp_2 {φ₁ φ₂ : Prop} : ⌜φ₁ → φ₂⌝ ⊢ₛ (⌜φ₁⌝ → ⌜φ₂⌝ : SPred σs) := imp_intro <| pure_and.mp.trans <| pure_mono (And.elim id) +theorem pure_imp {φ₁ φ₂ : Prop} : (⌜φ₁⌝ → ⌜φ₂⌝ : SPred σs) ⊣⊢ₛ ⌜φ₁ → φ₂⌝ := by + refine bientails.iff.mpr ⟨?_, pure_imp_2⟩ + if h : φ₁ + then exact (mp .rfl (pure_intro h)).trans (pure_mono fun h _ => h) + else exact pure_intro h.elim + +theorem pure_forall_2 {φ : α → Prop} : ⌜∀ x, φ x⌝ ⊢ₛ ∀ x, (⌜φ x⌝ : SPred σs) := forall_intro fun _ => pure_mono (· _) +theorem pure_forall {φ : α → Prop} : (∀ x, (⌜φ x⌝ : SPred σs)) ⊣⊢ₛ ⌜∀ x, φ x⌝ := by + refine bientails.iff.mpr ⟨?_, pure_forall_2⟩ + if h : ∃ x, ¬φ x + then let ⟨x, h⟩ := h + exact (forall_elim x).trans (pure_mono h.elim) + else exact pure_intro fun x => Classical.not_not.1 <| mt (⟨x, ·⟩) h + +theorem pure_exists {φ : α → Prop} : (∃ x, ⌜φ x⌝ : SPred σs) ⊣⊢ₛ ⌜∃ x, φ x⌝ := bientails.iff.mpr ⟨exists_elim fun a => pure_mono (⟨a, ·⟩), pure_elim' fun ⟨x, h⟩ => (pure_intro h).trans (exists_intro' x .rfl)⟩ + +@[simp] theorem true_intro_simp : (Q ⊢ₛ ⌜True⌝) ↔ True := iff_true_intro SPred.true_intro +@[simp] theorem true_intro_simp_nil {Q : SPred []} : (Q ⊢ₛ True) ↔ True := SPred.true_intro_simp + +/-! # Miscellaneous -/ + +theorem and_left_comm : P ∧ Q ∧ R ⊣⊢ₛ Q ∧ P ∧ R := and_assoc.symm.trans <| (and_congr_l and_comm).trans and_assoc +theorem and_right_comm : (P ∧ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∧ Q := and_assoc.trans <| (and_congr_r and_comm).trans and_assoc.symm + +/-! # Working with entailment -/ + +theorem entails_pure_intro {σs : List Type} (P Q : Prop) (h : P → Q) : SPred.entails ⌜P⌝ (σs := σs) ⌜Q⌝ := pure_elim' fun hp => pure_intro (h hp) + +@[simp] theorem entails_elim_nil (P Q : SPred []) : SPred.entails P Q ↔ P → Q := iff_of_eq rfl +theorem entails_elim_cons {σ : Type} {σs : List Type} (P Q : SPred (σ::σs)) : P ⊢ₛ Q ↔ ∀ s, (P s ⊢ₛ Q s) := by simp only [entails] +@[simp] theorem entails_pure_elim_cons {σ : Type} {σs : List Type} [Inhabited σ] (P Q : Prop) : SPred.entails ⌜P⌝ (σs := σ::σs) ⌜Q⌝ ↔ SPred.entails ⌜P⌝ (σs := σs) ⌜Q⌝:= by simp [entails] +@[simp] theorem entails_true_intro {σs : List Type} (P Q : SPred σs) : ⊢ₛ P → Q ↔ P ⊢ₛ Q := Iff.intro (fun h => (and_intro true_intro .rfl).trans (imp_elim h)) (fun h => imp_intro (and_elim_r.trans h)) diff --git a/src/Std/Do/SPred/Laws.lean b/src/Std/Do/SPred/Laws.lean new file mode 100644 index 0000000000..4e1c63e0ae --- /dev/null +++ b/src/Std/Do/SPred/Laws.lean @@ -0,0 +1,130 @@ +/- +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, Mario Carneiro, Sebastian Graf +-/ +prelude +import Std.Do.SPred.Notation + +namespace Std.Do.SPred + +/-! +# Laws of `SPred` + +This module contains lemmas about `SPred` that need to be proved by induction on σs. +That is, they need to proved by appealing to the model of `SPred` and cannot +be derived without doing so. + +`Std.Do.SPred.DerivedLaws` has some more laws that are derivative of what follows. +-/ + +/-! # Entailment -/ + +@[refl,simp] +theorem entails.refl {σs : List Type} (P : SPred σs) : P ⊢ₛ P := by + match σs with + | [] => simp [entails] + | σ :: _ => intro s; exact entails.refl (P s) + +theorem entails.trans {σs : List Type} {P Q R : SPred σs} : (P ⊢ₛ Q) → (Q ⊢ₛ R) → (P ⊢ₛ R) := by + match σs with + | [] => intro h₁ h₂; exact h₂ ∘ h₁ + | σ :: _ => intro h₁ h₂; intro s; exact entails.trans (h₁ s) (h₂ s) + +instance {σs : List Type} : Trans (@entails σs) entails entails where + trans := entails.trans + +/-! # Bientailment -/ + +theorem bientails.iff {σs : List Type} {P Q : SPred σs} : P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P) := by + induction σs with + | nil => exact Iff.intro (fun h => ⟨h.mp, h.mpr⟩) (fun h => ⟨h.1, h.2⟩) + | cons σ σs ih => + apply Iff.intro + · exact fun h => ⟨fun s => (ih.mp (h s)).1, fun s => (ih.mp (h s)).2⟩ + · intro h s; exact ih.mpr ⟨h.1 s, h.2 s⟩ + +@[refl,simp] +theorem bientails.refl {σs : List Type} (P : SPred σs) : P ⊣⊢ₛ P := by + induction σs <;> simp [bientails, *] + +theorem bientails.trans {σs : List Type} {P Q R : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ R) → (P ⊣⊢ₛ R) := by + induction σs + case nil => simp +contextual only [bientails, implies_true] + case cons σ σs ih => intro hpq hqr s; exact ih (hpq s) (hqr s) + +instance {σs : List Type} : Trans (@bientails σs) bientails bientails where + trans := bientails.trans + +theorem bientails.symm {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ P) := by + induction σs + case nil => exact Iff.symm + case cons σ σs ih => intro h s; exact ih (h s) + +theorem bientails.to_eq {σs : List Type} {P Q : SPred σs} (h : P ⊣⊢ₛ Q) : P = Q := by + induction σs + case nil => rw[iff_iff_eq.mp h] + case cons σ σs ih => + ext s; rw[ih (h s)] + +/-! # Pure -/ + +theorem pure_intro {σs : List Type} {φ : Prop} {P : SPred σs} : φ → P ⊢ₛ ⌜φ⌝ := by + induction σs <;> simp_all [entails] + +theorem pure_elim' {σs : List Type} {φ : Prop} {P : SPred σs} : (φ → ⌜True⌝ ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P := by + induction σs <;> simp_all [entails] + +-- Ideally, we'd like to prove the following theorem: +-- theorem pure_elim' {σs : List Type} {φ : Prop} : SPred.entails (σs:=σs) ⌜True⌝ ⌜φ⌝ → φ +-- Unfortunately, this is only true if all `σs` are Inhabited. + +/-! # Conjunction -/ + +theorem and_intro {σs : List Type} {P Q R : SPred σs} (h1 : P ⊢ₛ Q) (h2 : P ⊢ₛ R) : P ⊢ₛ Q ∧ R := by + induction σs <;> simp_all [entails] + +theorem and_elim_l {P Q : SPred σs} : P ∧ Q ⊢ₛ P := by + induction σs <;> simp_all [entails] + +theorem and_elim_r {P Q : SPred σs} : P ∧ Q ⊢ₛ Q := by + induction σs <;> simp_all [entails] + +/-! # Disjunction -/ + +theorem or_intro_l {σs : List Type} {P Q : SPred σs} : P ⊢ₛ P ∨ Q := by + induction σs <;> simp_all [entails] + +theorem or_intro_r {σs : List Type} {P Q : SPred σs} : Q ⊢ₛ P ∨ Q := by + induction σs <;> simp_all [entails] + +theorem or_elim {σs : List Type} {P Q R : SPred σs} (h1 : P ⊢ₛ R) (h2 : Q ⊢ₛ R) : P ∨ Q ⊢ₛ R := by + induction σs + case nil => exact (Or.elim · h1 h2) + case cons => simp_all [entails] + +/-! # Implication -/ + +theorem imp_intro {σs : List Type} {P Q R : SPred σs} (h : P ∧ Q ⊢ₛ R) : P ⊢ₛ Q → R := by + induction σs <;> simp_all [entails] + +theorem imp_elim {σs : List Type} {P Q R : SPred σs} (h : P ⊢ₛ Q → R) : P ∧ Q ⊢ₛ R := by + induction σs <;> simp_all [entails] + +/-! # Quantifiers -/ + +theorem forall_intro {σs : List Type} {P : SPred σs} {Ψ : α → SPred σs} (h : ∀ a, P ⊢ₛ Ψ a) : P ⊢ₛ ∀ a, Ψ a := by + induction σs <;> simp_all [entails] + +theorem forall_elim {σs : List Type} {Ψ : α → SPred σs} (a : α) : (∀ a, Ψ a) ⊢ₛ Ψ a := by + induction σs <;> simp_all [entails] + +theorem exists_intro {σs : List Type} {Ψ : α → SPred σs} (a : α) : Ψ a ⊢ₛ ∃ a, Ψ a := by + induction σs + case nil => intro _; exists a + case cons σ σs ih => intro s; exact @ih (fun a => Ψ a s) + +theorem exists_elim {σs : List Type} {Φ : α → SPred σs} {Q : SPred σs} (h : ∀ a, Φ a ⊢ₛ Q) : (∃ a, Φ a) ⊢ₛ Q := by + induction σs + case nil => intro ⟨a, ha⟩; exact h a ha + case cons σ σs ih => intro s; exact ih (fun a => h a s) diff --git a/src/Std/Do/SPred/Notation.lean b/src/Std/Do/SPred/Notation.lean new file mode 100644 index 0000000000..5f4d6f4161 --- /dev/null +++ b/src/Std/Do/SPred/Notation.lean @@ -0,0 +1,175 @@ +/- +Copyright (c) 2022 Lars König. All rights reserved. +Released under Apache 2.0 license. +Authors: Lars König, Sebastian Graf +-/ +prelude +import Std.Do.SPred.SPred + +namespace Std.Do.SPred.Notation + +open Lean Macro Parser PrettyPrinter + +-- define `spred` embedding in `term`. +-- An explicit `spred` marker avoids exponential blowup in terms +-- that do not opt into the extended syntax. +syntax:max "spred(" term ")" : term +syntax:max "term(" term ")" : term + +-- allow fallback to `term` +macro_rules + | `(spred(term($t))) => pure t + | `(spred($t)) => pure t + +-- push `spred` inside some `term` constructs +macro_rules + | `(spred(($P))) => ``((spred($P))) + | `(spred(fun $xs* => $b)) => ``(fun $xs* => spred($b)) + | `(spred(if $c then $t else $e)) => ``(if $c then spred($t) else spred($e)) + | `(spred(($P : $t))) => ``((spred($P) : $t)) + +/-- Remove an `spred` layer from a `term` syntax object. -/ +-- inverts the rules above. +partial def unpack [Monad m] [MonadRef m] [MonadQuotation m] : Term → m Term + | `(spred($P)) => do `($P) + | `(($P)) => do `(($(← unpack P))) + | `(if $c then $t else $e) => do + let t ← unpack t + let e ← unpack e + `(if $c then $t else $e) + | `(fun $xs* => $b) => do + let b ← unpack b + `(fun $xs* => $b) + | `(($P : $t)) => do ``(($(← unpack P) : $t)) + | `($t) => `($t) + +/-! # Idiom notation -/ + +/-- Embedding of pure Lean values into `SVal`. -/ +syntax "⌜" term "⌝" : term +/-- ‹t› in `SVal` idiom notation. Accesses the state of type `t`. -/ +syntax "‹" term "›ₛ" : term +/-- + Use getter `t : SVal σs σ` in `SVal` idiom notation; sugar for `SVal.uncurry t (by assumption)`. +-/ +syntax:max "#" term:max : term + +/-! # Sugar for `SPred` -/ + +/-- Entailment in `SPred`; sugar for `SPred.entails`. -/ +syntax:25 term:26 " ⊢ₛ " term:25 : term +/-- Tautology in `SPred`; sugar for `SPred.entails ⌜True⌝`. -/ +syntax:25 "⊢ₛ " term:25 : term +/-- Bi-entailment in `SPred`; sugar for `SPred.bientails`. -/ +syntax:25 term:25 " ⊣⊢ₛ " term:25 : term + +macro_rules + | `(⌜$t⌝) => ``(SVal.curry (fun tuple => $t)) + | `(#$t) => `(SVal.uncurry $t (by assumption)) + | `(‹$t›ₛ) => `(#(SVal.getThe $t)) + | `($P ⊢ₛ $Q) => ``(SPred.entails spred($P) spred($Q)) + | `(spred($P ∧ $Q)) => ``(SPred.and spred($P) spred($Q)) + | `(spred($P ∨ $Q)) => ``(SPred.or spred($P) spred($Q)) + | `(spred(¬ $P)) => ``(SPred.not spred($P)) + | `(spred($P → $Q)) => ``(SPred.imp spred($P) spred($Q)) + | `(spred($P ↔ $Q)) => ``(SPred.iff spred($P) spred($Q)) + | `(spred(∃ $xs:explicitBinders, $P)) => do expandExplicitBinders ``SPred.exists xs (← `(spred($P))) + | `(⊢ₛ $P) => ``(SPred.entails ⌜True⌝ spred($P)) + | `($P ⊣⊢ₛ $Q) => ``(SPred.bientails spred($P) spred($Q)) + -- Sadly, ∀ does not resently use expandExplicitBinders... + | `(spred(∀ _%$tk, $P)) => ``(SPred.forall (fun _%$tk => spred($P))) + | `(spred(∀ _%$tk : $ty, $P)) => ``(SPred.forall (fun _%$tk : $ty => spred($P))) + | `(spred(∀ (_%$tk $xs* : $ty), $P)) => ``(SPred.forall (fun _%$tk : $ty => spred(∀ ($xs* : $ty), $P))) + | `(spred(∀ $x:ident, $P)) => ``(SPred.forall (fun $x => spred($P))) + | `(spred(∀ ($x:ident : $ty), $P)) => ``(SPred.forall (fun $x : $ty => spred($P))) + | `(spred(∀ ($x:ident $xs* : $ty), $P)) => ``(SPred.forall (fun $x : $ty => spred(∀ ($xs* : $ty), $P))) + | `(spred(∀ $x:ident $xs*, $P)) => ``(SPred.forall (fun $x => spred(∀ $xs*, $P))) + | `(spred(∀ ($x:ident : $ty) $xs*, $P)) => ``(SPred.forall (fun $x : $ty => spred(∀ $xs*, $P))) + | `(spred(∀ ($x:ident $xs* : $ty) $ys*, $P)) => ``(SPred.forall (fun $x : $ty => spred(∀ ($xs* : $ty) $ys*, $P))) + +@[app_unexpander SVal.curry] +private def unexpandCurry : Unexpander + | `($_ $t $ts*) => do + match t with + | `(fun $_ => $e) => if ts.isEmpty then ``(⌜$e⌝) else ``(⌜$e⌝ $ts*) + | _ => throw () + | _ => throw () + +@[app_unexpander SVal.uncurry] +private def unexpandUncurry : Unexpander + | `($_ $f $ts*) => do + match f with + | `(SVal.getThe $t) => if ts.isEmpty then ``(‹$t›ₛ) else ``(‹$t›ₛ $ts*) + | `($t) => if ts.isEmpty then ``(#$t) else ``(#$t $ts*) + | _ => throw () + +@[app_unexpander SPred.entails] +private def unexpandEntails : Unexpander + | `($_ $P $Q) => do + let P ← unpack P; let Q ← unpack Q; + match P with + | `(⌜True⌝) => ``(⊢ₛ $Q) + | _ => ``($P ⊢ₛ $Q) + | _ => throw () + +@[app_unexpander SPred.bientails] +private def unexpandBientails : Unexpander + | `($_ $P $Q) => do + let P ← unpack P; let Q ← unpack Q; + ``($P ⊣⊢ₛ $Q) + | _ => throw () + +@[app_unexpander SPred.and] +private def unexpandAnd : Unexpander + | `($_ $P $Q) => do + let P ← unpack P; let Q ← unpack Q; + ``(spred($P ∧ $Q)) + | _ => throw () + +@[app_unexpander SPred.or] +private def unexpandOr : Unexpander + | `($_ $P $Q) => do + let P ← unpack P; let Q ← unpack Q; + ``(spred($P ∨ $Q)) + | _ => throw () + +@[app_unexpander SPred.not] +private def unexpandNot : Unexpander + | `($_ $P) => do + let P ← unpack P; + ``(spred(¬ $P)) + | _ => throw () + +@[app_unexpander SPred.imp] +private def unexpandImp : Unexpander + | `($_ $P $Q) => do + let P ← unpack P; let Q ← unpack Q; + ``(spred($P → $Q)) + | _ => throw () + +@[app_unexpander SPred.forall] +private def unexpandForall : Unexpander + | `($_ fun $x:ident => ∀ $y:ident $[$z:ident]*, $Ψ) => do + let Ψ ← unpack Ψ + ``(spred(∀ $x:ident $y:ident $[$z:ident]*, $Ψ)) + | `($_ fun $x:ident => $Ψ) => do + let Ψ ← unpack Ψ + ``(spred(∀ $x:ident, $Ψ)) + | _ => throw () + +@[app_unexpander SPred.exists] +private def unexpandExists : Unexpander + | `($_ fun $x:ident => ∃ $y:ident $[$z:ident]*, $Ψ) => do + let Ψ ← unpack Ψ + ``(spred(∃ $x:ident $y:ident $[$z:ident]*, $Ψ)) + | `($_ fun $x:ident => $Ψ) => do + let Ψ ← unpack Ψ + ``(spred(∃ $x:ident, $Ψ)) + | _ => throw () + +@[app_unexpander SPred.iff] +private def unexpandIff : Unexpander + | `($_ $P $Q) => do + let P ← unpack P; let Q ← unpack Q; + ``(spred($P ↔ $Q)) + | _ => throw () diff --git a/src/Std/Do/SPred/SPred.lean b/src/Std/Do/SPred/SPred.lean new file mode 100644 index 0000000000..b3bbf892ea --- /dev/null +++ b/src/Std/Do/SPred/SPred.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Init.Ext +import Std.Do.SPred.SVal + +/-! +# State-indexed predicates + +This module provides a type `SPred σs` of predicates indexed by a list of states. +This type forms the basis for the notion of assertion in `Std.Do`; see `Std.Do.Assertion`. +-/ + +namespace Std.Do + +/-- + A predicate indexed by a list of states. + ``` + example : SPred [Nat, Bool] = (Nat → Bool → Prop) := rfl + ``` +-/ +abbrev SPred (σs : List Type) : Type := SVal σs Prop + +namespace SPred + +/-- A pure proposition `P : Prop` embedded into `SPred`. For internal use in this module only; prefer to use idiom bracket notation `⌜P⌝. -/ +private abbrev pure {σs : List Type} (P : Prop) : SPred σs := SVal.curry (fun _ => P) + +@[ext] +theorem ext {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, P s = Q s) → P = Q := funext + +/-- Entailment in `SPred`. -/ +def entails {σs : List Type} (P Q : SPred σs) : Prop := match σs with +| [] => P → Q +| σ :: _ => ∀ (s : σ), entails (P s) (Q s) +@[simp] theorem entails_nil {P Q : SPred []} : entails P Q = (P → Q) := rfl +theorem entails_cons {σs : List Type} {P Q : SPred (σ::σs)} : entails P Q = (∀ s, entails (P s) (Q s)) := rfl +theorem entails_cons_intro {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, entails (P s) (Q s)) → entails P Q := by simp only [entails, imp_self] + +-- Reducibility of entails must be semi-reducible so that entails_refl is useful for rfl + +/-- Equivalence relation on `SPred`. Convert to `Eq` via `bientails.to_eq`. -/ +def bientails {σs : List Type} (P Q : SPred σs) : Prop := match σs with +| [] => P ↔ Q +| σ :: _ => ∀ (s : σ), bientails (P s) (Q s) +@[simp] theorem bientails_nil {P Q : SPred []} : bientails P Q = (P ↔ Q) := rfl +theorem bientails_cons {σs : List Type} {P Q : SPred (σ::σs)} : bientails P Q = (∀ s, bientails (P s) (Q s)) := rfl +theorem bientails_cons_intro {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, bientails (P s) (Q s)) → bientails P Q := by simp only [bientails, imp_self] + +/-- Conjunction in `SPred`. -/ +def and {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with +| [] => P ∧ Q +| σ :: _ => fun (s : σ) => and (P s) (Q s) +@[simp] theorem and_nil {P Q : SPred []} : and P Q = (P ∧ Q) := rfl +@[simp] theorem and_cons {σs : List Type} {P Q : SPred (σ::σs)} : and P Q s = and (P s) (Q s) := rfl + +/-- Disjunction in `SPred`. -/ +def or {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with +| [] => P ∨ Q +| σ :: _ => fun (s : σ) => or (P s) (Q s) +@[simp] theorem or_nil {P Q : SPred []} : or P Q = (P ∨ Q) := rfl +@[simp] theorem or_cons {σs : List Type} {P Q : SPred (σ::σs)} : or P Q s = or (P s) (Q s) := rfl + +/-- Negation in `SPred`. -/ +def not {σs : List Type} (P : SPred σs) : SPred σs := match σs with +| [] => ¬ P +| σ :: _ => fun (s : σ) => not (P s) +@[simp] theorem not_nil {P : SPred []} : not P = (¬ P) := rfl +@[simp] theorem not_cons {σs : List Type} {P : SPred (σ::σs)} : not P s = not (P s) := rfl + +/-- Implication in `SPred`. -/ +def imp {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with +| [] => P → Q +| σ :: _ => fun (s : σ) => imp (P s) (Q s) +@[simp] theorem imp_nil {P Q : SPred []} : imp P Q = (P → Q) := rfl +@[simp] theorem imp_cons {σs : List Type} {P Q : SPred (σ::σs)} : imp P Q s = imp (P s) (Q s) := rfl + +/-- Biconditional in `SPred`. -/ +def iff {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with +| [] => P ↔ Q +| σ :: _ => fun (s : σ) => iff (P s) (Q s) +@[simp] theorem iff_nil {P Q : SPred []} : iff P Q = (P ↔ Q) := rfl +@[simp] theorem iff_cons {σs : List Type} {P Q : SPred (σ::σs)} : iff P Q s = iff (P s) (Q s) := rfl + +/-- Existential quantifier in `SPred`. -/ +def «exists» {α} {σs : List Type} (P : α → SPred σs) : SPred σs := match σs with +| [] => ∃ a, P a +| σ :: _ => fun (s : σ) => «exists» (fun a => P a s) +@[simp] theorem exists_nil {α} {P : α → SPred []} : «exists» P = (∃ a, P a) := rfl +@[simp] theorem exists_cons {σs : List Type} {α} {P : α → SPred (σ::σs)} : «exists» P s = «exists» (fun a => P a s) := rfl + +/-- Universal quantifier in `SPred`. -/ +def «forall» {α} {σs : List Type} (P : α → SPred σs) : SPred σs := match σs with +| [] => ∀ a, P a +| σ :: _ => fun (s : σ) => «forall» (fun a => P a s) +@[simp] theorem forall_nil {α} {P : α → SPred []} : «forall» P = (∀ a, P a) := rfl +@[simp] theorem forall_cons {σs : List Type} {α} {P : α → SPred (σ::σs)} : «forall» P s = «forall» (fun a => P a s) := rfl + +/-- Conjunction of a list of `SPred`. -/ +def conjunction {σs : List Type} (env : List (SPred σs)) : SPred σs := match env with +| [] => pure True +| P::env => P.and (conjunction env) +@[simp] theorem conjunction_nil {σs : List Type} : conjunction ([] : List (SPred σs)) = pure True := rfl +@[simp] theorem conjunction_cons {σs : List Type} {P : SPred σs} {env : List (SPred σs)} : conjunction (P::env) = P.and (conjunction env) := rfl +@[simp] theorem conjunction_apply {σs : List Type} {env : List (SPred (σ::σs))} : conjunction env s = conjunction (env.map (· s)) := by + induction env <;> simp [conjunction, *] diff --git a/src/Std/Do/SPred/SVal.lean b/src/Std/Do/SPred/SVal.lean new file mode 100644 index 0000000000..8dd2f97f7c --- /dev/null +++ b/src/Std/Do/SPred/SVal.lean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Init.Data.List.Notation + +/-! # State-indexed values -/ + +namespace Std.Do + +/-- + A value indexed by a curried tuple of states. + ``` + example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl + ``` +-/ +abbrev SVal (σs : List Type) (α : Type) := match σs with +| [] => α +| σ :: σs => σ → SVal σs α +/- Note about the reducibility of SVal: +We need SVal to be reducible, otherwise type inference fails for `Triple`. +(Begs for investigation.) +-/ + +namespace SVal + +/-- A tuple capturing the whole state of an `SVal`. -/ +def StateTuple (σs : List Type) := match σs with +| [] => Unit +| σ :: σs => σ × StateTuple σs + +instance : Inhabited (StateTuple []) where + default := () + +instance [Inhabited σ] [Inhabited (StateTuple σs)] : Inhabited (StateTuple (σ :: σs)) where + default := (default, default) + +/-- Curry a function taking a `StateTuple` into an `SVal`. -/ +def curry {σs : List Type} (f : StateTuple σs → α) : SVal σs α := match σs with +| [] => f () +| _ :: _ => fun s => curry (fun s' => f (s, s')) +@[simp] theorem curry_nil {f : StateTuple [] → α} : curry f = f () := rfl +@[simp] theorem curry_cons {σ : Type} {σs : List Type} {f : StateTuple (σ::σs) → α} {s : σ} : curry f s = curry (fun s' => f (s, s')) := rfl + +/-- Uncurry an `SVal` into a function taking a `StateTuple`. -/ +def uncurry {σs : List Type} (f : SVal σs α) : StateTuple σs → α := match σs with +| [] => fun _ => f +| _ :: _ => fun (s, t) => uncurry (f s) t +@[simp] theorem uncurry_nil {σ : Type} {s : σ} : uncurry (σs:=[]) s = fun _ => s := rfl +@[simp] theorem uncurry_cons {σ : Type} {σs : List Type} {f : SVal (σ::σs) α} {s : σ} {t : StateTuple σs} : uncurry f (s, t) = uncurry (f s) t := rfl + +@[simp] theorem uncurry_curry {σs : List Type} {f : StateTuple σs → α} : uncurry (σs:=σs) (curry f) = f := by induction σs <;> (simp[uncurry, curry, *]; rfl) +@[simp] theorem curry_uncurry {σs : List Type} {f : SVal σs α} : curry (σs:=σs) (uncurry f) = f := by induction σs <;> simp[uncurry, curry, *] + +/-- Embed a pure value into an `SVal`. -/ +abbrev pure {σs : List Type} (a : α) : SVal σs α := curry (fun _ => a) + +instance [Inhabited α] : Inhabited (SVal σs α) where + default := pure default + +class GetTy (σ : Type) (σs : List Type) where + get : SVal σs σ + +instance : GetTy σ (σ :: σs) where + get := fun s => pure s + +instance [GetTy σ₁ σs] : GetTy σ₁ (σ₂ :: σs) where + get := fun _ => GetTy.get + +/-- Get the top-most state of type `σ` from an `SVal`. -/ +def getThe {σs : List Type} (σ : Type) [GetTy σ σs] : SVal σs σ := GetTy.get +@[simp] theorem getThe_here {σs : List Type} (σ : Type) (s : σ) : getThe (σs := σ::σs) σ s = pure s := rfl +@[simp] theorem getThe_there {σs : List Type} [GetTy σ σs] (σ' : Type) (s : σ') : getThe (σs := σ'::σs) σ s = getThe (σs := σs) σ := rfl diff --git a/src/Std/Tactic.lean b/src/Std/Tactic.lean index b2a31e3249..58d849a561 100644 --- a/src/Std/Tactic.lean +++ b/src/Std/Tactic.lean @@ -5,6 +5,7 @@ Authors: Henrik Böving -/ prelude import Std.Tactic.BVDecide +import Std.Tactic.Do /-! This directory is mainly used for bootstrapping reasons. Suppose a tactic generates a proof term diff --git a/src/Std/Tactic/Do.lean b/src/Std/Tactic/Do.lean new file mode 100644 index 0000000000..8284fd5e37 --- /dev/null +++ b/src/Std/Tactic/Do.lean @@ -0,0 +1,13 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Std.Tactic.Do.Syntax + +/-! +This directory contains the syntax definition for tactics related to the proof mode of `Std.Do.SPred`. +Their builtin implementation lives in `Lean.Elab.Tactic.Do` to enable using the tactics without +importing `Lean`. +-/ diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean new file mode 100644 index 0000000000..500176a88b --- /dev/null +++ b/src/Std/Tactic/Do/Syntax.lean @@ -0,0 +1,154 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +prelude +import Init.NotationExtra + +namespace Lean.Parser.Tactic + +@[inherit_doc Lean.Parser.Tactic.massumptionMacro] +syntax (name := massumption) "massumption" : tactic + +@[inherit_doc Lean.Parser.Tactic.mclearMacro] +syntax (name := mclear) "mclear" colGt ident : tactic + +@[inherit_doc Lean.Parser.Tactic.mconstructorMacro] +syntax (name := mconstructor) "mconstructor" : tactic + +@[inherit_doc Lean.Parser.Tactic.mexactMacro] +syntax (name := mexact) "mexact" colGt term : tactic + +@[inherit_doc Lean.Parser.Tactic.mexfalsoMacro] +syntax (name := mexfalso) "mexfalso" : tactic + +@[inherit_doc Lean.Parser.Tactic.mexistsMacro] +syntax (name := mexists) "mexists" term,+ : tactic + +@[inherit_doc Lean.Parser.Tactic.mframeMacro] +syntax (name := mframe) "mframe" : tactic + +/-- Duplicate a stateful `Std.Do.SPred` hypothesis. -/ +syntax (name := mdup) "mdup" ident " => " ident : tactic + +@[inherit_doc Lean.Parser.Tactic.mhaveMacro] +syntax (name := mhave) "mhave" ident optional(":" term) " := " term : tactic + +@[inherit_doc Lean.Parser.Tactic.mreplaceMacro] +syntax (name := mreplace) "mreplace" ident optional(":" term) " := " term : tactic + +@[inherit_doc Lean.Parser.Tactic.mrightMacro] +syntax (name := mright) "mright" : tactic + +@[inherit_doc Lean.Parser.Tactic.mleftMacro] +syntax (name := mleft) "mleft" : tactic + +@[inherit_doc Lean.Parser.Tactic.mpureMacro] +syntax (name := mpure) "mpure" colGt ident : tactic + +@[inherit_doc Lean.Parser.Tactic.mpureIntroMacro] +syntax (name := mpureIntro) "mpure_intro" : tactic + +@[inherit_doc Lean.Parser.Tactic.mrevertMacro] +syntax (name := mrevert) "mrevert" colGt ident : tactic + +@[inherit_doc Lean.Parser.Tactic.mspecializeMacro] +syntax (name := mspecialize) "mspecialize" ident (colGt term:max)* : tactic + +@[inherit_doc Lean.Parser.Tactic.mspecializePureMacro] +syntax (name := mspecializePure) "mspecialize_pure" term (colGt term:max)* " => " ident : tactic + +@[inherit_doc Lean.Parser.Tactic.mstartMacro] +syntax (name := mstart) "mstart" : tactic + +@[inherit_doc Lean.Parser.Tactic.mstopMacro] +syntax (name := mstop) "mstop" : tactic + +declare_syntax_cat mcasesPat +syntax mcasesPatAlts := sepBy1(mcasesPat, " | ") +syntax binderIdent : mcasesPat +syntax "-" : mcasesPat +syntax "⟨" mcasesPatAlts,* "⟩" : mcasesPat +syntax "(" mcasesPatAlts ")" : mcasesPat +syntax "⌜" binderIdent "⌝" : mcasesPat +syntax "□" binderIdent : mcasesPat + +macro "%" h:binderIdent : mcasesPat => `(mcasesPat| ⌜$h⌝) +macro "#" h:binderIdent : mcasesPat => `(mcasesPat| □ $h) + +inductive MCasesPat + | one (name : TSyntax ``binderIdent) + | clear + | tuple (args : List MCasesPat) + | alts (args : List MCasesPat) + | pure (h : TSyntax ``binderIdent) + | stateful (h : TSyntax ``binderIdent) + deriving Repr, Inhabited + +partial def MCasesPat.parse (pat : TSyntax `mcasesPat) : MacroM MCasesPat := do + match go ⟨← expandMacros pat⟩ with + | none => Macro.throwUnsupported + | some pat => return pat +where + go : TSyntax `mcasesPat → Option MCasesPat + | `(mcasesPat| $name:binderIdent) => some <| .one name + | `(mcasesPat| -) => some <| .clear + | `(mcasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.tuple ·.toList) + | `(mcasesPat| ⌜$h⌝) => some (.pure h) + | `(mcasesPat| □$h) => some (.stateful h) + | `(mcasesPat| ($pat)) => goAlts pat + | _ => none + goAlts : TSyntax ``mcasesPatAlts → Option MCasesPat + | `(mcasesPatAlts| $args|*) => + match args.getElems with + | #[arg] => go arg + | args => args.mapM go |>.map (.alts ·.toList) + | _ => none + +@[inherit_doc Lean.Parser.Tactic.mcasesMacro] +syntax (name := mcases) "mcases" ident " with " mcasesPat : tactic + +declare_syntax_cat mrefinePat +syntax binderIdent : mrefinePat +syntax mrefinePats := sepBy1(mrefinePat, ", ") +syntax "⟨" mrefinePats "⟩" : mrefinePat +syntax "(" mrefinePat ")" : mrefinePat +syntax "⌜" term "⌝" : mrefinePat +syntax "□" binderIdent : mrefinePat +syntax "?" binderIdent : mrefinePat + +macro "%" h:term : mrefinePat => `(mrefinePat| ⌜$h⌝) +macro "#" h:binderIdent : mrefinePat => `(mrefinePat| □ $h) + +inductive MRefinePat + | one (name : TSyntax ``binderIdent) + | tuple (args : List MRefinePat) + | pure (h : TSyntax `term) + | stateful (h : TSyntax ``binderIdent) + | hole (name : TSyntax ``binderIdent) + deriving Repr, Inhabited + +partial def MRefinePat.parse (pat : TSyntax `mrefinePat) : MacroM MRefinePat := do + match go ⟨← expandMacros pat⟩ with + | none => Macro.throwUnsupported + | some pat => return pat +where + go : TSyntax `mrefinePat → Option MRefinePat + | `(mrefinePat| $name:binderIdent) => some <| .one name + | `(mrefinePat| ?$name) => some (.hole name) + | `(mrefinePat| ⟨$[$args],*⟩) => args.mapM go |>.map (.tuple ·.toList) + | `(mrefinePat| ⌜$h⌝) => some (.pure h) + | `(mrefinePat| □$h) => some (.stateful h) + | `(mrefinePat| ($pat)) => go pat + | _ => none + +@[inherit_doc Lean.Parser.Tactic.mrefineMacro] +syntax (name := mrefine) "mrefine" mrefinePat : tactic + +declare_syntax_cat mintroPat +syntax mcasesPat : mintroPat +syntax "∀" binderIdent : mintroPat + +@[inherit_doc Lean.Parser.Tactic.mintroMacro] +syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic diff --git a/tests/lean/run/spredProofMode.lean b/tests/lean/run/spredProofMode.lean new file mode 100644 index 0000000000..b38629631a --- /dev/null +++ b/tests/lean/run/spredProofMode.lean @@ -0,0 +1,298 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +import Lean.Elab.Tactic.Do +import Std.Do + +open Std.Do + +variable (σs : List Type) + +theorem start_stop (Q : SPred σs) (H : Q ⊢ₛ Q) : Q ⊢ₛ Q := by + mstart + mintro HQ + mstop + exact H + +theorem exact (Q : SPred σs) : Q ⊢ₛ Q := by + mstart + mintro HQ + mexact HQ + +theorem exact_pure (P Q : SPred σs) (hP : ⊢ₛ P): Q ⊢ₛ P := by + mintro _ + mexact hP + +theorem clear (P Q : SPred σs) : P ⊢ₛ Q → Q := by + mintro HP + mintro HQ + mclear HP + mexact HQ + +theorem assumption (P Q : SPred σs) : Q ⊢ₛ P → Q := by + mintro _ _ + massumption + +theorem assumption_pure (P Q : SPred σs) (hP : ⊢ₛ P): Q ⊢ₛ P := by + mintro _ + massumption + +namespace pure + +theorem move (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by + mintro Hφ + mpure Hφ + mexact (ψ Hφ) + +theorem move_multiple (Q : SPred σs) : ⌜φ₁⌝ ⊢ₛ ⌜φ₂⌝ → Q → Q := by + mintro Hφ1 + mintro Hφ2 + mintro HQ + mpure Hφ1 + mpure Hφ2 + mexact HQ + +theorem move_conjunction (Q : SPred σs) : (⌜φ₁⌝ ∧ ⌜φ₂⌝) ⊢ₛ Q → Q := by + mintro Hφ + mintro HQ + mpure Hφ + mexact HQ + +end pure + +namespace pureintro + +theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by + mpure_intro + exact True.intro + +theorem or : ⊢ₛ ⌜True⌝ ∨ (⌜False⌝ : SPred σs) := by + mpure_intro + left + exact True.intro + +theorem with_proof (H : A → B) (P Q : SPred σs) : P ⊢ₛ Q → ⌜A⌝ → ⌜B⌝ := by + mintro _HP _HQ + mpure_intro + exact H + +end pureintro + +namespace frame + +theorem move (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by + mintro _ + mframe + mcases h with hP + mexact h + +theorem move_multiple (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by + mintro h + mcases h with ⟨hp, hQ, hq, rest⟩ + mframe + mexact hQ + +end frame + +theorem revert (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ R := by + mintro ⟨HP, HQ, HR⟩ + mrevert HR + mrevert HP + mintro HP' + mintro HR' + mexact HR' + +namespace constructor + +theorem and (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by + mintro HQ + mconstructor <;> mexact HQ + +end constructor + +theorem exfalso (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by + mintro HP + mexfalso + mexact HP + +namespace leftright + +theorem left (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by + mintro HP + mleft + mexact HP + +theorem right (P Q : SPred σs) : Q ⊢ₛ P ∨ Q := by + mintro HQ + mright + mexact HQ + +theorem complex (P Q R : SPred σs) : ⊢ₛ P → Q → P ∧ (R ∨ Q ∨ R) := by + mintro HP HQ + mconstructor + · massumption + mright + mleft + mexact HQ + +end leftright + +namespace specialize + +theorem simple (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by + mintro HP HPQ + mspecialize HPQ HP + mexact HPQ + +theorem multiple (P Q R : SPred σs) : ⊢ₛ P → Q → (P → Q → R) → R := by + mintro HP HQ HPQR + mspecialize HPQR HP HQ + mexact HPQR + +theorem pure_imp (P Q R : SPred σs) : (⊢ₛ P) → ⊢ₛ Q → (P → Q → R) → R := by + intro HP + mintro HQ HPQR + mspecialize HPQR HP HQ + mexact HPQR + +theorem forall' (y : Nat) (Q : Nat → SPred σs) : ⊢ₛ (∀ x, Q x) → Q (y + 1) := by + mintro HQ + mspecialize HQ (y + 1) + mexact HQ + +theorem mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by + mintro HQ HΨ + mspecialize HΨ (y + 1) hP HQ + mexact HΨ + +theorem pure_mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by + mintro HQ + mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ + mexact HΨ + +theorem pure_with_local (P : SPred σs) (hc : c) : (⌜c⌝ → P) ⊢ₛ P := by + mintro HP + mspecialize HP hc + mexact HP + +end specialize + +namespace havereplace + +theorem mrepl (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by + mintro HP HPQ + mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ + mexact HPQ + +theorem mhave (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by + mintro HP HPQ + mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ + mhave HQ := by mspecialize HPQ HP; mexact HPQ + mexact HQ + +theorem mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by + mintro HQ HΨ + mhave H := by mspecialize HΨ (y + 1) hP HQ; mexact HΨ + mexact H + +end havereplace + +namespace cases + +theorem rename (P : SPred σs) : P ⊢ₛ P := by + mintro HP + mcases HP with HP' + mexact HP' + +theorem clear (P Q : SPred σs) : ⊢ₛ P → Q → P := by + mintro HP HQ + mcases HQ with - + mexact HP + +theorem pure (P : SPred σs) (Q : Prop) : φ → (⊢ₛ P → ⌜Q⌝ → P) := by + intro hφ + mintro HP HQ + mcases HQ with ⌜hQ⌝ + mexact HP + +theorem pure_exact (P : SPred σs) (Q : Prop) (hqr : Q → ⊢ₛ R) : ⊢ₛ P → ⌜Q⌝ → R := by + mintro HP HQ + mcases HQ with ⌜hQ⌝ + mexact hqr hQ + +theorem and (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ R := by + mintro HPQR + mcases HPQR with ⟨HP, HQ, HR⟩ + mexact HR + +theorem and_clear_pure (P Q R : SPred σs) (φ : Prop) : (P ∧ Q ∧ ⌜φ⌝ ∧ R) ⊢ₛ R := by + mintro HPQR + mcases HPQR with ⟨_, -, ⌜hφ⌝, HR⟩ + mexact HR + +theorem or (P Q R : SPred σs) : P ∧ (Q ∨ R) ∧ (Q → R) ⊢ₛ R := by + mintro H + mcases H with ⟨-, ⟨HQ | HR⟩, HQR⟩ + · mspecialize HQR HQ + mexact HQR + · mexact HR + +theorem and_persistent (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ R := by + mintro HPQR + mcases HPQR with ⟨#HP, HQ, □HR⟩ + mexact HR + +theorem and_pure (P Q R : Prop) : (⌜P⌝ ∧ ⌜Q⌝ ∧ ⌜R⌝) ⊢ₛ (⌜R⌝ : SPred σs) := by + mintro HPQR + mcases HPQR with ⟨%HP, ⌜HQ⌝, HR⟩ + mpure_intro + exact HR + +end cases + +namespace introforall + +theorem beta_conj (P Q R : SPred (Nat::σs)) (H : ∀ n, P n ∧ Q n ⊢ₛ R n) : P ∧ Q ⊢ₛ R := by + mintro ⟨HP, HQ⟩ ∀s + mstop + exact H s + +end introforall + +namespace refine + +theorem and (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by + mintro ⟨HP, HQ, HR⟩ + mrefine ⟨HP, HR⟩ + +theorem exists_1 (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by + mintro H + mrefine ⟨⌜42⌝, H⟩ + +theorem exists_2 (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by + mintro H + mexists 42 + +end refine + +theorem mosel1 {α : Type} (P : SPred σs) (Φ Ψ : α → SPred σs) : + P ∧ (∃ a, Φ a ∨ Ψ a) ⊢ₛ ∃ a, (P ∧ Φ a) ∨ (P ∧ Ψ a) := by + mintro ⟨HP, ⟨a, ⟨HΦ | HΨ⟩⟩⟩ + · mexists a + mleft + mrefine ⟨HP, HΦ⟩ + · mexists a + mright + mrefine ⟨HP, HΨ⟩ + +theorem mosel3 {α : Type} (P : SPred σs) (Φ Ψ : α → SPred σs) : + P ∧ (∃ a, Φ a ∨ Ψ a) ⊢ₛ ∃ a, Φ a ∨ (P ∧ P ∧ Ψ a) := by + mintro ⟨HP, ⟨a, ⟨HΦ | HΨ⟩⟩⟩ + · mexists a + mleft + mexact HΦ + · mexists a + mright + mrefine ⟨HP, HP, HΨ⟩