Zulip Chat Archive

Stream: general

Topic: Unknown identifier, but works elsewhere


Quinn Culver (Jan 12 2023 at 18:05):

Aloha,

For some reason, I'm getting a mysterious 'unknown identifier' error.

import combinatorics.configuration
open configuration.projective_plane

open classical

universe u

variables {P L : Type u} [has_mem P L] [configuration.projective_plane P L]

lemma distinct_lines {p : P} {l₁ l₂ : L}
(h₁: p  l₁) (h₂: p  l₂)  : l₁  l₂ :=
begin
  by_contradiction,
  subst_vars,
  contradiction,
end

lemma axiom_3_alternative:  (p₁ p₂ p₃ p₄ : P),  (l : L),
  ¬(p₁  l  p₂  l  p₃  l)
   ¬(p₁  l  p₂  l  p₄  l)
   ¬(p₁  l  p₃  l  p₄  l)
   ¬(p₂  l  p₃  l   p₄  l)
  :=
  begin
    have h: (p₁ p₂ p₃ : P) (l₁ l₂ l₃ : L),
      p₁  l₂  p₁  l₃  p₂  l₁  p₂  l₂
         p₂  l₃  p₃  l₁  p₃  l₂  p₃  l₃,
      from exists_config,

    rcases h with p₁, p₂, p₃, l₁, l₂, l₃, hr⟩,
    rcases hr with h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩,

    have hl₃l₁: l₃  l₁,
      from distinct_lines h₂₃ h₂₁,

    let q := mk_point hl₃l₁,
    have hq: q  l₃  q  l₁, from mk_point_ax hl₃1₁, --ERROR here: unknown identifier 'hl₃1₁'
  end

The error message is unknown identifier 'hl₃1₁'

Mysteriously, the error-producing line, mutatis muntandis, works if I do

import combinatorics.configuration
open configuration.projective_plane

open classical

universe u

variables {P L : Type u} [has_mem P L] [configuration.projective_plane P L]

lemma distinct_lines {p : P} {l₁ l₂ : L}
(h₁: p  l₁) (h₂: p  l₂)  : l₁  l₂ :=
begin
  by_contradiction,
  subst_vars,
  contradiction,
end

lemma axiom_3_alternative:  (p₁ p₂ p₃ p₄ : P),  (l : L),
  ¬(p₁  l  p₂  l  p₃  l)
   ¬(p₁  l  p₂  l  p₄  l)
   ¬(p₁  l  p₃  l  p₄  l)
   ¬(p₂  l  p₃  l   p₄  l)
  :=
  begin
    have hl₁l₃: l₁  l₃, from distinct_lines h h₁₃,
    let q := mk_point hl₁l₃,
    have hq: q  l₁  q  l₃, from mk_point_ax hl₁l₃, --SAME LINE WORKS HERE
  end,

  begin
    sorry
  end,

Pardon me in advance for what is likely a silly oversight. :heart:

Patrick Johnson (Jan 12 2023 at 18:13):

Note the difference: hl₃1₁ and hl₃l₁


Last updated: Dec 20 2023 at 11:08 UTC