Metavariable not found bug with sorry collection #103

New Issue

aniva · 2024-10-02T16:55:45-07:00

aniva commented

2024-10-02 16:55:45 -07:00

Collecting sorrys from this:

theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := 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
     -- 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.
     have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry
     -- Combine facts to close goal
     sorry

results in unknown metavariable '?_uniq.123'

A simpler example:

theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by
   -- We have the fact of addition n + (m + 1) = (n + m) + 1, use it to show left and right are equal.
   have h_nat_add_succ: ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := sorry
   -- Combine facts to close goal
   sorry

gives

⊢ ∀ (n m : Nat), n + (m + 1) = n + m + 1

which is incorrect since only one goal's generated and there are two sorrys.

Collecting `sorry`s from this: ```lean theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := 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 -- 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. have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry -- Combine facts to close goal sorry ``` results in `unknown metavariable '?_uniq.123'` A simpler example: ```lean theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by -- We have the fact of addition n + (m + 1) = (n + m) + 1, use it to show left and right are equal. have h_nat_add_succ: ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := sorry -- Combine facts to close goal sorry ``` gives ``` ⊢ ∀ (n m : Nat), n + (m + 1) = n + m + 1 ``` which is incorrect since only one goal's generated and there are two `sorry`s.

aniva added this to the TACAS '25 milestone 2024-10-02 16:55:45 -07:00

aniva added the

labels 2024-10-02 16:55:45 -07:00

aniva self-assigned this 2024-10-02 16:55:45 -07:00

aniva referenced a pull request that will close this issue

2024-10-03 01:31:02 -07:00

feat: Collect holes in Lean file and put them into a `GoalState` #99