## Stream: new members

### Topic: defining a predicate

#### Patrick Thomas (Nov 26 2018 at 04:54):

Hi,

I do not have a lot of experience using computer theorem provers, and I have just started trying to learn Lean. As practice I am attempting to formalize and prove that the Principle of Induction implies the Principle of Induction from a Starting Point. So far I have:

open nat

-- Principle of Induction -> Principle of Induction from a Starting Point
example : ( forall P : nat -> Prop, ( ( P 0 /\ ( forall n, ( P n -> P (n + 1) ) ) ) -> ( forall n, P n ) ) ) -> ( forall Q : nat -> Prop, forall m, ( ( Q m /\ ( forall n, ( ( n >= m ) -> ( Q n -> Q (n + 1) ) ) ) ) -> ( forall n, ( ( n >= m ) -> Q n ) ) ) ) :=
assume a1 : forall P : nat -> Prop, ( ( P 0 /\ ( forall n, ( P n -> P (n + 1) ) ) ) -> ( forall n, P n ) ),
assume Q : nat -> Prop,
assume m : nat,
assume a2 : ( Q m /\ ( forall n, ( ( n >= m ) -> ( Q n -> Q (n + 1) ) ) ) ),
have s1 : Q m, from and.left a2,
have s2 : forall n, ( ( n >= m ) -> ( Q n -> Q (n + 1) ) ), from and.right a2,
have s3 : forall n, ( Q (n + m) -> Q ((n + m) + 1) ), from
assume n : nat,
have s4 : ( ( (n + m) >= m ) -> ( Q (n + m) -> Q ((n + m) + 1) ) ), from s2 (n + m),
have s5 : (n + m) >= m, from sorry,
show ( Q (n + m) -> Q ((n + m) + 1) ), from s4 s5,

-- define P' n to hold if and only if Q (m + n) holds
-- then P' 0 holds by s1, and forall n, ( P' n -> P' (n + 1) ) holds by s3
-- then forall n, P' n holds by a1
-- then Q (m + n) holds for all n
-- then Q holds for all n >= m


I am currently trying to define a predicate P' n : nat -> Prop that holds if and only if the predicate Q holds for m + n. Is there any chance that someone could show me how this can be done?

Thank you very much for your time,
Patrick

#### Johan Commelin (Nov 26 2018 at 05:12):

Hi @Patrick Thomas Welcome to Lean (and Zulip).

#### Johan Commelin (Nov 26 2018 at 05:13):

This is certainly possible.

#### Johan Commelin (Nov 26 2018 at 05:14):

By the way (depending on taste) you can make your code a bit more readable by using unicode.
For example, you can type \and or \to to get nice symbols for /\ and ->.

Thank you.

#### Johan Commelin (Nov 26 2018 at 05:15):

Are you using mathlib?

#### Johan Commelin (Nov 26 2018 at 05:15):

Because there must be some lemma in data/nat/basic.lean that will tell you that (n - m) + m = n if n ≥ m.

#### Patrick Thomas (Nov 26 2018 at 05:17):

No. I just read about it a couple of minutes ago actually.

#### Johan Commelin (Nov 26 2018 at 05:17):

Aah, it will be very helpful. There's tons of useful little facts in there.

#### Johan Commelin (Nov 26 2018 at 05:17):

Do you have a CS or a maths background, or both?

#### Patrick Thomas (Nov 26 2018 at 05:24):

I did an undergraduate degree in CS and physics, and have a strong interest in math. I started studying mathematical logic about a year ago in an attempt to understand computer proof assistants.

#### Johan Commelin (Nov 26 2018 at 05:27):

Ok, cool. There's a nice mix of CS and math in this community.

#### Patrick Thomas (Nov 26 2018 at 05:51):

Because there must be some lemma in data/nat/basic.lean that will tell you that (n - m) + m = n if n ≥ m.

I'm sorry, I'm not certain how I would use this in the proof. Is this in relation to step s5?

#### Johan Commelin (Nov 26 2018 at 06:22):

@Patrick Thomas I would first state something like let P' : Prop := foobar,
and then have quux : Q \iff P' := xyzzy,

#### Johan Commelin (Nov 26 2018 at 06:23):

In that latter proof you will need some lemma from mathlib, I guess.

#### Mario Carneiro (Nov 26 2018 at 08:26):

To define something in a proof, you can use let. In this case let P' := λ n, Q (m + n) will do. Here is a short proof following mathlib style. This is probably too dense for a first cut but I'm sure someone around here can unpack this a bit.

example
(H : ∀ P : nat → Prop, P 0 → (∀ n, P n → P (n + 1)) → ∀ n, P n)
(Q : nat → Prop) (m)
(h₁ : Q m) (h₂ : ∀ n ≥ m, Q n → Q (n + 1)) (n) (mn : n ≥ m) : Q n :=
let P' := λ n, Q (m + n) in
have P' (n - m), from H P' h₁ (λ n, h₂ _ (nat.le_add_right m n)) (n - m),
by simp [P'] at this; rwa nat.add_sub_cancel' mn at this


#### Kevin Buzzard (Nov 26 2018 at 08:29):

simp [P'] at this is using Lean's inbuilt simplifier to do a lot of dirty work involving equalities; rwa means "rewrite, then use an assumption". Both simp and rw are talked about in Theorem Proving in Lean, in the chapter on tactics: https://leanprover.github.io/theorem_proving_in_lean/tactics.html

#### Patrick Thomas (Nov 28 2018 at 05:48):

Thank you! This has helped.

Last updated: May 11 2021 at 23:11 UTC