Draft tactic hangs for some particular cases of have #186

New Issue

aniva · 2025-04-08T12:01:03-07:00

aniva commented

2025-04-08 12:01:03 -07:00

e.g. (taken from PyP)

root = """
theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry
"""

sketch = """
by
  -- Consider some n and m in Nats.
  intros n m
  -- Perform induction on n.
  induction n with
  | zero =>
    -- Base case: When n = 0, we need to show 0 + m = m + 0.
    -- We have the fact 0 + m = m by the definition of addition.
    have h_base: 0 + m = m := sorry
    -- We also have the fact m + 0 = m by the definition of addition.
    have h_symm: m + 0 = m := sorry
    -- Combine facts to close goal
    sorry
  | succ n ih =>
    -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.
    -- By the inductive hypothesis, we have n + m = m + n.
    have h_inductive: n + m = m + n := sorry
    -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.
    have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry
    -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.
    have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry
    sorry
"""

Curiously removing have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry solves this problem.

e.g. (taken from PyP) ```python root = """ theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry """ sketch = """ by -- Consider some n and m in Nats. intros n m -- Perform induction on n. induction n with | zero => -- Base case: When n = 0, we need to show 0 + m = m + 0. -- We have the fact 0 + m = m by the definition of addition. have h_base: 0 + m = m := sorry -- We also have the fact m + 0 = m by the definition of addition. have h_symm: m + 0 = m := sorry -- Combine facts to close goal sorry | succ n ih => -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n. -- By the inductive hypothesis, we have n + m = m + n. have h_inductive: n + m = m + n := sorry -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ. have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry -- 2. then to flip m + S n to something like S (n + m) we need to use the IH. have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry sorry """ ``` Curiously removing `have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry` solves this problem.

aniva added this to the 0.3 milestone 2025-04-08 12:01:03 -07:00

aniva added the

labels 2025-04-08 12:01:03 -07:00

aniva self-assigned this 2025-04-08 12:01:03 -07:00

aniva commented

2025-04-08 12:09:54 -07:00

This seems to be a problem with PyP and repl interaction. Could not repro with this

options.set {"timeout": 1000}
options.set {"printDependentMVars": true}
frontend.process {"file": "\ntheorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry\n", "invocations": false, "sorrys": true, "newConstants": false, "readHeader": false, "inheritEnv": false, "typeErrorsAsGoals": false}
goal.tactic {"stateId": 0, "goalId": 0, "draft": "\nby\n  -- Consider some n and m in Nats.\n  intros n m\n  -- Perform induction on n.\n  induction n with\n  | zero =>\n    -- Base case: When n = 0, we need to show 0 + m = m + 0.\n    -- We have the fact 0 + m = m by the definition of addition.\n    have h_base: 0 + m = m := sorry\n    -- We also have the fact m + 0 = m by the definition of addition.\n    have h_symm: m + 0 = m := sorry\n    -- Combine facts to close goal\n    sorry\n  | succ n ih =>\n    -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.\n    -- By the inductive hypothesis, we have n + m = m + n.\n    have h_inductive: n + m = m + n := sorry\n    -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.\n    have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry\n    -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.\n    have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry\n    -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.\n    have h1 : Nat.succ n + m = Nat.succ (n + m) := sorry\n    -- Combine facts to close goal\n    sorry\n"}

This seems to be a problem with PyP and repl interaction. Could not repro with this ``` options.set {"timeout": 1000} options.set {"printDependentMVars": true} frontend.process {"file": "\ntheorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry\n", "invocations": false, "sorrys": true, "newConstants": false, "readHeader": false, "inheritEnv": false, "typeErrorsAsGoals": false} goal.tactic {"stateId": 0, "goalId": 0, "draft": "\nby\n -- Consider some n and m in Nats.\n intros n m\n -- Perform induction on n.\n induction n with\n | zero =>\n -- Base case: When n = 0, we need to show 0 + m = m + 0.\n -- We have the fact 0 + m = m by the definition of addition.\n have h_base: 0 + m = m := sorry\n -- We also have the fact m + 0 = m by the definition of addition.\n have h_symm: m + 0 = m := sorry\n -- Combine facts to close goal\n sorry\n | succ n ih =>\n -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.\n -- By the inductive hypothesis, we have n + m = m + n.\n have h_inductive: n + m = m + n := sorry\n -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.\n have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry\n -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.\n have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry\n -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.\n have h1 : Nat.succ n + m = Nat.succ (n + m) := sorry\n -- Combine facts to close goal\n sorry\n"} ```

aniva commented

2025-04-09 00:21:52 -07:00

Can't repro.

aniva closed this issue

2025-04-09 00:21:52 -07:00

Sign in to join this conversation.