Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 29 2020 at 00:08):

intro hap,

view this post on Zulip 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))

view this post on Zulip 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??

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 01:17):

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

view this post on Zulip 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