Zulip Chat Archive

Stream: maths

Topic: How to formalize recursion theorem?


view this post on Zulip Rui Liu (Nov 13 2020 at 00:15):

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?

view this post on Zulip Johan Commelin (Nov 13 2020 at 06:49):

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

view this post on Zulip Rui Liu (Nov 13 2020 at 12:31):

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?

view this post on Zulip Reid Barton (Nov 13 2020 at 13:44):

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.

view this post on Zulip Reid Barton (Nov 13 2020 at 13:46):

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

view this post on Zulip Reid Barton (Nov 13 2020 at 13:54):

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 15:33):

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 15:34):

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

view this post on Zulip Rui Liu (Nov 13 2020 at 20:50):

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?

view this post on Zulip Reid Barton (Nov 13 2020 at 20:52):

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

view this post on Zulip Reid Barton (Nov 13 2020 at 20:53):

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

view this post on Zulip Rui Liu (Nov 14 2020 at 21:12):

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?

view this post on Zulip Reid Barton (Nov 14 2020 at 21:15):

I think just expanding everything and apply hypotheses will do it

view this post on Zulip Reid Barton (Nov 14 2020 at 21:19):

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)

view this post on Zulip Reid Barton (Nov 14 2020 at 21:24):

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

view this post on Zulip Rui Liu (Nov 14 2020 at 21:28):

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

view this post on Zulip Reid Barton (Nov 14 2020 at 21:31):

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

view this post on Zulip Reid Barton (Nov 14 2020 at 21:34):

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

view this post on Zulip Rui Liu (Nov 14 2020 at 21:45):

@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?

view this post on Zulip Reid Barton (Nov 14 2020 at 21:47):

e.g. after all the assumes, put _

view this post on Zulip Reid Barton (Nov 14 2020 at 21:48):

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

view this post on Zulip Reid Barton (Nov 14 2020 at 21:55):

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

view this post on Zulip Rui Liu (Nov 14 2020 at 22:03):

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?

view this post on Zulip Reid Barton (Nov 14 2020 at 22:06):

\exists

view this post on Zulip Mario Carneiro (Nov 14 2020 at 22:16):

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

view this post on Zulip Rui Liu (Nov 15 2020 at 15:42):

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)

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 17:34):

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

view this post on Zulip Rui Liu (Nov 15 2020 at 18:08):

@Kevin Buzzard What's proper term mode?

view this post on Zulip Reid Barton (Nov 15 2020 at 18:21):

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.

view this post on Zulip Reid Barton (Nov 15 2020 at 18:22):

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

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 18:23):

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

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 18:26):

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

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 18:26):

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

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 18:27):

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

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 18:28):

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

view this post on Zulip Reid Barton (Nov 15 2020 at 18:28):

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

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 18:30):

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

view this post on Zulip Reid Barton (Nov 15 2020 at 18:30):

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.

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 18:31):

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

view this post on Zulip Adam Topaz (Nov 15 2020 at 18:50):

Rui Liu said:

Kevin Buzzard What's proper term mode?

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

view this post on Zulip Rui Liu (Nov 15 2020 at 19:01):

@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?

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 19:42):

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

view this post on Zulip Mario Carneiro (Nov 15 2020 at 22:43):

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

view this post on Zulip Mario Carneiro (Nov 15 2020 at 23:35):

@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

view this post on Zulip Yakov Pechersky (Nov 15 2020 at 23:37):

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

view this post on Zulip Mario Carneiro (Nov 15 2020 at 23:37):

as in it keeps to axiomatically basic tactics

view this post on Zulip Mario Carneiro (Nov 15 2020 at 23:38):

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

view this post on Zulip Mario Carneiro (Nov 15 2020 at 23:39):

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

view this post on Zulip Johan Commelin (Nov 16 2020 at 07:03):

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

view this post on Zulip Eric Wieser (Nov 16 2020 at 13:04):

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

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 13:45):

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

view this post on Zulip Reid Barton (Nov 16 2020 at 13:54):

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

view this post on Zulip Rui Liu (Nov 16 2020 at 19:30):

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

view this post on Zulip Rui Liu (Nov 18 2020 at 00:08):

@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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:08):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:09):

it is similar to the difference between def and theorem

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:10):

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

view this post on Zulip Rui Liu (Nov 18 2020 at 00:12):

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?

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:14):

in this particular proof

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:16):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:16):

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

view this post on Zulip Rui Liu (Nov 18 2020 at 00:24):

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

view this post on Zulip Rui Liu (Nov 18 2020 at 00:26):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:41):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:41):

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


Last updated: May 06 2021 at 17:38 UTC