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

Stream: new members

[Lars Ericson]

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]

intro hap,

[Lars Ericson]

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]

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]

show r, from X is just a really long-winded way of saying X

[Lars Ericson]

@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