Goal duplication #192

New Issue

aniva · 2025-04-18T00:24:43-07:00

aniva commented

2025-04-18 00:24:43 -07:00

In Mathlib

frontend.process {"file": "open BigOperators Real Nat Topology\n\ntheorem amc12a_2019_p21 (z : ℂ) (h₀ : z = (1 + Complex.I) / Real.sqrt 2) :\n  ((∑ k : ℤ in Finset.Icc 1 12, z ^ k ^ 2) * (∑ k : ℤ in Finset.Icc 1 12, 1 / z ^ k ^ 2)) = 36 := sorry", "invocations": false, "sorrys": true, "newConstants": false, "readHeader": false, "inheritEnv": false, "typeErrorsAsGoals": false}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "ring_nf"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "ring_nf"}

State 2 has two identical goals.

Vide: https://github.com/stanford-centaur/PyPantograph/issues/97

In Mathlib ``` frontend.process {"file": "open BigOperators Real Nat Topology\n\ntheorem amc12a_2019_p21 (z : ℂ) (h₀ : z = (1 + Complex.I) / Real.sqrt 2) :\n ((∑ k : ℤ in Finset.Icc 1 12, z ^ k ^ 2) * (∑ k : ℤ in Finset.Icc 1 12, 1 / z ^ k ^ 2)) = 36 := sorry", "invocations": false, "sorrys": true, "newConstants": false, "readHeader": false, "inheritEnv": false, "typeErrorsAsGoals": false} goal.tactic {"stateId": 0, "goalId": 0, "tactic": "ring_nf"} goal.tactic {"stateId": 1, "goalId": 0, "tactic": "ring_nf"} ``` State 2 has two identical goals. Vide: https://github.com/stanford-centaur/PyPantograph/issues/97

aniva added this to the 0.3.1 milestone 2025-04-18 00:24:43 -07:00

aniva added the

labels 2025-04-18 00:24:43 -07:00

aniva self-assigned this 2025-04-18 00:24:43 -07:00

aniva referenced a pull request that will close this issue

2025-04-18 00:44:10 -07:00

fix(goal): Prevent duplication in idempotent tactics #193