defining a predicate

Stream: new members

[Patrick Thomas]

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]

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

[Johan Commelin]

This is certainly possible.

[Johan Commelin]

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]

Thank you.

[Johan Commelin]

Are you using mathlib?

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Thomas]

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]

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

[Patrick Thomas]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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]

Thank you! This has helped.