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