How to formalize recursion theorem?

Stream: maths

[Rui Liu]

I have defined natural numbers with Peano axioms, rather than inductive types. Any hint on how to formalize natural number recursion theorem from this framework?

The reference book I got is Elements of Set Theory, in which the recursion theorem is proved by taking union of functions. This operation doesn't seem to be very native in type theory language. Is there any other way to formalize it?

[Johan Commelin]

@Rui Liu Could you share some code? That will make it easier to help you.

[Rui Liu]

Johan Commelin said:

Rui Liu Could you share some code? That will make it easier to help you.

I have defined the following code for Peano axioms:

constant Nat: Type
constant Zero: Nat
constant Successor: Nat → Nat
constant AxiomNat1: ∀n:Nat, Successor n ≠ Zero
constant AxiomNat2: ∀n:Nat, ∀m:Nat, Successor n = Successor m → n = m
constant AxiomNat3: ∀P: Nat → Prop, (P Zero ∧ ∀n:Nat, P n → P (Successor n)) → ∀n:Nat, P n

Now I would like to prove the recursion theorem, which takes a:A and f: A → A, to get a unique recursion function g on Nat.

theorem recursion: ∀A:Type, Πa:A, Πf:(A → A), ∃g: Nat → A, (g Zero = a ∧ ∀n:Nat, g (Successor n) = f (g n)) := sorry

I know a proof in documented in "Elements of Set Theory" but that's too heavily based on sets and feel unnatural to do in type theory (not even sure if it will work). Is there a more natural way to prove it in type theory that only uses the axioms above without resorting to inductive types?

[Reid Barton]

I think you can approach the problem like this:

• there's no way we can produce the required function g directly, so we have to use (unique) choice to obtain it from its graph
• so let's try to produce the relation r : Nat -> A -> Prop which is supposed to be the graph of g
• now if we used the inductive type nat, we could define r as an inductive predicate with two constructors r 0 a and r n x -> r (n+1) (f x)
• by a general procedure, we can replace the inductive description of this predicate by the following "impredicative" one: take the intersection of all relations s satisfying s 0 a and forall n x, s n x -> s (n + 1) (f x), and call it r
• now try to prove by induction on n that this r is the graph of a function g
• since it satisfies the conditions r 0 a and r n x -> r (n+1) (f x) (basically by definition) we conclude the function g will satisfy the desired recurrence relation.

[Reid Barton]

in the next to last point by "is the graph of a function" I just mean that for each n, there is a unique y such that r n y

[Reid Barton]

Probably you could approximate the relation r "from below" rather than "from above", as well

[Mario Carneiro]

If you want a minimal addition to your setup that allows you to construct such functions, I suggest adding a constant the : unique A -> A

[Mario Carneiro]

or possibly even a first order version of that to avoid needing subtypes

[Rui Liu]

Reid Barton said:

I think you can approach the problem like this:

• there's no way we can produce the required function g directly, so we have to use (unique) choice to obtain it from its graph
• so let's try to produce the relation r : Nat -> A -> Prop which is supposed to be the graph of g
• now if we used the inductive type nat, we could define r as an inductive predicate with two constructors r 0 a and r n x -> r (n+1) (f x)
• by a general procedure, we can replace the inductive description of this predicate by the following "impredicative" one: take the intersection of all relations s satisfying s 0 a and forall n x, s n x -> s (n + 1) (f x), and call it r
• now try to prove by induction on n that this r is the graph of a function g
• since it satisfies the conditions r 0 a and r n x -> r (n+1) (f x) (basically by definition) we conclude the function g will satisfy the desired recurrence relation.

How do you define "intersection of all relations", when we're working in a synthetic theory rather than reducing everything to sets?

[Reid Barton]

Intersection meaning "and", if you will. The relations are all effectively subsets of Nat \x A.

[Reid Barton]

let r : Nat -> A -> Prop := \lam n x,
\all (s : Nat -> A -> Prop), (s 0 a /\ \all n x, s n x -> s (n + 1) (f x)) -> s n x

[Rui Liu]

Reid Barton said:

let r : Nat -> A -> Prop := \lam n x,
\all (s : Nat -> A -> Prop), (s 0 a /\ \all n x, s n x -> s (n + 1) (f x)) -> s n x

Thanks and I'm trying out this approach. Intuitively with this definition I should be able to prove:

h0: r 0 a
h1: forall n x, r n x -> r (n + 1) (f x)

These properties are directly provable when we define r as intersection in set theory. However in type theory, I managed to prove h0, but I don't see how to prove h1 yet. Any ideas?

[Reid Barton]

I think just expanding everything and apply hypotheses will do it

[Reid Barton]

we know every "good" s (satisfying the inner condition) satisfies s n x, and we need to show every good s satisfies s (n+1) (f x), but by definition, for a good s, s n x implies s (n+1) (f x)

[Reid Barton]

in general, any set theory that doesn't rely on a global membership relation (like ordinals) should translate directly to type theory

[Rui Liu]

Reid Barton said:

in general, any set theory that doesn't rely on a global membership relation (like ordinals) should translate directly to type theory

I might missed something ... but the following code doesn't type check:

constant Nat: Type
constant Zero: Nat
constant Succ: Nat → Nat
constant AxiomNat1: ∀n:Nat, Succ n ≠ Zero
constant AxiomNat2: ∀n:Nat, ∀m:Nat, Succ n = Succ m → n = m
constant AxiomNat3: ∀P: Nat → Prop, (P Zero ∧ ∀n:Nat, P n → P (Succ n)) → ∀n:Nat, P n

constant A: Type
constant a: A
constant f: A → A
def r: Nat → A → Prop :=
    λ (n: Nat) (x:A),
    ∀ s: Nat → A → Prop, (s Zero a ∧ ∀ (n: Nat) (x: A), s n x → s (Succ n) (f x)) → s n x

theorem h0: r Zero a :=
    assume s: Nat → A → Prop,
    assume h: s Zero a ∧ ∀ n x, s n x → s (Succ n) (f x),
    and.elim_left h

theorem h1: ∀ n x, r n x → r (Succ n) (f x) :=
    assume n: Nat,
    assume x: A,
    assume h: r n x,
    assume s: Nat → A → Prop,
    assume h': s Zero a ∧ ∀ (n: Nat) (x: A), s n x → s (Succ n) (f x),
    and.elim_right h' n x h

[Reid Barton]

You're using term mode = challenge mode.

theorem h1: ∀ n x, r n x → r (Succ n) (f x) :=
    assume n: Nat,
    assume x: A,
    assume h: r n x,
    assume s: Nat → A → Prop,
    assume h': s Zero a ∧ ∀ (n: Nat) (x: A), s n x → s (Succ n) (f x),
    begin
      apply h'.2,
      apply h,
      exact h',
    end

[Reid Barton]

Or in term mode, it's easier if you keep the proof type checking aside from holes (_).

[Rui Liu]

@Reid Barton

Thank you! I just spent like an hour staring at screen...

Or in term mode, it's easier if you keep the proof type checking aside from holes (_).

How do you do this?

Also you mentioned that it's also possible to approximate from below, can you elaborate how would you do with that strategy?

[Reid Barton]

e.g. after all the assumes, put _

[Reid Barton]

then only replace the _ by some other term with a hole that still type checks, like h'.2 _

[Reid Barton]

Rui Liu said:

Also you mentioned that it's also possible to approximate from below, can you elaborate how would you do with that strategy?

Something like: take the union of all relations s such that

• if s 0 x, then x = a
• if s (n+1) y, then there exists x with s n x and y = f x

[Rui Liu]

Reid Barton said:

Rui Liu said:

Also you mentioned that it's also possible to approximate from below, can you elaborate how would you do with that strategy?

Something like: take the union of all relations s such that

• if s 0 x, then x = a
• if s (n+1) y, then there exists x with s n x and y = f x

Sorry but how do you do union of relations in type theory?

[Reid Barton]

\exists

[Mario Carneiro]

I don't think this proof works, because to show the relation is not trivial you have to first prove the theorem

[Rui Liu]

Thanks for the help from everyone! I finally got this theorem formalized using @Reid Barton 's idea! This is so much more involved than informal proof, since I need to find out all the details to derive a simple property and find the correct way to invoke them in type theory. This makes me realize how much implicit formula manipulation that's happening in mind without realizing them.... Also, after several levels deep inside the proof, I don't see a good way to name the proof terms and bookkeeping them any more... All the important steps and non-important steps are all listed together, which doesn't give a good high level overview. I'd like to try tactics mode at some point and I don't know if they will solve some of the problems above.

Here's the proof (also here a reference on the proof http://math.iisc.ernet.in/~gadgil/BasicAnalysis/blog/2016/01/08/natural-numbers-axioms/) for anyone interested:

open classical

constant Nat: Type
constant Zero: Nat
constant Succ: Nat → Nat
constant AxiomNat1: ∀n:Nat, Succ n ≠ Zero
constant AxiomNat2: ∀n:Nat, ∀m:Nat, Succ n = Succ m → n = m
constant AxiomNat3: ∀{P: Nat → Prop}, (P Zero ∧ ∀n:Nat, P n → P (Succ n)) → ∀n:Nat, P n

def Unique: Π {S: Type}, Π P: S → Prop, Prop := λ (S: Type)(P: S → Prop), ∃x:S, P x ∧ ∀y:S, P y → y = x
def UniqueIntro: ∀ {A: Type}, ∀ {P: A → Prop}, ∀ (a: A), ∀ (h0: P a), ∀ (h1: ∀ b: A, P b → b = a), Unique P :=
    λ (A: Type) (P: A → Prop) (a: A) (h0: P a) (h1: ∀ b: A, P b → b = a), exists.intro a (and.intro h0 h1)
constant UniqueObj: Π {S: Type}, Π {P: S → Prop}, Unique P → S
constant UniqueProp: Π {S: Type}, Π {P: S → Prop}, Π (h: Unique P), P (UniqueObj h)
def UniqueEq: Π {S: Type}, Π {P: S → Prop}, Π {a b: S}, Unique P → P a → P b → a = b :=
    assume S: Type,
    assume P: S → Prop,
    assume a b: S,
    assume h: Unique P,
    assume ha: P a,
    assume hb: P b,
    exists.elim h (
        assume x: S,
        assume h: P x ∧ ∀ (y : S), P y → y = x,
        let ea: a = x := and.elim_right h a ha in
        let eb: b = x := and.elim_right h b hb in
        (eq.trans ea (eq.symm eb))
    )

theorem NotAnd: ∀ {P Q: Prop}, ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) :=
    assume P Q: Prop,
    assume h: ¬ (P ∧ Q),
    by_cases (
        assume p: P,
        by_cases (
            assume q: Q,
            absurd (and.intro p q) h
        ) (
            assume q: ¬ Q,
            or.intro_right _ q
        )
    ) (
        assume p: ¬ P,
        or.intro_left _ p
    )

theorem NotOr: ∀ {P Q: Prop}, ¬ (P ∨ Q) → (¬ P ∧ ¬ Q) :=
    assume P Q: Prop,
    assume h: ¬ (P ∨ Q),
    let np: ¬P := (assume p: P, h (or.intro_left _ p)) in
    let nq: ¬Q := (assume q: Q, h (or.intro_right _ q)) in
    and.intro np nq

theorem NotPOrQ: ∀ {P Q: Prop}, ¬ P ∨ Q → (P → Q) :=
    assume P Q: Prop,
    assume h: ¬P ∨ Q,
    assume p: P,
    or.elim h (
        assume notP: ¬P,
        absurd p notP
    ) (
        assume q: Q,
        q
    )

theorem NeSymm: ∀ {A:Type}, ∀ {a b:A}, a ≠ b → b ≠ a :=
    assume A:Type,
    assume a: A,
    assume b: A,
    assume h: a ≠ b,
    assume hh: b = a,
    h (eq.symm hh)

theorem NeNot: ∀ {A:Type}, ∀ {a b:A}, ¬ a ≠ b → a = b :=
    assume A: Type,
    assume a b: A,
    assume h: ¬ a ≠ b,
    by_contradiction (
        assume nh: a ≠ b,
        h nh
    )

theorem Recursion: ∀A:Type, Πa:A, Πf:(A → A), ∃g: Nat → A, (g Zero = a ∧ ∀n:Nat, g (Succ n) = f (g n)) :=
assume A: Type,
assume a: A,
assume f: A → A,
let r: Nat → A → Prop :=
    λ (n: Nat) (x:A),
    ∀ s: Nat → A → Prop, (s Zero a ∧ ∀ (n: Nat) (x: A), s n x → s (Succ n) (f x)) → s n x
in
let r0: r Zero a :=
    assume s: Nat → A → Prop,
    assume h: s Zero a ∧ ∀ n x, s n x → s (Succ n) (f x),
    and.elim_left h
in
let r1: ∀ n x, r n x → r (Succ n) (f x) :=
    assume n: Nat,
    assume x: A,
    assume h: r n x,
    assume s: Nat → A → Prop,
    assume h': s Zero a ∧ ∀ (n: Nat) (x: A), s n x → s (Succ n) (f x),
    and.elim_right h' n x (h s h')
in
let unique_zero: Unique (λ x: A, r Zero x) :=
    let unique: ∀b:A, r Zero b → b = a :=
        assume b:A,
        assume h: r Zero b,
        by_contradiction(
            assume b_ne_a: b ≠ a,
            let r' : Nat → A → Prop :=
                λ (n: Nat) (x: A),
                r n x ∧ (Zero ≠ n ∨ b ≠ x)
            in
            let r'0 : r' Zero a :=
                and.intro r0 (or.intro_right _ b_ne_a)
            in
            let r'1 : ∀ (n:Nat)(x:A), r' n x → r' (Succ n) (f x) :=
                assume n: Nat,
                assume x: A,
                assume r'_n_x: r' n x,
                let r_n_x: r n x := and.elim_left r'_n_x in
                let r_succ_n_f_x: r (Succ n) (f x) := r1 n x r_n_x in
                and.intro r_succ_n_f_x (or.intro_left (b ≠ f x) (NeSymm (AxiomNat1 n)))
            in
            let r'_zero_b : r' Zero b :=
                h r' (and.intro r'0 r'1)
            in
            or.elim (and.elim_right r'_zero_b)
                (assume f: Zero ≠ Zero, f (eq.refl Zero))
                (assume f: b ≠ b, f (eq.refl b))
        )
    in
    UniqueIntro a r0 unique
in
let unique_succ: ∀ n:Nat, Unique (λ x:A, r n x) → Unique (λ x:A, r (Succ n) x) :=
    assume n:Nat,
    assume h: Unique (λ x:A, r n x),
    let x: A := UniqueObj h in
    let r_n_x: r n x := UniqueProp h in
    let r_succ_n_f_x: r (Succ n) (f x) := r1 n x r_n_x in
    let unique: ∀ b:A, r (Succ n) b → b = (f x) :=
        assume b:A,
        assume r_succ_n_b: r (Succ n) b,
        by_contradiction(
            assume b_ne_x: b ≠ (f x),
            let r' : Nat → A → Prop :=
                λ (n': Nat) (x': A),
                r n' x' ∧ ((Succ n) ≠ n' ∨ b ≠ x')
            in
            let r'0 : r' Zero a :=
                and.intro r0 (or.intro_left _ (AxiomNat1 n))
            in
            let r'1 : ∀ (n':Nat)(x':A), r' n' x' → r' (Succ n') (f x') :=
                assume n': Nat,
                assume x': A,
                assume r'_n'_x': r' n' x',
                let r_n'_x': r n' x' := and.elim_left r'_n'_x' in
                let r_succ_n'_f_x': r (Succ n') (f x') := r1 n' x' r_n'_x' in
                let r'_succ_n'_f_x': r' (Succ n') (f x') := by_contradiction(
                    assume hh: ¬ (r' (Succ n') (f x')),
                    let hh': (¬ ((Succ n) ≠ (Succ n')) ∧ ¬ (b ≠ (f x'))) := NotOr (NotPOrQ (NotAnd hh) r_succ_n'_f_x') in
                    let eq1: Succ n = Succ n' := NeNot (and.elim_left hh') in
                    let eq2: b = f x' := NeNot (and.elim_right hh') in
                    let eq3: n = n' := AxiomNat2 n n' (eq1) in
                    let r_n_x': r n x' := eq.subst (eq.symm eq3) r_n'_x' in
                    let eq4: x = x' := UniqueEq h r_n_x r_n_x' in
                    let eq5: f x = f x' := congr_arg f eq4 in
                    b_ne_x (eq.trans eq2 (eq.symm eq5))
                ) in
                r'_succ_n'_f_x'
            in
            let r'_false : r' (Succ n) b :=
                r_succ_n_b r' (and.intro r'0 r'1)
            in
            or.elim (and.elim_right r'_false)
                (assume f: Succ n ≠ Succ n, f (eq.refl (Succ n)))
                (assume f: b ≠ b, f (eq.refl b))
        )
    in
    UniqueIntro (f x) r_succ_n_f_x unique
in
let unique_all: ∀ n:Nat, Unique (λ x:A, r n x) :=
    AxiomNat3 (and.intro unique_zero unique_succ)
in
let g: Π n:Nat, A := λ n:Nat, UniqueObj (unique_all n) in
let h0: g Zero = a :=
    let h: r Zero (g Zero) := UniqueProp unique_zero in
    UniqueEq unique_zero h r0
in
let h1: ∀ (n:Nat), g (Succ n) = f (g n) :=
    assume n:Nat,
    let h0: r (Succ n) (g (Succ n)) := UniqueProp (unique_all (Succ n)) in
    let h1: r (Succ n) (f (g n)) := r1 n (g n) (UniqueProp (unique_all n)) in
    UniqueEq (unique_all (Succ n)) h0 h1
in
exists.intro g (and.intro h0 h1)

[Kevin Buzzard]

You definitely want to try either proper term mode or tactic mode!

[Rui Liu]

@Kevin Buzzard What's proper term mode?

[Reid Barton]

I guess Kevin means a far more concise version of term mode. Using things like ⟨a, b⟩ instead of and.intro a b, h.2 instead of and.elim_right h, λ n x h s h', instead of five lines of assume.

[Reid Barton]

This proof looks like some kind of compiler intermediate language where there are only three constructs left--assume, let and function application.

[Kevin Buzzard]

theorem h1: ∀ n x, r n x → r (Succ n) (f x) :=
λ _ _ h _ h', h'.2 _ _ $ h _ $ h'

[Kevin Buzzard]

theorem NeNot: ∀ {A:Type}, ∀ {a b:A}, ¬ a ≠ b → a = b :=
begin
  finish
end

[Kevin Buzzard]

theorem NeSymm: ∀ {A:Type}, ∀ {a b:A}, a ≠ b → b ≠ a :=
begin
  library_search
end

[Kevin Buzzard]

theorem NotPOrQ: ∀ {P Q: Prop}, ¬ P ∨ Q → (P → Q) :=
begin
  tauto
end

[Kevin Buzzard]

(the latter three only work with import tactic at the top of your file, and working in a project with mathlib as a dependency)

[Reid Barton]

I guess maybe part of the exercise was to use almost nothing even from the core library.

[Kevin Buzzard]

theorem NotPOrQ  {P Q: Prop} (hn : ¬ P ∨ Q) (hp : P) : Q :=
begin
  cases hn,
  { contradiction },
  { assumption }
end

[Reid Barton]

Actually I think starting out with this style can be good if you have the stomach for it, because then as you learn more (syntax, library functions, tactics) you can understand how they work at this level.

[Kevin Buzzard]

Clearly Jeremy thinks the same way, or he wouldn't have written TPIL like that.

[Adam Topaz]

Rui Liu said:

Kevin Buzzard What's proper term mode?

Just like in math, "proper" = "compact" :)

[Rui Liu]

@Kevin Buzzard That's short :sweat: , what's good resource to learn more about tactics and more utilities? I know this https://leanprover.github.io/theorem_proving_in_lean/tactics.html , any more?

I guess maybe part of the exercise was to use almost nothing even from the core library.

@Reid Barton That was indeed the intention. I started to learn about type theory, then got interested in how to formalize maths in type theory. So I was deliberately not using any tools.

Btw, how do you manage proof term variables? I was struggling to give sensible names to it. Or is it when you're using more advanced tactic modes, you usually don't need to write proof variables?

[Kevin Buzzard]

More tactics here: https://leanprover-community.github.io/mathlib_docs/tactics.html . But many of these tactics need the maths library mathlib.

[Mario Carneiro]

Rui Liu said:

Btw, how do you manage proof term variables? I was struggling to give sensible names to it. Or is it when you're using more advanced tactic modes, you usually don't need to write proof variables?

You can inline the use of a variable if it appears only once. That way you only have to focus on the "interesting" subgoals. In tactic mode, if you use have without a name it gets the default name this, which is also useful if your proof is somewhat linear and you just keep shadowing the name

[Mario Carneiro]

@Rui Liu Here's a conversion of your proof to tactic style (keeping the original proof structure, i.e. no fancy tactics like finish or even rw). I have also tried to use mathlib style elsewhere.

import tactic

constant Nat : Type
constant Zero : Nat
constant Succ : Nat → Nat
constant AxiomNat1 : ∀n, Succ n ≠ Zero
constant AxiomNat2 {n m} : Succ n = Succ m → n = m
constant AxiomNat3 {P : Nat → Prop} : P Zero ∧ (∀n, P n → P (Succ n)) → ∀n, P n

def Unique {S : Type} (P : S → Prop) : Prop := ∃ x, P x ∧ ∀ y, P y → y = x
theorem UniqueIntro {A : Type} {P : A → Prop}
  (a : A) (h0 : P a) (h1 : ∀ b : A, P b → b = a) : Unique P := ⟨a, h0, h1⟩
constant UniqueObj {S : Type} {P : S → Prop} : Unique P → S
constant UniqueProp {S : Type} {P : S → Prop} (h : Unique P) : P (UniqueObj h)
theorem UniqueEq {S : Type} {P : S → Prop} {a b : S}
  (h : Unique P) (ha : P a) (hb : P b) : a = b :=
let ⟨x, h1, h2⟩ := h in (h2 _ ha).trans (h2 _ hb).symm

theorem NotAnd {P Q : Prop} : ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) := not_and_distrib.1

theorem NotOr {P Q : Prop} : ¬ (P ∨ Q) → (¬ P ∧ ¬ Q) := not_or_distrib.1

theorem NotPOrQ {P Q : Prop} : ¬ P ∨ Q → (P → Q) := or.neg_resolve_left

theorem NeSymm {A : Type} {a b : A} : a ≠ b → b ≠ a := ne.symm

theorem NeNot {A : Type} {a b : A} : ¬ a ≠ b → a = b := not_not.1

theorem Recursion {A : Type} (a : A) (f : A → A) :
  ∃ g : Nat → A, g Zero = a ∧ ∀n : Nat, g (Succ n) = f (g n) :=
begin
  let r : Nat → A → Prop := λ n x,
    ∀ s : Nat → A → Prop,
      s Zero a ∧ (∀ (n : Nat) (x : A), s n x → s (Succ n) (f x)) → s n x,
  have r0 : r Zero a := λ s h, h.1,
  have r1 : ∀ {n x}, r n x → r (Succ n) (f x) := λ n x h s h', h'.2 _ _ (h s h'),
  suffices hu : ∀ n : Nat, Unique (λ x : A, r n x),
  { let g : Π n : Nat, A := λ n, UniqueObj (hu n),
    have pg : ∀ n, r n (g n) := λ n, UniqueProp (hu n),
    refine ⟨g, UniqueEq (hu Zero) (pg Zero) r0, λ n, _⟩,
    exact UniqueEq (hu (Succ n)) (pg (Succ n)) (r1 (pg n)) },
  refine AxiomNat3 ⟨_, λ n h, _⟩,
  { refine ⟨a, r0, λ b h, _⟩,
    apply by_contradiction (λ b_ne_a, _),
    let r' : Nat → A → Prop := λ n x, r n x ∧ (Zero ≠ n ∨ b ≠ x),
    suffices : r' Zero b,
    { obtain f | f := this.2; exact f rfl },
    refine h r' ⟨_, _⟩,
    { exact ⟨r0, or.inr b_ne_a⟩ },
    { rintro n x ⟨h1, h2⟩,
      exact ⟨r1 h1, or.inl (AxiomNat1 n).symm⟩ } },
  { let x : A := UniqueObj h,
    have px : r n x := UniqueProp h,
    refine UniqueIntro (f x) (r1 px) (λ b pb, _),
    apply by_contradiction (λ b_ne_x, _),
    let r' : Nat → A → Prop := λ n' x', r n' x' ∧ (Succ n ≠ n' ∨ b ≠ x'),
    suffices : r' (Succ n) b,
    { obtain f | f := this.2; exact f rfl },
    refine pb r' ⟨_, _⟩,
    { exact ⟨r0, or.inl (AxiomNat1 n)⟩ },
    { rintro n' x' ⟨px', h2⟩,
      apply by_contradiction (λ hh, b_ne_x _),
      have := (not_and_distrib.1 hh).neg_resolve_left (r1 px'),
      obtain ⟨h3, h4⟩ := not_or_distrib.1 this,
      cases AxiomNat2 (not_not.1 h3),
      cases not_not.1 h4,
      congr,
      obtain rfl := UniqueEq h px px',
      refl } }
end

[Yakov Pechersky]

(Isn't obtain rfl := ... a fancy tactic?)

[Mario Carneiro]

as in it keeps to axiomatically basic tactics

[Mario Carneiro]

obtain rfl is a way to write subst h, a.k.a eq.rec

[Mario Carneiro]

but I think proper use of obtain or cases is important for writing tactic proofs

[Johan Commelin]

I think obtain is relatively new (compared to intro), but I wouldn't say it's "fancy".

[Eric Wieser]

If rw is being considered fancy I'd probably consider obtain fancy too

[Kevin Buzzard]

obtain is just syntax sugar for cases, right? rw is a non-trivial extension of eq.rec.

[Reid Barton]

I think obtain+rfl is actually subst which is somehow different from cases, but I still wouldn't count it as fancy

[Rui Liu]

@Mario Carneiro Thank you for the proof! Will try using this style some time!

[Rui Liu]

@Mario Carneiro Is there a reason to prefer have over let? I saw in your proof you got several places using have instead of let

[Mario Carneiro]

Use have for proofs and let only if you want to unfold the definition in subsequent reasoning

[Mario Carneiro]

it is similar to the difference between def and theorem

[Mario Carneiro]

Really you don't need let at all in the proof, you could just construct and then destruct an existential statement

[Rui Liu]

as far as I understand, let is a more general version of have, since in the places we want to unfold body only let works? Any reason for not always using let?

what's the difference between def and theorem?

Really you don't need let at all in the proof, you could just construct and then destruct an existential statement

Are you talking about this particular proof? or something in general?

[Mario Carneiro]

in this particular proof

[Mario Carneiro]

Using let clutters up the context with := ... because it has to retain the definition, and ultimately it boils down to a substitution anyway so it's not really using the cut rule in the way have does

[Mario Carneiro]

let x := e in a becomes a [e / x] while have x := e, a becomes (\lam x, a) e

[Rui Liu]

so the reason for preferring have is let is not needed?

[Rui Liu]

oh I see, so by "clutters up the context", you mean it will create a lot more entries in the context which makes it harder to look at the hypothesis

[Mario Carneiro]

This is less true of the widget view because it hides := ... in the context, unlike the plain text view, but I'm worried about an explosion of type checking cost in some cases

[Mario Carneiro]

generally, it is useful information for lean to know that a definition will not be used later except via its type