# Zulip Chat Archive

## Stream: new members

### Topic: What is the equivalent of term-mode assume in tactic mode?

#### Lars Ericson (Nov 29 2020 at 00:00):

I am looking at this example from section 4.4:

```
open classical
variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop
example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
iff.intro
(assume ⟨b, (hb : p b → r)⟩,
assume h2 : ∀ x, p x,
show r, from hb (h2 b))
(assume h1 : (∀ x, p x) → r,
show ∃ x, p x → r, from
by_cases
(assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩)
(assume hnap : ¬ ∀ x, p x,
by_contradiction
(assume hnex : ¬ ∃ x, p x → r,
have hap : ∀ x, p x, from
assume x,
by_contradiction
(assume hnp : ¬ p x,
have hex : ∃ x, p x → r,
from ⟨x, (assume hp, absurd hp hnp)⟩,
show false, from hnex hex),
show false, from hnap hap)))
```

I would like to translate this to tactic mode. TPIL tells us that term-mode `assume`

is a synonym for `λ`

. The expression `assume ⟨b, (hb : p b → r)⟩`

amounts to nested lambdas with free variables `b`

and `hb`

. If I try to just copy this over to term mode as follows:

```
open classical
variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop
lemma gobwd2 : ((∀ x, p x) → r) → (∃ x, p x → r) :=
begin
assume h1 : (∀ x, p x) → r,
assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩,
end
```

then I get a bunch of errors on the `assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩,`

:

```
10:26: error:
unknown identifier 'a'
10:35: error:
unknown identifier 'h1'
10:38: error:
unknown identifier 'hap'
10:25: error:
invalid constructor ⟨...⟩, expected type is not an inductive type
tactic ?m_1
10:25: error:
don't know how to synthesize placeholder
context:
α : Type u_1,
p : α → Prop,
r : Prop
⊢ Type ?
```

What is the correct way to translate `assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩`

into tactic mode? This one is complicated because `hap`

is used in the expression.

#### Reid Barton (Nov 29 2020 at 00:08):

`intro hap,`

#### Lars Ericson (Nov 29 2020 at 01:03):

It's not a straightforward translation but I'm slowly getting it, for example `foo_tactical`

versus `foo_termical`

:

```
open classical
variables (α : Type*) (p q : α → Prop)
variable r : Prop
lemma foo_tactical : (∃ x, p x → r) → (∀ x, p x) → r :=
begin
intro h2,
cases h2 with b hb,
assume h2: ∀ x, p x,
exact hb (h2 b),
end
lemma foo_termical : (∃ x, p x → r) → (∀ x, p x) → r :=
(assume ⟨b, (hb : p b → r)⟩,
assume h2 : ∀ x, p x,
show r, from hb (h2 b))
```

#### Kevin Buzzard (Nov 29 2020 at 01:17):

```
lemma foo_termical : (∃ x, p x → r) → (∀ x, p x) → r :=
λ ⟨b, hb⟩ h2, hb (h2 b)
```

Why all this `assume`

, `show`

stuff still??

#### Kevin Buzzard (Nov 29 2020 at 01:17):

`show r, from X`

is just a really long-winded way of saying `X`

#### Lars Ericson (Nov 29 2020 at 02:42):

@Kevin Buzzard the `foo_termical`

is from TPIL, and I am learning how to translate it into tactics in `foo_tactical`

. I didn't originate `foo_termical`

. It seems I will have to graduate to term mode soon. To smooth the transition, it helps me understand both modes to be able to translate back and forth. I also learn new techniques this way. So I'm taking a proof of something hard in section 4.4 which is in term mode and translating it to tactic mode. This is taking me a while. Here is the current state of my translation, it is half way:

```
open classical
variables (α : Type*) (p q : α → Prop)
variable r : Prop
variable a : α
include a
lemma foo11 : (∃ x, p x → r) → (∀ x, p x) → r :=
begin
intro h2,
cases h2 with b hb,
assume h2: ∀ x, p x,
exact hb (h2 b),
end
lemma foo12 : ((∀ x, p x) → r ) → (∃ x, p x → r) :=
begin
intro h1,
by_cases hap: ∀ x, p x,
{ have question_mark_from_constructor_is_really_a_lambda_expression := λ h', h1 hap,
exact ⟨a, question_mark_from_constructor_is_really_a_lambda_expression⟩, },
{ by_contra hnex,
exact (have hap1 : ∀ x, p x, from
assume x,
by_contradiction
(assume hnp : ¬ p x,
have hex : ∃ x, p x → r,
from ⟨x, (assume hp, absurd hp hnp)⟩,
hnex hex),
hap hap1), },
end
lemma foo2 : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
begin
split,
exact foo11 α p r a,
exact foo12 α p r a,
end
```

For example I discovered that when I see something like `?m_1`

as a result of a `constructor`

, that is really a lambda expression where the `?m_1`

is a bound variable and the `λ ?m_1`

is elided in the goal state. I infer that from this goal state after executing

```
have question_mark_from_constructor_is_really_a_lambda_expression := λ h', h1 hap,
```

The goal state is:

```
α : Type u_1,
p : α → Prop,
r : Prop,
a : α,
h1 : (∀ (x : α), p x) → r,
hap : ∀ (x : α), p x,
question_mark_from_constructor_is_really_a_lambda_expression : ?m_1 → r
⊢ ∃ (x : α), p x → r
```

Last updated: May 12 2021 at 05:19 UTC