beginner's problem [nightly]

Stream: lean4

[Aron]

import Mathlib.Logic.Basic
-- def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

-- syntax "∃!" term "," term: term
-- macro_rules
-- | `(∃! $t:term, $p:term) => `(exunique (fun $t => $p))

class incidence (point line: Type) (inc:point → line → Prop) :=
(one: ∀ P Q, P ≠ Q → ∃! l, inc P l ∧ inc Q l)
(two: ∀ l, ∃ P Q, P ≠ Q ∧ inc P l ∧ inc Q l)
(three: ∃ P Q R, P ≠ Q ∧ Q ≠ R ∧ P ≠ R ∧ ∀ l, ¬(inc P l ∧ inc Q l ∧ inc R l))

variable (point line:Type)
variable (inc:point → line → Prop)
variable [i: incidence point line inc]

theorem t1:
∀ l m,
l ≠ m
→ (∃ p, inc p l ∧ inc p m)
→ (∃! p, inc p l ∧ inc p m)
:= by
intro l m hlnm hex
have ⟨a,ha⟩:= hex
refine ⟨a, ha, λ b hb => ?_⟩
-- apply Classical.byContradiction; intro hanb
refine Classical.byContradiction fun hanb => ?_
rewrite [eq_comm,← ne_eq] at hanb
have ⟨hal,ham⟩:=ha
have ⟨hbl,hbm⟩:=hb
have h:=i.one a b hanb
have ⟨x,hx1,hx2⟩:=h
have hl':= hx2 l ⟨hal,hbl⟩
have hm':= hx2 m ⟨ham,hbm⟩
have hlm:= Eq.trans hl' (Eq.symm hm')
-- hlm hlnm
contradiction


theorem t2: ∀ l, ∃ p, ¬ inc p l := by
intro l
have ⟨p,q,r,hpnq,hqnr,hpnr,hncol⟩ := i.three
have hnl:= hncol l
apply Classical.byContradiction
intro hallinc
rw [not_exists,not_not] at hallinc
-- have hpqrinc:= And.intro (And.intro (hallinc p) (hallinc q)) (hallinc r)

././Trying.lean:46:15: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ¬¬?m.1516
case h
point line : Type
inc : point → line → Prop
i : incidence point line inc
l : line
p q r : point
hpnq : p ≠ q
hqnr : q ≠ r
hpnr : p ≠ r
hncol : ∀ (l : line), ¬(inc p l ∧ inc q l ∧ inc r l)
hnl : ¬(inc p l ∧ inc q l ∧ inc r l)
hallinc : ∀ (x : point), ¬¬inc x l
⊢ False

[Aron]

See the last line, not_not is not matching its pattern.

[Aron]

It isn't matching ¬¬something in hallinc : ∀ (x : point), ¬¬inc x l.

[Siddhartha Gadgil]

I believe rewrite will not work inside a ∀. Here is one way to achieve what you want (replacing the last line).

rw [not_exists] at hallinc
have halinc' : ∀ (x : point), inc x l := by
   intro x
   let hx := hallinc x
   rw [not_not] at hx
   assumption

Somebody more skilled than me at tactics will probably suggest a shorter way.

[Aron]

Siddhartha Gadgil said:

I believe rewrite will not work inside a ∀. Here is one way to achieve what you want (replacing the last line).

rw [not_exists] at hallinc
have halinc' : ∀ (x : point), inc x l := by
   intro x
   let hx := hallinc x
   rw [not_not] at hx
   assumption

Somebody more skilled than me at tactics will probably suggest a shorter way.

Why doesn't the nightly build automatically collapse not_not?

[Siddhartha Gadgil]

What do you mean by "collapse not_not"?

[Aron]

It seemed like the stable build of lean4 would automatically simplify not not p into p.

[Siddhartha Gadgil]

I don't expect ¬¬something is _definitionally equal_ to something.

[Siddhartha Gadgil]

If p is a literal boolean that will happen. Did it happen with boolean expressions?

[Siddhartha Gadgil]

I don't see how one could have reflexive equality of not not p and p for arbitrary boolean expressions. The definition of not is

@[inline] def not : Bool → Bool
  | true  => false
  | false => true

which, due to _inline_, will expand for literals and so simplify. But for expressions it should just inline to a nested match.

[Aron]

I guess my lean3 examples had not_not as a simplification tactic because they were working classically.

[Siddhartha Gadgil]

That makes sense. Simplification will do all this expansion.

[Siddhartha Gadgil]

i thought "automatically" meant definitional equality.

[Siddhartha Gadgil]

I just checked: simp does work within functions, so you could simply replace your last lines with

rw [not_exists] at hallinc
simp [not_not] at hallinc

[Siddhartha Gadgil]

Better still, simp [not_exists, not_not] at hallinc does the job.

[Aron]

Alright, now I'm having trouble getting And.assoc to work the way it advertises.

[Aron]

Apparently it works fine in rw, but not as a direct application.

[Aron]

Ignore that, the problem got solved so I don't mind.

[Aron]

Alright, I've got another.

import Mathlib.Logic.Basic
-- def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

-- syntax "∃!" term "," term: term
-- macro_rules
-- | `(∃! $t:term, $p:term) => `(exunique (fun $t => $p))

class incidence (point line: Type) (inc:point → line → Prop) :=
(one: ∀ P Q, P ≠ Q → ∃! l, inc P l ∧ inc Q l)
(two: ∀ l, ∃ P Q, P ≠ Q ∧ inc P l ∧ inc Q l)
(three: ∃ P Q R, P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ∀ l, ¬(inc P l ∧ inc Q l ∧ inc R l))

variable (point line:Type)
variable (inc:point → line → Prop)
variable [i: incidence point line inc]

theorem t1:
∀ l m,
l ≠ m
→ (∃ p, inc p l ∧ inc p m)
→ (∃! p, inc p l ∧ inc p m)
:= by
intro l m hlnm hex
have ⟨a,ha⟩:= hex
refine ⟨a, ha, λ b hb => ?_⟩
-- apply Classical.byContradiction; intro hanb
refine Classical.byContradiction fun hanb => ?_
rewrite [eq_comm,← ne_eq] at hanb
have ⟨hal,ham⟩:=ha
have ⟨hbl,hbm⟩:=hb
have h:=i.one a b hanb
have ⟨x,hx1,hx2⟩:=h
have hl':= hx2 l ⟨hal,hbl⟩
have hm':= hx2 m ⟨ham,hbm⟩
have hlm:= Eq.trans hl' (Eq.symm hm')
-- hlm hlnm
contradiction

theorem t2: ∀ l, ∃ p, ¬ inc p l := by
intro l
have ⟨p,q,r,hpnq,hpnr,hqnr,hncol⟩ := i.three
have hnl:= hncol l
apply Classical.byContradiction
intro hallinc
simp [not_not,not_exists] at hallinc
have hl:= And.intro (And.intro (hallinc p) (hallinc q)) (hallinc r)
-- exact hnl (And.assoc hl)
rw [And.assoc] at hl
contradiction

theorem another_point: ∀ (p:point), ∃ q, p ≠ q:=by
intro p
have ⟨a,b,c,hanb,hanc,hbnc,habc⟩:= i.three
apply Classical.byContradiction
simp [not_exists,ne_eq]
intro h
-- exact hab (Eq.trans (eq_comm.mp (h a)) (h b))
have ha:= h a
have hb:= h b
rw [eq_comm] at ha
have hab:= Eq.trans ha hb
exact hanb hab

theorem t3: ∀ p, ∃ l m, l ≠ m ∧ inc p l ∧ inc p m := by
intro p
have h:= another_point p

././Trying.lean:66:23: error: application type mismatch
  another_point p
argument
  p
has type
  point : Type
but is expected to have type
  Type : Type 1
././Trying.lean:64:53: error: unsolved goals
point line : Type
inc : point → line → Prop
i : incidence point line inc
p : point
h :
  ∀ (line : Type) (inc : sorryAx Type → line → Prop) [i : incidence (sorryAx Type) line inc] (p : sorryAx Type),
    ∃ q, p ≠ q
⊢ ∃ l m, l ≠ m ∧ inc p l ∧ inc p m

I'm trying to apply another_point at the bottom line, but it's not typechecking.
It's also saying the type involves sorryAx - not sure what that is.

[Marc Huisinga]

If you hover over another_point, it'll show you the type of the theorem.

[Aron]

Yes, it's ∀ (line : Type) (inc : sorryAx Type → line → Prop) [i : incidence (sorryAx Type) line inc] (p : sorryAx Type), ∃ q, p ≠ q.

[Kevin Buzzard]

So it's expecting a term of type Type and you gave it a term of type point

[Kevin Buzzard]

Which is exactly what the error says

[Aron]

Why would it be expecting a term of type Type when I defined the theorem with a term of type point?

[Aron]

theorem another_point: ∀ (p:point), ∃ q, p ≠ q:=by
intro p
have ⟨a,b,c,hanb,hanc,hbnc,habc⟩:= i.three
apply Classical.byContradiction
simp [not_exists,ne_eq]
intro h
-- exact hab (Eq.trans (eq_comm.mp (h a)) (h b))
have ha:= h a
have hb:= h b
rw [eq_comm] at ha
have hab:= Eq.trans ha hb
exact hanb hab

[Sébastien Michelland]

These are your variable definitions - the theorem implicitly uses them, so they have been included as parameters. The theorem uses them in the proof; see how you mention i.three.

If you change your variable declarations to use braces, the parameters will be made implicit and automatically inferred, resulting in the behavior that you expect - if inference succeeds.

[Aron]

Oh, so if I were to keep the variables as is, I would have had to define point, line, and inc in the call to another_point. Makes sense.

[Aron]

Tried changing to braces, everything's exploding.

[Aron]

Figured out something that works without braces, but I'm not sure how I'd go about condensing it to get the definitions out of the way.

theorem another_point: ∀ (p:point), ∃ q, p ≠ q:=by
intro p
have ⟨a,b,c,hanb,hanc,hbnc,habc⟩:= i.three
apply Classical.byContradiction
simp [not_exists,ne_eq]
intro h
-- exact hab (Eq.trans (eq_comm.mp (h a)) (h b))
have ha:= h a
have hb:= h b
have hab:= Eq.trans (eq_comm.mp ha) hb
exact hanb hab

theorem t3: ∀ p, ∃ l m, l ≠ m ∧ inc p l ∧ inc p m := by
intro p
have h:= another_point point line inc p

[Sébastien Michelland]

Yes precisely. I'm not too surprised it's exploding, in my experience changing binder types is always tricky. It helps to get them right on the first try when you already know what you will be able to infer. It's also a limitation of variable that every theorem gets the same binder type.

[Marc Huisinga]

The rule of thumb is that something can be inferred if it appears in the type of a later argument.
Applying this rule to your example, we can declare variable {point line : Type} implicit, but leave inc explicit. Then you can use another_point inc p and your file typechecks without issues.

[Kevin Buzzard]

In Lean 3 you can change the binder type of a variable after it's been declared with a line such as variable {line}

[Mario Carneiro]

that also works in lean 4