Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: fix bugs in nontriviality tactic #3175

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - chore: fix bugs in nontriviality tactic #3175

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
0735dee
feat: port Data.Polynomial.Mirror
ChrisHughes24 Mar 27, 2023
d9cd078
Initial file copy from mathport
ChrisHughes24 Mar 27, 2023
7d5d31c
automated fixes
ChrisHughes24 Mar 27, 2023
ed713fb
fix red
ChrisHughes24 Mar 27, 2023
1386974
auto: naming
ChrisHughes24 Mar 27, 2023
a5d1672
fix build
ChrisHughes24 Mar 27, 2023
a9014a2
fix nontriviality tactic
semorrison Mar 29, 2023
fc8544a
.
semorrison Mar 29, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions Mathlib/Data/Polynomial/Mirror.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,9 +69,7 @@ set_option linter.uppercaseLean3 false in
theorem mirror_natDegree : p.mirror.natDegree = p.natDegree := by
by_cases hp : p = 0
· rw [hp, mirror_zero]
--Porting note: below two lines were `nontriviality R` in Lean3
have : p.leadingCoeff ≠ 0 := by simpa
let _ : Nontrivial R := nontrivial_of_ne _ _ this
nontriviality R
rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]
rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
Expand Down
31 changes: 16 additions & 15 deletions Mathlib/Tactic/Nontriviality/Core.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,21 +29,22 @@ including `Subsingleton.le` and `eq_iff_true_of_subsingleton`.
-/
def nontrivialityByElim (α : Q(Type u)) (g : MVarId) (simpArgs : Array Syntax) : MetaM MVarId := do
let p : Q(Prop) ← g.getType
guard (← inferType p).isProp
let g₁ ← mkFreshExprMVarQ q(Subsingleton $α → $p)
let (_, g₁') ← g₁.mvarId!.intro1
g₁'.withContext try
-- FIXME: restore after lean4#2054 is fixed
-- g₁'.inferInstance <|> do
(do g₁'.assign (← synthInstance (← g₁'.getType))) <|> do
let simpArgs := simpArgs.push (Unhygienic.run `(Parser.Tactic.simpLemma| nontriviality))
let stx := open TSyntax.Compat in Unhygienic.run `(tactic| simp [$simpArgs,*])
let ([], _) ← runTactic g₁' stx | failure
catch _ => throwError
"Could not prove goal assuming `{q(Subsingleton $α)}`\n{MessageData.ofGoal g₁'}"
let g₂ : Q(Nontrivial $α → $p) ← mkFreshExprMVarQ q(Nontrivial $α → $p)
g.assign q(subsingleton_or_nontrivial_elim $g₁ $g₂)
pure g₂.mvarId!
guard (←instantiateMVars (← inferType p)).isProp
g.withContext do
let g₁ ← mkFreshExprMVarQ q(Subsingleton $α → $p)
let (_, g₁') ← g₁.mvarId!.intro1
g₁'.withContext try
-- FIXME: restore after lean4#2054 is fixed
-- g₁'.inferInstance <|> do
(do g₁'.assign (← synthInstance (← g₁'.getType))) <|> do
let simpArgs := simpArgs.push (Unhygienic.run `(Parser.Tactic.simpLemma| nontriviality))
let stx := open TSyntax.Compat in Unhygienic.run `(tactic| simp [$simpArgs,*])
let ([], _) ← runTactic g₁' stx | failure
catch _ => throwError
"Could not prove goal assuming `{q(Subsingleton $α)}`\n{MessageData.ofGoal g₁'}"
let g₂ : Q(Nontrivial $α → $p) ← mkFreshExprMVarQ q(Nontrivial $α → $p)
g.assign q(subsingleton_or_nontrivial_elim $g₁ $g₂)
pure g₂.mvarId!

/--
Tries to generate a `nontrivial α` instance using `nontrivial_of_ne` or `nontrivial_of_lt`
Expand Down