# Zulip Chat Archive

## 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 `->`

.

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

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