exists in hypothesis

Stream: lean4

[Aron]

I'm trying to break down an existential in a hypothesis.
Screen-Shot-2022-06-09-at-12.30.52-AM.png
How would I go about it?

[Aron]

h : ∃ x, (inc a x ∧ inc b x) ∧ ∀ (y : line), inc a y ∧ inc b y → x = y

[Aron]

In general, if I have h: exists x, p x, how do i get to two hypotheses x: domain(p) and hx: p x?

[Aron]

accidentally muted the topic. Trying to find it.

[Mario Carneiro]

cases h

[Mario Carneiro]

In that case I would probably do something like let \<x, \<ha, hb\>, H\> := h

[Aron]

I didn't even know let could be used like that, or that let is a keyword. How would I specify that an already specified element should be witness to the existential?

[Aron]

The documentation is so jank

[Aron]

In situ, I'm trying to take the following
h : ∃ x, (inc a x ∧ inc b x) ∧ ∀ (y : line), inc a y ∧ inc b y → x = y
l m: line
hl : inc a l ∧ inc b l
hm : inc a m ∧ inc b m

and produce:
hhhh : l=m

[Marcus Rossel]

@Aron: #backticks

A proof of l = m (without using tactics) could look something like:

let ⟨x, _, hy⟩ := h -- `hy` is `∀ (y : line), inc a y ∧ inc b y → x = y`
let hl' := hy l hl  -- `x = l`
let hm' := hy m hm  -- `x = m`
hl'.symm.trans hm'  -- `l = m` by combining `hl'` and `hm'`

In tactic mode it's basically the same:

have ⟨x, _, hy⟩ := h
have hl' := hy l hl
have hm' := hy m hm
exact hl'.symm.trans hm'

[Aron]

Trying it in tactic mode. Why does line 1 produce an extra copy of h as x\cross?

[Mario Carneiro]

#mwe <-- this is a link. click on it

[Mario Carneiro]

Aron said:

I didn't even know let could be used like that, or that let is a keyword. How would I specify that an already specified element should be witness to the existential?

The documentation is so jank

Have you seen https://leanprover.github.io/lean4/doc/ ? There is an example of let as a keyword on the first page

[Aron]

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))

theorem t1
(point line:Type)
(inc:point → line → Prop)
[i: incidence point line inc]:
∀ l m,
l ≠ m
→ (∃ p, inc p l ∧ inc p m)
→ (∃! p, inc p l ∧ inc p m)
:= by
intro l m hlnm hex
cases hex with | intro a ha =>
rw [exunique]
exists a
apply And.intro
exact ha
intro b hb
apply Classical.byContradiction
intro hanb
have h:= i.one a b hanb
cases ha with | intro hal ham =>
cases hb with | intro hbl hbm =>
have hl:=And.intro hal hbl
have hm:=And.intro ham hbm
rw [exunique] at h
have ⟨x, hx1, hx2⟩:= h
have hl' := hx2 l hl

Yes, but I haven't seen it in the context of a proof.

[Mario Carneiro]

Here are some minor cleanups of your proof:

theorem t1
  (point line : Type)
  (inc : point → line → Prop)
  [i : incidence point line inc] :
  ∀ 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, fun b hb => ?_⟩
  refine Classical.byContradiction fun hanb => ?_
  have h := i.one a b hanb
  have ⟨hal, ham⟩ := ha
  have ⟨hbl, hbm⟩ := hb
  have ⟨x, hx1, hx2⟩ := h
  have hl' := hx2 l ⟨hal, hbl⟩

[Mario Carneiro]

by the way I'm not seeing any x\cross in this code. Did you change the example?

[Aron]

Searching the lean4 documentation and Theorem Proving in Lean 4 doesn't show me anything about refine or ?_. Is the search button a work in progress?

[Mario Carneiro]

no but the documentation is

[Mario Carneiro]

things have improved a lot in the past 6 months but the documentation still lags a lot relative to lean 3

[Mario Carneiro]

It might help to check out the mathlib docs: https://leanprover-community.github.io/mathlib_docs/tactics.html

[Mario Carneiro]

(keeping in mind that those docs are for lean 3 and so there may be some differences or missing things in lean 4)

[Aron]

Is there a mathlib doc for lean4 available?

[Mario Carneiro]

docs4#Nat

[Mario Carneiro]

it's also a work in progress though

[Mario Carneiro]

there isn't really anything analogous to the mathlib tactics page there

[Mario Carneiro]

One way to learn the tactics is to browse library code like https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/List/Basic.lean

[Mario Carneiro]

if you want something closer to a complete listing you can look at https://github.com/leanprover/lean4/blob/master/src/Init/Tactics.lean

[Mario Carneiro]

But to answer the original question: refine is like exact except you can leave holes in the term using ?_ and they become subgoals

[Mario Carneiro]

it's very versatile, since you can use it to express apply, intro, cases or any combination of these

[Sebastian Ullrich]

refine has a docstring that should be displayed on hover