diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean index 882804ebbd..13e8ee7542 100644 --- a/src/Init/Ext.lean +++ b/src/Init/Ext.lean @@ -24,15 +24,16 @@ syntax extFlat := atomic("(" &"flat" " := " &"false" ")") /-- Registers an extensionality theorem. -* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers - them for the `ext` tactic. - -* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an `ext_iff` theorem. +* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an "`ext_iff`" theorem. The name of the theorem is from adding the suffix `_iff` to the theorem name. -* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`. +* When `@[ext]` is applied to a structure, it generates an `.ext` theorem and applies the `@[ext]` attribute to it. + The result is an `.ext` and an `.ext_iff` theorem with the `.ext` theorem registered for the `ext` tactic. -* The flag `@[ext (iff := false)]` prevents it from generating an `ext_iff` theorem. +* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the `ext` lemma. + Higher-priority lemmas are chosen first, and the default is `1000`. + +* The flag `@[ext (iff := false)]` disables generating an `ext_iff` theorem. * The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation, rather than flattening the parents' fields into the lemma's equality hypotheses. diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean index 982099329f..6e8dab1237 100644 --- a/src/Lean/Elab/Tactic/Ext.lean +++ b/src/Lean/Elab/Tactic/Ext.lean @@ -74,16 +74,16 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do let some (_, x, y) := ty.eq? | failNotEq let some xIdx := args.findIdx? (· == x) | failNotEq let some yIdx := args.findIdx? (· == y) | failNotEq - unless xIdx == yIdx + 1 || xIdx + 1 == yIdx do + unless xIdx + 1 == yIdx do throwError "expecting {x} and {y} to be consecutive arguments" - let startIdx := max xIdx yIdx + 1 + let startIdx := yIdx + 1 let toRevert := args[startIdx:].toArray let fvars ← toRevert.foldlM (init := {}) (fun st e => return collectFVars st (← inferType e)) for fvar in toRevert do unless ← Meta.isProof fvar do - throwError "argument {fvar} is not a proof, which is not supported" + throwError "argument {fvar} is not a proof, which is not supported for arguments after {x} and {y}" if fvars.fvarSet.contains fvar.fvarId! then - throwError "argument {fvar} is depended upon, which is not supported" + throwError "argument {fvar} is depended upon, which is not supported for arguments after {x} and {y}" let conj := mkAndN (← toRevert.mapM (inferType ·)).toList -- Make everything implicit except for inst implicits let mut newBis := #[] @@ -104,27 +104,31 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl throwError "'{structName}' is not a structure" let extName := structName.mkStr "ext" unless (← getEnv).contains extName do - Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do - let type ← mkExtType structName flat - let pf ← withSynthesize do - let indVal ← getConstInfoInduct structName - let params := Array.mkArray indVal.numParams (← `(_)) - Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false) - -- introduce the params, do cases on 'x' and 'y', and then substitute each equation - (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl)) - let pf ← instantiateMVars pf - if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}" - let info ← getConstInfo structName - addDecl <| Declaration.thmDecl { - name := extName - type - value := pf - levelParams := info.levelParams - } - modifyEnv fun env => addProtected env extName - Lean.addDeclarationRanges extName { - range := ← getDeclarationRange (← getRef) - selectionRange := ← getDeclarationRange (← getRef) } + try + Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do + let type ← mkExtType structName flat + let pf ← withSynthesize do + let indVal ← getConstInfoInduct structName + let params := Array.mkArray indVal.numParams (← `(_)) + Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false) + -- introduce the params, do cases on 'x' and 'y', and then substitute each equation + (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl)) + let pf ← instantiateMVars pf + if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}" + let info ← getConstInfo structName + addDecl <| Declaration.thmDecl { + name := extName + type + value := pf + levelParams := info.levelParams + } + modifyEnv fun env => addProtected env extName + Lean.addDeclarationRanges extName { + range := ← getDeclarationRange (← getRef) + selectionRange := ← getDeclarationRange (← getRef) } + catch e => + throwError m!"\ + Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}" return extName /-- @@ -138,29 +142,35 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do | .str n s => .str n (s ++ "_iff") | _ => .str extName "ext_iff" unless (← getEnv).contains extIffName do - let info ← getConstInfo extName - Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do - let type ← mkExtIffType extName - let pf ← withSynthesize do - Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by - intros - refine ⟨?_, ?_⟩ - · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem") - · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption) - let pf ← instantiateMVars pf - if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}" - addDecl <| Declaration.thmDecl { - name := extIffName - type - value := pf - levelParams := info.levelParams - } - -- Only declarations in a namespace can be protected: - unless extIffName.isAtomic do - modifyEnv fun env => addProtected env extIffName - Lean.addDeclarationRanges extIffName { - range := ← getDeclarationRange (← getRef) - selectionRange := ← getDeclarationRange (← getRef) } + try + let info ← getConstInfo extName + Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do + let type ← mkExtIffType extName + let pf ← withSynthesize do + Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by + intros + refine ⟨?_, ?_⟩ + · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem") + · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption) + let pf ← instantiateMVars pf + if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}" + addDecl <| Declaration.thmDecl { + name := extIffName + type + value := pf + levelParams := info.levelParams + } + -- Only declarations in a namespace can be protected: + unless extIffName.isAtomic do + modifyEnv fun env => addProtected env extIffName + Lean.addDeclarationRanges extIffName { + range := ← getDeclarationRange (← getRef) + selectionRange := ← getDeclarationRange (← getRef) } + catch e => + throwError m!"\ + Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\ + \n\ + Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem." return extIffName diff --git a/tests/lean/run/ext.lean b/tests/lean/run/ext.lean index bfbda098c5..5d423f332a 100644 --- a/tests/lean/run/ext.lean +++ b/tests/lean/run/ext.lean @@ -138,3 +138,35 @@ attribute [local ext] Subsingleton.elim /-- info: Subsingleton.elim_iff.{u} {α : Sort u} [h : Subsingleton α] {a b : α} : a = b ↔ True -/ #guard_msgs in #check Subsingleton.elim_iff end + + +/-! +More informative error (issue #4758) +-/ + +/-- +warning: declaration uses 'sorry' +--- +error: Failed to generate an 'ext_iff' theorem from 'weird_prod_ext': argument f is not a proof, which is not supported for arguments after p and q + +Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem. +-/ +#guard_msgs in +@[ext] +theorem weird_prod_ext (p q : α × β) + (f : α → α') (g : β → β') -- (hf : Function.Injective f) (hg : Function.Injective g) + (h : f p.1 = f q.1) (h' : g p.2 = g q.2) : + p = q := sorry + +/-- +error: Failed to generate an 'ext_iff' theorem from 'ext'': argument h1 is depended upon, which is not supported for arguments after p and q + +Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem. +-/ +#guard_msgs in +@[ext] +theorem Sigma.ext' {β : α → Type _} (p q : (i : α) × β i) + (h1 : p.1 = q.1) + (h2 : h1 ▸ p.2 = q.2) : + p = q := by + cases p; cases q; cases h1; cases h2; rfl