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.

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

tactic 'contradiction' failed, metavariable has already been assigned during simp #6066

Closed
3 tasks done
TwoFX opened this issue Nov 13, 2024 · 3 comments
Closed
3 tasks done
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@TwoFX
Copy link
Member

TwoFX commented Nov 13, 2024

Prerequisites

Please put an X between the brackets as you perform the following steps:

Description

inductive Impl  where
  | inner (size : Nat) (l r : Impl)
  | leaf

inductive Balanced : Impl → Prop where
  | leaf : Balanced leaf

@[inline]
def balanceLErase (r : Impl) (hrb : Balanced r)
     : Impl :=
  match r with
  | .leaf => .leaf
  | l@(.inner _ _ _) =>
    match l with
    | .leaf => .leaf
    | r@(.inner _ ll lr) =>
        match ll, lr with
          | .inner _ _ _, .inner _ _ _ => .leaf
          | _, _ => .leaf

/--
error: tactic 'contradiction' failed, metavariable has already been assigned
size✝² size✝¹ : Nat
l✝¹ r✝¹ : Impl
size✝ : Nat
l✝ r✝ : Impl
size_eq✝⁵ size_eq✝⁴ : size✝² = size✝²
hrb✝ : Balanced (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
motive :
  (ll lr : Impl) →
    (h : Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝) = Impl.inner size✝² ll lr) →
      (h_3 :
          namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
              (Impl.inner size✝² ll lr) h =
            Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) →
        Balanced
            (namedPattern
              (namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
                (Impl.inner size✝² ll lr) h)
              (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) h_3) →
          Sort u_1
h✝ :
  namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
      (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) ⋯ =
    Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)
hrb :
  Balanced
    (namedPattern
      (namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
        (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) ⋯)
      (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) h✝)
h_1 :
  (size : Nat) →
    (l r : Impl) →
      (size_1 : Nat) →
        (l_1 r_1 : Impl) →
          (h :
              Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝) =
                Impl.inner size✝² (Impl.inner size l r) (Impl.inner size_1 l_1 r_1)) →
            (h_3 :
                namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
                    (Impl.inner size✝² (Impl.inner size l r) (Impl.inner size_1 l_1 r_1)) h =
                  Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) →
              (hrb :
                  Balanced
                    (namedPattern
                      (namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
                        (Impl.inner size✝² (Impl.inner size l r) (Impl.inner size_1 l_1 r_1)) h)
                      (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) h_3)) →
                motive (Impl.inner size l r) (Impl.inner size_1 l_1 r_1) h h_3 hrb
h_2 :
  (x x_1 : Impl) →
    (h : Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝) = Impl.inner size✝² x x_1) →
      (h_3 :
          namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
              (Impl.inner size✝² x x_1) h =
            Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) →
        (hrb :
            Balanced
              (namedPattern
                (namedPattern (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝))
                  (Impl.inner size✝² x x_1) h)
                (Impl.inner size✝² (Impl.inner size✝¹ l✝¹ r✝¹) (Impl.inner size✝ l✝ r✝)) h_3)) →
          motive x x_1 h h_3 hrb
size_eq✝³ : size✝¹ = size✝¹
l_eq✝² : l✝¹ = l✝¹
r_eq✝³ : r✝¹ = r✝¹
size_eq✝² : size✝ = size✝
l_eq✝¹ : l✝ = l✝
r_eq✝² : r✝ = r✝
size_eq✝¹ : size✝² = size✝²
r_eq✝¹ : Impl.inner size✝ l✝ r✝ = Impl.inner size✝ l✝ r✝
size_eq✝ : size✝¹ = size✝¹
l_eq✝ : l✝¹ = l✝¹
r_eq✝ : r✝¹ = r✝¹
⊢ False
-/
#guard_msgs in
theorem size_balanceLErase {r : Impl} {hrb} :
    (balanceLErase r hrb) =  .leaf := by
  rw [balanceLErase.eq_def]
  simp only []

Expected behavior: No error

Actual behavior: See above

Versions

4.15.0-nightly-2024-11-13 on live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

@TwoFX TwoFX added the bug Something isn't working label Nov 13, 2024
@nomeata
Copy link
Collaborator

nomeata commented Nov 13, 2024

(I took the liberty to slightly adjust the #mwe to show that the issue appears with simp only [], and thus isn’t related to generating or applying the equational theorem.)

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Nov 15, 2024
leodemoura added a commit that referenced this issue Nov 18, 2024
This PR fixes an issue in the `injection` tactic. This tactic may execute multiple sub-tactics. If any of them fail, we must backtrack the partial assignment.
This issue was causing the error: "`mvarId` is already assigned" in issue #6066.
The issue is not yet resolved, as the equation generator for the match expressions is failing in the example provided in this issue.
leodemoura added a commit that referenced this issue Nov 18, 2024
This PR fixes an issue in the `injection` tactic. This tactic may execute multiple sub-tactics. If any of them fail, we must backtrack the partial assignment.
This issue was causing the error: "`mvarId` is already assigned" in issue #6066.
The issue is not yet resolved, as the equation generator for the match expressions is failing in the example provided in this issue.
github-merge-queue bot pushed a commit that referenced this issue Nov 18, 2024
This PR fixes an issue in the `injection` tactic. This tactic may
execute multiple sub-tactics. If any of them fail, we must backtrack the
partial assignment. This issue was causing the error: "`mvarId` is
already assigned" in issue #6066. The issue is not yet resolved, as the
equation generator for the match expressions is failing in the example
provided in this issue.
@leodemoura
Copy link
Member

#6109 fixes a minor problem in the injection tactic exposed by this issue. The real problem is in the equation generator for match expressions. It is failing at the inner match-expression. I did not investigate the issue yet.
There is a workaround: avoid named patters such as r@(.inner _ ll lr).

@nomeata
Copy link
Collaborator

nomeata commented Nov 18, 2024

With high probability #6065 and/or #6067 will cover the issue with split, so I think we can close this after #6109. Reopen if you disagree.

@nomeata nomeata closed this as completed Nov 18, 2024
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this issue Jan 21, 2025
This PR fixes an issue in the `injection` tactic. This tactic may
execute multiple sub-tactics. If any of them fail, we must backtrack the
partial assignment. This issue was causing the error: "`mvarId` is
already assigned" in issue leanprover#6066. The issue is not yet resolved, as the
equation generator for the match expressions is failing in the example
provided in this issue.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working P-medium We may work on this issue if we find the time
Projects
None yet
Development

No branches or pull requests

4 participants